compiler/coreSyn/CoreLint.lhs

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