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
 256         ; checkDeadIdOcc var
 257         ; var' <- lookupIdInScope var
 258         ; return (idType var')
 259         }
 260
 261 lintCoreExpr (Lit lit)
 262   = return (literalType lit)
 263
 264 --lintCoreExpr (Note (Coerce to_ty from_ty) expr)
 265 --  = do        { expr_ty <- lintCoreExpr expr
 266 --      ; to_ty <- lintTy to_ty
 267 --      ; from_ty <- lintTy from_ty
 268 --      ; checkTys from_ty expr_ty (mkCoerceErr from_ty expr_ty)
 269 --      ; return to_ty }
 270
 271 lintCoreExpr (Cast expr co)
 272   = do { expr_ty <- lintCoreExpr expr
 273        ; co' <- lintTy co
 274        ; let (from_ty, to_ty) = coercionKind co'
 275        ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
 276        ; return to_ty }
 277
 278 lintCoreExpr (Note _ expr)
 279   = lintCoreExpr expr
 280
 281 lintCoreExpr (Let (NonRec tv (Type ty)) body)
 282   =     -- See Note [Type let] in CoreSyn
 283     do  { checkL (isTyVar tv) (mkKindErrMsg tv ty)      -- Not quite accurate
 284         ; ty' <- lintTy ty
 285         ; kind' <- lintTy (tyVarKind tv)
 286         ; let tv' = setTyVarKind tv kind'
 287         ; checkKinds tv' ty'
 288                 -- Now extend the substitution so we
 289                 -- take advantage of it in the body
 290         ; addLoc (BodyOfLetRec [tv]) $
 291           addInScopeVars [tv'] $
 292           extendSubstL tv' ty' $
 293           lintCoreExpr body }
 294
 295 lintCoreExpr (Let (NonRec bndr rhs) body)
 296   = do  { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
 297         ; addLoc (BodyOfLetRec [bndr])
 298                  (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
 299
 300 lintCoreExpr (Let (Rec pairs) body)
 301   = lintAndScopeIds bndrs       $ \_ ->
 302     do  { mapM (lintSingleBinding NotTopLevel Recursive) pairs
 303         ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
 304   where
 305     bndrs = map fst pairs
 306
 307 lintCoreExpr e@(App fun arg)
 308   = do  { fun_ty <- lintCoreExpr fun
 309         ; addLoc (AnExpr e) $
 310           lintCoreArg fun_ty arg }
 311
 312 lintCoreExpr (Lam var expr)
 313   = addLoc (LambdaBodyOf var) $
 314     lintBinders [var] $ \[var'] ->
 315     do { body_ty <- lintCoreExpr expr
 316        ; if isId var' then
 317              return (mkFunTy (idType var') body_ty)
 318          else
 319              return (mkForAllTy var' body_ty)
 320        }
 321         -- The applySubst is needed to apply the subst to var
 322
 323 lintCoreExpr e@(Case scrut var alt_ty alts) =
 324        -- Check the scrutinee
 325   do { scrut_ty <- lintCoreExpr scrut
 326      ; alt_ty   <- lintTy alt_ty
 327      ; var_ty   <- lintTy (idType var)
 328
 329      ; let mb_tc_app = splitTyConApp_maybe (idType var)
 330      ; case mb_tc_app of
 331          Just (tycon, _)
 332               | debugIsOn &&
 333                 isAlgTyCon tycon &&
 334                 not (isOpenTyCon tycon) &&
 335                 null (tyConDataCons tycon) ->
 336                   pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
 337                         -- This can legitimately happen for type families
 338                       $ return ()
 339          _otherwise -> return ()
 340
 341         -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
 342
 343      ; subst <- getTvSubst
 344      ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
 345
 346      -- If the binder is an unboxed tuple type, don't put it in scope
 347      ; let scope = if (isUnboxedTupleType (idType var)) then
 348                        pass_var
 349                    else lintAndScopeId var
 350      ; scope $ \_ ->
 351        do { -- Check the alternatives
 352             mapM (lintCoreAlt scrut_ty alt_ty) alts
 353           ; checkCaseAlts e scrut_ty alts
 354           ; return alt_ty } }
 355   where
 356     pass_var f = f var
 357
 358 lintCoreExpr (Type ty)
 359   = do { ty' <- lintTy ty
 360        ; return (typeKind ty') }
 361 \end{code}
 362
 363 %************************************************************************
 364 %*                                                                      *
 365 \subsection[lintCoreArgs]{lintCoreArgs}
 366 %*                                                                      *
 367 %************************************************************************
 368
 369 The basic version of these functions checks that the argument is a
 370 subtype of the required type, as one would expect.
 371
 372 \begin{code}
 373 lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
 374 lintCoreArg  :: OutType -> CoreArg   -> LintM OutType
 375 -- First argument has already had substitution applied to it
 376 \end{code}
 377
 378 \begin{code}
 379 lintCoreArgs ty [] = return ty
 380 lintCoreArgs ty (a : args) =
 381   do { res <- lintCoreArg ty a
 382      ; lintCoreArgs res args }
 383
 384 lintCoreArg fun_ty (Type arg_ty) =
 385   do { arg_ty <- lintTy arg_ty
 386      ; lintTyApp fun_ty arg_ty }
 387
 388 lintCoreArg fun_ty arg =
 389        -- Make sure function type matches argument
 390   do { arg_ty <- lintCoreExpr arg
 391      ; let err1 =  mkAppMsg fun_ty arg_ty arg
 392            err2 = mkNonFunAppMsg fun_ty arg_ty arg
 393      ; case splitFunTy_maybe fun_ty of
 394         Just (arg,res) ->
 395           do { checkTys arg arg_ty err1
 396              ; return res }
 397         _ -> addErrL err2 }
 398 \end{code}
 399
 400 \begin{code}
 401 -- Both args have had substitution applied
 402 lintTyApp :: OutType -> OutType -> LintM OutType
 403 lintTyApp ty arg_ty
 404   = case splitForAllTy_maybe ty of
 405       Nothing -> addErrL (mkTyAppMsg ty arg_ty)
 406
 407       Just (tyvar,body)
 408         -> do   { checkL (isTyVar tyvar) (mkTyAppMsg ty arg_ty)
 409                 ; checkKinds tyvar arg_ty
 410                 ; return (substTyWith [tyvar] [arg_ty] body) }
 411
 412 checkKinds :: Var -> Type -> LintM ()
 413 checkKinds tyvar arg_ty
 414         -- Arg type might be boxed for a function with an uncommitted
 415         -- tyvar; notably this is used so that we can give
 416         --      error :: forall a:*. String -> a
 417         -- and then apply it to both boxed and unboxed types.
 418   = checkL (arg_kind `isSubKind` tyvar_kind)
 419            (mkKindErrMsg tyvar arg_ty)
 420   where
 421     tyvar_kind = tyVarKind tyvar
 422     arg_kind | isCoVar tyvar = coercionKindPredTy arg_ty
 423              | otherwise     = typeKind arg_ty
 424
 425 checkDeadIdOcc :: Id -> LintM ()
 426 -- Occurrences of an Id should never be dead....
 427 -- except when we are checking a case pattern
 428 checkDeadIdOcc id
 429   | isDeadOcc (idOccInfo id)
 430   = do { in_case <- inCasePat
 431        ; checkL in_case
 432                 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
 433   | otherwise
 434   = return ()
 435 \end{code}
 436
 437
 438 %************************************************************************
 439 %*                                                                      *
 440 \subsection[lintCoreAlts]{lintCoreAlts}
 441 %*                                                                      *
 442 %************************************************************************
 443
 444 \begin{code}
 445 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
 446 -- a) Check that the alts are non-empty
 447 -- b1) Check that the DEFAULT comes first, if it exists
 448 -- b2) Check that the others are in increasing order
 449 -- c) Check that there's a default for infinite types
 450 -- NB: Algebraic cases are not necessarily exhaustive, because
 451 --     the simplifer correctly eliminates case that can't
 452 --     possibly match.
 453
 454 checkCaseAlts e _ []
 455   = addErrL (mkNullAltsMsg e)
 456
 457 checkCaseAlts e ty alts =
 458   do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
 459      ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
 460      ; checkL (isJust maybe_deflt || not is_infinite_ty)
 461            (nonExhaustiveAltsMsg e) }
 462   where
 463     (con_alts, maybe_deflt) = findDefault alts
 464
 465         -- Check that successive alternatives have increasing tags
 466     increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
 467     increasing_tag _                         = True
 468
 469     non_deflt (DEFAULT, _, _) = False
 470     non_deflt _               = True
 471
 472     is_infinite_ty = case splitTyConApp_maybe ty of
 473                         Nothing         -> False
 474                         Just (tycon, _) -> isPrimTyCon tycon
 475 \end{code}
 476
 477 \begin{code}
 478 checkAltExpr :: CoreExpr -> OutType -> LintM ()
 479 checkAltExpr expr ann_ty
 480   = do { actual_ty <- lintCoreExpr expr
 481        ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
 482
 483 lintCoreAlt :: OutType          -- Type of scrutinee
 484             -> OutType          -- Type of the alternative
 485             -> CoreAlt
 486             -> LintM ()
 487
 488 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
 489   do { checkL (null args) (mkDefaultArgsMsg args)
 490      ; checkAltExpr rhs alt_ty }
 491
 492 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) =
 493   do { checkL (null args) (mkDefaultArgsMsg args)
 494      ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
 495      ; checkAltExpr rhs alt_ty }
 496   where
 497     lit_ty = literalType lit
 498
 499 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
 500   | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
 501   | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
 502   = addLoc (CaseAlt alt) $  do
 503     {   -- First instantiate the universally quantified
 504         -- type variables of the data constructor
 505         -- We've already check
 506       checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
 507     ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
 508
 509         -- And now bring the new binders into scope
 510     ; lintBinders args $ \ args -> do
 511     { addLoc (CasePat alt) $ do
 512           {    -- Check the pattern
 513                  -- Scrutinee type must be a tycon applicn; checked by caller
 514                  -- This code is remarkably compact considering what it does!
 515                  -- NB: args must be in scope here so that the lintCoreArgs
 516                  --     line works.
 517                  -- NB: relies on existential type args coming *after*
 518                  --     ordinary type args
 519           ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
 520           ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
 521           }
 522                -- Check the RHS
 523     ; checkAltExpr rhs alt_ty } }
 524
 525   | otherwise   -- Scrut-ty is wrong shape
 526   = addErrL (mkBadAltMsg scrut_ty alt)
 527 \end{code}
 528
 529 %************************************************************************
 530 %*                                                                      *
 531 \subsection[lint-types]{Types}
 532 %*                                                                      *
 533 %************************************************************************
 534
 535 \begin{code}
 536 -- When we lint binders, we (one at a time and in order):
 537 --  1. Lint var types or kinds (possibly substituting)
 538 --  2. Add the binder to the in scope set, and if its a coercion var,
 539 --     we may extend the substitution to reflect its (possibly) new kind
 540 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
 541 lintBinders [] linterF = linterF []
 542 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
 543                                  lintBinders vars $ \ vars' ->
 544                                  linterF (var':vars')
 545
 546 lintBinder :: Var -> (Var -> LintM a) -> LintM a
 547 lintBinder var linterF
 548   | isTyVar var = lint_ty_bndr
 549   | otherwise   = lintIdBndr var linterF
 550   where
 551     lint_ty_bndr = do { lintTy (tyVarKind var)
 552                       ; subst <- getTvSubst
 553                       ; let (subst', tv') = substTyVarBndr subst var
 554                       ; updateTvSubst subst' (linterF tv') }
 555
 556 lintIdBndr :: Var -> (Var -> LintM a) -> LintM a
 557 -- Do substitution on the type of a binder and add the var with this
 558 -- new type to the in-scope set of the second argument
 559 -- ToDo: lint its rules
 560 lintIdBndr id linterF
 561   = do  { checkL (not (isUnboxedTupleType (idType id)))
 562                  (mkUnboxedTupleMsg id)
 563                 -- No variable can be bound to an unboxed tuple.
 564         ; lintAndScopeId id $ \id' -> linterF id'
 565         }
 566
 567 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
 568 lintAndScopeIds ids linterF
 569   = go ids
 570   where
 571     go []       = linterF []
 572     go (id:ids) = do { lintAndScopeId id $ \id ->
 573                            lintAndScopeIds ids $ \ids ->
 574                            linterF (id:ids) }
 575
 576 lintAndScopeId :: Var -> (Var -> LintM a) -> LintM a
 577 lintAndScopeId id linterF
 578   = do { ty <- lintTy (idType id)
 579        ; let id' = setIdType id ty
 580        ; addInScopeVars [id'] $ (linterF id')
 581        }
 582
 583 lintTy :: InType -> LintM OutType
 584 -- Check the type, and apply the substitution to it
 585 -- See Note [Linting type lets]
 586 -- ToDo: check the kind structure of the type
 587 lintTy ty
 588   = do  { ty' <- applySubst ty
 589         ; mapM_ checkTyVarInScope (varSetElems (tyVarsOfType ty'))
 590         ; return ty' }
 591 \end{code}
 592
 593
 594 %************************************************************************
 595 %*                                                                      *
 596 \subsection[lint-monad]{The Lint monad}
 597 %*                                                                      *
 598 %************************************************************************
 599
 600 \begin{code}
 601 newtype LintM a =
 602    LintM { unLintM ::
 603             [LintLocInfo] ->         -- Locations
 604             TvSubst ->               -- Current type substitution; we also use this
 605                                      -- to keep track of all the variables in scope,
 606                                      -- both Ids and TyVars
 607             Bag Message ->           -- Error messages so far
 608             (Maybe a, Bag Message) } -- Result and error messages (if any)
 609
 610 {-      Note [Type substitution]
 611         ~~~~~~~~~~~~~~~~~~~~~~~~
 612 Why do we need a type substitution?  Consider
 613         /\(a:*). \(x:a). /\(a:*). id a x
 614 This is ill typed, because (renaming variables) it is really
 615         /\(a:*). \(x:a). /\(b:*). id b x
 616 Hence, when checking an application, we can't naively compare x's type
 617 (at its binding site) with its expected type (at a use site).  So we
 618 rename type binders as we go, maintaining a substitution.
 619
 620 The same substitution also supports let-type, current expressed as
 621         (/\(a:*). body) ty
 622 Here we substitute 'ty' for 'a' in 'body', on the fly.
 623 -}
 624
 625 instance Monad LintM where
 626   return x = LintM (\ _   _     errs -> (Just x, errs))
 627   fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
 628   m >>= k  = LintM (\ loc subst errs ->
 629                        let (res, errs') = unLintM m loc subst errs in
 630                          case res of
 631                            Just r -> unLintM (k r) loc subst errs'
 632                            Nothing -> (Nothing, errs'))
 633
 634 data LintLocInfo
 635   = RhsOf Id            -- The variable bound
 636   | LambdaBodyOf Id     -- The lambda-binder
 637   | BodyOfLetRec [Id]   -- One of the binders
 638   | CaseAlt CoreAlt     -- Case alternative
 639   | CasePat CoreAlt     -- The *pattern* of the case alternative
 640   | AnExpr CoreExpr     -- Some expression
 641   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
 642   | TopLevelBindings
 643 \end{code}
 644
 645
 646 \begin{code}
 647 initL :: LintM a -> Maybe Message {- errors -}
 648 initL m
 649   = case unLintM m [] emptyTvSubst emptyBag of
 650       (_, errs) | isEmptyBag errs -> Nothing
 651                 | otherwise       -> Just (vcat (punctuate (text "") (bagToList errs)))
 652 \end{code}
 653
 654 \begin{code}
 655 checkL :: Bool -> Message -> LintM ()
 656 checkL True  _   = return ()
 657 checkL False msg = addErrL msg
 658
 659 addErrL :: Message -> LintM a
 660 addErrL msg = LintM (\ loc subst errs -> (Nothing, addErr subst errs msg loc))
 661
 662 addErr :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
 663 addErr subst errs_so_far msg locs
 664   = ASSERT( notNull locs )
 665     errs_so_far `snocBag` mk_msg msg
 666   where
 667    (loc, cxt1) = dumpLoc (head locs)
 668    cxts        = [snd (dumpLoc loc) | loc <- locs]
 669    context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
 670                                       ptext (sLit "Substitution:") <+> ppr subst
 671                | otherwise          = cxt1
 672
 673    mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
 674
 675 addLoc :: LintLocInfo -> LintM a -> LintM a
 676 addLoc extra_loc m =
 677   LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
 678
 679 inCasePat :: LintM Bool         -- A slight hack; see the unique call site
 680 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
 681   where
 682     is_case_pat (CasePat {} : _) = True
 683     is_case_pat _other           = False
 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 _ errs -> unLintM m loc subst' errs)
 697
 698 getTvSubst :: LintM TvSubst
 699 getTvSubst = LintM (\ _ 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 :: LintLocInfo -> (SrcLoc, SDoc)
 758
 759 dumpLoc (RhsOf v)
 760   = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
 761
 762 dumpLoc (LambdaBodyOf b)
 763   = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
 764
 765 dumpLoc (BodyOfLetRec [])
 766   = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
 767
 768 dumpLoc (BodyOfLetRec bs@(_:_))
 769   = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
 770
 771 dumpLoc (AnExpr e)
 772   = (noSrcLoc, text "In the expression:" <+> ppr e)
 773
 774 dumpLoc (CaseAlt (con, args, _))
 775   = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
 776
 777 dumpLoc (CasePat (con, args, _))
 778   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
 779
 780 dumpLoc (ImportedUnfolding locn)
 781   = (locn, brackets (ptext (sLit "in an imported unfolding")))
 782 dumpLoc TopLevelBindings
 783   = (noSrcLoc, empty)
 784
 785 pp_binders :: [Var] -> SDoc
 786 pp_binders bs = sep (punctuate comma (map pp_binder bs))
 787
 788 pp_binder :: Var -> SDoc
 789 pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
 790             | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
 791 \end{code}
 792
 793 \begin{code}
 794 ------------------------------------------------------
 795 --      Messages for case expressions
 796
 797 mkNullAltsMsg :: CoreExpr -> Message
 798 mkNullAltsMsg e
 799   = hang (text "Case expression with no alternatives:")
 800          4 (ppr e)
 801
 802 mkDefaultArgsMsg :: [Var] -> Message
 803 mkDefaultArgsMsg args
 804   = hang (text "DEFAULT case with binders")
 805          4 (ppr args)
 806
 807 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
 808 mkCaseAltMsg e ty1 ty2
 809   = hang (text "Type of case alternatives not the same as the annotation on case:")
 810          4 (vcat [ppr ty1, ppr ty2, ppr e])
 811
 812 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
 813 mkScrutMsg var var_ty scrut_ty subst
 814   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
 815           text "Result binder type:" <+> ppr var_ty,--(idType var),
 816           text "Scrutinee type:" <+> ppr scrut_ty,
 817      hsep [ptext (sLit "Current TV subst"), ppr subst]]
 818
 819 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
 820 mkNonDefltMsg e
 821   = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
 822 mkNonIncreasingAltsMsg e
 823   = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
 824
 825 nonExhaustiveAltsMsg :: CoreExpr -> Message
 826 nonExhaustiveAltsMsg e
 827   = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
 828
 829 mkBadConMsg :: TyCon -> DataCon -> Message
 830 mkBadConMsg tycon datacon
 831   = vcat [
 832         text "In a case alternative, data constructor isn't in scrutinee type:",
 833         text "Scrutinee type constructor:" <+> ppr tycon,
 834         text "Data con:" <+> ppr datacon
 835     ]
 836
 837 mkBadPatMsg :: Type -> Type -> Message
 838 mkBadPatMsg con_result_ty scrut_ty
 839   = vcat [
 840         text "In a case alternative, pattern result type doesn't match scrutinee type:",
 841         text "Pattern result type:" <+> ppr con_result_ty,
 842         text "Scrutinee type:" <+> ppr scrut_ty
 843     ]
 844
 845 mkBadAltMsg :: Type -> CoreAlt -> Message
 846 mkBadAltMsg scrut_ty alt
 847   = vcat [ text "Data alternative when scrutinee is not a tycon application",
 848            text "Scrutinee type:" <+> ppr scrut_ty,
 849            text "Alternative:" <+> pprCoreAlt alt ]
 850
 851 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
 852 mkNewTyDataConAltMsg scrut_ty alt
 853   = vcat [ text "Data alternative for newtype datacon",
 854            text "Scrutinee type:" <+> ppr scrut_ty,
 855            text "Alternative:" <+> pprCoreAlt alt ]
 856
 857
 858 ------------------------------------------------------
 859 --      Other error messages
 860
 861 mkAppMsg :: Type -> Type -> CoreExpr -> Message
 862 mkAppMsg fun_ty arg_ty arg
 863   = vcat [ptext (sLit "Argument value doesn't match argument type:"),
 864               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
 865               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
 866               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
 867
 868 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
 869 mkNonFunAppMsg fun_ty arg_ty arg
 870   = vcat [ptext (sLit "Non-function type in function position"),
 871               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
 872               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
 873               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
 874
 875 mkKindErrMsg :: TyVar -> Type -> Message
 876 mkKindErrMsg tyvar arg_ty
 877   = vcat [ptext (sLit "Kinds don't match in type application:"),
 878           hang (ptext (sLit "Type variable:"))
 879                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
 880           hang (ptext (sLit "Arg type:"))
 881                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 882
 883 mkTyAppMsg :: Type -> Type -> Message
 884 mkTyAppMsg ty arg_ty
 885   = vcat [text "Illegal type application:",
 886               hang (ptext (sLit "Exp type:"))
 887                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
 888               hang (ptext (sLit "Arg type:"))
 889                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 890
 891 mkRhsMsg :: Id -> Type -> Message
 892 mkRhsMsg binder ty
 893   = vcat
 894     [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
 895             ppr binder],
 896      hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
 897      hsep [ptext (sLit "Rhs type:"), ppr ty]]
 898
 899 mkRhsPrimMsg :: Id -> CoreExpr -> Message
 900 mkRhsPrimMsg binder _rhs
 901   = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
 902                      ppr binder],
 903               hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
 904              ]
 905
 906 mkStrictMsg :: Id -> Message
 907 mkStrictMsg binder
 908   = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
 909                      ppr binder],
 910               hsep [ptext (sLit "Binder's demand info:"), ppr (idNewDemandInfo binder)]
 911              ]
 912
 913 mkArityMsg :: Id -> Message
 914 mkArityMsg binder
 915   = vcat [hsep [ptext (sLit "Demand type has "),
 916                      ppr (dmdTypeDepth dmd_ty),
 917                      ptext (sLit " arguments, rhs has "),
 918                      ppr (idArity binder),
 919                      ptext (sLit "arguments, "),
 920                      ppr binder],
 921               hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
 922
 923          ]
 924            where (StrictSig dmd_ty) = idNewStrictness binder
 925
 926 mkUnboxedTupleMsg :: Id -> Message
 927 mkUnboxedTupleMsg binder
 928   = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
 929           hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
 930
 931 mkCastErr :: Type -> Type -> Message
 932 mkCastErr from_ty expr_ty
 933   = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
 934           ptext (sLit "From-type:") <+> ppr from_ty,
 935           ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
 936     ]
 937
 938 dupVars :: [[Var]] -> Message
 939 dupVars vars
 940   = hang (ptext (sLit "Duplicate variables brought into scope"))
 941        2 (ppr vars)
 942 \end{code}