compiler/coreSyn/CoreLint.lhs

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