0e9bcce895a50549d898f9bbca0677bfc879176a
[ghc.git] / 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 {-# OPTIONS -fno-warn-tabs #-}
11 -- The above warning supression flag is a temporary kludge.
12 -- While working on this module you are encouraged to remove it and
13 -- detab the module (please do the detabbing in a separate patch). See
14 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
15 -- for details
16
17 {-# OPTIONS_GHC -fprof-auto #-}
18
19 module CoreLint ( lintCoreBindings, lintUnfolding ) where
20
21 #include "HsVersions.h"
22
23 import Demand
24 import CoreSyn
25 import CoreFVs
26 import CoreUtils
27 import Pair
28 import Bag
29 import Literal
30 import DataCon
31 import TysWiredIn
32 import TysPrim
33 import Var
34 import VarEnv
35 import VarSet
36 import Name
37 import Id
38 import PprCore
39 import ErrUtils
40 import Coercion
41 import SrcLoc
42 import Kind
43 import Type
44 import TypeRep
45 import TyCon
46 import CoAxiom
47 import BasicTypes
48 import StaticFlags
49 import ListSetOps
50 import PrelNames
51 import Outputable
52 import FastString
53 import Util
54 import OptCoercion ( checkAxInstCo )
55 import Control.Monad
56 import MonadUtils
57 import Data.Maybe
58 \end{code}
59
60 Note [GHC Formalism]
61 ~~~~~~~~~~~~~~~~~~~~
62 This file implements the type-checking algorithm for System FC, the "official"
63 name of the Core language. Type safety of FC is heart of the claim that
64 executables produced by GHC do not have segmentation faults. Thus, it is
65 useful to be able to reason about System FC independently of reading the code.
66 To this purpose, there is a document ghc.pdf built in docs/core-spec that
67 contains a formalism of the types and functions dealt with here. If you change
68 just about anything in this file or you change other types/functions throughout
69 the Core language (all signposted to this note), you should update that
70 formalism. See docs/core-spec/README for more info about how to do so.
71
72 %************************************************************************
73 %*                                                                      *
74 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
75 %*                                                                      *
76 %************************************************************************
77
78 Checks that a set of core bindings is well-formed.  The PprStyle and String
79 just control what we print in the event of an error.  The Bool value
80 indicates whether we have done any specialisation yet (in which case we do
81 some extra checks).
82
83 We check for
84         (a) type errors
85         (b) Out-of-scope type variables
86         (c) Out-of-scope local variables
87         (d) Ill-kinded types
88
89 If we have done specialisation the we check that there are
90         (a) No top-level bindings of primitive (unboxed type)
91
92 Outstanding issues:
93
94     --
95     -- Things are *not* OK if:
96     --
97     --  * Unsaturated type app before specialisation has been done;
98     --
99     --  * Oversaturated type app after specialisation (eta reduction
100     --   may well be happening...);
101
102
103 Note [Linting type lets]
104 ~~~~~~~~~~~~~~~~~~~~~~~~
105 In the desugarer, it's very very convenient to be able to say (in effect)
106         let a = Type Int in <body>
107 That is, use a type let.   See Note [Type let] in CoreSyn.
108
109 However, when linting <body> we need to remember that a=Int, else we might
110 reject a correct program.  So we carry a type substitution (in this example 
111 [a -> Int]) and apply this substitution before comparing types.  The functin
112         lintInTy :: Type -> LintM Type
113 returns a substituted type; that's the only reason it returns anything.
114
115 When we encounter a binder (like x::a) we must apply the substitution
116 to the type of the binding variable.  lintBinders does this.
117
118 For Ids, the type-substituted Id is added to the in_scope set (which 
119 itself is part of the TvSubst we are carrying down), and when we
120 find an occurence of an Id, we fetch it from the in-scope set.
121
122
123 \begin{code}
124 lintCoreBindings :: CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
125 --   Returns (warnings, errors)
126 -- If you edit this function, you may need to update the GHC formalism
127 -- See Note [GHC Formalism]
128 lintCoreBindings binds
129   = initL $ 
130     addLoc TopLevelBindings $
131     addInScopeVars binders  $
132         -- Put all the top-level binders in scope at the start
133         -- This is because transformation rules can bring something
134         -- into use 'unexpectedly'
135     do { checkL (null dups) (dupVars dups)
136        ; checkL (null ext_dups) (dupExtVars ext_dups)
137        ; mapM lint_bind binds }
138   where
139     binders = bindersOfBinds binds
140     (_, dups) = removeDups compare binders
141
142     -- dups_ext checks for names with different uniques
143     -- but but the same External name M.n.  We don't
144     -- allow this at top level:
145     --    M.n{r3}  = ...
146     --    M.n{r29} = ...
147     -- because they both get the same linker symbol
148     ext_dups = snd (removeDups ord_ext (map Var.varName binders))
149     ord_ext n1 n2 | Just m1 <- nameModule_maybe n1
150                   , Just m2 <- nameModule_maybe n2
151                   = compare (m1, nameOccName n1) (m2, nameOccName n2)
152                   | otherwise = LT
153
154     -- If you edit this function, you may need to update the GHC formalism
155     -- See Note [GHC Formalism]
156     lint_bind (Rec prs)         = mapM_ (lintSingleBinding TopLevel Recursive) prs
157     lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
158 \end{code}
159
160 %************************************************************************
161 %*                                                                      *
162 \subsection[lintUnfolding]{lintUnfolding}
163 %*                                                                      *
164 %************************************************************************
165
166 We use this to check all unfoldings that come in from interfaces
167 (it is very painful to catch errors otherwise):
168
169 \begin{code}
170 lintUnfolding :: SrcLoc
171               -> [Var]          -- Treat these as in scope
172               -> CoreExpr
173               -> Maybe MsgDoc   -- Nothing => OK
174
175 lintUnfolding locn vars expr
176   | isEmptyBag errs = Nothing
177   | otherwise       = Just (pprMessageBag errs)
178   where
179     (_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
180                             addInScopeVars vars            $
181                             lintCoreExpr expr)
182 \end{code}
183
184 %************************************************************************
185 %*                                                                      *
186 \subsection[lintCoreBinding]{lintCoreBinding}
187 %*                                                                      *
188 %************************************************************************
189
190 Check a core binding, returning the list of variables bound.
191
192 \begin{code}
193 lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
194 -- If you edit this function, you may need to update the GHC formalism
195 -- See Note [GHC Formalism]
196 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
197   = addLoc (RhsOf binder) $
198          -- Check the rhs 
199     do { ty <- lintCoreExpr rhs 
200        ; lintBinder binder -- Check match to RHS type
201        ; binder_ty <- applySubstTy binder_ty
202        ; checkTys binder_ty ty (mkRhsMsg binder ty)
203         -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
204        ; checkL (not (isUnLiftedType binder_ty)
205             || (isNonRec rec_flag && exprOkForSpeculation rhs))
206            (mkRhsPrimMsg binder rhs)
207         -- Check that if the binder is top-level or recursive, it's not demanded
208        ; checkL (not (isStrictId binder)
209             || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
210            (mkStrictMsg binder)
211         -- Check that if the binder is local, it is not marked as exported
212        ; checkL (not (isExportedId binder) || isTopLevel top_lvl_flag)
213            (mkNonTopExportedMsg binder)
214         -- Check that if the binder is local, it does not have an external name
215        ; checkL (not (isExternalName (Var.varName binder)) || isTopLevel top_lvl_flag)
216            (mkNonTopExternalNameMsg binder)
217         -- Check whether binder's specialisations contain any out-of-scope variables
218        ; mapM_ (checkBndrIdInScope binder) bndr_vars 
219
220        ; when (isStrongLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
221               (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
222               -- Only non-rule loop breakers inhibit inlining
223
224       -- Check whether arity and demand type are consistent (only if demand analysis
225       -- already happened)
226        ; checkL (case dmdTy of
227                   StrictSig dmd_ty -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs)
228            (mkArityMsg binder) }
229           
230         -- We should check the unfolding, if any, but this is tricky because
231         -- the unfolding is a SimplifiableCoreExpr. Give up for now.
232    where
233     binder_ty                  = idType binder
234     dmdTy                      = idStrictness binder
235     bndr_vars                  = varSetElems (idFreeVars binder)
236
237     -- If you edit this function, you may need to update the GHC formalism
238     -- See Note [GHC Formalism]
239     lintBinder var | isId var  = lintIdBndr var $ \_ -> (return ())
240                    | otherwise = return ()
241 \end{code}
242
243 %************************************************************************
244 %*                                                                      *
245 \subsection[lintCoreExpr]{lintCoreExpr}
246 %*                                                                      *
247 %************************************************************************
248
249 \begin{code}
250 --type InKind      = Kind       -- Substitution not yet applied
251 type InType      = Type 
252 type InCoercion  = Coercion
253 type InVar       = Var
254 type InTyVar     = TyVar
255
256 type OutKind     = Kind -- Substitution has been applied to this,
257                         -- but has not been linted yet
258 type LintedKind  = Kind -- Substitution applied, and type is linted
259
260 type OutType     = Type -- Substitution has been applied to this,
261                         -- but has not been linted yet
262
263 type LintedType  = Type -- Substitution applied, and type is linted
264
265 type OutCoercion = Coercion
266 type OutVar      = Var
267 type OutTyVar    = TyVar
268
269 lintCoreExpr :: CoreExpr -> LintM OutType
270 -- The returned type has the substitution from the monad 
271 -- already applied to it:
272 --      lintCoreExpr e subst = exprType (subst e)
273 --
274 -- The returned "type" can be a kind, if the expression is (Type ty)
275
276 -- If you edit this function, you may need to update the GHC formalism
277 -- See Note [GHC Formalism]
278 lintCoreExpr (Var var)
279   = do  { checkL (not (var == oneTupleDataConId))
280                  (ptext (sLit "Illegal one-tuple"))
281
282         ; checkL (isId var && not (isCoVar var))
283                  (ptext (sLit "Non term variable") <+> ppr var)
284
285         ; checkDeadIdOcc var
286         ; var' <- lookupIdInScope var
287         ; return (idType var') }
288
289 lintCoreExpr (Lit lit)
290   = return (literalType lit)
291
292 lintCoreExpr (Cast expr co)
293   = do { expr_ty <- lintCoreExpr expr
294        ; co' <- applySubstCo co
295        ; (_, from_ty, to_ty) <- lintCoercion co'
296        ; checkTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
297        ; return to_ty }
298
299 lintCoreExpr (Tick (Breakpoint _ ids) expr)
300   = do forM_ ids $ \id -> do
301          checkDeadIdOcc id
302          lookupIdInScope id
303        lintCoreExpr expr
304
305 lintCoreExpr (Tick _other_tickish expr)
306   = lintCoreExpr expr
307
308 lintCoreExpr (Let (NonRec tv (Type ty)) body)
309   | isTyVar tv
310   =     -- See Note [Linting type lets]
311     do  { ty' <- applySubstTy ty
312         ; lintTyBndr tv              $ \ tv' -> 
313     do  { addLoc (RhsOf tv) $ checkTyKind tv' ty'
314                 -- Now extend the substitution so we 
315                 -- take advantage of it in the body
316         ; extendSubstL tv' ty'       $ 
317           addLoc (BodyOfLetRec [tv]) $ 
318           lintCoreExpr body } }
319
320 lintCoreExpr (Let (NonRec bndr rhs) body)
321   | isId bndr
322   = do  { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
323         ; addLoc (BodyOfLetRec [bndr]) 
324                  (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
325
326   | otherwise
327   = failWithL (mkLetErr bndr rhs)       -- Not quite accurate
328
329 lintCoreExpr (Let (Rec pairs) body) 
330   = lintAndScopeIds bndrs       $ \_ ->
331     do  { checkL (null dups) (dupVars dups)
332         ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs 
333         ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
334   where
335     bndrs = map fst pairs
336     (_, dups) = removeDups compare bndrs
337
338 lintCoreExpr e@(App _ _)
339     = do { fun_ty <- lintCoreExpr fun
340          ; addLoc (AnExpr e) $ foldM lintCoreArg fun_ty args }
341   where
342     (fun, args) = collectArgs e
343
344 lintCoreExpr (Lam var expr)
345   = addLoc (LambdaBodyOf var) $
346     lintBinder var $ \ var' ->
347     do { body_ty <- lintCoreExpr expr
348        ; if isId var' then 
349              return (mkFunTy (idType var') body_ty) 
350          else
351              return (mkForAllTy var' body_ty)
352        }
353         -- The applySubstTy is needed to apply the subst to var
354
355 lintCoreExpr e@(Case scrut var alt_ty alts) =
356        -- Check the scrutinee
357   do { scrut_ty <- lintCoreExpr scrut
358      ; alt_ty   <- lintInTy alt_ty  
359      ; var_ty   <- lintInTy (idType var)        
360
361      ; case tyConAppTyCon_maybe (idType var) of 
362          Just tycon
363               | debugIsOn &&
364                 isAlgTyCon tycon && 
365                 not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
366                 null (tyConDataCons tycon) -> 
367                   pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
368                         -- This can legitimately happen for type families
369                       $ return ()
370          _otherwise -> return ()
371
372         -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
373
374      ; subst <- getTvSubst 
375      ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
376
377      ; lintAndScopeId var $ \_ ->
378        do { -- Check the alternatives
379             mapM_ (lintCoreAlt scrut_ty alt_ty) alts
380           ; checkCaseAlts e scrut_ty alts
381           ; return alt_ty } }
382
383 -- This case can't happen; linting types in expressions gets routed through
384 -- lintCoreArgs
385 lintCoreExpr (Type ty)
386   = pprPanic "lintCoreExpr" (ppr ty)
387
388 lintCoreExpr (Coercion co)
389   = do { co' <- lintInCo co
390        ; let Pair ty1 ty2 = coercionKind co'
391        ; return (mkCoercionType ty1 ty2) }
392
393 \end{code}
394
395 Note [Kind instantiation in coercions]
396 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
397 Consider the following coercion axiom:
398   ax_co [(k_ag :: BOX), (f_aa :: k_ag -> Constraint)] :: T k_ag f_aa ~ f_aa
399
400 Consider the following instantiation:
401   ax_co <* -> *> <Monad>
402
403 We need to split the co_ax_tvs into kind and type variables in order
404 to find out the coercion kind instantiations. Those can only be Refl
405 since we don't have kind coercions. This is just a way to represent
406 kind instantiation.
407
408 We use the number of kind variables to know how to split the coercions
409 instantiations between kind coercions and type coercions. We lint the
410 kind coercions and produce the following substitution which is to be
411 applied in the type variables:
412   k_ag   ~~>   * -> *
413
414 %************************************************************************
415 %*                                                                      *
416 \subsection[lintCoreArgs]{lintCoreArgs}
417 %*                                                                      *
418 %************************************************************************
419
420 The basic version of these functions checks that the argument is a
421 subtype of the required type, as one would expect.
422
423 \begin{code}
424 lintCoreArg  :: OutType -> CoreArg -> LintM OutType
425 lintCoreArg fun_ty (Type arg_ty)
426   = do { arg_ty' <- applySubstTy arg_ty
427        ; lintTyApp fun_ty arg_ty' }
428
429 lintCoreArg fun_ty arg
430   = do { arg_ty <- lintCoreExpr arg
431        ; lintValApp arg fun_ty arg_ty }
432
433 -----------------
434 lintAltBinders :: OutType     -- Scrutinee type
435                -> OutType     -- Constructor type
436                -> [OutVar]    -- Binders
437                -> LintM ()
438 -- If you edit this function, you may need to update the GHC formalism
439 -- See Note [GHC Formalism]
440 lintAltBinders scrut_ty con_ty [] 
441   = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty) 
442 lintAltBinders scrut_ty con_ty (bndr:bndrs)
443   | isTyVar bndr
444   = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
445        ; lintAltBinders scrut_ty con_ty' bndrs }
446   | otherwise
447   = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
448        ; lintAltBinders scrut_ty con_ty' bndrs } 
449
450 -----------------
451 lintTyApp :: OutType -> OutType -> LintM OutType
452 lintTyApp fun_ty arg_ty
453   | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
454   , isTyVar tyvar
455   = do  { checkTyKind tyvar arg_ty
456         ; return (substTyWith [tyvar] [arg_ty] body_ty) }
457
458   | otherwise
459   = failWithL (mkTyAppMsg fun_ty arg_ty)
460    
461 -----------------
462 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
463 lintValApp arg fun_ty arg_ty
464   | Just (arg,res) <- splitFunTy_maybe fun_ty
465   = do { checkTys arg arg_ty err1
466        ; return res }
467   | otherwise
468   = failWithL err2
469   where
470     err1 = mkAppMsg       fun_ty arg_ty arg
471     err2 = mkNonFunAppMsg fun_ty arg_ty arg
472 \end{code}
473
474 \begin{code}
475 checkTyKind :: OutTyVar -> OutType -> LintM ()
476 -- Both args have had substitution applied
477
478 -- If you edit this function, you may need to update the GHC formalism
479 -- See Note [GHC Formalism]
480 checkTyKind tyvar arg_ty
481   | isSuperKind tyvar_kind  -- kind forall
482   = lintKind arg_ty
483         -- Arg type might be boxed for a function with an uncommitted
484         -- tyvar; notably this is used so that we can give
485         --      error :: forall a:*. String -> a
486         -- and then apply it to both boxed and unboxed types.
487   | otherwise  -- type forall
488   = do { arg_kind <- lintType arg_ty
489        ; unless (arg_kind `isSubKind` tyvar_kind)
490                 (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
491   where
492     tyvar_kind = tyVarKind tyvar
493
494 checkDeadIdOcc :: Id -> LintM ()
495 -- Occurrences of an Id should never be dead....
496 -- except when we are checking a case pattern
497 checkDeadIdOcc id
498   | isDeadOcc (idOccInfo id)
499   = do { in_case <- inCasePat
500        ; checkL in_case
501                 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
502   | otherwise
503   = return ()
504 \end{code}
505
506
507 %************************************************************************
508 %*                                                                      *
509 \subsection[lintCoreAlts]{lintCoreAlts}
510 %*                                                                      *
511 %************************************************************************
512
513 \begin{code}
514 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
515 -- a) Check that the alts are non-empty
516 -- b1) Check that the DEFAULT comes first, if it exists
517 -- b2) Check that the others are in increasing order
518 -- c) Check that there's a default for infinite types
519 -- NB: Algebraic cases are not necessarily exhaustive, because
520 --     the simplifer correctly eliminates case that can't 
521 --     possibly match.
522
523 checkCaseAlts e ty alts = 
524   do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
525      ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
526      ; checkL (isJust maybe_deflt || not is_infinite_ty)
527            (nonExhaustiveAltsMsg e) }
528   where
529     (con_alts, maybe_deflt) = findDefault alts
530
531         -- Check that successive alternatives have increasing tags 
532     increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
533     increasing_tag _                         = True
534
535     non_deflt (DEFAULT, _, _) = False
536     non_deflt _               = True
537
538     is_infinite_ty = case tyConAppTyCon_maybe ty of
539                         Nothing    -> False
540                         Just tycon -> isPrimTyCon tycon
541 \end{code}
542
543 \begin{code}
544 checkAltExpr :: CoreExpr -> OutType -> LintM ()
545 checkAltExpr expr ann_ty
546   = do { actual_ty <- lintCoreExpr expr 
547        ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
548
549 lintCoreAlt :: OutType          -- Type of scrutinee
550             -> OutType          -- Type of the alternative
551             -> CoreAlt
552             -> LintM ()
553 -- If you edit this function, you may need to update the GHC formalism
554 -- See Note [GHC Formalism]
555 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
556   do { checkL (null args) (mkDefaultArgsMsg args)
557      ; checkAltExpr rhs alt_ty }
558
559 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
560   | litIsLifted lit
561   = failWithL integerScrutinisedMsg
562   | otherwise
563   = do { checkL (null args) (mkDefaultArgsMsg args)
564        ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
565        ; checkAltExpr rhs alt_ty }
566   where
567     lit_ty = literalType lit
568
569 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
570   | isNewTyCon (dataConTyCon con) 
571   = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
572   | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
573   = addLoc (CaseAlt alt) $  do
574     {   -- First instantiate the universally quantified 
575         -- type variables of the data constructor
576         -- We've already check
577       checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
578     ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
579
580         -- And now bring the new binders into scope
581     ; lintBinders args $ \ args' -> do
582     { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
583     ; checkAltExpr rhs alt_ty } }
584
585   | otherwise   -- Scrut-ty is wrong shape
586   = addErrL (mkBadAltMsg scrut_ty alt)
587 \end{code}
588
589 %************************************************************************
590 %*                                                                      *
591 \subsection[lint-types]{Types}
592 %*                                                                      *
593 %************************************************************************
594
595 \begin{code}
596 -- When we lint binders, we (one at a time and in order):
597 --  1. Lint var types or kinds (possibly substituting)
598 --  2. Add the binder to the in scope set, and if its a coercion var,
599 --     we may extend the substitution to reflect its (possibly) new kind
600 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
601 lintBinders [] linterF = linterF []
602 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
603                                  lintBinders vars $ \ vars' ->
604                                  linterF (var':vars')
605
606 -- If you edit this function, you may need to update the GHC formalism
607 -- See Note [GHC Formalism]
608 lintBinder :: Var -> (Var -> LintM a) -> LintM a
609 lintBinder var linterF
610   | isId var  = lintIdBndr var linterF
611   | otherwise = lintTyBndr var linterF
612
613 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
614 lintTyBndr tv thing_inside
615   = do { subst <- getTvSubst
616        ; let (subst', tv') = Type.substTyVarBndr subst tv
617        ; lintTyBndrKind tv'
618        ; updateTvSubst subst' (thing_inside tv') }
619
620 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
621 -- Do substitution on the type of a binder and add the var with this 
622 -- new type to the in-scope set of the second argument
623 -- ToDo: lint its rules
624
625 lintIdBndr id linterF 
626   = do  { lintAndScopeId id $ \id' -> linterF id' }
627
628 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
629 lintAndScopeIds ids linterF 
630   = go ids
631   where
632     go []       = linterF []
633     go (id:ids) = lintAndScopeId id $ \id ->
634                   lintAndScopeIds ids $ \ids ->
635                   linterF (id:ids)
636
637 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
638 lintAndScopeId id linterF 
639   = do { ty <- lintInTy (idType id)
640        ; let id' = setIdType id ty
641        ; addInScopeVar id' $ (linterF id') }
642 \end{code}
643
644
645 %************************************************************************
646 %*                                                                      *
647              Types and kinds
648 %*                                                                      *
649 %************************************************************************
650
651 We have a single linter for types and kinds.  That is convenient
652 because sometimes it's not clear whether the thing we are looking
653 at is a type or a kind.
654
655 \begin{code}
656 lintInTy :: InType -> LintM LintedType
657 -- Types only, not kinds
658 -- Check the type, and apply the substitution to it
659 -- See Note [Linting type lets]
660 lintInTy ty 
661   = addLoc (InType ty) $
662     do  { ty' <- applySubstTy ty
663         ; _k  <- lintType ty'
664         ; return ty' }
665
666 -------------------
667 lintTyBndrKind :: OutTyVar -> LintM ()
668 -- Handles both type and kind foralls.
669 lintTyBndrKind tv = lintKind (tyVarKind tv)
670
671 -------------------
672 lintType :: OutType -> LintM LintedKind
673 -- The returned Kind has itself been linted
674
675 -- If you edit this function, you may need to update the GHC formalism
676 -- See Note [GHC Formalism]
677 lintType (TyVarTy tv)
678   = do { checkTyCoVarInScope tv
679        ; return (tyVarKind tv) }
680          -- We checked its kind when we added it to the envt
681
682 lintType ty@(AppTy t1 t2) 
683   = do { k1 <- lintType t1
684        ; k2 <- lintType t2
685        ; lint_ty_app ty k1 [(t2,k2)] }
686
687 lintType ty@(FunTy t1 t2)    -- (->) has two different rules, for types and kinds
688   = do { k1 <- lintType t1
689        ; k2 <- lintType t2
690        ; lintArrow (ptext (sLit "type or kind") <+> quotes (ppr ty)) k1 k2 }
691
692 lintType ty@(TyConApp tc tys)
693   | not (isUnLiftedTyCon tc) || tys `lengthIs` tyConArity tc
694        -- Check that primitive types are saturated
695        -- See Note [The kind invariant] in TypeRep
696   = do { ks <- mapM lintType tys
697        ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
698   | otherwise
699   = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
700
701 lintType (ForAllTy tv ty)
702   = do { lintTyBndrKind tv
703        ; addInScopeVar tv (lintType ty) }
704
705 lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
706
707 \end{code}
708
709
710 \begin{code}
711 lintKind :: OutKind -> LintM ()
712 -- If you edit this function, you may need to update the GHC formalism
713 -- See Note [GHC Formalism]
714 lintKind k = do { sk <- lintType k 
715                 ; unless (isSuperKind sk) 
716                          (addErrL (hang (ptext (sLit "Ill-kinded kind:") <+> ppr k)
717                                       2 (ptext (sLit "has kind:") <+> ppr sk))) }
718 \end{code}
719
720
721 \begin{code}
722 lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
723 -- If you edit this function, you may need to update the GHC formalism
724 -- See Note [GHC Formalism]
725 lintArrow what k1 k2   -- Eg lintArrow "type or kind `blah'" k1 k2
726                        -- or lintarrow "coercion `blah'" k1 k2
727   | isSuperKind k1 
728   = return superKind
729   | otherwise
730   = do { unless (okArrowArgKind k1)    (addErrL (msg (ptext (sLit "argument")) k1))
731        ; unless (okArrowResultKind k2) (addErrL (msg (ptext (sLit "result"))   k2))
732        ; return liftedTypeKind }
733   where
734     msg ar k
735       = vcat [ hang (ptext (sLit "Ill-kinded") <+> ar)
736                   2 (ptext (sLit "in") <+> what)
737              , what <+> ptext (sLit "kind:") <+> ppr k ]
738
739 lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
740 lint_ty_app ty k tys 
741   = lint_app (ptext (sLit "type") <+> quotes (ppr ty)) k tys
742
743 ----------------
744 lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
745 lint_co_app ty k tys 
746   = lint_app (ptext (sLit "coercion") <+> quotes (ppr ty)) k tys
747
748 ----------------
749 lintTyLit :: TyLit -> LintM ()
750 lintTyLit (NumTyLit n)
751   | n >= 0    = return ()
752   | otherwise = failWithL msg
753     where msg = ptext (sLit "Negative type literal:") <+> integer n
754 lintTyLit (StrTyLit _) = return ()
755
756 lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
757 -- (lint_app d fun_kind arg_tys)
758 --    We have an application (f arg_ty1 .. arg_tyn),
759 --    where f :: fun_kind
760 -- Takes care of linting the OutTypes
761
762 -- If you edit this function, you may need to update the GHC formalism
763 -- See Note [GHC Formalism]
764 lint_app doc kfn kas
765     = foldlM go_app kfn kas
766   where
767     fail_msg = vcat [ hang (ptext (sLit "Kind application error in")) 2 doc
768                     , nest 2 (ptext (sLit "Function kind =") <+> ppr kfn)
769                     , nest 2 (ptext (sLit "Arg kinds =") <+> ppr kas) ]
770
771     go_app kfn ka
772       | Just kfn' <- coreView kfn
773       = go_app kfn' ka
774
775     go_app (FunTy kfa kfb) (_,ka)
776       = do { unless (ka `isSubKind` kfa) (addErrL fail_msg)
777            ; return kfb }
778
779     go_app (ForAllTy kv kfn) (ta,ka)
780       = do { unless (ka `isSubKind` tyVarKind kv) (addErrL fail_msg)
781            ; return (substKiWith [kv] [ta] kfn) }
782
783     go_app _ _ = failWithL fail_msg
784 \end{code}
785
786 %************************************************************************
787 %*                                                                      *
788          Linting coercions
789 %*                                                                      *
790 %************************************************************************
791
792 \begin{code}
793 lintInCo :: InCoercion -> LintM OutCoercion
794 -- Check the coercion, and apply the substitution to it
795 -- See Note [Linting type lets]
796 lintInCo co
797   = addLoc (InCo co) $
798     do  { co' <- applySubstCo co
799         ; _   <- lintCoercion co'
800         ; return co' }
801
802 lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType)
803 -- Check the kind of a coercion term, returning the kind
804 -- Post-condition: the returned OutTypes are lint-free
805 --                 and have the same kind as each other
806
807 -- If you edit this function, you may need to update the GHC formalism
808 -- See Note [GHC Formalism]
809 lintCoercion (Refl ty)
810   = do { k <- lintType ty
811        ; return (k, ty, ty) }
812
813 lintCoercion co@(TyConAppCo tc cos)
814   | tc `hasKey` funTyConKey
815   , [co1,co2] <- cos
816   = do { (k1,s1,t1) <- lintCoercion co1
817        ; (k2,s2,t2) <- lintCoercion co2
818        ; rk <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k1 k2
819        ; return (rk, mkFunTy s1 s2, mkFunTy t1 t2) }
820
821   | otherwise
822   = do { (ks,ss,ts) <- mapAndUnzip3M lintCoercion cos
823        ; rk <- lint_co_app co (tyConKind tc) (ss `zip` ks)
824        ; return (rk, mkTyConApp tc ss, mkTyConApp tc ts) }
825
826 lintCoercion co@(AppCo co1 co2)
827   = do { (k1,s1,t1) <- lintCoercion co1
828        ; (k2,s2,t2) <- lintCoercion co2
829        ; rk <- lint_co_app co k1 [(s2,k2)]
830        ; return (rk, mkAppTy s1 s2, mkAppTy t1 t2) }
831
832 lintCoercion (ForAllCo tv co)
833   = do { lintTyBndrKind tv
834        ; (k, s, t) <- addInScopeVar tv (lintCoercion co)
835        ; return (k, mkForAllTy tv s, mkForAllTy tv t) }
836
837 lintCoercion (CoVarCo cv)
838   | not (isCoVar cv)
839   = failWithL (hang (ptext (sLit "Bad CoVarCo:") <+> ppr cv)
840                   2 (ptext (sLit "With offending type:") <+> ppr (varType cv)))
841   | otherwise
842   = do { checkTyCoVarInScope cv
843        ; cv' <- lookupIdInScope cv 
844        ; let (s,t) = coVarKind cv'
845              k     = typeKind s
846        ; when (isSuperKind k) $
847          checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality"))
848                                    2 (ppr cv))
849        ; return (k, s, t) }
850
851 lintCoercion (UnsafeCo ty1 ty2)
852   = do { k1 <- lintType ty1
853        ; _k2 <- lintType ty2
854 --       ; unless (k1 `eqKind` k2) $ 
855 --         failWithL (hang (ptext (sLit "Unsafe coercion changes kind"))
856 --                       2 (ppr co))
857        ; return (k1, ty1, ty2) }
858
859 lintCoercion (SymCo co) 
860   = do { (k, ty1, ty2) <- lintCoercion co
861        ; return (k, ty2, ty1) }
862
863 lintCoercion co@(TransCo co1 co2)
864   = do { (k1, ty1a, ty1b) <- lintCoercion co1
865        ; (_,  ty2a, ty2b) <- lintCoercion co2
866        ; checkL (ty1b `eqType` ty2a)
867                 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
868                     2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
869        ; return (k1, ty1a, ty2b) }
870
871 lintCoercion the_co@(NthCo n co)
872   = do { (_,s,t) <- lintCoercion co
873        ; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
874            (Just (tc_s, tys_s), Just (tc_t, tys_t)) 
875              | tc_s == tc_t
876              , tys_s `equalLength` tys_t
877              , n < length tys_s
878              -> return (ks, ts, tt)
879              where
880                ts = getNth tys_s n
881                tt = getNth tys_t n
882                ks = typeKind ts
883
884            _ -> failWithL (hang (ptext (sLit "Bad getNth:"))
885                               2 (ppr the_co $$ ppr s $$ ppr t)) }
886
887 lintCoercion the_co@(LRCo lr co)
888   = do { (_,s,t) <- lintCoercion co
889        ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
890            (Just s_pr, Just t_pr) 
891              -> return (k, s_pick, t_pick)
892              where
893                s_pick = pickLR lr s_pr
894                t_pick = pickLR lr t_pr
895                k = typeKind s_pick
896
897            _ -> failWithL (hang (ptext (sLit "Bad LRCo:"))
898                               2 (ppr the_co $$ ppr s $$ ppr t)) }
899
900 lintCoercion (InstCo co arg_ty)
901   = do { (k,s,t)  <- lintCoercion co
902        ; arg_kind <- lintType arg_ty
903        ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
904           (Just (tv1,ty1), Just (tv2,ty2))
905             | arg_kind `isSubKind` tyVarKind tv1
906             -> return (k, substTyWith [tv1] [arg_ty] ty1, 
907                           substTyWith [tv2] [arg_ty] ty2) 
908             | otherwise
909             -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
910           _ -> failWithL (ptext (sLit "Bad argument of inst")) }
911
912 lintCoercion co@(AxiomInstCo con ind cos)
913   = do { unless (0 <= ind && ind < brListLength (coAxiomBranches con))
914                 (bad_ax (ptext (sLit "index out of range")))
915          -- See Note [Kind instantiation in coercions]
916        ; let CoAxBranch { cab_tvs = ktvs
917                         , cab_lhs = lhs
918                         , cab_rhs = rhs } = coAxiomNthBranch con ind
919        ; unless (equalLength ktvs cos) (bad_ax (ptext (sLit "lengths")))
920        ; in_scope <- getInScope
921        ; let empty_subst = mkTvSubst in_scope emptyTvSubstEnv
922        ; (subst_l, subst_r) <- foldlM check_ki 
923                                       (empty_subst, empty_subst) 
924                                       (ktvs `zip` cos)
925        ; let lhs' = Type.substTys subst_l lhs
926              rhs' = Type.substTy subst_r rhs
927        ; case checkAxInstCo co of
928            Just bad_index -> bad_ax $ ptext (sLit "inconsistent with") <+> (ppr bad_index)
929            Nothing -> return ()
930        ; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs') }
931   where
932     bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what)
933                         2 (ppr co))
934
935     check_ki (subst_l, subst_r) (ktv, co)
936       = do { (k, t1, t2) <- lintCoercion co
937            ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)
938                   -- Using subst_l is ok, because subst_l and subst_r
939                   -- must agree on kind equalities
940            ; unless (k `isSubKind` ktv_kind) 
941                     (bad_ax (ptext (sLit "check_ki2") <+> vcat [ ppr co, ppr k, ppr ktv, ppr ktv_kind ] ))
942            ; return (Type.extendTvSubst subst_l ktv t1, 
943                      Type.extendTvSubst subst_r ktv t2) } 
944 \end{code}
945
946 %************************************************************************
947 %*                                                                      *
948 \subsection[lint-monad]{The Lint monad}
949 %*                                                                      *
950 %************************************************************************
951
952 \begin{code}
953
954 -- If you edit this type, you may need to update the GHC formalism
955 -- See Note [GHC Formalism]
956 newtype LintM a = 
957    LintM { unLintM :: 
958             [LintLocInfo] ->         -- Locations
959             TvSubst ->               -- Current type substitution; we also use this
960                                      -- to keep track of all the variables in scope,
961                                      -- both Ids and TyVars
962             WarnsAndErrs ->           -- Error and warning messages so far
963             (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
964
965 type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)
966
967 {-      Note [Type substitution]
968         ~~~~~~~~~~~~~~~~~~~~~~~~
969 Why do we need a type substitution?  Consider
970         /\(a:*). \(x:a). /\(a:*). id a x
971 This is ill typed, because (renaming variables) it is really
972         /\(a:*). \(x:a). /\(b:*). id b x
973 Hence, when checking an application, we can't naively compare x's type
974 (at its binding site) with its expected type (at a use site).  So we
975 rename type binders as we go, maintaining a substitution.
976
977 The same substitution also supports let-type, current expressed as
978         (/\(a:*). body) ty
979 Here we substitute 'ty' for 'a' in 'body', on the fly.
980 -}
981
982 instance Monad LintM where
983   return x = LintM (\ _   _     errs -> (Just x, errs))
984   fail err = failWithL (text err)
985   m >>= k  = LintM (\ loc subst errs -> 
986                        let (res, errs') = unLintM m loc subst errs in
987                          case res of
988                            Just r -> unLintM (k r) loc subst errs'
989                            Nothing -> (Nothing, errs'))
990
991 data LintLocInfo
992   = RhsOf Id            -- The variable bound
993   | LambdaBodyOf Id     -- The lambda-binder
994   | BodyOfLetRec [Id]   -- One of the binders
995   | CaseAlt CoreAlt     -- Case alternative
996   | CasePat CoreAlt     -- The *pattern* of the case alternative
997   | AnExpr CoreExpr     -- Some expression
998   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
999   | TopLevelBindings
1000   | InType Type         -- Inside a type
1001   | InCo   Coercion     -- Inside a coercion
1002 \end{code}
1003
1004                  
1005 \begin{code}
1006 initL :: LintM a -> WarnsAndErrs    -- Errors and warnings
1007 initL m
1008   = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
1009       (_, errs) -> errs
1010 \end{code}
1011
1012 \begin{code}
1013 checkL :: Bool -> MsgDoc -> LintM ()
1014 checkL True  _   = return ()
1015 checkL False msg = failWithL msg
1016
1017 failWithL :: MsgDoc -> LintM a
1018 failWithL msg = LintM $ \ loc subst (warns,errs) ->
1019                 (Nothing, (warns, addMsg subst errs msg loc))
1020
1021 addErrL :: MsgDoc -> LintM ()
1022 addErrL msg = LintM $ \ loc subst (warns,errs) -> 
1023               (Just (), (warns, addMsg subst errs msg loc))
1024
1025 addWarnL :: MsgDoc -> LintM ()
1026 addWarnL msg = LintM $ \ loc subst (warns,errs) -> 
1027               (Just (), (addMsg subst warns msg loc, errs))
1028
1029 addMsg :: TvSubst ->  Bag MsgDoc -> MsgDoc -> [LintLocInfo] -> Bag MsgDoc
1030 addMsg subst msgs msg locs
1031   = ASSERT( notNull locs )
1032     msgs `snocBag` mk_msg msg
1033   where
1034    (loc, cxt1) = dumpLoc (head locs)
1035    cxts        = [snd (dumpLoc loc) | loc <- locs]   
1036    context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
1037                                       ptext (sLit "Substitution:") <+> ppr subst
1038                | otherwise          = cxt1
1039  
1040    mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
1041
1042 addLoc :: LintLocInfo -> LintM a -> LintM a
1043 addLoc extra_loc m =
1044   LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
1045
1046 inCasePat :: LintM Bool         -- A slight hack; see the unique call site
1047 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
1048   where
1049     is_case_pat (CasePat {} : _) = True
1050     is_case_pat _other           = False
1051
1052 addInScopeVars :: [Var] -> LintM a -> LintM a
1053 addInScopeVars vars m
1054   = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
1055
1056 addInScopeVar :: Var -> LintM a -> LintM a
1057 addInScopeVar var m
1058   = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
1059
1060 updateTvSubst :: TvSubst -> LintM a -> LintM a
1061 updateTvSubst subst' m = 
1062   LintM (\ loc _ errs -> unLintM m loc subst' errs)
1063
1064 getTvSubst :: LintM TvSubst
1065 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
1066
1067 getInScope :: LintM InScopeSet
1068 getInScope = LintM (\ _ subst errs -> (Just (getTvInScope subst), errs))
1069
1070 applySubstTy :: InType -> LintM OutType
1071 applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
1072
1073 applySubstCo :: InCoercion -> LintM OutCoercion
1074 applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
1075
1076 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
1077 extendSubstL tv ty m
1078   = LintM (\ loc subst errs -> unLintM m loc (Type.extendTvSubst subst tv ty) errs)
1079 \end{code}
1080
1081 \begin{code}
1082 lookupIdInScope :: Id -> LintM Id
1083 lookupIdInScope id 
1084   | not (mustHaveLocalBinding id)
1085   = return id   -- An imported Id
1086   | otherwise   
1087   = do  { subst <- getTvSubst
1088         ; case lookupInScope (getTvInScope subst) id of
1089                 Just v  -> return v
1090                 Nothing -> do { addErrL out_of_scope
1091                               ; return id } }
1092   where
1093     out_of_scope = pprBndr LetBind id <+> ptext (sLit "is out of scope")
1094
1095
1096 oneTupleDataConId :: Id -- Should not happen
1097 oneTupleDataConId = dataConWorkId (tupleCon BoxedTuple 1)
1098
1099 checkBndrIdInScope :: Var -> Var -> LintM ()
1100 checkBndrIdInScope binder id 
1101   = checkInScope msg id
1102     where
1103      msg = ptext (sLit "is out of scope inside info for") <+> 
1104            ppr binder
1105
1106 checkTyCoVarInScope :: Var -> LintM ()
1107 checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
1108
1109 checkInScope :: SDoc -> Var -> LintM ()
1110 checkInScope loc_msg var =
1111  do { subst <- getTvSubst
1112     ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
1113              (hsep [pprBndr LetBind var, loc_msg]) }
1114
1115 checkTys :: OutType -> OutType -> MsgDoc -> LintM ()
1116 -- check ty2 is subtype of ty1 (ie, has same structure but usage
1117 -- annotations need only be consistent, not equal)
1118 -- Assumes ty1,ty2 are have alrady had the substitution applied
1119 checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
1120 \end{code}
1121
1122 %************************************************************************
1123 %*                                                                      *
1124 \subsection{Error messages}
1125 %*                                                                      *
1126 %************************************************************************
1127
1128 \begin{code}
1129 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
1130
1131 dumpLoc (RhsOf v)
1132   = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
1133
1134 dumpLoc (LambdaBodyOf b)
1135   = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
1136
1137 dumpLoc (BodyOfLetRec [])
1138   = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
1139
1140 dumpLoc (BodyOfLetRec bs@(_:_))
1141   = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
1142
1143 dumpLoc (AnExpr e)
1144   = (noSrcLoc, text "In the expression:" <+> ppr e)
1145
1146 dumpLoc (CaseAlt (con, args, _))
1147   = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1148
1149 dumpLoc (CasePat (con, args, _))
1150   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1151
1152 dumpLoc (ImportedUnfolding locn)
1153   = (locn, brackets (ptext (sLit "in an imported unfolding")))
1154 dumpLoc TopLevelBindings
1155   = (noSrcLoc, empty)
1156 dumpLoc (InType ty)
1157   = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1158 dumpLoc (InCo co)
1159   = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
1160
1161 pp_binders :: [Var] -> SDoc
1162 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1163
1164 pp_binder :: Var -> SDoc
1165 pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
1166             | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1167 \end{code}
1168
1169 \begin{code}
1170 ------------------------------------------------------
1171 --      Messages for case expressions
1172
1173 mkDefaultArgsMsg :: [Var] -> MsgDoc
1174 mkDefaultArgsMsg args 
1175   = hang (text "DEFAULT case with binders")
1176          4 (ppr args)
1177
1178 mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
1179 mkCaseAltMsg e ty1 ty2
1180   = hang (text "Type of case alternatives not the same as the annotation on case:")
1181          4 (vcat [ppr ty1, ppr ty2, ppr e])
1182
1183 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> MsgDoc
1184 mkScrutMsg var var_ty scrut_ty subst
1185   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1186           text "Result binder type:" <+> ppr var_ty,--(idType var),
1187           text "Scrutinee type:" <+> ppr scrut_ty,
1188      hsep [ptext (sLit "Current TV subst"), ppr subst]]
1189
1190 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
1191 mkNonDefltMsg e
1192   = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1193 mkNonIncreasingAltsMsg e
1194   = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1195
1196 nonExhaustiveAltsMsg :: CoreExpr -> MsgDoc
1197 nonExhaustiveAltsMsg e
1198   = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1199
1200 mkBadConMsg :: TyCon -> DataCon -> MsgDoc
1201 mkBadConMsg tycon datacon
1202   = vcat [
1203         text "In a case alternative, data constructor isn't in scrutinee type:",
1204         text "Scrutinee type constructor:" <+> ppr tycon,
1205         text "Data con:" <+> ppr datacon
1206     ]
1207
1208 mkBadPatMsg :: Type -> Type -> MsgDoc
1209 mkBadPatMsg con_result_ty scrut_ty
1210   = vcat [
1211         text "In a case alternative, pattern result type doesn't match scrutinee type:",
1212         text "Pattern result type:" <+> ppr con_result_ty,
1213         text "Scrutinee type:" <+> ppr scrut_ty
1214     ]
1215
1216 integerScrutinisedMsg :: MsgDoc
1217 integerScrutinisedMsg
1218   = text "In a LitAlt, the literal is lifted (probably Integer)"
1219
1220 mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
1221 mkBadAltMsg scrut_ty alt
1222   = vcat [ text "Data alternative when scrutinee is not a tycon application",
1223            text "Scrutinee type:" <+> ppr scrut_ty,
1224            text "Alternative:" <+> pprCoreAlt alt ]
1225
1226 mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc
1227 mkNewTyDataConAltMsg scrut_ty alt
1228   = vcat [ text "Data alternative for newtype datacon",
1229            text "Scrutinee type:" <+> ppr scrut_ty,
1230            text "Alternative:" <+> pprCoreAlt alt ]
1231
1232
1233 ------------------------------------------------------
1234 --      Other error messages
1235
1236 mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1237 mkAppMsg fun_ty arg_ty arg
1238   = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1239               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1240               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1241               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1242
1243 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1244 mkNonFunAppMsg fun_ty arg_ty arg
1245   = vcat [ptext (sLit "Non-function type in function position"),
1246               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1247               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1248               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1249
1250 mkLetErr :: TyVar -> CoreExpr -> MsgDoc
1251 mkLetErr bndr rhs
1252   = vcat [ptext (sLit "Bad `let' binding:"),
1253           hang (ptext (sLit "Variable:"))
1254                  4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
1255           hang (ptext (sLit "Rhs:"))   
1256                  4 (ppr rhs)]
1257
1258 mkTyAppMsg :: Type -> Type -> MsgDoc
1259 mkTyAppMsg ty arg_ty
1260   = vcat [text "Illegal type application:",
1261               hang (ptext (sLit "Exp type:"))
1262                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1263               hang (ptext (sLit "Arg type:"))   
1264                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1265
1266 mkRhsMsg :: Id -> Type -> MsgDoc
1267 mkRhsMsg binder ty
1268   = vcat
1269     [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1270             ppr binder],
1271      hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1272      hsep [ptext (sLit "Rhs type:"), ppr ty]]
1273
1274 mkRhsPrimMsg :: Id -> CoreExpr -> MsgDoc
1275 mkRhsPrimMsg binder _rhs
1276   = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1277                      ppr binder],
1278               hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1279              ]
1280
1281 mkStrictMsg :: Id -> MsgDoc
1282 mkStrictMsg binder
1283   = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1284                      ppr binder],
1285               hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1286              ]
1287
1288 mkNonTopExportedMsg :: Id -> MsgDoc
1289 mkNonTopExportedMsg binder
1290   = hsep [ptext (sLit "Non-top-level binder is marked as exported:"), ppr binder]
1291
1292 mkNonTopExternalNameMsg :: Id -> MsgDoc
1293 mkNonTopExternalNameMsg binder
1294   = hsep [ptext (sLit "Non-top-level binder has an external name:"), ppr binder]
1295
1296 mkKindErrMsg :: TyVar -> Type -> MsgDoc
1297 mkKindErrMsg tyvar arg_ty
1298   = vcat [ptext (sLit "Kinds don't match in type application:"),
1299           hang (ptext (sLit "Type variable:"))
1300                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1301           hang (ptext (sLit "Arg type:"))   
1302                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1303
1304 mkArityMsg :: Id -> MsgDoc
1305 mkArityMsg binder
1306   = vcat [hsep [ptext (sLit "Demand type has"),
1307                 ppr (dmdTypeDepth dmd_ty),
1308                 ptext (sLit "arguments, rhs has"),
1309                 ppr (idArity binder),
1310                 ptext (sLit "arguments,"),
1311                 ppr binder],
1312               hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1313
1314          ]
1315            where (StrictSig dmd_ty) = idStrictness binder
1316
1317 mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> MsgDoc
1318 mkCastErr expr co from_ty expr_ty
1319   = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1320           ptext (sLit "From-type:") <+> ppr from_ty,
1321           ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty,
1322           ptext (sLit "Actual enclosed expr:") <+> ppr expr,
1323           ptext (sLit "Coercion used in cast:") <+> ppr co
1324          ]
1325
1326 dupVars :: [[Var]] -> MsgDoc
1327 dupVars vars
1328   = hang (ptext (sLit "Duplicate variables brought into scope"))
1329        2 (ppr vars)
1330
1331 dupExtVars :: [[Name]] -> MsgDoc
1332 dupExtVars vars
1333   = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))
1334        2 (ppr vars)
1335 \end{code}