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