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