compiler/coreSyn/CoreLint.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
   4 %
   5
   6 A ``lint'' pass to check for Core correctness
   7
   8 \begin{code}
   9 module CoreLint (
  10         lintCoreBindings,
  11         lintUnfolding,
  12         showPass, endPass
  13     ) where
  14
  15 #include "HsVersions.h"
  16
  17 import NewDemand
  18 import CoreSyn
  19 import CoreFVs
  20 import CoreUtils
  21 import Bag
  22 import Literal
  23 import DataCon
  24 import TysWiredIn
  25 import Var
  26 import VarEnv
  27 import VarSet
  28 import Name
  29 import Id
  30 import PprCore
  31 import ErrUtils
  32 import SrcLoc
  33 import Type
  34 import Coercion
  35 import TyCon
  36 import BasicTypes
  37 import StaticFlags
  38 import DynFlags
  39 import Outputable
  40
  41 #ifdef DEBUG
  42 import Util             ( notNull )
  43 #endif
  44
  45 import Data.Maybe
  46 \end{code}
  47
  48 %************************************************************************
  49 %*                                                                      *
  50 \subsection{End pass}
  51 %*                                                                      *
  52 %************************************************************************
  53
  54 @showPass@ and @endPass@ don't really belong here, but it makes a convenient
  55 place for them.  They print out stuff before and after core passes,
  56 and do Core Lint when necessary.
  57
  58 \begin{code}
  59 endPass :: DynFlags -> String -> DynFlag -> [CoreBind] -> IO [CoreBind]
  60 endPass dflags pass_name dump_flag binds
  61   = do
  62         -- Report result size if required
  63         -- This has the side effect of forcing the intermediate to be evaluated
  64         debugTraceMsg dflags 2 $
  65                 (text "    Result size =" <+> int (coreBindsSize binds))
  66
  67         -- Report verbosely, if required
  68         dumpIfSet_core dflags dump_flag pass_name (pprCoreBindings binds)
  69
  70         -- Type check
  71         lintCoreBindings dflags pass_name binds
  72
  73         return binds
  74 \end{code}
  75
  76
  77 %************************************************************************
  78 %*                                                                      *
  79 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
  80 %*                                                                      *
  81 %************************************************************************
  82
  83 Checks that a set of core bindings is well-formed.  The PprStyle and String
  84 just control what we print in the event of an error.  The Bool value
  85 indicates whether we have done any specialisation yet (in which case we do
  86 some extra checks).
  87
  88 We check for
  89         (a) type errors
  90         (b) Out-of-scope type variables
  91         (c) Out-of-scope local variables
  92         (d) Ill-kinded types
  93
  94 If we have done specialisation the we check that there are
  95         (a) No top-level bindings of primitive (unboxed type)
  96
  97 Outstanding issues:
  98
  99     --
 100     -- Things are *not* OK if:
 101     --
 102     --  * Unsaturated type app before specialisation has been done;
 103     --
 104     --  * Oversaturated type app after specialisation (eta reduction
 105     --   may well be happening...);
 106
 107
 108 Note [Type lets]
 109 ~~~~~~~~~~~~~~~~
 110 In the desugarer, it's very very convenient to be able to say (in effect)
 111         let a = Int in <body>
 112 That is, use a type let.  (See notes just below for why we want this.)
 113
 114 We don't have type lets in Core, so the desugarer uses type lambda
 115         (/\a. <body>) Int
 116 However, in the lambda form, we'd get lint errors from:
 117         (/\a. let x::a = 4 in <body>) Int
 118 because (x::a) doesn't look compatible with (4::Int).
 119
 120 So (HACK ALERT) the Lint phase does type-beta reduction "on the fly",
 121 as it were.  It carries a type substitution (in this example [a -> Int])
 122 and applies this substitution before comparing types.  The functin
 123         lintTy :: Type -> LintM Type
 124 returns a substituted type; that's the only reason it returns anything.
 125
 126 When we encounter a binder (like x::a) we must apply the substitution
 127 to the type of the binding variable.  lintBinders does this.
 128
 129 For Ids, the type-substituted Id is added to the in_scope set (which
 130 itself is part of the TvSubst we are carrying down), and when we
 131 find an occurence of an Id, we fetch it from the in-scope set.
 132
 133
 134 Why we need type let
 135 ~~~~~~~~~~~~~~~~~~~~
 136 It's needed when dealing with desugarer output for GADTs. Consider
 137   data T = forall a. T a (a->Int) Bool
 138    f :: T -> ... ->
 139    f (T x f True)  = <e1>
 140    f (T y g False) = <e2>
 141 After desugaring we get
 142         f t b = case t of
 143                   T a (x::a) (f::a->Int) (b:Bool) ->
 144                     case b of
 145                         True -> <e1>
 146                         False -> (/\b. let y=x; g=f in <e2>) a
 147 And for a reason I now forget, the ...<e2>... can mention a; so
 148 we want Lint to know that b=a.  Ugh.
 149
 150 I tried quite hard to make the necessity for this go away, by changing the
 151 desugarer, but the fundamental problem is this:
 152
 153         T a (x::a) (y::Int) -> let fail::a = ...
 154                                in (/\b. ...(case ... of
 155                                                 True  -> x::b
 156                                                 False -> fail)
 157                                   ) a
 158 Now the inner case look as though it has incompatible branches.
 159
 160
 161 \begin{code}
 162 lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
 163
 164 lintCoreBindings dflags whoDunnit binds
 165   | not (dopt Opt_DoCoreLinting dflags)
 166   = return ()
 167
 168 lintCoreBindings dflags whoDunnit binds
 169   = case (initL (lint_binds binds)) of
 170       Nothing       -> showPass dflags ("Core Linted result of " ++ whoDunnit)
 171       Just bad_news -> printDump (display bad_news)     >>
 172                        ghcExit dflags 1
 173   where
 174         -- Put all the top-level binders in scope at the start
 175         -- This is because transformation rules can bring something
 176         -- into use 'unexpectedly'
 177     lint_binds binds = addInScopeVars (bindersOfBinds binds) $
 178                        mapM lint_bind binds
 179
 180     lint_bind (Rec prs)         = mapM_ (lintSingleBinding TopLevel Recursive) prs
 181     lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
 182
 183     display bad_news
 184       = vcat [  text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
 185                 bad_news,
 186                 ptext SLIT("*** Offending Program ***"),
 187                 pprCoreBindings binds,
 188                 ptext SLIT("*** End of Offense ***")
 189         ]
 190 \end{code}
 191
 192 %************************************************************************
 193 %*                                                                      *
 194 \subsection[lintUnfolding]{lintUnfolding}
 195 %*                                                                      *
 196 %************************************************************************
 197
 198 We use this to check all unfoldings that come in from interfaces
 199 (it is very painful to catch errors otherwise):
 200
 201 \begin{code}
 202 lintUnfolding :: SrcLoc
 203               -> [Var]          -- Treat these as in scope
 204               -> CoreExpr
 205               -> Maybe Message  -- Nothing => OK
 206
 207 lintUnfolding locn vars expr
 208   = initL (addLoc (ImportedUnfolding locn) $
 209            addInScopeVars vars             $
 210            lintCoreExpr expr)
 211 \end{code}
 212
 213 %************************************************************************
 214 %*                                                                      *
 215 \subsection[lintCoreBinding]{lintCoreBinding}
 216 %*                                                                      *
 217 %************************************************************************
 218
 219 Check a core binding, returning the list of variables bound.
 220
 221 \begin{code}
 222 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
 223   = addLoc (RhsOf binder) $
 224          -- Check the rhs
 225     do { ty <- lintCoreExpr rhs
 226        ; lintBinder binder -- Check match to RHS type
 227        ; binder_ty <- applySubst binder_ty
 228        ; checkTys binder_ty ty (mkRhsMsg binder ty)
 229         -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
 230        ; checkL (not (isUnLiftedType binder_ty)
 231             || (isNonRec rec_flag && exprOkForSpeculation rhs))
 232            (mkRhsPrimMsg binder rhs)
 233         -- Check that if the binder is top-level or recursive, it's not demanded
 234        ; checkL (not (isStrictId binder)
 235             || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
 236            (mkStrictMsg binder)
 237         -- Check whether binder's specialisations contain any out-of-scope variables
 238        ; mapM_ (checkBndrIdInScope binder) bndr_vars
 239
 240       -- Check whether arity and demand type are consistent (only if demand analysis
 241       -- already happened)
 242        ; checkL (case maybeDmdTy of
 243                   Just (StrictSig dmd_ty) -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs
 244                   Nothing -> True)
 245            (mkArityMsg binder) }
 246
 247         -- We should check the unfolding, if any, but this is tricky because
 248         -- the unfolding is a SimplifiableCoreExpr. Give up for now.
 249    where
 250     binder_ty                  = idType binder
 251     maybeDmdTy                 = idNewStrictness_maybe binder
 252     bndr_vars                  = varSetElems (idFreeVars binder)
 253     lintBinder var | isId var  = lintIdBndr var $ \_ -> (return ())
 254                    | otherwise = return ()
 255 \end{code}
 256
 257 %************************************************************************
 258 %*                                                                      *
 259 \subsection[lintCoreExpr]{lintCoreExpr}
 260 %*                                                                      *
 261 %************************************************************************
 262
 263 \begin{code}
 264 type InType  = Type     -- Substitution not yet applied
 265 type OutType = Type     -- Substitution has been applied to this
 266
 267 lintCoreExpr :: CoreExpr -> LintM OutType
 268 -- The returned type has the substitution from the monad
 269 -- already applied to it:
 270 --      lintCoreExpr e subst = exprType (subst e)
 271
 272 lintCoreExpr (Var var)
 273   = do  { checkL (not (var == oneTupleDataConId))
 274                  (ptext SLIT("Illegal one-tuple"))
 275         ; var' <- lookupIdInScope var
 276         ; return (idType var')
 277         }
 278
 279 lintCoreExpr (Lit lit)
 280   = return (literalType lit)
 281
 282 --lintCoreExpr (Note (Coerce to_ty from_ty) expr)
 283 --  = do        { expr_ty <- lintCoreExpr expr
 284 --      ; to_ty <- lintTy to_ty
 285 --      ; from_ty <- lintTy from_ty
 286 --      ; checkTys from_ty expr_ty (mkCoerceErr from_ty expr_ty)
 287 --      ; return to_ty }
 288
 289 lintCoreExpr (Cast expr co)
 290   = do { expr_ty <- lintCoreExpr expr
 291        ; co' <- lintTy co
 292        ; let (from_ty, to_ty) = coercionKind co'
 293        ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
 294        ; return to_ty }
 295
 296 lintCoreExpr (Note other_note expr)
 297   = lintCoreExpr expr
 298
 299 lintCoreExpr (Let (NonRec bndr rhs) body)
 300   = do  { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
 301         ; addLoc (BodyOfLetRec [bndr])
 302                  (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
 303
 304 lintCoreExpr (Let (Rec pairs) body)
 305   = lintAndScopeIds bndrs       $ \_ ->
 306     do  { mapM (lintSingleBinding NotTopLevel Recursive) pairs
 307         ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
 308   where
 309     bndrs = map fst pairs
 310
 311 lintCoreExpr e@(App fun (Type ty))
 312 -- See Note [Type let] above
 313   = addLoc (AnExpr e) $
 314     go fun [ty]
 315   where
 316     go (App fun (Type ty)) tys
 317         = do { go fun (ty:tys) }
 318     go (Lam tv body) (ty:tys)
 319         = do  { checkL (isTyVar tv) (mkKindErrMsg tv ty)        -- Not quite accurate
 320               ; ty' <- lintTy ty
 321               ; let kind = tyVarKind tv
 322               ; kind' <- lintTy kind
 323               ; let tv' = setTyVarKind tv kind'
 324               ; checkKinds tv' ty'
 325                 -- Now extend the substitution so we
 326                 -- take advantage of it in the body
 327               ; addInScopeVars [tv'] $
 328                 extendSubstL tv' ty' $
 329                 go body tys }
 330     go fun tys
 331         = do  { fun_ty <- lintCoreExpr fun
 332               ; lintCoreArgs fun_ty (map Type tys) }
 333
 334 lintCoreExpr e@(App fun arg)
 335   = do  { fun_ty <- lintCoreExpr fun
 336         ; addLoc (AnExpr e) $
 337           lintCoreArg fun_ty arg }
 338
 339 lintCoreExpr (Lam var expr)
 340   = addLoc (LambdaBodyOf var) $
 341     lintBinders [var] $ \[var'] ->
 342     do { body_ty <- lintCoreExpr expr
 343        ; if isId var' then
 344              return (mkFunTy (idType var') body_ty)
 345          else
 346              return (mkForAllTy var' body_ty)
 347        }
 348         -- The applySubst is needed to apply the subst to var
 349
 350 lintCoreExpr e@(Case scrut var alt_ty alts) =
 351        -- Check the scrutinee
 352   do { scrut_ty <- lintCoreExpr scrut
 353      ; alt_ty   <- lintTy alt_ty
 354      ; var_ty   <- lintTy (idType var)
 355         -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
 356
 357      ; subst <- getTvSubst
 358      ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
 359
 360      -- If the binder is an unboxed tuple type, don't put it in scope
 361      ; let scope = if (isUnboxedTupleType (idType var)) then
 362                        pass_var
 363                    else lintAndScopeId var
 364      ; scope $ \_ ->
 365        do { -- Check the alternatives
 366             checkCaseAlts e scrut_ty alts
 367           ; mapM (lintCoreAlt scrut_ty alt_ty) alts
 368           ; return alt_ty } }
 369   where
 370     pass_var f = f var
 371
 372 lintCoreExpr e@(Type ty)
 373   = addErrL (mkStrangeTyMsg e)
 374 \end{code}
 375
 376 %************************************************************************
 377 %*                                                                      *
 378 \subsection[lintCoreArgs]{lintCoreArgs}
 379 %*                                                                      *
 380 %************************************************************************
 381
 382 The basic version of these functions checks that the argument is a
 383 subtype of the required type, as one would expect.
 384
 385 \begin{code}
 386 lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
 387 lintCoreArg  :: OutType -> CoreArg   -> LintM OutType
 388 -- First argument has already had substitution applied to it
 389 \end{code}
 390
 391 \begin{code}
 392 lintCoreArgs ty [] = return ty
 393 lintCoreArgs ty (a : args) =
 394   do { res <- lintCoreArg ty a
 395      ; lintCoreArgs res args }
 396
 397 lintCoreArg fun_ty a@(Type arg_ty) =
 398   do { arg_ty <- lintTy arg_ty
 399      ; lintTyApp fun_ty arg_ty }
 400
 401 lintCoreArg fun_ty arg =
 402        -- Make sure function type matches argument
 403   do { arg_ty <- lintCoreExpr arg
 404      ; let err1 =  mkAppMsg fun_ty arg_ty arg
 405            err2 = mkNonFunAppMsg fun_ty arg_ty arg
 406      ; case splitFunTy_maybe fun_ty of
 407         Just (arg,res) ->
 408           do { checkTys arg arg_ty err1
 409              ; return res }
 410         _ -> addErrL err2 }
 411 \end{code}
 412
 413 \begin{code}
 414 -- Both args have had substitution applied
 415 lintTyApp :: OutType -> OutType -> LintM OutType
 416 lintTyApp ty arg_ty
 417   = case splitForAllTy_maybe ty of
 418       Nothing -> addErrL (mkTyAppMsg ty arg_ty)
 419
 420       Just (tyvar,body)
 421         -> do   { checkL (isTyVar tyvar) (mkTyAppMsg ty arg_ty)
 422                 ; checkKinds tyvar arg_ty
 423                 ; return (substTyWith [tyvar] [arg_ty] body) }
 424
 425 checkKinds tyvar arg_ty
 426         -- Arg type might be boxed for a function with an uncommitted
 427         -- tyvar; notably this is used so that we can give
 428         --      error :: forall a:*. String -> a
 429         -- and then apply it to both boxed and unboxed types.
 430   = checkL (arg_kind `isSubKind` tyvar_kind)
 431            (mkKindErrMsg tyvar arg_ty)
 432   where
 433     tyvar_kind = tyVarKind tyvar
 434     arg_kind | isCoVar tyvar = coercionKindPredTy arg_ty
 435              | otherwise     = typeKind arg_ty
 436 \end{code}
 437
 438
 439 %************************************************************************
 440 %*                                                                      *
 441 \subsection[lintCoreAlts]{lintCoreAlts}
 442 %*                                                                      *
 443 %************************************************************************
 444
 445 \begin{code}
 446 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
 447 -- a) Check that the alts are non-empty
 448 -- b1) Check that the DEFAULT comes first, if it exists
 449 -- b2) Check that the others are in increasing order
 450 -- c) Check that there's a default for infinite types
 451 -- NB: Algebraic cases are not necessarily exhaustive, because
 452 --     the simplifer correctly eliminates case that can't
 453 --     possibly match.
 454
 455 checkCaseAlts e ty []
 456   = addErrL (mkNullAltsMsg e)
 457
 458 checkCaseAlts e ty alts =
 459   do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
 460      ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
 461      ; checkL (isJust maybe_deflt || not is_infinite_ty)
 462            (nonExhaustiveAltsMsg e) }
 463   where
 464     (con_alts, maybe_deflt) = findDefault alts
 465
 466         -- Check that successive alternatives have increasing tags
 467     increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
 468     increasing_tag other                     = True
 469
 470     non_deflt (DEFAULT, _, _) = False
 471     non_deflt alt             = True
 472
 473     is_infinite_ty = case splitTyConApp_maybe ty of
 474                         Nothing                     -> False
 475                         Just (tycon, tycon_arg_tys) -> isPrimTyCon tycon
 476 \end{code}
 477
 478 \begin{code}
 479 checkAltExpr :: CoreExpr -> OutType -> LintM ()
 480 checkAltExpr expr ann_ty
 481   = do { actual_ty <- lintCoreExpr expr
 482        ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
 483
 484 lintCoreAlt :: OutType          -- Type of scrutinee
 485             -> OutType          -- Type of the alternative
 486             -> CoreAlt
 487             -> LintM ()
 488
 489 lintCoreAlt scrut_ty alt_ty alt@(DEFAULT, args, rhs) =
 490   do { checkL (null args) (mkDefaultArgsMsg args)
 491      ; checkAltExpr rhs alt_ty }
 492
 493 lintCoreAlt scrut_ty alt_ty alt@(LitAlt lit, args, rhs) =
 494   do { checkL (null args) (mkDefaultArgsMsg args)
 495      ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
 496      ; checkAltExpr rhs alt_ty }
 497   where
 498     lit_ty = literalType lit
 499
 500 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
 501   | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
 502   | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
 503   = addLoc (CaseAlt alt) $  do
 504     {   -- First instantiate the universally quantified
 505         -- type variables of the data constructor
 506         -- We've already check
 507       checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
 508     ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
 509
 510         -- And now bring the new binders into scope
 511     ; lintBinders args $ \ args -> do
 512     { addLoc (CasePat alt) $ do
 513           {    -- Check the pattern
 514                  -- Scrutinee type must be a tycon applicn; checked by caller
 515                  -- This code is remarkably compact considering what it does!
 516                  -- NB: args must be in scope here so that the lintCoreArgs line works.
 517                  -- NB: relies on existential type args coming *after* ordinary type args
 518
 519           ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
 520           ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
 521           }
 522                -- Check the RHS
 523     ; checkAltExpr rhs alt_ty } }
 524
 525   | otherwise   -- Scrut-ty is wrong shape
 526   = addErrL (mkBadAltMsg scrut_ty alt)
 527 \end{code}
 528
 529 %************************************************************************
 530 %*                                                                      *
 531 \subsection[lint-types]{Types}
 532 %*                                                                      *
 533 %************************************************************************
 534
 535 \begin{code}
 536 -- When we lint binders, we (one at a time and in order):
 537 --  1. Lint var types or kinds (possibly substituting)
 538 --  2. Add the binder to the in scope set, and if its a coercion var,
 539 --     we may extend the substitution to reflect its (possibly) new kind
 540 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
 541 lintBinders [] linterF = linterF []
 542 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
 543                                  lintBinders vars $ \ vars' ->
 544                                  linterF (var':vars')
 545
 546 lintBinder :: Var -> (Var -> LintM a) -> LintM a
 547 lintBinder var linterF
 548   | isTyVar var = lint_ty_bndr
 549   | otherwise   = lintIdBndr var linterF
 550   where
 551     lint_ty_bndr = do { lintTy (tyVarKind var)
 552                       ; subst <- getTvSubst
 553                       ; let (subst', tv') = substTyVarBndr subst var
 554                       ; updateTvSubst subst' (linterF tv') }
 555
 556 lintIdBndr :: Var -> (Var -> LintM a) -> LintM a
 557 -- Do substitution on the type of a binder and add the var with this
 558 -- new type to the in-scope set of the second argument
 559 -- ToDo: lint its rules
 560 lintIdBndr id linterF
 561   = do  { checkL (not (isUnboxedTupleType (idType id)))
 562                  (mkUnboxedTupleMsg id)
 563                 -- No variable can be bound to an unboxed tuple.
 564         ; lintAndScopeId id $ \id' -> linterF id'
 565         }
 566
 567 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
 568 lintAndScopeIds ids linterF
 569   = go ids
 570   where
 571     go []       = linterF []
 572     go (id:ids) = do { lintAndScopeId id $ \id ->
 573                            lintAndScopeIds ids $ \ids ->
 574                            linterF (id:ids) }
 575
 576 lintAndScopeId :: Var -> (Var -> LintM a) -> LintM a
 577 lintAndScopeId id linterF
 578   = do { ty <- lintTy (idType id)
 579        ; let id' = Var.setIdType id ty
 580        ; addInScopeVars [id'] $ (linterF id')
 581        }
 582
 583 lintTy :: InType -> LintM OutType
 584 -- Check the type, and apply the substitution to it
 585 -- ToDo: check the kind structure of the type
 586 lintTy ty
 587   = do  { ty' <- applySubst ty
 588         ; mapM_ checkTyVarInScope (varSetElems (tyVarsOfType ty'))
 589         ; return ty' }
 590 \end{code}
 591
 592
 593 %************************************************************************
 594 %*                                                                      *
 595 \subsection[lint-monad]{The Lint monad}
 596 %*                                                                      *
 597 %************************************************************************
 598
 599 \begin{code}
 600 newtype LintM a =
 601    LintM { unLintM ::
 602             [LintLocInfo] ->         -- Locations
 603             TvSubst ->               -- Current type substitution; we also use this
 604                                      -- to keep track of all the variables in scope,
 605                                      -- both Ids and TyVars
 606             Bag Message ->           -- Error messages so far
 607             (Maybe a, Bag Message) } -- Result and error messages (if any)
 608
 609 {-      Note [Type substitution]
 610         ~~~~~~~~~~~~~~~~~~~~~~~~
 611 Why do we need a type substitution?  Consider
 612         /\(a:*). \(x:a). /\(a:*). id a x
 613 This is ill typed, because (renaming variables) it is really
 614         /\(a:*). \(x:a). /\(b:*). id b x
 615 Hence, when checking an application, we can't naively compare x's type
 616 (at its binding site) with its expected type (at a use site).  So we
 617 rename type binders as we go, maintaining a substitution.
 618
 619 The same substitution also supports let-type, current expressed as
 620         (/\(a:*). body) ty
 621 Here we substitute 'ty' for 'a' in 'body', on the fly.
 622 -}
 623
 624 instance Monad LintM where
 625   return x = LintM (\ loc subst errs -> (Just x, errs))
 626   fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
 627   m >>= k  = LintM (\ loc subst errs ->
 628                        let (res, errs') = unLintM m loc subst errs in
 629                          case res of
 630                            Just r -> unLintM (k r) loc subst errs'
 631                            Nothing -> (Nothing, errs'))
 632
 633 data LintLocInfo
 634   = RhsOf Id            -- The variable bound
 635   | LambdaBodyOf Id     -- The lambda-binder
 636   | BodyOfLetRec [Id]   -- One of the binders
 637   | CaseAlt CoreAlt     -- Case alternative
 638   | CasePat CoreAlt     -- *Pattern* of the case alternative
 639   | AnExpr CoreExpr     -- Some expression
 640   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
 641 \end{code}
 642
 643
 644 \begin{code}
 645 initL :: LintM a -> Maybe Message {- errors -}
 646 initL m
 647   = case unLintM m [] emptyTvSubst emptyBag of
 648       (_, errs) | isEmptyBag errs -> Nothing
 649                 | otherwise       -> Just (vcat (punctuate (text "") (bagToList errs)))
 650 \end{code}
 651
 652 \begin{code}
 653 checkL :: Bool -> Message -> LintM ()
 654 checkL True  msg = return ()
 655 checkL False msg = addErrL msg
 656
 657 addErrL :: Message -> LintM a
 658 addErrL msg = LintM (\ loc subst errs -> (Nothing, addErr subst errs msg loc))
 659
 660 addErr :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
 661 addErr subst errs_so_far msg locs
 662   = ASSERT( notNull locs )
 663     errs_so_far `snocBag` mk_msg msg
 664   where
 665    (loc, cxt1) = dumpLoc (head locs)
 666    cxts        = [snd (dumpLoc loc) | loc <- locs]
 667    context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
 668                                       ptext SLIT("Substitution:") <+> ppr subst
 669                | otherwise          = cxt1
 670
 671    mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
 672
 673 addLoc :: LintLocInfo -> LintM a -> LintM a
 674 addLoc extra_loc m =
 675   LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
 676
 677 addInScopeVars :: [Var] -> LintM a -> LintM a
 678 addInScopeVars vars m =
 679   LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst vars) errs)
 680
 681 updateTvSubst :: TvSubst -> LintM a -> LintM a
 682 updateTvSubst subst' m =
 683   LintM (\ loc subst errs -> unLintM m loc subst' errs)
 684
 685 getTvSubst :: LintM TvSubst
 686 getTvSubst = LintM (\ loc subst errs -> (Just subst, errs))
 687
 688 applySubst :: Type -> LintM Type
 689 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
 690
 691 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
 692 extendSubstL tv ty m
 693   = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
 694 \end{code}
 695
 696 \begin{code}
 697 lookupIdInScope :: Id -> LintM Id
 698 lookupIdInScope id
 699   | not (mustHaveLocalBinding id)
 700   = return id   -- An imported Id
 701   | otherwise
 702   = do  { subst <- getTvSubst
 703         ; case lookupInScope (getTvInScope subst) id of
 704                 Just v  -> return v
 705                 Nothing -> do { addErrL out_of_scope
 706                               ; return id } }
 707   where
 708     out_of_scope = ppr id <+> ptext SLIT("is out of scope")
 709
 710
 711 oneTupleDataConId :: Id -- Should not happen
 712 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
 713
 714 checkBndrIdInScope :: Var -> Var -> LintM ()
 715 checkBndrIdInScope binder id
 716   = checkInScope msg id
 717     where
 718      msg = ptext SLIT("is out of scope inside info for") <+>
 719            ppr binder
 720
 721 checkTyVarInScope :: TyVar -> LintM ()
 722 checkTyVarInScope tv = checkInScope (ptext SLIT("is out of scope")) tv
 723
 724 checkInScope :: SDoc -> Var -> LintM ()
 725 checkInScope loc_msg var =
 726  do { subst <- getTvSubst
 727     ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
 728              (hsep [ppr var, loc_msg]) }
 729
 730 checkTys :: Type -> Type -> Message -> LintM ()
 731 -- check ty2 is subtype of ty1 (ie, has same structure but usage
 732 -- annotations need only be consistent, not equal)
 733 -- Assumes ty1,ty2 are have alrady had the substitution applied
 734 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
 735 \end{code}
 736
 737 %************************************************************************
 738 %*                                                                      *
 739 \subsection{Error messages}
 740 %*                                                                      *
 741 %************************************************************************
 742
 743 \begin{code}
 744 dumpLoc (RhsOf v)
 745   = (getSrcLoc v, brackets (ptext SLIT("RHS of") <+> pp_binders [v]))
 746
 747 dumpLoc (LambdaBodyOf b)
 748   = (getSrcLoc b, brackets (ptext SLIT("in body of lambda with binder") <+> pp_binder b))
 749
 750 dumpLoc (BodyOfLetRec [])
 751   = (noSrcLoc, brackets (ptext SLIT("In body of a letrec with no binders")))
 752
 753 dumpLoc (BodyOfLetRec bs@(_:_))
 754   = ( getSrcLoc (head bs), brackets (ptext SLIT("in body of letrec with binders") <+> pp_binders bs))
 755
 756 dumpLoc (AnExpr e)
 757   = (noSrcLoc, text "In the expression:" <+> ppr e)
 758
 759 dumpLoc (CaseAlt (con, args, rhs))
 760   = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
 761
 762 dumpLoc (CasePat (con, args, rhs))
 763   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
 764
 765 dumpLoc (ImportedUnfolding locn)
 766   = (locn, brackets (ptext SLIT("in an imported unfolding")))
 767
 768 pp_binders :: [Var] -> SDoc
 769 pp_binders bs = sep (punctuate comma (map pp_binder bs))
 770
 771 pp_binder :: Var -> SDoc
 772 pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
 773             | isTyVar b = hsep [ppr b, dcolon, ppr (tyVarKind b)]
 774 \end{code}
 775
 776 \begin{code}
 777 ------------------------------------------------------
 778 --      Messages for case expressions
 779
 780 mkNullAltsMsg :: CoreExpr -> Message
 781 mkNullAltsMsg e
 782   = hang (text "Case expression with no alternatives:")
 783          4 (ppr e)
 784
 785 mkDefaultArgsMsg :: [Var] -> Message
 786 mkDefaultArgsMsg args
 787   = hang (text "DEFAULT case with binders")
 788          4 (ppr args)
 789
 790 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
 791 mkCaseAltMsg e ty1 ty2
 792   = hang (text "Type of case alternatives not the same as the annotation on case:")
 793          4 (vcat [ppr ty1, ppr ty2, ppr e])
 794
 795 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
 796 mkScrutMsg var var_ty scrut_ty subst
 797   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
 798           text "Result binder type:" <+> ppr var_ty,--(idType var),
 799           text "Scrutinee type:" <+> ppr scrut_ty,
 800      hsep [ptext SLIT("Current TV subst"), ppr subst]]
 801
 802 mkNonDefltMsg e
 803   = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
 804 mkNonIncreasingAltsMsg e
 805   = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
 806
 807 nonExhaustiveAltsMsg :: CoreExpr -> Message
 808 nonExhaustiveAltsMsg e
 809   = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
 810
 811 mkBadConMsg :: TyCon -> DataCon -> Message
 812 mkBadConMsg tycon datacon
 813   = vcat [
 814         text "In a case alternative, data constructor isn't in scrutinee type:",
 815         text "Scrutinee type constructor:" <+> ppr tycon,
 816         text "Data con:" <+> ppr datacon
 817     ]
 818
 819 mkBadPatMsg :: Type -> Type -> Message
 820 mkBadPatMsg con_result_ty scrut_ty
 821   = vcat [
 822         text "In a case alternative, pattern result type doesn't match scrutinee type:",
 823         text "Pattern result type:" <+> ppr con_result_ty,
 824         text "Scrutinee type:" <+> ppr scrut_ty
 825     ]
 826
 827 mkBadAltMsg :: Type -> CoreAlt -> Message
 828 mkBadAltMsg scrut_ty alt
 829   = vcat [ text "Data alternative when scrutinee is not a tycon application",
 830            text "Scrutinee type:" <+> ppr scrut_ty,
 831            text "Alternative:" <+> pprCoreAlt alt ]
 832
 833 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
 834 mkNewTyDataConAltMsg scrut_ty alt
 835   = vcat [ text "Data alternative for newtype datacon",
 836            text "Scrutinee type:" <+> ppr scrut_ty,
 837            text "Alternative:" <+> pprCoreAlt alt ]
 838
 839
 840 ------------------------------------------------------
 841 --      Other error messages
 842
 843 mkAppMsg :: Type -> Type -> CoreExpr -> Message
 844 mkAppMsg fun_ty arg_ty arg
 845   = vcat [ptext SLIT("Argument value doesn't match argument type:"),
 846               hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
 847               hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
 848               hang (ptext SLIT("Arg:")) 4 (ppr arg)]
 849
 850 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
 851 mkNonFunAppMsg fun_ty arg_ty arg
 852   = vcat [ptext SLIT("Non-function type in function position"),
 853               hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
 854               hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
 855               hang (ptext SLIT("Arg:")) 4 (ppr arg)]
 856
 857 mkKindErrMsg :: TyVar -> Type -> Message
 858 mkKindErrMsg tyvar arg_ty
 859   = vcat [ptext SLIT("Kinds don't match in type application:"),
 860           hang (ptext SLIT("Type variable:"))
 861                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
 862           hang (ptext SLIT("Arg type:"))
 863                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 864
 865 mkTyAppMsg :: Type -> Type -> Message
 866 mkTyAppMsg ty arg_ty
 867   = vcat [text "Illegal type application:",
 868               hang (ptext SLIT("Exp type:"))
 869                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
 870               hang (ptext SLIT("Arg type:"))
 871                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 872
 873 mkRhsMsg :: Id -> Type -> Message
 874 mkRhsMsg binder ty
 875   = vcat
 876     [hsep [ptext SLIT("The type of this binder doesn't match the type of its RHS:"),
 877             ppr binder],
 878      hsep [ptext SLIT("Binder's type:"), ppr (idType binder)],
 879      hsep [ptext SLIT("Rhs type:"), ppr ty]]
 880
 881 mkRhsPrimMsg :: Id -> CoreExpr -> Message
 882 mkRhsPrimMsg binder rhs
 883   = vcat [hsep [ptext SLIT("The type of this binder is primitive:"),
 884                      ppr binder],
 885               hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]
 886              ]
 887
 888 mkStrictMsg :: Id -> Message
 889 mkStrictMsg binder
 890   = vcat [hsep [ptext SLIT("Recursive or top-level binder has strict demand info:"),
 891                      ppr binder],
 892               hsep [ptext SLIT("Binder's demand info:"), ppr (idNewDemandInfo binder)]
 893              ]
 894
 895 mkArityMsg :: Id -> Message
 896 mkArityMsg binder
 897   = vcat [hsep [ptext SLIT("Demand type has "),
 898                      ppr (dmdTypeDepth dmd_ty),
 899                      ptext SLIT(" arguments, rhs has "),
 900                      ppr (idArity binder),
 901                      ptext SLIT("arguments, "),
 902                      ppr binder],
 903               hsep [ptext SLIT("Binder's strictness signature:"), ppr dmd_ty]
 904
 905          ]
 906            where (StrictSig dmd_ty) = idNewStrictness binder
 907
 908 mkUnboxedTupleMsg :: Id -> Message
 909 mkUnboxedTupleMsg binder
 910   = vcat [hsep [ptext SLIT("A variable has unboxed tuple type:"), ppr binder],
 911           hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]]
 912
 913 mkCastErr from_ty expr_ty
 914   = vcat [ptext SLIT("From-type of Cast differs from type of enclosed expression"),
 915           ptext SLIT("From-type:") <+> ppr from_ty,
 916           ptext SLIT("Type of enclosed expr:") <+> ppr expr_ty
 917     ]
 918
 919 mkStrangeTyMsg e
 920   = ptext SLIT("Type where expression expected:") <+> ppr e
 921 \end{code}