compiler/coreSyn/CoreLint.lhs

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