compiler/coreSyn/CoreLint.lhs

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