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