f9e7f863c417b285209c474c46f1346545594565
[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
11 module CoreLint (
12 lintCoreBindings, lintUnfolding,
13 lintPassResult, lintInteractiveExpr, lintExpr,
14 lintAnnots,
15
16 -- ** Debug output
17 endPass, endPassIO,
18 dumpPassResult,
19 CoreLint.dumpIfSet,
20 ) where
21
22 #include "HsVersions.h"
23
24 import CoreSyn
25 import CoreFVs
26 import CoreUtils
27 import CoreStats ( coreBindsStats )
28 import CoreMonad
29 import Bag
30 import Literal
31 import DataCon
32 import TysWiredIn
33 import TcType ( isFloatingTy )
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 RepType
46 import TyCoRep -- checks validity of types/coercions
47 import TyCon
48 import CoAxiom
49 import BasicTypes
50 import ErrUtils as Err
51 import StaticFlags
52 import ListSetOps
53 import PrelNames
54 import Outputable
55 import FastString
56 import Util
57 import InstEnv ( instanceDFunId )
58 import OptCoercion ( checkAxInstCo )
59 import UniqSupply
60 import CoreArity ( typeArity )
61 import Demand ( splitStrictSig, isBotRes )
62
63 import HscTypes
64 import DynFlags
65 import Control.Monad
66 #if __GLASGOW_HASKELL__ > 710
67 import qualified Control.Monad.Fail as MonadFail
68 #endif
69 import MonadUtils
70 import Data.Maybe
71 import Pair
72 import qualified GHC.LanguageExtensions as LangExt
73
74 {-
75 Note [GHC Formalism]
76 ~~~~~~~~~~~~~~~~~~~~
77 This file implements the type-checking algorithm for System FC, the "official"
78 name of the Core language. Type safety of FC is heart of the claim that
79 executables produced by GHC do not have segmentation faults. Thus, it is
80 useful to be able to reason about System FC independently of reading the code.
81 To this purpose, there is a document core-spec.pdf built in docs/core-spec that
82 contains a formalism of the types and functions dealt with here. If you change
83 just about anything in this file or you change other types/functions throughout
84 the Core language (all signposted to this note), you should update that
85 formalism. See docs/core-spec/README for more info about how to do so.
86
87 Note [check vs lint]
88 ~~~~~~~~~~~~~~~~~~~~
89 This file implements both a type checking algorithm and also general sanity
90 checking. For example, the "sanity checking" checks for TyConApp on the left
91 of an AppTy, which should never happen. These sanity checks don't really
92 affect any notion of type soundness. Yet, it is convenient to do the sanity
93 checks at the same time as the type checks. So, we use the following naming
94 convention:
95
96 - Functions that begin with 'lint'... are involved in type checking. These
97 functions might also do some sanity checking.
98
99 - Functions that begin with 'check'... are *not* involved in type checking.
100 They exist only for sanity checking.
101
102 Issues surrounding variable naming, shadowing, and such are considered *not*
103 to be part of type checking, as the formalism omits these details.
104
105 Summary of checks
106 ~~~~~~~~~~~~~~~~~
107 Checks that a set of core bindings is well-formed. The PprStyle and String
108 just control what we print in the event of an error. The Bool value
109 indicates whether we have done any specialisation yet (in which case we do
110 some extra checks).
111
112 We check for
113 (a) type errors
114 (b) Out-of-scope type variables
115 (c) Out-of-scope local variables
116 (d) Ill-kinded types
117 (e) Incorrect unsafe coercions
118
119 If we have done specialisation the we check that there are
120 (a) No top-level bindings of primitive (unboxed type)
121
122 Outstanding issues:
123
124 -- Things are *not* OK if:
125 --
126 -- * Unsaturated type app before specialisation has been done;
127 --
128 -- * Oversaturated type app after specialisation (eta reduction
129 -- may well be happening...);
130
131
132 Note [Linting type lets]
133 ~~~~~~~~~~~~~~~~~~~~~~~~
134 In the desugarer, it's very very convenient to be able to say (in effect)
135 let a = Type Int in <body>
136 That is, use a type let. See Note [Type let] in CoreSyn.
137
138 However, when linting <body> we need to remember that a=Int, else we might
139 reject a correct program. So we carry a type substitution (in this example
140 [a -> Int]) and apply this substitution before comparing types. The functin
141 lintInTy :: Type -> LintM (Type, Kind)
142 returns a substituted type.
143
144 When we encounter a binder (like x::a) we must apply the substitution
145 to the type of the binding variable. lintBinders does this.
146
147 For Ids, the type-substituted Id is added to the in_scope set (which
148 itself is part of the TCvSubst we are carrying down), and when we
149 find an occurrence of an Id, we fetch it from the in-scope set.
150
151 Note [Bad unsafe coercion]
152 ~~~~~~~~~~~~~~~~~~~~~~~~~~
153
154 For discussion see https://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions
155 Linter introduces additional rules that checks improper coercion between
156 different types, called bad coercions. Following coercions are forbidden:
157
158 (a) coercions between boxed and unboxed values;
159 (b) coercions between unlifted values of the different sizes, here
160 active size is checked, i.e. size of the actual value but not
161 the space allocated for value;
162 (c) coercions between floating and integral boxed values, this check
163 is not yet supported for unboxed tuples, as no semantics were
164 specified for that;
165 (d) coercions from / to vector type
166 (e) If types are unboxed tuples then tuple (# A_1,..,A_n #) can be
167 coerced to (# B_1,..,B_m #) if n=m and for each pair A_i, B_i rules
168 (a-e) holds.
169
170 ************************************************************************
171 * *
172 Beginning and ending passes
173 * *
174 ************************************************************************
175
176 These functions are not CoreM monad stuff, but they probably ought to
177 be, and it makes a conveneint place. place for them. They print out
178 stuff before and after core passes, and do Core Lint when necessary.
179 -}
180
181 endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> CoreM ()
182 endPass pass binds rules
183 = do { hsc_env <- getHscEnv
184 ; print_unqual <- getPrintUnqualified
185 ; liftIO $ endPassIO hsc_env print_unqual pass binds rules }
186
187 endPassIO :: HscEnv -> PrintUnqualified
188 -> CoreToDo -> CoreProgram -> [CoreRule] -> IO ()
189 -- Used by the IO-is CorePrep too
190 endPassIO hsc_env print_unqual pass binds rules
191 = do { dumpPassResult dflags print_unqual mb_flag
192 (ppr pass) (pprPassDetails pass) binds rules
193 ; lintPassResult hsc_env pass binds }
194 where
195 dflags = hsc_dflags hsc_env
196 mb_flag = case coreDumpFlag pass of
197 Just flag | dopt flag dflags -> Just flag
198 | dopt Opt_D_verbose_core2core dflags -> Just flag
199 _ -> Nothing
200
201 dumpIfSet :: DynFlags -> Bool -> CoreToDo -> SDoc -> SDoc -> IO ()
202 dumpIfSet dflags dump_me pass extra_info doc
203 = Err.dumpIfSet dflags dump_me (showSDoc dflags (ppr pass <+> extra_info)) doc
204
205 dumpPassResult :: DynFlags
206 -> PrintUnqualified
207 -> Maybe DumpFlag -- Just df => show details in a file whose
208 -- name is specified by df
209 -> SDoc -- Header
210 -> SDoc -- Extra info to appear after header
211 -> CoreProgram -> [CoreRule]
212 -> IO ()
213 dumpPassResult dflags unqual mb_flag hdr extra_info binds rules
214 = do { forM_ mb_flag $ \flag ->
215 Err.dumpSDoc dflags unqual flag (showSDoc dflags hdr) dump_doc
216
217 -- Report result size
218 -- This has the side effect of forcing the intermediate to be evaluated
219 -- if it's not already forced by a -ddump flag.
220 ; Err.debugTraceMsg dflags 2 size_doc
221 }
222
223 where
224 size_doc = sep [text "Result size of" <+> hdr, nest 2 (equals <+> ppr (coreBindsStats binds))]
225
226 dump_doc = vcat [ nest 2 extra_info
227 , size_doc
228 , blankLine
229 , pprCoreBindingsWithSize binds
230 , ppUnless (null rules) pp_rules ]
231 pp_rules = vcat [ blankLine
232 , text "------ Local rules for imported ids --------"
233 , pprRules rules ]
234
235 coreDumpFlag :: CoreToDo -> Maybe DumpFlag
236 coreDumpFlag (CoreDoSimplify {}) = Just Opt_D_verbose_core2core
237 coreDumpFlag (CoreDoPluginPass {}) = Just Opt_D_verbose_core2core
238 coreDumpFlag CoreDoFloatInwards = Just Opt_D_verbose_core2core
239 coreDumpFlag (CoreDoFloatOutwards {}) = Just Opt_D_verbose_core2core
240 coreDumpFlag CoreLiberateCase = Just Opt_D_verbose_core2core
241 coreDumpFlag CoreDoStaticArgs = Just Opt_D_verbose_core2core
242 coreDumpFlag CoreDoCallArity = Just Opt_D_dump_call_arity
243 coreDumpFlag CoreDoStrictness = Just Opt_D_dump_stranal
244 coreDumpFlag CoreDoWorkerWrapper = Just Opt_D_dump_worker_wrapper
245 coreDumpFlag CoreDoSpecialising = Just Opt_D_dump_spec
246 coreDumpFlag CoreDoSpecConstr = Just Opt_D_dump_spec
247 coreDumpFlag CoreCSE = Just Opt_D_dump_cse
248 coreDumpFlag CoreDoVectorisation = Just Opt_D_dump_vect
249 coreDumpFlag CoreDesugar = Just Opt_D_dump_ds
250 coreDumpFlag CoreDesugarOpt = Just Opt_D_dump_ds
251 coreDumpFlag CoreTidy = Just Opt_D_dump_simpl
252 coreDumpFlag CorePrep = Just Opt_D_dump_prep
253
254 coreDumpFlag CoreDoPrintCore = Nothing
255 coreDumpFlag (CoreDoRuleCheck {}) = Nothing
256 coreDumpFlag CoreDoNothing = Nothing
257 coreDumpFlag (CoreDoPasses {}) = Nothing
258
259 {-
260 ************************************************************************
261 * *
262 Top-level interfaces
263 * *
264 ************************************************************************
265 -}
266
267 lintPassResult :: HscEnv -> CoreToDo -> CoreProgram -> IO ()
268 lintPassResult hsc_env pass binds
269 | not (gopt Opt_DoCoreLinting dflags)
270 = return ()
271 | otherwise
272 = do { let (warns, errs) = lintCoreBindings dflags pass (interactiveInScope hsc_env) binds
273 ; Err.showPass dflags ("Core Linted result of " ++ showPpr dflags pass)
274 ; displayLintResults dflags pass warns errs binds }
275 where
276 dflags = hsc_dflags hsc_env
277
278 displayLintResults :: DynFlags -> CoreToDo
279 -> Bag Err.MsgDoc -> Bag Err.MsgDoc -> CoreProgram
280 -> IO ()
281 displayLintResults dflags pass warns errs binds
282 | not (isEmptyBag errs)
283 = do { log_action dflags dflags NoReason Err.SevDump noSrcSpan defaultDumpStyle
284 (vcat [ lint_banner "errors" (ppr pass), Err.pprMessageBag errs
285 , text "*** Offending Program ***"
286 , pprCoreBindings binds
287 , text "*** End of Offense ***" ])
288 ; Err.ghcExit dflags 1 }
289
290 | not (isEmptyBag warns)
291 , not opt_NoDebugOutput
292 , showLintWarnings pass
293 = log_action dflags dflags NoReason Err.SevDump noSrcSpan defaultDumpStyle
294 (lint_banner "warnings" (ppr pass) $$ Err.pprMessageBag warns)
295
296 | otherwise = return ()
297 where
298
299 lint_banner :: String -> SDoc -> SDoc
300 lint_banner string pass = text "*** Core Lint" <+> text string
301 <+> text ": in result of" <+> pass
302 <+> text "***"
303
304 showLintWarnings :: CoreToDo -> Bool
305 -- Disable Lint warnings on the first simplifier pass, because
306 -- there may be some INLINE knots still tied, which is tiresomely noisy
307 showLintWarnings (CoreDoSimplify _ (SimplMode { sm_phase = InitialPhase })) = False
308 showLintWarnings _ = True
309
310 lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO ()
311 lintInteractiveExpr what hsc_env expr
312 | not (gopt Opt_DoCoreLinting dflags)
313 = return ()
314 | Just err <- lintExpr dflags (interactiveInScope hsc_env) expr
315 = do { display_lint_err err
316 ; Err.ghcExit dflags 1 }
317 | otherwise
318 = return ()
319 where
320 dflags = hsc_dflags hsc_env
321
322 display_lint_err err
323 = do { log_action dflags dflags NoReason Err.SevDump
324 noSrcSpan defaultDumpStyle
325 (vcat [ lint_banner "errors" (text what)
326 , err
327 , text "*** Offending Program ***"
328 , pprCoreExpr expr
329 , text "*** End of Offense ***" ])
330 ; Err.ghcExit dflags 1 }
331
332 interactiveInScope :: HscEnv -> [Var]
333 -- In GHCi we may lint expressions, or bindings arising from 'deriving'
334 -- clauses, that mention variables bound in the interactive context.
335 -- These are Local things (see Note [Interactively-bound Ids in GHCi] in HscTypes).
336 -- So we have to tell Lint about them, lest it reports them as out of scope.
337 --
338 -- We do this by find local-named things that may appear free in interactive
339 -- context. This function is pretty revolting and quite possibly not quite right.
340 -- When we are not in GHCi, the interactive context (hsc_IC hsc_env) is empty
341 -- so this is a (cheap) no-op.
342 --
343 -- See Trac #8215 for an example
344 interactiveInScope hsc_env
345 = tyvars ++ ids
346 where
347 -- C.f. TcRnDriver.setInteractiveContext, Desugar.deSugarExpr
348 ictxt = hsc_IC hsc_env
349 (cls_insts, _fam_insts) = ic_instances ictxt
350 te1 = mkTypeEnvWithImplicits (ic_tythings ictxt)
351 te = extendTypeEnvWithIds te1 (map instanceDFunId cls_insts)
352 ids = typeEnvIds te
353 tyvars = tyCoVarsOfTypesList $ map idType ids
354 -- Why the type variables? How can the top level envt have free tyvars?
355 -- I think it's because of the GHCi debugger, which can bind variables
356 -- f :: [t] -> [t]
357 -- where t is a RuntimeUnk (see TcType)
358
359 lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
360 -- Returns (warnings, errors)
361 -- If you edit this function, you may need to update the GHC formalism
362 -- See Note [GHC Formalism]
363 lintCoreBindings dflags pass local_in_scope binds
364 = initL dflags flags $
365 addLoc TopLevelBindings $
366 addInScopeVars local_in_scope $
367 addInScopeVars binders $
368 -- Put all the top-level binders in scope at the start
369 -- This is because transformation rules can bring something
370 -- into use 'unexpectedly'
371 do { checkL (null dups) (dupVars dups)
372 ; checkL (null ext_dups) (dupExtVars ext_dups)
373 ; mapM lint_bind binds }
374 where
375 flags = LF { lf_check_global_ids = check_globals
376 , lf_check_inline_loop_breakers = check_lbs
377 , lf_check_static_ptrs = check_static_ptrs }
378
379 -- See Note [Checking for global Ids]
380 check_globals = case pass of
381 CoreTidy -> False
382 CorePrep -> False
383 _ -> True
384
385 -- See Note [Checking for INLINE loop breakers]
386 check_lbs = case pass of
387 CoreDesugar -> False
388 CoreDesugarOpt -> False
389 _ -> True
390
391 -- See Note [Checking StaticPtrs]
392 check_static_ptrs | not (xopt LangExt.StaticPointers dflags) = AllowAnywhere
393 | otherwise = case pass of
394 CoreDoFloatOutwards _ -> AllowAtTopLevel
395 CoreTidy -> RejectEverywhere
396 CorePrep -> AllowAtTopLevel
397 _ -> AllowAnywhere
398
399 binders = bindersOfBinds binds
400 (_, dups) = removeDups compare binders
401
402 -- dups_ext checks for names with different uniques
403 -- but but the same External name M.n. We don't
404 -- allow this at top level:
405 -- M.n{r3} = ...
406 -- M.n{r29} = ...
407 -- because they both get the same linker symbol
408 ext_dups = snd (removeDups ord_ext (map Var.varName binders))
409 ord_ext n1 n2 | Just m1 <- nameModule_maybe n1
410 , Just m2 <- nameModule_maybe n2
411 = compare (m1, nameOccName n1) (m2, nameOccName n2)
412 | otherwise = LT
413
414 -- If you edit this function, you may need to update the GHC formalism
415 -- See Note [GHC Formalism]
416 lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
417 lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
418
419 {-
420 ************************************************************************
421 * *
422 \subsection[lintUnfolding]{lintUnfolding}
423 * *
424 ************************************************************************
425
426 We use this to check all unfoldings that come in from interfaces
427 (it is very painful to catch errors otherwise):
428 -}
429
430 lintUnfolding :: DynFlags
431 -> SrcLoc
432 -> VarSet -- Treat these as in scope
433 -> CoreExpr
434 -> Maybe MsgDoc -- Nothing => OK
435
436 lintUnfolding dflags locn vars expr
437 | isEmptyBag errs = Nothing
438 | otherwise = Just (pprMessageBag errs)
439 where
440 (_warns, errs) = initL dflags defaultLintFlags linter
441 linter = addLoc (ImportedUnfolding locn) $
442 addInScopeVarSet vars $
443 lintCoreExpr expr
444
445 lintExpr :: DynFlags
446 -> [Var] -- Treat these as in scope
447 -> CoreExpr
448 -> Maybe MsgDoc -- Nothing => OK
449
450 lintExpr dflags vars expr
451 | isEmptyBag errs = Nothing
452 | otherwise = Just (pprMessageBag errs)
453 where
454 (_warns, errs) = initL dflags defaultLintFlags linter
455 linter = addLoc TopLevelBindings $
456 addInScopeVars vars $
457 lintCoreExpr expr
458
459 {-
460 ************************************************************************
461 * *
462 \subsection[lintCoreBinding]{lintCoreBinding}
463 * *
464 ************************************************************************
465
466 Check a core binding, returning the list of variables bound.
467 -}
468
469 lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
470 -- If you edit this function, you may need to update the GHC formalism
471 -- See Note [GHC Formalism]
472 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
473 = addLoc (RhsOf binder) $
474 -- Check the rhs
475 do { ty <- lintRhs rhs
476 ; lint_bndr binder -- Check match to RHS type
477 ; binder_ty <- applySubstTy (idType binder)
478 ; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty)
479
480 -- Check the let/app invariant
481 -- See Note [CoreSyn let/app invariant] in CoreSyn
482 ; checkL (not (isUnliftedType binder_ty)
483 || (isNonRec rec_flag && exprOkForSpeculation rhs))
484 (mkRhsPrimMsg binder rhs)
485
486 -- Check that if the binder is top-level or recursive, it's not demanded
487 ; checkL (not (isStrictId binder)
488 || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
489 (mkStrictMsg binder)
490
491 ; flags <- getLintFlags
492 ; when (lf_check_inline_loop_breakers flags
493 && isStrongLoopBreaker (idOccInfo binder)
494 && isInlinePragma (idInlinePragma binder))
495 (addWarnL (text "INLINE binder is (non-rule) loop breaker:" <+> ppr binder))
496 -- Only non-rule loop breakers inhibit inlining
497
498 -- Check whether arity and demand type are consistent (only if demand analysis
499 -- already happened)
500 --
501 -- Note (Apr 2014): this is actually ok. See Note [Demand analysis for trivial right-hand sides]
502 -- in DmdAnal. After eta-expansion in CorePrep the rhs is no longer trivial.
503 -- ; let dmdTy = idStrictness binder
504 -- ; checkL (case dmdTy of
505 -- StrictSig dmd_ty -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs)
506 -- (mkArityMsg binder)
507
508 -- Check that the binder's arity is within the bounds imposed by
509 -- the type and the strictness signature. See Note [exprArity invariant]
510 -- and Note [Trimming arity]
511 ; checkL (idArity binder <= length (typeArity (idType binder)))
512 (text "idArity" <+> ppr (idArity binder) <+>
513 text "exceeds typeArity" <+>
514 ppr (length (typeArity (idType binder))) <> colon <+>
515 ppr binder)
516
517 ; case splitStrictSig (idStrictness binder) of
518 (demands, result_info) | isBotRes result_info ->
519 checkL (idArity binder <= length demands)
520 (text "idArity" <+> ppr (idArity binder) <+>
521 text "exceeds arity imposed by the strictness signature" <+>
522 ppr (idStrictness binder) <> colon <+>
523 ppr binder)
524 _ -> return ()
525
526 ; mapM_ (lintCoreRule binder_ty) (idCoreRules binder)
527 ; lintIdUnfolding binder binder_ty (idUnfolding binder) }
528
529 -- We should check the unfolding, if any, but this is tricky because
530 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
531 where
532 -- If you edit this function, you may need to update the GHC formalism
533 -- See Note [GHC Formalism]
534 lint_bndr var | isId var = lintIdBndr top_lvl_flag var $ \_ -> return ()
535 | otherwise = return ()
536
537 -- | Checks the RHS of top-level bindings. It only differs from 'lintCoreExpr'
538 -- in that it doesn't reject occurrences of the function 'makeStatic' when they
539 -- appear at the top level and @lf_check_static_ptrs == AllowAtTopLevel@.
540 --
541 -- See Note [Checking StaticPtrs].
542 lintRhs :: CoreExpr -> LintM OutType
543 lintRhs rhs = fmap lf_check_static_ptrs getLintFlags >>= go
544 where
545 -- Allow occurrences of 'makeStatic' at the top-level but produce errors
546 -- otherwise.
547 go AllowAtTopLevel
548 | (binders0, rhs') <- collectTyBinders rhs
549 , Just (fun, t, info, e) <- collectMakeStaticArgs rhs'
550 = foldr
551 -- imitate @lintCoreExpr (Lam ...)@
552 (\var loopBinders ->
553 addLoc (LambdaBodyOf var) $
554 lintBinder var $ \var' ->
555 do { body_ty <- loopBinders
556 ; return $ mkLamType var' body_ty }
557 )
558 -- imitate @lintCoreExpr (App ...)@
559 (do fun_ty <- lintCoreExpr fun
560 addLoc (AnExpr rhs') $ lintCoreArgs fun_ty [Type t, info, e]
561 )
562 binders0
563 go _ = lintCoreExpr rhs
564
565 lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
566 lintIdUnfolding bndr bndr_ty (CoreUnfolding { uf_tmpl = rhs, uf_src = src })
567 | isStableSource src
568 = do { ty <- lintCoreExpr rhs
569 ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) }
570
571 lintIdUnfolding bndr bndr_ty (DFunUnfolding { df_con = con, df_bndrs = bndrs
572 , df_args = args })
573 = do { ty <- lintBinders bndrs $ \ bndrs' ->
574 do { res_ty <- lintCoreArgs (dataConRepType con) args
575 ; return (mkLamTypes bndrs' res_ty) }
576 ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "dfun unfolding") ty) }
577
578 lintIdUnfolding _ _ _
579 = return () -- Do not Lint unstable unfoldings, because that leads
580 -- to exponential behaviour; c.f. CoreFVs.idUnfoldingVars
581
582 {-
583 Note [Checking for INLINE loop breakers]
584 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
585 It's very suspicious if a strong loop breaker is marked INLINE.
586
587 However, the desugarer generates instance methods with INLINE pragmas
588 that form a mutually recursive group. Only after a round of
589 simplification are they unravelled. So we suppress the test for
590 the desugarer.
591
592 ************************************************************************
593 * *
594 \subsection[lintCoreExpr]{lintCoreExpr}
595 * *
596 ************************************************************************
597 -}
598
599 -- For OutType, OutKind, the substitution has been applied,
600 -- but has not been linted yet
601
602 type LintedType = Type -- Substitution applied, and type is linted
603 type LintedKind = Kind
604
605 lintCoreExpr :: CoreExpr -> LintM OutType
606 -- The returned type has the substitution from the monad
607 -- already applied to it:
608 -- lintCoreExpr e subst = exprType (subst e)
609 --
610 -- The returned "type" can be a kind, if the expression is (Type ty)
611
612 -- If you edit this function, you may need to update the GHC formalism
613 -- See Note [GHC Formalism]
614 lintCoreExpr (Var var)
615 = do { checkL (isNonCoVarId var)
616 (text "Non term variable" <+> ppr var)
617
618 ; checkDeadIdOcc var
619 ; var' <- lookupIdInScope var
620 ; return (idType var') }
621
622 lintCoreExpr (Lit lit)
623 = return (literalType lit)
624
625 lintCoreExpr (Cast expr co)
626 = do { expr_ty <- lintCoreExpr expr
627 ; co' <- applySubstCo co
628 ; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
629 ; lintL (classifiesTypeWithValues k2)
630 (text "Target of cast not # or *:" <+> ppr co)
631 ; lintRole co' Representational r
632 ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
633 ; return to_ty }
634
635 lintCoreExpr (Tick (Breakpoint _ ids) expr)
636 = do forM_ ids $ \id -> do
637 checkDeadIdOcc id
638 lookupIdInScope id
639 lintCoreExpr expr
640
641 lintCoreExpr (Tick _other_tickish expr)
642 = lintCoreExpr expr
643
644 lintCoreExpr (Let (NonRec tv (Type ty)) body)
645 | isTyVar tv
646 = -- See Note [Linting type lets]
647 do { ty' <- applySubstTy ty
648 ; lintTyBndr tv $ \ tv' ->
649 do { addLoc (RhsOf tv) $ lintTyKind tv' ty'
650 -- Now extend the substitution so we
651 -- take advantage of it in the body
652 ; extendSubstL tv' ty' $
653 addLoc (BodyOfLetRec [tv]) $
654 lintCoreExpr body } }
655
656 lintCoreExpr (Let (NonRec bndr rhs) body)
657 | isId bndr
658 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
659 ; addLoc (BodyOfLetRec [bndr])
660 (lintIdBndr NotTopLevel bndr $ \_ -> lintCoreExpr body) }
661
662 | otherwise
663 = failWithL (mkLetErr bndr rhs) -- Not quite accurate
664
665 lintCoreExpr (Let (Rec pairs) body)
666 = lintIdBndrs bndrs $ \_ ->
667 do { checkL (null dups) (dupVars dups)
668 ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
669 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
670 where
671 bndrs = map fst pairs
672 (_, dups) = removeDups compare bndrs
673
674 lintCoreExpr e@(App _ _)
675 = do lf <- getLintFlags
676 -- Check for a nested occurrence of the StaticPtr constructor.
677 -- See Note [Checking StaticPtrs].
678 case fun of
679 Var b | lf_check_static_ptrs lf /= AllowAnywhere
680 , idName b == makeStaticName
681 -> do
682 failWithL $ text "Found makeStatic nested in an expression: " <+>
683 ppr e
684 _ -> go
685 where
686 go = do { fun_ty <- lintCoreExpr fun
687 ; addLoc (AnExpr e) $ lintCoreArgs fun_ty args }
688
689 (fun, args) = collectArgs e
690
691 lintCoreExpr (Lam var expr)
692 = addLoc (LambdaBodyOf var) $
693 lintBinder var $ \ var' ->
694 do { body_ty <- lintCoreExpr expr
695 ; return $ mkLamType var' body_ty }
696
697 lintCoreExpr e@(Case scrut var alt_ty alts) =
698 -- Check the scrutinee
699 do { let scrut_diverges = exprIsBottom scrut
700 ; scrut_ty <- lintCoreExpr scrut
701 ; (alt_ty, _) <- lintInTy alt_ty
702 ; (var_ty, _) <- lintInTy (idType var)
703
704 -- See Note [No alternatives lint check]
705 ; when (null alts) $
706 do { checkL (not (exprIsHNF scrut))
707 (text "No alternatives for a case scrutinee in head-normal form:" <+> ppr scrut)
708 ; checkWarnL scrut_diverges
709 (text "No alternatives for a case scrutinee not known to diverge for sure:" <+> ppr scrut)
710 }
711
712 -- See Note [Rules for floating-point comparisons] in PrelRules
713 ; let isLitPat (LitAlt _, _ , _) = True
714 isLitPat _ = False
715 ; checkL (not $ isFloatingTy scrut_ty && any isLitPat alts)
716 (ptext (sLit $ "Lint warning: Scrutinising floating-point " ++
717 "expression with literal pattern in case " ++
718 "analysis (see Trac #9238).")
719 $$ text "scrut" <+> ppr scrut)
720
721 ; case tyConAppTyCon_maybe (idType var) of
722 Just tycon
723 | debugIsOn
724 , isAlgTyCon tycon
725 , not (isAbstractTyCon tycon)
726 , null (tyConDataCons tycon)
727 , not scrut_diverges
728 -> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
729 -- This can legitimately happen for type families
730 $ return ()
731 _otherwise -> return ()
732
733 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
734
735 ; subst <- getTCvSubst
736 ; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
737
738 ; lintIdBndr NotTopLevel var $ \_ ->
739 do { -- Check the alternatives
740 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
741 ; checkCaseAlts e scrut_ty alts
742 ; return alt_ty } }
743
744 -- This case can't happen; linting types in expressions gets routed through
745 -- lintCoreArgs
746 lintCoreExpr (Type ty)
747 = failWithL (text "Type found as expression" <+> ppr ty)
748
749 lintCoreExpr (Coercion co)
750 = do { (k1, k2, ty1, ty2, role) <- lintInCo co
751 ; return (mkHeteroCoercionType role k1 k2 ty1 ty2) }
752
753 {-
754 Note [No alternatives lint check]
755 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
756 Case expressions with no alternatives are odd beasts, and worth looking at
757 in the linter (cf Trac #10180). We check two things:
758
759 * exprIsHNF is false: certainly, it would be terribly wrong if the
760 scrutinee was already in head normal form.
761
762 * exprIsBottom is true: we should be able to see why GHC believes the
763 scrutinee is diverging for sure.
764
765 In principle, the first check is redundant: exprIsBottom == True will
766 always imply exprIsHNF == False. But the first check is reliable: If
767 exprIsHNF == True, then there definitely is a problem (exprIsHNF errs
768 on the right side). If the second check triggers then it may be the
769 case that the compiler got smarter elsewhere, and the empty case is
770 correct, but that exprIsBottom is unable to see it. In particular, the
771 empty-type check in exprIsBottom is an approximation. Therefore, this
772 check is not fully reliable, and we keep both around.
773
774 ************************************************************************
775 * *
776 \subsection[lintCoreArgs]{lintCoreArgs}
777 * *
778 ************************************************************************
779
780 The basic version of these functions checks that the argument is a
781 subtype of the required type, as one would expect.
782 -}
783
784
785 lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
786 lintCoreArgs fun_ty args = foldM lintCoreArg fun_ty args
787
788 lintCoreArg :: OutType -> CoreArg -> LintM OutType
789 lintCoreArg fun_ty (Type arg_ty)
790 = do { checkL (not (isCoercionTy arg_ty))
791 (text "Unnecessary coercion-to-type injection:"
792 <+> ppr arg_ty)
793 ; arg_ty' <- applySubstTy arg_ty
794 ; lintTyApp fun_ty arg_ty' }
795
796 lintCoreArg fun_ty arg
797 = do { arg_ty <- lintCoreExpr arg
798 -- See Note [Levity polymorphism invariants] in CoreSyn
799 ; lintL (not (isTypeLevPoly arg_ty))
800 (text "Levity-polymorphic argument:" <+>
801 (ppr arg <+> dcolon <+> parens (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))))
802 -- check for levity polymorphism first, because otherwise isUnliftedType panics
803
804 ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
805 (mkLetAppMsg arg)
806 ; lintValApp arg fun_ty arg_ty }
807
808 -----------------
809 lintAltBinders :: OutType -- Scrutinee type
810 -> OutType -- Constructor type
811 -> [OutVar] -- Binders
812 -> LintM ()
813 -- If you edit this function, you may need to update the GHC formalism
814 -- See Note [GHC Formalism]
815 lintAltBinders scrut_ty con_ty []
816 = ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
817 lintAltBinders scrut_ty con_ty (bndr:bndrs)
818 | isTyVar bndr
819 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
820 ; lintAltBinders scrut_ty con_ty' bndrs }
821 | otherwise
822 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
823 ; lintAltBinders scrut_ty con_ty' bndrs }
824
825 -----------------
826 lintTyApp :: OutType -> OutType -> LintM OutType
827 lintTyApp fun_ty arg_ty
828 | Just (tv,body_ty) <- splitForAllTy_maybe fun_ty
829 = do { lintTyKind tv arg_ty
830 ; in_scope <- getInScope
831 -- substTy needs the set of tyvars in scope to avoid generating
832 -- uniques that are already in scope.
833 -- See Note [The substitution invariant] in TyCoRep
834 ; return (substTyWithInScope in_scope [tv] [arg_ty] body_ty) }
835
836 | otherwise
837 = failWithL (mkTyAppMsg fun_ty arg_ty)
838
839 -----------------
840 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
841 lintValApp arg fun_ty arg_ty
842 | Just (arg,res) <- splitFunTy_maybe fun_ty
843 = do { ensureEqTys arg arg_ty err1
844 ; return res }
845 | otherwise
846 = failWithL err2
847 where
848 err1 = mkAppMsg fun_ty arg_ty arg
849 err2 = mkNonFunAppMsg fun_ty arg_ty arg
850
851 lintTyKind :: OutTyVar -> OutType -> LintM ()
852 -- Both args have had substitution applied
853
854 -- If you edit this function, you may need to update the GHC formalism
855 -- See Note [GHC Formalism]
856 lintTyKind tyvar arg_ty
857 -- Arg type might be boxed for a function with an uncommitted
858 -- tyvar; notably this is used so that we can give
859 -- error :: forall a:*. String -> a
860 -- and then apply it to both boxed and unboxed types.
861 = do { arg_kind <- lintType arg_ty
862 ; unless (arg_kind `eqType` tyvar_kind)
863 (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
864 where
865 tyvar_kind = tyVarKind tyvar
866
867 checkDeadIdOcc :: Id -> LintM ()
868 -- Occurrences of an Id should never be dead....
869 -- except when we are checking a case pattern
870 checkDeadIdOcc id
871 | isDeadOcc (idOccInfo id)
872 = do { in_case <- inCasePat
873 ; checkL in_case
874 (text "Occurrence of a dead Id" <+> ppr id) }
875 | otherwise
876 = return ()
877
878 {-
879 ************************************************************************
880 * *
881 \subsection[lintCoreAlts]{lintCoreAlts}
882 * *
883 ************************************************************************
884 -}
885
886 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
887 -- a) Check that the alts are non-empty
888 -- b1) Check that the DEFAULT comes first, if it exists
889 -- b2) Check that the others are in increasing order
890 -- c) Check that there's a default for infinite types
891 -- NB: Algebraic cases are not necessarily exhaustive, because
892 -- the simplifier correctly eliminates case that can't
893 -- possibly match.
894
895 checkCaseAlts e ty alts =
896 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
897 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
898
899 -- For types Int#, Word# with an infinite (well, large!) number of
900 -- possible values, there should usually be a DEFAULT case
901 -- But (see Note [Empty case alternatives] in CoreSyn) it's ok to
902 -- have *no* case alternatives.
903 -- In effect, this is a kind of partial test. I suppose it's possible
904 -- that we might *know* that 'x' was 1 or 2, in which case
905 -- case x of { 1 -> e1; 2 -> e2 }
906 -- would be fine.
907 ; checkL (isJust maybe_deflt || not is_infinite_ty || null alts)
908 (nonExhaustiveAltsMsg e) }
909 where
910 (con_alts, maybe_deflt) = findDefault alts
911
912 -- Check that successive alternatives have increasing tags
913 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
914 increasing_tag _ = True
915
916 non_deflt (DEFAULT, _, _) = False
917 non_deflt _ = True
918
919 is_infinite_ty = case tyConAppTyCon_maybe ty of
920 Nothing -> False
921 Just tycon -> isPrimTyCon tycon
922
923 lintAltExpr :: CoreExpr -> OutType -> LintM ()
924 lintAltExpr expr ann_ty
925 = do { actual_ty <- lintCoreExpr expr
926 ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
927
928 lintCoreAlt :: OutType -- Type of scrutinee
929 -> OutType -- Type of the alternative
930 -> CoreAlt
931 -> LintM ()
932 -- If you edit this function, you may need to update the GHC formalism
933 -- See Note [GHC Formalism]
934 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
935 do { lintL (null args) (mkDefaultArgsMsg args)
936 ; lintAltExpr rhs alt_ty }
937
938 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
939 | litIsLifted lit
940 = failWithL integerScrutinisedMsg
941 | otherwise
942 = do { lintL (null args) (mkDefaultArgsMsg args)
943 ; ensureEqTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
944 ; lintAltExpr rhs alt_ty }
945 where
946 lit_ty = literalType lit
947
948 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
949 | isNewTyCon (dataConTyCon con)
950 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
951 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
952 = addLoc (CaseAlt alt) $ do
953 { -- First instantiate the universally quantified
954 -- type variables of the data constructor
955 -- We've already check
956 lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
957 ; let con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys
958
959 -- And now bring the new binders into scope
960 ; lintBinders args $ \ args' -> do
961 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
962 ; lintAltExpr rhs alt_ty } }
963
964 | otherwise -- Scrut-ty is wrong shape
965 = addErrL (mkBadAltMsg scrut_ty alt)
966
967 {-
968 ************************************************************************
969 * *
970 \subsection[lint-types]{Types}
971 * *
972 ************************************************************************
973 -}
974
975 -- When we lint binders, we (one at a time and in order):
976 -- 1. Lint var types or kinds (possibly substituting)
977 -- 2. Add the binder to the in scope set, and if its a coercion var,
978 -- we may extend the substitution to reflect its (possibly) new kind
979 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
980 lintBinders [] linterF = linterF []
981 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
982 lintBinders vars $ \ vars' ->
983 linterF (var':vars')
984
985 -- If you edit this function, you may need to update the GHC formalism
986 -- See Note [GHC Formalism]
987 lintBinder :: Var -> (Var -> LintM a) -> LintM a
988 lintBinder var linterF
989 | isTyVar var = lintTyBndr var linterF
990 | isCoVar var = lintCoBndr var linterF
991 | otherwise = lintIdBndr NotTopLevel var linterF
992
993 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
994 lintTyBndr tv thing_inside
995 = do { subst <- getTCvSubst
996 ; let (subst', tv') = substTyVarBndr subst tv
997 ; lintKind (varType tv')
998 ; updateTCvSubst subst' (thing_inside tv') }
999
1000 lintCoBndr :: InCoVar -> (OutCoVar -> LintM a) -> LintM a
1001 lintCoBndr cv thing_inside
1002 = do { subst <- getTCvSubst
1003 ; let (subst', cv') = substCoVarBndr subst cv
1004 ; lintKind (varType cv')
1005 ; lintL (isCoercionType (varType cv'))
1006 (text "CoVar with non-coercion type:" <+> pprTyVar cv)
1007 ; updateTCvSubst subst' (thing_inside cv') }
1008
1009 lintIdBndrs :: [Var] -> ([Var] -> LintM a) -> LintM a
1010 lintIdBndrs ids linterF
1011 = go ids
1012 where
1013 go [] = linterF []
1014 go (id:ids) = lintIdBndr NotTopLevel id $ \id ->
1015 lintIdBndrs ids $ \ids ->
1016 linterF (id:ids)
1017
1018 lintIdBndr :: TopLevelFlag -> InVar -> (OutVar -> LintM a) -> LintM a
1019 -- Do substitution on the type of a binder and add the var with this
1020 -- new type to the in-scope set of the second argument
1021 -- ToDo: lint its rules
1022 lintIdBndr top_lvl id linterF
1023 = do { flags <- getLintFlags
1024 ; checkL (not (lf_check_global_ids flags) || isLocalId id)
1025 (text "Non-local Id binder" <+> ppr id)
1026 -- See Note [Checking for global Ids]
1027
1028 -- Check that if the binder is nested, it is not marked as exported
1029 ; checkL (not (isExportedId id) || isTopLevel top_lvl)
1030 (mkNonTopExportedMsg id)
1031
1032 -- Check that if the binder is nested, it does not have an external name
1033 ; checkL (not (isExternalName (Var.varName id)) || isTopLevel top_lvl)
1034 (mkNonTopExternalNameMsg id)
1035
1036 ; (ty, k) <- lintInTy (idType id)
1037 -- See Note [Levity polymorphism invariants] in CoreSyn
1038 ; lintL (not (isKindLevPoly k))
1039 (text "Levity-polymorphic binder:" <+>
1040 (ppr id <+> dcolon <+> parens (ppr ty <+> dcolon <+> ppr k)))
1041
1042 ; let id' = setIdType id ty
1043 ; addInScopeVar id' $ (linterF id') }
1044
1045 {-
1046 %************************************************************************
1047 %* *
1048 Types
1049 %* *
1050 %************************************************************************
1051 -}
1052
1053 lintInTy :: InType -> LintM (LintedType, LintedKind)
1054 -- Types only, not kinds
1055 -- Check the type, and apply the substitution to it
1056 -- See Note [Linting type lets]
1057 lintInTy ty
1058 = addLoc (InType ty) $
1059 do { ty' <- applySubstTy ty
1060 ; k <- lintType ty'
1061 ; lintKind k
1062 ; return (ty', k) }
1063
1064 checkTyCon :: TyCon -> LintM ()
1065 checkTyCon tc
1066 = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
1067
1068 -------------------
1069 lintType :: OutType -> LintM LintedKind
1070 -- The returned Kind has itself been linted
1071
1072 -- If you edit this function, you may need to update the GHC formalism
1073 -- See Note [GHC Formalism]
1074 lintType (TyVarTy tv)
1075 = do { checkL (isTyVar tv) (mkBadTyVarMsg tv)
1076 ; lintTyCoVarInScope tv
1077 ; return (tyVarKind tv) }
1078 -- We checked its kind when we added it to the envt
1079
1080 lintType ty@(AppTy t1 t2)
1081 | TyConApp {} <- t1
1082 = failWithL $ text "TyConApp to the left of AppTy:" <+> ppr ty
1083 | otherwise
1084 = do { k1 <- lintType t1
1085 ; k2 <- lintType t2
1086 ; lint_ty_app ty k1 [(t2,k2)] }
1087
1088 lintType ty@(TyConApp tc tys)
1089 | Just ty' <- coreView ty
1090 = lintType ty' -- Expand type synonyms, so that we do not bogusly complain
1091 -- about un-saturated type synonyms
1092
1093 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
1094 -- Also type synonyms and type families
1095 , length tys < tyConArity tc
1096 = failWithL (hang (text "Un-saturated type application") 2 (ppr ty))
1097
1098 | otherwise
1099 = do { checkTyCon tc
1100 ; ks <- mapM lintType tys
1101 ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
1102
1103 -- arrows can related *unlifted* kinds, so this has to be separate from
1104 -- a dependent forall.
1105 lintType ty@(FunTy t1 t2)
1106 = do { k1 <- lintType t1
1107 ; k2 <- lintType t2
1108 ; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 }
1109
1110 lintType t@(ForAllTy (TvBndr tv _vis) ty)
1111 = do { lintL (isTyVar tv) (text "Covar bound in type:" <+> ppr t)
1112 ; lintTyBndr tv $ \tv' ->
1113 do { k <- lintType ty
1114 ; lintL (not (tv' `elemVarSet` tyCoVarsOfType k))
1115 (text "Variable escape in forall:" <+> ppr t)
1116 ; lintL (classifiesTypeWithValues k)
1117 (text "Non-* and non-# kind in forall:" <+> ppr t)
1118 ; return k }}
1119
1120 lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
1121
1122 lintType (CastTy ty co)
1123 = do { k1 <- lintType ty
1124 ; (k1', k2) <- lintStarCoercion co
1125 ; ensureEqTys k1 k1' (mkCastErr ty co k1' k1)
1126 ; return k2 }
1127
1128 lintType (CoercionTy co)
1129 = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
1130 ; return $ mkHeteroCoercionType r k1 k2 ty1 ty2 }
1131
1132 lintKind :: OutKind -> LintM ()
1133 -- If you edit this function, you may need to update the GHC formalism
1134 -- See Note [GHC Formalism]
1135 lintKind k = do { sk <- lintType k
1136 ; unless (classifiesTypeWithValues sk)
1137 (addErrL (hang (text "Ill-kinded kind:" <+> ppr k)
1138 2 (text "has kind:" <+> ppr sk))) }
1139
1140 -- confirms that a type is really *
1141 lintStar :: SDoc -> OutKind -> LintM ()
1142 lintStar doc k
1143 = lintL (classifiesTypeWithValues k)
1144 (text "Non-*-like kind when *-like expected:" <+> ppr k $$
1145 text "when checking" <+> doc)
1146
1147 lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
1148 -- If you edit this function, you may need to update the GHC formalism
1149 -- See Note [GHC Formalism]
1150 lintArrow what k1 k2 -- Eg lintArrow "type or kind `blah'" k1 k2
1151 -- or lintarrow "coercion `blah'" k1 k2
1152 = do { unless (okArrowArgKind k1) (addErrL (msg (text "argument") k1))
1153 ; unless (okArrowResultKind k2) (addErrL (msg (text "result") k2))
1154 ; return liftedTypeKind }
1155 where
1156 msg ar k
1157 = vcat [ hang (text "Ill-kinded" <+> ar)
1158 2 (text "in" <+> what)
1159 , what <+> text "kind:" <+> ppr k ]
1160
1161 lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
1162 lint_ty_app ty k tys
1163 = lint_app (text "type" <+> quotes (ppr ty)) k tys
1164
1165 ----------------
1166 lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
1167 lint_co_app ty k tys
1168 = lint_app (text "coercion" <+> quotes (ppr ty)) k tys
1169
1170 ----------------
1171 lintTyLit :: TyLit -> LintM ()
1172 lintTyLit (NumTyLit n)
1173 | n >= 0 = return ()
1174 | otherwise = failWithL msg
1175 where msg = text "Negative type literal:" <+> integer n
1176 lintTyLit (StrTyLit _) = return ()
1177
1178 lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
1179 -- (lint_app d fun_kind arg_tys)
1180 -- We have an application (f arg_ty1 .. arg_tyn),
1181 -- where f :: fun_kind
1182 -- Takes care of linting the OutTypes
1183
1184 -- If you edit this function, you may need to update the GHC formalism
1185 -- See Note [GHC Formalism]
1186 lint_app doc kfn kas
1187 = do { in_scope <- getInScope
1188 -- We need the in_scope set to satisfy the invariant in
1189 -- Note [The substitution invariant] in TyCoRep
1190 ; foldlM (go_app in_scope) kfn kas }
1191 where
1192 fail_msg = vcat [ hang (text "Kind application error in") 2 doc
1193 , nest 2 (text "Function kind =" <+> ppr kfn)
1194 , nest 2 (text "Arg kinds =" <+> ppr kas) ]
1195
1196 go_app in_scope kfn ka
1197 | Just kfn' <- coreView kfn
1198 = go_app in_scope kfn' ka
1199
1200 go_app _ (FunTy kfa kfb) (_,ka)
1201 = do { unless (ka `eqType` kfa) (addErrL fail_msg)
1202 ; return kfb }
1203
1204 go_app in_scope (ForAllTy (TvBndr kv _vis) kfn) (ta,ka)
1205 = do { unless (ka `eqType` tyVarKind kv) (addErrL fail_msg)
1206 ; return (substTyWithInScope in_scope [kv] [ta] kfn) }
1207
1208 go_app _ _ _ = failWithL fail_msg
1209
1210 {- *********************************************************************
1211 * *
1212 Linting rules
1213 * *
1214 ********************************************************************* -}
1215
1216 lintCoreRule :: OutType -> CoreRule -> LintM ()
1217 lintCoreRule _ (BuiltinRule {})
1218 = return () -- Don't bother
1219
1220 lintCoreRule fun_ty (Rule { ru_name = name, ru_bndrs = bndrs
1221 , ru_args = args, ru_rhs = rhs })
1222 = lintBinders bndrs $ \ _ ->
1223 do { lhs_ty <- foldM lintCoreArg fun_ty args
1224 ; rhs_ty <- lintCoreExpr rhs
1225 ; ensureEqTys lhs_ty rhs_ty $
1226 (rule_doc <+> vcat [ text "lhs type:" <+> ppr lhs_ty
1227 , text "rhs type:" <+> ppr rhs_ty ])
1228 ; let bad_bndrs = filterOut (`elemVarSet` exprsFreeVars args) $
1229 filter (`elemVarSet` exprFreeVars rhs) $
1230 bndrs
1231
1232 ; checkL (null bad_bndrs)
1233 (rule_doc <+> text "unbound" <+> ppr bad_bndrs)
1234 -- See Note [Linting rules]
1235 }
1236 where
1237 rule_doc = text "Rule" <+> doubleQuotes (ftext name) <> colon
1238
1239 {- Note [Linting rules]
1240 ~~~~~~~~~~~~~~~~~~~~~~~
1241 It's very bad if simplifying a rule means that one of the template
1242 variables (ru_bndrs) that /is/ mentioned on the RHS becomes
1243 not-mentioned in the LHS (ru_args). How can that happen? Well, in
1244 Trac #10602, SpecConstr stupidly constructed a rule like
1245
1246 forall x,c1,c2.
1247 f (x |> c1 |> c2) = ....
1248
1249 But simplExpr collapses those coercions into one. (Indeed in
1250 Trac #10602, it collapsed to the identity and was removed altogether.)
1251
1252 We don't have a great story for what to do here, but at least
1253 this check will nail it.
1254
1255 NB (Trac #11643): it's possible that a variable listed in the
1256 binders becomes not-mentioned on both LHS and RHS. Here's a silly
1257 example:
1258 RULE forall x y. f (g x y) = g (x+1 (y-1)
1259 And suppose worker/wrapper decides that 'x' is Absent. Then
1260 we'll end up with
1261 RULE forall x y. f ($gw y) = $gw (x+1)
1262 This seems sufficiently obscure that there isn't enough payoff to
1263 try to trim the forall'd binder list.
1264 -}
1265
1266 {-
1267 ************************************************************************
1268 * *
1269 Linting coercions
1270 * *
1271 ************************************************************************
1272 -}
1273
1274 lintInCo :: InCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
1275 -- Check the coercion, and apply the substitution to it
1276 -- See Note [Linting type lets]
1277 lintInCo co
1278 = addLoc (InCo co) $
1279 do { co' <- applySubstCo co
1280 ; lintCoercion co' }
1281
1282 -- lints a coercion, confirming that its lh kind and its rh kind are both *
1283 -- also ensures that the role is Nominal
1284 lintStarCoercion :: OutCoercion -> LintM (LintedType, LintedType)
1285 lintStarCoercion g
1286 = do { (k1, k2, t1, t2, r) <- lintCoercion g
1287 ; lintStar (text "the kind of the left type in" <+> ppr g) k1
1288 ; lintStar (text "the kind of the right type in" <+> ppr g) k2
1289 ; lintRole g Nominal r
1290 ; return (t1, t2) }
1291
1292 lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
1293 -- Check the kind of a coercion term, returning the kind
1294 -- Post-condition: the returned OutTypes are lint-free
1295 --
1296 -- If lintCoercion co = (k1, k2, s1, s2, r)
1297 -- then co :: s1 ~r s2
1298 -- s1 :: k2
1299 -- s2 :: k2
1300
1301 -- If you edit this function, you may need to update the GHC formalism
1302 -- See Note [GHC Formalism]
1303 lintCoercion (Refl r ty)
1304 = do { k <- lintType ty
1305 ; return (k, k, ty, ty, r) }
1306
1307 lintCoercion co@(TyConAppCo r tc cos)
1308 | tc `hasKey` funTyConKey
1309 , [co1,co2] <- cos
1310 = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
1311 ; (k2,k'2,s2,t2,r2) <- lintCoercion co2
1312 ; k <- lintArrow (text "coercion" <+> quotes (ppr co)) k1 k2
1313 ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2
1314 ; lintRole co1 r r1
1315 ; lintRole co2 r r2
1316 ; return (k, k', mkFunTy s1 s2, mkFunTy t1 t2, r) }
1317
1318 | Just {} <- synTyConDefn_maybe tc
1319 = failWithL (text "Synonym in TyConAppCo:" <+> ppr co)
1320
1321 | otherwise
1322 = do { checkTyCon tc
1323 ; (k's, ks, ss, ts, rs) <- mapAndUnzip5M lintCoercion cos
1324 ; k' <- lint_co_app co (tyConKind tc) (ss `zip` k's)
1325 ; k <- lint_co_app co (tyConKind tc) (ts `zip` ks)
1326 ; _ <- zipWith3M lintRole cos (tyConRolesX r tc) rs
1327 ; return (k', k, mkTyConApp tc ss, mkTyConApp tc ts, r) }
1328
1329 lintCoercion co@(AppCo co1 co2)
1330 | TyConAppCo {} <- co1
1331 = failWithL (text "TyConAppCo to the left of AppCo:" <+> ppr co)
1332 | Refl _ (TyConApp {}) <- co1
1333 = failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co)
1334 | otherwise
1335 = do { (k1, k2, s1, s2, r1) <- lintCoercion co1
1336 ; (k'1, k'2, t1, t2, r2) <- lintCoercion co2
1337 ; k3 <- lint_co_app co k1 [(t1,k'1)]
1338 ; k4 <- lint_co_app co k2 [(t2,k'2)]
1339 ; if r1 == Phantom
1340 then lintL (r2 == Phantom || r2 == Nominal)
1341 (text "Second argument in AppCo cannot be R:" $$
1342 ppr co)
1343 else lintRole co Nominal r2
1344 ; return (k3, k4, mkAppTy s1 t1, mkAppTy s2 t2, r1) }
1345
1346 ----------
1347 lintCoercion (ForAllCo tv1 kind_co co)
1348 = do { (_, k2) <- lintStarCoercion kind_co
1349 ; let tv2 = setTyVarKind tv1 k2
1350 ; addInScopeVar tv1 $
1351 do {
1352 ; (k3, k4, t1, t2, r) <- lintCoercion co
1353 ; in_scope <- getInScope
1354 ; let tyl = mkInvForAllTy tv1 t1
1355 subst = mkTvSubst in_scope $
1356 -- We need both the free vars of the `t2` and the
1357 -- free vars of the range of the substitution in
1358 -- scope. All the free vars of `t2` and `kind_co` should
1359 -- already be in `in_scope`, because they've been
1360 -- linted and `tv2` has the same unique as `tv1`.
1361 -- See Note [The substitution invariant]
1362 unitVarEnv tv1 (TyVarTy tv2 `mkCastTy` mkSymCo kind_co)
1363 tyr = mkInvForAllTy tv2 $
1364 substTy subst t2
1365 ; return (k3, k4, tyl, tyr, r) } }
1366
1367 lintCoercion (CoVarCo cv)
1368 | not (isCoVar cv)
1369 = failWithL (hang (text "Bad CoVarCo:" <+> ppr cv)
1370 2 (text "With offending type:" <+> ppr (varType cv)))
1371 | otherwise
1372 = do { lintTyCoVarInScope cv
1373 ; cv' <- lookupIdInScope cv
1374 ; lintUnliftedCoVar cv
1375 ; return $ coVarKindsTypesRole cv' }
1376
1377 -- See Note [Bad unsafe coercion]
1378 lintCoercion co@(UnivCo prov r ty1 ty2)
1379 = do { k1 <- lintType ty1
1380 ; k2 <- lintType ty2
1381 ; case prov of
1382 UnsafeCoerceProv -> return () -- no extra checks
1383
1384 PhantomProv kco -> do { lintRole co Phantom r
1385 ; check_kinds kco k1 k2 }
1386
1387 ProofIrrelProv kco -> do { lintL (isCoercionTy ty1) $
1388 mkBadProofIrrelMsg ty1 co
1389 ; lintL (isCoercionTy ty2) $
1390 mkBadProofIrrelMsg ty2 co
1391 ; check_kinds kco k1 k2 }
1392
1393 PluginProv _ -> return () -- no extra checks
1394 HoleProv h -> addErrL $
1395 text "Unfilled coercion hole:" <+> ppr h
1396
1397 ; when (r /= Phantom && classifiesTypeWithValues k1
1398 && classifiesTypeWithValues k2)
1399 (checkTypes ty1 ty2)
1400 ; return (k1, k2, ty1, ty2, r) }
1401 where
1402 report s = hang (text $ "Unsafe coercion between " ++ s)
1403 2 (vcat [ text "From:" <+> ppr ty1
1404 , text " To:" <+> ppr ty2])
1405 isUnBoxed :: PrimRep -> Bool
1406 isUnBoxed = not . isGcPtrRep
1407
1408 -- see #9122 for discussion of these checks
1409 checkTypes t1 t2
1410 = do { checkWarnL (reps1 `equalLength` reps2)
1411 (report "values with different # of reps")
1412 ; zipWithM_ validateCoercion reps1 reps2 }
1413 where
1414 reps1 = typePrimRep t1
1415 reps2 = typePrimRep t2
1416
1417 validateCoercion :: PrimRep -> PrimRep -> LintM ()
1418 validateCoercion rep1 rep2
1419 = do { dflags <- getDynFlags
1420 ; checkWarnL (isUnBoxed rep1 == isUnBoxed rep2)
1421 (report "unboxed and boxed value")
1422 ; checkWarnL (TyCon.primRepSizeW dflags rep1
1423 == TyCon.primRepSizeW dflags rep2)
1424 (report "unboxed values of different size")
1425 ; let fl = liftM2 (==) (TyCon.primRepIsFloat rep1)
1426 (TyCon.primRepIsFloat rep2)
1427 ; case fl of
1428 Nothing -> addWarnL (report "vector types")
1429 Just False -> addWarnL (report "float and integral values")
1430 _ -> return ()
1431 }
1432
1433 check_kinds kco k1 k2 = do { (k1', k2') <- lintStarCoercion kco
1434 ; ensureEqTys k1 k1' (mkBadUnivCoMsg CLeft co)
1435 ; ensureEqTys k2 k2' (mkBadUnivCoMsg CRight co) }
1436
1437
1438 lintCoercion (SymCo co)
1439 = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
1440 ; return (k2, k1, ty2, ty1, r) }
1441
1442 lintCoercion co@(TransCo co1 co2)
1443 = do { (k1a, _k1b, ty1a, ty1b, r1) <- lintCoercion co1
1444 ; (_k2a, k2b, ty2a, ty2b, r2) <- lintCoercion co2
1445 ; ensureEqTys ty1b ty2a
1446 (hang (text "Trans coercion mis-match:" <+> ppr co)
1447 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
1448 ; lintRole co r1 r2
1449 ; return (k1a, k2b, ty1a, ty2b, r1) }
1450
1451 lintCoercion the_co@(NthCo n co)
1452 = do { (_, _, s, t, r) <- lintCoercion co
1453 ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
1454 { (Just (tv_s, _ty_s), Just (tv_t, _ty_t))
1455 | n == 0
1456 -> return (ks, kt, ts, tt, Nominal)
1457 where
1458 ts = tyVarKind tv_s
1459 tt = tyVarKind tv_t
1460 ks = typeKind ts
1461 kt = typeKind tt
1462
1463 ; _ -> case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
1464 { (Just (tc_s, tys_s), Just (tc_t, tys_t))
1465 | tc_s == tc_t
1466 , isInjectiveTyCon tc_s r
1467 -- see Note [NthCo and newtypes] in TyCoRep
1468 , tys_s `equalLength` tys_t
1469 , n < length tys_s
1470 -> return (ks, kt, ts, tt, tr)
1471 where
1472 ts = getNth tys_s n
1473 tt = getNth tys_t n
1474 tr = nthRole r tc_s n
1475 ks = typeKind ts
1476 kt = typeKind tt
1477
1478 ; _ -> failWithL (hang (text "Bad getNth:")
1479 2 (ppr the_co $$ ppr s $$ ppr t)) }}}
1480
1481 lintCoercion the_co@(LRCo lr co)
1482 = do { (_,_,s,t,r) <- lintCoercion co
1483 ; lintRole co Nominal r
1484 ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
1485 (Just s_pr, Just t_pr)
1486 -> return (ks_pick, kt_pick, s_pick, t_pick, Nominal)
1487 where
1488 s_pick = pickLR lr s_pr
1489 t_pick = pickLR lr t_pr
1490 ks_pick = typeKind s_pick
1491 kt_pick = typeKind t_pick
1492
1493 _ -> failWithL (hang (text "Bad LRCo:")
1494 2 (ppr the_co $$ ppr s $$ ppr t)) }
1495
1496 lintCoercion (InstCo co arg)
1497 = do { (k3, k4, t1',t2', r) <- lintCoercion co
1498 ; (k1',k2',s1,s2, r') <- lintCoercion arg
1499 ; lintRole arg Nominal r'
1500 ; in_scope <- getInScope
1501 ; case (splitForAllTy_maybe t1', splitForAllTy_maybe t2') of
1502 (Just (tv1,t1), Just (tv2,t2))
1503 | k1' `eqType` tyVarKind tv1
1504 , k2' `eqType` tyVarKind tv2
1505 -> return (k3, k4,
1506 substTyWithInScope in_scope [tv1] [s1] t1,
1507 substTyWithInScope in_scope [tv2] [s2] t2, r)
1508 | otherwise
1509 -> failWithL (text "Kind mis-match in inst coercion")
1510 _ -> failWithL (text "Bad argument of inst") }
1511
1512 lintCoercion co@(AxiomInstCo con ind cos)
1513 = do { unless (0 <= ind && ind < numBranches (coAxiomBranches con))
1514 (bad_ax (text "index out of range"))
1515 ; let CoAxBranch { cab_tvs = ktvs
1516 , cab_cvs = cvs
1517 , cab_roles = roles
1518 , cab_lhs = lhs
1519 , cab_rhs = rhs } = coAxiomNthBranch con ind
1520 ; unless (length ktvs + length cvs == length cos) $
1521 bad_ax (text "lengths")
1522 ; subst <- getTCvSubst
1523 ; let empty_subst = zapTCvSubst subst
1524 ; (subst_l, subst_r) <- foldlM check_ki
1525 (empty_subst, empty_subst)
1526 (zip3 (ktvs ++ cvs) roles cos)
1527 ; let lhs' = substTys subst_l lhs
1528 rhs' = substTy subst_r rhs
1529 ; case checkAxInstCo co of
1530 Just bad_branch -> bad_ax $ text "inconsistent with" <+>
1531 pprCoAxBranch con bad_branch
1532 Nothing -> return ()
1533 ; let s2 = mkTyConApp (coAxiomTyCon con) lhs'
1534 ; return (typeKind s2, typeKind rhs', s2, rhs', coAxiomRole con) }
1535 where
1536 bad_ax what = addErrL (hang (text "Bad axiom application" <+> parens what)
1537 2 (ppr co))
1538
1539 check_ki (subst_l, subst_r) (ktv, role, arg)
1540 = do { (k', k'', s', t', r) <- lintCoercion arg
1541 ; lintRole arg role r
1542 ; let ktv_kind_l = substTy subst_l (tyVarKind ktv)
1543 ktv_kind_r = substTy subst_r (tyVarKind ktv)
1544 ; unless (k' `eqType` ktv_kind_l)
1545 (bad_ax (text "check_ki1" <+> vcat [ ppr co, ppr k', ppr ktv, ppr ktv_kind_l ] ))
1546 ; unless (k'' `eqType` ktv_kind_r)
1547 (bad_ax (text "check_ki2" <+> vcat [ ppr co, ppr k'', ppr ktv, ppr ktv_kind_r ] ))
1548 ; return (extendTCvSubst subst_l ktv s',
1549 extendTCvSubst subst_r ktv t') }
1550
1551 lintCoercion (CoherenceCo co1 co2)
1552 = do { (_, k2, t1, t2, r) <- lintCoercion co1
1553 ; let lhsty = mkCastTy t1 co2
1554 ; k1' <- lintType lhsty
1555 ; return (k1', k2, lhsty, t2, r) }
1556
1557 lintCoercion (KindCo co)
1558 = do { (k1, k2, _, _, _) <- lintCoercion co
1559 ; return (liftedTypeKind, liftedTypeKind, k1, k2, Nominal) }
1560
1561 lintCoercion (SubCo co')
1562 = do { (k1,k2,s,t,r) <- lintCoercion co'
1563 ; lintRole co' Nominal r
1564 ; return (k1,k2,s,t,Representational) }
1565
1566 lintCoercion this@(AxiomRuleCo co cs)
1567 = do { eqs <- mapM lintCoercion cs
1568 ; lintRoles 0 (coaxrAsmpRoles co) eqs
1569 ; case coaxrProves co [ Pair l r | (_,_,l,r,_) <- eqs ] of
1570 Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
1571 Just (Pair l r) ->
1572 return (typeKind l, typeKind r, l, r, coaxrRole co) }
1573 where
1574 err m xs = failWithL $
1575 hang (text m) 2 $ vcat (text "Rule:" <+> ppr (coaxrName co) : xs)
1576
1577 lintRoles n (e : es) ((_,_,_,_,r) : rs)
1578 | e == r = lintRoles (n+1) es rs
1579 | otherwise = err "Argument roles mismatch"
1580 [ text "In argument:" <+> int (n+1)
1581 , text "Expected:" <+> ppr e
1582 , text "Found:" <+> ppr r ]
1583 lintRoles _ [] [] = return ()
1584 lintRoles n [] rs = err "Too many coercion arguments"
1585 [ text "Expected:" <+> int n
1586 , text "Provided:" <+> int (n + length rs) ]
1587
1588 lintRoles n es [] = err "Not enough coercion arguments"
1589 [ text "Expected:" <+> int (n + length es)
1590 , text "Provided:" <+> int n ]
1591
1592 ----------
1593 lintUnliftedCoVar :: CoVar -> LintM ()
1594 lintUnliftedCoVar cv
1595 = when (not (isUnliftedType (coVarKind cv))) $
1596 failWithL (text "Bad lifted equality:" <+> ppr cv
1597 <+> dcolon <+> ppr (coVarKind cv))
1598
1599 {-
1600 ************************************************************************
1601 * *
1602 \subsection[lint-monad]{The Lint monad}
1603 * *
1604 ************************************************************************
1605 -}
1606
1607 -- If you edit this type, you may need to update the GHC formalism
1608 -- See Note [GHC Formalism]
1609 data LintEnv
1610 = LE { le_flags :: LintFlags -- Linting the result of this pass
1611 , le_loc :: [LintLocInfo] -- Locations
1612 , le_subst :: TCvSubst -- Current type substitution; we also use this
1613 -- to keep track of all the variables in scope,
1614 -- both Ids and TyVars
1615 , le_dynflags :: DynFlags -- DynamicFlags
1616 }
1617
1618 data LintFlags
1619 = LF { lf_check_global_ids :: Bool -- See Note [Checking for global Ids]
1620 , lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers]
1621 , lf_check_static_ptrs :: StaticPtrCheck
1622 -- ^ See Note [Checking StaticPtrs]
1623 }
1624
1625 -- See Note [Checking StaticPtrs]
1626 data StaticPtrCheck
1627 = AllowAnywhere
1628 -- ^ Allow 'makeStatic' to occur anywhere.
1629 | AllowAtTopLevel
1630 -- ^ Allow 'makeStatic' calls at the top-level only.
1631 | RejectEverywhere
1632 -- ^ Reject any 'makeStatic' occurrence.
1633 deriving Eq
1634
1635 defaultLintFlags :: LintFlags
1636 defaultLintFlags = LF { lf_check_global_ids = False
1637 , lf_check_inline_loop_breakers = True
1638 , lf_check_static_ptrs = AllowAnywhere
1639 }
1640
1641 newtype LintM a =
1642 LintM { unLintM ::
1643 LintEnv ->
1644 WarnsAndErrs -> -- Error and warning messages so far
1645 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
1646
1647 type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)
1648
1649 {- Note [Checking for global Ids]
1650 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1651 Before CoreTidy, all locally-bound Ids must be LocalIds, even
1652 top-level ones. See Note [Exported LocalIds] and Trac #9857.
1653
1654 Note [Checking StaticPtrs]
1655 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1656 See Note [Grand plan for static forms] in StaticPtrTable for an overview.
1657
1658 Every occurrence of the function 'makeStatic' should be moved to the
1659 top level by the FloatOut pass. It's vital that we don't have nested
1660 'makeStatic' occurrences after CorePrep, because we populate the Static
1661 Pointer Table from the top-level bindings. See SimplCore Note [Grand
1662 plan for static forms].
1663
1664 The linter checks that no occurrence is left behind, nested within an
1665 expression. The check is enabled only after the FloatOut, CorePrep,
1666 and CoreTidy passes and only if the module uses the StaticPointers
1667 language extension. Checking more often doesn't help since the condition
1668 doesn't hold until after the first FloatOut pass.
1669
1670 Note [Type substitution]
1671 ~~~~~~~~~~~~~~~~~~~~~~~~
1672 Why do we need a type substitution? Consider
1673 /\(a:*). \(x:a). /\(a:*). id a x
1674 This is ill typed, because (renaming variables) it is really
1675 /\(a:*). \(x:a). /\(b:*). id b x
1676 Hence, when checking an application, we can't naively compare x's type
1677 (at its binding site) with its expected type (at a use site). So we
1678 rename type binders as we go, maintaining a substitution.
1679
1680 The same substitution also supports let-type, current expressed as
1681 (/\(a:*). body) ty
1682 Here we substitute 'ty' for 'a' in 'body', on the fly.
1683 -}
1684
1685 instance Functor LintM where
1686 fmap = liftM
1687
1688 instance Applicative LintM where
1689 pure x = LintM $ \ _ errs -> (Just x, errs)
1690 (<*>) = ap
1691
1692 instance Monad LintM where
1693 fail err = failWithL (text err)
1694 m >>= k = LintM (\ env errs ->
1695 let (res, errs') = unLintM m env errs in
1696 case res of
1697 Just r -> unLintM (k r) env errs'
1698 Nothing -> (Nothing, errs'))
1699
1700 #if __GLASGOW_HASKELL__ > 710
1701 instance MonadFail.MonadFail LintM where
1702 fail err = failWithL (text err)
1703 #endif
1704
1705 instance HasDynFlags LintM where
1706 getDynFlags = LintM (\ e errs -> (Just (le_dynflags e), errs))
1707
1708 data LintLocInfo
1709 = RhsOf Id -- The variable bound
1710 | LambdaBodyOf Id -- The lambda-binder
1711 | BodyOfLetRec [Id] -- One of the binders
1712 | CaseAlt CoreAlt -- Case alternative
1713 | CasePat CoreAlt -- The *pattern* of the case alternative
1714 | AnExpr CoreExpr -- Some expression
1715 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
1716 | TopLevelBindings
1717 | InType Type -- Inside a type
1718 | InCo Coercion -- Inside a coercion
1719
1720 initL :: DynFlags -> LintFlags -> LintM a -> WarnsAndErrs -- Errors and warnings
1721 initL dflags flags m
1722 = case unLintM m env (emptyBag, emptyBag) of
1723 (_, errs) -> errs
1724 where
1725 env = LE { le_flags = flags, le_subst = emptyTCvSubst, le_loc = [], le_dynflags = dflags }
1726
1727 getLintFlags :: LintM LintFlags
1728 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
1729
1730 checkL :: Bool -> MsgDoc -> LintM ()
1731 checkL True _ = return ()
1732 checkL False msg = failWithL msg
1733
1734 -- like checkL, but relevant to type checking
1735 lintL :: Bool -> MsgDoc -> LintM ()
1736 lintL = checkL
1737
1738 checkWarnL :: Bool -> MsgDoc -> LintM ()
1739 checkWarnL True _ = return ()
1740 checkWarnL False msg = addWarnL msg
1741
1742 failWithL :: MsgDoc -> LintM a
1743 failWithL msg = LintM $ \ env (warns,errs) ->
1744 (Nothing, (warns, addMsg env errs msg))
1745
1746 addErrL :: MsgDoc -> LintM ()
1747 addErrL msg = LintM $ \ env (warns,errs) ->
1748 (Just (), (warns, addMsg env errs msg))
1749
1750 addWarnL :: MsgDoc -> LintM ()
1751 addWarnL msg = LintM $ \ env (warns,errs) ->
1752 (Just (), (addMsg env warns msg, errs))
1753
1754 addMsg :: LintEnv -> Bag MsgDoc -> MsgDoc -> Bag MsgDoc
1755 addMsg env msgs msg
1756 = ASSERT( notNull locs )
1757 msgs `snocBag` mk_msg msg
1758 where
1759 locs = le_loc env
1760 (loc, cxt1) = dumpLoc (head locs)
1761 cxts = [snd (dumpLoc loc) | loc <- locs]
1762 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
1763 text "Substitution:" <+> ppr (le_subst env)
1764 | otherwise = cxt1
1765
1766 mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
1767
1768 addLoc :: LintLocInfo -> LintM a -> LintM a
1769 addLoc extra_loc m
1770 = LintM $ \ env errs ->
1771 unLintM m (env { le_loc = extra_loc : le_loc env }) errs
1772
1773 inCasePat :: LintM Bool -- A slight hack; see the unique call site
1774 inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
1775 where
1776 is_case_pat (LE { le_loc = CasePat {} : _ }) = True
1777 is_case_pat _other = False
1778
1779 addInScopeVars :: [Var] -> LintM a -> LintM a
1780 addInScopeVars vars m
1781 = LintM $ \ env errs ->
1782 unLintM m (env { le_subst = extendTCvInScopeList (le_subst env) vars })
1783 errs
1784
1785 addInScopeVarSet :: VarSet -> LintM a -> LintM a
1786 addInScopeVarSet vars m
1787 = LintM $ \ env errs ->
1788 unLintM m (env { le_subst = extendTCvInScopeSet (le_subst env) vars })
1789 errs
1790
1791 addInScopeVar :: Var -> LintM a -> LintM a
1792 addInScopeVar var m
1793 = LintM $ \ env errs ->
1794 unLintM m (env { le_subst = extendTCvInScope (le_subst env) var }) errs
1795
1796 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
1797 extendSubstL tv ty m
1798 = LintM $ \ env errs ->
1799 unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
1800
1801 updateTCvSubst :: TCvSubst -> LintM a -> LintM a
1802 updateTCvSubst subst' m
1803 = LintM $ \ env errs -> unLintM m (env { le_subst = subst' }) errs
1804
1805 getTCvSubst :: LintM TCvSubst
1806 getTCvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
1807
1808 getInScope :: LintM InScopeSet
1809 getInScope = LintM (\ env errs -> (Just (getTCvInScope $ le_subst env), errs))
1810
1811 applySubstTy :: InType -> LintM OutType
1812 applySubstTy ty = do { subst <- getTCvSubst; return (substTy subst ty) }
1813
1814 applySubstCo :: InCoercion -> LintM OutCoercion
1815 applySubstCo co = do { subst <- getTCvSubst; return (substCo subst co) }
1816
1817 lookupIdInScope :: Id -> LintM Id
1818 lookupIdInScope id
1819 | not (mustHaveLocalBinding id)
1820 = return id -- An imported Id
1821 | otherwise
1822 = do { subst <- getTCvSubst
1823 ; case lookupInScope (getTCvInScope subst) id of
1824 Just v -> return v
1825 Nothing -> do { addErrL out_of_scope
1826 ; return id } }
1827 where
1828 out_of_scope = pprBndr LetBind id <+> text "is out of scope"
1829
1830 lintTyCoVarInScope :: Var -> LintM ()
1831 lintTyCoVarInScope v = lintInScope (text "is out of scope") v
1832
1833 lintInScope :: SDoc -> Var -> LintM ()
1834 lintInScope loc_msg var =
1835 do { subst <- getTCvSubst
1836 ; lintL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
1837 (hsep [pprBndr LetBind var, loc_msg]) }
1838
1839 ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
1840 -- check ty2 is subtype of ty1 (ie, has same structure but usage
1841 -- annotations need only be consistent, not equal)
1842 -- Assumes ty1,ty2 are have already had the substitution applied
1843 ensureEqTys ty1 ty2 msg = lintL (ty1 `eqType` ty2) msg
1844
1845 lintRole :: Outputable thing
1846 => thing -- where the role appeared
1847 -> Role -- expected
1848 -> Role -- actual
1849 -> LintM ()
1850 lintRole co r1 r2
1851 = lintL (r1 == r2)
1852 (text "Role incompatibility: expected" <+> ppr r1 <> comma <+>
1853 text "got" <+> ppr r2 $$
1854 text "in" <+> ppr co)
1855
1856 {-
1857 ************************************************************************
1858 * *
1859 \subsection{Error messages}
1860 * *
1861 ************************************************************************
1862 -}
1863
1864 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
1865
1866 dumpLoc (RhsOf v)
1867 = (getSrcLoc v, brackets (text "RHS of" <+> pp_binders [v]))
1868
1869 dumpLoc (LambdaBodyOf b)
1870 = (getSrcLoc b, brackets (text "in body of lambda with binder" <+> pp_binder b))
1871
1872 dumpLoc (BodyOfLetRec [])
1873 = (noSrcLoc, brackets (text "In body of a letrec with no binders"))
1874
1875 dumpLoc (BodyOfLetRec bs@(_:_))
1876 = ( getSrcLoc (head bs), brackets (text "in body of letrec with binders" <+> pp_binders bs))
1877
1878 dumpLoc (AnExpr e)
1879 = (noSrcLoc, text "In the expression:" <+> ppr e)
1880
1881 dumpLoc (CaseAlt (con, args, _))
1882 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1883
1884 dumpLoc (CasePat (con, args, _))
1885 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1886
1887 dumpLoc (ImportedUnfolding locn)
1888 = (locn, brackets (text "in an imported unfolding"))
1889 dumpLoc TopLevelBindings
1890 = (noSrcLoc, Outputable.empty)
1891 dumpLoc (InType ty)
1892 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1893 dumpLoc (InCo co)
1894 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
1895
1896 pp_binders :: [Var] -> SDoc
1897 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1898
1899 pp_binder :: Var -> SDoc
1900 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1901 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1902
1903 ------------------------------------------------------
1904 -- Messages for case expressions
1905
1906 mkDefaultArgsMsg :: [Var] -> MsgDoc
1907 mkDefaultArgsMsg args
1908 = hang (text "DEFAULT case with binders")
1909 4 (ppr args)
1910
1911 mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
1912 mkCaseAltMsg e ty1 ty2
1913 = hang (text "Type of case alternatives not the same as the annotation on case:")
1914 4 (vcat [ text "Actual type:" <+> ppr ty1,
1915 text "Annotation on case:" <+> ppr ty2,
1916 text "Alt Rhs:" <+> ppr e ])
1917
1918 mkScrutMsg :: Id -> Type -> Type -> TCvSubst -> MsgDoc
1919 mkScrutMsg var var_ty scrut_ty subst
1920 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1921 text "Result binder type:" <+> ppr var_ty,--(idType var),
1922 text "Scrutinee type:" <+> ppr scrut_ty,
1923 hsep [text "Current TCv subst", ppr subst]]
1924
1925 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
1926 mkNonDefltMsg e
1927 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1928 mkNonIncreasingAltsMsg e
1929 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1930
1931 nonExhaustiveAltsMsg :: CoreExpr -> MsgDoc
1932 nonExhaustiveAltsMsg e
1933 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1934
1935 mkBadConMsg :: TyCon -> DataCon -> MsgDoc
1936 mkBadConMsg tycon datacon
1937 = vcat [
1938 text "In a case alternative, data constructor isn't in scrutinee type:",
1939 text "Scrutinee type constructor:" <+> ppr tycon,
1940 text "Data con:" <+> ppr datacon
1941 ]
1942
1943 mkBadPatMsg :: Type -> Type -> MsgDoc
1944 mkBadPatMsg con_result_ty scrut_ty
1945 = vcat [
1946 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1947 text "Pattern result type:" <+> ppr con_result_ty,
1948 text "Scrutinee type:" <+> ppr scrut_ty
1949 ]
1950
1951 integerScrutinisedMsg :: MsgDoc
1952 integerScrutinisedMsg
1953 = text "In a LitAlt, the literal is lifted (probably Integer)"
1954
1955 mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
1956 mkBadAltMsg scrut_ty alt
1957 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1958 text "Scrutinee type:" <+> ppr scrut_ty,
1959 text "Alternative:" <+> pprCoreAlt alt ]
1960
1961 mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc
1962 mkNewTyDataConAltMsg scrut_ty alt
1963 = vcat [ text "Data alternative for newtype datacon",
1964 text "Scrutinee type:" <+> ppr scrut_ty,
1965 text "Alternative:" <+> pprCoreAlt alt ]
1966
1967
1968 ------------------------------------------------------
1969 -- Other error messages
1970
1971 mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1972 mkAppMsg fun_ty arg_ty arg
1973 = vcat [text "Argument value doesn't match argument type:",
1974 hang (text "Fun type:") 4 (ppr fun_ty),
1975 hang (text "Arg type:") 4 (ppr arg_ty),
1976 hang (text "Arg:") 4 (ppr arg)]
1977
1978 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1979 mkNonFunAppMsg fun_ty arg_ty arg
1980 = vcat [text "Non-function type in function position",
1981 hang (text "Fun type:") 4 (ppr fun_ty),
1982 hang (text "Arg type:") 4 (ppr arg_ty),
1983 hang (text "Arg:") 4 (ppr arg)]
1984
1985 mkLetErr :: TyVar -> CoreExpr -> MsgDoc
1986 mkLetErr bndr rhs
1987 = vcat [text "Bad `let' binding:",
1988 hang (text "Variable:")
1989 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
1990 hang (text "Rhs:")
1991 4 (ppr rhs)]
1992
1993 mkTyAppMsg :: Type -> Type -> MsgDoc
1994 mkTyAppMsg ty arg_ty
1995 = vcat [text "Illegal type application:",
1996 hang (text "Exp type:")
1997 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1998 hang (text "Arg type:")
1999 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
2000
2001 mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc
2002 mkRhsMsg binder what ty
2003 = vcat
2004 [hsep [text "The type of this binder doesn't match the type of its" <+> what <> colon,
2005 ppr binder],
2006 hsep [text "Binder's type:", ppr (idType binder)],
2007 hsep [text "Rhs type:", ppr ty]]
2008
2009 mkLetAppMsg :: CoreExpr -> MsgDoc
2010 mkLetAppMsg e
2011 = hang (text "This argument does not satisfy the let/app invariant:")
2012 2 (ppr e)
2013
2014 mkRhsPrimMsg :: Id -> CoreExpr -> MsgDoc
2015 mkRhsPrimMsg binder _rhs
2016 = vcat [hsep [text "The type of this binder is primitive:",
2017 ppr binder],
2018 hsep [text "Binder's type:", ppr (idType binder)]
2019 ]
2020
2021 mkStrictMsg :: Id -> MsgDoc
2022 mkStrictMsg binder
2023 = vcat [hsep [text "Recursive or top-level binder has strict demand info:",
2024 ppr binder],
2025 hsep [text "Binder's demand info:", ppr (idDemandInfo binder)]
2026 ]
2027
2028 mkNonTopExportedMsg :: Id -> MsgDoc
2029 mkNonTopExportedMsg binder
2030 = hsep [text "Non-top-level binder is marked as exported:", ppr binder]
2031
2032 mkNonTopExternalNameMsg :: Id -> MsgDoc
2033 mkNonTopExternalNameMsg binder
2034 = hsep [text "Non-top-level binder has an external name:", ppr binder]
2035
2036 mkKindErrMsg :: TyVar -> Type -> MsgDoc
2037 mkKindErrMsg tyvar arg_ty
2038 = vcat [text "Kinds don't match in type application:",
2039 hang (text "Type variable:")
2040 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
2041 hang (text "Arg type:")
2042 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
2043
2044 {- Not needed now
2045 mkArityMsg :: Id -> MsgDoc
2046 mkArityMsg binder
2047 = vcat [hsep [text "Demand type has",
2048 ppr (dmdTypeDepth dmd_ty),
2049 text "arguments, rhs has",
2050 ppr (idArity binder),
2051 text "arguments,",
2052 ppr binder],
2053 hsep [text "Binder's strictness signature:", ppr dmd_ty]
2054
2055 ]
2056 where (StrictSig dmd_ty) = idStrictness binder
2057 -}
2058 mkCastErr :: Outputable casted => casted -> Coercion -> Type -> Type -> MsgDoc
2059 mkCastErr expr co from_ty expr_ty
2060 = vcat [text "From-type of Cast differs from type of enclosed expression",
2061 text "From-type:" <+> ppr from_ty,
2062 text "Type of enclosed expr:" <+> ppr expr_ty,
2063 text "Actual enclosed expr:" <+> ppr expr,
2064 text "Coercion used in cast:" <+> ppr co
2065 ]
2066
2067 mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc
2068 mkBadUnivCoMsg lr co
2069 = text "Kind mismatch on the" <+> pprLeftOrRight lr <+>
2070 text "side of a UnivCo:" <+> ppr co
2071
2072 mkBadProofIrrelMsg :: Type -> Coercion -> SDoc
2073 mkBadProofIrrelMsg ty co
2074 = hang (text "Found a non-coercion in a proof-irrelevance UnivCo:")
2075 2 (vcat [ text "type:" <+> ppr ty
2076 , text "co:" <+> ppr co ])
2077
2078 mkBadTyVarMsg :: Var -> SDoc
2079 mkBadTyVarMsg tv
2080 = text "Non-tyvar used in TyVarTy:"
2081 <+> ppr tv <+> dcolon <+> ppr (varType tv)
2082
2083 pprLeftOrRight :: LeftOrRight -> MsgDoc
2084 pprLeftOrRight CLeft = text "left"
2085 pprLeftOrRight CRight = text "right"
2086
2087 dupVars :: [[Var]] -> MsgDoc
2088 dupVars vars
2089 = hang (text "Duplicate variables brought into scope")
2090 2 (ppr vars)
2091
2092 dupExtVars :: [[Name]] -> MsgDoc
2093 dupExtVars vars
2094 = hang (text "Duplicate top-level variables with the same qualified name")
2095 2 (ppr vars)
2096
2097 {-
2098 ************************************************************************
2099 * *
2100 \subsection{Annotation Linting}
2101 * *
2102 ************************************************************************
2103 -}
2104
2105 -- | This checks whether a pass correctly looks through debug
2106 -- annotations (@SourceNote@). This works a bit different from other
2107 -- consistency checks: We check this by running the given task twice,
2108 -- noting all differences between the results.
2109 lintAnnots :: SDoc -> (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
2110 lintAnnots pname pass guts = do
2111 -- Run the pass as we normally would
2112 dflags <- getDynFlags
2113 when (gopt Opt_DoAnnotationLinting dflags) $
2114 liftIO $ Err.showPass dflags "Annotation linting - first run"
2115 nguts <- pass guts
2116 -- If appropriate re-run it without debug annotations to make sure
2117 -- that they made no difference.
2118 when (gopt Opt_DoAnnotationLinting dflags) $ do
2119 liftIO $ Err.showPass dflags "Annotation linting - second run"
2120 nguts' <- withoutAnnots pass guts
2121 -- Finally compare the resulting bindings
2122 liftIO $ Err.showPass dflags "Annotation linting - comparison"
2123 let binds = flattenBinds $ mg_binds nguts
2124 binds' = flattenBinds $ mg_binds nguts'
2125 (diffs,_) = diffBinds True (mkRnEnv2 emptyInScopeSet) binds binds'
2126 when (not (null diffs)) $ CoreMonad.putMsg $ vcat
2127 [ lint_banner "warning" pname
2128 , text "Core changes with annotations:"
2129 , withPprStyle defaultDumpStyle $ nest 2 $ vcat diffs
2130 ]
2131 -- Return actual new guts
2132 return nguts
2133
2134 -- | Run the given pass without annotations. This means that we both
2135 -- set the debugLevel setting to 0 in the environment as well as all
2136 -- annotations from incoming modules.
2137 withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
2138 withoutAnnots pass guts = do
2139 -- Remove debug flag from environment.
2140 dflags <- getDynFlags
2141 let removeFlag env = env{ hsc_dflags = dflags{ debugLevel = 0} }
2142 withoutFlag corem =
2143 liftIO =<< runCoreM <$> fmap removeFlag getHscEnv <*> getRuleBase <*>
2144 getUniqueSupplyM <*> getModule <*>
2145 getVisibleOrphanMods <*>
2146 getPrintUnqualified <*> getSrcSpanM <*>
2147 pure corem
2148 -- Nuke existing ticks in module.
2149 -- TODO: Ticks in unfoldings. Maybe change unfolding so it removes
2150 -- them in absence of debugLevel > 0.
2151 let nukeTicks = stripTicksE (not . tickishIsCode)
2152 nukeAnnotsBind :: CoreBind -> CoreBind
2153 nukeAnnotsBind bind = case bind of
2154 Rec bs -> Rec $ map (\(b,e) -> (b, nukeTicks e)) bs
2155 NonRec b e -> NonRec b $ nukeTicks e
2156 nukeAnnotsMod mg@ModGuts{mg_binds=binds}
2157 = mg{mg_binds = map nukeAnnotsBind binds}
2158 -- Perform pass with all changes applied
2159 fmap fst $ withoutFlag $ pass (nukeAnnotsMod guts)