CoreLint.lhs 30.7 KB
Newer Older
1

2
%
Simon Marlow's avatar
Simon Marlow committed
3
% (c) The University of Glasgow 2006
4
% (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
5
%
Simon Marlow's avatar
Simon Marlow committed
6
7

A ``lint'' pass to check for Core correctness
8
9

\begin{code}
10
{-# OPTIONS -w #-}
11
12
13
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and fix
-- any warnings in the module. See
Ian Lynagh's avatar
Ian Lynagh committed
14
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
15
16
-- for details

17
18
module CoreLint (
	lintCoreBindings,
19
	lintUnfolding, 
20
	showPass, endPass
21
22
    ) where

23
#include "HsVersions.h"
24

25
import NewDemand
26
import CoreSyn
Simon Marlow's avatar
Simon Marlow committed
27
28
import CoreFVs
import CoreUtils
29
import Bag
Simon Marlow's avatar
Simon Marlow committed
30
31
32
33
34
import Literal
import DataCon
import TysWiredIn
import Var
import VarEnv
35
import VarSet
Simon Marlow's avatar
Simon Marlow committed
36
import Name
37
import Id
38
import PprCore
Simon Marlow's avatar
Simon Marlow committed
39
40
41
42
43
44
45
import ErrUtils
import SrcLoc
import Type
import Coercion
import TyCon
import BasicTypes
import StaticFlags
46
import ListSetOps
Simon Marlow's avatar
Simon Marlow committed
47
import DynFlags
48
import Outputable
49
import Util
Simon Marlow's avatar
Simon Marlow committed
50
import Data.Maybe
51
52
\end{code}

53
54
%************************************************************************
%*									*
55
\subsection{End pass}
56
57
58
%*									*
%************************************************************************

59
@showPass@ and @endPass@ don't really belong here, but it makes a convenient
60
61
62
63
place for them.  They print out stuff before and after core passes,
and do Core Lint when necessary.

\begin{code}
64
endPass :: DynFlags -> String -> DynFlag -> [CoreBind] -> IO [CoreBind]
65
endPass dflags pass_name dump_flag binds
66
  = do 
67
68
	-- Report result size if required
	-- This has the side effect of forcing the intermediate to be evaluated
69
	debugTraceMsg dflags 2 $
70
		(text "    Result size =" <+> int (coreBindsSize binds))
71

72
	-- Report verbosely, if required
73
	dumpIfSet_core dflags dump_flag pass_name (pprCoreBindings binds)
74
75

	-- Type check
76
	lintCoreBindings dflags pass_name binds
77

78
	return binds
79
80
81
\end{code}


82
83
%************************************************************************
%*									*
84
\subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
85
86
87
%*									*
%************************************************************************

88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
Checks that a set of core bindings is well-formed.  The PprStyle and String
just control what we print in the event of an error.  The Bool value
indicates whether we have done any specialisation yet (in which case we do
some extra checks).

We check for
	(a) type errors
	(b) Out-of-scope type variables
	(c) Out-of-scope local variables
	(d) Ill-kinded types

If we have done specialisation the we check that there are
	(a) No top-level bindings of primitive (unboxed type)

Outstanding issues:

    --
    -- Things are *not* OK if:
    --
107
    --  * Unsaturated type app before specialisation has been done;
108
    --
109
    --  * Oversaturated type app after specialisation (eta reduction
110
    --   may well be happening...);
111

112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165

Note [Type lets]
~~~~~~~~~~~~~~~~
In the desugarer, it's very very convenient to be able to say (in effect)
	let a = Int in <body>
That is, use a type let.  (See notes just below for why we want this.)

We don't have type lets in Core, so the desugarer uses type lambda
	(/\a. <body>) Int
However, in the lambda form, we'd get lint errors from:
	(/\a. let x::a = 4 in <body>) Int
because (x::a) doesn't look compatible with (4::Int).

So (HACK ALERT) the Lint phase does type-beta reduction "on the fly",
as it were.  It carries a type substitution (in this example [a -> Int])
and applies this substitution before comparing types.  The functin
	lintTy :: Type -> LintM Type
returns a substituted type; that's the only reason it returns anything.

When we encounter a binder (like x::a) we must apply the substitution
to the type of the binding variable.  lintBinders does this.

For Ids, the type-substituted Id is added to the in_scope set (which 
itself is part of the TvSubst we are carrying down), and when we
find an occurence of an Id, we fetch it from the in-scope set.


Why we need type let
~~~~~~~~~~~~~~~~~~~~
It's needed when dealing with desugarer output for GADTs. Consider
  data T = forall a. T a (a->Int) Bool
   f :: T -> ... -> 
   f (T x f True)  = <e1>
   f (T y g False) = <e2>
After desugaring we get
	f t b = case t of 
		  T a (x::a) (f::a->Int) (b:Bool) ->
		    case b of 
			True -> <e1>
			False -> (/\b. let y=x; g=f in <e2>) a
And for a reason I now forget, the ...<e2>... can mention a; so 
we want Lint to know that b=a.  Ugh.

I tried quite hard to make the necessity for this go away, by changing the 
desugarer, but the fundamental problem is this:
	
	T a (x::a) (y::Int) -> let fail::a = ...
			       in (/\b. ...(case ... of       
						True  -> x::b
					 	False -> fail)
				  ) a
Now the inner case look as though it has incompatible branches.


166
\begin{code}
167
lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
168

169
lintCoreBindings dflags whoDunnit binds
170
  | not (dopt Opt_DoCoreLinting dflags)
sof's avatar
sof committed
171
172
  = return ()

173
lintCoreBindings dflags whoDunnit binds
174
  = case (initL (lint_binds binds)) of
175
      Nothing       -> showPass dflags ("Core Linted result of " ++ whoDunnit)
176
      Just bad_news -> printDump (display bad_news)	>>
177
		       ghcExit dflags 1
178
  where
179
180
181
	-- Put all the top-level binders in scope at the start
	-- This is because transformation rules can bring something
	-- into use 'unexpectedly'
182
183
    lint_binds binds = addLoc TopLevelBindings $
		       addInScopeVars (bindersOfBinds binds) $
184
		       mapM lint_bind binds 
185

186
187
    lint_bind (Rec prs)		= mapM_ (lintSingleBinding TopLevel Recursive) prs
    lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
sof's avatar
sof committed
188

189
190
191
    display bad_news
      = vcat [  text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
		bad_news,
sof's avatar
sof committed
192
		ptext SLIT("*** Offending Program ***"),
193
		pprCoreBindings binds,
sof's avatar
sof committed
194
195
		ptext SLIT("*** End of Offense ***")
	]
196
197
\end{code}

198
199
200
201
202
203
%************************************************************************
%*									*
\subsection[lintUnfolding]{lintUnfolding}
%*									*
%************************************************************************

204
205
We use this to check all unfoldings that come in from interfaces
(it is very painful to catch errors otherwise):
206

207
\begin{code}
208
lintUnfolding :: SrcLoc
209
	      -> [Var]		-- Treat these as in scope
210
	      -> CoreExpr
211
	      -> Maybe Message	-- Nothing => OK
212

213
lintUnfolding locn vars expr
214
  = initL (addLoc (ImportedUnfolding locn) $
215
216
	   addInScopeVars vars	           $
	   lintCoreExpr expr)
217
218
\end{code}

219
220
221
222
223
%************************************************************************
%*									*
\subsection[lintCoreBinding]{lintCoreBinding}
%*									*
%************************************************************************
224

225
Check a core binding, returning the list of variables bound.
226
227

\begin{code}
228
lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
229
  = addLoc (RhsOf binder) $
230
231
232
233
234
235
236
         -- Check the rhs 
    do { ty <- lintCoreExpr rhs	
       ; lintBinder binder -- Check match to RHS type
       ; binder_ty <- applySubst binder_ty
       ; checkTys binder_ty ty (mkRhsMsg binder ty)
        -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
       ; checkL (not (isUnLiftedType binder_ty)
237
            || (isNonRec rec_flag && exprOkForSpeculation rhs))
238
 	   (mkRhsPrimMsg binder rhs)
239
240
241
242
        -- Check that if the binder is top-level or recursive, it's not demanded
       ; checkL (not (isStrictId binder)
            || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
           (mkStrictMsg binder)
sof's avatar
sof committed
243
        -- Check whether binder's specialisations contain any out-of-scope variables
244
245
246
247
248
249
250
251
       ; mapM_ (checkBndrIdInScope binder) bndr_vars 

      -- Check whether arity and demand type are consistent (only if demand analysis
      -- already happened)
       ; checkL (case maybeDmdTy of
                  Just (StrictSig dmd_ty) -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs
                  Nothing -> True)
           (mkArityMsg binder) }
sof's avatar
sof committed
252
	  
253
	-- We should check the unfolding, if any, but this is tricky because
254
255
256
257
258
 	-- the unfolding is a SimplifiableCoreExpr. Give up for now.
   where
    binder_ty                  = idType binder
    maybeDmdTy                 = idNewStrictness_maybe binder
    bndr_vars                  = varSetElems (idFreeVars binder)
259
260
    lintBinder var | isId var  = lintIdBndr var $ \_ -> (return ())
	           | otherwise = return ()
261
262
\end{code}

263
264
265
266
267
268
%************************************************************************
%*									*
\subsection[lintCoreExpr]{lintCoreExpr}
%*									*
%************************************************************************

269
\begin{code}
270
271
type InType  = Type	-- Substitution not yet applied
type OutType = Type	-- Substitution has been applied to this
272

273
lintCoreExpr :: CoreExpr -> LintM OutType
274
275
-- The returned type has the substitution from the monad 
-- already applied to it:
276
--	lintCoreExpr e subst = exprType (subst e)
277
278

lintCoreExpr (Var var)
279
280
281
282
283
  = do	{ checkL (not (var == oneTupleDataConId))
		 (ptext SLIT("Illegal one-tuple"))
	; var' <- lookupIdInScope var
        ; return (idType var')
        }
284

285
286
lintCoreExpr (Lit lit)
  = return (literalType lit)
287

288
289
290
291
292
293
294
295
296
297
298
299
300
--lintCoreExpr (Note (Coerce to_ty from_ty) expr)
--  = do	{ expr_ty <- lintCoreExpr expr
--	; to_ty <- lintTy to_ty
--	; from_ty <- lintTy from_ty	
--	; checkTys from_ty expr_ty (mkCoerceErr from_ty expr_ty)
--	; return to_ty }

lintCoreExpr (Cast expr co)
  = do { expr_ty <- lintCoreExpr expr
       ; co' <- lintTy co
       ; let (from_ty, to_ty) = coercionKind co'
       ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
       ; return to_ty }
301
302
303

lintCoreExpr (Note other_note expr)
  = lintCoreExpr expr
304

305
lintCoreExpr (Let (NonRec bndr rhs) body)
306
  = do	{ lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
307
	; addLoc (BodyOfLetRec [bndr])
308
		 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
309

310
lintCoreExpr (Let (Rec pairs) body) 
311
  = lintAndScopeIds bndrs	$ \_ ->
312
    do	{ mapM (lintSingleBinding NotTopLevel Recursive) pairs	
313
	; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
314
315
  where
    bndrs = map fst pairs
316

317
lintCoreExpr e@(App fun (Type ty))
318
-- See Note [Type let] above
319
320
  = addLoc (AnExpr e) $
    go fun [ty]
321
322
323
324
325
  where
    go (App fun (Type ty)) tys
	= do { go fun (ty:tys) }
    go (Lam tv body) (ty:tys)
	= do  { checkL (isTyVar tv) (mkKindErrMsg tv ty)	-- Not quite accurate
326
327
328
329
330
	      ; ty' <- lintTy ty 
              ; let kind = tyVarKind tv
              ; kind' <- lintTy kind
              ; let tv' = setTyVarKind tv kind'
	      ; checkKinds tv' ty'              
331
332
		-- Now extend the substitution so we 
		-- take advantage of it in the body
333
334
	      ; addInScopeVars [tv'] $
	        extendSubstL tv' ty' $
335
336
337
338
339
		go body tys }
    go fun tys
	= do  { fun_ty <- lintCoreExpr fun
	      ; lintCoreArgs fun_ty (map Type tys) }

340
lintCoreExpr e@(App fun arg)
341
  = do	{ fun_ty <- lintCoreExpr fun
342
	; addLoc (AnExpr e) $
343
          lintCoreArg fun_ty arg }
344
345

lintCoreExpr (Lam var expr)
346
  = addLoc (LambdaBodyOf var) $
347
348
349
350
351
352
353
    lintBinders [var] $ \[var'] -> 
    do { body_ty <- lintCoreExpr expr
       ; if isId var' then 
             return (mkFunTy (idType var') body_ty) 
	 else
	     return (mkForAllTy var' body_ty)
       }
354
355
356
357
358
359
360
	-- The applySubst is needed to apply the subst to var

lintCoreExpr e@(Case scrut var alt_ty alts) =
       -- Check the scrutinee
  do { scrut_ty <- lintCoreExpr scrut
     ; alt_ty   <- lintTy alt_ty  
     ; var_ty   <- lintTy (idType var)	
361
	-- Don't use lintIdBndr on var, because unboxed tuple is legitimate
362

363
364
     ; subst <- getTvSubst 
     ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
365
366

     -- If the binder is an unboxed tuple type, don't put it in scope
367
368
369
370
     ; let scope = if (isUnboxedTupleType (idType var)) then 
                       pass_var 
                   else lintAndScopeId var
     ; scope $ \_ ->
371
       do { -- Check the alternatives
372
373
            mapM (lintCoreAlt scrut_ty alt_ty) alts
          ; checkCaseAlts e scrut_ty alts
374
          ; return alt_ty } }
375
376
  where
    pass_var f = f var
377
378
379

lintCoreExpr e@(Type ty)
  = addErrL (mkStrangeTyMsg e)
380
\end{code}
381

382
383
384
385
386
%************************************************************************
%*									*
\subsection[lintCoreArgs]{lintCoreArgs}
%*									*
%************************************************************************
387

388
389
The basic version of these functions checks that the argument is a
subtype of the required type, as one would expect.
390

391
\begin{code}
392
393
lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
lintCoreArg  :: OutType -> CoreArg   -> LintM OutType
394
-- First argument has already had substitution applied to it
395
396
397
\end{code}

\begin{code}
398
399
400
401
402
lintCoreArgs ty [] = return ty
lintCoreArgs ty (a : args) = 
  do { res <- lintCoreArg ty a
     ; lintCoreArgs res args }

403
lintCoreArg fun_ty a@(Type arg_ty) = 
404
  do { arg_ty <- lintTy arg_ty	
405
     ; lintTyApp fun_ty arg_ty }
406
407
408
409

lintCoreArg fun_ty arg = 
       -- Make sure function type matches argument
  do { arg_ty <- lintCoreExpr arg
410
411
     ; let err1 =  mkAppMsg fun_ty arg_ty arg
           err2 = mkNonFunAppMsg fun_ty arg_ty arg
412
413
     ; case splitFunTy_maybe fun_ty of
        Just (arg,res) -> 
414
          do { checkTys arg arg_ty err1
415
             ; return res }
416
        _ -> addErrL err2 }
417
\end{code}
418

419
\begin{code}
420
-- Both args have had substitution applied
421
lintTyApp :: OutType -> OutType -> LintM OutType
422
423
424
lintTyApp ty arg_ty 
  = case splitForAllTy_maybe ty of
      Nothing -> addErrL (mkTyAppMsg ty arg_ty)
425

426
427
428
429
430
431
432
433
434
435
      Just (tyvar,body)
        -> do	{ checkL (isTyVar tyvar) (mkTyAppMsg ty arg_ty)
		; checkKinds tyvar arg_ty
		; return (substTyWith [tyvar] [arg_ty] body) }

checkKinds tyvar arg_ty
	-- Arg type might be boxed for a function with an uncommitted
	-- tyvar; notably this is used so that we can give
	-- 	error :: forall a:*. String -> a
	-- and then apply it to both boxed and unboxed types.
436
  = checkL (arg_kind `isSubKind` tyvar_kind)
437
438
439
	   (mkKindErrMsg tyvar arg_ty)
  where
    tyvar_kind = tyVarKind tyvar
440
    arg_kind | isCoVar tyvar = coercionKindPredTy arg_ty
441
	     | otherwise     = typeKind arg_ty
442
\end{code}
443
444


445
446
447
448
449
450
451
%************************************************************************
%*									*
\subsection[lintCoreAlts]{lintCoreAlts}
%*									*
%************************************************************************

\begin{code}
452
checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
453
-- a) Check that the alts are non-empty
454
455
-- b1) Check that the DEFAULT comes first, if it exists
-- b2) Check that the others are in increasing order
456
457
458
459
460
461
462
463
-- c) Check that there's a default for infinite types
-- NB: Algebraic cases are not necessarily exhaustive, because
--     the simplifer correctly eliminates case that can't 
--     possibly match.

checkCaseAlts e ty [] 
  = addErrL (mkNullAltsMsg e)

464
465
checkCaseAlts e ty alts = 
  do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
466
     ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
467
468
     ; checkL (isJust maybe_deflt || not is_infinite_ty)
	   (nonExhaustiveAltsMsg e) }
469
470
  where
    (con_alts, maybe_deflt) = findDefault alts
471

472
473
474
475
	-- Check that successive alternatives have increasing tags 
    increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
    increasing_tag other 		     = True

476
477
478
479
480
481
    non_deflt (DEFAULT, _, _) = False
    non_deflt alt	      = True

    is_infinite_ty = case splitTyConApp_maybe ty of
			Nothing			    -> False
			Just (tycon, tycon_arg_tys) -> isPrimTyCon tycon
482
483
484
\end{code}

\begin{code}
485
486
checkAltExpr :: CoreExpr -> OutType -> LintM ()
checkAltExpr expr ann_ty
487
  = do { actual_ty <- lintCoreExpr expr 
488
       ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
489

490
491
lintCoreAlt :: OutType 		-- Type of scrutinee
            -> OutType          -- Type of the alternative
492
	    -> CoreAlt
493
	    -> LintM ()
494

495
496
497
lintCoreAlt scrut_ty alt_ty alt@(DEFAULT, args, rhs) = 
  do { checkL (null args) (mkDefaultArgsMsg args)
     ; checkAltExpr rhs alt_ty }
498

499
500
lintCoreAlt scrut_ty alt_ty alt@(LitAlt lit, args, rhs) = 
  do { checkL (null args) (mkDefaultArgsMsg args)
501
     ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)	
502
     ; checkAltExpr rhs alt_ty } 
503
504
  where
    lit_ty = literalType lit
505

506
lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
507
  | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
508
  | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
509
510
511
  = addLoc (CaseAlt alt) $  do
    {   -- First instantiate the universally quantified 
	-- type variables of the data constructor
512
513
514
	-- We've already check
      checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
    ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
515
516
517
518
519

	-- And now bring the new binders into scope
    ; lintBinders args $ \ args -> do
    { addLoc (CasePat alt) $ do
	  {    -- Check the pattern
520
521
522
523
524
		 -- Scrutinee type must be a tycon applicn; checked by caller
		 -- This code is remarkably compact considering what it does!
		 -- NB: args must be in scope here so that the lintCoreArgs line works.
	         -- NB: relies on existential type args coming *after* ordinary type args

525
	  ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
526
527
528
	  ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty) 
 	  }
	       -- Check the RHS
529
    ; checkAltExpr rhs alt_ty } }
530
531
532

  | otherwise	-- Scrut-ty is wrong shape
  = addErrL (mkBadAltMsg scrut_ty alt)
533
\end{code}
534

sof's avatar
sof committed
535
536
%************************************************************************
%*									*
537
\subsection[lint-types]{Types}
sof's avatar
sof committed
538
539
540
541
%*									*
%************************************************************************

\begin{code}
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
-- When we lint binders, we (one at a time and in order):
--  1. Lint var types or kinds (possibly substituting)
--  2. Add the binder to the in scope set, and if its a coercion var,
--     we may extend the substitution to reflect its (possibly) new kind
lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
lintBinders [] linterF = linterF []
lintBinders (var:vars) linterF = lintBinder var $ \var' ->
				 lintBinders vars $ \ vars' ->
				 linterF (var':vars')

lintBinder :: Var -> (Var -> LintM a) -> LintM a
lintBinder var linterF
  | isTyVar var = lint_ty_bndr
  | otherwise   = lintIdBndr var linterF
  where
    lint_ty_bndr = do { lintTy (tyVarKind var)
		      ; subst <- getTvSubst
		      ; let (subst', tv') = substTyVarBndr subst var
		      ; updateTvSubst subst' (linterF tv') }

lintIdBndr :: Var -> (Var -> LintM a) -> LintM a
-- Do substitution on the type of a binder and add the var with this 
-- new type to the in-scope set of the second argument
565
-- ToDo: lint its rules
566
lintIdBndr id linterF 
567
568
569
  = do 	{ checkL (not (isUnboxedTupleType (idType id))) 
		 (mkUnboxedTupleMsg id)
		-- No variable can be bound to an unboxed tuple.
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
        ; lintAndScopeId id $ \id' -> linterF id'
        }

lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
lintAndScopeIds ids linterF 
  = go ids
  where
    go []       = linterF []
    go (id:ids) = do { lintAndScopeId id $ \id ->
                           lintAndScopeIds ids $ \ids ->
                           linterF (id:ids) }

lintAndScopeId :: Var -> (Var -> LintM a) -> LintM a
lintAndScopeId id linterF 
  = do { ty <- lintTy (idType id)
585
       ; let id' = Var.setIdType id ty
586
587
       ; addInScopeVars [id'] $ (linterF id')
       }
588

589
lintTy :: InType -> LintM OutType
590
591
592
593
-- Check the type, and apply the substitution to it
-- ToDo: check the kind structure of the type
lintTy ty 
  = do	{ ty' <- applySubst ty
594
	; mapM_ checkTyVarInScope (varSetElems (tyVarsOfType ty'))
595
	; return ty' }
sof's avatar
sof committed
596
597
\end{code}

598
    
599
600
601
602
603
604
605
%************************************************************************
%*									*
\subsection[lint-monad]{The Lint monad}
%*									*
%************************************************************************

\begin{code}
606
607
608
609
610
611
612
613
614
newtype LintM a = 
   LintM { unLintM :: 
            [LintLocInfo] ->         -- Locations
            TvSubst ->               -- Current type substitution; we also use this
				     -- to keep track of all the variables in scope,
				     -- both Ids and TyVars
	    Bag Message ->           -- Error messages so far
	    (Maybe a, Bag Message) } -- Result and error messages (if any)

615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
{-	Note [Type substitution]
	~~~~~~~~~~~~~~~~~~~~~~~~
Why do we need a type substitution?  Consider
	/\(a:*). \(x:a). /\(a:*). id a x
This is ill typed, because (renaming variables) it is really
	/\(a:*). \(x:a). /\(b:*). id b x
Hence, when checking an application, we can't naively compare x's type
(at its binding site) with its expected type (at a use site).  So we
rename type binders as we go, maintaining a substitution.

The same substitution also supports let-type, current expressed as
	(/\(a:*). body) ty
Here we substitute 'ty' for 'a' in 'body', on the fly.
-}

630
631
632
633
634
635
636
637
instance Monad LintM where
  return x = LintM (\ loc subst errs -> (Just x, errs))
  fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
  m >>= k  = LintM (\ loc subst errs -> 
                       let (res, errs') = unLintM m loc subst errs in
                         case res of
                           Just r -> unLintM (k r) loc subst errs'
                           Nothing -> (Nothing, errs'))
638
639

data LintLocInfo
640
641
642
  = RhsOf Id		-- The variable bound
  | LambdaBodyOf Id	-- The lambda-binder
  | BodyOfLetRec [Id]	-- One of the binders
643
644
  | CaseAlt CoreAlt	-- Case alternative
  | CasePat CoreAlt	-- *Pattern* of the case alternative
645
646
  | AnExpr CoreExpr	-- Some expression
  | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
647
  | TopLevelBindings
648
649
\end{code}

650
                 
651
\begin{code}
652
initL :: LintM a -> Maybe Message {- errors -}
653
initL m
654
  = case unLintM m [] emptyTvSubst emptyBag of
655
656
      (_, errs) | isEmptyBag errs -> Nothing
		| otherwise	  -> Just (vcat (punctuate (text "") (bagToList errs)))
657
658
659
\end{code}

\begin{code}
sof's avatar
sof committed
660
checkL :: Bool -> Message -> LintM ()
661
checkL True  msg = return ()
662
checkL False msg = addErrL msg
sof's avatar
sof committed
663

sof's avatar
sof committed
664
addErrL :: Message -> LintM a
665
addErrL msg = LintM (\ loc subst errs -> (Nothing, addErr subst errs msg loc))
666

667
668
addErr :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
addErr subst errs_so_far msg locs
sof's avatar
sof committed
669
  = ASSERT( notNull locs )
sof's avatar
sof committed
670
671
    errs_so_far `snocBag` mk_msg msg
  where
672
673
   (loc, cxt1) = dumpLoc (head locs)
   cxts        = [snd (dumpLoc loc) | loc <- locs]   
674
675
   context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
				      ptext SLIT("Substitution:") <+> ppr subst
676
677
	       | otherwise	    = cxt1
 
678
   mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
679
680

addLoc :: LintLocInfo -> LintM a -> LintM a
681
682
addLoc extra_loc m =
  LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
683

684
addInScopeVars :: [Var] -> LintM a -> LintM a
685
686
687
688
689
690
691
addInScopeVars vars m
  | null dups
  = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst vars) errs)
  | otherwise
  = addErrL (dupVars dups)
  where
    (_, dups) = removeDups compare vars 
692

693
694
695
updateTvSubst :: TvSubst -> LintM a -> LintM a
updateTvSubst subst' m = 
  LintM (\ loc subst errs -> unLintM m loc subst' errs)
696
697
698
699
700
701
702
703
704
705

getTvSubst :: LintM TvSubst
getTvSubst = LintM (\ loc subst errs -> (Just subst, errs))

applySubst :: Type -> LintM Type
applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }

extendSubstL :: TyVar -> Type -> LintM a -> LintM a
extendSubstL tv ty m
  = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
706
707
708
\end{code}

\begin{code}
709
710
711
712
713
714
715
716
717
718
719
720
721
lookupIdInScope :: Id -> LintM Id
lookupIdInScope id 
  | not (mustHaveLocalBinding id)
  = return id	-- An imported Id
  | otherwise	
  = do	{ subst <- getTvSubst
	; case lookupInScope (getTvInScope subst) id of
		Just v  -> return v
		Nothing -> do { addErrL out_of_scope
			      ; return id } }
  where
    out_of_scope = ppr id <+> ptext SLIT("is out of scope")

722
723
724

oneTupleDataConId :: Id	-- Should not happen
oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
sof's avatar
sof committed
725

726
checkBndrIdInScope :: Var -> Var -> LintM ()
727
checkBndrIdInScope binder id 
sof's avatar
sof committed
728
729
  = checkInScope msg id
    where
730
     msg = ptext SLIT("is out of scope inside info for") <+> 
sof's avatar
sof committed
731
732
	   ppr binder

733
734
735
checkTyVarInScope :: TyVar -> LintM ()
checkTyVarInScope tv = checkInScope (ptext SLIT("is out of scope")) tv

736
checkInScope :: SDoc -> Var -> LintM ()
737
738
739
740
checkInScope loc_msg var =
 do { subst <- getTvSubst
    ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
             (hsep [ppr var, loc_msg]) }
sof's avatar
sof committed
741

sof's avatar
sof committed
742
checkTys :: Type -> Type -> Message -> LintM ()
743
744
-- check ty2 is subtype of ty1 (ie, has same structure but usage
-- annotations need only be consistent, not equal)
745
-- Assumes ty1,ty2 are have alrady had the substitution applied
746
checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
747
748
\end{code}

749
750
751
752
753
754
%************************************************************************
%*									*
\subsection{Error messages}
%*									*
%************************************************************************

755
\begin{code}
sof's avatar
sof committed
756
757
dumpLoc (RhsOf v)
  = (getSrcLoc v, brackets (ptext SLIT("RHS of") <+> pp_binders [v]))
758

sof's avatar
sof committed
759
760
dumpLoc (LambdaBodyOf b)
  = (getSrcLoc b, brackets (ptext SLIT("in body of lambda with binder") <+> pp_binder b))
sof's avatar
sof committed
761

762
763
764
765
dumpLoc (BodyOfLetRec [])
  = (noSrcLoc, brackets (ptext SLIT("In body of a letrec with no binders")))

dumpLoc (BodyOfLetRec bs@(_:_))
sof's avatar
sof committed
766
  = ( getSrcLoc (head bs), brackets (ptext SLIT("in body of letrec with binders") <+> pp_binders bs))
767

sof's avatar
sof committed
768
769
dumpLoc (AnExpr e)
  = (noSrcLoc, text "In the expression:" <+> ppr e)
sof's avatar
sof committed
770

sof's avatar
sof committed
771
dumpLoc (CaseAlt (con, args, rhs))
772
773
774
775
  = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))

dumpLoc (CasePat (con, args, rhs))
  = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
776

sof's avatar
sof committed
777
778
dumpLoc (ImportedUnfolding locn)
  = (locn, brackets (ptext SLIT("in an imported unfolding")))
779
780
dumpLoc TopLevelBindings
  = (noSrcLoc, empty)
781

782
pp_binders :: [Var] -> SDoc
783
784
pp_binders bs = sep (punctuate comma (map pp_binder bs))

785
786
787
pp_binder :: Var -> SDoc
pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
            | isTyVar b = hsep [ppr b, dcolon, ppr (tyVarKind b)]
788
\end{code}
789

790
791
792
793
\begin{code}
------------------------------------------------------
--	Messages for case expressions

sof's avatar
sof committed
794
mkNullAltsMsg :: CoreExpr -> Message
795
796
797
798
mkNullAltsMsg e 
  = hang (text "Case expression with no alternatives:")
	 4 (ppr e)

799
mkDefaultArgsMsg :: [Var] -> Message
800
801
802
803
mkDefaultArgsMsg args 
  = hang (text "DEFAULT case with binders")
	 4 (ppr args)

804
805
806
807
mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
mkCaseAltMsg e ty1 ty2
  = hang (text "Type of case alternatives not the same as the annotation on case:")
	 4 (vcat [ppr ty1, ppr ty2, ppr e])
808

809
810
mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
mkScrutMsg var var_ty scrut_ty subst
811
  = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
812
813
814
	  text "Result binder type:" <+> ppr var_ty,--(idType var),
	  text "Scrutinee type:" <+> ppr scrut_ty,
     hsep [ptext SLIT("Current TV subst"), ppr subst]]
815

816
817
mkNonDefltMsg e
  = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
818
819
mkNonIncreasingAltsMsg e
  = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
820

sof's avatar
sof committed
821
nonExhaustiveAltsMsg :: CoreExpr -> Message
822
nonExhaustiveAltsMsg e
823
  = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
824

825
826
827
828
829
830
831
832
mkBadConMsg :: TyCon -> DataCon -> Message
mkBadConMsg tycon datacon
  = vcat [
	text "In a case alternative, data constructor isn't in scrutinee type:",
	text "Scrutinee type constructor:" <+> ppr tycon,
	text "Data con:" <+> ppr datacon
    ]

sof's avatar
sof committed
833
mkBadPatMsg :: Type -> Type -> Message
834
835
836
837
838
839
mkBadPatMsg con_result_ty scrut_ty
  = vcat [
	text "In a case alternative, pattern result type doesn't match scrutinee type:",
	text "Pattern result type:" <+> ppr con_result_ty,
	text "Scrutinee type:" <+> ppr scrut_ty
    ]
840

841
842
843
844
845
846
mkBadAltMsg :: Type -> CoreAlt -> Message
mkBadAltMsg scrut_ty alt
  = vcat [ text "Data alternative when scrutinee is not a tycon application",
	   text "Scrutinee type:" <+> ppr scrut_ty,
	   text "Alternative:" <+> pprCoreAlt alt ]

847
848
849
850
851
852
853
mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
mkNewTyDataConAltMsg scrut_ty alt
  = vcat [ text "Data alternative for newtype datacon",
	   text "Scrutinee type:" <+> ppr scrut_ty,
	   text "Alternative:" <+> pprCoreAlt alt ]


854
855
------------------------------------------------------
--	Other error messages
856

857
858
mkAppMsg :: Type -> Type -> CoreExpr -> Message
mkAppMsg fun_ty arg_ty arg
sof's avatar
sof committed
859
  = vcat [ptext SLIT("Argument value doesn't match argument type:"),
860
861
862
	      hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
	      hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
	      hang (ptext SLIT("Arg:")) 4 (ppr arg)]
863

864
865
866
867
868
869
870
mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
mkNonFunAppMsg fun_ty arg_ty arg
  = vcat [ptext SLIT("Non-function type in function position"),
	      hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
	      hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
	      hang (ptext SLIT("Arg:")) 4 (ppr arg)]

sof's avatar
sof committed
871
mkKindErrMsg :: TyVar -> Type -> Message
872
mkKindErrMsg tyvar arg_ty
873
874
  = vcat [ptext SLIT("Kinds don't match in type application:"),
	  hang (ptext SLIT("Type variable:"))
875
		 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
876
	  hang (ptext SLIT("Arg type:"))   
877
	         4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
878

sof's avatar
sof committed
879
mkTyAppMsg :: Type -> Type -> Message
880
881
mkTyAppMsg ty arg_ty
  = vcat [text "Illegal type application:",
882
	      hang (ptext SLIT("Exp type:"))
883
		 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
884
	      hang (ptext SLIT("Arg type:"))   
885
	         4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
886

sof's avatar
sof committed
887
mkRhsMsg :: Id -> Type -> Message
888
mkRhsMsg binder ty
sof's avatar
sof committed
889
890
  = vcat
    [hsep [ptext SLIT("The type of this binder doesn't match the type of its RHS:"),
891
892
893
	    ppr binder],
     hsep [ptext SLIT("Binder's type:"), ppr (idType binder)],
     hsep [ptext SLIT("Rhs type:"), ppr ty]]
894

sof's avatar
sof committed
895
mkRhsPrimMsg :: Id -> CoreExpr -> Message
896
mkRhsPrimMsg binder rhs
sof's avatar
sof committed
897
  = vcat [hsep [ptext SLIT("The type of this binder is primitive:"),
898
899
		     ppr binder],
	      hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]
900
	     ]
901

902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
mkStrictMsg :: Id -> Message
mkStrictMsg binder
  = vcat [hsep [ptext SLIT("Recursive or top-level binder has strict demand info:"),
		     ppr binder],
	      hsep [ptext SLIT("Binder's demand info:"), ppr (idNewDemandInfo binder)]
	     ]

mkArityMsg :: Id -> Message
mkArityMsg binder
  = vcat [hsep [ptext SLIT("Demand type has "),
                     ppr (dmdTypeDepth dmd_ty),
                     ptext SLIT(" arguments, rhs has "),
                     ppr (idArity binder),
                     ptext SLIT("arguments, "),
		     ppr binder],
	      hsep [ptext SLIT("Binder's strictness signature:"), ppr dmd_ty]

         ]
           where (StrictSig dmd_ty) = idNewStrictness binder

sof's avatar
sof committed
922
mkUnboxedTupleMsg :: Id -> Message
923
924
925
926
mkUnboxedTupleMsg binder
  = vcat [hsep [ptext SLIT("A variable has unboxed tuple type:"), ppr binder],
	  hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]]

927
928
mkCastErr from_ty expr_ty
  = vcat [ptext SLIT("From-type of Cast differs from type of enclosed expression"),
929
930
931
	  ptext SLIT("From-type:") <+> ppr from_ty,
	  ptext SLIT("Type of enclosed expr:") <+> ppr expr_ty
    ]
932

933
934
935
936
dupVars vars
  = hang (ptext SLIT("Duplicate variables brought into scope"))
       2 (ppr vars)

937
938
mkStrangeTyMsg e
  = ptext SLIT("Type where expression expected:") <+> ppr e
939
\end{code}