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