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