Implememt -fdefer-type-errors (Trac #5624)
[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 MsgDoc, Bag MsgDoc)
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 MsgDoc   -- 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 lintKindCoercion :: OutCoercion -> LintM OutKind
704 -- Kind coercions are only reflexivity because they mean kind
705 -- instantiation.  See Note [Kind coercions] in Coercion
706 lintKindCoercion co
707   = do { (k1,k2) <- lintCoercion co
708        ; checkL (k1 `eqKind` k2) 
709                 (hang (ptext (sLit "Non-refl kind coercion")) 
710                     2 (ppr co))
711        ; return k1 }
712
713 lintCoercion :: OutCoercion -> LintM (OutType, OutType)
714 -- Check the kind of a coercion term, returning the kind
715 -- Post-condition: the returned OutTypes are lint-free
716 --                 and have the same kind as each other
717 lintCoercion (Refl ty)
718   = do { _ <- lintType ty
719        ; return (ty, ty) }
720
721 lintCoercion co@(TyConAppCo tc cos)
722   = do   -- We use the kind of the type constructor to know how many
723          -- kind coercions we have (one kind coercion for one kind
724          -- instantiation).
725        { let ki | tc `hasKey` funTyConKey && length cos == 2
726                   = mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind
727                   -- It's a fully applied function, so we must use the
728                   -- most permissive type for the arrow constructor
729                 | otherwise = tyConKind tc
730              (kvs, _) = splitForAllTys ki
731              (cokis, cotys) = splitAt (length kvs) cos
732          -- kis are the kind instantiations of tc
733        ; kis <- mapM lintKindCoercion cokis
734        ; (ss,ts) <- mapAndUnzipM lintCoercion cotys
735        ; check_co_app co ki (kis ++ ss)
736        ; return (mkTyConApp tc (kis ++ ss), mkTyConApp tc (kis ++ ts)) }
737
738
739 lintCoercion co@(AppCo co1 co2)
740   = do { (s1,t1) <- lintCoercion co1
741        ; (s2,t2) <- lintCoercion co2
742        ; check_co_app co (typeKind s1) [s2]
743        ; return (mkAppTy s1 s2, mkAppTy t1 t2) }
744
745 lintCoercion (ForAllCo v co)
746   = do { let kind = tyVarKind v
747          -- lintKind when type forall, otherwise we are a kind forall
748        ; unless (isSuperKind kind) (lintKind kind)
749        ; (s,t) <- addInScopeVar v (lintCoercion co)
750        ; return (ForAllTy v s, ForAllTy v t) }
751
752 lintCoercion (CoVarCo cv)
753   | not (isCoVar cv)
754   = failWithL (hang (ptext (sLit "Bad CoVarCo:") <+> ppr cv)
755                   2 (ptext (sLit "With offending type:") <+> ppr (varType cv)))
756   | otherwise
757   = do { checkTyCoVarInScope cv
758        ; cv' <- lookupIdInScope cv 
759        ; return (coVarKind cv') }
760
761 lintCoercion (AxiomInstCo (CoAxiom { co_ax_tvs = ktvs
762                                    , co_ax_lhs = lhs
763                                    , co_ax_rhs = rhs })
764                            cos)
765   = ASSERT2 (not (any isKiVar tvs), ppr ktvs)
766     do   -- see Note [Kind instantiation in coercions]
767        { kis <- checkKiCoKinds kvs kcos
768        ; let tvs' = map (updateTyVarKind (Type.substTy subst)) tvs
769              subst = zipOpenTvSubst kvs kis
770        ; (tys1, tys2) <- liftM unzip (checkTyCoKinds tvs' tcos)
771        ; return (substTyWith ktvs (kis ++ tys1) lhs,
772                  substTyWith ktvs (kis ++ tys2) rhs) }
773   where
774     (kvs, tvs) = splitKiTyVars ktvs
775     (kcos, tcos) = splitAt (length kvs) cos
776
777 lintCoercion (UnsafeCo ty1 ty2)
778   = do { _ <- lintType ty1
779        ; _ <- lintType ty2
780        ; return (ty1, ty2) }
781
782 lintCoercion (SymCo co) 
783   = do { (ty1, ty2) <- lintCoercion co
784        ; return (ty2, ty1) }
785
786 lintCoercion co@(TransCo co1 co2)
787   = do { (ty1a, ty1b) <- lintCoercion co1
788        ; (ty2a, ty2b) <- lintCoercion co2
789        ; checkL (ty1b `eqType` ty2a)
790                 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
791                     2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
792        ; return (ty1a, ty2b) }
793
794 lintCoercion the_co@(NthCo d co)
795   = do { (s,t) <- lintCoercion co
796        ; sn <- checkTcApp the_co d s
797        ; tn <- checkTcApp the_co d t
798        ; return (sn, tn) }
799
800 lintCoercion (InstCo co arg_ty)
801   = do { co_tys    <- lintCoercion co
802        ; arg_kind  <- lintType arg_ty
803        ; case splitForAllTy_maybe `traverse` toPair co_tys of
804           Just (Pair (tv1,ty1) (tv2,ty2))
805             | arg_kind `isSubKind` tyVarKind tv1
806             -> return (substTyWith [tv1] [arg_ty] ty1, 
807                        substTyWith [tv2] [arg_ty] ty2) 
808             | otherwise
809             -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
810           Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
811
812 ----------
813 checkTcApp :: OutCoercion -> Int -> Type -> LintM OutType
814 checkTcApp co n ty
815   | Just tys <- tyConAppArgs_maybe ty
816   , n < length tys
817   = return (tys !! n)
818   | otherwise
819   = failWithL (hang (ptext (sLit "Bad getNth:") <+> ppr co)
820                   2 (ptext (sLit "Offending type:") <+> ppr ty))
821
822 -------------------
823 lintType :: OutType -> LintM Kind
824 lintType (TyVarTy tv)
825   = do { checkTyCoVarInScope tv
826        ; let kind = tyVarKind tv
827        ; lintKind kind
828        ; WARN( isSuperKind kind, msg )
829          return kind }
830   where msg = hang (ptext (sLit "Expecting a type, but got a kind"))
831                  2 (ptext (sLit "Offending kind:") <+> ppr tv)
832
833 lintType ty@(AppTy t1 t2) 
834   = do { k1 <- lintType t1
835        ; lint_ty_app ty k1 [t2] }
836
837 lintType ty@(FunTy t1 t2)
838   = lint_ty_app ty (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind) [t1,t2]
839
840 lintType ty@(TyConApp tc tys)
841   | tyConHasKind tc   -- Guards for SuperKindOon
842   , not (isUnLiftedTyCon tc) || tys `lengthIs` tyConArity tc
843        -- Check that primitive types are saturated
844        -- See Note [The kind invariant] in TypeRep
845   = lint_ty_app ty (tyConKind tc) tys
846   | otherwise
847   = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
848
849 lintType (ForAllTy tv ty)
850   = do { lintTyBndrKind tv
851        ; addInScopeVar tv (lintType ty) }
852
853 ----------------
854 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
855 lint_ty_app ty k tys = lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k tys
856
857 ----------------
858 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
859 check_co_app ty k tys = lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty)) k tys >> return ()
860
861 ----------------
862 lint_kind_app :: SDoc -> Kind -> [OutType] -> LintM Kind
863 -- Takes care of linting the OutTypes
864 lint_kind_app doc kfn tys = go kfn tys
865   where
866     fail_msg = vcat [ hang (ptext (sLit "Kind application error in")) 2 doc
867                     , nest 2 (ptext (sLit "Function kind =") <+> ppr kfn)
868                     , nest 2 (ptext (sLit "Arg types =") <+> ppr tys) ]
869
870     go kfn [] = return kfn
871     go kfn (ty:tys) =
872       case splitKindFunTy_maybe kfn of
873       { Nothing ->
874           case splitForAllTy_maybe kfn of
875           { Nothing -> failWithL fail_msg
876           ; Just (kv, body) -> do
877               -- Something of kind (forall kv. body) gets instantiated
878               -- with ty. 'kv' is a kind variable and 'ty' is a kind.
879             { unless (isSuperKind (tyVarKind kv)) (addErrL fail_msg)
880             ; lintKind ty
881             ; go (substKiWith [kv] [ty] body) tys } }
882       ; Just (kfa, kfb) -> do
883           -- Something of kind (kfa -> kfb) is applied to ty. 'ty' is
884           -- a type accepting kind 'kfa'.
885         { k <- lintType ty
886         ; lintKind kfa
887         ; unless (k `isSubKind` kfa) (addErrL fail_msg)
888         ; go kfb tys } }
889
890 \end{code}
891
892 %************************************************************************
893 %*                                                                      *
894 \subsection[lint-monad]{The Lint monad}
895 %*                                                                      *
896 %************************************************************************
897
898 \begin{code}
899 newtype LintM a = 
900    LintM { unLintM :: 
901             [LintLocInfo] ->         -- Locations
902             TvSubst ->               -- Current type substitution; we also use this
903                                      -- to keep track of all the variables in scope,
904                                      -- both Ids and TyVars
905             WarnsAndErrs ->           -- Error and warning messages so far
906             (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
907
908 type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)
909
910 {-      Note [Type substitution]
911         ~~~~~~~~~~~~~~~~~~~~~~~~
912 Why do we need a type substitution?  Consider
913         /\(a:*). \(x:a). /\(a:*). id a x
914 This is ill typed, because (renaming variables) it is really
915         /\(a:*). \(x:a). /\(b:*). id b x
916 Hence, when checking an application, we can't naively compare x's type
917 (at its binding site) with its expected type (at a use site).  So we
918 rename type binders as we go, maintaining a substitution.
919
920 The same substitution also supports let-type, current expressed as
921         (/\(a:*). body) ty
922 Here we substitute 'ty' for 'a' in 'body', on the fly.
923 -}
924
925 instance Monad LintM where
926   return x = LintM (\ _   _     errs -> (Just x, errs))
927   fail err = failWithL (text err)
928   m >>= k  = LintM (\ loc subst errs -> 
929                        let (res, errs') = unLintM m loc subst errs in
930                          case res of
931                            Just r -> unLintM (k r) loc subst errs'
932                            Nothing -> (Nothing, errs'))
933
934 data LintLocInfo
935   = RhsOf Id            -- The variable bound
936   | LambdaBodyOf Id     -- The lambda-binder
937   | BodyOfLetRec [Id]   -- One of the binders
938   | CaseAlt CoreAlt     -- Case alternative
939   | CasePat CoreAlt     -- The *pattern* of the case alternative
940   | AnExpr CoreExpr     -- Some expression
941   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
942   | TopLevelBindings
943   | InType Type         -- Inside a type
944   | InCo   Coercion     -- Inside a coercion
945 \end{code}
946
947                  
948 \begin{code}
949 initL :: LintM a -> WarnsAndErrs    -- Errors and warnings
950 initL m
951   = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
952       (_, errs) -> errs
953 \end{code}
954
955 \begin{code}
956 checkL :: Bool -> MsgDoc -> LintM ()
957 checkL True  _   = return ()
958 checkL False msg = failWithL msg
959
960 failWithL :: MsgDoc -> LintM a
961 failWithL msg = LintM $ \ loc subst (warns,errs) ->
962                 (Nothing, (warns, addMsg subst errs msg loc))
963
964 addErrL :: MsgDoc -> LintM ()
965 addErrL msg = LintM $ \ loc subst (warns,errs) -> 
966               (Just (), (warns, addMsg subst errs msg loc))
967
968 addWarnL :: MsgDoc -> LintM ()
969 addWarnL msg = LintM $ \ loc subst (warns,errs) -> 
970               (Just (), (addMsg subst warns msg loc, errs))
971
972 addMsg :: TvSubst ->  Bag MsgDoc -> MsgDoc -> [LintLocInfo] -> Bag MsgDoc
973 addMsg subst msgs msg locs
974   = ASSERT( notNull locs )
975     msgs `snocBag` mk_msg msg
976   where
977    (loc, cxt1) = dumpLoc (head locs)
978    cxts        = [snd (dumpLoc loc) | loc <- locs]   
979    context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
980                                       ptext (sLit "Substitution:") <+> ppr subst
981                | otherwise          = cxt1
982  
983    mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
984
985 addLoc :: LintLocInfo -> LintM a -> LintM a
986 addLoc extra_loc m =
987   LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
988
989 inCasePat :: LintM Bool         -- A slight hack; see the unique call site
990 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
991   where
992     is_case_pat (CasePat {} : _) = True
993     is_case_pat _other           = False
994
995 addInScopeVars :: [Var] -> LintM a -> LintM a
996 addInScopeVars vars m
997   = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
998
999 addInScopeVar :: Var -> LintM a -> LintM a
1000 addInScopeVar var m
1001   = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
1002
1003 updateTvSubst :: TvSubst -> LintM a -> LintM a
1004 updateTvSubst subst' m = 
1005   LintM (\ loc _ errs -> unLintM m loc subst' errs)
1006
1007 getTvSubst :: LintM TvSubst
1008 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
1009
1010 applySubstTy :: InType -> LintM OutType
1011 applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
1012
1013 applySubstCo :: InCoercion -> LintM OutCoercion
1014 applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
1015
1016 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
1017 extendSubstL tv ty m
1018   = LintM (\ loc subst errs -> unLintM m loc (Type.extendTvSubst subst tv ty) errs)
1019 \end{code}
1020
1021 \begin{code}
1022 lookupIdInScope :: Id -> LintM Id
1023 lookupIdInScope id 
1024   | not (mustHaveLocalBinding id)
1025   = return id   -- An imported Id
1026   | otherwise   
1027   = do  { subst <- getTvSubst
1028         ; case lookupInScope (getTvInScope subst) id of
1029                 Just v  -> return v
1030                 Nothing -> do { addErrL out_of_scope
1031                               ; return id } }
1032   where
1033     out_of_scope = ppr id <+> ptext (sLit "is out of scope")
1034
1035
1036 oneTupleDataConId :: Id -- Should not happen
1037 oneTupleDataConId = dataConWorkId (tupleCon BoxedTuple 1)
1038
1039 checkBndrIdInScope :: Var -> Var -> LintM ()
1040 checkBndrIdInScope binder id 
1041   = checkInScope msg id
1042     where
1043      msg = ptext (sLit "is out of scope inside info for") <+> 
1044            ppr binder
1045
1046 checkTyCoVarInScope :: Var -> LintM ()
1047 checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
1048
1049 checkInScope :: SDoc -> Var -> LintM ()
1050 checkInScope loc_msg var =
1051  do { subst <- getTvSubst
1052     ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
1053              (hsep [ppr var, loc_msg]) }
1054
1055 checkTys :: OutType -> OutType -> MsgDoc -> LintM ()
1056 -- check ty2 is subtype of ty1 (ie, has same structure but usage
1057 -- annotations need only be consistent, not equal)
1058 -- Assumes ty1,ty2 are have alrady had the substitution applied
1059 checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
1060 \end{code}
1061
1062 %************************************************************************
1063 %*                                                                      *
1064 \subsection{Error messages}
1065 %*                                                                      *
1066 %************************************************************************
1067
1068 \begin{code}
1069 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
1070
1071 dumpLoc (RhsOf v)
1072   = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
1073
1074 dumpLoc (LambdaBodyOf b)
1075   = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
1076
1077 dumpLoc (BodyOfLetRec [])
1078   = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
1079
1080 dumpLoc (BodyOfLetRec bs@(_:_))
1081   = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
1082
1083 dumpLoc (AnExpr e)
1084   = (noSrcLoc, text "In the expression:" <+> ppr e)
1085
1086 dumpLoc (CaseAlt (con, args, _))
1087   = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1088
1089 dumpLoc (CasePat (con, args, _))
1090   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1091
1092 dumpLoc (ImportedUnfolding locn)
1093   = (locn, brackets (ptext (sLit "in an imported unfolding")))
1094 dumpLoc TopLevelBindings
1095   = (noSrcLoc, empty)
1096 dumpLoc (InType ty)
1097   = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1098 dumpLoc (InCo co)
1099   = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
1100
1101 pp_binders :: [Var] -> SDoc
1102 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1103
1104 pp_binder :: Var -> SDoc
1105 pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
1106             | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1107 \end{code}
1108
1109 \begin{code}
1110 ------------------------------------------------------
1111 --      Messages for case expressions
1112
1113 mkNullAltsMsg :: CoreExpr -> MsgDoc
1114 mkNullAltsMsg e 
1115   = hang (text "Case expression with no alternatives:")
1116          4 (ppr e)
1117
1118 mkDefaultArgsMsg :: [Var] -> MsgDoc
1119 mkDefaultArgsMsg args 
1120   = hang (text "DEFAULT case with binders")
1121          4 (ppr args)
1122
1123 mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
1124 mkCaseAltMsg e ty1 ty2
1125   = hang (text "Type of case alternatives not the same as the annotation on case:")
1126          4 (vcat [ppr ty1, ppr ty2, ppr e])
1127
1128 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> MsgDoc
1129 mkScrutMsg var var_ty scrut_ty subst
1130   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1131           text "Result binder type:" <+> ppr var_ty,--(idType var),
1132           text "Scrutinee type:" <+> ppr scrut_ty,
1133      hsep [ptext (sLit "Current TV subst"), ppr subst]]
1134
1135 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
1136 mkNonDefltMsg e
1137   = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1138 mkNonIncreasingAltsMsg e
1139   = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1140
1141 nonExhaustiveAltsMsg :: CoreExpr -> MsgDoc
1142 nonExhaustiveAltsMsg e
1143   = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1144
1145 mkBadConMsg :: TyCon -> DataCon -> MsgDoc
1146 mkBadConMsg tycon datacon
1147   = vcat [
1148         text "In a case alternative, data constructor isn't in scrutinee type:",
1149         text "Scrutinee type constructor:" <+> ppr tycon,
1150         text "Data con:" <+> ppr datacon
1151     ]
1152
1153 mkBadPatMsg :: Type -> Type -> MsgDoc
1154 mkBadPatMsg con_result_ty scrut_ty
1155   = vcat [
1156         text "In a case alternative, pattern result type doesn't match scrutinee type:",
1157         text "Pattern result type:" <+> ppr con_result_ty,
1158         text "Scrutinee type:" <+> ppr scrut_ty
1159     ]
1160
1161 integerScrutinisedMsg :: MsgDoc
1162 integerScrutinisedMsg
1163   = text "In a LitAlt, the literal is lifted (probably Integer)"
1164
1165 mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
1166 mkBadAltMsg scrut_ty alt
1167   = vcat [ text "Data alternative when scrutinee is not a tycon application",
1168            text "Scrutinee type:" <+> ppr scrut_ty,
1169            text "Alternative:" <+> pprCoreAlt alt ]
1170
1171 mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc
1172 mkNewTyDataConAltMsg scrut_ty alt
1173   = vcat [ text "Data alternative for newtype datacon",
1174            text "Scrutinee type:" <+> ppr scrut_ty,
1175            text "Alternative:" <+> pprCoreAlt alt ]
1176
1177
1178 ------------------------------------------------------
1179 --      Other error messages
1180
1181 mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1182 mkAppMsg fun_ty arg_ty arg
1183   = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1184               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1185               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1186               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1187
1188 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1189 mkNonFunAppMsg fun_ty arg_ty arg
1190   = vcat [ptext (sLit "Non-function type in function position"),
1191               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1192               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1193               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1194
1195 mkLetErr :: TyVar -> CoreExpr -> MsgDoc
1196 mkLetErr bndr rhs
1197   = vcat [ptext (sLit "Bad `let' binding:"),
1198           hang (ptext (sLit "Variable:"))
1199                  4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
1200           hang (ptext (sLit "Rhs:"))   
1201                  4 (ppr rhs)]
1202
1203 mkTyCoAppErrMsg :: TyVar -> Coercion -> MsgDoc
1204 mkTyCoAppErrMsg tyvar arg_co
1205   = vcat [ptext (sLit "Kinds don't match in lifted coercion application:"),
1206           hang (ptext (sLit "Type variable:"))
1207                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1208           hang (ptext (sLit "Arg coercion:"))   
1209                  4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))]
1210
1211 mkTyAppMsg :: Type -> Type -> MsgDoc
1212 mkTyAppMsg ty arg_ty
1213   = vcat [text "Illegal type application:",
1214               hang (ptext (sLit "Exp type:"))
1215                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1216               hang (ptext (sLit "Arg type:"))   
1217                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1218
1219 mkRhsMsg :: Id -> Type -> MsgDoc
1220 mkRhsMsg binder ty
1221   = vcat
1222     [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1223             ppr binder],
1224      hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1225      hsep [ptext (sLit "Rhs type:"), ppr ty]]
1226
1227 mkRhsPrimMsg :: Id -> CoreExpr -> MsgDoc
1228 mkRhsPrimMsg binder _rhs
1229   = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1230                      ppr binder],
1231               hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1232              ]
1233
1234 mkStrictMsg :: Id -> MsgDoc
1235 mkStrictMsg binder
1236   = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1237                      ppr binder],
1238               hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1239              ]
1240
1241
1242 mkKindErrMsg :: TyVar -> Type -> MsgDoc
1243 mkKindErrMsg tyvar arg_ty
1244   = vcat [ptext (sLit "Kinds don't match in type application:"),
1245           hang (ptext (sLit "Type variable:"))
1246                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1247           hang (ptext (sLit "Arg type:"))   
1248                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1249
1250 mkArityMsg :: Id -> MsgDoc
1251 mkArityMsg binder
1252   = vcat [hsep [ptext (sLit "Demand type has "),
1253                      ppr (dmdTypeDepth dmd_ty),
1254                      ptext (sLit " arguments, rhs has "),
1255                      ppr (idArity binder),
1256                      ptext (sLit "arguments, "),
1257                      ppr binder],
1258               hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1259
1260          ]
1261            where (StrictSig dmd_ty) = idStrictness binder
1262
1263 mkUnboxedTupleMsg :: Id -> MsgDoc
1264 mkUnboxedTupleMsg binder
1265   = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1266           hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1267
1268 mkCastErr :: Type -> Type -> MsgDoc
1269 mkCastErr from_ty expr_ty
1270   = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1271           ptext (sLit "From-type:") <+> ppr from_ty,
1272           ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1273     ]
1274
1275 dupVars :: [[Var]] -> MsgDoc
1276 dupVars vars
1277   = hang (ptext (sLit "Duplicate variables brought into scope"))
1278        2 (ppr vars)
1279
1280 dupExtVars :: [[Name]] -> MsgDoc
1281 dupExtVars vars
1282   = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))
1283        2 (ppr vars)
1284 \end{code}
1285
1286 -------------- DEAD CODE  -------------------
1287
1288 -------------------
1289 checkCoKind :: CoVar -> OutCoercion -> LintM ()
1290 -- Both args have had substitution applied
1291 checkCoKind covar arg_co
1292   = do { (s2,t2) <- lintCoercion arg_co
1293        ; unless (s1 `eqType` s2 && t1 `coreEqType` t2)
1294                 (addErrL (mkCoAppErrMsg covar arg_co)) }
1295   where
1296     (s1,t1) = coVarKind covar
1297
1298 lintCoVarKind :: OutCoVar -> LintM ()
1299 -- Check the kind of a coercion binder
1300 lintCoVarKind tv
1301   = do { (ty1,ty2) <- lintSplitCoVar tv
1302        ; lintEqType ty1 ty2
1303
1304
1305 -------------------
1306 lintSplitCoVar :: CoVar -> LintM (Type,Type)
1307 lintSplitCoVar cv
1308   = case coVarKind_maybe cv of
1309       Just ts -> return ts
1310       Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
1311                                 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
1312
1313 mkCoVarLetErr :: CoVar -> Coercion -> MsgDoc
1314 mkCoVarLetErr covar co
1315   = vcat [ptext (sLit "Bad `let' binding for coercion variable:"),
1316           hang (ptext (sLit "Coercion variable:"))
1317                  4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
1318           hang (ptext (sLit "Arg coercion:"))   
1319                  4 (ppr co)]
1320
1321 mkCoAppErrMsg :: CoVar -> Coercion -> MsgDoc
1322 mkCoAppErrMsg covar arg_co
1323   = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1324           hang (ptext (sLit "Coercion variable:"))
1325                  4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
1326           hang (ptext (sLit "Arg coercion:"))   
1327                  4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))]
1328
1329
1330 mkCoAppMsg :: Type -> Coercion -> MsgDoc
1331 mkCoAppMsg ty arg_co
1332   = vcat [text "Illegal type application:",
1333               hang (ptext (sLit "exp type:"))
1334                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1335               hang (ptext (sLit "arg type:"))   
1336                  4 (ppr arg_co <+> dcolon <+> ppr (coercionKind arg_co))]
1337