compiler/coreSyn/CoreLint.lhs

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