compiler/coreSyn/CoreLint.lhs

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