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