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
 219 lintCoreExpr (Lit lit)
 220   = return (literalType lit)
 221
 222 lintCoreExpr (Cast expr co)
 223   = do { expr_ty <- lintCoreExpr expr
 224        ; co' <- applySubst co
 225        ; (from_ty, to_ty) <- lintCoercion co'
 226        ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
 227        ; return to_ty }
 228
 229 lintCoreExpr (Note _ expr)
 230   = lintCoreExpr expr
 231
 232 lintCoreExpr (Let (NonRec tv (Type ty)) body)
 233   =     -- See Note [Type let] in CoreSyn
 234     do  { checkL (isTyVar tv) (mkKindErrMsg tv ty)      -- Not quite accurate
 235         ; ty' <- lintInTy ty
 236         ; lintTyBndr tv              $ \ tv' ->
 237           addLoc (BodyOfLetRec [tv]) $
 238           extendSubstL tv' ty'       $ do
 239         { checkKinds tv' ty'
 240                 -- Now extend the substitution so we
 241                 -- take advantage of it in the body
 242         ; lintCoreExpr body } }
 243
 244 lintCoreExpr (Let (NonRec bndr rhs) body)
 245   = do  { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
 246         ; addLoc (BodyOfLetRec [bndr])
 247                  (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
 248
 249 lintCoreExpr (Let (Rec pairs) body)
 250   = lintAndScopeIds bndrs       $ \_ ->
 251     do  { mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
 252         ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
 253   where
 254     bndrs = map fst pairs
 255
 256 lintCoreExpr e@(App fun arg)
 257   = do  { fun_ty <- lintCoreExpr fun
 258         ; addLoc (AnExpr e) $
 259           lintCoreArg fun_ty arg }
 260
 261 lintCoreExpr (Lam var expr)
 262   = addLoc (LambdaBodyOf var) $
 263     lintBinders [var] $ \[var'] ->
 264     do { body_ty <- lintCoreExpr expr
 265        ; if isId var' then
 266              return (mkFunTy (idType var') body_ty)
 267          else
 268              return (mkForAllTy var' body_ty)
 269        }
 270         -- The applySubst is needed to apply the subst to var
 271
 272 lintCoreExpr e@(Case scrut var alt_ty alts) =
 273        -- Check the scrutinee
 274   do { scrut_ty <- lintCoreExpr scrut
 275      ; alt_ty   <- lintInTy alt_ty
 276      ; var_ty   <- lintInTy (idType var)
 277
 278      ; let mb_tc_app = splitTyConApp_maybe (idType var)
 279      ; case mb_tc_app of
 280          Just (tycon, _)
 281               | debugIsOn &&
 282                 isAlgTyCon tycon &&
 283                 not (isOpenTyCon tycon) &&
 284                 null (tyConDataCons tycon) ->
 285                   pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
 286                         -- This can legitimately happen for type families
 287                       $ return ()
 288          _otherwise -> return ()
 289
 290         -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
 291
 292      ; subst <- getTvSubst
 293      ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
 294
 295      -- If the binder is an unboxed tuple type, don't put it in scope
 296      ; let scope = if (isUnboxedTupleType (idType var)) then
 297                        pass_var
 298                    else lintAndScopeId var
 299      ; scope $ \_ ->
 300        do { -- Check the alternatives
 301             mapM_ (lintCoreAlt scrut_ty alt_ty) alts
 302           ; checkCaseAlts e scrut_ty alts
 303           ; return alt_ty } }
 304   where
 305     pass_var f = f var
 306
 307 lintCoreExpr (Type ty)
 308   = do { ty' <- lintInTy ty
 309        ; return (typeKind ty') }
 310 \end{code}
 311
 312 %************************************************************************
 313 %*                                                                      *
 314 \subsection[lintCoreArgs]{lintCoreArgs}
 315 %*                                                                      *
 316 %************************************************************************
 317
 318 The basic version of these functions checks that the argument is a
 319 subtype of the required type, as one would expect.
 320
 321 \begin{code}
 322 lintCoreArg  :: OutType -> CoreArg -> LintM OutType
 323 lintCoreArg fun_ty (Type arg_ty)
 324   = do  { arg_ty' <- applySubst arg_ty
 325         ; lintTyApp fun_ty arg_ty' }
 326
 327 lintCoreArg fun_ty arg
 328  = do { arg_ty <- lintCoreExpr arg
 329       ; lintValApp arg fun_ty arg_ty }
 330
 331 -----------------
 332 lintAltBinders :: OutType     -- Scrutinee type
 333                -> OutType     -- Constructor type
 334                -> [OutVar]    -- Binders
 335                -> LintM ()
 336 lintAltBinders scrut_ty con_ty []
 337   = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
 338 lintAltBinders scrut_ty con_ty (bndr:bndrs)
 339   | isTyVar bndr
 340   = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
 341        ; lintAltBinders scrut_ty con_ty' bndrs }
 342   | otherwise
 343   = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
 344        ; lintAltBinders scrut_ty con_ty' bndrs }
 345
 346 -----------------
 347 lintTyApp :: OutType -> OutType -> LintM OutType
 348 lintTyApp fun_ty arg_ty
 349   | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
 350   = do  { checkKinds tyvar arg_ty
 351         ; if isCoVar tyvar then
 352              return body_ty   -- Co-vars don't appear in body_ty!
 353           else
 354              return (substTyWith [tyvar] [arg_ty] body_ty) }
 355   | otherwise
 356   = failWithL (mkTyAppMsg fun_ty arg_ty)
 357
 358 -----------------
 359 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
 360 lintValApp arg fun_ty arg_ty
 361   | Just (arg,res) <- splitFunTy_maybe fun_ty
 362   = do { checkTys arg arg_ty err1
 363        ; return res }
 364   | otherwise
 365   = failWithL err2
 366   where
 367     err1 = mkAppMsg       fun_ty arg_ty arg
 368     err2 = mkNonFunAppMsg fun_ty arg_ty arg
 369 \end{code}
 370
 371 \begin{code}
 372 checkKinds :: Var -> OutType -> LintM ()
 373 -- Both args have had substitution applied
 374 checkKinds tyvar arg_ty
 375         -- Arg type might be boxed for a function with an uncommitted
 376         -- tyvar; notably this is used so that we can give
 377         --      error :: forall a:*. String -> a
 378         -- and then apply it to both boxed and unboxed types.
 379   | isCoVar tyvar = do { (s2,t2) <- lintCoercion arg_ty
 380                        ; unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
 381                                 (addErrL (mkCoAppErrMsg tyvar arg_ty)) }
 382   | otherwise     = do { arg_kind <- lintType arg_ty
 383                        ; unless (arg_kind `isSubKind` tyvar_kind)
 384                                 (addErrL (mkKindErrMsg tyvar arg_ty)) }
 385   where
 386     tyvar_kind = tyVarKind tyvar
 387     (s1,t1)    = coVarKind tyvar
 388
 389 checkDeadIdOcc :: Id -> LintM ()
 390 -- Occurrences of an Id should never be dead....
 391 -- except when we are checking a case pattern
 392 checkDeadIdOcc id
 393   | isDeadOcc (idOccInfo id)
 394   = do { in_case <- inCasePat
 395        ; checkL in_case
 396                 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
 397   | otherwise
 398   = return ()
 399 \end{code}
 400
 401
 402 %************************************************************************
 403 %*                                                                      *
 404 \subsection[lintCoreAlts]{lintCoreAlts}
 405 %*                                                                      *
 406 %************************************************************************
 407
 408 \begin{code}
 409 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
 410 -- a) Check that the alts are non-empty
 411 -- b1) Check that the DEFAULT comes first, if it exists
 412 -- b2) Check that the others are in increasing order
 413 -- c) Check that there's a default for infinite types
 414 -- NB: Algebraic cases are not necessarily exhaustive, because
 415 --     the simplifer correctly eliminates case that can't
 416 --     possibly match.
 417
 418 checkCaseAlts e _ []
 419   = addErrL (mkNullAltsMsg e)
 420
 421 checkCaseAlts e ty alts =
 422   do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
 423      ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
 424      ; checkL (isJust maybe_deflt || not is_infinite_ty)
 425            (nonExhaustiveAltsMsg e) }
 426   where
 427     (con_alts, maybe_deflt) = findDefault alts
 428
 429         -- Check that successive alternatives have increasing tags
 430     increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
 431     increasing_tag _                         = True
 432
 433     non_deflt (DEFAULT, _, _) = False
 434     non_deflt _               = True
 435
 436     is_infinite_ty = case splitTyConApp_maybe ty of
 437                         Nothing         -> False
 438                         Just (tycon, _) -> isPrimTyCon tycon
 439 \end{code}
 440
 441 \begin{code}
 442 checkAltExpr :: CoreExpr -> OutType -> LintM ()
 443 checkAltExpr expr ann_ty
 444   = do { actual_ty <- lintCoreExpr expr
 445        ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
 446
 447 lintCoreAlt :: OutType          -- Type of scrutinee
 448             -> OutType          -- Type of the alternative
 449             -> CoreAlt
 450             -> LintM ()
 451
 452 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
 453   do { checkL (null args) (mkDefaultArgsMsg args)
 454      ; checkAltExpr rhs alt_ty }
 455
 456 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) =
 457   do { checkL (null args) (mkDefaultArgsMsg args)
 458      ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
 459      ; checkAltExpr rhs alt_ty }
 460   where
 461     lit_ty = literalType lit
 462
 463 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
 464   | isNewTyCon (dataConTyCon con)
 465   = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
 466   | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
 467   = addLoc (CaseAlt alt) $  do
 468     {   -- First instantiate the universally quantified
 469         -- type variables of the data constructor
 470         -- We've already check
 471       checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
 472     ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
 473
 474         -- And now bring the new binders into scope
 475     ; lintBinders args $ \ args' -> do
 476     { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
 477     ; checkAltExpr rhs alt_ty } }
 478
 479   | otherwise   -- Scrut-ty is wrong shape
 480   = addErrL (mkBadAltMsg scrut_ty alt)
 481 \end{code}
 482
 483 %************************************************************************
 484 %*                                                                      *
 485 \subsection[lint-types]{Types}
 486 %*                                                                      *
 487 %************************************************************************
 488
 489 \begin{code}
 490 -- When we lint binders, we (one at a time and in order):
 491 --  1. Lint var types or kinds (possibly substituting)
 492 --  2. Add the binder to the in scope set, and if its a coercion var,
 493 --     we may extend the substitution to reflect its (possibly) new kind
 494 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
 495 lintBinders [] linterF = linterF []
 496 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
 497                                  lintBinders vars $ \ vars' ->
 498                                  linterF (var':vars')
 499
 500 lintBinder :: Var -> (Var -> LintM a) -> LintM a
 501 lintBinder var linterF
 502   | isId var  = lintIdBndr var linterF
 503   | otherwise = lintTyBndr var linterF
 504
 505 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
 506 lintTyBndr tv thing_inside
 507   = do { subst <- getTvSubst
 508        ; let (subst', tv') = substTyVarBndr subst tv
 509        ; lintTyBndrKind tv'
 510        ; updateTvSubst subst' (thing_inside tv') }
 511
 512 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
 513 -- Do substitution on the type of a binder and add the var with this
 514 -- new type to the in-scope set of the second argument
 515 -- ToDo: lint its rules
 516
 517 lintIdBndr id linterF
 518   = do  { checkL (not (isUnboxedTupleType (idType id)))
 519                  (mkUnboxedTupleMsg id)
 520                 -- No variable can be bound to an unboxed tuple.
 521         ; lintAndScopeId id $ \id' -> linterF id' }
 522
 523 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
 524 lintAndScopeIds ids linterF
 525   = go ids
 526   where
 527     go []       = linterF []
 528     go (id:ids) = lintAndScopeId id $ \id ->
 529                   lintAndScopeIds ids $ \ids ->
 530                   linterF (id:ids)
 531
 532 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
 533 lintAndScopeId id linterF
 534   = do { ty <- lintInTy (idType id)
 535        ; let id' = setIdType id ty
 536        ; addInScopeVar id' $ (linterF id') }
 537 \end{code}
 538
 539
 540 %************************************************************************
 541 %*                                                                      *
 542 \subsection[lint-monad]{The Lint monad}
 543 %*                                                                      *
 544 %************************************************************************
 545
 546 \begin{code}
 547 lintInTy :: InType -> LintM OutType
 548 -- Check the type, and apply the substitution to it
 549 -- See Note [Linting type lets]
 550 -- ToDo: check the kind structure of the type
 551 lintInTy ty
 552   = addLoc (InType ty) $
 553     do  { ty' <- applySubst ty
 554         ; _ <- lintType ty'
 555         ; return ty' }
 556
 557 -------------------
 558 lintKind :: Kind -> LintM ()
 559 -- Check well-formedness of kinds: *, *->*, etc
 560 lintKind (TyConApp tc [])
 561   | getUnique tc `elem` kindKeys
 562   = return ()
 563 lintKind (FunTy k1 k2)
 564   = lintKind k1 >> lintKind k2
 565 lintKind kind
 566   = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
 567
 568 -------------------
 569 lintTyBndrKind :: OutTyVar -> LintM ()
 570 lintTyBndrKind tv
 571   | isCoVar tv = lintCoVarKind tv
 572   | otherwise  = lintKind (tyVarKind tv)
 573
 574 -------------------
 575 lintCoVarKind :: OutCoVar -> LintM ()
 576 -- Check the kind of a coercion binder
 577 lintCoVarKind tv
 578   = do { (ty1,ty2) <- lintSplitCoVar tv
 579        ; k1 <- lintType ty1
 580        ; k2 <- lintType ty2
 581        ; unless (k1 `eqKind` k2)
 582                 (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:")
 583                               , nest 2 (quotes (ppr tv))
 584                               , ppr [k1,k2] ])) }
 585
 586 -------------------
 587 lintSplitCoVar :: CoVar -> LintM (Type,Type)
 588 lintSplitCoVar cv
 589   = case coVarKind_maybe cv of
 590       Just ts -> return ts
 591       Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
 592                                 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
 593
 594 -------------------
 595 lintCoercion :: OutType -> LintM (OutType, OutType)
 596 -- Check the kind of a coercion term, returning the kind
 597 lintCoercion ty@(TyVarTy tv)
 598   = do { checkTyVarInScope tv
 599        ; if isCoVar tv then return (coVarKind tv)
 600                        else return (ty, ty) }
 601
 602 lintCoercion ty@(AppTy ty1 ty2)
 603   = do { (s1,t1) <- lintCoercion ty1
 604        ; (s2,t2) <- lintCoercion ty2
 605        ; check_co_app ty (typeKind s1) [s2]
 606        ; return (AppTy s1 s2, AppTy t1 t2) }
 607
 608 lintCoercion ty@(FunTy ty1 ty2)
 609   = do { (s1,t1) <- lintCoercion ty1
 610        ; (s2,t2) <- lintCoercion ty2
 611        ; check_co_app ty (tyConKind funTyCon) [s1, s2]
 612        ; return (FunTy s1 s2, FunTy t1 t2) }
 613
 614 lintCoercion ty@(TyConApp tc tys)
 615   | Just (ar, desc) <- isCoercionTyCon_maybe tc
 616   = do { unless (tys `lengthAtLeast` ar) (badCo ty)
 617        ; (s,t) <- lintCoTyConApp ty desc (take ar tys)
 618        ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
 619        ; check_co_app ty (typeKind s) ss
 620        ; return (mkAppTys s ss, mkAppTys t ts) }
 621
 622   | not (tyConHasKind tc)       -- Just something bizarre like SuperKindTyCon
 623   = badCo ty
 624
 625   | otherwise
 626   = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
 627        ; check_co_app ty (tyConKind tc) ss
 628        ; return (TyConApp tc ss, TyConApp tc ts) }
 629
 630 lintCoercion ty@(PredTy (ClassP cls tys))
 631   = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
 632        ; check_co_app ty (tyConKind (classTyCon cls)) ss
 633        ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
 634
 635 lintCoercion (PredTy (IParam n p_ty))
 636   = do { (s,t) <- lintCoercion p_ty
 637        ; return (PredTy (IParam n s), PredTy (IParam n t)) }
 638
 639 lintCoercion ty@(PredTy (EqPred {}))
 640   = failWithL (badEq ty)
 641
 642 lintCoercion (ForAllTy tv ty)
 643   | isCoVar tv
 644   = do { (co1, co2) <- lintSplitCoVar tv
 645        ; (s1,t1)    <- lintCoercion co1
 646        ; (s2,t2)    <- lintCoercion co2
 647        ; (sr,tr)    <- lintCoercion ty
 648        ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) }
 649
 650   | otherwise
 651   = do { lintKind (tyVarKind tv)
 652        ; (s,t) <- addInScopeVar tv (lintCoercion ty)
 653        ; return (ForAllTy tv s, ForAllTy tv t) }
 654
 655 badCo :: Coercion -> LintM a
 656 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
 657
 658 ---------------
 659 lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type)
 660 -- Always called with correct number of coercion arguments
 661 -- First arg is just for error message
 662 lintCoTyConApp _ CoLeft  (co:_) = lintLR   fst      co
 663 lintCoTyConApp _ CoRight (co:_) = lintLR   snd      co
 664 lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3   co
 665 lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3   co
 666 lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co
 667
 668 lintCoTyConApp _ CoSym (co:_)
 669   = do { (ty1,ty2) <- lintCoercion co
 670        ; return (ty2,ty1) }
 671
 672 lintCoTyConApp co CoTrans (co1:co2:_)
 673   = do { (ty1a, ty1b) <- lintCoercion co1
 674        ; (ty2a, ty2b) <- lintCoercion co2
 675        ; checkL (ty1b `coreEqType` ty2a)
 676                 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
 677                     2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
 678        ; return (ty1a, ty2b) }
 679
 680 lintCoTyConApp _ CoInst (co:arg_ty:_)
 681   = do { co_tys <- lintCoercion co
 682        ; arg_kind  <- lintType arg_ty
 683        ; case decompInst_maybe co_tys of
 684           Just ((tv1,tv2), (ty1,ty2))
 685             | arg_kind `isSubKind` tyVarKind tv1
 686             -> return (substTyWith [tv1] [arg_ty] ty1,
 687                        substTyWith [tv2] [arg_ty] ty2)
 688             | otherwise
 689             -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
 690           Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
 691
 692 lintCoTyConApp _ (CoAxiom { co_ax_tvs = tvs
 693                           , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
 694   = do { (tys1, tys2) <- mapAndUnzipM lintCoercion cos
 695        ; sequence_ (zipWith checkKinds tvs tys1)
 696        ; return (substTyWith tvs tys1 lhs_ty,
 697                  substTyWith tvs tys2 rhs_ty) }
 698
 699 lintCoTyConApp _ CoUnsafe (ty1:ty2:_)
 700   = do { _ <- lintType ty1
 701        ; _ <- lintType ty2      -- Ignore kinds; it's unsafe!
 702        ; return (ty1,ty2) }
 703
 704 lintCoTyConApp _ _ _ = panic "lintCoTyConApp"  -- Called with wrong number of coercion args
 705
 706 ----------
 707 lintLR :: (forall a. (a,a)->a) -> Coercion -> LintM (Type,Type)
 708 lintLR sel co
 709   = do { (ty1,ty2) <- lintCoercion co
 710        ; case decompLR_maybe (ty1,ty2) of
 711            Just res -> return (sel res)
 712            Nothing  -> failWithL (ptext (sLit "Bad argument of left/right")) }
 713
 714 ----------
 715 lintCsel :: (forall a. (a,a,a)->a) -> Coercion -> LintM (Type,Type)
 716 lintCsel sel co
 717   = do { (ty1,ty2) <- lintCoercion co
 718        ; case decompCsel_maybe (ty1,ty2) of
 719            Just res -> return (sel res)
 720            Nothing  -> failWithL (ptext (sLit "Bad argument of csel")) }
 721
 722 -------------------
 723 lintType :: OutType -> LintM Kind
 724 lintType (TyVarTy tv)
 725   = do { checkTyVarInScope tv
 726        ; return (tyVarKind tv) }
 727
 728 lintType ty@(AppTy t1 t2)
 729   = do { k1 <- lintType t1
 730        ; lint_ty_app ty k1 [t2] }
 731
 732 lintType ty@(FunTy t1 t2)
 733   = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
 734
 735 lintType ty@(TyConApp tc tys)
 736   | tyConHasKind tc
 737   = lint_ty_app ty (tyConKind tc) tys
 738   | otherwise
 739   = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
 740
 741 lintType (ForAllTy tv ty)
 742   = do { lintTyBndrKind tv
 743        ; addInScopeVar tv (lintType ty) }
 744
 745 lintType ty@(PredTy (ClassP cls tys))
 746   = lint_ty_app ty (tyConKind (classTyCon cls)) tys
 747
 748 lintType (PredTy (IParam _ p_ty))
 749   = lintType p_ty
 750
 751 lintType ty@(PredTy (EqPred {}))
 752   = failWithL (badEq ty)
 753
 754 ----------------
 755 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
 756 lint_ty_app ty k tys
 757   = do { ks <- mapM lintType tys
 758        ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
 759
 760 ----------------
 761 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
 762 check_co_app ty k tys
 763   = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
 764                             k (map typeKind tys)
 765        ; return () }
 766
 767 ----------------
 768 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
 769 lint_kind_app doc kfn ks = go kfn ks
 770   where
 771     fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
 772                      nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
 773                      nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
 774
 775     go kfn []     = return kfn
 776     go kfn (k:ks) = case splitKindFunTy_maybe kfn of
 777                       Nothing         -> failWithL fail_msg
 778                       Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
 779                                                      (addErrL fail_msg)
 780                                             ; go kfb ks }
 781 --------------
 782 badEq :: Type -> SDoc
 783 badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
 784               1 (quotes (ppr ty))
 785 \end{code}
 786
 787 %************************************************************************
 788 %*                                                                      *
 789 \subsection[lint-monad]{The Lint monad}
 790 %*                                                                      *
 791 %************************************************************************
 792
 793 \begin{code}
 794 newtype LintM a =
 795    LintM { unLintM ::
 796             [LintLocInfo] ->         -- Locations
 797             TvSubst ->               -- Current type substitution; we also use this
 798                                      -- to keep track of all the variables in scope,
 799                                      -- both Ids and TyVars
 800             WarnsAndErrs ->           -- Error and warning messages so far
 801             (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
 802
 803 type WarnsAndErrs = (Bag Message, Bag Message)
 804
 805 {-      Note [Type substitution]
 806         ~~~~~~~~~~~~~~~~~~~~~~~~
 807 Why do we need a type substitution?  Consider
 808         /\(a:*). \(x:a). /\(a:*). id a x
 809 This is ill typed, because (renaming variables) it is really
 810         /\(a:*). \(x:a). /\(b:*). id b x
 811 Hence, when checking an application, we can't naively compare x's type
 812 (at its binding site) with its expected type (at a use site).  So we
 813 rename type binders as we go, maintaining a substitution.
 814
 815 The same substitution also supports let-type, current expressed as
 816         (/\(a:*). body) ty
 817 Here we substitute 'ty' for 'a' in 'body', on the fly.
 818 -}
 819
 820 instance Monad LintM where
 821   return x = LintM (\ _   _     errs -> (Just x, errs))
 822   fail err = failWithL (text err)
 823   m >>= k  = LintM (\ loc subst errs ->
 824                        let (res, errs') = unLintM m loc subst errs in
 825                          case res of
 826                            Just r -> unLintM (k r) loc subst errs'
 827                            Nothing -> (Nothing, errs'))
 828
 829 data LintLocInfo
 830   = RhsOf Id            -- The variable bound
 831   | LambdaBodyOf Id     -- The lambda-binder
 832   | BodyOfLetRec [Id]   -- One of the binders
 833   | CaseAlt CoreAlt     -- Case alternative
 834   | CasePat CoreAlt     -- The *pattern* of the case alternative
 835   | AnExpr CoreExpr     -- Some expression
 836   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
 837   | TopLevelBindings
 838   | InType Type         -- Inside a type
 839 \end{code}
 840
 841
 842 \begin{code}
 843 initL :: LintM a -> WarnsAndErrs    -- Errors and warnings
 844 initL m
 845   = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
 846       (_, errs) -> errs
 847 \end{code}
 848
 849 \begin{code}
 850 checkL :: Bool -> Message -> LintM ()
 851 checkL True  _   = return ()
 852 checkL False msg = failWithL msg
 853
 854 failWithL :: Message -> LintM a
 855 failWithL msg = LintM $ \ loc subst (warns,errs) ->
 856                 (Nothing, (warns, addMsg subst errs msg loc))
 857
 858 addErrL :: Message -> LintM ()
 859 addErrL msg = LintM $ \ loc subst (warns,errs) ->
 860               (Just (), (warns, addMsg subst errs msg loc))
 861
 862 addWarnL :: Message -> LintM ()
 863 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
 864               (Just (), (addMsg subst warns msg loc, errs))
 865
 866 addMsg :: TvSubst ->  Bag Message -> Message -> [LintLocInfo] -> Bag Message
 867 addMsg subst msgs msg locs
 868   = ASSERT( notNull locs )
 869     msgs `snocBag` mk_msg msg
 870   where
 871    (loc, cxt1) = dumpLoc (head locs)
 872    cxts        = [snd (dumpLoc loc) | loc <- locs]
 873    context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
 874                                       ptext (sLit "Substitution:") <+> ppr subst
 875                | otherwise          = cxt1
 876
 877    mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
 878
 879 addLoc :: LintLocInfo -> LintM a -> LintM a
 880 addLoc extra_loc m =
 881   LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
 882
 883 inCasePat :: LintM Bool         -- A slight hack; see the unique call site
 884 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
 885   where
 886     is_case_pat (CasePat {} : _) = True
 887     is_case_pat _other           = False
 888
 889 addInScopeVars :: [Var] -> LintM a -> LintM a
 890 addInScopeVars vars m
 891   | null dups
 892   = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
 893   | otherwise
 894   = failWithL (dupVars dups)
 895   where
 896     (_, dups) = removeDups compare vars
 897
 898 addInScopeVar :: Var -> LintM a -> LintM a
 899 addInScopeVar var m
 900   = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
 901
 902 updateTvSubst :: TvSubst -> LintM a -> LintM a
 903 updateTvSubst subst' m =
 904   LintM (\ loc _ errs -> unLintM m loc subst' errs)
 905
 906 getTvSubst :: LintM TvSubst
 907 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
 908
 909 applySubst :: Type -> LintM Type
 910 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
 911
 912 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
 913 extendSubstL tv ty m
 914   = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
 915 \end{code}
 916
 917 \begin{code}
 918 lookupIdInScope :: Id -> LintM Id
 919 lookupIdInScope id
 920   | not (mustHaveLocalBinding id)
 921   = return id   -- An imported Id
 922   | otherwise
 923   = do  { subst <- getTvSubst
 924         ; case lookupInScope (getTvInScope subst) id of
 925                 Just v  -> return v
 926                 Nothing -> do { addErrL out_of_scope
 927                               ; return id } }
 928   where
 929     out_of_scope = ppr id <+> ptext (sLit "is out of scope")
 930
 931
 932 oneTupleDataConId :: Id -- Should not happen
 933 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
 934
 935 checkBndrIdInScope :: Var -> Var -> LintM ()
 936 checkBndrIdInScope binder id
 937   = checkInScope msg id
 938     where
 939      msg = ptext (sLit "is out of scope inside info for") <+>
 940            ppr binder
 941
 942 checkTyVarInScope :: TyVar -> LintM ()
 943 checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
 944
 945 checkInScope :: SDoc -> Var -> LintM ()
 946 checkInScope loc_msg var =
 947  do { subst <- getTvSubst
 948     ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
 949              (hsep [ppr var, loc_msg]) }
 950
 951 checkTys :: OutType -> OutType -> Message -> LintM ()
 952 -- check ty2 is subtype of ty1 (ie, has same structure but usage
 953 -- annotations need only be consistent, not equal)
 954 -- Assumes ty1,ty2 are have alrady had the substitution applied
 955 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
 956 \end{code}
 957
 958 %************************************************************************
 959 %*                                                                      *
 960 \subsection{Error messages}
 961 %*                                                                      *
 962 %************************************************************************
 963
 964 \begin{code}
 965 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
 966
 967 dumpLoc (RhsOf v)
 968   = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
 969
 970 dumpLoc (LambdaBodyOf b)
 971   = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
 972
 973 dumpLoc (BodyOfLetRec [])
 974   = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
 975
 976 dumpLoc (BodyOfLetRec bs@(_:_))
 977   = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
 978
 979 dumpLoc (AnExpr e)
 980   = (noSrcLoc, text "In the expression:" <+> ppr e)
 981
 982 dumpLoc (CaseAlt (con, args, _))
 983   = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
 984
 985 dumpLoc (CasePat (con, args, _))
 986   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
 987
 988 dumpLoc (ImportedUnfolding locn)
 989   = (locn, brackets (ptext (sLit "in an imported unfolding")))
 990 dumpLoc TopLevelBindings
 991   = (noSrcLoc, empty)
 992 dumpLoc (InType ty)
 993   = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
 994
 995 pp_binders :: [Var] -> SDoc
 996 pp_binders bs = sep (punctuate comma (map pp_binder bs))
 997
 998 pp_binder :: Var -> SDoc
 999 pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
1000             | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1001 \end{code}
1002
1003 \begin{code}
1004 ------------------------------------------------------
1005 --      Messages for case expressions
1006
1007 mkNullAltsMsg :: CoreExpr -> Message
1008 mkNullAltsMsg e
1009   = hang (text "Case expression with no alternatives:")
1010          4 (ppr e)
1011
1012 mkDefaultArgsMsg :: [Var] -> Message
1013 mkDefaultArgsMsg args
1014   = hang (text "DEFAULT case with binders")
1015          4 (ppr args)
1016
1017 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
1018 mkCaseAltMsg e ty1 ty2
1019   = hang (text "Type of case alternatives not the same as the annotation on case:")
1020          4 (vcat [ppr ty1, ppr ty2, ppr e])
1021
1022 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
1023 mkScrutMsg var var_ty scrut_ty subst
1024   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1025           text "Result binder type:" <+> ppr var_ty,--(idType var),
1026           text "Scrutinee type:" <+> ppr scrut_ty,
1027      hsep [ptext (sLit "Current TV subst"), ppr subst]]
1028
1029 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
1030 mkNonDefltMsg e
1031   = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1032 mkNonIncreasingAltsMsg e
1033   = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1034
1035 nonExhaustiveAltsMsg :: CoreExpr -> Message
1036 nonExhaustiveAltsMsg e
1037   = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1038
1039 mkBadConMsg :: TyCon -> DataCon -> Message
1040 mkBadConMsg tycon datacon
1041   = vcat [
1042         text "In a case alternative, data constructor isn't in scrutinee type:",
1043         text "Scrutinee type constructor:" <+> ppr tycon,
1044         text "Data con:" <+> ppr datacon
1045     ]
1046
1047 mkBadPatMsg :: Type -> Type -> Message
1048 mkBadPatMsg con_result_ty scrut_ty
1049   = vcat [
1050         text "In a case alternative, pattern result type doesn't match scrutinee type:",
1051         text "Pattern result type:" <+> ppr con_result_ty,
1052         text "Scrutinee type:" <+> ppr scrut_ty
1053     ]
1054
1055 mkBadAltMsg :: Type -> CoreAlt -> Message
1056 mkBadAltMsg scrut_ty alt
1057   = vcat [ text "Data alternative when scrutinee is not a tycon application",
1058            text "Scrutinee type:" <+> ppr scrut_ty,
1059            text "Alternative:" <+> pprCoreAlt alt ]
1060
1061 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1062 mkNewTyDataConAltMsg scrut_ty alt
1063   = vcat [ text "Data alternative for newtype datacon",
1064            text "Scrutinee type:" <+> ppr scrut_ty,
1065            text "Alternative:" <+> pprCoreAlt alt ]
1066
1067
1068 ------------------------------------------------------
1069 --      Other error messages
1070
1071 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1072 mkAppMsg fun_ty arg_ty arg
1073   = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1074               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1075               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1076               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1077
1078 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1079 mkNonFunAppMsg fun_ty arg_ty arg
1080   = vcat [ptext (sLit "Non-function type in function position"),
1081               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1082               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1083               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1084
1085 mkKindErrMsg :: TyVar -> Type -> Message
1086 mkKindErrMsg tyvar arg_ty
1087   = vcat [ptext (sLit "Kinds don't match in type application:"),
1088           hang (ptext (sLit "Type variable:"))
1089                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1090           hang (ptext (sLit "Arg type:"))
1091                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1092
1093 mkCoAppErrMsg :: TyVar -> Type -> Message
1094 mkCoAppErrMsg tyvar arg_ty
1095   = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1096           hang (ptext (sLit "Coercion variable:"))
1097                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1098           hang (ptext (sLit "Arg coercion:"))
1099                  4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
1100
1101 mkTyAppMsg :: Type -> Type -> Message
1102 mkTyAppMsg ty arg_ty
1103   = vcat [text "Illegal type application:",
1104               hang (ptext (sLit "Exp type:"))
1105                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1106               hang (ptext (sLit "Arg type:"))
1107                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1108
1109 mkRhsMsg :: Id -> Type -> Message
1110 mkRhsMsg binder ty
1111   = vcat
1112     [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1113             ppr binder],
1114      hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1115      hsep [ptext (sLit "Rhs type:"), ppr ty]]
1116
1117 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1118 mkRhsPrimMsg binder _rhs
1119   = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1120                      ppr binder],
1121               hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1122              ]
1123
1124 mkStrictMsg :: Id -> Message
1125 mkStrictMsg binder
1126   = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1127                      ppr binder],
1128               hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1129              ]
1130
1131 mkArityMsg :: Id -> Message
1132 mkArityMsg binder
1133   = vcat [hsep [ptext (sLit "Demand type has "),
1134                      ppr (dmdTypeDepth dmd_ty),
1135                      ptext (sLit " arguments, rhs has "),
1136                      ppr (idArity binder),
1137                      ptext (sLit "arguments, "),
1138                      ppr binder],
1139               hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1140
1141          ]
1142            where (StrictSig dmd_ty) = idStrictness binder
1143
1144 mkUnboxedTupleMsg :: Id -> Message
1145 mkUnboxedTupleMsg binder
1146   = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1147           hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1148
1149 mkCastErr :: Type -> Type -> Message
1150 mkCastErr from_ty expr_ty
1151   = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1152           ptext (sLit "From-type:") <+> ppr from_ty,
1153           ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1154     ]
1155
1156 dupVars :: [[Var]] -> Message
1157 dupVars vars
1158   = hang (ptext (sLit "Duplicate variables brought into scope"))
1159        2 (ppr vars)
1160 \end{code}