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