compiler/coreSyn/CoreLint.lhs

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