coreSyn/CoreLint.lhs

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