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