CoreLint.lhs 42.4 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_GHC -fprof-auto #-}
Ian Lynagh's avatar
Ian Lynagh committed
11
12
13
14
15
16
17
{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

18
module CoreLint ( lintCoreBindings, lintUnfolding ) where
19

20
#include "HsVersions.h"
21

22
import Demand
23
import CoreSyn
Simon Marlow's avatar
Simon Marlow committed
24
25
import CoreFVs
import CoreUtils
26
import Pair
27
import Bag
Simon Marlow's avatar
Simon Marlow committed
28
29
30
import Literal
import DataCon
import TysWiredIn
batterseapower's avatar
batterseapower committed
31
import TysPrim
Simon Marlow's avatar
Simon Marlow committed
32
33
import Var
import VarEnv
34
import VarSet
Simon Marlow's avatar
Simon Marlow committed
35
import Name
36
import Id
37
import PprCore
Simon Marlow's avatar
Simon Marlow committed
38
import ErrUtils
batterseapower's avatar
batterseapower committed
39
import Coercion
Simon Marlow's avatar
Simon Marlow committed
40
import SrcLoc
41
import Kind
Simon Marlow's avatar
Simon Marlow committed
42
import Type
43
import TypeRep
Simon Marlow's avatar
Simon Marlow committed
44
45
46
import TyCon
import BasicTypes
import StaticFlags
47
import ListSetOps
48
import PrelNames
49
import Outputable
50
import FastString
51
import Util
52
import Control.Monad
53
import MonadUtils
Simon Marlow's avatar
Simon Marlow committed
54
import Data.Maybe
55
56
57
58
\end{code}

%************************************************************************
%*									*
59
\subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
60
61
62
%*									*
%************************************************************************

63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
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:
    --
82
    --  * Unsaturated type app before specialisation has been done;
83
    --
84
    --  * Oversaturated type app after specialisation (eta reduction
85
    --   may well be happening...);
86

87

88
89
Note [Linting type lets]
~~~~~~~~~~~~~~~~~~~~~~~~
90
In the desugarer, it's very very convenient to be able to say (in effect)
91
92
93
94
95
96
	let a = Type Int in <body>
That is, use a type let.   See Note [Type let] in CoreSyn.

However, when linting <body> we need to remember that a=Int, else we might
reject a correct program.  So we carry a type substitution (in this example 
[a -> Int]) and apply this substitution before comparing types.  The functin
97
	lintInTy :: Type -> LintM Type
98
99
100
101
102
103
104
105
106
107
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.


108
\begin{code}
109
lintCoreBindings :: CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
110
111
--   Returns (warnings, errors)
lintCoreBindings binds
112
113
114
  = initL $ 
    addLoc TopLevelBindings $
    addInScopeVars binders  $
115
116
117
	-- Put all the top-level binders in scope at the start
	-- This is because transformation rules can bring something
	-- into use 'unexpectedly'
118
119
120
121
122
123
124
125
126
127
128
129
130
    do { checkL (null dups) (dupVars dups)
       ; checkL (null ext_dups) (dupExtVars ext_dups)
       ; mapM lint_bind binds }
  where
    binders = bindersOfBinds binds
    (_, dups) = removeDups compare binders

    -- dups_ext checks for names with different uniques
    -- but but the same External name M.n.  We don't
    -- allow this at top level:
    --    M.n{r3}  = ...
    --    M.n{r29} = ...
    -- becuase they both get the same linker symbol
131
132
133
134
135
    ext_dups = snd (removeDups ord_ext (map Var.varName binders))
    ord_ext n1 n2 | Just m1 <- nameModule_maybe n1
                  , Just m2 <- nameModule_maybe n2
                  = compare (m1, nameOccName n1) (m2, nameOccName n2)
                  | otherwise = LT
136

137
138
    lint_bind (Rec prs)		= mapM_ (lintSingleBinding TopLevel Recursive) prs
    lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
139
140
\end{code}

141
142
143
144
145
146
%************************************************************************
%*									*
\subsection[lintUnfolding]{lintUnfolding}
%*									*
%************************************************************************

147
148
We use this to check all unfoldings that come in from interfaces
(it is very painful to catch errors otherwise):
149

150
\begin{code}
151
lintUnfolding :: SrcLoc
152
	      -> [Var]		-- Treat these as in scope
153
	      -> CoreExpr
154
	      -> Maybe MsgDoc	-- Nothing => OK
155

156
lintUnfolding locn vars expr
157
  | isEmptyBag errs = Nothing
158
  | otherwise       = Just (pprMessageBag errs)
159
160
161
162
  where
    (_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
                            addInScopeVars vars	           $
                            lintCoreExpr expr)
163
164
\end{code}

165
166
167
168
169
%************************************************************************
%*									*
\subsection[lintCoreBinding]{lintCoreBinding}
%*									*
%************************************************************************
170

171
Check a core binding, returning the list of variables bound.
172
173

\begin{code}
twanvl's avatar
twanvl committed
174
lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
175
lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
176
  = addLoc (RhsOf binder) $
177
178
179
         -- Check the rhs 
    do { ty <- lintCoreExpr rhs	
       ; lintBinder binder -- Check match to RHS type
180
       ; binder_ty <- applySubstTy binder_ty
181
182
183
       ; checkTys binder_ty ty (mkRhsMsg binder ty)
        -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
       ; checkL (not (isUnLiftedType binder_ty)
184
            || (isNonRec rec_flag && exprOkForSpeculation rhs))
185
 	   (mkRhsPrimMsg binder rhs)
186
187
188
189
        -- 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
190
        -- Check whether binder's specialisations contain any out-of-scope variables
191
192
       ; mapM_ (checkBndrIdInScope binder) bndr_vars 

193
       ; when (isStrongLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
194
195
              (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
	      -- Only non-rule loop breakers inhibit inlining
196

197
198
199
200
201
202
      -- 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
203
	  
204
	-- We should check the unfolding, if any, but this is tricky because
205
206
207
 	-- the unfolding is a SimplifiableCoreExpr. Give up for now.
   where
    binder_ty                  = idType binder
208
    maybeDmdTy                 = idStrictness_maybe binder
209
    bndr_vars                  = varSetElems (idFreeVars binder)
210
211
    lintBinder var | isId var  = lintIdBndr var $ \_ -> (return ())
	           | otherwise = return ()
212
213
\end{code}

214
215
216
217
218
219
%************************************************************************
%*									*
\subsection[lintCoreExpr]{lintCoreExpr}
%*									*
%************************************************************************

220
\begin{code}
dreixel's avatar
dreixel committed
221
222
--type InKind      = Kind	-- Substitution not yet applied
type InType      = Type	
223
224
225
type InCoercion  = Coercion
type InVar       = Var
type InTyVar     = TyVar
226

227
228
229
230
231
232
233
234
235
type OutKind     = Kind	-- Substitution has been applied to this,
                        -- but has not been linted yet
type LintedKind  = Kind -- Substitution applied, and type is linted

type OutType     = Type	-- Substitution has been applied to this,
                        -- but has not been linted yet

type LintedType  = Type -- Substitution applied, and type is linted

236
237
238
type OutCoercion = Coercion
type OutVar      = Var
type OutTyVar    = TyVar
239

240
lintCoreExpr :: CoreExpr -> LintM OutType
241
242
-- The returned type has the substitution from the monad 
-- already applied to it:
243
--	lintCoreExpr e subst = exprType (subst e)
244
245
--
-- The returned "type" can be a kind, if the expression is (Type ty)
246
247

lintCoreExpr (Var var)
248
  = do	{ checkL (not (var == oneTupleDataConId))
Ian Lynagh's avatar
Ian Lynagh committed
249
		 (ptext (sLit "Illegal one-tuple"))
250

251
252
253
        ; checkL (isId var && not (isCoVar var))
                 (ptext (sLit "Non term variable") <+> ppr var)

254
        ; checkDeadIdOcc var
255
	; var' <- lookupIdInScope var
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
256
        ; return (idType var') }
257

258
259
lintCoreExpr (Lit lit)
  = return (literalType lit)
260

261
262
lintCoreExpr (Cast expr co)
  = do { expr_ty <- lintCoreExpr expr
263
       ; co' <- applySubstCo co
264
       ; (_, from_ty, to_ty) <- lintCoercion co'
265
266
       ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
       ; return to_ty }
267

268
269
270
271
272
273
274
lintCoreExpr (Tick (Breakpoint _ ids) expr)
  = do forM_ ids $ \id -> do
         checkDeadIdOcc id
         lookupIdInScope id
       lintCoreExpr expr

lintCoreExpr (Tick _other_tickish expr)
275
  = lintCoreExpr expr
276

277
lintCoreExpr (Let (NonRec tv (Type ty)) body)
278
279
  | isTyVar tv
  =	-- See Note [Linting type lets]
280
    do	{ ty' <- applySubstTy ty
281
        ; lintTyBndr tv              $ \ tv' -> 
282
    do  { addLoc (RhsOf tv) $ checkTyKind tv' ty'
283
284
		-- Now extend the substitution so we 
		-- take advantage of it in the body
285
286
287
        ; extendSubstL tv' ty'       $ 
          addLoc (BodyOfLetRec [tv]) $ 
          lintCoreExpr body } }
288

289
lintCoreExpr (Let (NonRec bndr rhs) body)
290
  | isId bndr
291
  = do	{ lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
292
	; addLoc (BodyOfLetRec [bndr]) 
293
		 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
294

295
296
297
  | otherwise
  = failWithL (mkLetErr bndr rhs)	-- Not quite accurate

298
lintCoreExpr (Let (Rec pairs) body) 
299
  = lintAndScopeIds bndrs	$ \_ ->
300
301
    do	{ checkL (null dups) (dupVars dups)
        ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs	
302
	; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
303
304
  where
    bndrs = map fst pairs
305
    (_, dups) = removeDups compare bndrs
306

batterseapower's avatar
batterseapower committed
307
308
309
310
311
lintCoreExpr e@(App _ _)
    = do { fun_ty <- lintCoreExpr fun
         ; addLoc (AnExpr e) $ foldM lintCoreArg fun_ty args }
  where
    (fun, args) = collectArgs e
312
313

lintCoreExpr (Lam var expr)
314
  = addLoc (LambdaBodyOf var) $
315
316
    lintBinder var $ \ var' ->
    do { body_ty <- lintCoreExpr expr
317
318
319
320
321
       ; if isId var' then 
             return (mkFunTy (idType var') body_ty) 
	 else
	     return (mkForAllTy var' body_ty)
       }
322
	-- The applySubstTy is needed to apply the subst to var
323
324
325
326

lintCoreExpr e@(Case scrut var alt_ty alts) =
       -- Check the scrutinee
  do { scrut_ty <- lintCoreExpr scrut
327
328
     ; alt_ty   <- lintInTy alt_ty  
     ; var_ty   <- lintInTy (idType var)	
329

330
331
     ; case tyConAppTyCon_maybe (idType var) of 
         Just tycon
332
333
              | debugIsOn &&
                isAlgTyCon tycon && 
334
		not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
335
                null (tyConDataCons tycon) -> 
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
336
337
                  pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
			-- This can legitimately happen for type families
338
339
340
                      $ return ()
         _otherwise -> return ()

341
	-- Don't use lintIdBndr on var, because unboxed tuple is legitimate
342

343
344
     ; subst <- getTvSubst 
     ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
345
346

     -- If the binder is an unboxed tuple type, don't put it in scope
347
348
349
350
     ; let scope = if (isUnboxedTupleType (idType var)) then 
                       pass_var 
                   else lintAndScopeId var
     ; scope $ \_ ->
351
       do { -- Check the alternatives
352
            mapM_ (lintCoreAlt scrut_ty alt_ty) alts
353
          ; checkCaseAlts e scrut_ty alts
354
          ; return alt_ty } }
355
356
  where
    pass_var f = f var
357

358
lintCoreExpr (Type ty)
359
  = do { ty' <- lintInTy ty
360
       ; return (typeKind ty') }
361
362
363
364

lintCoreExpr (Coercion co)
  = do { co' <- lintInCo co
       ; let Pair ty1 ty2 = coercionKind co'
batterseapower's avatar
batterseapower committed
365
       ; return (mkCoercionType ty1 ty2) }
366
\end{code}
367

dreixel's avatar
dreixel committed
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
Note [Kind instantiation in coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following coercion axiom:
  ax_co [(k_ag :: BOX), (f_aa :: k_ag -> Constraint)] :: T k_ag f_aa ~ f_aa

Consider the following instantiation:
  ax_co <* -> *> <Monad>

We need to split the co_ax_tvs into kind and type variables in order
to find out the coercion kind instantiations. Those can only be Refl
since we don't have kind coercions. This is just a way to represent
kind instantiation.

We use the number of kind variables to know how to split the coercions
instantiations between kind coercions and type coercions. We lint the
kind coercions and produce the following substitution which is to be
applied in the type variables:
  k_ag   ~~>   * -> *


388
389
390
391
392
%************************************************************************
%*									*
\subsection[lintCoreArgs]{lintCoreArgs}
%*									*
%************************************************************************
393

394
395
The basic version of these functions checks that the argument is a
subtype of the required type, as one would expect.
396

397
\begin{code}
398
lintCoreArg  :: OutType -> CoreArg -> LintM OutType
399
lintCoreArg fun_ty (Type arg_ty)
400
401
  = do { arg_ty' <- applySubstTy arg_ty
       ; lintTyApp fun_ty arg_ty' }
402
403

lintCoreArg fun_ty arg
404
405
  = do { arg_ty <- lintCoreExpr arg
       ; lintValApp arg fun_ty arg_ty }
406
407
408
409
410
411
412
413
414

-----------------
lintAltBinders :: OutType     -- Scrutinee type
	       -> OutType     -- Constructor type
               -> [OutVar]    -- Binders
               -> LintM ()
lintAltBinders scrut_ty con_ty [] 
  = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty) 
lintAltBinders scrut_ty con_ty (bndr:bndrs)
415
  | isTyVar bndr
416
417
418
419
420
421
422
423
424
425
  = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
       ; lintAltBinders scrut_ty con_ty' bndrs }
  | otherwise
  = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
       ; lintAltBinders scrut_ty con_ty' bndrs } 

-----------------
lintTyApp :: OutType -> OutType -> LintM OutType
lintTyApp fun_ty arg_ty
  | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
426
427
428
429
  , isTyVar tyvar
  = do	{ checkTyKind tyvar arg_ty
        ; return (substTyWith [tyvar] [arg_ty] body_ty) }

430
431
  | otherwise
  = failWithL (mkTyAppMsg fun_ty arg_ty)
432
433
434
435
436
437
438
439
440
441
442
443
   
-----------------
lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
lintValApp arg fun_ty arg_ty
  | Just (arg,res) <- splitFunTy_maybe fun_ty
  = do { checkTys arg arg_ty err1
       ; return res }
  | otherwise
  = failWithL err2
  where
    err1 = mkAppMsg       fun_ty arg_ty arg
    err2 = mkNonFunAppMsg fun_ty arg_ty arg
444
\end{code}
445

446
\begin{code}
447
checkTyKind :: OutTyVar -> OutType -> LintM ()
448
-- Both args have had substitution applied
449
checkTyKind tyvar arg_ty
dreixel's avatar
dreixel committed
450
451
  | isSuperKind tyvar_kind  -- kind forall
  = lintKind arg_ty
452
453
454
455
	-- 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.
dreixel's avatar
dreixel committed
456
  | otherwise  -- type forall
457
458
  = do { arg_kind <- lintType arg_ty
       ; unless (arg_kind `isSubKind` tyvar_kind)
459
                (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
460
461
  where
    tyvar_kind = tyVarKind tyvar
462

463
464
465
466
467
468
469
470
471
472
checkDeadIdOcc :: Id -> LintM ()
-- Occurrences of an Id should never be dead....
-- except when we are checking a case pattern
checkDeadIdOcc id
  | isDeadOcc (idOccInfo id)
  = do { in_case <- inCasePat
       ; checkL in_case
		(ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
  | otherwise
  = return ()
473
\end{code}
474
475


476
477
478
479
480
481
482
%************************************************************************
%*									*
\subsection[lintCoreAlts]{lintCoreAlts}
%*									*
%************************************************************************

\begin{code}
483
checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
484
-- a) Check that the alts are non-empty
485
486
-- b1) Check that the DEFAULT comes first, if it exists
-- b2) Check that the others are in increasing order
487
488
489
490
491
-- 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.

twanvl's avatar
twanvl committed
492
checkCaseAlts e _ []
493
494
  = addErrL (mkNullAltsMsg e)

495
496
checkCaseAlts e ty alts = 
  do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
497
     ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
498
499
     ; checkL (isJust maybe_deflt || not is_infinite_ty)
	   (nonExhaustiveAltsMsg e) }
500
501
  where
    (con_alts, maybe_deflt) = findDefault alts
502

503
504
	-- Check that successive alternatives have increasing tags 
    increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
twanvl's avatar
twanvl committed
505
    increasing_tag _                         = True
506

507
    non_deflt (DEFAULT, _, _) = False
twanvl's avatar
twanvl committed
508
    non_deflt _               = True
509

510
511
512
    is_infinite_ty = case tyConAppTyCon_maybe ty of
                        Nothing    -> False
                        Just tycon -> isPrimTyCon tycon
513
514
515
\end{code}

\begin{code}
516
517
checkAltExpr :: CoreExpr -> OutType -> LintM ()
checkAltExpr expr ann_ty
518
  = do { actual_ty <- lintCoreExpr expr 
519
       ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
520

521
522
lintCoreAlt :: OutType 		-- Type of scrutinee
            -> OutType          -- Type of the alternative
523
	    -> CoreAlt
524
	    -> LintM ()
525

twanvl's avatar
twanvl committed
526
lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
527
528
  do { checkL (null args) (mkDefaultArgsMsg args)
     ; checkAltExpr rhs alt_ty }
529

530
lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
531
532
  | litIsLifted lit
  = failWithL integerScrutinisedMsg
533
  | otherwise
534
535
536
  = do { checkL (null args) (mkDefaultArgsMsg args)
       ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
       ; checkAltExpr rhs alt_ty }
537
538
  where
    lit_ty = literalType lit
539

540
lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
541
542
  | isNewTyCon (dataConTyCon con) 
  = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
543
  | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
544
545
546
  = addLoc (CaseAlt alt) $  do
    {   -- First instantiate the universally quantified 
	-- type variables of the data constructor
547
548
549
	-- We've already check
      checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
    ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
550
551

	-- And now bring the new binders into scope
552
553
    ; lintBinders args $ \ args' -> do
    { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
554
    ; checkAltExpr rhs alt_ty } }
555
556
557

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

sof's avatar
sof committed
560
561
%************************************************************************
%*									*
562
\subsection[lint-types]{Types}
sof's avatar
sof committed
563
564
565
566
%*									*
%************************************************************************

\begin{code}
567
568
569
570
571
572
573
574
575
576
577
578
-- 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
579
580
581
582
583
584
  | isId var  = lintIdBndr var linterF
  | otherwise = lintTyBndr var linterF

lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
lintTyBndr tv thing_inside
  = do { subst <- getTvSubst
585
       ; let (subst', tv') = Type.substTyVarBndr subst tv
586
587
       ; lintTyBndrKind tv'
       ; updateTvSubst subst' (thing_inside tv') }
588

589
lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
590
591
-- 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
592
-- ToDo: lint its rules
593

594
lintIdBndr id linterF 
595
596
597
  = do 	{ checkL (not (isUnboxedTupleType (idType id))) 
		 (mkUnboxedTupleMsg id)
		-- No variable can be bound to an unboxed tuple.
598
        ; lintAndScopeId id $ \id' -> linterF id' }
599
600
601
602
603
604

lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
lintAndScopeIds ids linterF 
  = go ids
  where
    go []       = linterF []
605
606
607
    go (id:ids) = lintAndScopeId id $ \id ->
                  lintAndScopeIds ids $ \ids ->
                  linterF (id:ids)
608

609
lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
610
lintAndScopeId id linterF 
611
  = do { ty <- lintInTy (idType id)
612
       ; let id' = setIdType id ty
613
614
615
616
617
618
       ; addInScopeVar id' $ (linterF id') }
\end{code}


%************************************************************************
%*									*
619
             Types and kinds
620
621
%*									*
%************************************************************************
622

623
624
625
626
We have a single linter for types and kinds.  That is convenient
because sometimes it's not clear whether the thing we are looking
at is a type or a kind.

627
\begin{code}
628
629
lintInTy :: InType -> LintM LintedType
-- Types only, not kinds
630
-- Check the type, and apply the substitution to it
631
-- See Note [Linting type lets]
632
633
lintInTy ty 
  = addLoc (InType ty) $
634
    do	{ ty' <- applySubstTy ty
635
	; _k  <- lintType ty'
636
	; return ty' }
sof's avatar
sof committed
637

638
639
-------------------
lintTyBndrKind :: OutTyVar -> LintM ()
dreixel's avatar
dreixel committed
640
-- Handles both type and kind foralls.
641
lintTyBndrKind tv = lintKind (tyVarKind tv)
642

643
-------------------
644
lintType :: OutType -> LintM LintedKind
645
646
647
-- The returned Kind has itself been linted
lintType (TyVarTy tv)
  = do { checkTyCoVarInScope tv
648
649
       ; return (tyVarKind tv) }
         -- We checked its kind when we added it to the envt
650
651
652

lintType ty@(AppTy t1 t2) 
  = do { k1 <- lintType t1
653
654
       ; k2 <- lintType t2
       ; lint_ty_app ty k1 [(t2,k2)] }
655

656
657
658
659
lintType ty@(FunTy t1 t2)    -- (->) has two different rules, for types and kinds
  = do { k1 <- lintType t1
       ; k2 <- lintType t2
       ; lintArrow (ptext (sLit "type or kind") <+> quotes (ppr ty)) k1 k2 }
660
661

lintType ty@(TyConApp tc tys)
662
  | not (isUnLiftedTyCon tc) || tys `lengthIs` tyConArity tc
663
664
       -- Check that primitive types are saturated
       -- See Note [The kind invariant] in TypeRep
665
666
  = do { ks <- mapM lintType tys
       ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
667
668
669
670
671
672
  | otherwise
  = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))

lintType (ForAllTy tv ty)
  = do { lintTyBndrKind tv
       ; addInScopeVar tv (lintType ty) }
673
\end{code}
674

675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701

\begin{code}
lintKind :: OutKind -> LintM ()
lintKind k = do { sk <- lintType k 
                ; unless (isSuperKind sk) 
                         (addErrL (hang (ptext (sLit "Ill-kinded kind:") <+> ppr k)
                                      2 (ptext (sLit "has kind:") <+> ppr sk))) }
\end{code}


\begin{code}
lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
lintArrow what k1 k2   -- Eg lintArrow "type or kind `blah'" k1 k2
                       -- or lintarrow "coercion `blah'" k1 k2
  | isSuperKind k1 
  = return superKind
  | otherwise
  = do { unless (k1 `isSubKind` argTypeKind)  (addErrL (msg (ptext (sLit "argument")) k1))
       ; unless (k2 `isSubKind` openTypeKind) (addErrL (msg (ptext (sLit "result"))   k2))
       ; return liftedTypeKind }
  where
    msg ar k
      = vcat [ hang (ptext (sLit "Ill-kinded") <+> ar)
                  2 (ptext (sLit "in") <+> what)
             , what <+> ptext (sLit "kind:") <+> ppr k ]

lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
702
lint_ty_app ty k tys 
703
  = lint_app (ptext (sLit "type") <+> quotes (ppr ty)) k tys
704
705

----------------
706
lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
707
lint_co_app ty k tys 
708
  = lint_app (ptext (sLit "coercion") <+> quotes (ppr ty)) k tys
709
710

----------------
711
712
lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
-- (lint_app d fun_kind arg_tys)
713
714
715
--    We have an application (f arg_ty1 .. arg_tyn),
--    where f :: fun_kind
-- Takes care of linting the OutTypes
716
717
lint_app doc kfn kas
    = foldlM go_app kfn kas
718
719
720
  where
    fail_msg = vcat [ hang (ptext (sLit "Kind application error in")) 2 doc
                    , nest 2 (ptext (sLit "Function kind =") <+> ppr kfn)
721
722
723
724
725
726
727
728
729
730
731
732
733
                    , nest 2 (ptext (sLit "Arg kinds =") <+> ppr kas) ]

    go_app kfn ka
      | Just kfn' <- coreView kfn
      = go_app kfn' ka

    go_app (FunTy kfa kfb) (_,ka)
      = do { unless (ka `isSubKind` kfa) (addErrL fail_msg)
           ; return kfb }

    go_app (ForAllTy kv kfn) (ta,ka)
      = do { unless (ka `isSubKind` tyVarKind kv) (addErrL fail_msg)
           ; return (substKiWith [kv] [ta] kfn) }
734

735
    go_app _ _ = failWithL fail_msg
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
\end{code}

%************************************************************************
%*									*
         Linting coercions
%*									*
%************************************************************************

\begin{code}
lintInCo :: InCoercion -> LintM OutCoercion
-- Check the coercion, and apply the substitution to it
-- See Note [Linting type lets]
lintInCo co
  = addLoc (InCo co) $
    do  { co' <- applySubstCo co
        ; _   <- lintCoercion co'
        ; return co' }

754
lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType)
755
-- Check the kind of a coercion term, returning the kind
756
757
-- Post-condition: the returned OutTypes are lint-free
--                 and have the same kind as each other
758
lintCoercion (Refl ty)
759
760
  = do { k <- lintType ty
       ; return (k, ty, ty) }
761

762
lintCoercion co@(TyConAppCo tc cos)
763
764
765
766
767
768
  | tc `hasKey` funTyConKey
  , [co1,co2] <- cos
  = do { (k1,s1,t1) <- lintCoercion co1
       ; (k2,s2,t2) <- lintCoercion co2
       ; rk <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k1 k2
       ; return (rk, mkFunTy s1 s2, mkFunTy t1 t2) }
769

770
771
772
773
  | otherwise
  = do { (ks,ss,ts) <- mapAndUnzip3M lintCoercion cos
       ; rk <- lint_co_app co (tyConKind tc) (ss `zip` ks)
       ; return (rk, mkTyConApp tc ss, mkTyConApp tc ts) }
774

775
lintCoercion co@(AppCo co1 co2)
776
777
778
779
780
781
782
783
784
  = do { (k1,s1,t1) <- lintCoercion co1
       ; (k2,s2,t2) <- lintCoercion co2
       ; rk <- lint_co_app co k1 [(s2,k2)]
       ; return (rk, mkAppTy s1 s2, mkAppTy t1 t2) }

lintCoercion (ForAllCo tv co)
  = do { lintTyBndrKind tv
       ; (k, s, t) <- addInScopeVar tv (lintCoercion co)
       ; return (k, mkForAllTy tv s, mkForAllTy tv t) }
785

786
lintCoercion (CoVarCo cv)
batterseapower's avatar
batterseapower committed
787
788
789
790
  | not (isCoVar cv)
  = failWithL (hang (ptext (sLit "Bad CoVarCo:") <+> ppr cv)
                  2 (ptext (sLit "With offending type:") <+> ppr (varType cv)))
  | otherwise
791
  = do { checkTyCoVarInScope cv
792
       ; cv' <- lookupIdInScope cv 
793
794
       ; let (s,t) = coVarKind cv'
       ; return (typeKind s, s, t) }
795
796

lintCoercion (UnsafeCo ty1 ty2)
797
798
799
800
801
802
  = do { k1 <- lintType ty1
       ; _k2 <- lintType ty2
--       ; unless (k1 `eqKind` k2) $ 
--         failWithL (hang (ptext (sLit "Unsafe coercion changes kind"))
--                       2 (ppr co))
       ; return (k1, ty1, ty2) }
803
804

lintCoercion (SymCo co) 
805
806
  = do { (k, ty1, ty2) <- lintCoercion co
       ; return (k, ty2, ty1) }
807
808

lintCoercion co@(TransCo co1 co2)
809
810
  = do { (k1, ty1a, ty1b) <- lintCoercion co1
       ; (_,  ty2a, ty2b) <- lintCoercion co2
811
       ; checkL (ty1b `eqType` ty2a)
812
813
                (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
                    2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
       ; return (k1, ty1a, ty2b) }

lintCoercion the_co@(NthCo n co)
  = do { (_,s,t) <- lintCoercion co
       ; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
           (Just (tc_s, tys_s), Just (tc_t, tys_t)) 
             | tc_s == tc_t
             , tys_s `equalLength` tys_t
             , n < length tys_s
             -> return (ks, ts, tt)
             where
               ts = tys_s !! n
               tt = tys_t !! n
               ks = typeKind ts

           _ -> failWithL (hang (ptext (sLit "Bad getNth:"))
                              2 (ppr the_co $$ ppr s $$ ppr t)) }
831
832

lintCoercion (InstCo co arg_ty)
833
834
835
836
  = do { (k,s,t)  <- lintCoercion co
       ; arg_kind <- lintType arg_ty
       ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
          (Just (tv1,ty1), Just (tv2,ty2))
837
            | arg_kind `isSubKind` tyVarKind tv1
838
839
            -> return (k, substTyWith [tv1] [arg_ty] ty1, 
                          substTyWith [tv2] [arg_ty] ty2) 
840
841
            | otherwise
            -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
	  _ -> failWithL (ptext (sLit "Bad argument of inst")) }

lintCoercion co@(AxiomInstCo (CoAxiom { co_ax_tvs = ktvs
                                      , co_ax_lhs = lhs
                                      , co_ax_rhs = rhs })
                             cos)
  = do {  -- See Note [Kind instantiation in coercions]
         let (kvs, tvs)   = splitKiTyVars ktvs
             (kcos, tcos) = splitAt (length kvs) cos
       ; unless (not (any isKiVar tvs)
                 && kvs `equalLength` kcos 
                 && tvs `equalLength` tcos) (bad_ax (ptext (sLit "lengths")))

       ; kis <- mapM check_ki kcos
       ; let tvs' = map (updateTyVarKind (Type.substTy subst)) tvs
             subst = zipOpenTvSubst kvs kis
       ; (tks, tys1, tys2) <- mapAndUnzip3M lintCoercion tcos

       ; zipWithM_ check_ki2 tvs' tks
       ; let lhs' = substTyWith ktvs (kis ++ tys1) lhs
             rhs' = substTyWith ktvs (kis ++ tys2) rhs

       ; return (typeKind lhs', lhs', rhs') }
  where
    bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what)
                        2 (ppr co))
    check_ki co
      = do { (k, k1, k2) <- lintCoercion co
           ; unless (isSuperKind k)  (bad_ax (ptext (sLit "check_ki1a")))
           ; unless (k1 `eqKind` k2) (bad_ax (ptext (sLit "check_ki1b")))
           ; return k1 }   -- Kind coercions must be refl

    check_ki2 tv k = unless (k `isSubKind` tyVarKind tv) 
                            (bad_ax (ptext (sLit "check_ki2")))
876
\end{code}
dreixel's avatar
dreixel committed
877

878
879
880
881
882
883
884
%************************************************************************
%*									*
\subsection[lint-monad]{The Lint monad}
%*									*
%************************************************************************

\begin{code}
885
886
887
888
889
890
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
891
892
893
	    WarnsAndErrs ->           -- Error and warning messages so far
	    (Maybe a, WarnsAndErrs) } -- Result and messages (if any)

894
type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)
895

896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
{-	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.
-}

911
instance Monad LintM where
twanvl's avatar
twanvl committed
912
  return x = LintM (\ _   _     errs -> (Just x, errs))
913
  fail err = failWithL (text err)
914
915
916
917
918
  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'))
919
920

data LintLocInfo
921
922
923
  = RhsOf Id		-- The variable bound
  | LambdaBodyOf Id	-- The lambda-binder
  | BodyOfLetRec [Id]	-- One of the binders
924
  | CaseAlt CoreAlt	-- Case alternative
Thomas Schilling's avatar
Thomas Schilling committed
925
  | CasePat CoreAlt	-- The *pattern* of the case alternative
926
927
  | AnExpr CoreExpr	-- Some expression
  | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
928
  | TopLevelBindings
929
  | InType Type		-- Inside a type
930
  | InCo   Coercion     -- Inside a coercion
931
932
\end{code}

933
                 
934
\begin{code}
935
initL :: LintM a -> WarnsAndErrs    -- Errors and warnings
936
initL m
937
938
  = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
      (_, errs) -> errs
939
940
941
\end{code}

\begin{code}
942
checkL :: Bool -> MsgDoc -> LintM ()
twanvl's avatar
twanvl committed
943
checkL True  _   = return ()
944
945
checkL False msg = failWithL msg

946
failWithL :: MsgDoc -> LintM a
947
948
failWithL msg = LintM $ \ loc subst (warns,errs) ->
                (Nothing, (warns, addMsg subst errs msg loc))
sof's avatar
sof committed
949

950
addErrL :: MsgDoc -> LintM ()
951
952
addErrL msg = LintM $ \ loc subst (warns,errs) -> 
              (Just (), (warns, addMsg subst errs msg loc))
953

954
addWarnL :: MsgDoc -> LintM ()
955
956
957
addWarnL msg = LintM $ \ loc subst (warns,errs) -> 
              (Just (), (addMsg subst warns msg loc, errs))

958
addMsg :: TvSubst ->  Bag MsgDoc -> MsgDoc -> [LintLocInfo] -> Bag MsgDoc
959
addMsg subst msgs msg locs
sof's avatar
sof committed
960
  = ASSERT( notNull locs )
961
    msgs `snocBag` mk_msg msg
sof's avatar
sof committed
962
  where
963
964
   (loc, cxt1) = dumpLoc (head locs)
   cxts        = [snd (dumpLoc loc) | loc <- locs]   
965
   context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
Ian Lynagh's avatar
Ian Lynagh committed
966
				      ptext (sLit "Substitution:") <+> ppr subst
967
968
	       | otherwise	    = cxt1
 
969
   mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
970
971

addLoc :: LintLocInfo -> LintM a -> LintM a
972
973
addLoc extra_loc m =
  LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
974

975
976
977
978
979
980
inCasePat :: LintM Bool		-- A slight hack; see the unique call site
inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
  where
    is_case_pat (CasePat {} : _) = True
    is_case_pat _other           = False

981
addInScopeVars :: [Var] -> LintM a -> LintM a
982
addInScopeVars vars m
983
  = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
984

985
986
987
988
addInScopeVar :: Var -> LintM a -> LintM a
addInScopeVar var m
  = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)

989
990
updateTvSubst :: TvSubst -> LintM a -> LintM a
updateTvSubst subst' m = 
twanvl's avatar
twanvl committed
991
  LintM (\ loc _ errs -> unLintM m loc subst' errs)
992
993

getTvSubst :: LintM TvSubst
twanvl's avatar
twanvl committed
994
getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
995

996
applySubstTy :: InType -> LintM OutType
997
998
applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }

999
applySubstCo :: InCoercion -> LintM OutCoercion
1000
applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
1001
1002
1003

extendSubstL :: TyVar -> Type -> LintM a -> LintM a
extendSubstL tv ty m
1004
  = LintM (\ loc subst errs -> unLintM m loc (Type.extendTvSubst subst tv ty) errs)
1005
1006
1007
\end{code}

\begin{code}
1008
1009
1010
1011
1012
1013
1014
1015
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
1016
		Nothing -> do { addErrL out_of_scope
1017
1018
			      ; return id } }
  where
Ian Lynagh's avatar
Ian Lynagh committed
1019
    out_of_scope = ppr id <+> ptext (sLit "is out of scope")
1020

1021
1022

oneTupleDataConId :: Id	-- Should not happen
batterseapower's avatar
batterseapower committed
1023
oneTupleDataConId = dataConWorkId (tupleCon BoxedTuple 1)
sof's avatar
sof committed
1024

1025
checkBndrIdInScope :: Var -> Var -> LintM ()
1026
checkBndrIdInScope binder id 
sof's avatar
sof committed
1027
1028
  = checkInScope msg id
    where
Ian Lynagh's avatar
Ian Lynagh committed
1029
     msg = ptext (sLit "is out of scope inside info for") <+> 
sof's avatar
sof committed
1030
1031
	   ppr binder

1032
checkTyCoVarInScope :: Var -> LintM ()
1033
checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
1034

1035
checkInScope :: SDoc -> Var -> LintM ()
1036
1037
1038
1039
checkInScope loc_msg var =
 do { subst <- getTvSubst
    ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
             (hsep [ppr var, loc_msg]) }
sof's avatar
sof committed
1040

1041
checkTys :: OutType -> OutType -> MsgDoc -> LintM ()
1042
1043
-- check ty2 is subtype of ty1 (ie, has same structure but usage
-- annotations need only be consistent, not equal)
1044
-- Assumes ty1,ty2 are have alrady had the substitution applied
1045
checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
1046
1047
\end{code}

1048
1049
1050
1051
1052
1053
%************************************************************************
%*									*
\subsection{Error messages}
%*									*
%************************************************************************

1054
\begin{code}
twanvl's avatar
twanvl committed
1055
1056
dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)

sof's avatar
sof committed
1057
dumpLoc (RhsOf v)
Ian Lynagh's avatar
Ian Lynagh committed
1058
  = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
1059

sof's avatar
sof committed
1060
dumpLoc (LambdaBodyOf b)
Ian Lynagh's avatar
Ian Lynagh committed
1061
  = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
sof's avatar
sof committed
1062

1063
dumpLoc (BodyOfLetRec [])
Ian Lynagh's avatar
Ian Lynagh committed
1064
  = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
1065
1066

dumpLoc (BodyOfLetRec bs@(_:_))
Ian Lynagh's avatar
Ian Lynagh committed
1067
  = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
1068

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