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