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