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