newtype fixes, coercions for non-recursive newtypes now optional
[ghc-hetmet.git] / compiler / coreSyn / CoreLint.lhs
1 %
2 % (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
3 %
4 \section[CoreLint]{A ``lint'' pass to check for Core correctness}
5
6 \begin{code}
7 module CoreLint (
8         lintCoreBindings,
9         lintUnfolding, 
10         showPass, endPass
11     ) where
12
13 #include "HsVersions.h"
14
15 import CoreSyn
16 import CoreFVs          ( idFreeVars )
17 import CoreUtils        ( findDefault, exprOkForSpeculation, coreBindsSize )
18 import Bag
19 import Literal          ( literalType )
20 import DataCon          ( dataConRepType, dataConTyCon, dataConWorkId )
21 import TysWiredIn       ( tupleCon )
22 import Var              ( Var, Id, TyVar, isCoVar, idType, tyVarKind, 
23                           mustHaveLocalBinding, setTyVarKind, setIdType  )
24 import VarEnv           ( lookupInScope )
25 import VarSet
26 import Name             ( getSrcLoc )
27 import PprCore
28 import ErrUtils         ( dumpIfSet_core, ghcExit, Message, showPass,
29                           mkLocMessage, debugTraceMsg )
30 import SrcLoc           ( SrcLoc, noSrcLoc, mkSrcSpan )
31 import Type             ( Type, tyVarsOfType, coreEqType,
32                           splitFunTy_maybe, mkTyVarTys,
33                           splitForAllTy_maybe, splitTyConApp_maybe,
34                           isUnLiftedType, typeKind, mkForAllTy, mkFunTy,
35                           isUnboxedTupleType, isSubKind,
36                           substTyWith, emptyTvSubst, extendTvInScope, 
37                           TvSubst, TvSubstEnv, mkTvSubst, setTvSubstEnv, substTy,
38                           extendTvSubst, composeTvSubst, substTyVarBndr, isInScope,
39                           getTvSubstEnv, getTvInScope, mkTyVarTy )
40 import Coercion         ( Coercion, coercionKind, coercionKindTyConApp )
41 import TyCon            ( isPrimTyCon, isNewTyCon )
42 import BasicTypes       ( RecFlag(..), Boxity(..), isNonRec )
43 import StaticFlags      ( opt_PprStyle_Debug )
44 import DynFlags         ( DynFlags, DynFlag(..), dopt )
45 import Outputable
46
47 #ifdef DEBUG
48 import Util             ( notNull )
49 #endif
50
51 import Maybe
52
53 \end{code}
54
55 %************************************************************************
56 %*                                                                      *
57 \subsection{End pass}
58 %*                                                                      *
59 %************************************************************************
60
61 @showPass@ and @endPass@ don't really belong here, but it makes a convenient
62 place for them.  They print out stuff before and after core passes,
63 and do Core Lint when necessary.
64
65 \begin{code}
66 endPass :: DynFlags -> String -> DynFlag -> [CoreBind] -> IO [CoreBind]
67 endPass dflags pass_name dump_flag binds
68   = do 
69         -- Report result size if required
70         -- This has the side effect of forcing the intermediate to be evaluated
71         debugTraceMsg dflags 2 $
72                 (text "    Result size =" <+> int (coreBindsSize binds))
73
74         -- Report verbosely, if required
75         dumpIfSet_core dflags dump_flag pass_name (pprCoreBindings binds)
76
77         -- Type check
78         lintCoreBindings dflags pass_name binds
79
80         return binds
81 \end{code}
82
83
84 %************************************************************************
85 %*                                                                      *
86 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
87 %*                                                                      *
88 %************************************************************************
89
90 Checks that a set of core bindings is well-formed.  The PprStyle and String
91 just control what we print in the event of an error.  The Bool value
92 indicates whether we have done any specialisation yet (in which case we do
93 some extra checks).
94
95 We check for
96         (a) type errors
97         (b) Out-of-scope type variables
98         (c) Out-of-scope local variables
99         (d) Ill-kinded types
100
101 If we have done specialisation the we check that there are
102         (a) No top-level bindings of primitive (unboxed type)
103
104 Outstanding issues:
105
106     --
107     -- Things are *not* OK if:
108     --
109     --  * Unsaturated type app before specialisation has been done;
110     --
111     --  * Oversaturated type app after specialisation (eta reduction
112     --   may well be happening...);
113
114
115 Note [Type lets]
116 ~~~~~~~~~~~~~~~~
117 In the desugarer, it's very very convenient to be able to say (in effect)
118         let a = Int in <body>
119 That is, use a type let.  (See notes just below for why we want this.)
120
121 We don't have type lets in Core, so the desugarer uses type lambda
122         (/\a. <body>) Int
123 However, in the lambda form, we'd get lint errors from:
124         (/\a. let x::a = 4 in <body>) Int
125 because (x::a) doesn't look compatible with (4::Int).
126
127 So (HACK ALERT) the Lint phase does type-beta reduction "on the fly",
128 as it were.  It carries a type substitution (in this example [a -> Int])
129 and applies this substitution before comparing types.  The functin
130         lintTy :: Type -> LintM Type
131 returns a substituted type; that's the only reason it returns anything.
132
133 When we encounter a binder (like x::a) we must apply the substitution
134 to the type of the binding variable.  lintBinders does this.
135
136 For Ids, the type-substituted Id is added to the in_scope set (which 
137 itself is part of the TvSubst we are carrying down), and when we
138 find an occurence of an Id, we fetch it from the in-scope set.
139
140
141 Why we need type let
142 ~~~~~~~~~~~~~~~~~~~~
143 It's needed when dealing with desugarer output for GADTs. Consider
144   data T = forall a. T a (a->Int) Bool
145    f :: T -> ... -> 
146    f (T x f True)  = <e1>
147    f (T y g False) = <e2>
148 After desugaring we get
149         f t b = case t of 
150                   T a (x::a) (f::a->Int) (b:Bool) ->
151                     case b of 
152                         True -> <e1>
153                         False -> (/\b. let y=x; g=f in <e2>) a
154 And for a reason I now forget, the ...<e2>... can mention a; so 
155 we want Lint to know that b=a.  Ugh.
156
157 I tried quite hard to make the necessity for this go away, by changing the 
158 desugarer, but the fundamental problem is this:
159         
160         T a (x::a) (y::Int) -> let fail::a = ...
161                                in (/\b. ...(case ... of       
162                                                 True  -> x::b
163                                                 False -> fail)
164                                   ) a
165 Now the inner case look as though it has incompatible branches.
166
167
168 \begin{code}
169 lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
170
171 lintCoreBindings dflags whoDunnit binds
172   | not (dopt Opt_DoCoreLinting dflags)
173   = return ()
174
175 lintCoreBindings dflags whoDunnit binds
176   = case (initL (lint_binds binds)) of
177       Nothing       -> showPass dflags ("Core Linted result of " ++ whoDunnit)
178       Just bad_news -> printDump (display bad_news)     >>
179                        ghcExit dflags 1
180   where
181         -- Put all the top-level binders in scope at the start
182         -- This is because transformation rules can bring something
183         -- into use 'unexpectedly'
184     lint_binds binds = addInScopeVars (bindersOfBinds binds) $
185                        mapM lint_bind binds 
186
187     lint_bind (Rec prs)         = mapM_ (lintSingleBinding Recursive) prs
188     lint_bind (NonRec bndr rhs) = lintSingleBinding NonRecursive (bndr,rhs)
189
190     display bad_news
191       = vcat [  text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
192                 bad_news,
193                 ptext SLIT("*** Offending Program ***"),
194                 pprCoreBindings binds,
195                 ptext SLIT("*** End of Offense ***")
196         ]
197 \end{code}
198
199 %************************************************************************
200 %*                                                                      *
201 \subsection[lintUnfolding]{lintUnfolding}
202 %*                                                                      *
203 %************************************************************************
204
205 We use this to check all unfoldings that come in from interfaces
206 (it is very painful to catch errors otherwise):
207
208 \begin{code}
209 lintUnfolding :: SrcLoc
210               -> [Var]          -- Treat these as in scope
211               -> CoreExpr
212               -> Maybe Message  -- Nothing => OK
213
214 lintUnfolding locn vars expr
215   = initL (addLoc (ImportedUnfolding locn) $
216            addInScopeVars vars             $
217            lintCoreExpr expr)
218 \end{code}
219
220 %************************************************************************
221 %*                                                                      *
222 \subsection[lintCoreBinding]{lintCoreBinding}
223 %*                                                                      *
224 %************************************************************************
225
226 Check a core binding, returning the list of variables bound.
227
228 \begin{code}
229 lintSingleBinding rec_flag (binder,rhs)
230   = addLoc (RhsOf binder) $
231          -- Check the rhs 
232     do { ty <- lintCoreExpr rhs 
233        ; lintBinder binder -- Check match to RHS type
234        ; binder_ty <- applySubst binder_ty
235        ; checkTys binder_ty ty (mkRhsMsg binder ty)
236         -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
237        ; checkL (not (isUnLiftedType binder_ty)
238             || (isNonRec rec_flag && exprOkForSpeculation rhs))
239            (mkRhsPrimMsg binder rhs)
240         -- Check whether binder's specialisations contain any out-of-scope variables
241        ; mapM_ (checkBndrIdInScope binder) bndr_vars }
242           
243         -- We should check the unfolding, if any, but this is tricky because
244         -- the unfolding is a SimplifiableCoreExpr. Give up for now.
245   where
246     binder_ty = idType binder
247     bndr_vars = varSetElems (idFreeVars binder)
248     lintBinder var | isId var  = lintIdBndr var $ \_ -> (return ())
249                    | otherwise = return ()
250 \end{code}
251
252 %************************************************************************
253 %*                                                                      *
254 \subsection[lintCoreExpr]{lintCoreExpr}
255 %*                                                                      *
256 %************************************************************************
257
258 \begin{code}
259 type InType  = Type     -- Substitution not yet applied
260 type OutType = Type     -- Substitution has been applied to this
261
262 lintCoreExpr :: CoreExpr -> LintM OutType
263 -- The returned type has the substitution from the monad 
264 -- already applied to it:
265 --      lintCoreExpr e subst = exprType (subst e)
266
267 lintCoreExpr (Var var)
268   = do  { checkL (not (var == oneTupleDataConId))
269                  (ptext SLIT("Illegal one-tuple"))
270         ; var' <- lookupIdInScope var
271         ; return (idType var')
272         }
273
274 lintCoreExpr (Lit lit)
275   = return (literalType lit)
276
277 --lintCoreExpr (Note (Coerce to_ty from_ty) expr)
278 --  = do        { expr_ty <- lintCoreExpr expr
279 --      ; to_ty <- lintTy to_ty
280 --      ; from_ty <- lintTy from_ty     
281 --      ; checkTys from_ty expr_ty (mkCoerceErr from_ty expr_ty)
282 --      ; return to_ty }
283
284 lintCoreExpr (Cast expr co)
285   = do { expr_ty <- lintCoreExpr expr
286        ; co' <- lintTy co
287        ; let (from_ty, to_ty) = coercionKind co'
288        ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
289        ; return to_ty }
290
291 lintCoreExpr (Note other_note expr)
292   = lintCoreExpr expr
293
294 lintCoreExpr (Let (NonRec bndr rhs) body)
295   = do  { lintSingleBinding NonRecursive (bndr,rhs)
296         ; addLoc (BodyOfLetRec [bndr])
297                  (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
298
299 lintCoreExpr (Let (Rec pairs) body) 
300   = lintAndScopeIds bndrs       $ \_ ->
301     do  { mapM (lintSingleBinding Recursive) pairs      
302         ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
303   where
304     bndrs = map fst pairs
305
306 lintCoreExpr e@(App fun (Type ty))
307 -- See Note [Type let] above
308   = addLoc (AnExpr e) $
309     go fun [ty]
310   where
311     go (App fun (Type ty)) tys
312         = do { go fun (ty:tys) }
313     go (Lam tv body) (ty:tys)
314         = do  { checkL (isTyVar tv) (mkKindErrMsg tv ty)        -- Not quite accurate
315               ; ty' <- lintTy ty 
316               ; let kind = tyVarKind tv
317               ; kind' <- lintTy kind
318               ; let tv' = setTyVarKind tv kind'
319               ; checkKinds tv' ty'              
320                 -- Now extend the substitution so we 
321                 -- take advantage of it in the body
322               ; addInScopeVars [tv'] $
323                 extendSubstL tv' ty' $
324                 go body tys }
325     go fun tys
326         = do  { fun_ty <- lintCoreExpr fun
327               ; lintCoreArgs fun_ty (map Type tys) }
328
329 lintCoreExpr e@(App fun arg)
330   = do  { fun_ty <- lintCoreExpr fun
331         ; addLoc (AnExpr e) $
332           lintCoreArg fun_ty arg }
333
334 lintCoreExpr (Lam var expr)
335   = addLoc (LambdaBodyOf var) $
336     lintBinders [var] $ \[var'] -> 
337     do { body_ty <- lintCoreExpr expr
338        ; if isId var' then 
339              return (mkFunTy (idType var') body_ty) 
340          else
341              return (mkForAllTy var' body_ty)
342        }
343         -- The applySubst is needed to apply the subst to var
344
345 lintCoreExpr e@(Case scrut var alt_ty alts) =
346        -- Check the scrutinee
347   do { scrut_ty <- lintCoreExpr scrut
348      ; alt_ty   <- lintTy alt_ty  
349      ; var_ty   <- lintTy (idType var)  
350         -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
351
352      ; subst <- getTvSubst 
353      ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
354
355      -- If the binder is an unboxed tuple type, don't put it in scope
356      ; let scope = if (isUnboxedTupleType (idType var)) then 
357                        pass_var 
358                    else lintAndScopeId var
359      ; scope $ \_ ->
360        do { -- Check the alternatives
361             checkCaseAlts e scrut_ty alts
362           ; mapM (lintCoreAlt scrut_ty alt_ty) alts
363           ; return alt_ty } }
364   where
365     pass_var f = f var
366
367 lintCoreExpr e@(Type ty)
368   = addErrL (mkStrangeTyMsg e)
369 \end{code}
370
371 %************************************************************************
372 %*                                                                      *
373 \subsection[lintCoreArgs]{lintCoreArgs}
374 %*                                                                      *
375 %************************************************************************
376
377 The basic version of these functions checks that the argument is a
378 subtype of the required type, as one would expect.
379
380 \begin{code}
381 lintCoreArgs :: Type -> [CoreArg] -> LintM Type
382 lintCoreArg  :: Type -> CoreArg   -> LintM Type
383 -- First argument has already had substitution applied to it
384 \end{code}
385
386 \begin{code}
387 lintCoreArgs ty [] = return ty
388 lintCoreArgs ty (a : args) = 
389   do { res <- lintCoreArg ty a
390      ; lintCoreArgs res args }
391
392 lintCoreArg fun_ty a@(Type arg_ty) = 
393   do { arg_ty <- lintTy arg_ty  
394      ; lintTyApp fun_ty arg_ty }
395
396 lintCoreArg fun_ty arg = 
397        -- Make sure function type matches argument
398   do { arg_ty <- lintCoreExpr arg
399      ; let err = mkAppMsg fun_ty arg_ty arg
400      ; case splitFunTy_maybe fun_ty of
401         Just (arg,res) -> 
402           do { checkTys arg arg_ty err 
403              ; return res }
404         _ -> addErrL err }
405 \end{code}
406
407 \begin{code}
408 -- Both args have had substitution applied
409 lintTyApp ty arg_ty 
410   = case splitForAllTy_maybe ty of
411       Nothing -> addErrL (mkTyAppMsg ty arg_ty)
412
413       Just (tyvar,body)
414         -> do   { checkL (isTyVar tyvar) (mkTyAppMsg ty arg_ty)
415                 ; checkKinds tyvar arg_ty
416                 ; return (substTyWith [tyvar] [arg_ty] body) }
417
418 lintTyApps fun_ty [] = return fun_ty
419
420 lintTyApps fun_ty (arg_ty : arg_tys) = 
421   do { fun_ty' <- lintTyApp fun_ty arg_ty
422      ; lintTyApps fun_ty' arg_tys }
423
424 checkKinds tyvar arg_ty
425         -- Arg type might be boxed for a function with an uncommitted
426         -- tyvar; notably this is used so that we can give
427         --      error :: forall a:*. String -> a
428         -- and then apply it to both boxed and unboxed types.
429   = checkL (arg_kind `isSubKind` tyvar_kind)
430            (mkKindErrMsg tyvar arg_ty)
431   where
432     tyvar_kind = tyVarKind tyvar
433     arg_kind | isCoVar tyvar = coercionKindTyConApp arg_ty
434              | otherwise     = typeKind arg_ty
435 \end{code}
436
437
438 %************************************************************************
439 %*                                                                      *
440 \subsection[lintCoreAlts]{lintCoreAlts}
441 %*                                                                      *
442 %************************************************************************
443
444 \begin{code}
445 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
446 -- a) Check that the alts are non-empty
447 -- b1) Check that the DEFAULT comes first, if it exists
448 -- b2) Check that the others are in increasing order
449 -- c) Check that there's a default for infinite types
450 -- NB: Algebraic cases are not necessarily exhaustive, because
451 --     the simplifer correctly eliminates case that can't 
452 --     possibly match.
453
454 checkCaseAlts e ty [] 
455   = addErrL (mkNullAltsMsg e)
456
457 checkCaseAlts e ty alts = 
458   do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
459      ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
460      ; checkL (isJust maybe_deflt || not is_infinite_ty)
461            (nonExhaustiveAltsMsg e) }
462   where
463     (con_alts, maybe_deflt) = findDefault alts
464
465         -- Check that successive alternatives have increasing tags 
466     increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
467     increasing_tag other                     = True
468
469     non_deflt (DEFAULT, _, _) = False
470     non_deflt alt             = True
471
472     is_infinite_ty = case splitTyConApp_maybe ty of
473                         Nothing                     -> False
474                         Just (tycon, tycon_arg_tys) -> isPrimTyCon tycon
475 \end{code}
476
477 \begin{code}
478 checkAltExpr :: CoreExpr -> OutType -> LintM ()
479 checkAltExpr expr ann_ty
480   = do { actual_ty <- lintCoreExpr expr 
481        ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
482
483 lintCoreAlt :: OutType          -- Type of scrutinee
484             -> OutType          -- Type of the alternative
485             -> CoreAlt
486             -> LintM ()
487
488 lintCoreAlt scrut_ty alt_ty alt@(DEFAULT, args, rhs) = 
489   do { checkL (null args) (mkDefaultArgsMsg args)
490      ; checkAltExpr rhs alt_ty }
491
492 lintCoreAlt scrut_ty alt_ty alt@(LitAlt lit, args, rhs) = 
493   do { checkL (null args) (mkDefaultArgsMsg args)
494      ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)   
495      ; checkAltExpr rhs alt_ty } 
496   where
497     lit_ty = literalType lit
498
499 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
500   | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
501   | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
502   = addLoc (CaseAlt alt) $  lintBinders args $ \ args -> 
503     
504       do        { addLoc (CasePat alt) $ do
505             {    -- Check the pattern
506                  -- Scrutinee type must be a tycon applicn; checked by caller
507                  -- This code is remarkably compact considering what it does!
508                  -- NB: args must be in scope here so that the lintCoreArgs line works.
509                  -- NB: relies on existential type args coming *after* ordinary type args
510
511           ; con_result_ty <-  
512                                lintCoreArgs (dataConRepType con)
513                                                 (map Type tycon_arg_tys ++ varsToCoreExprs args)
514           ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty) 
515           }
516                -- Check the RHS
517         ; checkAltExpr rhs alt_ty }
518
519   | otherwise   -- Scrut-ty is wrong shape
520   = addErrL (mkBadAltMsg scrut_ty alt)
521 \end{code}
522
523 %************************************************************************
524 %*                                                                      *
525 \subsection[lint-types]{Types}
526 %*                                                                      *
527 %************************************************************************
528
529 \begin{code}
530 -- When we lint binders, we (one at a time and in order):
531 --  1. Lint var types or kinds (possibly substituting)
532 --  2. Add the binder to the in scope set, and if its a coercion var,
533 --     we may extend the substitution to reflect its (possibly) new kind
534 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
535 lintBinders [] linterF = linterF []
536 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
537                                  lintBinders vars $ \ vars' ->
538                                  linterF (var':vars')
539
540 lintBinder :: Var -> (Var -> LintM a) -> LintM a
541 lintBinder var linterF
542   | isTyVar var = lint_ty_bndr
543   | otherwise   = lintIdBndr var linterF
544   where
545     lint_ty_bndr = do { lintTy (tyVarKind var)
546                       ; subst <- getTvSubst
547                       ; let (subst', tv') = substTyVarBndr subst var
548                       ; updateTvSubst subst' (linterF tv') }
549
550 lintIdBndr :: Var -> (Var -> LintM a) -> LintM a
551 -- Do substitution on the type of a binder and add the var with this 
552 -- new type to the in-scope set of the second argument
553 -- ToDo: lint its rules
554 lintIdBndr id linterF 
555   = do  { checkL (not (isUnboxedTupleType (idType id))) 
556                  (mkUnboxedTupleMsg id)
557                 -- No variable can be bound to an unboxed tuple.
558         ; lintAndScopeId id $ \id' -> linterF id'
559         }
560
561 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
562 lintAndScopeIds ids linterF 
563   = go ids
564   where
565     go []       = linterF []
566     go (id:ids) = do { lintAndScopeId id $ \id ->
567                            lintAndScopeIds ids $ \ids ->
568                            linterF (id:ids) }
569
570 lintAndScopeId :: Var -> (Var -> LintM a) -> LintM a
571 lintAndScopeId id linterF 
572   = do { ty <- lintTy (idType id)
573        ; let id' = setIdType id ty
574        ; addInScopeVars [id'] $ (linterF id')
575        }
576
577 lintTy :: InType -> LintM OutType
578 -- Check the type, and apply the substitution to it
579 -- ToDo: check the kind structure of the type
580 lintTy ty 
581   = do  { ty' <- applySubst ty
582         ; mapM_ checkTyVarInScope (varSetElems (tyVarsOfType ty'))
583         ; return ty' }
584 \end{code}
585
586     
587 %************************************************************************
588 %*                                                                      *
589 \subsection[lint-monad]{The Lint monad}
590 %*                                                                      *
591 %************************************************************************
592
593 \begin{code}
594 newtype LintM a = 
595    LintM { unLintM :: 
596             [LintLocInfo] ->         -- Locations
597             TvSubst ->               -- Current type substitution; we also use this
598                                      -- to keep track of all the variables in scope,
599                                      -- both Ids and TyVars
600             Bag Message ->           -- Error messages so far
601             (Maybe a, Bag Message) } -- Result and error messages (if any)
602
603 instance Monad LintM where
604   return x = LintM (\ loc subst errs -> (Just x, errs))
605   fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
606   m >>= k  = LintM (\ loc subst errs -> 
607                        let (res, errs') = unLintM m loc subst errs in
608                          case res of
609                            Just r -> unLintM (k r) loc subst errs'
610                            Nothing -> (Nothing, errs'))
611
612 data LintLocInfo
613   = RhsOf Id            -- The variable bound
614   | LambdaBodyOf Id     -- The lambda-binder
615   | BodyOfLetRec [Id]   -- One of the binders
616   | CaseAlt CoreAlt     -- Case alternative
617   | CasePat CoreAlt     -- *Pattern* of the case alternative
618   | AnExpr CoreExpr     -- Some expression
619   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
620 \end{code}
621
622                  
623 \begin{code}
624 initL :: LintM a -> Maybe Message {- errors -}
625 initL m
626   = case unLintM m [] emptyTvSubst emptyBag of
627       (_, errs) | isEmptyBag errs -> Nothing
628                 | otherwise       -> Just (vcat (punctuate (text "") (bagToList errs)))
629 \end{code}
630
631 \begin{code}
632 checkL :: Bool -> Message -> LintM ()
633 checkL True  msg = return ()
634 checkL False msg = addErrL msg
635
636 addErrL :: Message -> LintM a
637 addErrL msg = LintM (\ loc subst errs -> (Nothing, addErr subst errs msg loc))
638
639 addErr :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
640 addErr subst errs_so_far msg locs
641   = ASSERT( notNull locs )
642     errs_so_far `snocBag` mk_msg msg
643   where
644    (loc, cxt1) = dumpLoc (head locs)
645    cxts        = [snd (dumpLoc loc) | loc <- locs]   
646    context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
647                                       ptext SLIT("Substitution:") <+> ppr subst
648                | otherwise          = cxt1
649  
650    mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
651
652 addLoc :: LintLocInfo -> LintM a -> LintM a
653 addLoc extra_loc m =
654   LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
655
656 addInScopeVars :: [Var] -> LintM a -> LintM a
657 addInScopeVars vars m = 
658   LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst vars) errs)
659
660 updateTvSubst :: TvSubst -> LintM a -> LintM a
661 updateTvSubst subst' m = 
662   LintM (\ loc subst errs -> unLintM m loc subst' errs)
663
664 getTvSubst :: LintM TvSubst
665 getTvSubst = LintM (\ loc subst errs -> (Just subst, errs))
666
667 applySubst :: Type -> LintM Type
668 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
669
670 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
671 extendSubstL tv ty m
672   = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
673 \end{code}
674
675 \begin{code}
676 lookupIdInScope :: Id -> LintM Id
677 lookupIdInScope id 
678   | not (mustHaveLocalBinding id)
679   = return id   -- An imported Id
680   | otherwise   
681   = do  { subst <- getTvSubst
682         ; case lookupInScope (getTvInScope subst) id of
683                 Just v  -> return v
684                 Nothing -> do { addErrL out_of_scope
685                               ; return id } }
686   where
687     out_of_scope = ppr id <+> ptext SLIT("is out of scope")
688
689
690 oneTupleDataConId :: Id -- Should not happen
691 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
692
693 checkBndrIdInScope :: Var -> Var -> LintM ()
694 checkBndrIdInScope binder id 
695   = checkInScope msg id
696     where
697      msg = ptext SLIT("is out of scope inside info for") <+> 
698            ppr binder
699
700 checkTyVarInScope :: TyVar -> LintM ()
701 checkTyVarInScope tv = checkInScope (ptext SLIT("is out of scope")) tv
702
703 checkInScope :: SDoc -> Var -> LintM ()
704 checkInScope loc_msg var =
705  do { subst <- getTvSubst
706     ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
707              (hsep [ppr var, loc_msg]) }
708
709 checkTys :: Type -> Type -> Message -> LintM ()
710 -- check ty2 is subtype of ty1 (ie, has same structure but usage
711 -- annotations need only be consistent, not equal)
712 -- Assumes ty1,ty2 are have alrady had the substitution applied
713 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
714 \end{code}
715
716 %************************************************************************
717 %*                                                                      *
718 \subsection{Error messages}
719 %*                                                                      *
720 %************************************************************************
721
722 \begin{code}
723 dumpLoc (RhsOf v)
724   = (getSrcLoc v, brackets (ptext SLIT("RHS of") <+> pp_binders [v]))
725
726 dumpLoc (LambdaBodyOf b)
727   = (getSrcLoc b, brackets (ptext SLIT("in body of lambda with binder") <+> pp_binder b))
728
729 dumpLoc (BodyOfLetRec [])
730   = (noSrcLoc, brackets (ptext SLIT("In body of a letrec with no binders")))
731
732 dumpLoc (BodyOfLetRec bs@(_:_))
733   = ( getSrcLoc (head bs), brackets (ptext SLIT("in body of letrec with binders") <+> pp_binders bs))
734
735 dumpLoc (AnExpr e)
736   = (noSrcLoc, text "In the expression:" <+> ppr e)
737
738 dumpLoc (CaseAlt (con, args, rhs))
739   = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
740
741 dumpLoc (CasePat (con, args, rhs))
742   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
743
744 dumpLoc (ImportedUnfolding locn)
745   = (locn, brackets (ptext SLIT("in an imported unfolding")))
746
747 pp_binders :: [Var] -> SDoc
748 pp_binders bs = sep (punctuate comma (map pp_binder bs))
749
750 pp_binder :: Var -> SDoc
751 pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
752             | isTyVar b = hsep [ppr b, dcolon, ppr (tyVarKind b)]
753 \end{code}
754
755 \begin{code}
756 ------------------------------------------------------
757 --      Messages for case expressions
758
759 mkNullAltsMsg :: CoreExpr -> Message
760 mkNullAltsMsg e 
761   = hang (text "Case expression with no alternatives:")
762          4 (ppr e)
763
764 mkDefaultArgsMsg :: [Var] -> Message
765 mkDefaultArgsMsg args 
766   = hang (text "DEFAULT case with binders")
767          4 (ppr args)
768
769 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
770 mkCaseAltMsg e ty1 ty2
771   = hang (text "Type of case alternatives not the same as the annotation on case:")
772          4 (vcat [ppr ty1, ppr ty2, ppr e])
773
774 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
775 mkScrutMsg var var_ty scrut_ty subst
776   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
777           text "Result binder type:" <+> ppr var_ty,--(idType var),
778           text "Scrutinee type:" <+> ppr scrut_ty,
779      hsep [ptext SLIT("Current TV subst"), ppr subst]]
780
781
782 mkNonDefltMsg e
783   = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
784 mkNonIncreasingAltsMsg e
785   = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
786
787 nonExhaustiveAltsMsg :: CoreExpr -> Message
788 nonExhaustiveAltsMsg e
789   = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
790
791 mkBadPatMsg :: Type -> Type -> Message
792 mkBadPatMsg con_result_ty scrut_ty
793   = vcat [
794         text "In a case alternative, pattern result type doesn't match scrutinee type:",
795         text "Pattern result type:" <+> ppr con_result_ty,
796         text "Scrutinee type:" <+> ppr scrut_ty
797     ]
798
799 mkBadAltMsg :: Type -> CoreAlt -> Message
800 mkBadAltMsg scrut_ty alt
801   = vcat [ text "Data alternative when scrutinee is not a tycon application",
802            text "Scrutinee type:" <+> ppr scrut_ty,
803            text "Alternative:" <+> pprCoreAlt alt ]
804
805 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
806 mkNewTyDataConAltMsg scrut_ty alt
807   = vcat [ text "Data alternative for newtype datacon",
808            text "Scrutinee type:" <+> ppr scrut_ty,
809            text "Alternative:" <+> pprCoreAlt alt ]
810
811
812 ------------------------------------------------------
813 --      Other error messages
814
815 mkAppMsg :: Type -> Type -> CoreExpr -> Message
816 mkAppMsg fun_ty arg_ty arg
817   = vcat [ptext SLIT("Argument value doesn't match argument type:"),
818               hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
819               hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
820               hang (ptext SLIT("Arg:")) 4 (ppr arg)]
821
822 mkKindErrMsg :: TyVar -> Type -> Message
823 mkKindErrMsg tyvar arg_ty
824   = vcat [ptext SLIT("Kinds don't match in type application:"),
825           hang (ptext SLIT("Type variable:"))
826                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
827           hang (ptext SLIT("Arg type:"))   
828                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
829
830 mkTyAppMsg :: Type -> Type -> Message
831 mkTyAppMsg ty arg_ty
832   = vcat [text "Illegal type application:",
833               hang (ptext SLIT("Exp type:"))
834                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
835               hang (ptext SLIT("Arg type:"))   
836                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
837
838 mkRhsMsg :: Id -> Type -> Message
839 mkRhsMsg binder ty
840   = vcat
841     [hsep [ptext SLIT("The type of this binder doesn't match the type of its RHS:"),
842             ppr binder],
843      hsep [ptext SLIT("Binder's type:"), ppr (idType binder)],
844      hsep [ptext SLIT("Rhs type:"), ppr ty]]
845
846 mkRhsPrimMsg :: Id -> CoreExpr -> Message
847 mkRhsPrimMsg binder rhs
848   = vcat [hsep [ptext SLIT("The type of this binder is primitive:"),
849                      ppr binder],
850               hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]
851              ]
852
853 mkUnboxedTupleMsg :: Id -> Message
854 mkUnboxedTupleMsg binder
855   = vcat [hsep [ptext SLIT("A variable has unboxed tuple type:"), ppr binder],
856           hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]]
857
858 mkCastErr from_ty expr_ty
859   = vcat [ptext SLIT("From-type of Cast differs from type of enclosed expression"),
860           ptext SLIT("From-type:") <+> ppr from_ty,
861           ptext SLIT("Type of enclosed expr:") <+> ppr expr_ty
862     ]
863
864 mkStrangeTyMsg e
865   = ptext SLIT("Type where expression expected:") <+> ppr e
866 \end{code}