compiler/coreSyn/CoreLint.lhs

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