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 Demand
  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 TypeRep
  32 import Coercion
  33 import TyCon
  34 import Class
  35 import BasicTypes
  36 import StaticFlags
  37 import ListSetOps
  38 import PrelNames
  39 import Outputable
  40 import FastString
  41 import Util
  42 import Control.Monad
  43 import Data.Maybe
  44 \end{code}
  45
  46 %************************************************************************
  47 %*                                                                      *
  48 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
  49 %*                                                                      *
  50 %************************************************************************
  51
  52 Checks that a set of core bindings is well-formed.  The PprStyle and String
  53 just control what we print in the event of an error.  The Bool value
  54 indicates whether we have done any specialisation yet (in which case we do
  55 some extra checks).
  56
  57 We check for
  58         (a) type errors
  59         (b) Out-of-scope type variables
  60         (c) Out-of-scope local variables
  61         (d) Ill-kinded types
  62
  63 If we have done specialisation the we check that there are
  64         (a) No top-level bindings of primitive (unboxed type)
  65
  66 Outstanding issues:
  67
  68     --
  69     -- Things are *not* OK if:
  70     --
  71     --  * Unsaturated type app before specialisation has been done;
  72     --
  73     --  * Oversaturated type app after specialisation (eta reduction
  74     --   may well be happening...);
  75
  76
  77 Note [Linting type lets]
  78 ~~~~~~~~~~~~~~~~~~~~~~~~
  79 In the desugarer, it's very very convenient to be able to say (in effect)
  80         let a = Type Int in <body>
  81 That is, use a type let.   See Note [Type let] in CoreSyn.
  82
  83 However, when linting <body> we need to remember that a=Int, else we might
  84 reject a correct program.  So we carry a type substitution (in this example
  85 [a -> Int]) and apply this substitution before comparing types.  The functin
  86         lintInTy :: Type -> LintM Type
  87 returns a substituted type; that's the only reason it returns anything.
  88
  89 When we encounter a binder (like x::a) we must apply the substitution
  90 to the type of the binding variable.  lintBinders does this.
  91
  92 For Ids, the type-substituted Id is added to the in_scope set (which
  93 itself is part of the TvSubst we are carrying down), and when we
  94 find an occurence of an Id, we fetch it from the in-scope set.
  95
  96
  97 \begin{code}
  98 lintCoreBindings :: [CoreBind] -> (Bag Message, Bag Message)
  99 --   Returns (warnings, errors)
 100 lintCoreBindings binds
 101   = initL (lint_binds binds)
 102   where
 103         -- Put all the top-level binders in scope at the start
 104         -- This is because transformation rules can bring something
 105         -- into use 'unexpectedly'
 106     lint_binds binds = addLoc TopLevelBindings $
 107                        addInScopeVars (bindersOfBinds binds) $
 108                        mapM lint_bind binds
 109
 110     lint_bind (Rec prs)         = mapM_ (lintSingleBinding TopLevel Recursive) prs
 111     lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
 112 \end{code}
 113
 114 %************************************************************************
 115 %*                                                                      *
 116 \subsection[lintUnfolding]{lintUnfolding}
 117 %*                                                                      *
 118 %************************************************************************
 119
 120 We use this to check all unfoldings that come in from interfaces
 121 (it is very painful to catch errors otherwise):
 122
 123 \begin{code}
 124 lintUnfolding :: SrcLoc
 125               -> [Var]          -- Treat these as in scope
 126               -> CoreExpr
 127               -> Maybe Message  -- Nothing => OK
 128
 129 lintUnfolding locn vars expr
 130   | isEmptyBag errs = Nothing
 131   | otherwise       = Just (pprMessageBag errs)
 132   where
 133     (_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
 134                             addInScopeVars vars            $
 135                             lintCoreExpr expr)
 136 \end{code}
 137
 138 %************************************************************************
 139 %*                                                                      *
 140 \subsection[lintCoreBinding]{lintCoreBinding}
 141 %*                                                                      *
 142 %************************************************************************
 143
 144 Check a core binding, returning the list of variables bound.
 145
 146 \begin{code}
 147 lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
 148 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
 149   = addLoc (RhsOf binder) $
 150          -- Check the rhs
 151     do { ty <- lintCoreExpr rhs
 152        ; lintBinder binder -- Check match to RHS type
 153        ; binder_ty <- applySubst binder_ty
 154        ; checkTys binder_ty ty (mkRhsMsg binder ty)
 155         -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
 156        ; checkL (not (isUnLiftedType binder_ty)
 157             || (isNonRec rec_flag && exprOkForSpeculation rhs))
 158            (mkRhsPrimMsg binder rhs)
 159         -- Check that if the binder is top-level or recursive, it's not demanded
 160        ; checkL (not (isStrictId binder)
 161             || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
 162            (mkStrictMsg binder)
 163         -- Check whether binder's specialisations contain any out-of-scope variables
 164        ; mapM_ (checkBndrIdInScope binder) bndr_vars
 165
 166        ; when (isNonRuleLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
 167               (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
 168               -- Only non-rule loop breakers inhibit inlining
 169
 170       -- Check whether arity and demand type are consistent (only if demand analysis
 171       -- already happened)
 172        ; checkL (case maybeDmdTy of
 173                   Just (StrictSig dmd_ty) -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs
 174                   Nothing -> True)
 175            (mkArityMsg binder) }
 176
 177         -- We should check the unfolding, if any, but this is tricky because
 178         -- the unfolding is a SimplifiableCoreExpr. Give up for now.
 179    where
 180     binder_ty                  = idType binder
 181     maybeDmdTy                 = idStrictness_maybe binder
 182     bndr_vars                  = varSetElems (idFreeVars binder)
 183     lintBinder var | isId var  = lintIdBndr var $ \_ -> (return ())
 184                    | otherwise = return ()
 185 \end{code}
 186
 187 %************************************************************************
 188 %*                                                                      *
 189 \subsection[lintCoreExpr]{lintCoreExpr}
 190 %*                                                                      *
 191 %************************************************************************
 192
 193 \begin{code}
 194 type InType  = Type     -- Substitution not yet applied
 195 type InVar   = Var
 196 type InTyVar = TyVar
 197
 198 type OutType  = Type    -- Substitution has been applied to this
 199 type OutVar   = Var
 200 type OutTyVar = TyVar
 201 type OutCoVar = CoVar
 202
 203 lintCoreExpr :: CoreExpr -> LintM OutType
 204 -- The returned type has the substitution from the monad
 205 -- already applied to it:
 206 --      lintCoreExpr e subst = exprType (subst e)
 207 --
 208 -- The returned "type" can be a kind, if the expression is (Type ty)
 209
 210 lintCoreExpr (Var var)
 211   = do  { checkL (not (var == oneTupleDataConId))
 212                  (ptext (sLit "Illegal one-tuple"))
 213
 214         ; checkDeadIdOcc var
 215         ; var' <- lookupIdInScope var
 216         ; return (idType var') }
 217
 218 lintCoreExpr (Lit lit)
 219   = return (literalType lit)
 220
 221 lintCoreExpr (Cast expr co)
 222   = do { expr_ty <- lintCoreExpr expr
 223        ; co' <- applySubst co
 224        ; (from_ty, to_ty) <- lintCoercion co'
 225        ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
 226        ; return to_ty }
 227
 228 lintCoreExpr (Note _ expr)
 229   = lintCoreExpr expr
 230
 231 lintCoreExpr (Let (NonRec tv (Type ty)) body)
 232   | isTyVar tv
 233   =     -- See Note [Linting type lets]
 234     do  { ty' <- addLoc (RhsOf tv) $ lintInTy ty
 235         ; lintTyBndr tv              $ \ tv' ->
 236           addLoc (BodyOfLetRec [tv]) $
 237           extendSubstL tv' ty'       $ do
 238         { checkKinds tv' ty'
 239                 -- Now extend the substitution so we
 240                 -- take advantage of it in the body
 241         ; lintCoreExpr body } }
 242
 243   | isCoVar tv
 244   = do { co <- applySubst ty
 245        ; (s1,s2) <- addLoc (RhsOf tv) $ lintCoercion co
 246        ; lintTyBndr tv  $ \ tv' ->
 247          addLoc (BodyOfLetRec [tv]) $ do
 248        { let (t1,t2) = coVarKind tv'
 249        ; checkTys s1 t1 (mkTyVarLetErr tv ty)
 250        ; checkTys s2 t2 (mkTyVarLetErr tv ty)
 251        ; lintCoreExpr body } }
 252
 253   | otherwise
 254   = failWithL (mkTyVarLetErr tv ty)     -- Not quite accurate
 255
 256 lintCoreExpr (Let (NonRec bndr rhs) body)
 257   = do  { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
 258         ; addLoc (BodyOfLetRec [bndr])
 259                  (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
 260
 261 lintCoreExpr (Let (Rec pairs) body)
 262   = lintAndScopeIds bndrs       $ \_ ->
 263     do  { mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
 264         ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
 265   where
 266     bndrs = map fst pairs
 267
 268 lintCoreExpr e@(App fun arg)
 269   = do  { fun_ty <- lintCoreExpr fun
 270         ; addLoc (AnExpr e) $
 271           lintCoreArg fun_ty arg }
 272
 273 lintCoreExpr (Lam var expr)
 274   = addLoc (LambdaBodyOf var) $
 275     lintBinders [var] $ \ vars' ->
 276     do { let [var'] = vars'
 277        ; body_ty <- lintCoreExpr expr
 278        ; if isId var' then
 279              return (mkFunTy (idType var') body_ty)
 280          else
 281              return (mkForAllTy var' body_ty)
 282        }
 283         -- The applySubst is needed to apply the subst to var
 284
 285 lintCoreExpr e@(Case scrut var alt_ty alts) =
 286        -- Check the scrutinee
 287   do { scrut_ty <- lintCoreExpr scrut
 288      ; alt_ty   <- lintInTy alt_ty
 289      ; var_ty   <- lintInTy (idType var)
 290
 291      ; let mb_tc_app = splitTyConApp_maybe (idType var)
 292      ; case mb_tc_app of
 293          Just (tycon, _)
 294               | debugIsOn &&
 295                 isAlgTyCon tycon &&
 296                 not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
 297                 null (tyConDataCons tycon) ->
 298                   pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
 299                         -- This can legitimately happen for type families
 300                       $ return ()
 301          _otherwise -> return ()
 302
 303         -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
 304
 305      ; subst <- getTvSubst
 306      ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
 307
 308      -- If the binder is an unboxed tuple type, don't put it in scope
 309      ; let scope = if (isUnboxedTupleType (idType var)) then
 310                        pass_var
 311                    else lintAndScopeId var
 312      ; scope $ \_ ->
 313        do { -- Check the alternatives
 314             mapM_ (lintCoreAlt scrut_ty alt_ty) alts
 315           ; checkCaseAlts e scrut_ty alts
 316           ; return alt_ty } }
 317   where
 318     pass_var f = f var
 319
 320 lintCoreExpr (Type ty)
 321   = do { ty' <- lintInTy ty
 322        ; return (typeKind ty') }
 323 \end{code}
 324
 325 %************************************************************************
 326 %*                                                                      *
 327 \subsection[lintCoreArgs]{lintCoreArgs}
 328 %*                                                                      *
 329 %************************************************************************
 330
 331 The basic version of these functions checks that the argument is a
 332 subtype of the required type, as one would expect.
 333
 334 \begin{code}
 335 lintCoreArg  :: OutType -> CoreArg -> LintM OutType
 336 lintCoreArg fun_ty (Type arg_ty)
 337   = do  { arg_ty' <- applySubst arg_ty
 338         ; lintTyApp fun_ty arg_ty' }
 339
 340 lintCoreArg fun_ty arg
 341  = do { arg_ty <- lintCoreExpr arg
 342       ; lintValApp arg fun_ty arg_ty }
 343
 344 -----------------
 345 lintAltBinders :: OutType     -- Scrutinee type
 346                -> OutType     -- Constructor type
 347                -> [OutVar]    -- Binders
 348                -> LintM ()
 349 lintAltBinders scrut_ty con_ty []
 350   = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
 351 lintAltBinders scrut_ty con_ty (bndr:bndrs)
 352   | isTyCoVar bndr
 353   = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
 354        ; lintAltBinders scrut_ty con_ty' bndrs }
 355   | otherwise
 356   = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
 357        ; lintAltBinders scrut_ty con_ty' bndrs }
 358
 359 -----------------
 360 lintTyApp :: OutType -> OutType -> LintM OutType
 361 lintTyApp fun_ty arg_ty
 362   | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
 363   = do  { checkKinds tyvar arg_ty
 364         ; if isCoVar tyvar then
 365              return body_ty   -- Co-vars don't appear in body_ty!
 366           else
 367              return (substTyWith [tyvar] [arg_ty] body_ty) }
 368   | otherwise
 369   = failWithL (mkTyAppMsg fun_ty arg_ty)
 370
 371 -----------------
 372 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
 373 lintValApp arg fun_ty arg_ty
 374   | Just (arg,res) <- splitFunTy_maybe fun_ty
 375   = do { checkTys arg arg_ty err1
 376        ; return res }
 377   | otherwise
 378   = failWithL err2
 379   where
 380     err1 = mkAppMsg       fun_ty arg_ty arg
 381     err2 = mkNonFunAppMsg fun_ty arg_ty arg
 382 \end{code}
 383
 384 \begin{code}
 385 checkKinds :: OutVar -> OutType -> LintM ()
 386 -- Both args have had substitution applied
 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 = do { (s2,t2) <- lintCoercion arg_ty
 393                        ; unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
 394                                 (addErrL (mkCoAppErrMsg tyvar arg_ty)) }
 395   | otherwise     = do { arg_kind <- lintType arg_ty
 396                        ; unless (arg_kind `isSubKind` tyvar_kind)
 397                                 (addErrL (mkKindErrMsg tyvar arg_ty)) }
 398   where
 399     tyvar_kind = tyVarKind tyvar
 400     (s1,t1)    = coVarKind tyvar
 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)
 478   = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
 479   | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
 480   = addLoc (CaseAlt alt) $  do
 481     {   -- First instantiate the universally quantified
 482         -- type variables of the data constructor
 483         -- We've already check
 484       checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
 485     ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
 486
 487         -- And now bring the new binders into scope
 488     ; lintBinders args $ \ args' -> do
 489     { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
 490     ; checkAltExpr rhs alt_ty } }
 491
 492   | otherwise   -- Scrut-ty is wrong shape
 493   = addErrL (mkBadAltMsg scrut_ty alt)
 494 \end{code}
 495
 496 %************************************************************************
 497 %*                                                                      *
 498 \subsection[lint-types]{Types}
 499 %*                                                                      *
 500 %************************************************************************
 501
 502 \begin{code}
 503 -- When we lint binders, we (one at a time and in order):
 504 --  1. Lint var types or kinds (possibly substituting)
 505 --  2. Add the binder to the in scope set, and if its a coercion var,
 506 --     we may extend the substitution to reflect its (possibly) new kind
 507 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
 508 lintBinders [] linterF = linterF []
 509 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
 510                                  lintBinders vars $ \ vars' ->
 511                                  linterF (var':vars')
 512
 513 lintBinder :: Var -> (Var -> LintM a) -> LintM a
 514 lintBinder var linterF
 515   | isId var  = lintIdBndr var linterF
 516   | otherwise = lintTyBndr var linterF
 517
 518 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
 519 lintTyBndr tv thing_inside
 520   = do { subst <- getTvSubst
 521        ; let (subst', tv') = substTyVarBndr subst tv
 522        ; lintTyBndrKind tv'
 523        ; updateTvSubst subst' (thing_inside tv') }
 524
 525 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
 526 -- Do substitution on the type of a binder and add the var with this
 527 -- new type to the in-scope set of the second argument
 528 -- ToDo: lint its rules
 529
 530 lintIdBndr id linterF
 531   = do  { checkL (not (isUnboxedTupleType (idType id)))
 532                  (mkUnboxedTupleMsg id)
 533                 -- No variable can be bound to an unboxed tuple.
 534         ; lintAndScopeId id $ \id' -> linterF id' }
 535
 536 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
 537 lintAndScopeIds ids linterF
 538   = go ids
 539   where
 540     go []       = linterF []
 541     go (id:ids) = lintAndScopeId id $ \id ->
 542                   lintAndScopeIds ids $ \ids ->
 543                   linterF (id:ids)
 544
 545 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
 546 lintAndScopeId id linterF
 547   = do { ty <- lintInTy (idType id)
 548        ; let id' = setIdType id ty
 549        ; addInScopeVar id' $ (linterF id') }
 550 \end{code}
 551
 552
 553 %************************************************************************
 554 %*                                                                      *
 555 \subsection[lint-monad]{The Lint monad}
 556 %*                                                                      *
 557 %************************************************************************
 558
 559 \begin{code}
 560 lintInTy :: 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 lintInTy ty
 565   = addLoc (InType ty) $
 566     do  { ty' <- applySubst ty
 567         ; _ <- lintType ty'
 568         ; return ty' }
 569
 570 -------------------
 571 lintKind :: Kind -> LintM ()
 572 -- Check well-formedness of kinds: *, *->*, etc
 573 lintKind (TyConApp tc [])
 574   | getUnique tc `elem` kindKeys
 575   = return ()
 576 lintKind (FunTy k1 k2)
 577   = lintKind k1 >> lintKind k2
 578 lintKind kind
 579   = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
 580
 581 -------------------
 582 lintTyBndrKind :: OutTyVar -> LintM ()
 583 lintTyBndrKind tv
 584   | isCoVar tv = lintCoVarKind tv
 585   | otherwise  = lintKind (tyVarKind tv)
 586
 587 -------------------
 588 lintCoVarKind :: OutCoVar -> LintM ()
 589 -- Check the kind of a coercion binder
 590 lintCoVarKind tv
 591   = do { (ty1,ty2) <- lintSplitCoVar tv
 592        ; k1 <- lintType ty1
 593        ; k2 <- lintType ty2
 594        ; unless (k1 `eqKind` k2)
 595                 (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:")
 596                               , nest 2 (quotes (ppr tv))
 597                               , ppr [k1,k2] ])) }
 598
 599 -------------------
 600 lintSplitCoVar :: CoVar -> LintM (Type,Type)
 601 lintSplitCoVar cv
 602   = case coVarKind_maybe cv of
 603       Just ts -> return ts
 604       Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
 605                                 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
 606
 607 -------------------
 608 lintCoercion, lintCoercion' :: OutType -> LintM (OutType, OutType)
 609 -- Check the kind of a coercion term, returning the kind
 610 lintCoercion co
 611   = addLoc (InCoercion co) $ lintCoercion' co
 612
 613 lintCoercion' ty@(TyVarTy tv)
 614   = do { checkTyVarInScope tv
 615        ; if isCoVar tv then return (coVarKind tv)
 616                        else return (ty, ty) }
 617
 618 lintCoercion' ty@(AppTy ty1 ty2)
 619   = do { (s1,t1) <- lintCoercion ty1
 620        ; (s2,t2) <- lintCoercion ty2
 621        ; check_co_app ty (typeKind s1) [s2]
 622        ; return (mkAppTy s1 s2, mkAppTy t1 t2) }
 623
 624 lintCoercion' ty@(FunTy ty1 ty2)
 625   = do { (s1,t1) <- lintCoercion ty1
 626        ; (s2,t2) <- lintCoercion ty2
 627        ; check_co_app ty (tyConKind funTyCon) [s1, s2]
 628        ; return (FunTy s1 s2, FunTy t1 t2) }
 629
 630 lintCoercion' ty@(TyConApp tc tys)
 631   | Just (ar, desc) <- isCoercionTyCon_maybe tc
 632   = do { unless (tys `lengthAtLeast` ar) (badCo ty)
 633        ; (s,t) <- lintCoTyConApp ty desc (take ar tys)
 634        ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
 635        ; check_co_app ty (typeKind s) ss
 636        ; return (mkAppTys s ss, mkAppTys t ts) }
 637
 638   | not (tyConHasKind tc)       -- Just something bizarre like SuperKindTyCon
 639   = badCo ty
 640
 641   | otherwise
 642   = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
 643        ; check_co_app ty (tyConKind tc) ss
 644        ; return (TyConApp tc ss, TyConApp tc ts) }
 645
 646 lintCoercion' ty@(PredTy (ClassP cls tys))
 647   = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
 648        ; check_co_app ty (tyConKind (classTyCon cls)) ss
 649        ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
 650
 651 lintCoercion' (PredTy (IParam n p_ty))
 652   = do { (s,t) <- lintCoercion p_ty
 653        ; return (PredTy (IParam n s), PredTy (IParam n t)) }
 654
 655 lintCoercion' ty@(PredTy (EqPred {}))
 656   = failWithL (badEq ty)
 657
 658 lintCoercion' (ForAllTy tv ty)
 659   | isCoVar tv
 660   = do { (co1, co2) <- lintSplitCoVar tv
 661        ; (s1,t1)    <- lintCoercion co1
 662        ; (s2,t2)    <- lintCoercion co2
 663        ; (sr,tr)    <- lintCoercion ty
 664        ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) }
 665
 666   | otherwise
 667   = do { lintKind (tyVarKind tv)
 668        ; (s,t) <- addInScopeVar tv (lintCoercion ty)
 669        ; return (ForAllTy tv s, ForAllTy tv t) }
 670
 671 badCo :: Coercion -> LintM a
 672 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
 673
 674 ---------------
 675 lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type)
 676 -- Always called with correct number of coercion arguments
 677 -- First arg is just for error message
 678 lintCoTyConApp _ CoLeft  (co:_) = lintLR   fst      co
 679 lintCoTyConApp _ CoRight (co:_) = lintLR   snd      co
 680 lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3   co
 681 lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3   co
 682 lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co
 683
 684 lintCoTyConApp _ CoSym (co:_)
 685   = do { (ty1,ty2) <- lintCoercion co
 686        ; return (ty2,ty1) }
 687
 688 lintCoTyConApp co CoTrans (co1:co2:_)
 689   = do { (ty1a, ty1b) <- lintCoercion co1
 690        ; (ty2a, ty2b) <- lintCoercion co2
 691        ; checkL (ty1b `coreEqType` ty2a)
 692                 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
 693                     2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
 694        ; return (ty1a, ty2b) }
 695
 696 lintCoTyConApp _ CoInst (co:arg_ty:_)
 697   = do { co_tys <- lintCoercion co
 698        ; arg_kind  <- lintType arg_ty
 699        ; case decompInst_maybe co_tys of
 700           Just ((tv1,tv2), (ty1,ty2))
 701             | arg_kind `isSubKind` tyVarKind tv1
 702             -> return (substTyWith [tv1] [arg_ty] ty1,
 703                        substTyWith [tv2] [arg_ty] ty2)
 704             | otherwise
 705             -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
 706           Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
 707
 708 lintCoTyConApp _ (CoAxiom { co_ax_tvs = tvs
 709                           , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
 710   = do { (tys1, tys2) <- mapAndUnzipM lintCoercion cos
 711        ; sequence_ (zipWith checkKinds tvs tys1)
 712        ; return (substTyWith tvs tys1 lhs_ty,
 713                  substTyWith tvs tys2 rhs_ty) }
 714
 715 lintCoTyConApp _ CoUnsafe (ty1:ty2:_)
 716   = do { _ <- lintType ty1
 717        ; _ <- lintType ty2      -- Ignore kinds; it's unsafe!
 718        ; return (ty1,ty2) }
 719
 720 lintCoTyConApp _ _ _ = panic "lintCoTyConApp"  -- Called with wrong number of coercion args
 721
 722 ----------
 723 lintLR :: (forall a. (a,a)->a) -> Coercion -> LintM (Type,Type)
 724 lintLR sel co
 725   = do { (ty1,ty2) <- lintCoercion co
 726        ; case decompLR_maybe (ty1,ty2) of
 727            Just res -> return (sel res)
 728            Nothing  -> failWithL (ptext (sLit "Bad argument of left/right")) }
 729
 730 ----------
 731 lintCsel :: (forall a. (a,a,a)->a) -> Coercion -> LintM (Type,Type)
 732 lintCsel sel co
 733   = do { (ty1,ty2) <- lintCoercion co
 734        ; case decompCsel_maybe (ty1,ty2) of
 735            Just res -> return (sel res)
 736            Nothing  -> failWithL (ptext (sLit "Bad argument of csel")) }
 737
 738 -------------------
 739 lintType :: OutType -> LintM Kind
 740 lintType (TyVarTy tv)
 741   = do { checkTyVarInScope tv
 742        ; return (tyVarKind tv) }
 743
 744 lintType ty@(AppTy t1 t2)
 745   = do { k1 <- lintType t1
 746        ; lint_ty_app ty k1 [t2] }
 747
 748 lintType ty@(FunTy t1 t2)
 749   = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
 750
 751 lintType ty@(TyConApp tc tys)
 752   | tyConHasKind tc
 753   = lint_ty_app ty (tyConKind tc) tys
 754   | otherwise
 755   = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
 756
 757 lintType (ForAllTy tv ty)
 758   = do { lintTyBndrKind tv
 759        ; addInScopeVar tv (lintType ty) }
 760
 761 lintType ty@(PredTy (ClassP cls tys))
 762   = lint_ty_app ty (tyConKind (classTyCon cls)) tys
 763
 764 lintType (PredTy (IParam _ p_ty))
 765   = lintType p_ty
 766
 767 lintType ty@(PredTy (EqPred {}))
 768   = failWithL (badEq ty)
 769
 770 ----------------
 771 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
 772 lint_ty_app ty k tys
 773   = do { ks <- mapM lintType tys
 774        ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
 775
 776 ----------------
 777 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
 778 check_co_app ty k tys
 779   = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
 780                             k (map typeKind tys)
 781        ; return () }
 782
 783 ----------------
 784 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
 785 lint_kind_app doc kfn ks = go kfn ks
 786   where
 787     fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
 788                      nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
 789                      nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
 790
 791     go kfn []     = return kfn
 792     go kfn (k:ks) = case splitKindFunTy_maybe kfn of
 793                       Nothing         -> failWithL fail_msg
 794                       Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
 795                                                      (addErrL fail_msg)
 796                                             ; go kfb ks }
 797 --------------
 798 badEq :: Type -> SDoc
 799 badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
 800               1 (quotes (ppr ty))
 801 \end{code}
 802
 803 %************************************************************************
 804 %*                                                                      *
 805 \subsection[lint-monad]{The Lint monad}
 806 %*                                                                      *
 807 %************************************************************************
 808
 809 \begin{code}
 810 newtype LintM a =
 811    LintM { unLintM ::
 812             [LintLocInfo] ->         -- Locations
 813             TvSubst ->               -- Current type substitution; we also use this
 814                                      -- to keep track of all the variables in scope,
 815                                      -- both Ids and TyVars
 816             WarnsAndErrs ->           -- Error and warning messages so far
 817             (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
 818
 819 type WarnsAndErrs = (Bag Message, Bag Message)
 820
 821 {-      Note [Type substitution]
 822         ~~~~~~~~~~~~~~~~~~~~~~~~
 823 Why do we need a type substitution?  Consider
 824         /\(a:*). \(x:a). /\(a:*). id a x
 825 This is ill typed, because (renaming variables) it is really
 826         /\(a:*). \(x:a). /\(b:*). id b x
 827 Hence, when checking an application, we can't naively compare x's type
 828 (at its binding site) with its expected type (at a use site).  So we
 829 rename type binders as we go, maintaining a substitution.
 830
 831 The same substitution also supports let-type, current expressed as
 832         (/\(a:*). body) ty
 833 Here we substitute 'ty' for 'a' in 'body', on the fly.
 834 -}
 835
 836 instance Monad LintM where
 837   return x = LintM (\ _   _     errs -> (Just x, errs))
 838   fail err = failWithL (text err)
 839   m >>= k  = LintM (\ loc subst errs ->
 840                        let (res, errs') = unLintM m loc subst errs in
 841                          case res of
 842                            Just r -> unLintM (k r) loc subst errs'
 843                            Nothing -> (Nothing, errs'))
 844
 845 data LintLocInfo
 846   = RhsOf Id            -- The variable bound
 847   | LambdaBodyOf Id     -- The lambda-binder
 848   | BodyOfLetRec [Id]   -- One of the binders
 849   | CaseAlt CoreAlt     -- Case alternative
 850   | CasePat CoreAlt     -- The *pattern* of the case alternative
 851   | AnExpr CoreExpr     -- Some expression
 852   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
 853   | TopLevelBindings
 854   | InType Type         -- Inside a type
 855   | InCoercion Coercion -- Inside a type
 856 \end{code}
 857
 858
 859 \begin{code}
 860 initL :: LintM a -> WarnsAndErrs    -- Errors and warnings
 861 initL m
 862   = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
 863       (_, errs) -> errs
 864 \end{code}
 865
 866 \begin{code}
 867 checkL :: Bool -> Message -> LintM ()
 868 checkL True  _   = return ()
 869 checkL False msg = failWithL msg
 870
 871 failWithL :: Message -> LintM a
 872 failWithL msg = LintM $ \ loc subst (warns,errs) ->
 873                 (Nothing, (warns, addMsg subst errs msg loc))
 874
 875 addErrL :: Message -> LintM ()
 876 addErrL msg = LintM $ \ loc subst (warns,errs) ->
 877               (Just (), (warns, addMsg subst errs msg loc))
 878
 879 addWarnL :: Message -> LintM ()
 880 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
 881               (Just (), (addMsg subst warns msg loc, errs))
 882
 883 addMsg :: TvSubst ->  Bag Message -> Message -> [LintLocInfo] -> Bag Message
 884 addMsg subst msgs msg locs
 885   = ASSERT( notNull locs )
 886     msgs `snocBag` mk_msg msg
 887   where
 888    (loc, cxt1) = dumpLoc (head locs)
 889    cxts        = [snd (dumpLoc loc) | loc <- locs]
 890    context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
 891                                       ptext (sLit "Substitution:") <+> ppr subst
 892                | otherwise          = cxt1
 893
 894    mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
 895
 896 addLoc :: LintLocInfo -> LintM a -> LintM a
 897 addLoc extra_loc m =
 898   LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
 899
 900 inCasePat :: LintM Bool         -- A slight hack; see the unique call site
 901 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
 902   where
 903     is_case_pat (CasePat {} : _) = True
 904     is_case_pat _other           = False
 905
 906 addInScopeVars :: [Var] -> LintM a -> LintM a
 907 addInScopeVars vars m
 908   | null dups
 909   = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
 910   | otherwise
 911   = failWithL (dupVars dups)
 912   where
 913     (_, dups) = removeDups compare vars
 914
 915 addInScopeVar :: Var -> LintM a -> LintM a
 916 addInScopeVar var m
 917   = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
 918
 919 updateTvSubst :: TvSubst -> LintM a -> LintM a
 920 updateTvSubst subst' m =
 921   LintM (\ loc _ errs -> unLintM m loc subst' errs)
 922
 923 getTvSubst :: LintM TvSubst
 924 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
 925
 926 applySubst :: Type -> LintM Type
 927 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
 928
 929 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
 930 extendSubstL tv ty m
 931   = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
 932 \end{code}
 933
 934 \begin{code}
 935 lookupIdInScope :: Id -> LintM Id
 936 lookupIdInScope id
 937   | not (mustHaveLocalBinding id)
 938   = return id   -- An imported Id
 939   | otherwise
 940   = do  { subst <- getTvSubst
 941         ; case lookupInScope (getTvInScope subst) id of
 942                 Just v  -> return v
 943                 Nothing -> do { addErrL out_of_scope
 944                               ; return id } }
 945   where
 946     out_of_scope = ppr id <+> ptext (sLit "is out of scope")
 947
 948
 949 oneTupleDataConId :: Id -- Should not happen
 950 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
 951
 952 checkBndrIdInScope :: Var -> Var -> LintM ()
 953 checkBndrIdInScope binder id
 954   = checkInScope msg id
 955     where
 956      msg = ptext (sLit "is out of scope inside info for") <+>
 957            ppr binder
 958
 959 checkTyVarInScope :: TyVar -> LintM ()
 960 checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
 961
 962 checkInScope :: SDoc -> Var -> LintM ()
 963 checkInScope loc_msg var =
 964  do { subst <- getTvSubst
 965     ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
 966              (hsep [ppr var, loc_msg]) }
 967
 968 checkTys :: OutType -> OutType -> Message -> LintM ()
 969 -- check ty2 is subtype of ty1 (ie, has same structure but usage
 970 -- annotations need only be consistent, not equal)
 971 -- Assumes ty1,ty2 are have alrady had the substitution applied
 972 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
 973 \end{code}
 974
 975 %************************************************************************
 976 %*                                                                      *
 977 \subsection{Error messages}
 978 %*                                                                      *
 979 %************************************************************************
 980
 981 \begin{code}
 982 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
 983
 984 dumpLoc (RhsOf v)
 985   = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
 986
 987 dumpLoc (LambdaBodyOf b)
 988   = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
 989
 990 dumpLoc (BodyOfLetRec [])
 991   = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
 992
 993 dumpLoc (BodyOfLetRec bs@(_:_))
 994   = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
 995
 996 dumpLoc (AnExpr e)
 997   = (noSrcLoc, text "In the expression:" <+> ppr e)
 998
 999 dumpLoc (CaseAlt (con, args, _))
1000   = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1001
1002 dumpLoc (CasePat (con, args, _))
1003   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1004
1005 dumpLoc (ImportedUnfolding locn)
1006   = (locn, brackets (ptext (sLit "in an imported unfolding")))
1007 dumpLoc TopLevelBindings
1008   = (noSrcLoc, empty)
1009 dumpLoc (InType ty)
1010   = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1011 dumpLoc (InCoercion ty)
1012   = (noSrcLoc, text "In the coercion" <+> quotes (ppr ty))
1013
1014 pp_binders :: [Var] -> SDoc
1015 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1016
1017 pp_binder :: Var -> SDoc
1018 pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
1019             | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1020 \end{code}
1021
1022 \begin{code}
1023 ------------------------------------------------------
1024 --      Messages for case expressions
1025
1026 mkNullAltsMsg :: CoreExpr -> Message
1027 mkNullAltsMsg e
1028   = hang (text "Case expression with no alternatives:")
1029          4 (ppr e)
1030
1031 mkDefaultArgsMsg :: [Var] -> Message
1032 mkDefaultArgsMsg args
1033   = hang (text "DEFAULT case with binders")
1034          4 (ppr args)
1035
1036 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
1037 mkCaseAltMsg e ty1 ty2
1038   = hang (text "Type of case alternatives not the same as the annotation on case:")
1039          4 (vcat [ppr ty1, ppr ty2, ppr e])
1040
1041 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
1042 mkScrutMsg var var_ty scrut_ty subst
1043   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1044           text "Result binder type:" <+> ppr var_ty,--(idType var),
1045           text "Scrutinee type:" <+> ppr scrut_ty,
1046      hsep [ptext (sLit "Current TV subst"), ppr subst]]
1047
1048 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
1049 mkNonDefltMsg e
1050   = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1051 mkNonIncreasingAltsMsg e
1052   = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1053
1054 nonExhaustiveAltsMsg :: CoreExpr -> Message
1055 nonExhaustiveAltsMsg e
1056   = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1057
1058 mkBadConMsg :: TyCon -> DataCon -> Message
1059 mkBadConMsg tycon datacon
1060   = vcat [
1061         text "In a case alternative, data constructor isn't in scrutinee type:",
1062         text "Scrutinee type constructor:" <+> ppr tycon,
1063         text "Data con:" <+> ppr datacon
1064     ]
1065
1066 mkBadPatMsg :: Type -> Type -> Message
1067 mkBadPatMsg con_result_ty scrut_ty
1068   = vcat [
1069         text "In a case alternative, pattern result type doesn't match scrutinee type:",
1070         text "Pattern result type:" <+> ppr con_result_ty,
1071         text "Scrutinee type:" <+> ppr scrut_ty
1072     ]
1073
1074 mkBadAltMsg :: Type -> CoreAlt -> Message
1075 mkBadAltMsg scrut_ty alt
1076   = vcat [ text "Data alternative when scrutinee is not a tycon application",
1077            text "Scrutinee type:" <+> ppr scrut_ty,
1078            text "Alternative:" <+> pprCoreAlt alt ]
1079
1080 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1081 mkNewTyDataConAltMsg scrut_ty alt
1082   = vcat [ text "Data alternative for newtype datacon",
1083            text "Scrutinee type:" <+> ppr scrut_ty,
1084            text "Alternative:" <+> pprCoreAlt alt ]
1085
1086
1087 ------------------------------------------------------
1088 --      Other error messages
1089
1090 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1091 mkAppMsg fun_ty arg_ty arg
1092   = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1093               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1094               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1095               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1096
1097 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1098 mkNonFunAppMsg fun_ty arg_ty arg
1099   = vcat [ptext (sLit "Non-function type in function position"),
1100               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1101               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1102               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1103
1104 mkTyVarLetErr :: TyVar -> Type -> Message
1105 mkTyVarLetErr tyvar ty
1106   = vcat [ptext (sLit "Bad `let' binding for type or coercion variable:"),
1107           hang (ptext (sLit "Type/coercion variable:"))
1108                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1109           hang (ptext (sLit "Arg type/coercion:"))
1110                  4 (ppr ty)]
1111
1112 mkKindErrMsg :: TyVar -> Type -> Message
1113 mkKindErrMsg tyvar arg_ty
1114   = vcat [ptext (sLit "Kinds don't match in type application:"),
1115           hang (ptext (sLit "Type variable:"))
1116                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1117           hang (ptext (sLit "Arg type:"))
1118                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1119
1120 mkCoAppErrMsg :: TyVar -> Type -> Message
1121 mkCoAppErrMsg tyvar arg_ty
1122   = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1123           hang (ptext (sLit "Coercion variable:"))
1124                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1125           hang (ptext (sLit "Arg coercion:"))
1126                  4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
1127
1128 mkTyAppMsg :: Type -> Type -> Message
1129 mkTyAppMsg ty arg_ty
1130   = vcat [text "Illegal type application:",
1131               hang (ptext (sLit "Exp type:"))
1132                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1133               hang (ptext (sLit "Arg type:"))
1134                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1135
1136 mkRhsMsg :: Id -> Type -> Message
1137 mkRhsMsg binder ty
1138   = vcat
1139     [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1140             ppr binder],
1141      hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1142      hsep [ptext (sLit "Rhs type:"), ppr ty]]
1143
1144 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1145 mkRhsPrimMsg binder _rhs
1146   = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1147                      ppr binder],
1148               hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1149              ]
1150
1151 mkStrictMsg :: Id -> Message
1152 mkStrictMsg binder
1153   = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1154                      ppr binder],
1155               hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1156              ]
1157
1158 mkArityMsg :: Id -> Message
1159 mkArityMsg binder
1160   = vcat [hsep [ptext (sLit "Demand type has "),
1161                      ppr (dmdTypeDepth dmd_ty),
1162                      ptext (sLit " arguments, rhs has "),
1163                      ppr (idArity binder),
1164                      ptext (sLit "arguments, "),
1165                      ppr binder],
1166               hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1167
1168          ]
1169            where (StrictSig dmd_ty) = idStrictness binder
1170
1171 mkUnboxedTupleMsg :: Id -> Message
1172 mkUnboxedTupleMsg binder
1173   = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1174           hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1175
1176 mkCastErr :: Type -> Type -> Message
1177 mkCastErr from_ty expr_ty
1178   = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1179           ptext (sLit "From-type:") <+> ppr from_ty,
1180           ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1181     ]
1182
1183 dupVars :: [[Var]] -> Message
1184 dupVars vars
1185   = hang (ptext (sLit "Duplicate variables brought into scope"))
1186        2 (ppr vars)
1187 \end{code}