4893885e6e4453932f06bd00cf6dc32669d012d8
[ghc-hetmet.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 module CoreLint ( lintCoreBindings, lintUnfolding ) where
11
12 #include "HsVersions.h"
13
14 import Demand
15 import CoreSyn
16 import CoreFVs
17 import CoreUtils
18 import Bag
19 import Literal
20 import DataCon
21 import TysWiredIn
22 import Var
23 import VarEnv
24 import VarSet
25 import Name
26 import Id
27 import PprCore
28 import ErrUtils
29 import SrcLoc
30 import Type
31 import TypeRep
32 import Coercion
33 import TyCon
34 import Class
35 import BasicTypes
36 import StaticFlags
37 import ListSetOps
38 import PrelNames
39 import DynFlags
40 import Outputable
41 import FastString
42 import Util
43 import Control.Monad
44 import Data.Maybe
45 \end{code}
46
47 %************************************************************************
48 %*                                                                      *
49 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
50 %*                                                                      *
51 %************************************************************************
52
53 Checks that a set of core bindings is well-formed.  The PprStyle and String
54 just control what we print in the event of an error.  The Bool value
55 indicates whether we have done any specialisation yet (in which case we do
56 some extra checks).
57
58 We check for
59         (a) type errors
60         (b) Out-of-scope type variables
61         (c) Out-of-scope local variables
62         (d) Ill-kinded types
63
64 If we have done specialisation the we check that there are
65         (a) No top-level bindings of primitive (unboxed type)
66
67 Outstanding issues:
68
69     --
70     -- Things are *not* OK if:
71     --
72     --  * Unsaturated type app before specialisation has been done;
73     --
74     --  * Oversaturated type app after specialisation (eta reduction
75     --   may well be happening...);
76
77
78 Note [Linting type lets]
79 ~~~~~~~~~~~~~~~~~~~~~~~~
80 In the desugarer, it's very very convenient to be able to say (in effect)
81         let a = Type Int in <body>
82 That is, use a type let.   See Note [Type let] in CoreSyn.
83
84 However, when linting <body> we need to remember that a=Int, else we might
85 reject a correct program.  So we carry a type substitution (in this example 
86 [a -> Int]) and apply this substitution before comparing types.  The functin
87         lintInTy :: Type -> LintM Type
88 returns a substituted type; that's the only reason it returns anything.
89
90 When we encounter a binder (like x::a) we must apply the substitution
91 to the type of the binding variable.  lintBinders does this.
92
93 For Ids, the type-substituted Id is added to the in_scope set (which 
94 itself is part of the TvSubst we are carrying down), and when we
95 find an occurence of an Id, we fetch it from the in-scope set.
96
97
98 \begin{code}
99 lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
100
101 lintCoreBindings dflags _whoDunnit _binds
102   | not (dopt Opt_DoCoreLinting dflags)
103   = return ()
104
105 lintCoreBindings dflags whoDunnit binds
106   | isEmptyBag errs
107   = do { showPass dflags ("Core Linted result of " ++ whoDunnit)
108        ; unless (isEmptyBag warns || opt_NoDebugOutput) $ printDump $
109          (banner "warnings" $$ displayMessageBag warns)
110        ; return () }
111
112   | otherwise
113   = do { printDump (vcat [ banner "errors", displayMessageBag errs
114                          , ptext (sLit "*** Offending Program ***")
115                          , pprCoreBindings binds
116                          , ptext (sLit "*** End of Offense ***") ])
117
118        ; ghcExit dflags 1 }
119   where
120     (warns, errs) = initL (lint_binds binds)
121
122         -- Put all the top-level binders in scope at the start
123         -- This is because transformation rules can bring something
124         -- into use 'unexpectedly'
125     lint_binds binds = addLoc TopLevelBindings $
126                        addInScopeVars (bindersOfBinds binds) $
127                        mapM lint_bind binds 
128
129     lint_bind (Rec prs)         = mapM_ (lintSingleBinding TopLevel Recursive) prs
130     lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
131
132     banner string = ptext (sLit "*** Core Lint")      <+> text string 
133                     <+> ptext (sLit ": in result of") <+> text whoDunnit 
134                     <+> ptext (sLit "***")
135
136 displayMessageBag :: Bag Message -> SDoc
137 displayMessageBag msgs = vcat (punctuate blankLine (bagToList msgs))
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 (displayMessageBag 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 <- applySubst 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 (isNonRuleLoopBreaker (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 InType  = Type     -- Substitution not yet applied
221 type InVar   = Var
222 type InTyVar = TyVar
223
224 type OutType  = Type    -- Substitution has been applied to this
225 type OutVar   = Var
226 type OutTyVar = TyVar
227 type OutCoVar = CoVar
228
229 lintCoreExpr :: CoreExpr -> LintM OutType
230 -- The returned type has the substitution from the monad 
231 -- already applied to it:
232 --      lintCoreExpr e subst = exprType (subst e)
233 --
234 -- The returned "type" can be a kind, if the expression is (Type ty)
235
236 lintCoreExpr (Var var)
237   = do  { checkL (not (var == oneTupleDataConId))
238                  (ptext (sLit "Illegal one-tuple"))
239
240         ; checkDeadIdOcc var
241         ; var' <- lookupIdInScope var
242         ; return (idType var')
243         }
244
245 lintCoreExpr (Lit lit)
246   = return (literalType lit)
247
248 lintCoreExpr (Cast expr co)
249   = do { expr_ty <- lintCoreExpr expr
250        ; co' <- applySubst co
251        ; (from_ty, to_ty) <- lintCoercion co'
252        ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
253        ; return to_ty }
254
255 lintCoreExpr (Note _ expr)
256   = lintCoreExpr expr
257
258 lintCoreExpr (Let (NonRec tv (Type ty)) body)
259   =     -- See Note [Type let] in CoreSyn
260     do  { checkL (isTyVar tv) (mkKindErrMsg tv ty)      -- Not quite accurate
261         ; ty' <- lintInTy ty
262         ; lintTyBndr tv              $ \ tv' -> 
263           addLoc (BodyOfLetRec [tv]) $ 
264           extendSubstL tv' ty'       $ do
265         { checkKinds tv' ty'              
266                 -- Now extend the substitution so we 
267                 -- take advantage of it in the body
268         ; lintCoreExpr body } }
269
270 lintCoreExpr (Let (NonRec bndr rhs) body)
271   = do  { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
272         ; addLoc (BodyOfLetRec [bndr])
273                  (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
274
275 lintCoreExpr (Let (Rec pairs) body) 
276   = lintAndScopeIds bndrs       $ \_ ->
277     do  { mapM_ (lintSingleBinding NotTopLevel Recursive) pairs 
278         ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
279   where
280     bndrs = map fst pairs
281
282 lintCoreExpr e@(App fun arg)
283   = do  { fun_ty <- lintCoreExpr fun
284         ; addLoc (AnExpr e) $
285           lintCoreArg fun_ty arg }
286
287 lintCoreExpr (Lam var expr)
288   = addLoc (LambdaBodyOf var) $
289     lintBinders [var] $ \[var'] -> 
290     do { body_ty <- lintCoreExpr expr
291        ; if isId var' then 
292              return (mkFunTy (idType var') body_ty) 
293          else
294              return (mkForAllTy var' body_ty)
295        }
296         -- The applySubst is needed to apply the subst to var
297
298 lintCoreExpr e@(Case scrut var alt_ty alts) =
299        -- Check the scrutinee
300   do { scrut_ty <- lintCoreExpr scrut
301      ; alt_ty   <- lintInTy alt_ty  
302      ; var_ty   <- lintInTy (idType var)        
303
304      ; let mb_tc_app = splitTyConApp_maybe (idType var)
305      ; case mb_tc_app of 
306          Just (tycon, _)
307               | debugIsOn &&
308                 isAlgTyCon tycon && 
309                 not (isOpenTyCon tycon) &&
310                 null (tyConDataCons tycon) -> 
311                   pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
312                         -- This can legitimately happen for type families
313                       $ return ()
314          _otherwise -> return ()
315
316         -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
317
318      ; subst <- getTvSubst 
319      ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
320
321      -- If the binder is an unboxed tuple type, don't put it in scope
322      ; let scope = if (isUnboxedTupleType (idType var)) then 
323                        pass_var 
324                    else lintAndScopeId var
325      ; scope $ \_ ->
326        do { -- Check the alternatives
327             mapM_ (lintCoreAlt scrut_ty alt_ty) alts
328           ; checkCaseAlts e scrut_ty alts
329           ; return alt_ty } }
330   where
331     pass_var f = f var
332
333 lintCoreExpr (Type ty)
334   = do { ty' <- lintInTy ty
335        ; return (typeKind ty') }
336 \end{code}
337
338 %************************************************************************
339 %*                                                                      *
340 \subsection[lintCoreArgs]{lintCoreArgs}
341 %*                                                                      *
342 %************************************************************************
343
344 The basic version of these functions checks that the argument is a
345 subtype of the required type, as one would expect.
346
347 \begin{code}
348 lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
349 lintCoreArg  :: OutType -> CoreArg   -> LintM OutType
350 -- First argument has already had substitution applied to it
351 \end{code}
352
353 \begin{code}
354 lintCoreArgs ty [] = return ty
355 lintCoreArgs ty (a : args) = 
356   do { res <- lintCoreArg ty a
357      ; lintCoreArgs res args }
358
359 lintCoreArg fun_ty (Type arg_ty)
360   | Just (tyvar,body) <- splitForAllTy_maybe fun_ty
361   = do  { arg_ty' <- applySubst arg_ty
362         ; checkKinds tyvar arg_ty'
363         ; if isCoVar tyvar then 
364              return body   -- Co-vars don't appear in body!
365           else 
366              return (substTyWith [tyvar] [arg_ty'] body) }
367   | otherwise
368   = failWithL (mkTyAppMsg fun_ty arg_ty)
369
370 lintCoreArg fun_ty arg
371        -- Make sure function type matches argument
372  = do { arg_ty <- lintCoreExpr arg
373       ; let err1 = mkAppMsg fun_ty arg_ty arg
374             err2 = mkNonFunAppMsg fun_ty arg_ty arg
375       ; case splitFunTy_maybe fun_ty of
376           Just (arg,res) -> 
377             do { checkTys arg arg_ty err1
378                ; return res }
379           _ -> failWithL err2 }
380 \end{code}
381
382 \begin{code}
383 checkKinds :: Var -> OutType -> LintM ()
384 -- Both args have had substitution applied
385 checkKinds tyvar arg_ty
386         -- Arg type might be boxed for a function with an uncommitted
387         -- tyvar; notably this is used so that we can give
388         --      error :: forall a:*. String -> a
389         -- and then apply it to both boxed and unboxed types.
390   | isCoVar tyvar = do { (s2,t2) <- lintCoercion arg_ty
391                        ; unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
392                                 (addErrL (mkCoAppErrMsg tyvar arg_ty)) }
393   | otherwise     = do { arg_kind <- lintType arg_ty
394                        ; unless (arg_kind `isSubKind` tyvar_kind)
395                                 (addErrL (mkKindErrMsg tyvar arg_ty)) }
396   where
397     tyvar_kind = tyVarKind tyvar
398     (s1,t1)    = coVarKind tyvar
399
400 checkDeadIdOcc :: Id -> LintM ()
401 -- Occurrences of an Id should never be dead....
402 -- except when we are checking a case pattern
403 checkDeadIdOcc id
404   | isDeadOcc (idOccInfo id)
405   = do { in_case <- inCasePat
406        ; checkL in_case
407                 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
408   | otherwise
409   = return ()
410 \end{code}
411
412
413 %************************************************************************
414 %*                                                                      *
415 \subsection[lintCoreAlts]{lintCoreAlts}
416 %*                                                                      *
417 %************************************************************************
418
419 \begin{code}
420 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
421 -- a) Check that the alts are non-empty
422 -- b1) Check that the DEFAULT comes first, if it exists
423 -- b2) Check that the others are in increasing order
424 -- c) Check that there's a default for infinite types
425 -- NB: Algebraic cases are not necessarily exhaustive, because
426 --     the simplifer correctly eliminates case that can't 
427 --     possibly match.
428
429 checkCaseAlts e _ []
430   = addErrL (mkNullAltsMsg e)
431
432 checkCaseAlts e ty alts = 
433   do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
434      ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
435      ; checkL (isJust maybe_deflt || not is_infinite_ty)
436            (nonExhaustiveAltsMsg e) }
437   where
438     (con_alts, maybe_deflt) = findDefault alts
439
440         -- Check that successive alternatives have increasing tags 
441     increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
442     increasing_tag _                         = True
443
444     non_deflt (DEFAULT, _, _) = False
445     non_deflt _               = True
446
447     is_infinite_ty = case splitTyConApp_maybe ty of
448                         Nothing         -> False
449                         Just (tycon, _) -> isPrimTyCon tycon
450 \end{code}
451
452 \begin{code}
453 checkAltExpr :: CoreExpr -> OutType -> LintM ()
454 checkAltExpr expr ann_ty
455   = do { actual_ty <- lintCoreExpr expr 
456        ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
457
458 lintCoreAlt :: OutType          -- Type of scrutinee
459             -> OutType          -- Type of the alternative
460             -> CoreAlt
461             -> LintM ()
462
463 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
464   do { checkL (null args) (mkDefaultArgsMsg args)
465      ; checkAltExpr rhs alt_ty }
466
467 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) = 
468   do { checkL (null args) (mkDefaultArgsMsg args)
469      ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)   
470      ; checkAltExpr rhs alt_ty } 
471   where
472     lit_ty = literalType lit
473
474 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
475   | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
476   | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
477   = addLoc (CaseAlt alt) $  do
478     {   -- First instantiate the universally quantified 
479         -- type variables of the data constructor
480         -- We've already check
481       checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
482     ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
483
484         -- And now bring the new binders into scope
485     ; lintBinders args $ \ args -> do
486     { addLoc (CasePat alt) $ do
487           {    -- Check the pattern
488                  -- Scrutinee type must be a tycon applicn; checked by caller
489                  -- This code is remarkably compact considering what it does!
490                  -- NB: args must be in scope here so that the lintCoreArgs
491                  --     line works. 
492                  -- NB: relies on existential type args coming *after*
493                  --     ordinary type args 
494           ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
495           ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty) 
496           }
497                -- Check the RHS
498     ; checkAltExpr rhs alt_ty } }
499
500   | otherwise   -- Scrut-ty is wrong shape
501   = addErrL (mkBadAltMsg scrut_ty alt)
502 \end{code}
503
504 %************************************************************************
505 %*                                                                      *
506 \subsection[lint-types]{Types}
507 %*                                                                      *
508 %************************************************************************
509
510 \begin{code}
511 -- When we lint binders, we (one at a time and in order):
512 --  1. Lint var types or kinds (possibly substituting)
513 --  2. Add the binder to the in scope set, and if its a coercion var,
514 --     we may extend the substitution to reflect its (possibly) new kind
515 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
516 lintBinders [] linterF = linterF []
517 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
518                                  lintBinders vars $ \ vars' ->
519                                  linterF (var':vars')
520
521 lintBinder :: Var -> (Var -> LintM a) -> LintM a
522 lintBinder var linterF
523   | isId var  = lintIdBndr var linterF
524   | otherwise = lintTyBndr var linterF
525
526 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
527 lintTyBndr tv thing_inside
528   = do { subst <- getTvSubst
529        ; let (subst', tv') = substTyVarBndr subst tv
530        ; lintTyBndrKind tv'
531        ; updateTvSubst subst' (thing_inside tv') }
532
533 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
534 -- Do substitution on the type of a binder and add the var with this 
535 -- new type to the in-scope set of the second argument
536 -- ToDo: lint its rules
537
538 lintIdBndr id linterF 
539   = do  { checkL (not (isUnboxedTupleType (idType id))) 
540                  (mkUnboxedTupleMsg id)
541                 -- No variable can be bound to an unboxed tuple.
542         ; lintAndScopeId id $ \id' -> linterF id' }
543
544 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
545 lintAndScopeIds ids linterF 
546   = go ids
547   where
548     go []       = linterF []
549     go (id:ids) = lintAndScopeId id $ \id ->
550                   lintAndScopeIds ids $ \ids ->
551                   linterF (id:ids)
552
553 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
554 lintAndScopeId id linterF 
555   = do { ty <- lintInTy (idType id)
556        ; let id' = setIdType id ty
557        ; addInScopeVar id' $ (linterF id') }
558 \end{code}
559
560
561 %************************************************************************
562 %*                                                                      *
563 \subsection[lint-monad]{The Lint monad}
564 %*                                                                      *
565 %************************************************************************
566
567 \begin{code}
568 lintInTy :: InType -> LintM OutType
569 -- Check the type, and apply the substitution to it
570 -- See Note [Linting type lets]
571 -- ToDo: check the kind structure of the type
572 lintInTy ty 
573   = addLoc (InType ty) $
574     do  { ty' <- applySubst ty
575         ; _ <- lintType ty'
576         ; return ty' }
577
578 -------------------
579 lintKind :: Kind -> LintM ()
580 -- Check well-formedness of kinds: *, *->*, etc
581 lintKind (TyConApp tc []) 
582   | getUnique tc `elem` kindKeys
583   = return ()
584 lintKind (FunTy k1 k2)
585   = lintKind k1 >> lintKind k2
586 lintKind kind 
587   = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
588
589 -------------------
590 lintTyBndrKind :: OutTyVar -> LintM ()
591 lintTyBndrKind tv 
592   | isCoVar tv = lintCoVarKind tv
593   | otherwise  = lintKind (tyVarKind tv)
594
595 -------------------
596 lintCoVarKind :: OutCoVar -> LintM ()
597 -- Check the kind of a coercion binder
598 lintCoVarKind tv
599   = do { (ty1,ty2) <- lintSplitCoVar tv
600        ; k1 <- lintType ty1
601        ; k2 <- lintType ty2
602        ; unless (k1 `eqKind` k2) 
603                 (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:")
604                               , nest 2 (quotes (ppr tv))
605                               , ppr [k1,k2] ])) }
606
607 -------------------
608 lintSplitCoVar :: CoVar -> LintM (Type,Type)
609 lintSplitCoVar cv
610   = case coVarKind_maybe cv of
611       Just ts -> return ts
612       Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
613                                 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
614
615 -------------------
616 lintCoercion :: OutType -> LintM (OutType, OutType)
617 -- Check the kind of a coercion term, returning the kind
618 lintCoercion ty@(TyVarTy tv)
619   = do { checkTyVarInScope tv
620        ; if isCoVar tv then return (coVarKind tv) 
621                        else return (ty, ty) }
622
623 lintCoercion ty@(AppTy ty1 ty2) 
624   = do { (s1,t1) <- lintCoercion ty1
625        ; (s2,t2) <- lintCoercion ty2
626        ; check_co_app ty (typeKind s1) [s2]
627        ; return (AppTy s1 s2, AppTy t1 t2) }
628
629 lintCoercion ty@(FunTy ty1 ty2) 
630   = do { (s1,t1) <- lintCoercion ty1
631        ; (s2,t2) <- lintCoercion ty2
632        ; check_co_app ty (tyConKind funTyCon) [s1, s2]
633        ; return (FunTy s1 s2, FunTy t1 t2) }
634
635 lintCoercion ty@(TyConApp tc tys) 
636   | Just (ar, rule) <- isCoercionTyCon_maybe tc
637   = do { unless (tys `lengthAtLeast` ar) (badCo ty)
638        ; (s,t)   <- rule lintType lintCoercion 
639                          True (take ar tys)
640        ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
641        ; check_co_app ty (typeKind s) ss
642        ; return (mkAppTys s ss, mkAppTys t ts) }
643
644   | not (tyConHasKind tc)       -- Just something bizarre like SuperKindTyCon
645   = badCo ty
646
647   | otherwise
648   = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
649        ; check_co_app ty (tyConKind tc) ss
650        ; return (TyConApp tc ss, TyConApp tc ts) }
651
652 lintCoercion ty@(PredTy (ClassP cls tys))
653   = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
654        ; check_co_app ty (tyConKind (classTyCon cls)) ss
655        ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
656
657 lintCoercion (PredTy (IParam n p_ty))
658   = do { (s,t) <- lintCoercion p_ty
659        ; return (PredTy (IParam n s), PredTy (IParam n t)) }
660
661 lintCoercion ty@(PredTy (EqPred {}))
662   = failWithL (badEq ty)
663
664 lintCoercion (ForAllTy tv ty)
665   | isCoVar tv
666   = do { (co1, co2) <- lintSplitCoVar tv
667        ; (s1,t1)    <- lintCoercion co1
668        ; (s2,t2)    <- lintCoercion co2
669        ; (sr,tr)    <- lintCoercion ty
670        ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) }
671
672   | otherwise
673   = do { lintKind (tyVarKind tv)
674        ; (s,t) <- addInScopeVar tv (lintCoercion ty)
675        ; return (ForAllTy tv s, ForAllTy tv t) }
676
677 badCo :: Coercion -> LintM a
678 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
679
680 -------------------
681 lintType :: OutType -> LintM Kind
682 lintType (TyVarTy tv)
683   = do { checkTyVarInScope tv
684        ; return (tyVarKind tv) }
685
686 lintType ty@(AppTy t1 t2) 
687   = do { k1 <- lintType t1
688        ; lint_ty_app ty k1 [t2] }
689
690 lintType ty@(FunTy t1 t2)
691   = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
692
693 lintType ty@(TyConApp tc tys)
694   | tyConHasKind tc
695   = lint_ty_app ty (tyConKind tc) tys
696   | otherwise
697   = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
698
699 lintType (ForAllTy tv ty)
700   = do { lintTyBndrKind tv
701        ; addInScopeVar tv (lintType ty) }
702
703 lintType ty@(PredTy (ClassP cls tys))
704   = lint_ty_app ty (tyConKind (classTyCon cls)) tys
705
706 lintType (PredTy (IParam _ p_ty))
707   = lintType p_ty
708
709 lintType ty@(PredTy (EqPred {}))
710   = failWithL (badEq ty)
711
712 ----------------
713 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
714 lint_ty_app ty k tys 
715   = do { ks <- mapM lintType tys
716        ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
717                       
718 ----------------
719 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
720 check_co_app ty k tys 
721   = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))  
722                             k (map typeKind tys)
723        ; return () }
724                       
725 ----------------
726 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
727 lint_kind_app doc kfn ks = go kfn ks
728   where
729     fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
730                      nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
731                      nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
732
733     go kfn []     = return kfn
734     go kfn (k:ks) = case splitKindFunTy_maybe kfn of
735                       Nothing         -> failWithL fail_msg
736                       Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
737                                                      (addErrL fail_msg)
738                                             ; go kfb ks } 
739 --------------
740 badEq :: Type -> SDoc
741 badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
742               1 (quotes (ppr ty))
743 \end{code}
744     
745 %************************************************************************
746 %*                                                                      *
747 \subsection[lint-monad]{The Lint monad}
748 %*                                                                      *
749 %************************************************************************
750
751 \begin{code}
752 newtype LintM a = 
753    LintM { unLintM :: 
754             [LintLocInfo] ->         -- Locations
755             TvSubst ->               -- Current type substitution; we also use this
756                                      -- to keep track of all the variables in scope,
757                                      -- both Ids and TyVars
758             WarnsAndErrs ->           -- Error and warning messages so far
759             (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
760
761 type WarnsAndErrs = (Bag Message, Bag Message)
762
763 {-      Note [Type substitution]
764         ~~~~~~~~~~~~~~~~~~~~~~~~
765 Why do we need a type substitution?  Consider
766         /\(a:*). \(x:a). /\(a:*). id a x
767 This is ill typed, because (renaming variables) it is really
768         /\(a:*). \(x:a). /\(b:*). id b x
769 Hence, when checking an application, we can't naively compare x's type
770 (at its binding site) with its expected type (at a use site).  So we
771 rename type binders as we go, maintaining a substitution.
772
773 The same substitution also supports let-type, current expressed as
774         (/\(a:*). body) ty
775 Here we substitute 'ty' for 'a' in 'body', on the fly.
776 -}
777
778 instance Monad LintM where
779   return x = LintM (\ _   _     errs -> (Just x, errs))
780   fail err = failWithL (text err)
781   m >>= k  = LintM (\ loc subst errs -> 
782                        let (res, errs') = unLintM m loc subst errs in
783                          case res of
784                            Just r -> unLintM (k r) loc subst errs'
785                            Nothing -> (Nothing, errs'))
786
787 data LintLocInfo
788   = RhsOf Id            -- The variable bound
789   | LambdaBodyOf Id     -- The lambda-binder
790   | BodyOfLetRec [Id]   -- One of the binders
791   | CaseAlt CoreAlt     -- Case alternative
792   | CasePat CoreAlt     -- The *pattern* of the case alternative
793   | AnExpr CoreExpr     -- Some expression
794   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
795   | TopLevelBindings
796   | InType Type         -- Inside a type
797 \end{code}
798
799                  
800 \begin{code}
801 initL :: LintM a -> WarnsAndErrs    -- Errors and warnings
802 initL m
803   = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
804       (_, errs) -> errs
805 \end{code}
806
807 \begin{code}
808 checkL :: Bool -> Message -> LintM ()
809 checkL True  _   = return ()
810 checkL False msg = failWithL msg
811
812 failWithL :: Message -> LintM a
813 failWithL msg = LintM $ \ loc subst (warns,errs) ->
814                 (Nothing, (warns, addMsg subst errs msg loc))
815
816 addErrL :: Message -> LintM ()
817 addErrL msg = LintM $ \ loc subst (warns,errs) -> 
818               (Just (), (warns, addMsg subst errs msg loc))
819
820 addWarnL :: Message -> LintM ()
821 addWarnL msg = LintM $ \ loc subst (warns,errs) -> 
822               (Just (), (addMsg subst warns msg loc, errs))
823
824 addMsg :: TvSubst ->  Bag Message -> Message -> [LintLocInfo] -> Bag Message
825 addMsg subst msgs msg locs
826   = ASSERT( notNull locs )
827     msgs `snocBag` mk_msg msg
828   where
829    (loc, cxt1) = dumpLoc (head locs)
830    cxts        = [snd (dumpLoc loc) | loc <- locs]   
831    context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
832                                       ptext (sLit "Substitution:") <+> ppr subst
833                | otherwise          = cxt1
834  
835    mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
836
837 addLoc :: LintLocInfo -> LintM a -> LintM a
838 addLoc extra_loc m =
839   LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
840
841 inCasePat :: LintM Bool         -- A slight hack; see the unique call site
842 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
843   where
844     is_case_pat (CasePat {} : _) = True
845     is_case_pat _other           = False
846
847 addInScopeVars :: [Var] -> LintM a -> LintM a
848 addInScopeVars vars m
849   | null dups
850   = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
851   | otherwise
852   = failWithL (dupVars dups)
853   where
854     (_, dups) = removeDups compare vars 
855
856 addInScopeVar :: Var -> LintM a -> LintM a
857 addInScopeVar var m
858   = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
859
860 updateTvSubst :: TvSubst -> LintM a -> LintM a
861 updateTvSubst subst' m = 
862   LintM (\ loc _ errs -> unLintM m loc subst' errs)
863
864 getTvSubst :: LintM TvSubst
865 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
866
867 applySubst :: Type -> LintM Type
868 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
869
870 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
871 extendSubstL tv ty m
872   = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
873 \end{code}
874
875 \begin{code}
876 lookupIdInScope :: Id -> LintM Id
877 lookupIdInScope id 
878   | not (mustHaveLocalBinding id)
879   = return id   -- An imported Id
880   | otherwise   
881   = do  { subst <- getTvSubst
882         ; case lookupInScope (getTvInScope subst) id of
883                 Just v  -> return v
884                 Nothing -> do { addErrL out_of_scope
885                               ; return id } }
886   where
887     out_of_scope = ppr id <+> ptext (sLit "is out of scope")
888
889
890 oneTupleDataConId :: Id -- Should not happen
891 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
892
893 checkBndrIdInScope :: Var -> Var -> LintM ()
894 checkBndrIdInScope binder id 
895   = checkInScope msg id
896     where
897      msg = ptext (sLit "is out of scope inside info for") <+> 
898            ppr binder
899
900 checkTyVarInScope :: TyVar -> LintM ()
901 checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
902
903 checkInScope :: SDoc -> Var -> LintM ()
904 checkInScope loc_msg var =
905  do { subst <- getTvSubst
906     ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
907              (hsep [ppr var, loc_msg]) }
908
909 checkTys :: Type -> Type -> Message -> LintM ()
910 -- check ty2 is subtype of ty1 (ie, has same structure but usage
911 -- annotations need only be consistent, not equal)
912 -- Assumes ty1,ty2 are have alrady had the substitution applied
913 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
914 \end{code}
915
916 %************************************************************************
917 %*                                                                      *
918 \subsection{Error messages}
919 %*                                                                      *
920 %************************************************************************
921
922 \begin{code}
923 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
924
925 dumpLoc (RhsOf v)
926   = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
927
928 dumpLoc (LambdaBodyOf b)
929   = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
930
931 dumpLoc (BodyOfLetRec [])
932   = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
933
934 dumpLoc (BodyOfLetRec bs@(_:_))
935   = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
936
937 dumpLoc (AnExpr e)
938   = (noSrcLoc, text "In the expression:" <+> ppr e)
939
940 dumpLoc (CaseAlt (con, args, _))
941   = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
942
943 dumpLoc (CasePat (con, args, _))
944   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
945
946 dumpLoc (ImportedUnfolding locn)
947   = (locn, brackets (ptext (sLit "in an imported unfolding")))
948 dumpLoc TopLevelBindings
949   = (noSrcLoc, empty)
950 dumpLoc (InType ty)
951   = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
952
953 pp_binders :: [Var] -> SDoc
954 pp_binders bs = sep (punctuate comma (map pp_binder bs))
955
956 pp_binder :: Var -> SDoc
957 pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
958             | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
959 \end{code}
960
961 \begin{code}
962 ------------------------------------------------------
963 --      Messages for case expressions
964
965 mkNullAltsMsg :: CoreExpr -> Message
966 mkNullAltsMsg e 
967   = hang (text "Case expression with no alternatives:")
968          4 (ppr e)
969
970 mkDefaultArgsMsg :: [Var] -> Message
971 mkDefaultArgsMsg args 
972   = hang (text "DEFAULT case with binders")
973          4 (ppr args)
974
975 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
976 mkCaseAltMsg e ty1 ty2
977   = hang (text "Type of case alternatives not the same as the annotation on case:")
978          4 (vcat [ppr ty1, ppr ty2, ppr e])
979
980 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
981 mkScrutMsg var var_ty scrut_ty subst
982   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
983           text "Result binder type:" <+> ppr var_ty,--(idType var),
984           text "Scrutinee type:" <+> ppr scrut_ty,
985      hsep [ptext (sLit "Current TV subst"), ppr subst]]
986
987 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
988 mkNonDefltMsg e
989   = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
990 mkNonIncreasingAltsMsg e
991   = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
992
993 nonExhaustiveAltsMsg :: CoreExpr -> Message
994 nonExhaustiveAltsMsg e
995   = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
996
997 mkBadConMsg :: TyCon -> DataCon -> Message
998 mkBadConMsg tycon datacon
999   = vcat [
1000         text "In a case alternative, data constructor isn't in scrutinee type:",
1001         text "Scrutinee type constructor:" <+> ppr tycon,
1002         text "Data con:" <+> ppr datacon
1003     ]
1004
1005 mkBadPatMsg :: Type -> Type -> Message
1006 mkBadPatMsg con_result_ty scrut_ty
1007   = vcat [
1008         text "In a case alternative, pattern result type doesn't match scrutinee type:",
1009         text "Pattern result type:" <+> ppr con_result_ty,
1010         text "Scrutinee type:" <+> ppr scrut_ty
1011     ]
1012
1013 mkBadAltMsg :: Type -> CoreAlt -> Message
1014 mkBadAltMsg scrut_ty alt
1015   = vcat [ text "Data alternative when scrutinee is not a tycon application",
1016            text "Scrutinee type:" <+> ppr scrut_ty,
1017            text "Alternative:" <+> pprCoreAlt alt ]
1018
1019 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1020 mkNewTyDataConAltMsg scrut_ty alt
1021   = vcat [ text "Data alternative for newtype datacon",
1022            text "Scrutinee type:" <+> ppr scrut_ty,
1023            text "Alternative:" <+> pprCoreAlt alt ]
1024
1025
1026 ------------------------------------------------------
1027 --      Other error messages
1028
1029 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1030 mkAppMsg fun_ty arg_ty arg
1031   = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1032               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1033               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1034               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1035
1036 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1037 mkNonFunAppMsg fun_ty arg_ty arg
1038   = vcat [ptext (sLit "Non-function type in function position"),
1039               hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1040               hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1041               hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1042
1043 mkKindErrMsg :: TyVar -> Type -> Message
1044 mkKindErrMsg tyvar arg_ty
1045   = vcat [ptext (sLit "Kinds don't match in type application:"),
1046           hang (ptext (sLit "Type variable:"))
1047                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1048           hang (ptext (sLit "Arg type:"))   
1049                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1050
1051 mkCoAppErrMsg :: TyVar -> Type -> Message
1052 mkCoAppErrMsg tyvar arg_ty
1053   = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1054           hang (ptext (sLit "Coercion variable:"))
1055                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1056           hang (ptext (sLit "Arg coercion:"))   
1057                  4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
1058
1059 mkTyAppMsg :: Type -> Type -> Message
1060 mkTyAppMsg ty arg_ty
1061   = vcat [text "Illegal type application:",
1062               hang (ptext (sLit "Exp type:"))
1063                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1064               hang (ptext (sLit "Arg type:"))   
1065                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1066
1067 mkRhsMsg :: Id -> Type -> Message
1068 mkRhsMsg binder ty
1069   = vcat
1070     [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1071             ppr binder],
1072      hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1073      hsep [ptext (sLit "Rhs type:"), ppr ty]]
1074
1075 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1076 mkRhsPrimMsg binder _rhs
1077   = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1078                      ppr binder],
1079               hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1080              ]
1081
1082 mkStrictMsg :: Id -> Message
1083 mkStrictMsg binder
1084   = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1085                      ppr binder],
1086               hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1087              ]
1088
1089 mkArityMsg :: Id -> Message
1090 mkArityMsg binder
1091   = vcat [hsep [ptext (sLit "Demand type has "),
1092                      ppr (dmdTypeDepth dmd_ty),
1093                      ptext (sLit " arguments, rhs has "),
1094                      ppr (idArity binder),
1095                      ptext (sLit "arguments, "),
1096                      ppr binder],
1097               hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1098
1099          ]
1100            where (StrictSig dmd_ty) = idStrictness binder
1101
1102 mkUnboxedTupleMsg :: Id -> Message
1103 mkUnboxedTupleMsg binder
1104   = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1105           hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1106
1107 mkCastErr :: Type -> Type -> Message
1108 mkCastErr from_ty expr_ty
1109   = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1110           ptext (sLit "From-type:") <+> ppr from_ty,
1111           ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1112     ]
1113
1114 dupVars :: [[Var]] -> Message
1115 dupVars vars
1116   = hang (ptext (sLit "Duplicate variables brought into scope"))
1117        2 (ppr vars)
1118 \end{code}