Annotation linting
[ghc.git] / compiler / coreSyn / CoreLint.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
4
5
6 A ``lint'' pass to check for Core correctness
7 -}
8
9 {-# LANGUAGE CPP #-}
10 {-# OPTIONS_GHC -fprof-auto #-}
11
12 module CoreLint (
13 lintCoreBindings, lintUnfolding,
14 lintPassResult, lintInteractiveExpr, lintExpr,
15 lintAnnots,
16
17 -- ** Debug output
18 CoreLint.showPass, showPassIO, endPass, endPassIO,
19 dumpPassResult,
20 CoreLint.dumpIfSet,
21 ) where
22
23 #include "HsVersions.h"
24
25 import CoreSyn
26 import CoreFVs
27 import CoreUtils
28 import CoreMonad
29 import Bag
30 import Literal
31 import DataCon
32 import TysWiredIn
33 import TysPrim
34 import Var
35 import VarEnv
36 import VarSet
37 import Name
38 import Id
39 import PprCore
40 import ErrUtils
41 import Coercion
42 import SrcLoc
43 import Kind
44 import Type
45 import TypeRep
46 import TyCon
47 import CoAxiom
48 import BasicTypes
49 import ErrUtils as Err
50 import StaticFlags
51 import ListSetOps
52 import PrelNames
53 import Outputable
54 import FastString
55 import Util
56 import InstEnv ( instanceDFunId )
57 import OptCoercion ( checkAxInstCo )
58 import UniqSupply
59
60 import HscTypes
61 import DynFlags
62 import Control.Monad
63 import MonadUtils
64 import Data.Maybe
65 import Pair
66
67 {-
68 Note [GHC Formalism]
69 ~~~~~~~~~~~~~~~~~~~~
70 This file implements the type-checking algorithm for System FC, the "official"
71 name of the Core language. Type safety of FC is heart of the claim that
72 executables produced by GHC do not have segmentation faults. Thus, it is
73 useful to be able to reason about System FC independently of reading the code.
74 To this purpose, there is a document ghc.pdf built in docs/core-spec that
75 contains a formalism of the types and functions dealt with here. If you change
76 just about anything in this file or you change other types/functions throughout
77 the Core language (all signposted to this note), you should update that
78 formalism. See docs/core-spec/README for more info about how to do so.
79
80 Summary of checks
81 ~~~~~~~~~~~~~~~~~
82 Checks that a set of core bindings is well-formed. The PprStyle and String
83 just control what we print in the event of an error. The Bool value
84 indicates whether we have done any specialisation yet (in which case we do
85 some extra checks).
86
87 We check for
88 (a) type errors
89 (b) Out-of-scope type variables
90 (c) Out-of-scope local variables
91 (d) Ill-kinded types
92
93 If we have done specialisation the we check that there are
94 (a) No top-level bindings of primitive (unboxed type)
95
96 Outstanding issues:
97
98 -- Things are *not* OK if:
99 --
100 -- * Unsaturated type app before specialisation has been done;
101 --
102 -- * Oversaturated type app after specialisation (eta reduction
103 -- may well be happening...);
104
105
106 Note [Linting type lets]
107 ~~~~~~~~~~~~~~~~~~~~~~~~
108 In the desugarer, it's very very convenient to be able to say (in effect)
109 let a = Type Int in <body>
110 That is, use a type let. See Note [Type let] in CoreSyn.
111
112 However, when linting <body> we need to remember that a=Int, else we might
113 reject a correct program. So we carry a type substitution (in this example
114 [a -> Int]) and apply this substitution before comparing types. The functin
115 lintInTy :: Type -> LintM Type
116 returns a substituted type; that's the only reason it returns anything.
117
118 When we encounter a binder (like x::a) we must apply the substitution
119 to the type of the binding variable. lintBinders does this.
120
121 For Ids, the type-substituted Id is added to the in_scope set (which
122 itself is part of the TvSubst we are carrying down), and when we
123 find an occurrence of an Id, we fetch it from the in-scope set.
124
125 ************************************************************************
126 * *
127 Beginning and ending passes
128 * *
129 ************************************************************************
130
131 These functions are not CoreM monad stuff, but they probably ought to
132 be, and it makes a conveneint place. place for them. They print out
133 stuff before and after core passes, and do Core Lint when necessary.
134 -}
135
136 showPass :: CoreToDo -> CoreM ()
137 showPass pass = do { dflags <- getDynFlags
138 ; liftIO $ showPassIO dflags pass }
139
140 showPassIO :: DynFlags -> CoreToDo -> IO ()
141 showPassIO dflags pass = Err.showPass dflags (showPpr dflags pass)
142
143 endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> CoreM ()
144 endPass pass binds rules
145 = do { hsc_env <- getHscEnv
146 ; print_unqual <- getPrintUnqualified
147 ; liftIO $ endPassIO hsc_env print_unqual pass binds rules }
148
149 endPassIO :: HscEnv -> PrintUnqualified
150 -> CoreToDo -> CoreProgram -> [CoreRule] -> IO ()
151 -- Used by the IO-is CorePrep too
152 endPassIO hsc_env print_unqual pass binds rules
153 = do { dumpPassResult dflags print_unqual mb_flag
154 (ppr pass) (pprPassDetails pass) binds rules
155 ; lintPassResult hsc_env pass binds }
156 where
157 dflags = hsc_dflags hsc_env
158 mb_flag = case coreDumpFlag pass of
159 Just flag | dopt flag dflags -> Just flag
160 | dopt Opt_D_verbose_core2core dflags -> Just flag
161 _ -> Nothing
162
163 dumpIfSet :: DynFlags -> Bool -> CoreToDo -> SDoc -> SDoc -> IO ()
164 dumpIfSet dflags dump_me pass extra_info doc
165 = Err.dumpIfSet dflags dump_me (showSDoc dflags (ppr pass <+> extra_info)) doc
166
167 dumpPassResult :: DynFlags
168 -> PrintUnqualified
169 -> Maybe DumpFlag -- Just df => show details in a file whose
170 -- name is specified by df
171 -> SDoc -- Header
172 -> SDoc -- Extra info to appear after header
173 -> CoreProgram -> [CoreRule]
174 -> IO ()
175 dumpPassResult dflags unqual mb_flag hdr extra_info binds rules
176 | Just flag <- mb_flag
177 = Err.dumpSDoc dflags unqual flag (showSDoc dflags hdr) dump_doc
178
179 | otherwise
180 = Err.debugTraceMsg dflags 2 size_doc
181 -- Report result size
182 -- This has the side effect of forcing the intermediate to be evaluated
183
184 where
185 size_doc = sep [text "Result size of" <+> hdr, nest 2 (equals <+> ppr (coreBindsStats binds))]
186
187 dump_doc = vcat [ nest 2 extra_info
188 , size_doc
189 , blankLine
190 , pprCoreBindings binds
191 , ppUnless (null rules) pp_rules ]
192 pp_rules = vcat [ blankLine
193 , ptext (sLit "------ Local rules for imported ids --------")
194 , pprRules rules ]
195
196 coreDumpFlag :: CoreToDo -> Maybe DumpFlag
197 coreDumpFlag (CoreDoSimplify {}) = Just Opt_D_verbose_core2core
198 coreDumpFlag (CoreDoPluginPass {}) = Just Opt_D_verbose_core2core
199 coreDumpFlag CoreDoFloatInwards = Just Opt_D_verbose_core2core
200 coreDumpFlag (CoreDoFloatOutwards {}) = Just Opt_D_verbose_core2core
201 coreDumpFlag CoreLiberateCase = Just Opt_D_verbose_core2core
202 coreDumpFlag CoreDoStaticArgs = Just Opt_D_verbose_core2core
203 coreDumpFlag CoreDoCallArity = Just Opt_D_dump_call_arity
204 coreDumpFlag CoreDoStrictness = Just Opt_D_dump_stranal
205 coreDumpFlag CoreDoWorkerWrapper = Just Opt_D_dump_worker_wrapper
206 coreDumpFlag CoreDoSpecialising = Just Opt_D_dump_spec
207 coreDumpFlag CoreDoSpecConstr = Just Opt_D_dump_spec
208 coreDumpFlag CoreCSE = Just Opt_D_dump_cse
209 coreDumpFlag CoreDoVectorisation = Just Opt_D_dump_vect
210 coreDumpFlag CoreDesugar = Just Opt_D_dump_ds
211 coreDumpFlag CoreDesugarOpt = Just Opt_D_dump_ds
212 coreDumpFlag CoreTidy = Just Opt_D_dump_simpl
213 coreDumpFlag CorePrep = Just Opt_D_dump_prep
214
215 coreDumpFlag CoreDoPrintCore = Nothing
216 coreDumpFlag (CoreDoRuleCheck {}) = Nothing
217 coreDumpFlag CoreDoNothing = Nothing
218 coreDumpFlag (CoreDoPasses {}) = Nothing
219
220 {-
221 ************************************************************************
222 * *
223 Top-level interfaces
224 * *
225 ************************************************************************
226 -}
227
228 lintPassResult :: HscEnv -> CoreToDo -> CoreProgram -> IO ()
229 lintPassResult hsc_env pass binds
230 | not (gopt Opt_DoCoreLinting dflags)
231 = return ()
232 | otherwise
233 = do { let (warns, errs) = lintCoreBindings pass (interactiveInScope hsc_env) binds
234 ; Err.showPass dflags ("Core Linted result of " ++ showPpr dflags pass)
235 ; displayLintResults dflags pass warns errs binds }
236 where
237 dflags = hsc_dflags hsc_env
238
239 displayLintResults :: DynFlags -> CoreToDo
240 -> Bag Err.MsgDoc -> Bag Err.MsgDoc -> CoreProgram
241 -> IO ()
242 displayLintResults dflags pass warns errs binds
243 | not (isEmptyBag errs)
244 = do { log_action dflags dflags Err.SevDump noSrcSpan defaultDumpStyle
245 (vcat [ lint_banner "errors" (ppr pass), Err.pprMessageBag errs
246 , ptext (sLit "*** Offending Program ***")
247 , pprCoreBindings binds
248 , ptext (sLit "*** End of Offense ***") ])
249 ; Err.ghcExit dflags 1 }
250
251 | not (isEmptyBag warns)
252 , not (case pass of { CoreDesugar -> True; _ -> False })
253 -- Suppress warnings after desugaring pass because some
254 -- are legitimate. Notably, the desugarer generates instance
255 -- methods with INLINE pragmas that form a mutually recursive
256 -- group. Only afer a round of simplification are they unravelled.
257 , not opt_NoDebugOutput
258 , showLintWarnings pass
259 = log_action dflags dflags Err.SevDump noSrcSpan defaultDumpStyle
260 (lint_banner "warnings" (ppr pass) $$ Err.pprMessageBag warns)
261
262 | otherwise = return ()
263 where
264
265 lint_banner :: String -> SDoc -> SDoc
266 lint_banner string pass = ptext (sLit "*** Core Lint") <+> text string
267 <+> ptext (sLit ": in result of") <+> pass
268 <+> ptext (sLit "***")
269
270 showLintWarnings :: CoreToDo -> Bool
271 -- Disable Lint warnings on the first simplifier pass, because
272 -- there may be some INLINE knots still tied, which is tiresomely noisy
273 showLintWarnings (CoreDoSimplify _ (SimplMode { sm_phase = InitialPhase })) = False
274 showLintWarnings _ = True
275
276 lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO ()
277 lintInteractiveExpr what hsc_env expr
278 | not (gopt Opt_DoCoreLinting dflags)
279 = return ()
280 | Just err <- lintExpr (interactiveInScope hsc_env) expr
281 = do { display_lint_err err
282 ; Err.ghcExit dflags 1 }
283 | otherwise
284 = return ()
285 where
286 dflags = hsc_dflags hsc_env
287
288 display_lint_err err
289 = do { log_action dflags dflags Err.SevDump noSrcSpan defaultDumpStyle
290 (vcat [ lint_banner "errors" (text what)
291 , err
292 , ptext (sLit "*** Offending Program ***")
293 , pprCoreExpr expr
294 , ptext (sLit "*** End of Offense ***") ])
295 ; Err.ghcExit dflags 1 }
296
297 interactiveInScope :: HscEnv -> [Var]
298 -- In GHCi we may lint expressions, or bindings arising from 'deriving'
299 -- clauses, that mention variables bound in the interactive context.
300 -- These are Local things (see Note [Interactively-bound Ids in GHCi] in HscTypes).
301 -- So we have to tell Lint about them, lest it reports them as out of scope.
302 --
303 -- We do this by find local-named things that may appear free in interactive
304 -- context. This function is pretty revolting and quite possibly not quite right.
305 -- When we are not in GHCi, the interactive context (hsc_IC hsc_env) is empty
306 -- so this is a (cheap) no-op.
307 --
308 -- See Trac #8215 for an example
309 interactiveInScope hsc_env
310 = varSetElems tyvars ++ ids
311 where
312 -- C.f. TcRnDriver.setInteractiveContext, Desugar.deSugarExpr
313 ictxt = hsc_IC hsc_env
314 (cls_insts, _fam_insts) = ic_instances ictxt
315 te1 = mkTypeEnvWithImplicits (ic_tythings ictxt)
316 te = extendTypeEnvWithIds te1 (map instanceDFunId cls_insts)
317 ids = typeEnvIds te
318 tyvars = mapUnionVarSet (tyVarsOfType . idType) ids
319 -- Why the type variables? How can the top level envt have free tyvars?
320 -- I think it's because of the GHCi debugger, which can bind variables
321 -- f :: [t] -> [t]
322 -- where t is a RuntimeUnk (see TcType)
323
324 lintCoreBindings :: CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
325 -- Returns (warnings, errors)
326 -- If you edit this function, you may need to update the GHC formalism
327 -- See Note [GHC Formalism]
328 lintCoreBindings pass local_in_scope binds
329 = initL flags $
330 addLoc TopLevelBindings $
331 addInScopeVars local_in_scope $
332 addInScopeVars binders $
333 -- Put all the top-level binders in scope at the start
334 -- This is because transformation rules can bring something
335 -- into use 'unexpectedly'
336 do { checkL (null dups) (dupVars dups)
337 ; checkL (null ext_dups) (dupExtVars ext_dups)
338 ; mapM lint_bind binds }
339 where
340 flags = LF { lf_check_global_ids = check_globals }
341
342 -- See Note [Checking for global Ids]
343 check_globals = case pass of
344 CoreTidy -> False
345 CorePrep -> False
346 _ -> True
347
348 binders = bindersOfBinds binds
349 (_, dups) = removeDups compare binders
350
351 -- dups_ext checks for names with different uniques
352 -- but but the same External name M.n. We don't
353 -- allow this at top level:
354 -- M.n{r3} = ...
355 -- M.n{r29} = ...
356 -- because they both get the same linker symbol
357 ext_dups = snd (removeDups ord_ext (map Var.varName binders))
358 ord_ext n1 n2 | Just m1 <- nameModule_maybe n1
359 , Just m2 <- nameModule_maybe n2
360 = compare (m1, nameOccName n1) (m2, nameOccName n2)
361 | otherwise = LT
362
363 -- If you edit this function, you may need to update the GHC formalism
364 -- See Note [GHC Formalism]
365 lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
366 lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
367
368 {-
369 ************************************************************************
370 * *
371 \subsection[lintUnfolding]{lintUnfolding}
372 * *
373 ************************************************************************
374
375 We use this to check all unfoldings that come in from interfaces
376 (it is very painful to catch errors otherwise):
377 -}
378
379 lintUnfolding :: SrcLoc
380 -> [Var] -- Treat these as in scope
381 -> CoreExpr
382 -> Maybe MsgDoc -- Nothing => OK
383
384 lintUnfolding locn vars expr
385 | isEmptyBag errs = Nothing
386 | otherwise = Just (pprMessageBag errs)
387 where
388 (_warns, errs) = initL defaultLintFlags linter
389 linter = addLoc (ImportedUnfolding locn) $
390 addInScopeVars vars $
391 lintCoreExpr expr
392
393 lintExpr :: [Var] -- Treat these as in scope
394 -> CoreExpr
395 -> Maybe MsgDoc -- Nothing => OK
396
397 lintExpr vars expr
398 | isEmptyBag errs = Nothing
399 | otherwise = Just (pprMessageBag errs)
400 where
401 (_warns, errs) = initL defaultLintFlags linter
402 linter = addLoc TopLevelBindings $
403 addInScopeVars vars $
404 lintCoreExpr expr
405
406 {-
407 ************************************************************************
408 * *
409 \subsection[lintCoreBinding]{lintCoreBinding}
410 * *
411 ************************************************************************
412
413 Check a core binding, returning the list of variables bound.
414 -}
415
416 lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
417 -- If you edit this function, you may need to update the GHC formalism
418 -- See Note [GHC Formalism]
419 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
420 = addLoc (RhsOf binder) $
421 -- Check the rhs
422 do { ty <- lintCoreExpr rhs
423 ; lintBinder binder -- Check match to RHS type
424 ; binder_ty <- applySubstTy binder_ty
425 ; checkTys binder_ty ty (mkRhsMsg binder (ptext (sLit "RHS")) ty)
426
427 -- Check the let/app invariant
428 -- See Note [CoreSyn let/app invariant] in CoreSyn
429 ; checkL (not (isUnLiftedType binder_ty)
430 || (isNonRec rec_flag && exprOkForSpeculation rhs))
431 (mkRhsPrimMsg binder rhs)
432
433 -- Check that if the binder is top-level or recursive, it's not demanded
434 ; checkL (not (isStrictId binder)
435 || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
436 (mkStrictMsg binder)
437
438 -- Check that if the binder is local, it is not marked as exported
439 ; checkL (not (isExportedId binder) || isTopLevel top_lvl_flag)
440 (mkNonTopExportedMsg binder)
441
442 -- Check that if the binder is local, it does not have an external name
443 ; checkL (not (isExternalName (Var.varName binder)) || isTopLevel top_lvl_flag)
444 (mkNonTopExternalNameMsg binder)
445
446 -- Check whether binder's specialisations contain any out-of-scope variables
447 ; mapM_ (checkBndrIdInScope binder) bndr_vars
448
449 ; when (isStrongLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
450 (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
451 -- Only non-rule loop breakers inhibit inlining
452
453 -- Check whether arity and demand type are consistent (only if demand analysis
454 -- already happened)
455 --
456 -- Note (Apr 2014): this is actually ok. See Note [Demand analysis for trivial right-hand sides]
457 -- in DmdAnal. After eta-expansion in CorePrep the rhs is no longer trivial.
458 -- ; let dmdTy = idStrictness binder
459 -- ; checkL (case dmdTy of
460 -- StrictSig dmd_ty -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs)
461 -- (mkArityMsg binder)
462
463 ; lintIdUnfolding binder binder_ty (idUnfolding binder) }
464
465 -- We should check the unfolding, if any, but this is tricky because
466 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
467 where
468 binder_ty = idType binder
469 bndr_vars = varSetElems (idFreeVars binder)
470
471 -- If you edit this function, you may need to update the GHC formalism
472 -- See Note [GHC Formalism]
473 lintBinder var | isId var = lintIdBndr var $ \_ -> (return ())
474 | otherwise = return ()
475
476 lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
477 lintIdUnfolding bndr bndr_ty (CoreUnfolding { uf_tmpl = rhs, uf_src = src })
478 | isStableSource src
479 = do { ty <- lintCoreExpr rhs
480 ; checkTys bndr_ty ty (mkRhsMsg bndr (ptext (sLit "unfolding")) ty) }
481 lintIdUnfolding _ _ _
482 = return () -- We could check more
483
484 {-
485 ************************************************************************
486 * *
487 \subsection[lintCoreExpr]{lintCoreExpr}
488 * *
489 ************************************************************************
490 -}
491
492 --type InKind = Kind -- Substitution not yet applied
493 type InType = Type
494 type InCoercion = Coercion
495 type InVar = Var
496 type InTyVar = TyVar
497
498 type OutKind = Kind -- Substitution has been applied to this,
499 -- but has not been linted yet
500 type LintedKind = Kind -- Substitution applied, and type is linted
501
502 type OutType = Type -- Substitution has been applied to this,
503 -- but has not been linted yet
504
505 type LintedType = Type -- Substitution applied, and type is linted
506
507 type OutCoercion = Coercion
508 type OutVar = Var
509 type OutTyVar = TyVar
510
511 lintCoreExpr :: CoreExpr -> LintM OutType
512 -- The returned type has the substitution from the monad
513 -- already applied to it:
514 -- lintCoreExpr e subst = exprType (subst e)
515 --
516 -- The returned "type" can be a kind, if the expression is (Type ty)
517
518 -- If you edit this function, you may need to update the GHC formalism
519 -- See Note [GHC Formalism]
520 lintCoreExpr (Var var)
521 = do { checkL (not (var == oneTupleDataConId))
522 (ptext (sLit "Illegal one-tuple"))
523
524 ; checkL (isId var && not (isCoVar var))
525 (ptext (sLit "Non term variable") <+> ppr var)
526
527 ; checkDeadIdOcc var
528 ; var' <- lookupIdInScope var
529 ; return (idType var') }
530
531 lintCoreExpr (Lit lit)
532 = return (literalType lit)
533
534 lintCoreExpr (Cast expr co)
535 = do { expr_ty <- lintCoreExpr expr
536 ; co' <- applySubstCo co
537 ; (_, from_ty, to_ty, r) <- lintCoercion co'
538 ; checkRole co' Representational r
539 ; checkTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
540 ; return to_ty }
541
542 lintCoreExpr (Tick (Breakpoint _ ids) expr)
543 = do forM_ ids $ \id -> do
544 checkDeadIdOcc id
545 lookupIdInScope id
546 lintCoreExpr expr
547
548 lintCoreExpr (Tick _other_tickish expr)
549 = lintCoreExpr expr
550
551 lintCoreExpr (Let (NonRec tv (Type ty)) body)
552 | isTyVar tv
553 = -- See Note [Linting type lets]
554 do { ty' <- applySubstTy ty
555 ; lintTyBndr tv $ \ tv' ->
556 do { addLoc (RhsOf tv) $ checkTyKind tv' ty'
557 -- Now extend the substitution so we
558 -- take advantage of it in the body
559 ; extendSubstL tv' ty' $
560 addLoc (BodyOfLetRec [tv]) $
561 lintCoreExpr body } }
562
563 lintCoreExpr (Let (NonRec bndr rhs) body)
564 | isId bndr
565 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
566 ; addLoc (BodyOfLetRec [bndr])
567 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
568
569 | otherwise
570 = failWithL (mkLetErr bndr rhs) -- Not quite accurate
571
572 lintCoreExpr (Let (Rec pairs) body)
573 = lintAndScopeIds bndrs $ \_ ->
574 do { checkL (null dups) (dupVars dups)
575 ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
576 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
577 where
578 bndrs = map fst pairs
579 (_, dups) = removeDups compare bndrs
580
581 lintCoreExpr e@(App _ _)
582 = do { fun_ty <- lintCoreExpr fun
583 ; addLoc (AnExpr e) $ foldM lintCoreArg fun_ty args }
584 where
585 (fun, args) = collectArgs e
586
587 lintCoreExpr (Lam var expr)
588 = addLoc (LambdaBodyOf var) $
589 lintBinder var $ \ var' ->
590 do { body_ty <- lintCoreExpr expr
591 ; if isId var' then
592 return (mkFunTy (idType var') body_ty)
593 else
594 return (mkForAllTy var' body_ty)
595 }
596 -- The applySubstTy is needed to apply the subst to var
597
598 lintCoreExpr e@(Case scrut var alt_ty alts) =
599 -- Check the scrutinee
600 do { scrut_ty <- lintCoreExpr scrut
601 ; alt_ty <- lintInTy alt_ty
602 ; var_ty <- lintInTy (idType var)
603
604 ; case tyConAppTyCon_maybe (idType var) of
605 Just tycon
606 | debugIsOn &&
607 isAlgTyCon tycon &&
608 not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
609 null (tyConDataCons tycon) ->
610 pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
611 -- This can legitimately happen for type families
612 $ return ()
613 _otherwise -> return ()
614
615 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
616
617 ; subst <- getTvSubst
618 ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
619
620 ; lintAndScopeId var $ \_ ->
621 do { -- Check the alternatives
622 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
623 ; checkCaseAlts e scrut_ty alts
624 ; return alt_ty } }
625
626 -- This case can't happen; linting types in expressions gets routed through
627 -- lintCoreArgs
628 lintCoreExpr (Type ty)
629 = pprPanic "lintCoreExpr" (ppr ty)
630
631 lintCoreExpr (Coercion co)
632 = do { (_kind, ty1, ty2, role) <- lintInCo co
633 ; return (mkCoercionType role ty1 ty2) }
634
635 {-
636 Note [Kind instantiation in coercions]
637 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
638 Consider the following coercion axiom:
639 ax_co [(k_ag :: BOX), (f_aa :: k_ag -> Constraint)] :: T k_ag f_aa ~ f_aa
640
641 Consider the following instantiation:
642 ax_co <* -> *> <Monad>
643
644 We need to split the co_ax_tvs into kind and type variables in order
645 to find out the coercion kind instantiations. Those can only be Refl
646 since we don't have kind coercions. This is just a way to represent
647 kind instantiation.
648
649 We use the number of kind variables to know how to split the coercions
650 instantiations between kind coercions and type coercions. We lint the
651 kind coercions and produce the following substitution which is to be
652 applied in the type variables:
653 k_ag ~~> * -> *
654
655 ************************************************************************
656 * *
657 \subsection[lintCoreArgs]{lintCoreArgs}
658 * *
659 ************************************************************************
660
661 The basic version of these functions checks that the argument is a
662 subtype of the required type, as one would expect.
663 -}
664
665 lintCoreArg :: OutType -> CoreArg -> LintM OutType
666 lintCoreArg fun_ty (Type arg_ty)
667 = do { arg_ty' <- applySubstTy arg_ty
668 ; lintTyApp fun_ty arg_ty' }
669
670 lintCoreArg fun_ty arg
671 = do { arg_ty <- lintCoreExpr arg
672 ; checkL (not (isUnLiftedType arg_ty) || exprOkForSpeculation arg)
673 (mkLetAppMsg arg)
674 ; lintValApp arg fun_ty arg_ty }
675
676 -----------------
677 lintAltBinders :: OutType -- Scrutinee type
678 -> OutType -- Constructor type
679 -> [OutVar] -- Binders
680 -> LintM ()
681 -- If you edit this function, you may need to update the GHC formalism
682 -- See Note [GHC Formalism]
683 lintAltBinders scrut_ty con_ty []
684 = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
685 lintAltBinders scrut_ty con_ty (bndr:bndrs)
686 | isTyVar bndr
687 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
688 ; lintAltBinders scrut_ty con_ty' bndrs }
689 | otherwise
690 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
691 ; lintAltBinders scrut_ty con_ty' bndrs }
692
693 -----------------
694 lintTyApp :: OutType -> OutType -> LintM OutType
695 lintTyApp fun_ty arg_ty
696 | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
697 , isTyVar tyvar
698 = do { checkTyKind tyvar arg_ty
699 ; return (substTyWith [tyvar] [arg_ty] body_ty) }
700
701 | otherwise
702 = failWithL (mkTyAppMsg fun_ty arg_ty)
703
704 -----------------
705 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
706 lintValApp arg fun_ty arg_ty
707 | Just (arg,res) <- splitFunTy_maybe fun_ty
708 = do { checkTys arg arg_ty err1
709 ; return res }
710 | otherwise
711 = failWithL err2
712 where
713 err1 = mkAppMsg fun_ty arg_ty arg
714 err2 = mkNonFunAppMsg fun_ty arg_ty arg
715
716 checkTyKind :: OutTyVar -> OutType -> LintM ()
717 -- Both args have had substitution applied
718
719 -- If you edit this function, you may need to update the GHC formalism
720 -- See Note [GHC Formalism]
721 checkTyKind tyvar arg_ty
722 | isSuperKind tyvar_kind -- kind forall
723 = lintKind arg_ty
724 -- Arg type might be boxed for a function with an uncommitted
725 -- tyvar; notably this is used so that we can give
726 -- error :: forall a:*. String -> a
727 -- and then apply it to both boxed and unboxed types.
728 | otherwise -- type forall
729 = do { arg_kind <- lintType arg_ty
730 ; unless (arg_kind `isSubKind` tyvar_kind)
731 (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
732 where
733 tyvar_kind = tyVarKind tyvar
734
735 checkDeadIdOcc :: Id -> LintM ()
736 -- Occurrences of an Id should never be dead....
737 -- except when we are checking a case pattern
738 checkDeadIdOcc id
739 | isDeadOcc (idOccInfo id)
740 = do { in_case <- inCasePat
741 ; checkL in_case
742 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
743 | otherwise
744 = return ()
745
746 {-
747 ************************************************************************
748 * *
749 \subsection[lintCoreAlts]{lintCoreAlts}
750 * *
751 ************************************************************************
752 -}
753
754 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
755 -- a) Check that the alts are non-empty
756 -- b1) Check that the DEFAULT comes first, if it exists
757 -- b2) Check that the others are in increasing order
758 -- c) Check that there's a default for infinite types
759 -- NB: Algebraic cases are not necessarily exhaustive, because
760 -- the simplifer correctly eliminates case that can't
761 -- possibly match.
762
763 checkCaseAlts e ty alts =
764 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
765 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
766
767 -- For types Int#, Word# with an infinite (well, large!) number of
768 -- possible values, there should usually be a DEFAULT case
769 -- But (see Note [Empty case alternatives] in CoreSyn) it's ok to
770 -- have *no* case alternatives.
771 -- In effect, this is a kind of partial test. I suppose it's possible
772 -- that we might *know* that 'x' was 1 or 2, in which case
773 -- case x of { 1 -> e1; 2 -> e2 }
774 -- would be fine.
775 ; checkL (isJust maybe_deflt || not is_infinite_ty || null alts)
776 (nonExhaustiveAltsMsg e) }
777 where
778 (con_alts, maybe_deflt) = findDefault alts
779
780 -- Check that successive alternatives have increasing tags
781 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
782 increasing_tag _ = True
783
784 non_deflt (DEFAULT, _, _) = False
785 non_deflt _ = True
786
787 is_infinite_ty = case tyConAppTyCon_maybe ty of
788 Nothing -> False
789 Just tycon -> isPrimTyCon tycon
790
791 checkAltExpr :: CoreExpr -> OutType -> LintM ()
792 checkAltExpr expr ann_ty
793 = do { actual_ty <- lintCoreExpr expr
794 ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
795
796 lintCoreAlt :: OutType -- Type of scrutinee
797 -> OutType -- Type of the alternative
798 -> CoreAlt
799 -> LintM ()
800 -- If you edit this function, you may need to update the GHC formalism
801 -- See Note [GHC Formalism]
802 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
803 do { checkL (null args) (mkDefaultArgsMsg args)
804 ; checkAltExpr rhs alt_ty }
805
806 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
807 | litIsLifted lit
808 = failWithL integerScrutinisedMsg
809 | otherwise
810 = do { checkL (null args) (mkDefaultArgsMsg args)
811 ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
812 ; checkAltExpr rhs alt_ty }
813 where
814 lit_ty = literalType lit
815
816 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
817 | isNewTyCon (dataConTyCon con)
818 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
819 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
820 = addLoc (CaseAlt alt) $ do
821 { -- First instantiate the universally quantified
822 -- type variables of the data constructor
823 -- We've already check
824 checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
825 ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
826
827 -- And now bring the new binders into scope
828 ; lintBinders args $ \ args' -> do
829 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
830 ; checkAltExpr rhs alt_ty } }
831
832 | otherwise -- Scrut-ty is wrong shape
833 = addErrL (mkBadAltMsg scrut_ty alt)
834
835 {-
836 ************************************************************************
837 * *
838 \subsection[lint-types]{Types}
839 * *
840 ************************************************************************
841 -}
842
843 -- When we lint binders, we (one at a time and in order):
844 -- 1. Lint var types or kinds (possibly substituting)
845 -- 2. Add the binder to the in scope set, and if its a coercion var,
846 -- we may extend the substitution to reflect its (possibly) new kind
847 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
848 lintBinders [] linterF = linterF []
849 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
850 lintBinders vars $ \ vars' ->
851 linterF (var':vars')
852
853 -- If you edit this function, you may need to update the GHC formalism
854 -- See Note [GHC Formalism]
855 lintBinder :: Var -> (Var -> LintM a) -> LintM a
856 lintBinder var linterF
857 | isId var = lintIdBndr var linterF
858 | otherwise = lintTyBndr var linterF
859
860 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
861 lintTyBndr tv thing_inside
862 = do { subst <- getTvSubst
863 ; let (subst', tv') = Type.substTyVarBndr subst tv
864 ; lintTyBndrKind tv'
865 ; updateTvSubst subst' (thing_inside tv') }
866
867 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
868 -- Do substitution on the type of a binder and add the var with this
869 -- new type to the in-scope set of the second argument
870 -- ToDo: lint its rules
871
872 lintIdBndr id linterF
873 = do { lintAndScopeId id $ \id' -> linterF id' }
874
875 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
876 lintAndScopeIds ids linterF
877 = go ids
878 where
879 go [] = linterF []
880 go (id:ids) = lintAndScopeId id $ \id ->
881 lintAndScopeIds ids $ \ids ->
882 linterF (id:ids)
883
884 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
885 lintAndScopeId id linterF
886 = do { flags <- getLintFlags
887 ; checkL (not (lf_check_global_ids flags) || isLocalId id)
888 (ptext (sLit "Non-local Id binder") <+> ppr id)
889 -- See Note [Checking for global Ids]
890 ; ty <- lintInTy (idType id)
891 ; let id' = setIdType id ty
892 ; addInScopeVar id' $ (linterF id') }
893
894 {-
895 ************************************************************************
896 * *
897 Types and kinds
898 * *
899 ************************************************************************
900
901 We have a single linter for types and kinds. That is convenient
902 because sometimes it's not clear whether the thing we are looking
903 at is a type or a kind.
904 -}
905
906 lintInTy :: InType -> LintM LintedType
907 -- Types only, not kinds
908 -- Check the type, and apply the substitution to it
909 -- See Note [Linting type lets]
910 lintInTy ty
911 = addLoc (InType ty) $
912 do { ty' <- applySubstTy ty
913 ; _k <- lintType ty'
914 ; return ty' }
915
916 -------------------
917 lintTyBndrKind :: OutTyVar -> LintM ()
918 -- Handles both type and kind foralls.
919 lintTyBndrKind tv = lintKind (tyVarKind tv)
920
921 -------------------
922 lintType :: OutType -> LintM LintedKind
923 -- The returned Kind has itself been linted
924
925 -- If you edit this function, you may need to update the GHC formalism
926 -- See Note [GHC Formalism]
927 lintType (TyVarTy tv)
928 = do { checkTyCoVarInScope tv
929 ; return (tyVarKind tv) }
930 -- We checked its kind when we added it to the envt
931
932 lintType ty@(AppTy t1 t2)
933 = do { k1 <- lintType t1
934 ; k2 <- lintType t2
935 ; lint_ty_app ty k1 [(t2,k2)] }
936
937 lintType ty@(FunTy t1 t2) -- (->) has two different rules, for types and kinds
938 = do { k1 <- lintType t1
939 ; k2 <- lintType t2
940 ; lintArrow (ptext (sLit "type or kind") <+> quotes (ppr ty)) k1 k2 }
941
942 lintType ty@(TyConApp tc tys)
943 | Just ty' <- coreView ty
944 = lintType ty' -- Expand type synonyms, so that we do not bogusly complain
945 -- about un-saturated type synonyms
946
947 | isUnLiftedTyCon tc || isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
948 -- See Note [The kind invariant] in TypeRep
949 -- Also type synonyms and type families
950 , length tys < tyConArity tc
951 = failWithL (hang (ptext (sLit "Un-saturated type application")) 2 (ppr ty))
952
953 | otherwise
954 = do { ks <- mapM lintType tys
955 ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
956
957 lintType (ForAllTy tv ty)
958 = do { lintTyBndrKind tv
959 ; addInScopeVar tv (lintType ty) }
960
961 lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
962
963 lintKind :: OutKind -> LintM ()
964 -- If you edit this function, you may need to update the GHC formalism
965 -- See Note [GHC Formalism]
966 lintKind k = do { sk <- lintType k
967 ; unless (isSuperKind sk)
968 (addErrL (hang (ptext (sLit "Ill-kinded kind:") <+> ppr k)
969 2 (ptext (sLit "has kind:") <+> ppr sk))) }
970
971 lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
972 -- If you edit this function, you may need to update the GHC formalism
973 -- See Note [GHC Formalism]
974 lintArrow what k1 k2 -- Eg lintArrow "type or kind `blah'" k1 k2
975 -- or lintarrow "coercion `blah'" k1 k2
976 | isSuperKind k1
977 = return superKind
978 | otherwise
979 = do { unless (okArrowArgKind k1) (addErrL (msg (ptext (sLit "argument")) k1))
980 ; unless (okArrowResultKind k2) (addErrL (msg (ptext (sLit "result")) k2))
981 ; return liftedTypeKind }
982 where
983 msg ar k
984 = vcat [ hang (ptext (sLit "Ill-kinded") <+> ar)
985 2 (ptext (sLit "in") <+> what)
986 , what <+> ptext (sLit "kind:") <+> ppr k ]
987
988 lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
989 lint_ty_app ty k tys
990 = lint_app (ptext (sLit "type") <+> quotes (ppr ty)) k tys
991
992 ----------------
993 lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
994 lint_co_app ty k tys
995 = lint_app (ptext (sLit "coercion") <+> quotes (ppr ty)) k tys
996
997 ----------------
998 lintTyLit :: TyLit -> LintM ()
999 lintTyLit (NumTyLit n)
1000 | n >= 0 = return ()
1001 | otherwise = failWithL msg
1002 where msg = ptext (sLit "Negative type literal:") <+> integer n
1003 lintTyLit (StrTyLit _) = return ()
1004
1005 lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
1006 -- (lint_app d fun_kind arg_tys)
1007 -- We have an application (f arg_ty1 .. arg_tyn),
1008 -- where f :: fun_kind
1009 -- Takes care of linting the OutTypes
1010
1011 -- If you edit this function, you may need to update the GHC formalism
1012 -- See Note [GHC Formalism]
1013 lint_app doc kfn kas
1014 = foldlM go_app kfn kas
1015 where
1016 fail_msg = vcat [ hang (ptext (sLit "Kind application error in")) 2 doc
1017 , nest 2 (ptext (sLit "Function kind =") <+> ppr kfn)
1018 , nest 2 (ptext (sLit "Arg kinds =") <+> ppr kas) ]
1019
1020 go_app kfn ka
1021 | Just kfn' <- coreView kfn
1022 = go_app kfn' ka
1023
1024 go_app (FunTy kfa kfb) (_,ka)
1025 = do { unless (ka `isSubKind` kfa) (addErrL fail_msg)
1026 ; return kfb }
1027
1028 go_app (ForAllTy kv kfn) (ta,ka)
1029 = do { unless (ka `isSubKind` tyVarKind kv) (addErrL fail_msg)
1030 ; return (substKiWith [kv] [ta] kfn) }
1031
1032 go_app _ _ = failWithL fail_msg
1033
1034 {-
1035 ************************************************************************
1036 * *
1037 Linting coercions
1038 * *
1039 ************************************************************************
1040 -}
1041
1042 lintInCo :: InCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
1043 -- Check the coercion, and apply the substitution to it
1044 -- See Note [Linting type lets]
1045 lintInCo co
1046 = addLoc (InCo co) $
1047 do { co' <- applySubstCo co
1048 ; lintCoercion co' }
1049
1050 lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
1051 -- Check the kind of a coercion term, returning the kind
1052 -- Post-condition: the returned OutTypes are lint-free
1053 -- and have the same kind as each other
1054
1055 -- If you edit this function, you may need to update the GHC formalism
1056 -- See Note [GHC Formalism]
1057 lintCoercion (Refl r ty)
1058 = do { k <- lintType ty
1059 ; return (k, ty, ty, r) }
1060
1061 lintCoercion co@(TyConAppCo r tc cos)
1062 | tc `hasKey` funTyConKey
1063 , [co1,co2] <- cos
1064 = do { (k1,s1,t1,r1) <- lintCoercion co1
1065 ; (k2,s2,t2,r2) <- lintCoercion co2
1066 ; rk <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k1 k2
1067 ; checkRole co1 r r1
1068 ; checkRole co2 r r2
1069 ; return (rk, mkFunTy s1 s2, mkFunTy t1 t2, r) }
1070
1071 | Just {} <- synTyConDefn_maybe tc
1072 = failWithL (ptext (sLit "Synonym in TyConAppCo:") <+> ppr co)
1073
1074 | otherwise
1075 = do { (ks,ss,ts,rs) <- mapAndUnzip4M lintCoercion cos
1076 ; rk <- lint_co_app co (tyConKind tc) (ss `zip` ks)
1077 ; _ <- zipWith3M checkRole cos (tyConRolesX r tc) rs
1078 ; return (rk, mkTyConApp tc ss, mkTyConApp tc ts, r) }
1079
1080 lintCoercion co@(AppCo co1 co2)
1081 = do { (k1,s1,t1,r1) <- lintCoercion co1
1082 ; (k2,s2,t2,r2) <- lintCoercion co2
1083 ; rk <- lint_co_app co k1 [(s2,k2)]
1084 ; if r1 == Phantom
1085 then checkL (r2 == Phantom || r2 == Nominal)
1086 (ptext (sLit "Second argument in AppCo cannot be R:") $$
1087 ppr co)
1088 else checkRole co Nominal r2
1089 ; return (rk, mkAppTy s1 s2, mkAppTy t1 t2, r1) }
1090
1091 lintCoercion (ForAllCo tv co)
1092 = do { lintTyBndrKind tv
1093 ; (k, s, t, r) <- addInScopeVar tv (lintCoercion co)
1094 ; return (k, mkForAllTy tv s, mkForAllTy tv t, r) }
1095
1096 lintCoercion (CoVarCo cv)
1097 | not (isCoVar cv)
1098 = failWithL (hang (ptext (sLit "Bad CoVarCo:") <+> ppr cv)
1099 2 (ptext (sLit "With offending type:") <+> ppr (varType cv)))
1100 | otherwise
1101 = do { checkTyCoVarInScope cv
1102 ; cv' <- lookupIdInScope cv
1103 ; let (s,t) = coVarKind cv'
1104 k = typeKind s
1105 r = coVarRole cv'
1106 ; when (isSuperKind k) $
1107 do { checkL (r == Nominal) (hang (ptext (sLit "Non-nominal kind equality"))
1108 2 (ppr cv))
1109 ; checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality"))
1110 2 (ppr cv)) }
1111 ; return (k, s, t, r) }
1112
1113 lintCoercion (UnivCo r ty1 ty2)
1114 = do { k1 <- lintType ty1
1115 ; _k2 <- lintType ty2
1116 -- ; unless (k1 `eqKind` k2) $
1117 -- failWithL (hang (ptext (sLit "Unsafe coercion changes kind"))
1118 -- 2 (ppr co))
1119 ; return (k1, ty1, ty2, r) }
1120
1121 lintCoercion (SymCo co)
1122 = do { (k, ty1, ty2, r) <- lintCoercion co
1123 ; return (k, ty2, ty1, r) }
1124
1125 lintCoercion co@(TransCo co1 co2)
1126 = do { (k1, ty1a, ty1b, r1) <- lintCoercion co1
1127 ; (_, ty2a, ty2b, r2) <- lintCoercion co2
1128 ; checkL (ty1b `eqType` ty2a)
1129 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
1130 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
1131 ; checkRole co r1 r2
1132 ; return (k1, ty1a, ty2b, r1) }
1133
1134 lintCoercion the_co@(NthCo n co)
1135 = do { (_,s,t,r) <- lintCoercion co
1136 ; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
1137 (Just (tc_s, tys_s), Just (tc_t, tys_t))
1138 | tc_s == tc_t
1139 , tys_s `equalLength` tys_t
1140 , n < length tys_s
1141 -> return (ks, ts, tt, tr)
1142 where
1143 ts = getNth tys_s n
1144 tt = getNth tys_t n
1145 tr = nthRole r tc_s n
1146 ks = typeKind ts
1147
1148 _ -> failWithL (hang (ptext (sLit "Bad getNth:"))
1149 2 (ppr the_co $$ ppr s $$ ppr t)) }
1150
1151 lintCoercion the_co@(LRCo lr co)
1152 = do { (_,s,t,r) <- lintCoercion co
1153 ; checkRole co Nominal r
1154 ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
1155 (Just s_pr, Just t_pr)
1156 -> return (k, s_pick, t_pick, Nominal)
1157 where
1158 s_pick = pickLR lr s_pr
1159 t_pick = pickLR lr t_pr
1160 k = typeKind s_pick
1161
1162 _ -> failWithL (hang (ptext (sLit "Bad LRCo:"))
1163 2 (ppr the_co $$ ppr s $$ ppr t)) }
1164
1165 lintCoercion (InstCo co arg_ty)
1166 = do { (k,s,t,r) <- lintCoercion co
1167 ; arg_kind <- lintType arg_ty
1168 ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
1169 (Just (tv1,ty1), Just (tv2,ty2))
1170 | arg_kind `isSubKind` tyVarKind tv1
1171 -> return (k, substTyWith [tv1] [arg_ty] ty1,
1172 substTyWith [tv2] [arg_ty] ty2, r)
1173 | otherwise
1174 -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
1175 _ -> failWithL (ptext (sLit "Bad argument of inst")) }
1176
1177 lintCoercion co@(AxiomInstCo con ind cos)
1178 = do { unless (0 <= ind && ind < brListLength (coAxiomBranches con))
1179 (bad_ax (ptext (sLit "index out of range")))
1180 -- See Note [Kind instantiation in coercions]
1181 ; let CoAxBranch { cab_tvs = ktvs
1182 , cab_roles = roles
1183 , cab_lhs = lhs
1184 , cab_rhs = rhs } = coAxiomNthBranch con ind
1185 ; unless (equalLength ktvs cos) (bad_ax (ptext (sLit "lengths")))
1186 ; in_scope <- getInScope
1187 ; let empty_subst = mkTvSubst in_scope emptyTvSubstEnv
1188 ; (subst_l, subst_r) <- foldlM check_ki
1189 (empty_subst, empty_subst)
1190 (zip3 ktvs roles cos)
1191 ; let lhs' = Type.substTys subst_l lhs
1192 rhs' = Type.substTy subst_r rhs
1193 ; case checkAxInstCo co of
1194 Just bad_branch -> bad_ax $ ptext (sLit "inconsistent with") <+> (pprCoAxBranch (coAxiomTyCon con) bad_branch)
1195 Nothing -> return ()
1196 ; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs', coAxiomRole con) }
1197 where
1198 bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what)
1199 2 (ppr co))
1200
1201 check_ki (subst_l, subst_r) (ktv, role, co)
1202 = do { (k, t1, t2, r) <- lintCoercion co
1203 ; checkRole co role r
1204 ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)
1205 -- Using subst_l is ok, because subst_l and subst_r
1206 -- must agree on kind equalities
1207 ; unless (k `isSubKind` ktv_kind)
1208 (bad_ax (ptext (sLit "check_ki2") <+> vcat [ ppr co, ppr k, ppr ktv, ppr ktv_kind ] ))
1209 ; return (Type.extendTvSubst subst_l ktv t1,
1210 Type.extendTvSubst subst_r ktv t2) }
1211
1212 lintCoercion co@(SubCo co')
1213 = do { (k,s,t,r) <- lintCoercion co'
1214 ; checkRole co Nominal r
1215 ; return (k,s,t,Representational) }
1216
1217
1218 lintCoercion this@(AxiomRuleCo co ts cs)
1219 = do _ks <- mapM lintType ts
1220 eqs <- mapM lintCoercion cs
1221
1222 let tyNum = length ts
1223
1224 case compare (coaxrTypeArity co) tyNum of
1225 EQ -> return ()
1226 LT -> err "Too many type arguments"
1227 [ txt "expected" <+> int (coaxrTypeArity co)
1228 , txt "provided" <+> int tyNum ]
1229 GT -> err "Not enough type arguments"
1230 [ txt "expected" <+> int (coaxrTypeArity co)
1231 , txt "provided" <+> int tyNum ]
1232 checkRoles 0 (coaxrAsmpRoles co) eqs
1233
1234 case coaxrProves co ts [ Pair l r | (_,l,r,_) <- eqs ] of
1235 Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
1236 Just (Pair l r) ->
1237 do kL <- lintType l
1238 kR <- lintType r
1239 unless (eqKind kL kR)
1240 $ err "Kind error in CoAxiomRule"
1241 [ppr kL <+> txt "/=" <+> ppr kR]
1242 return (kL, l, r, coaxrRole co)
1243 where
1244 txt = ptext . sLit
1245 err m xs = failWithL $
1246 hang (txt m) 2 $ vcat (txt "Rule:" <+> ppr (coaxrName co) : xs)
1247
1248 checkRoles n (e : es) ((_,_,_,r) : rs)
1249 | e == r = checkRoles (n+1) es rs
1250 | otherwise = err "Argument roles mismatch"
1251 [ txt "In argument:" <+> int (n+1)
1252 , txt "Expected:" <+> ppr e
1253 , txt "Found:" <+> ppr r ]
1254 checkRoles _ [] [] = return ()
1255 checkRoles n [] rs = err "Too many coercion arguments"
1256 [ txt "Expected:" <+> int n
1257 , txt "Provided:" <+> int (n + length rs) ]
1258
1259 checkRoles n es [] = err "Not enough coercion arguments"
1260 [ txt "Expected:" <+> int (n + length es)
1261 , txt "Provided:" <+> int n ]
1262
1263 {-
1264 ************************************************************************
1265 * *
1266 \subsection[lint-monad]{The Lint monad}
1267 * *
1268 ************************************************************************
1269 -}
1270
1271 -- If you edit this type, you may need to update the GHC formalism
1272 -- See Note [GHC Formalism]
1273 data LintEnv
1274 = LE { le_flags :: LintFlags -- Linting the result of this pass
1275 , le_loc :: [LintLocInfo] -- Locations
1276 , le_subst :: TvSubst -- Current type substitution; we also use this
1277 } -- to keep track of all the variables in scope,
1278 -- both Ids and TyVars
1279
1280 newtype LintFlags -- Currently only one flag
1281 = LF { lf_check_global_ids :: Bool -- See Note [Checking for global Ids]
1282 }
1283
1284 defaultLintFlags :: LintFlags
1285 defaultLintFlags = LF { lf_check_global_ids = False }
1286
1287 newtype LintM a =
1288 LintM { unLintM ::
1289 LintEnv ->
1290 WarnsAndErrs -> -- Error and warning messages so far
1291 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
1292
1293 type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)
1294
1295 {- Note [Checking for global Ids]
1296 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1297 Before CoreTidy, all locally-bound Ids must be LocalIds, even
1298 top-level ones. See Note [Exported LocalIds] and Trac #9857.
1299
1300 Note [Type substitution]
1301 ~~~~~~~~~~~~~~~~~~~~~~~~
1302 Why do we need a type substitution? Consider
1303 /\(a:*). \(x:a). /\(a:*). id a x
1304 This is ill typed, because (renaming variables) it is really
1305 /\(a:*). \(x:a). /\(b:*). id b x
1306 Hence, when checking an application, we can't naively compare x's type
1307 (at its binding site) with its expected type (at a use site). So we
1308 rename type binders as we go, maintaining a substitution.
1309
1310 The same substitution also supports let-type, current expressed as
1311 (/\(a:*). body) ty
1312 Here we substitute 'ty' for 'a' in 'body', on the fly.
1313 -}
1314
1315 instance Functor LintM where
1316 fmap = liftM
1317
1318 instance Applicative LintM where
1319 pure = return
1320 (<*>) = ap
1321
1322 instance Monad LintM where
1323 return x = LintM (\ _ errs -> (Just x, errs))
1324 fail err = failWithL (text err)
1325 m >>= k = LintM (\ env errs ->
1326 let (res, errs') = unLintM m env errs in
1327 case res of
1328 Just r -> unLintM (k r) env errs'
1329 Nothing -> (Nothing, errs'))
1330
1331 data LintLocInfo
1332 = RhsOf Id -- The variable bound
1333 | LambdaBodyOf Id -- The lambda-binder
1334 | BodyOfLetRec [Id] -- One of the binders
1335 | CaseAlt CoreAlt -- Case alternative
1336 | CasePat CoreAlt -- The *pattern* of the case alternative
1337 | AnExpr CoreExpr -- Some expression
1338 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
1339 | TopLevelBindings
1340 | InType Type -- Inside a type
1341 | InCo Coercion -- Inside a coercion
1342
1343 initL :: LintFlags -> LintM a -> WarnsAndErrs -- Errors and warnings
1344 initL flags m
1345 = case unLintM m env (emptyBag, emptyBag) of
1346 (_, errs) -> errs
1347 where
1348 env = LE { le_flags = flags, le_subst = emptyTvSubst, le_loc = [] }
1349
1350 getLintFlags :: LintM LintFlags
1351 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
1352
1353 checkL :: Bool -> MsgDoc -> LintM ()
1354 checkL True _ = return ()
1355 checkL False msg = failWithL msg
1356
1357 failWithL :: MsgDoc -> LintM a
1358 failWithL msg = LintM $ \ env (warns,errs) ->
1359 (Nothing, (warns, addMsg env errs msg))
1360
1361 addErrL :: MsgDoc -> LintM ()
1362 addErrL msg = LintM $ \ env (warns,errs) ->
1363 (Just (), (warns, addMsg env errs msg))
1364
1365 addWarnL :: MsgDoc -> LintM ()
1366 addWarnL msg = LintM $ \ env (warns,errs) ->
1367 (Just (), (addMsg env warns msg, errs))
1368
1369 addMsg :: LintEnv -> Bag MsgDoc -> MsgDoc -> Bag MsgDoc
1370 addMsg env msgs msg
1371 = ASSERT( notNull locs )
1372 msgs `snocBag` mk_msg msg
1373 where
1374 locs = le_loc env
1375 (loc, cxt1) = dumpLoc (head locs)
1376 cxts = [snd (dumpLoc loc) | loc <- locs]
1377 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
1378 ptext (sLit "Substitution:") <+> ppr (le_subst env)
1379 | otherwise = cxt1
1380
1381 mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
1382
1383 addLoc :: LintLocInfo -> LintM a -> LintM a
1384 addLoc extra_loc m
1385 = LintM $ \ env errs ->
1386 unLintM m (env { le_loc = extra_loc : le_loc env }) errs
1387
1388 inCasePat :: LintM Bool -- A slight hack; see the unique call site
1389 inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
1390 where
1391 is_case_pat (LE { le_loc = CasePat {} : _ }) = True
1392 is_case_pat _other = False
1393
1394 addInScopeVars :: [Var] -> LintM a -> LintM a
1395 addInScopeVars vars m
1396 = LintM $ \ env errs ->
1397 unLintM m (env { le_subst = extendTvInScopeList (le_subst env) vars })
1398 errs
1399
1400 addInScopeVar :: Var -> LintM a -> LintM a
1401 addInScopeVar var m
1402 = LintM $ \ env errs ->
1403 unLintM m (env { le_subst = extendTvInScope (le_subst env) var }) errs
1404
1405 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
1406 extendSubstL tv ty m
1407 = LintM $ \ env errs ->
1408 unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
1409
1410 updateTvSubst :: TvSubst -> LintM a -> LintM a
1411 updateTvSubst subst' m
1412 = LintM $ \ env errs -> unLintM m (env { le_subst = subst' }) errs
1413
1414 getTvSubst :: LintM TvSubst
1415 getTvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
1416
1417 getInScope :: LintM InScopeSet
1418 getInScope = LintM (\ env errs -> (Just (getTvInScope (le_subst env)), errs))
1419
1420 applySubstTy :: InType -> LintM OutType
1421 applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
1422
1423 applySubstCo :: InCoercion -> LintM OutCoercion
1424 applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
1425
1426 lookupIdInScope :: Id -> LintM Id
1427 lookupIdInScope id
1428 | not (mustHaveLocalBinding id)
1429 = return id -- An imported Id
1430 | otherwise
1431 = do { subst <- getTvSubst
1432 ; case lookupInScope (getTvInScope subst) id of
1433 Just v -> return v
1434 Nothing -> do { addErrL out_of_scope
1435 ; return id } }
1436 where
1437 out_of_scope = pprBndr LetBind id <+> ptext (sLit "is out of scope")
1438
1439
1440 oneTupleDataConId :: Id -- Should not happen
1441 oneTupleDataConId = dataConWorkId (tupleCon BoxedTuple 1)
1442
1443 checkBndrIdInScope :: Var -> Var -> LintM ()
1444 checkBndrIdInScope binder id
1445 = checkInScope msg id
1446 where
1447 msg = ptext (sLit "is out of scope inside info for") <+>
1448 ppr binder
1449
1450 checkTyCoVarInScope :: Var -> LintM ()
1451 checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
1452
1453 checkInScope :: SDoc -> Var -> LintM ()
1454 checkInScope loc_msg var =
1455 do { subst <- getTvSubst
1456 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
1457 (hsep [pprBndr LetBind var, loc_msg]) }
1458
1459 checkTys :: OutType -> OutType -> MsgDoc -> LintM ()
1460 -- check ty2 is subtype of ty1 (ie, has same structure but usage
1461 -- annotations need only be consistent, not equal)
1462 -- Assumes ty1,ty2 are have alrady had the substitution applied
1463 checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
1464
1465 checkRole :: Coercion
1466 -> Role -- expected
1467 -> Role -- actual
1468 -> LintM ()
1469 checkRole co r1 r2
1470 = checkL (r1 == r2)
1471 (ptext (sLit "Role incompatibility: expected") <+> ppr r1 <> comma <+>
1472 ptext (sLit "got") <+> ppr r2 $$
1473 ptext (sLit "in") <+> ppr co)
1474
1475 {-
1476 ************************************************************************
1477 * *
1478 \subsection{Error messages}
1479 * *
1480 ************************************************************************
1481 -}
1482
1483 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
1484
1485 dumpLoc (RhsOf v)
1486 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
1487
1488 dumpLoc (LambdaBodyOf b)
1489 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
1490
1491 dumpLoc (BodyOfLetRec [])
1492 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
1493
1494 dumpLoc (BodyOfLetRec bs@(_:_))
1495 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
1496
1497 dumpLoc (AnExpr e)
1498 = (noSrcLoc, text "In the expression:" <+> ppr e)
1499
1500 dumpLoc (CaseAlt (con, args, _))
1501 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1502
1503 dumpLoc (CasePat (con, args, _))
1504 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1505
1506 dumpLoc (ImportedUnfolding locn)
1507 = (locn, brackets (ptext (sLit "in an imported unfolding")))
1508 dumpLoc TopLevelBindings
1509 = (noSrcLoc, Outputable.empty)
1510 dumpLoc (InType ty)
1511 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1512 dumpLoc (InCo co)
1513 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
1514
1515 pp_binders :: [Var] -> SDoc
1516 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1517
1518 pp_binder :: Var -> SDoc
1519 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1520 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1521
1522 ------------------------------------------------------
1523 -- Messages for case expressions
1524
1525 mkDefaultArgsMsg :: [Var] -> MsgDoc
1526 mkDefaultArgsMsg args
1527 = hang (text "DEFAULT case with binders")
1528 4 (ppr args)
1529
1530 mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
1531 mkCaseAltMsg e ty1 ty2
1532 = hang (text "Type of case alternatives not the same as the annotation on case:")
1533 4 (vcat [ppr ty1, ppr ty2, ppr e])
1534
1535 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> MsgDoc
1536 mkScrutMsg var var_ty scrut_ty subst
1537 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1538 text "Result binder type:" <+> ppr var_ty,--(idType var),
1539 text "Scrutinee type:" <+> ppr scrut_ty,
1540 hsep [ptext (sLit "Current TV subst"), ppr subst]]
1541
1542 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
1543 mkNonDefltMsg e
1544 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1545 mkNonIncreasingAltsMsg e
1546 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1547
1548 nonExhaustiveAltsMsg :: CoreExpr -> MsgDoc
1549 nonExhaustiveAltsMsg e
1550 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1551
1552 mkBadConMsg :: TyCon -> DataCon -> MsgDoc
1553 mkBadConMsg tycon datacon
1554 = vcat [
1555 text "In a case alternative, data constructor isn't in scrutinee type:",
1556 text "Scrutinee type constructor:" <+> ppr tycon,
1557 text "Data con:" <+> ppr datacon
1558 ]
1559
1560 mkBadPatMsg :: Type -> Type -> MsgDoc
1561 mkBadPatMsg con_result_ty scrut_ty
1562 = vcat [
1563 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1564 text "Pattern result type:" <+> ppr con_result_ty,
1565 text "Scrutinee type:" <+> ppr scrut_ty
1566 ]
1567
1568 integerScrutinisedMsg :: MsgDoc
1569 integerScrutinisedMsg
1570 = text "In a LitAlt, the literal is lifted (probably Integer)"
1571
1572 mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
1573 mkBadAltMsg scrut_ty alt
1574 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1575 text "Scrutinee type:" <+> ppr scrut_ty,
1576 text "Alternative:" <+> pprCoreAlt alt ]
1577
1578 mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc
1579 mkNewTyDataConAltMsg scrut_ty alt
1580 = vcat [ text "Data alternative for newtype datacon",
1581 text "Scrutinee type:" <+> ppr scrut_ty,
1582 text "Alternative:" <+> pprCoreAlt alt ]
1583
1584
1585 ------------------------------------------------------
1586 -- Other error messages
1587
1588 mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1589 mkAppMsg fun_ty arg_ty arg
1590 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1591 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1592 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1593 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1594
1595 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1596 mkNonFunAppMsg fun_ty arg_ty arg
1597 = vcat [ptext (sLit "Non-function type in function position"),
1598 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1599 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1600 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1601
1602 mkLetErr :: TyVar -> CoreExpr -> MsgDoc
1603 mkLetErr bndr rhs
1604 = vcat [ptext (sLit "Bad `let' binding:"),
1605 hang (ptext (sLit "Variable:"))
1606 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
1607 hang (ptext (sLit "Rhs:"))
1608 4 (ppr rhs)]
1609
1610 mkTyAppMsg :: Type -> Type -> MsgDoc
1611 mkTyAppMsg ty arg_ty
1612 = vcat [text "Illegal type application:",
1613 hang (ptext (sLit "Exp type:"))
1614 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1615 hang (ptext (sLit "Arg type:"))
1616 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1617
1618 mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc
1619 mkRhsMsg binder what ty
1620 = vcat
1621 [hsep [ptext (sLit "The type of this binder doesn't match the type of its") <+> what <> colon,
1622 ppr binder],
1623 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1624 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1625
1626 mkLetAppMsg :: CoreExpr -> MsgDoc
1627 mkLetAppMsg e
1628 = hang (ptext (sLit "This argument does not satisfy the let/app invariant:"))
1629 2 (ppr e)
1630
1631 mkRhsPrimMsg :: Id -> CoreExpr -> MsgDoc
1632 mkRhsPrimMsg binder _rhs
1633 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1634 ppr binder],
1635 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1636 ]
1637
1638 mkStrictMsg :: Id -> MsgDoc
1639 mkStrictMsg binder
1640 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1641 ppr binder],
1642 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1643 ]
1644
1645 mkNonTopExportedMsg :: Id -> MsgDoc
1646 mkNonTopExportedMsg binder
1647 = hsep [ptext (sLit "Non-top-level binder is marked as exported:"), ppr binder]
1648
1649 mkNonTopExternalNameMsg :: Id -> MsgDoc
1650 mkNonTopExternalNameMsg binder
1651 = hsep [ptext (sLit "Non-top-level binder has an external name:"), ppr binder]
1652
1653 mkKindErrMsg :: TyVar -> Type -> MsgDoc
1654 mkKindErrMsg tyvar arg_ty
1655 = vcat [ptext (sLit "Kinds don't match in type application:"),
1656 hang (ptext (sLit "Type variable:"))
1657 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1658 hang (ptext (sLit "Arg type:"))
1659 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1660
1661 {- Not needed now
1662 mkArityMsg :: Id -> MsgDoc
1663 mkArityMsg binder
1664 = vcat [hsep [ptext (sLit "Demand type has"),
1665 ppr (dmdTypeDepth dmd_ty),
1666 ptext (sLit "arguments, rhs has"),
1667 ppr (idArity binder),
1668 ptext (sLit "arguments,"),
1669 ppr binder],
1670 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1671
1672 ]
1673 where (StrictSig dmd_ty) = idStrictness binder
1674 -}
1675 mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> MsgDoc
1676 mkCastErr expr co from_ty expr_ty
1677 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1678 ptext (sLit "From-type:") <+> ppr from_ty,
1679 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty,
1680 ptext (sLit "Actual enclosed expr:") <+> ppr expr,
1681 ptext (sLit "Coercion used in cast:") <+> ppr co
1682 ]
1683
1684 dupVars :: [[Var]] -> MsgDoc
1685 dupVars vars
1686 = hang (ptext (sLit "Duplicate variables brought into scope"))
1687 2 (ppr vars)
1688
1689 dupExtVars :: [[Name]] -> MsgDoc
1690 dupExtVars vars
1691 = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))
1692 2 (ppr vars)
1693
1694 {-
1695 ************************************************************************
1696 * *
1697 \subsection{Annotation Linting}
1698 * *
1699 ************************************************************************
1700 -}
1701
1702 -- | This checks whether a pass correctly looks through debug
1703 -- annotations (@SourceNote@). This works a bit different from other
1704 -- consistency checks: We check this by running the given task twice,
1705 -- noting all differences between the results.
1706 lintAnnots :: SDoc -> (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
1707 lintAnnots pname pass guts = do
1708 -- Run the pass as we normally would
1709 dflags <- getDynFlags
1710 when (gopt Opt_DoAnnotationLinting dflags) $
1711 liftIO $ Err.showPass dflags "Annotation linting - first run"
1712 nguts <- pass guts
1713 -- If appropriate re-run it without debug annotations to make sure
1714 -- that they made no difference.
1715 when (gopt Opt_DoAnnotationLinting dflags) $ do
1716 liftIO $ Err.showPass dflags "Annotation linting - second run"
1717 nguts' <- withoutAnnots pass guts
1718 -- Finally compare the resulting bindings
1719 liftIO $ Err.showPass dflags "Annotation linting - comparison"
1720 let binds = flattenBinds $ mg_binds nguts
1721 binds' = flattenBinds $ mg_binds nguts'
1722 (diffs,_) = diffBinds True (mkRnEnv2 emptyInScopeSet) binds binds'
1723 when (not (null diffs)) $ CoreMonad.putMsg $ vcat
1724 [ lint_banner "warning" pname
1725 , text "Core changes with annotations:"
1726 , withPprStyle defaultDumpStyle $ nest 2 $ vcat diffs
1727 ]
1728 -- Return actual new guts
1729 return nguts
1730
1731 -- | Run the given pass without annotations. This means that we both
1732 -- remove the @Opt_Debug@ flag from the environment as well as all
1733 -- annotations from incoming modules.
1734 withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
1735 withoutAnnots pass guts = do
1736 -- Remove debug flag from environment.
1737 dflags <- getDynFlags
1738 let removeFlag env = env{hsc_dflags = gopt_unset dflags Opt_Debug}
1739 withoutFlag corem =
1740 liftIO =<< runCoreM <$> fmap removeFlag getHscEnv <*> getRuleBase <*>
1741 getUniqueSupplyM <*> getModule <*>
1742 getPrintUnqualified <*> pure corem
1743 -- Nuke existing ticks in module.
1744 -- TODO: Ticks in unfoldings. Maybe change unfolding so it removes
1745 -- them in absence of @Opt_Debug@?
1746 let nukeTicks = snd . stripTicks (not . tickishIsCode)
1747 nukeAnnotsBind :: CoreBind -> CoreBind
1748 nukeAnnotsBind bind = case bind of
1749 Rec bs -> Rec $ map (\(b,e) -> (b, nukeTicks e)) bs
1750 NonRec b e -> NonRec b $ nukeTicks e
1751 nukeAnnotsMod mg@ModGuts{mg_binds=binds}
1752 = mg{mg_binds = map nukeAnnotsBind binds}
1753 -- Perform pass with all changes applied
1754 fmap fst $ withoutFlag $ pass (nukeAnnotsMod guts)