Compute demand signatures assuming idArity
[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, lintTypes,
15
16 -- ** Debug output
17 endPass, endPassIO,
18 dumpPassResult,
19 CoreLint.dumpIfSet,
20 ) where
21
22 #include "HsVersions.h"
23
24 import GhcPrelude
25
26 import CoreSyn
27 import CoreFVs
28 import CoreUtils
29 import CoreStats ( coreBindsStats )
30 import CoreMonad
31 import Bag
32 import Literal
33 import DataCon
34 import TysWiredIn
35 import TysPrim
36 import TcType ( isFloatingTy )
37 import Var
38 import VarEnv
39 import VarSet
40 import Name
41 import Id
42 import IdInfo
43 import PprCore
44 import ErrUtils
45 import Coercion
46 import SrcLoc
47 import Kind
48 import Type
49 import RepType
50 import TyCoRep -- checks validity of types/coercions
51 import TyCon
52 import CoAxiom
53 import BasicTypes
54 import ErrUtils as Err
55 import ListSetOps
56 import PrelNames
57 import Outputable
58 import FastString
59 import Util
60 import InstEnv ( instanceDFunId )
61 import OptCoercion ( checkAxInstCo )
62 import UniqSupply
63 import CoreArity ( typeArity )
64 import Demand ( splitStrictSig, isBotRes )
65
66 import HscTypes
67 import DynFlags
68 import Control.Monad
69 import qualified Control.Monad.Fail as MonadFail
70 import MonadUtils
71 import Data.Foldable ( toList )
72 import Data.List.NonEmpty ( NonEmpty )
73 import Data.Maybe
74 import Pair
75 import qualified GHC.LanguageExtensions as LangExt
76
77 {-
78 Note [GHC Formalism]
79 ~~~~~~~~~~~~~~~~~~~~
80 This file implements the type-checking algorithm for System FC, the "official"
81 name of the Core language. Type safety of FC is heart of the claim that
82 executables produced by GHC do not have segmentation faults. Thus, it is
83 useful to be able to reason about System FC independently of reading the code.
84 To this purpose, there is a document core-spec.pdf built in docs/core-spec that
85 contains a formalism of the types and functions dealt with here. If you change
86 just about anything in this file or you change other types/functions throughout
87 the Core language (all signposted to this note), you should update that
88 formalism. See docs/core-spec/README for more info about how to do so.
89
90 Note [check vs lint]
91 ~~~~~~~~~~~~~~~~~~~~
92 This file implements both a type checking algorithm and also general sanity
93 checking. For example, the "sanity checking" checks for TyConApp on the left
94 of an AppTy, which should never happen. These sanity checks don't really
95 affect any notion of type soundness. Yet, it is convenient to do the sanity
96 checks at the same time as the type checks. So, we use the following naming
97 convention:
98
99 - Functions that begin with 'lint'... are involved in type checking. These
100 functions might also do some sanity checking.
101
102 - Functions that begin with 'check'... are *not* involved in type checking.
103 They exist only for sanity checking.
104
105 Issues surrounding variable naming, shadowing, and such are considered *not*
106 to be part of type checking, as the formalism omits these details.
107
108 Summary of checks
109 ~~~~~~~~~~~~~~~~~
110 Checks that a set of core bindings is well-formed. The PprStyle and String
111 just control what we print in the event of an error. The Bool value
112 indicates whether we have done any specialisation yet (in which case we do
113 some extra checks).
114
115 We check for
116 (a) type errors
117 (b) Out-of-scope type variables
118 (c) Out-of-scope local variables
119 (d) Ill-kinded types
120 (e) Incorrect unsafe coercions
121
122 If we have done specialisation the we check that there are
123 (a) No top-level bindings of primitive (unboxed type)
124
125 Outstanding issues:
126
127 -- Things are *not* OK if:
128 --
129 -- * Unsaturated type app before specialisation has been done;
130 --
131 -- * Oversaturated type app after specialisation (eta reduction
132 -- may well be happening...);
133
134
135 Note [Linting function types]
136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
137 As described in Note [Representation of function types], all saturated
138 applications of funTyCon are represented with the FunTy constructor. We check
139 this invariant in lintType.
140
141 Note [Linting type lets]
142 ~~~~~~~~~~~~~~~~~~~~~~~~
143 In the desugarer, it's very very convenient to be able to say (in effect)
144 let a = Type Int in <body>
145 That is, use a type let. See Note [Type let] in CoreSyn.
146
147 However, when linting <body> we need to remember that a=Int, else we might
148 reject a correct program. So we carry a type substitution (in this example
149 [a -> Int]) and apply this substitution before comparing types. The functin
150 lintInTy :: Type -> LintM (Type, Kind)
151 returns a substituted type.
152
153 When we encounter a binder (like x::a) we must apply the substitution
154 to the type of the binding variable. lintBinders does this.
155
156 For Ids, the type-substituted Id is added to the in_scope set (which
157 itself is part of the TCvSubst we are carrying down), and when we
158 find an occurrence of an Id, we fetch it from the in-scope set.
159
160 Note [Bad unsafe coercion]
161 ~~~~~~~~~~~~~~~~~~~~~~~~~~
162 For discussion see https://gitlab.haskell.org/ghc/ghc/wikis/bad-unsafe-coercions
163 Linter introduces additional rules that checks improper coercion between
164 different types, called bad coercions. Following coercions are forbidden:
165
166 (a) coercions between boxed and unboxed values;
167 (b) coercions between unlifted values of the different sizes, here
168 active size is checked, i.e. size of the actual value but not
169 the space allocated for value;
170 (c) coercions between floating and integral boxed values, this check
171 is not yet supported for unboxed tuples, as no semantics were
172 specified for that;
173 (d) coercions from / to vector type
174 (e) If types are unboxed tuples then tuple (# A_1,..,A_n #) can be
175 coerced to (# B_1,..,B_m #) if n=m and for each pair A_i, B_i rules
176 (a-e) holds.
177
178 Note [Join points]
179 ~~~~~~~~~~~~~~~~~~
180 We check the rules listed in Note [Invariants on join points] in CoreSyn. The
181 only one that causes any difficulty is the first: All occurrences must be tail
182 calls. To this end, along with the in-scope set, we remember in le_joins the
183 subset of in-scope Ids that are valid join ids. For example:
184
185 join j x = ... in
186 case e of
187 A -> jump j y -- good
188 B -> case (jump j z) of -- BAD
189 C -> join h = jump j w in ... -- good
190 D -> let x = jump j v in ... -- BAD
191
192 A join point remains valid in case branches, so when checking the A
193 branch, j is still valid. When we check the scrutinee of the inner
194 case, however, we set le_joins to empty, and catch the
195 error. Similarly, join points can occur free in RHSes of other join
196 points but not the RHSes of value bindings (thunks and functions).
197
198 ************************************************************************
199 * *
200 Beginning and ending passes
201 * *
202 ************************************************************************
203
204 These functions are not CoreM monad stuff, but they probably ought to
205 be, and it makes a convenient place for them. They print out stuff
206 before and after core passes, and do Core Lint when necessary.
207 -}
208
209 endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> CoreM ()
210 endPass pass binds rules
211 = do { hsc_env <- getHscEnv
212 ; print_unqual <- getPrintUnqualified
213 ; liftIO $ endPassIO hsc_env print_unqual pass binds rules }
214
215 endPassIO :: HscEnv -> PrintUnqualified
216 -> CoreToDo -> CoreProgram -> [CoreRule] -> IO ()
217 -- Used by the IO-is CorePrep too
218 endPassIO hsc_env print_unqual pass binds rules
219 = do { dumpPassResult dflags print_unqual mb_flag
220 (ppr pass) (pprPassDetails pass) binds rules
221 ; lintPassResult hsc_env pass binds }
222 where
223 dflags = hsc_dflags hsc_env
224 mb_flag = case coreDumpFlag pass of
225 Just flag | dopt flag dflags -> Just flag
226 | dopt Opt_D_verbose_core2core dflags -> Just flag
227 _ -> Nothing
228
229 dumpIfSet :: DynFlags -> Bool -> CoreToDo -> SDoc -> SDoc -> IO ()
230 dumpIfSet dflags dump_me pass extra_info doc
231 = Err.dumpIfSet dflags dump_me (showSDoc dflags (ppr pass <+> extra_info)) doc
232
233 dumpPassResult :: DynFlags
234 -> PrintUnqualified
235 -> Maybe DumpFlag -- Just df => show details in a file whose
236 -- name is specified by df
237 -> SDoc -- Header
238 -> SDoc -- Extra info to appear after header
239 -> CoreProgram -> [CoreRule]
240 -> IO ()
241 dumpPassResult dflags unqual mb_flag hdr extra_info binds rules
242 = do { forM_ mb_flag $ \flag ->
243 Err.dumpSDoc dflags unqual flag (showSDoc dflags hdr) dump_doc
244
245 -- Report result size
246 -- This has the side effect of forcing the intermediate to be evaluated
247 -- if it's not already forced by a -ddump flag.
248 ; Err.debugTraceMsg dflags 2 size_doc
249 }
250
251 where
252 size_doc = sep [text "Result size of" <+> hdr, nest 2 (equals <+> ppr (coreBindsStats binds))]
253
254 dump_doc = vcat [ nest 2 extra_info
255 , size_doc
256 , blankLine
257 , pprCoreBindingsWithSize binds
258 , ppUnless (null rules) pp_rules ]
259 pp_rules = vcat [ blankLine
260 , text "------ Local rules for imported ids --------"
261 , pprRules rules ]
262
263 coreDumpFlag :: CoreToDo -> Maybe DumpFlag
264 coreDumpFlag (CoreDoSimplify {}) = Just Opt_D_verbose_core2core
265 coreDumpFlag (CoreDoPluginPass {}) = Just Opt_D_verbose_core2core
266 coreDumpFlag CoreDoFloatInwards = Just Opt_D_verbose_core2core
267 coreDumpFlag (CoreDoFloatOutwards {}) = Just Opt_D_verbose_core2core
268 coreDumpFlag CoreLiberateCase = Just Opt_D_verbose_core2core
269 coreDumpFlag CoreDoStaticArgs = Just Opt_D_verbose_core2core
270 coreDumpFlag CoreDoCallArity = Just Opt_D_dump_call_arity
271 coreDumpFlag CoreDoExitify = Just Opt_D_dump_exitify
272 coreDumpFlag CoreDoStrictness = Just Opt_D_dump_stranal
273 coreDumpFlag CoreDoWorkerWrapper = Just Opt_D_dump_worker_wrapper
274 coreDumpFlag CoreDoSpecialising = Just Opt_D_dump_spec
275 coreDumpFlag CoreDoSpecConstr = Just Opt_D_dump_spec
276 coreDumpFlag CoreCSE = Just Opt_D_dump_cse
277 coreDumpFlag CoreDesugar = Just Opt_D_dump_ds_preopt
278 coreDumpFlag CoreDesugarOpt = Just Opt_D_dump_ds
279 coreDumpFlag CoreTidy = Just Opt_D_dump_simpl
280 coreDumpFlag CorePrep = Just Opt_D_dump_prep
281 coreDumpFlag CoreOccurAnal = Just Opt_D_dump_occur_anal
282
283 coreDumpFlag CoreDoPrintCore = Nothing
284 coreDumpFlag (CoreDoRuleCheck {}) = Nothing
285 coreDumpFlag CoreDoNothing = Nothing
286 coreDumpFlag (CoreDoPasses {}) = Nothing
287
288 {-
289 ************************************************************************
290 * *
291 Top-level interfaces
292 * *
293 ************************************************************************
294 -}
295
296 lintPassResult :: HscEnv -> CoreToDo -> CoreProgram -> IO ()
297 lintPassResult hsc_env pass binds
298 | not (gopt Opt_DoCoreLinting dflags)
299 = return ()
300 | otherwise
301 = do { let (warns, errs) = lintCoreBindings dflags pass (interactiveInScope hsc_env) binds
302 ; Err.showPass dflags ("Core Linted result of " ++ showPpr dflags pass)
303 ; displayLintResults dflags pass warns errs binds }
304 where
305 dflags = hsc_dflags hsc_env
306
307 displayLintResults :: DynFlags -> CoreToDo
308 -> Bag Err.MsgDoc -> Bag Err.MsgDoc -> CoreProgram
309 -> IO ()
310 displayLintResults dflags pass warns errs binds
311 | not (isEmptyBag errs)
312 = do { putLogMsg dflags NoReason Err.SevDump noSrcSpan
313 (defaultDumpStyle dflags)
314 (vcat [ lint_banner "errors" (ppr pass), Err.pprMessageBag errs
315 , text "*** Offending Program ***"
316 , pprCoreBindings binds
317 , text "*** End of Offense ***" ])
318 ; Err.ghcExit dflags 1 }
319
320 | not (isEmptyBag warns)
321 , not (hasNoDebugOutput dflags)
322 , showLintWarnings pass
323 -- If the Core linter encounters an error, output to stderr instead of
324 -- stdout (#13342)
325 = putLogMsg dflags NoReason Err.SevInfo noSrcSpan
326 (defaultDumpStyle dflags)
327 (lint_banner "warnings" (ppr pass) $$ Err.pprMessageBag (mapBag ($$ blankLine) warns))
328
329 | otherwise = return ()
330 where
331
332 lint_banner :: String -> SDoc -> SDoc
333 lint_banner string pass = text "*** Core Lint" <+> text string
334 <+> text ": in result of" <+> pass
335 <+> text "***"
336
337 showLintWarnings :: CoreToDo -> Bool
338 -- Disable Lint warnings on the first simplifier pass, because
339 -- there may be some INLINE knots still tied, which is tiresomely noisy
340 showLintWarnings (CoreDoSimplify _ (SimplMode { sm_phase = InitialPhase })) = False
341 showLintWarnings _ = True
342
343 lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO ()
344 lintInteractiveExpr what hsc_env expr
345 | not (gopt Opt_DoCoreLinting dflags)
346 = return ()
347 | Just err <- lintExpr dflags (interactiveInScope hsc_env) expr
348 = do { display_lint_err err
349 ; Err.ghcExit dflags 1 }
350 | otherwise
351 = return ()
352 where
353 dflags = hsc_dflags hsc_env
354
355 display_lint_err err
356 = do { putLogMsg dflags NoReason Err.SevDump
357 noSrcSpan (defaultDumpStyle dflags)
358 (vcat [ lint_banner "errors" (text what)
359 , err
360 , text "*** Offending Program ***"
361 , pprCoreExpr expr
362 , text "*** End of Offense ***" ])
363 ; Err.ghcExit dflags 1 }
364
365 interactiveInScope :: HscEnv -> [Var]
366 -- In GHCi we may lint expressions, or bindings arising from 'deriving'
367 -- clauses, that mention variables bound in the interactive context.
368 -- These are Local things (see Note [Interactively-bound Ids in GHCi] in HscTypes).
369 -- So we have to tell Lint about them, lest it reports them as out of scope.
370 --
371 -- We do this by find local-named things that may appear free in interactive
372 -- context. This function is pretty revolting and quite possibly not quite right.
373 -- When we are not in GHCi, the interactive context (hsc_IC hsc_env) is empty
374 -- so this is a (cheap) no-op.
375 --
376 -- See #8215 for an example
377 interactiveInScope hsc_env
378 = tyvars ++ ids
379 where
380 -- C.f. TcRnDriver.setInteractiveContext, Desugar.deSugarExpr
381 ictxt = hsc_IC hsc_env
382 (cls_insts, _fam_insts) = ic_instances ictxt
383 te1 = mkTypeEnvWithImplicits (ic_tythings ictxt)
384 te = extendTypeEnvWithIds te1 (map instanceDFunId cls_insts)
385 ids = typeEnvIds te
386 tyvars = tyCoVarsOfTypesList $ map idType ids
387 -- Why the type variables? How can the top level envt have free tyvars?
388 -- I think it's because of the GHCi debugger, which can bind variables
389 -- f :: [t] -> [t]
390 -- where t is a RuntimeUnk (see TcType)
391
392 lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
393 -- Returns (warnings, errors)
394 -- If you edit this function, you may need to update the GHC formalism
395 -- See Note [GHC Formalism]
396 lintCoreBindings dflags pass local_in_scope binds
397 = initL dflags flags in_scope_set $
398 addLoc TopLevelBindings $
399 lintLetBndrs TopLevel binders $
400 -- Put all the top-level binders in scope at the start
401 -- This is because transformation rules can bring something
402 -- into use 'unexpectedly'
403 do { checkL (null dups) (dupVars dups)
404 ; checkL (null ext_dups) (dupExtVars ext_dups)
405 ; mapM lint_bind binds }
406 where
407 in_scope_set = mkInScopeSet (mkVarSet local_in_scope)
408
409 flags = defaultLintFlags
410 { lf_check_global_ids = check_globals
411 , lf_check_inline_loop_breakers = check_lbs
412 , lf_check_static_ptrs = check_static_ptrs }
413
414 -- See Note [Checking for global Ids]
415 check_globals = case pass of
416 CoreTidy -> False
417 CorePrep -> False
418 _ -> True
419
420 -- See Note [Checking for INLINE loop breakers]
421 check_lbs = case pass of
422 CoreDesugar -> False
423 CoreDesugarOpt -> False
424 _ -> True
425
426 -- See Note [Checking StaticPtrs]
427 check_static_ptrs | not (xopt LangExt.StaticPointers dflags) = AllowAnywhere
428 | otherwise = case pass of
429 CoreDoFloatOutwards _ -> AllowAtTopLevel
430 CoreTidy -> RejectEverywhere
431 CorePrep -> AllowAtTopLevel
432 _ -> AllowAnywhere
433
434 binders = bindersOfBinds binds
435 (_, dups) = removeDups compare binders
436
437 -- dups_ext checks for names with different uniques
438 -- but but the same External name M.n. We don't
439 -- allow this at top level:
440 -- M.n{r3} = ...
441 -- M.n{r29} = ...
442 -- because they both get the same linker symbol
443 ext_dups = snd (removeDups ord_ext (map Var.varName binders))
444 ord_ext n1 n2 | Just m1 <- nameModule_maybe n1
445 , Just m2 <- nameModule_maybe n2
446 = compare (m1, nameOccName n1) (m2, nameOccName n2)
447 | otherwise = LT
448
449 -- If you edit this function, you may need to update the GHC formalism
450 -- See Note [GHC Formalism]
451 lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
452 lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
453
454 {-
455 ************************************************************************
456 * *
457 \subsection[lintUnfolding]{lintUnfolding}
458 * *
459 ************************************************************************
460
461 Note [Linting Unfoldings from Interfaces]
462 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
463
464 We use this to check all top-level unfoldings that come in from interfaces
465 (it is very painful to catch errors otherwise).
466
467 We do not need to call lintUnfolding on unfoldings that are nested within
468 top-level unfoldings; they are linted when we lint the top-level unfolding;
469 hence the `TopLevelFlag` on `tcPragExpr` in TcIface.
470
471 -}
472
473 lintUnfolding :: DynFlags
474 -> SrcLoc
475 -> VarSet -- Treat these as in scope
476 -> CoreExpr
477 -> Maybe MsgDoc -- Nothing => OK
478
479 lintUnfolding dflags locn vars expr
480 | isEmptyBag errs = Nothing
481 | otherwise = Just (pprMessageBag errs)
482 where
483 in_scope = mkInScopeSet vars
484 (_warns, errs) = initL dflags defaultLintFlags in_scope linter
485 linter = addLoc (ImportedUnfolding locn) $
486 lintCoreExpr expr
487
488 lintExpr :: DynFlags
489 -> [Var] -- Treat these as in scope
490 -> CoreExpr
491 -> Maybe MsgDoc -- Nothing => OK
492
493 lintExpr dflags vars expr
494 | isEmptyBag errs = Nothing
495 | otherwise = Just (pprMessageBag errs)
496 where
497 in_scope = mkInScopeSet (mkVarSet vars)
498 (_warns, errs) = initL dflags defaultLintFlags in_scope linter
499 linter = addLoc TopLevelBindings $
500 lintCoreExpr expr
501
502 {-
503 ************************************************************************
504 * *
505 \subsection[lintCoreBinding]{lintCoreBinding}
506 * *
507 ************************************************************************
508
509 Check a core binding, returning the list of variables bound.
510 -}
511
512 lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
513 -- If you edit this function, you may need to update the GHC formalism
514 -- See Note [GHC Formalism]
515 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
516 = addLoc (RhsOf binder) $
517 -- Check the rhs
518 do { ty <- lintRhs binder rhs
519 ; binder_ty <- applySubstTy (idType binder)
520 ; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty)
521
522 -- If the binding is for a CoVar, the RHS should be (Coercion co)
523 -- See Note [CoreSyn type and coercion invariant] in CoreSyn
524 ; checkL (not (isCoVar binder) || isCoArg rhs)
525 (mkLetErr binder rhs)
526
527 -- Check that it's not levity-polymorphic
528 -- Do this first, because otherwise isUnliftedType panics
529 -- Annoyingly, this duplicates the test in lintIdBdr,
530 -- because for non-rec lets we call lintSingleBinding first
531 ; checkL (isJoinId binder || not (isTypeLevPoly binder_ty))
532 (badBndrTyMsg binder (text "levity-polymorphic"))
533
534 -- Check the let/app invariant
535 -- See Note [CoreSyn let/app invariant] in CoreSyn
536 ; checkL ( isJoinId binder
537 || not (isUnliftedType binder_ty)
538 || (isNonRec rec_flag && exprOkForSpeculation rhs)
539 || exprIsTickedString rhs)
540 (badBndrTyMsg binder (text "unlifted"))
541
542 -- Check that if the binder is top-level or recursive, it's not
543 -- demanded. Primitive string literals are exempt as there is no
544 -- computation to perform, see Note [CoreSyn top-level string literals].
545 ; checkL (not (isStrictId binder)
546 || (isNonRec rec_flag && not (isTopLevel top_lvl_flag))
547 || exprIsTickedString rhs)
548 (mkStrictMsg binder)
549
550 -- Check that if the binder is at the top level and has type Addr#,
551 -- that it is a string literal, see
552 -- Note [CoreSyn top-level string literals].
553 ; checkL (not (isTopLevel top_lvl_flag && binder_ty `eqType` addrPrimTy)
554 || exprIsTickedString rhs)
555 (mkTopNonLitStrMsg binder)
556
557 ; flags <- getLintFlags
558
559 -- Check that a join-point binder has a valid type
560 -- NB: lintIdBinder has checked that it is not top-level bound
561 ; case isJoinId_maybe binder of
562 Nothing -> return ()
563 Just arity -> checkL (isValidJoinPointType arity binder_ty)
564 (mkInvalidJoinPointMsg binder binder_ty)
565
566 ; when (lf_check_inline_loop_breakers flags
567 && isStableUnfolding (realIdUnfolding binder)
568 && isStrongLoopBreaker (idOccInfo binder)
569 && isInlinePragma (idInlinePragma binder))
570 (addWarnL (text "INLINE binder is (non-rule) loop breaker:" <+> ppr binder))
571 -- Only non-rule loop breakers inhibit inlining
572
573 -- We used to check that the dmdTypeDepth of a demand signature never
574 -- exceeds idArity, but that is an unnecessary complication, see
575 -- Note [idArity varies independently of dmdTypeDepth] in DmdAnal
576
577 -- Check that the binder's arity is within the bounds imposed by
578 -- the type and the strictness signature. See Note [exprArity invariant]
579 -- and Note [Trimming arity]
580 ; checkL (typeArity (idType binder) `lengthAtLeast` idArity binder)
581 (text "idArity" <+> ppr (idArity binder) <+>
582 text "exceeds typeArity" <+>
583 ppr (length (typeArity (idType binder))) <> colon <+>
584 ppr binder)
585
586 ; case splitStrictSig (idStrictness binder) of
587 (demands, result_info) | isBotRes result_info ->
588 checkL (demands `lengthAtLeast` idArity binder)
589 (text "idArity" <+> ppr (idArity binder) <+>
590 text "exceeds arity imposed by the strictness signature" <+>
591 ppr (idStrictness binder) <> colon <+>
592 ppr binder)
593 _ -> return ()
594
595 ; mapM_ (lintCoreRule binder binder_ty) (idCoreRules binder)
596
597 ; addLoc (UnfoldingOf binder) $
598 lintIdUnfolding binder binder_ty (idUnfolding binder) }
599
600 -- We should check the unfolding, if any, but this is tricky because
601 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
602
603 -- | Checks the RHS of bindings. It only differs from 'lintCoreExpr'
604 -- in that it doesn't reject occurrences of the function 'makeStatic' when they
605 -- appear at the top level and @lf_check_static_ptrs == AllowAtTopLevel@, and
606 -- for join points, it skips the outer lambdas that take arguments to the
607 -- join point.
608 --
609 -- See Note [Checking StaticPtrs].
610 lintRhs :: Id -> CoreExpr -> LintM OutType
611 lintRhs bndr rhs
612 | Just arity <- isJoinId_maybe bndr
613 = lint_join_lams arity arity True rhs
614 | AlwaysTailCalled arity <- tailCallInfo (idOccInfo bndr)
615 = lint_join_lams arity arity False rhs
616 where
617 lint_join_lams 0 _ _ rhs
618 = lintCoreExpr rhs
619
620 lint_join_lams n tot enforce (Lam var expr)
621 = addLoc (LambdaBodyOf var) $
622 lintBinder LambdaBind var $ \ var' ->
623 do { body_ty <- lint_join_lams (n-1) tot enforce expr
624 ; return $ mkLamType var' body_ty }
625
626 lint_join_lams n tot True _other
627 = failWithL $ mkBadJoinArityMsg bndr tot (tot-n) rhs
628 lint_join_lams _ _ False rhs
629 = markAllJoinsBad $ lintCoreExpr rhs
630 -- Future join point, not yet eta-expanded
631 -- Body is not a tail position
632
633 -- Allow applications of the data constructor @StaticPtr@ at the top
634 -- but produce errors otherwise.
635 lintRhs _bndr rhs = fmap lf_check_static_ptrs getLintFlags >>= go
636 where
637 -- Allow occurrences of 'makeStatic' at the top-level but produce errors
638 -- otherwise.
639 go AllowAtTopLevel
640 | (binders0, rhs') <- collectTyBinders rhs
641 , Just (fun, t, info, e) <- collectMakeStaticArgs rhs'
642 = markAllJoinsBad $
643 foldr
644 -- imitate @lintCoreExpr (Lam ...)@
645 (\var loopBinders ->
646 addLoc (LambdaBodyOf var) $
647 lintBinder LambdaBind var $ \var' ->
648 do { body_ty <- loopBinders
649 ; return $ mkLamType var' body_ty }
650 )
651 -- imitate @lintCoreExpr (App ...)@
652 (do fun_ty <- lintCoreExpr fun
653 addLoc (AnExpr rhs') $ lintCoreArgs fun_ty [Type t, info, e]
654 )
655 binders0
656 go _ = markAllJoinsBad $ lintCoreExpr rhs
657
658 lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
659 lintIdUnfolding bndr bndr_ty uf
660 | isStableUnfolding uf
661 , Just rhs <- maybeUnfoldingTemplate uf
662 = do { ty <- lintRhs bndr rhs
663 ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) }
664 lintIdUnfolding _ _ _
665 = return () -- Do not Lint unstable unfoldings, because that leads
666 -- to exponential behaviour; c.f. CoreFVs.idUnfoldingVars
667
668 {-
669 Note [Checking for INLINE loop breakers]
670 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
671 It's very suspicious if a strong loop breaker is marked INLINE.
672
673 However, the desugarer generates instance methods with INLINE pragmas
674 that form a mutually recursive group. Only after a round of
675 simplification are they unravelled. So we suppress the test for
676 the desugarer.
677
678 ************************************************************************
679 * *
680 \subsection[lintCoreExpr]{lintCoreExpr}
681 * *
682 ************************************************************************
683 -}
684
685 -- For OutType, OutKind, the substitution has been applied,
686 -- but has not been linted yet
687
688 type LintedType = Type -- Substitution applied, and type is linted
689 type LintedKind = Kind
690
691 lintCoreExpr :: CoreExpr -> LintM OutType
692 -- The returned type has the substitution from the monad
693 -- already applied to it:
694 -- lintCoreExpr e subst = exprType (subst e)
695 --
696 -- The returned "type" can be a kind, if the expression is (Type ty)
697
698 -- If you edit this function, you may need to update the GHC formalism
699 -- See Note [GHC Formalism]
700 lintCoreExpr (Var var)
701 = lintVarOcc var 0
702
703 lintCoreExpr (Lit lit)
704 = return (literalType lit)
705
706 lintCoreExpr (Cast expr co)
707 = do { expr_ty <- markAllJoinsBad $ lintCoreExpr expr
708 ; co' <- applySubstCo co
709 ; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
710 ; checkValueKind k2 (text "target of cast" <+> quotes (ppr co))
711 ; lintRole co' Representational r
712 ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
713 ; return to_ty }
714
715 lintCoreExpr (Tick tickish expr)
716 = do case tickish of
717 Breakpoint _ ids -> forM_ ids $ \id -> do
718 checkDeadIdOcc id
719 lookupIdInScope id
720 _ -> return ()
721 markAllJoinsBadIf block_joins $ lintCoreExpr expr
722 where
723 block_joins = not (tickish `tickishScopesLike` SoftScope)
724 -- TODO Consider whether this is the correct rule. It is consistent with
725 -- the simplifier's behaviour - cost-centre-scoped ticks become part of
726 -- the continuation, and thus they behave like part of an evaluation
727 -- context, but soft-scoped and non-scoped ticks simply wrap the result
728 -- (see Simplify.simplTick).
729
730 lintCoreExpr (Let (NonRec tv (Type ty)) body)
731 | isTyVar tv
732 = -- See Note [Linting type lets]
733 do { ty' <- applySubstTy ty
734 ; lintTyBndr tv $ \ tv' ->
735 do { addLoc (RhsOf tv) $ lintTyKind tv' ty'
736 -- Now extend the substitution so we
737 -- take advantage of it in the body
738 ; extendSubstL tv ty' $
739 addLoc (BodyOfLetRec [tv]) $
740 lintCoreExpr body } }
741
742 lintCoreExpr (Let (NonRec bndr rhs) body)
743 | isId bndr
744 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
745 ; addLoc (BodyOfLetRec [bndr])
746 (lintBinder LetBind bndr $ \_ ->
747 addGoodJoins [bndr] $
748 lintCoreExpr body) }
749
750 | otherwise
751 = failWithL (mkLetErr bndr rhs) -- Not quite accurate
752
753 lintCoreExpr e@(Let (Rec pairs) body)
754 = lintLetBndrs NotTopLevel bndrs $
755 addGoodJoins bndrs $
756 do { -- Check that the list of pairs is non-empty
757 checkL (not (null pairs)) (emptyRec e)
758
759 -- Check that there are no duplicated binders
760 ; checkL (null dups) (dupVars dups)
761
762 -- Check that either all the binders are joins, or none
763 ; checkL (all isJoinId bndrs || all (not . isJoinId) bndrs) $
764 mkInconsistentRecMsg bndrs
765
766 ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
767 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
768 where
769 bndrs = map fst pairs
770 (_, dups) = removeDups compare bndrs
771
772 lintCoreExpr e@(App _ _)
773 = addLoc (AnExpr e) $
774 do { fun_ty <- lintCoreFun fun (length args)
775 ; lintCoreArgs fun_ty args }
776 where
777 (fun, args) = collectArgs e
778
779 lintCoreExpr (Lam var expr)
780 = addLoc (LambdaBodyOf var) $
781 markAllJoinsBad $
782 lintBinder LambdaBind var $ \ var' ->
783 do { body_ty <- lintCoreExpr expr
784 ; return $ mkLamType var' body_ty }
785
786 lintCoreExpr e@(Case scrut var alt_ty alts) =
787 -- Check the scrutinee
788 do { let scrut_diverges = exprIsBottom scrut
789 ; scrut_ty <- markAllJoinsBad $ lintCoreExpr scrut
790 ; (alt_ty, _) <- lintInTy alt_ty
791 ; (var_ty, _) <- lintInTy (idType var)
792
793 -- We used to try to check whether a case expression with no
794 -- alternatives was legitimate, but this didn't work.
795 -- See Note [No alternatives lint check] for details.
796
797 -- See Note [Rules for floating-point comparisons] in PrelRules
798 ; let isLitPat (LitAlt _, _ , _) = True
799 isLitPat _ = False
800 ; checkL (not $ isFloatingTy scrut_ty && any isLitPat alts)
801 (ptext (sLit $ "Lint warning: Scrutinising floating-point " ++
802 "expression with literal pattern in case " ++
803 "analysis (see #9238).")
804 $$ text "scrut" <+> ppr scrut)
805
806 ; case tyConAppTyCon_maybe (idType var) of
807 Just tycon
808 | debugIsOn
809 , isAlgTyCon tycon
810 , not (isAbstractTyCon tycon)
811 , null (tyConDataCons tycon)
812 , not scrut_diverges
813 -> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
814 -- This can legitimately happen for type families
815 $ return ()
816 _otherwise -> return ()
817
818 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
819
820 ; subst <- getTCvSubst
821 ; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
822
823 ; lintBinder CaseBind var $ \_ ->
824 do { -- Check the alternatives
825 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
826 ; checkCaseAlts e scrut_ty alts
827 ; return alt_ty } }
828
829 -- This case can't happen; linting types in expressions gets routed through
830 -- lintCoreArgs
831 lintCoreExpr (Type ty)
832 = failWithL (text "Type found as expression" <+> ppr ty)
833
834 lintCoreExpr (Coercion co)
835 = do { (k1, k2, ty1, ty2, role) <- lintInCo co
836 ; return (mkHeteroCoercionType role k1 k2 ty1 ty2) }
837
838 ----------------------
839 lintVarOcc :: Var -> Int -- Number of arguments (type or value) being passed
840 -> LintM Type -- returns type of the *variable*
841 lintVarOcc var nargs
842 = do { checkL (isNonCoVarId var)
843 (text "Non term variable" <+> ppr var)
844 -- See CoreSyn Note [Variable occurrences in Core]
845
846 -- Cneck that the type of the occurrence is the same
847 -- as the type of the binding site
848 ; ty <- applySubstTy (idType var)
849 ; var' <- lookupIdInScope var
850 ; let ty' = idType var'
851 ; ensureEqTys ty ty' $ mkBndrOccTypeMismatchMsg var' var ty' ty
852
853 -- Check for a nested occurrence of the StaticPtr constructor.
854 -- See Note [Checking StaticPtrs].
855 ; lf <- getLintFlags
856 ; when (nargs /= 0 && lf_check_static_ptrs lf /= AllowAnywhere) $
857 checkL (idName var /= makeStaticName) $
858 text "Found makeStatic nested in an expression"
859
860 ; checkDeadIdOcc var
861 ; checkJoinOcc var nargs
862
863 ; return (idType var') }
864
865 lintCoreFun :: CoreExpr
866 -> Int -- Number of arguments (type or val) being passed
867 -> LintM Type -- Returns type of the *function*
868 lintCoreFun (Var var) nargs
869 = lintVarOcc var nargs
870
871 lintCoreFun (Lam var body) nargs
872 -- Act like lintCoreExpr of Lam, but *don't* call markAllJoinsBad; see
873 -- Note [Beta redexes]
874 | nargs /= 0
875 = addLoc (LambdaBodyOf var) $
876 lintBinder LambdaBind var $ \ var' ->
877 do { body_ty <- lintCoreFun body (nargs - 1)
878 ; return $ mkLamType var' body_ty }
879
880 lintCoreFun expr nargs
881 = markAllJoinsBadIf (nargs /= 0) $
882 lintCoreExpr expr
883
884 ------------------
885 checkDeadIdOcc :: Id -> LintM ()
886 -- Occurrences of an Id should never be dead....
887 -- except when we are checking a case pattern
888 checkDeadIdOcc id
889 | isDeadOcc (idOccInfo id)
890 = do { in_case <- inCasePat
891 ; checkL in_case
892 (text "Occurrence of a dead Id" <+> ppr id) }
893 | otherwise
894 = return ()
895
896 ------------------
897 checkJoinOcc :: Id -> JoinArity -> LintM ()
898 -- Check that if the occurrence is a JoinId, then so is the
899 -- binding site, and it's a valid join Id
900 checkJoinOcc var n_args
901 | Just join_arity_occ <- isJoinId_maybe var
902 = do { mb_join_arity_bndr <- lookupJoinId var
903 ; case mb_join_arity_bndr of {
904 Nothing -> -- Binder is not a join point
905 addErrL (invalidJoinOcc var) ;
906
907 Just join_arity_bndr ->
908
909 do { checkL (join_arity_bndr == join_arity_occ) $
910 -- Arity differs at binding site and occurrence
911 mkJoinBndrOccMismatchMsg var join_arity_bndr join_arity_occ
912
913 ; checkL (n_args == join_arity_occ) $
914 -- Arity doesn't match #args
915 mkBadJumpMsg var join_arity_occ n_args } } }
916
917 | otherwise
918 = return ()
919
920 {-
921 Note [No alternatives lint check]
922 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
923 Case expressions with no alternatives are odd beasts, and it would seem
924 like they would worth be looking at in the linter (cf #10180). We
925 used to check two things:
926
927 * exprIsHNF is false: it would *seem* to be terribly wrong if
928 the scrutinee was already in head normal form.
929
930 * exprIsBottom is true: we should be able to see why GHC believes the
931 scrutinee is diverging for sure.
932
933 It was already known that the second test was not entirely reliable.
934 Unfortunately (#13990), the first test turned out not to be reliable
935 either. Getting the checks right turns out to be somewhat complicated.
936
937 For example, suppose we have (comment 8)
938
939 data T a where
940 TInt :: T Int
941
942 absurdTBool :: T Bool -> a
943 absurdTBool v = case v of
944
945 data Foo = Foo !(T Bool)
946
947 absurdFoo :: Foo -> a
948 absurdFoo (Foo x) = absurdTBool x
949
950 GHC initially accepts the empty case because of the GADT conditions. But then
951 we inline absurdTBool, getting
952
953 absurdFoo (Foo x) = case x of
954
955 x is in normal form (because the Foo constructor is strict) but the
956 case is empty. To avoid this problem, GHC would have to recognize
957 that matching on Foo x is already absurd, which is not so easy.
958
959 More generally, we don't really know all the ways that GHC can
960 lose track of why an expression is bottom, so we shouldn't make too
961 much fuss when that happens.
962
963
964 Note [Beta redexes]
965 ~~~~~~~~~~~~~~~~~~~
966 Consider:
967
968 join j @x y z = ... in
969 (\@x y z -> jump j @x y z) @t e1 e2
970
971 This is clearly ill-typed, since the jump is inside both an application and a
972 lambda, either of which is enough to disqualify it as a tail call (see Note
973 [Invariants on join points] in CoreSyn). However, strictly from a
974 lambda-calculus perspective, the term doesn't go wrong---after the two beta
975 reductions, the jump *is* a tail call and everything is fine.
976
977 Why would we want to allow this when we have let? One reason is that a compound
978 beta redex (that is, one with more than one argument) has different scoping
979 rules: naively reducing the above example using lets will capture any free
980 occurrence of y in e2. More fundamentally, type lets are tricky; many passes,
981 such as Float Out, tacitly assume that the incoming program's type lets have
982 all been dealt with by the simplifier. Thus we don't want to let-bind any types
983 in, say, CoreSubst.simpleOptPgm, which in some circumstances can run immediately
984 before Float Out.
985
986 All that said, currently CoreSubst.simpleOptPgm is the only thing using this
987 loophole, doing so to avoid re-traversing large functions (beta-reducing a type
988 lambda without introducing a type let requires a substitution). TODO: Improve
989 simpleOptPgm so that we can forget all this ever happened.
990
991 ************************************************************************
992 * *
993 \subsection[lintCoreArgs]{lintCoreArgs}
994 * *
995 ************************************************************************
996
997 The basic version of these functions checks that the argument is a
998 subtype of the required type, as one would expect.
999 -}
1000
1001
1002 lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
1003 lintCoreArgs fun_ty args = foldM lintCoreArg fun_ty args
1004
1005 lintCoreArg :: OutType -> CoreArg -> LintM OutType
1006 lintCoreArg fun_ty (Type arg_ty)
1007 = do { checkL (not (isCoercionTy arg_ty))
1008 (text "Unnecessary coercion-to-type injection:"
1009 <+> ppr arg_ty)
1010 ; arg_ty' <- applySubstTy arg_ty
1011 ; lintTyApp fun_ty arg_ty' }
1012
1013 lintCoreArg fun_ty arg
1014 = do { arg_ty <- markAllJoinsBad $ lintCoreExpr arg
1015 -- See Note [Levity polymorphism invariants] in CoreSyn
1016 ; lintL (not (isTypeLevPoly arg_ty))
1017 (text "Levity-polymorphic argument:" <+>
1018 (ppr arg <+> dcolon <+> parens (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))))
1019 -- check for levity polymorphism first, because otherwise isUnliftedType panics
1020
1021 ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
1022 (mkLetAppMsg arg)
1023 ; lintValApp arg fun_ty arg_ty }
1024
1025 -----------------
1026 lintAltBinders :: OutType -- Scrutinee type
1027 -> OutType -- Constructor type
1028 -> [OutVar] -- Binders
1029 -> LintM ()
1030 -- If you edit this function, you may need to update the GHC formalism
1031 -- See Note [GHC Formalism]
1032 lintAltBinders scrut_ty con_ty []
1033 = ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
1034 lintAltBinders scrut_ty con_ty (bndr:bndrs)
1035 | isTyVar bndr
1036 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
1037 ; lintAltBinders scrut_ty con_ty' bndrs }
1038 | otherwise
1039 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
1040 ; lintAltBinders scrut_ty con_ty' bndrs }
1041
1042 -----------------
1043 lintTyApp :: OutType -> OutType -> LintM OutType
1044 lintTyApp fun_ty arg_ty
1045 | Just (tv,body_ty) <- splitForAllTy_maybe fun_ty
1046 = do { lintTyKind tv arg_ty
1047 ; in_scope <- getInScope
1048 -- substTy needs the set of tyvars in scope to avoid generating
1049 -- uniques that are already in scope.
1050 -- See Note [The substitution invariant] in TyCoRep
1051 ; return (substTyWithInScope in_scope [tv] [arg_ty] body_ty) }
1052
1053 | otherwise
1054 = failWithL (mkTyAppMsg fun_ty arg_ty)
1055
1056 -----------------
1057 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
1058 lintValApp arg fun_ty arg_ty
1059 | Just (arg,res) <- splitFunTy_maybe fun_ty
1060 = do { ensureEqTys arg arg_ty err1
1061 ; return res }
1062 | otherwise
1063 = failWithL err2
1064 where
1065 err1 = mkAppMsg fun_ty arg_ty arg
1066 err2 = mkNonFunAppMsg fun_ty arg_ty arg
1067
1068 lintTyKind :: OutTyVar -> OutType -> LintM ()
1069 -- Both args have had substitution applied
1070
1071 -- If you edit this function, you may need to update the GHC formalism
1072 -- See Note [GHC Formalism]
1073 lintTyKind tyvar arg_ty
1074 -- Arg type might be boxed for a function with an uncommitted
1075 -- tyvar; notably this is used so that we can give
1076 -- error :: forall a:*. String -> a
1077 -- and then apply it to both boxed and unboxed types.
1078 = do { arg_kind <- lintType arg_ty
1079 ; unless (arg_kind `eqType` tyvar_kind)
1080 (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "Linted Arg kind:" <+> ppr arg_kind))) }
1081 where
1082 tyvar_kind = tyVarKind tyvar
1083
1084 {-
1085 ************************************************************************
1086 * *
1087 \subsection[lintCoreAlts]{lintCoreAlts}
1088 * *
1089 ************************************************************************
1090 -}
1091
1092 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
1093 -- a) Check that the alts are non-empty
1094 -- b1) Check that the DEFAULT comes first, if it exists
1095 -- b2) Check that the others are in increasing order
1096 -- c) Check that there's a default for infinite types
1097 -- NB: Algebraic cases are not necessarily exhaustive, because
1098 -- the simplifier correctly eliminates case that can't
1099 -- possibly match.
1100
1101 checkCaseAlts e ty alts =
1102 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
1103 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
1104
1105 -- For types Int#, Word# with an infinite (well, large!) number of
1106 -- possible values, there should usually be a DEFAULT case
1107 -- But (see Note [Empty case alternatives] in CoreSyn) it's ok to
1108 -- have *no* case alternatives.
1109 -- In effect, this is a kind of partial test. I suppose it's possible
1110 -- that we might *know* that 'x' was 1 or 2, in which case
1111 -- case x of { 1 -> e1; 2 -> e2 }
1112 -- would be fine.
1113 ; checkL (isJust maybe_deflt || not is_infinite_ty || null alts)
1114 (nonExhaustiveAltsMsg e) }
1115 where
1116 (con_alts, maybe_deflt) = findDefault alts
1117
1118 -- Check that successive alternatives have strictly increasing tags
1119 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
1120 increasing_tag _ = True
1121
1122 non_deflt (DEFAULT, _, _) = False
1123 non_deflt _ = True
1124
1125 is_infinite_ty = case tyConAppTyCon_maybe ty of
1126 Nothing -> False
1127 Just tycon -> isPrimTyCon tycon
1128
1129 lintAltExpr :: CoreExpr -> OutType -> LintM ()
1130 lintAltExpr expr ann_ty
1131 = do { actual_ty <- lintCoreExpr expr
1132 ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
1133
1134 lintCoreAlt :: OutType -- Type of scrutinee
1135 -> OutType -- Type of the alternative
1136 -> CoreAlt
1137 -> LintM ()
1138 -- If you edit this function, you may need to update the GHC formalism
1139 -- See Note [GHC Formalism]
1140 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
1141 do { lintL (null args) (mkDefaultArgsMsg args)
1142 ; lintAltExpr rhs alt_ty }
1143
1144 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
1145 | litIsLifted lit
1146 = failWithL integerScrutinisedMsg
1147 | otherwise
1148 = do { lintL (null args) (mkDefaultArgsMsg args)
1149 ; ensureEqTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
1150 ; lintAltExpr rhs alt_ty }
1151 where
1152 lit_ty = literalType lit
1153
1154 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
1155 | isNewTyCon (dataConTyCon con)
1156 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
1157 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
1158 = addLoc (CaseAlt alt) $ do
1159 { -- First instantiate the universally quantified
1160 -- type variables of the data constructor
1161 -- We've already check
1162 lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
1163 ; let con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys
1164
1165 -- And now bring the new binders into scope
1166 ; lintBinders CasePatBind args $ \ args' -> do
1167 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
1168 ; lintAltExpr rhs alt_ty } }
1169
1170 | otherwise -- Scrut-ty is wrong shape
1171 = addErrL (mkBadAltMsg scrut_ty alt)
1172
1173 {-
1174 ************************************************************************
1175 * *
1176 \subsection[lint-types]{Types}
1177 * *
1178 ************************************************************************
1179 -}
1180
1181 -- When we lint binders, we (one at a time and in order):
1182 -- 1. Lint var types or kinds (possibly substituting)
1183 -- 2. Add the binder to the in scope set, and if its a coercion var,
1184 -- we may extend the substitution to reflect its (possibly) new kind
1185 lintBinders :: BindingSite -> [Var] -> ([Var] -> LintM a) -> LintM a
1186 lintBinders _ [] linterF = linterF []
1187 lintBinders site (var:vars) linterF = lintBinder site var $ \var' ->
1188 lintBinders site vars $ \ vars' ->
1189 linterF (var':vars')
1190
1191 -- If you edit this function, you may need to update the GHC formalism
1192 -- See Note [GHC Formalism]
1193 lintBinder :: BindingSite -> Var -> (Var -> LintM a) -> LintM a
1194 lintBinder site var linterF
1195 | isTyVar var = lintTyBndr var linterF
1196 | isCoVar var = lintCoBndr var linterF
1197 | otherwise = lintIdBndr NotTopLevel site var linterF
1198
1199 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
1200 lintTyBndr tv thing_inside
1201 = do { subst <- getTCvSubst
1202 ; let (subst', tv') = substTyVarBndr subst tv
1203 ; lintKind (varType tv')
1204 ; updateTCvSubst subst' (thing_inside tv') }
1205
1206 lintCoBndr :: InCoVar -> (OutCoVar -> LintM a) -> LintM a
1207 lintCoBndr cv thing_inside
1208 = do { subst <- getTCvSubst
1209 ; let (subst', cv') = substCoVarBndr subst cv
1210 ; lintKind (varType cv')
1211 ; lintL (isCoVarType (varType cv'))
1212 (text "CoVar with non-coercion type:" <+> pprTyVar cv)
1213 ; updateTCvSubst subst' (thing_inside cv') }
1214
1215 lintLetBndrs :: TopLevelFlag -> [Var] -> LintM a -> LintM a
1216 lintLetBndrs top_lvl ids linterF
1217 = go ids
1218 where
1219 go [] = linterF
1220 go (id:ids) = lintIdBndr top_lvl LetBind id $ \_ ->
1221 go ids
1222
1223 lintIdBndr :: TopLevelFlag -> BindingSite
1224 -> InVar -> (OutVar -> LintM a) -> LintM a
1225 -- Do substitution on the type of a binder and add the var with this
1226 -- new type to the in-scope set of the second argument
1227 -- ToDo: lint its rules
1228 lintIdBndr top_lvl bind_site id linterF
1229 = ASSERT2( isId id, ppr id )
1230 do { flags <- getLintFlags
1231 ; checkL (not (lf_check_global_ids flags) || isLocalId id)
1232 (text "Non-local Id binder" <+> ppr id)
1233 -- See Note [Checking for global Ids]
1234
1235 -- Check that if the binder is nested, it is not marked as exported
1236 ; checkL (not (isExportedId id) || is_top_lvl)
1237 (mkNonTopExportedMsg id)
1238
1239 -- Check that if the binder is nested, it does not have an external name
1240 ; checkL (not (isExternalName (Var.varName id)) || is_top_lvl)
1241 (mkNonTopExternalNameMsg id)
1242
1243 ; (ty, k) <- lintInTy (idType id)
1244
1245 -- See Note [Levity polymorphism invariants] in CoreSyn
1246 ; lintL (isJoinId id || not (isKindLevPoly k))
1247 (text "Levity-polymorphic binder:" <+>
1248 (ppr id <+> dcolon <+> parens (ppr ty <+> dcolon <+> ppr k)))
1249
1250 -- Check that a join-id is a not-top-level let-binding
1251 ; when (isJoinId id) $
1252 checkL (not is_top_lvl && is_let_bind) $
1253 mkBadJoinBindMsg id
1254
1255 -- Check that the Id does not have type (t1 ~# t2) or (t1 ~R# t2);
1256 -- if so, it should be a CoVar, and checked by lintCoVarBndr
1257 ; lintL (not (isCoVarType ty))
1258 (text "Non-CoVar has coercion type" <+> ppr id <+> dcolon <+> ppr ty)
1259
1260 ; let id' = setIdType id ty
1261 ; addInScopeVar id' $ (linterF id') }
1262 where
1263 is_top_lvl = isTopLevel top_lvl
1264 is_let_bind = case bind_site of
1265 LetBind -> True
1266 _ -> False
1267
1268 {-
1269 %************************************************************************
1270 %* *
1271 Types
1272 %* *
1273 %************************************************************************
1274 -}
1275
1276 lintTypes :: DynFlags
1277 -> [TyCoVar] -- Treat these as in scope
1278 -> [Type]
1279 -> Maybe MsgDoc -- Nothing => OK
1280 lintTypes dflags vars tys
1281 | isEmptyBag errs = Nothing
1282 | otherwise = Just (pprMessageBag errs)
1283 where
1284 in_scope = emptyInScopeSet
1285 (_warns, errs) = initL dflags defaultLintFlags in_scope linter
1286 linter = lintBinders LambdaBind vars $ \_ ->
1287 mapM_ lintInTy tys
1288
1289 lintInTy :: InType -> LintM (LintedType, LintedKind)
1290 -- Types only, not kinds
1291 -- Check the type, and apply the substitution to it
1292 -- See Note [Linting type lets]
1293 lintInTy ty
1294 = addLoc (InType ty) $
1295 do { ty' <- applySubstTy ty
1296 ; k <- lintType ty'
1297 ; lintKind k -- The kind returned by lintType is already
1298 -- a LintedKind but we also want to check that
1299 -- k :: *, which lintKind does
1300 ; return (ty', k) }
1301
1302 checkTyCon :: TyCon -> LintM ()
1303 checkTyCon tc
1304 = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
1305
1306 -------------------
1307 lintType :: OutType -> LintM LintedKind
1308 -- The returned Kind has itself been linted
1309
1310 -- If you edit this function, you may need to update the GHC formalism
1311 -- See Note [GHC Formalism]
1312 lintType (TyVarTy tv)
1313 = do { checkL (isTyVar tv) (mkBadTyVarMsg tv)
1314 ; lintTyCoVarInScope tv
1315 ; return (tyVarKind tv) }
1316 -- We checked its kind when we added it to the envt
1317
1318 lintType ty@(AppTy t1 t2)
1319 | TyConApp {} <- t1
1320 = failWithL $ text "TyConApp to the left of AppTy:" <+> ppr ty
1321 | otherwise
1322 = do { k1 <- lintType t1
1323 ; k2 <- lintType t2
1324 ; lint_ty_app ty k1 [(t2,k2)] }
1325
1326 lintType ty@(TyConApp tc tys)
1327 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
1328 = do { report_unsat <- lf_report_unsat_syns <$> getLintFlags
1329 ; lintTySynFamApp report_unsat ty tc tys }
1330
1331 | isFunTyCon tc
1332 , tys `lengthIs` 4
1333 -- We should never see a saturated application of funTyCon; such
1334 -- applications should be represented with the FunTy constructor.
1335 -- See Note [Linting function types] and
1336 -- Note [Representation of function types].
1337 = failWithL (hang (text "Saturated application of (->)") 2 (ppr ty))
1338
1339 | otherwise -- Data types, data families, primitive types
1340 = do { checkTyCon tc
1341 ; ks <- mapM lintType tys
1342 ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
1343
1344 -- arrows can related *unlifted* kinds, so this has to be separate from
1345 -- a dependent forall.
1346 lintType ty@(FunTy _ t1 t2)
1347 = do { k1 <- lintType t1
1348 ; k2 <- lintType t2
1349 ; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 }
1350
1351 lintType t@(ForAllTy (Bndr tv _vis) ty)
1352 -- forall over types
1353 | isTyVar tv
1354 = lintTyBndr tv $ \tv' ->
1355 do { k <- lintType ty
1356 ; checkValueKind k (text "the body of forall:" <+> ppr t)
1357 ; case occCheckExpand [tv'] k of -- See Note [Stupid type synonyms]
1358 Just k' -> return k'
1359 Nothing -> failWithL (hang (text "Variable escape in forall:")
1360 2 (vcat [ text "type:" <+> ppr t
1361 , text "kind:" <+> ppr k ]))
1362 }
1363
1364 lintType t@(ForAllTy (Bndr cv _vis) ty)
1365 -- forall over coercions
1366 = do { lintL (isCoVar cv)
1367 (text "Non-Tyvar or Non-Covar bound in type:" <+> ppr t)
1368 ; lintL (cv `elemVarSet` tyCoVarsOfType ty)
1369 (text "Covar does not occur in the body:" <+> ppr t)
1370 ; lintCoBndr cv $ \_ ->
1371 do { k <- lintType ty
1372 ; checkValueKind k (text "the body of forall:" <+> ppr t)
1373 ; return liftedTypeKind
1374 -- We don't check variable escape here. Namely, k could refer to cv'
1375 -- See Note [NthCo and newtypes] in TyCoRep
1376 }}
1377
1378 lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
1379
1380 lintType (CastTy ty co)
1381 = do { k1 <- lintType ty
1382 ; (k1', k2) <- lintStarCoercion co
1383 ; ensureEqTys k1 k1' (mkCastTyErr ty co k1' k1)
1384 ; return k2 }
1385
1386 lintType (CoercionTy co)
1387 = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
1388 ; return $ mkHeteroCoercionType r k1 k2 ty1 ty2 }
1389
1390 {- Note [Stupid type synonyms]
1391 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1392 Consider (#14939)
1393 type Alg cls ob = ob
1394 f :: forall (cls :: * -> Constraint) (b :: Alg cls *). b
1395
1396 Here 'cls' appears free in b's kind, which would usually be illegal
1397 (because in (forall a. ty), ty's kind should not mention 'a'). But
1398 #in this case (Alg cls *) = *, so all is well. Currently we allow
1399 this, and make Lint expand synonyms where necessary to make it so.
1400
1401 c.f. TcUnify.occCheckExpand and CoreUtils.coreAltsType which deal
1402 with the same problem. A single systematic solution eludes me.
1403 -}
1404
1405 -----------------
1406 lintTySynFamApp :: Bool -> Type -> TyCon -> [Type] -> LintM LintedKind
1407 -- The TyCon is a type synonym or a type family (not a data family)
1408 -- See Note [Linting type synonym applications]
1409 -- c.f. TcValidity.check_syn_tc_app
1410 lintTySynFamApp report_unsat ty tc tys
1411 | report_unsat -- Report unsaturated only if report_unsat is on
1412 , tys `lengthLessThan` tyConArity tc
1413 = failWithL (hang (text "Un-saturated type application") 2 (ppr ty))
1414
1415 -- Deal with type synonyms
1416 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
1417 , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
1418 = do { -- Kind-check the argument types, but without reporting
1419 -- un-saturated type families/synonyms
1420 ks <- setReportUnsat False (mapM lintType tys)
1421
1422 ; when report_unsat $
1423 do { _ <- lintType expanded_ty
1424 ; return () }
1425
1426 ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
1427
1428 -- Otherwise this must be a type family
1429 | otherwise
1430 = do { ks <- mapM lintType tys
1431 ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
1432
1433 -----------------
1434 lintKind :: OutKind -> LintM ()
1435 -- If you edit this function, you may need to update the GHC formalism
1436 -- See Note [GHC Formalism]
1437 lintKind k = do { sk <- lintType k
1438 ; unless (classifiesTypeWithValues sk)
1439 (addErrL (hang (text "Ill-kinded kind:" <+> ppr k)
1440 2 (text "has kind:" <+> ppr sk))) }
1441
1442 -----------------
1443 -- Confirms that a type is really *, #, Constraint etc
1444 checkValueKind :: OutKind -> SDoc -> LintM ()
1445 checkValueKind k doc
1446 = lintL (classifiesTypeWithValues k)
1447 (text "Non-*-like kind when *-like expected:" <+> ppr k $$
1448 text "when checking" <+> doc)
1449
1450 -----------------
1451 lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
1452 -- If you edit this function, you may need to update the GHC formalism
1453 -- See Note [GHC Formalism]
1454 lintArrow what k1 k2 -- Eg lintArrow "type or kind `blah'" k1 k2
1455 -- or lintarrow "coercion `blah'" k1 k2
1456 = do { unless (classifiesTypeWithValues k1) (addErrL (msg (text "argument") k1))
1457 ; unless (classifiesTypeWithValues k2) (addErrL (msg (text "result") k2))
1458 ; return liftedTypeKind }
1459 where
1460 msg ar k
1461 = vcat [ hang (text "Ill-kinded" <+> ar)
1462 2 (text "in" <+> what)
1463 , what <+> text "kind:" <+> ppr k ]
1464
1465 -----------------
1466 lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
1467 lint_ty_app ty k tys
1468 = lint_app (text "type" <+> quotes (ppr ty)) k tys
1469
1470 ----------------
1471 lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
1472 lint_co_app ty k tys
1473 = lint_app (text "coercion" <+> quotes (ppr ty)) k tys
1474
1475 ----------------
1476 lintTyLit :: TyLit -> LintM ()
1477 lintTyLit (NumTyLit n)
1478 | n >= 0 = return ()
1479 | otherwise = failWithL msg
1480 where msg = text "Negative type literal:" <+> integer n
1481 lintTyLit (StrTyLit _) = return ()
1482
1483 lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
1484 -- (lint_app d fun_kind arg_tys)
1485 -- We have an application (f arg_ty1 .. arg_tyn),
1486 -- where f :: fun_kind
1487 -- Takes care of linting the OutTypes
1488
1489 -- If you edit this function, you may need to update the GHC formalism
1490 -- See Note [GHC Formalism]
1491 lint_app doc kfn kas
1492 = do { in_scope <- getInScope
1493 -- We need the in_scope set to satisfy the invariant in
1494 -- Note [The substitution invariant] in TyCoRep
1495 ; foldlM (go_app in_scope) kfn kas }
1496 where
1497 fail_msg extra = vcat [ hang (text "Kind application error in") 2 doc
1498 , nest 2 (text "Function kind =" <+> ppr kfn)
1499 , nest 2 (text "Arg kinds =" <+> ppr kas)
1500 , extra ]
1501
1502 go_app in_scope kfn tka
1503 | Just kfn' <- coreView kfn
1504 = go_app in_scope kfn' tka
1505
1506 go_app _ (FunTy _ kfa kfb) tka@(_,ka)
1507 = do { unless (ka `eqType` kfa) $
1508 addErrL (fail_msg (text "Fun:" <+> (ppr kfa $$ ppr tka)))
1509 ; return kfb }
1510
1511 go_app in_scope (ForAllTy (Bndr kv _vis) kfn) tka@(ta,ka)
1512 = do { let kv_kind = varType kv
1513 ; unless (ka `eqType` kv_kind) $
1514 addErrL (fail_msg (text "Forall:" <+> (ppr kv $$ ppr kv_kind $$ ppr tka)))
1515 ; return $ substTy (extendTCvSubst (mkEmptyTCvSubst in_scope) kv ta) kfn }
1516
1517 go_app _ kfn ka
1518 = failWithL (fail_msg (text "Not a fun:" <+> (ppr kfn $$ ppr ka)))
1519
1520 {- *********************************************************************
1521 * *
1522 Linting rules
1523 * *
1524 ********************************************************************* -}
1525
1526 lintCoreRule :: OutVar -> OutType -> CoreRule -> LintM ()
1527 lintCoreRule _ _ (BuiltinRule {})
1528 = return () -- Don't bother
1529
1530 lintCoreRule fun fun_ty rule@(Rule { ru_name = name, ru_bndrs = bndrs
1531 , ru_args = args, ru_rhs = rhs })
1532 = lintBinders LambdaBind bndrs $ \ _ ->
1533 do { lhs_ty <- lintCoreArgs fun_ty args
1534 ; rhs_ty <- case isJoinId_maybe fun of
1535 Just join_arity
1536 -> do { checkL (args `lengthIs` join_arity) $
1537 mkBadJoinPointRuleMsg fun join_arity rule
1538 -- See Note [Rules for join points]
1539 ; lintCoreExpr rhs }
1540 _ -> markAllJoinsBad $ lintCoreExpr rhs
1541 ; ensureEqTys lhs_ty rhs_ty $
1542 (rule_doc <+> vcat [ text "lhs type:" <+> ppr lhs_ty
1543 , text "rhs type:" <+> ppr rhs_ty
1544 , text "fun_ty:" <+> ppr fun_ty ])
1545 ; let bad_bndrs = filter is_bad_bndr bndrs
1546
1547 ; checkL (null bad_bndrs)
1548 (rule_doc <+> text "unbound" <+> ppr bad_bndrs)
1549 -- See Note [Linting rules]
1550 }
1551 where
1552 rule_doc = text "Rule" <+> doubleQuotes (ftext name) <> colon
1553
1554 lhs_fvs = exprsFreeVars args
1555 rhs_fvs = exprFreeVars rhs
1556
1557 is_bad_bndr :: Var -> Bool
1558 -- See Note [Unbound RULE binders] in Rules
1559 is_bad_bndr bndr = not (bndr `elemVarSet` lhs_fvs)
1560 && bndr `elemVarSet` rhs_fvs
1561 && isNothing (isReflCoVar_maybe bndr)
1562
1563
1564 {- Note [Linting rules]
1565 ~~~~~~~~~~~~~~~~~~~~~~~
1566 It's very bad if simplifying a rule means that one of the template
1567 variables (ru_bndrs) that /is/ mentioned on the RHS becomes
1568 not-mentioned in the LHS (ru_args). How can that happen? Well, in
1569 #10602, SpecConstr stupidly constructed a rule like
1570
1571 forall x,c1,c2.
1572 f (x |> c1 |> c2) = ....
1573
1574 But simplExpr collapses those coercions into one. (Indeed in
1575 #10602, it collapsed to the identity and was removed altogether.)
1576
1577 We don't have a great story for what to do here, but at least
1578 this check will nail it.
1579
1580 NB (#11643): it's possible that a variable listed in the
1581 binders becomes not-mentioned on both LHS and RHS. Here's a silly
1582 example:
1583 RULE forall x y. f (g x y) = g (x+1) (y-1)
1584 And suppose worker/wrapper decides that 'x' is Absent. Then
1585 we'll end up with
1586 RULE forall x y. f ($gw y) = $gw (x+1)
1587 This seems sufficiently obscure that there isn't enough payoff to
1588 try to trim the forall'd binder list.
1589
1590 Note [Rules for join points]
1591 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1592
1593 A join point cannot be partially applied. However, the left-hand side of a rule
1594 for a join point is effectively a *pattern*, not a piece of code, so there's an
1595 argument to be made for allowing a situation like this:
1596
1597 join $sj :: Int -> Int -> String
1598 $sj n m = ...
1599 j :: forall a. Eq a => a -> a -> String
1600 {-# RULES "SPEC j" jump j @ Int $dEq = jump $sj #-}
1601 j @a $dEq x y = ...
1602
1603 Applying this rule can't turn a well-typed program into an ill-typed one, so
1604 conceivably we could allow it. But we can always eta-expand such an
1605 "undersaturated" rule (see 'CoreArity.etaExpandToJoinPointRule'), and in fact
1606 the simplifier would have to in order to deal with the RHS. So we take a
1607 conservative view and don't allow undersaturated rules for join points. See
1608 Note [Rules and join points] in OccurAnal for further discussion.
1609 -}
1610
1611 {-
1612 ************************************************************************
1613 * *
1614 Linting coercions
1615 * *
1616 ************************************************************************
1617 -}
1618
1619 lintInCo :: InCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
1620 -- Check the coercion, and apply the substitution to it
1621 -- See Note [Linting type lets]
1622 lintInCo co
1623 = addLoc (InCo co) $
1624 do { co' <- applySubstCo co
1625 ; lintCoercion co' }
1626
1627 -- lints a coercion, confirming that its lh kind and its rh kind are both *
1628 -- also ensures that the role is Nominal
1629 lintStarCoercion :: OutCoercion -> LintM (LintedType, LintedType)
1630 lintStarCoercion g
1631 = do { (k1, k2, t1, t2, r) <- lintCoercion g
1632 ; checkValueKind k1 (text "the kind of the left type in" <+> ppr g)
1633 ; checkValueKind k2 (text "the kind of the right type in" <+> ppr g)
1634 ; lintRole g Nominal r
1635 ; return (t1, t2) }
1636
1637 lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
1638 -- Check the kind of a coercion term, returning the kind
1639 -- Post-condition: the returned OutTypes are lint-free
1640 --
1641 -- If lintCoercion co = (k1, k2, s1, s2, r)
1642 -- then co :: s1 ~r s2
1643 -- s1 :: k1
1644 -- s2 :: k2
1645
1646 -- If you edit this function, you may need to update the GHC formalism
1647 -- See Note [GHC Formalism]
1648 lintCoercion (Refl ty)
1649 = do { k <- lintType ty
1650 ; return (k, k, ty, ty, Nominal) }
1651
1652 lintCoercion (GRefl r ty MRefl)
1653 = do { k <- lintType ty
1654 ; return (k, k, ty, ty, r) }
1655
1656 lintCoercion (GRefl r ty (MCo co))
1657 = do { k <- lintType ty
1658 ; (_, _, k1, k2, r') <- lintCoercion co
1659 ; ensureEqTys k k1
1660 (hang (text "GRefl coercion kind mis-match:" <+> ppr co)
1661 2 (vcat [ppr ty, ppr k, ppr k1]))
1662 ; lintRole co Nominal r'
1663 ; return (k1, k2, ty, mkCastTy ty co, r) }
1664
1665 lintCoercion co@(TyConAppCo r tc cos)
1666 | tc `hasKey` funTyConKey
1667 , [_rep1,_rep2,_co1,_co2] <- cos
1668 = do { failWithL (text "Saturated TyConAppCo (->):" <+> ppr co)
1669 } -- All saturated TyConAppCos should be FunCos
1670
1671 | Just {} <- synTyConDefn_maybe tc
1672 = failWithL (text "Synonym in TyConAppCo:" <+> ppr co)
1673
1674 | otherwise
1675 = do { checkTyCon tc
1676 ; (k's, ks, ss, ts, rs) <- mapAndUnzip5M lintCoercion cos
1677 ; k' <- lint_co_app co (tyConKind tc) (ss `zip` k's)
1678 ; k <- lint_co_app co (tyConKind tc) (ts `zip` ks)
1679 ; _ <- zipWith3M lintRole cos (tyConRolesX r tc) rs
1680 ; return (k', k, mkTyConApp tc ss, mkTyConApp tc ts, r) }
1681
1682 lintCoercion co@(AppCo co1 co2)
1683 | TyConAppCo {} <- co1
1684 = failWithL (text "TyConAppCo to the left of AppCo:" <+> ppr co)
1685 | Just (TyConApp {}, _) <- isReflCo_maybe co1
1686 = failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co)
1687 | otherwise
1688 = do { (k1, k2, s1, s2, r1) <- lintCoercion co1
1689 ; (k'1, k'2, t1, t2, r2) <- lintCoercion co2
1690 ; k3 <- lint_co_app co k1 [(t1,k'1)]
1691 ; k4 <- lint_co_app co k2 [(t2,k'2)]
1692 ; if r1 == Phantom
1693 then lintL (r2 == Phantom || r2 == Nominal)
1694 (text "Second argument in AppCo cannot be R:" $$
1695 ppr co)
1696 else lintRole co Nominal r2
1697 ; return (k3, k4, mkAppTy s1 t1, mkAppTy s2 t2, r1) }
1698
1699 ----------
1700 lintCoercion (ForAllCo tv1 kind_co co)
1701 -- forall over types
1702 | isTyVar tv1
1703 = do { (_, k2) <- lintStarCoercion kind_co
1704 ; let tv2 = setTyVarKind tv1 k2
1705 ; addInScopeVar tv1 $
1706 do {
1707 ; (k3, k4, t1, t2, r) <- lintCoercion co
1708 ; in_scope <- getInScope
1709 ; let tyl = mkInvForAllTy tv1 t1
1710 subst = mkTvSubst in_scope $
1711 -- We need both the free vars of the `t2` and the
1712 -- free vars of the range of the substitution in
1713 -- scope. All the free vars of `t2` and `kind_co` should
1714 -- already be in `in_scope`, because they've been
1715 -- linted and `tv2` has the same unique as `tv1`.
1716 -- See Note [The substitution invariant]
1717 unitVarEnv tv1 (TyVarTy tv2 `mkCastTy` mkSymCo kind_co)
1718 tyr = mkInvForAllTy tv2 $
1719 substTy subst t2
1720 ; return (k3, k4, tyl, tyr, r) } }
1721
1722 lintCoercion (ForAllCo cv1 kind_co co)
1723 -- forall over coercions
1724 = ASSERT( isCoVar cv1 )
1725 do { lintL (almostDevoidCoVarOfCo cv1 co)
1726 (text "Covar can only appear in Refl and GRefl: " <+> ppr co)
1727 ; (_, k2) <- lintStarCoercion kind_co
1728 ; let cv2 = setVarType cv1 k2
1729 ; addInScopeVar cv1 $
1730 do {
1731 ; (k3, k4, t1, t2, r) <- lintCoercion co
1732 ; checkValueKind k3 (text "the body of a ForAllCo over covar:" <+> ppr co)
1733 ; checkValueKind k4 (text "the body of a ForAllCo over covar:" <+> ppr co)
1734 -- See Note [Weird typing rule for ForAllTy] in Type
1735 ; in_scope <- getInScope
1736 ; let tyl = mkTyCoInvForAllTy cv1 t1
1737 r2 = coVarRole cv1
1738 kind_co' = downgradeRole r2 Nominal kind_co
1739 eta1 = mkNthCo r2 2 kind_co'
1740 eta2 = mkNthCo r2 3 kind_co'
1741 subst = mkCvSubst in_scope $
1742 -- We need both the free vars of the `t2` and the
1743 -- free vars of the range of the substitution in
1744 -- scope. All the free vars of `t2` and `kind_co` should
1745 -- already be in `in_scope`, because they've been
1746 -- linted and `cv2` has the same unique as `cv1`.
1747 -- See Note [The substitution invariant]
1748 unitVarEnv cv1 (eta1 `mkTransCo` (mkCoVarCo cv2)
1749 `mkTransCo` (mkSymCo eta2))
1750 tyr = mkTyCoInvForAllTy cv2 $
1751 substTy subst t2
1752 ; return (liftedTypeKind, liftedTypeKind, tyl, tyr, r) } }
1753 -- See Note [Weird typing rule for ForAllTy] in Type
1754
1755 lintCoercion co@(FunCo r co1 co2)
1756 = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
1757 ; (k2,k'2,s2,t2,r2) <- lintCoercion co2
1758 ; k <- lintArrow (text "coercion" <+> quotes (ppr co)) k1 k2
1759 ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2
1760 ; lintRole co1 r r1
1761 ; lintRole co2 r r2
1762 ; return (k, k', mkVisFunTy s1 s2, mkVisFunTy t1 t2, r) }
1763
1764 lintCoercion (CoVarCo cv)
1765 | not (isCoVar cv)
1766 = failWithL (hang (text "Bad CoVarCo:" <+> ppr cv)
1767 2 (text "With offending type:" <+> ppr (varType cv)))
1768 | otherwise
1769 = do { lintTyCoVarInScope cv
1770 ; cv' <- lookupIdInScope cv
1771 ; lintUnliftedCoVar cv
1772 ; return $ coVarKindsTypesRole cv' }
1773
1774 -- See Note [Bad unsafe coercion]
1775 lintCoercion co@(UnivCo prov r ty1 ty2)
1776 = do { k1 <- lintType ty1
1777 ; k2 <- lintType ty2
1778 ; case prov of
1779 UnsafeCoerceProv -> return () -- no extra checks
1780
1781 PhantomProv kco -> do { lintRole co Phantom r
1782 ; check_kinds kco k1 k2 }
1783
1784 ProofIrrelProv kco -> do { lintL (isCoercionTy ty1) $
1785 mkBadProofIrrelMsg ty1 co
1786 ; lintL (isCoercionTy ty2) $
1787 mkBadProofIrrelMsg ty2 co
1788 ; check_kinds kco k1 k2 }
1789
1790 PluginProv _ -> return () -- no extra checks
1791
1792 ; when (r /= Phantom && classifiesTypeWithValues k1
1793 && classifiesTypeWithValues k2)
1794 (checkTypes ty1 ty2)
1795 ; return (k1, k2, ty1, ty2, r) }
1796 where
1797 report s = hang (text $ "Unsafe coercion: " ++ s)
1798 2 (vcat [ text "From:" <+> ppr ty1
1799 , text " To:" <+> ppr ty2])
1800 isUnBoxed :: PrimRep -> Bool
1801 isUnBoxed = not . isGcPtrRep
1802
1803 -- see #9122 for discussion of these checks
1804 checkTypes t1 t2
1805 = do { checkWarnL (not lev_poly1)
1806 (report "left-hand type is levity-polymorphic")
1807 ; checkWarnL (not lev_poly2)
1808 (report "right-hand type is levity-polymorphic")
1809 ; when (not (lev_poly1 || lev_poly2)) $
1810 do { checkWarnL (reps1 `equalLength` reps2)
1811 (report "between values with different # of reps")
1812 ; zipWithM_ validateCoercion reps1 reps2 }}
1813 where
1814 lev_poly1 = isTypeLevPoly t1
1815 lev_poly2 = isTypeLevPoly t2
1816
1817 -- don't look at these unless lev_poly1/2 are False
1818 -- Otherwise, we get #13458
1819 reps1 = typePrimRep t1
1820 reps2 = typePrimRep t2
1821
1822 validateCoercion :: PrimRep -> PrimRep -> LintM ()
1823 validateCoercion rep1 rep2
1824 = do { dflags <- getDynFlags
1825 ; checkWarnL (isUnBoxed rep1 == isUnBoxed rep2)
1826 (report "between unboxed and boxed value")
1827 ; checkWarnL (TyCon.primRepSizeB dflags rep1
1828 == TyCon.primRepSizeB dflags rep2)
1829 (report "between unboxed values of different size")
1830 ; let fl = liftM2 (==) (TyCon.primRepIsFloat rep1)
1831 (TyCon.primRepIsFloat rep2)
1832 ; case fl of
1833 Nothing -> addWarnL (report "between vector types")
1834 Just False -> addWarnL (report "between float and integral values")
1835 _ -> return ()
1836 }
1837
1838 check_kinds kco k1 k2 = do { (k1', k2') <- lintStarCoercion kco
1839 ; ensureEqTys k1 k1' (mkBadUnivCoMsg CLeft co)
1840 ; ensureEqTys k2 k2' (mkBadUnivCoMsg CRight co) }
1841
1842
1843 lintCoercion (SymCo co)
1844 = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
1845 ; return (k2, k1, ty2, ty1, r) }
1846
1847 lintCoercion co@(TransCo co1 co2)
1848 = do { (k1a, _k1b, ty1a, ty1b, r1) <- lintCoercion co1
1849 ; (_k2a, k2b, ty2a, ty2b, r2) <- lintCoercion co2
1850 ; ensureEqTys ty1b ty2a
1851 (hang (text "Trans coercion mis-match:" <+> ppr co)
1852 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
1853 ; lintRole co r1 r2
1854 ; return (k1a, k2b, ty1a, ty2b, r1) }
1855
1856 lintCoercion the_co@(NthCo r0 n co)
1857 = do { (_, _, s, t, r) <- lintCoercion co
1858 ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
1859 { (Just (tcv_s, _ty_s), Just (tcv_t, _ty_t))
1860 -- works for both tyvar and covar
1861 | n == 0
1862 , (isForAllTy_ty s && isForAllTy_ty t)
1863 || (isForAllTy_co s && isForAllTy_co t)
1864 -> do { lintRole the_co Nominal r0
1865 ; return (ks, kt, ts, tt, r0) }
1866 where
1867 ts = varType tcv_s
1868 tt = varType tcv_t
1869 ks = typeKind ts
1870 kt = typeKind tt
1871
1872 ; _ -> case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
1873 { (Just (tc_s, tys_s), Just (tc_t, tys_t))
1874 | tc_s == tc_t
1875 , isInjectiveTyCon tc_s r
1876 -- see Note [NthCo and newtypes] in TyCoRep
1877 , tys_s `equalLength` tys_t
1878 , tys_s `lengthExceeds` n
1879 -> do { lintRole the_co tr r0
1880 ; return (ks, kt, ts, tt, r0) }
1881 where
1882 ts = getNth tys_s n
1883 tt = getNth tys_t n
1884 tr = nthRole r tc_s n
1885 ks = typeKind ts
1886 kt = typeKind tt
1887
1888 ; _ -> failWithL (hang (text "Bad getNth:")
1889 2 (ppr the_co $$ ppr s $$ ppr t)) }}}
1890
1891 lintCoercion the_co@(LRCo lr co)
1892 = do { (_,_,s,t,r) <- lintCoercion co
1893 ; lintRole co Nominal r
1894 ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
1895 (Just s_pr, Just t_pr)
1896 -> return (ks_pick, kt_pick, s_pick, t_pick, Nominal)
1897 where
1898 s_pick = pickLR lr s_pr
1899 t_pick = pickLR lr t_pr
1900 ks_pick = typeKind s_pick
1901 kt_pick = typeKind t_pick
1902
1903 _ -> failWithL (hang (text "Bad LRCo:")
1904 2 (ppr the_co $$ ppr s $$ ppr t)) }
1905
1906 lintCoercion (InstCo co arg)
1907 = do { (k3, k4, t1',t2', r) <- lintCoercion co
1908 ; (k1',k2',s1,s2, r') <- lintCoercion arg
1909 ; lintRole arg Nominal r'
1910 ; in_scope <- getInScope
1911 ; case (splitForAllTy_ty_maybe t1', splitForAllTy_ty_maybe t2') of
1912 -- forall over tvar
1913 { (Just (tv1,t1), Just (tv2,t2))
1914 | k1' `eqType` tyVarKind tv1
1915 , k2' `eqType` tyVarKind tv2
1916 -> return (k3, k4,
1917 substTyWithInScope in_scope [tv1] [s1] t1,
1918 substTyWithInScope in_scope [tv2] [s2] t2, r)
1919 | otherwise
1920 -> failWithL (text "Kind mis-match in inst coercion")
1921 ; _ -> case (splitForAllTy_co_maybe t1', splitForAllTy_co_maybe t2') of
1922 -- forall over covar
1923 { (Just (cv1, t1), Just (cv2, t2))
1924 | k1' `eqType` varType cv1
1925 , k2' `eqType` varType cv2
1926 , CoercionTy s1' <- s1
1927 , CoercionTy s2' <- s2
1928 -> do { return $
1929 (liftedTypeKind, liftedTypeKind
1930 -- See Note [Weird typing rule for ForAllTy] in Type
1931 , substTy (mkCvSubst in_scope $ unitVarEnv cv1 s1') t1
1932 , substTy (mkCvSubst in_scope $ unitVarEnv cv2 s2') t2
1933 , r) }
1934 | otherwise
1935 -> failWithL (text "Kind mis-match in inst coercion")
1936 ; _ -> failWithL (text "Bad argument of inst") }}}
1937
1938 lintCoercion co@(AxiomInstCo con ind cos)
1939 = do { unless (0 <= ind && ind < numBranches (coAxiomBranches con))
1940 (bad_ax (text "index out of range"))
1941 ; let CoAxBranch { cab_tvs = ktvs
1942 , cab_cvs = cvs
1943 , cab_roles = roles
1944 , cab_lhs = lhs
1945 , cab_rhs = rhs } = coAxiomNthBranch con ind
1946 ; unless (cos `equalLength` (ktvs ++ cvs)) $
1947 bad_ax (text "lengths")
1948 ; subst <- getTCvSubst
1949 ; let empty_subst = zapTCvSubst subst
1950 ; (subst_l, subst_r) <- foldlM check_ki
1951 (empty_subst, empty_subst)
1952 (zip3 (ktvs ++ cvs) roles cos)
1953 ; let lhs' = substTys subst_l lhs
1954 rhs' = substTy subst_r rhs
1955 fam_tc = coAxiomTyCon con
1956 ; case checkAxInstCo co of
1957 Just bad_branch -> bad_ax $ text "inconsistent with" <+>
1958 pprCoAxBranch fam_tc bad_branch
1959 Nothing -> return ()
1960 ; let s2 = mkTyConApp fam_tc lhs'
1961 ; return (typeKind s2, typeKind rhs', s2, rhs', coAxiomRole con) }
1962 where
1963 bad_ax what = addErrL (hang (text "Bad axiom application" <+> parens what)
1964 2 (ppr co))
1965
1966 check_ki (subst_l, subst_r) (ktv, role, arg)
1967 = do { (k', k'', s', t', r) <- lintCoercion arg
1968 ; lintRole arg role r
1969 ; let ktv_kind_l = substTy subst_l (tyVarKind ktv)
1970 ktv_kind_r = substTy subst_r (tyVarKind ktv)
1971 ; unless (k' `eqType` ktv_kind_l)
1972 (bad_ax (text "check_ki1" <+> vcat [ ppr co, ppr k', ppr ktv, ppr ktv_kind_l ] ))
1973 ; unless (k'' `eqType` ktv_kind_r)
1974 (bad_ax (text "check_ki2" <+> vcat [ ppr co, ppr k'', ppr ktv, ppr ktv_kind_r ] ))
1975 ; return (extendTCvSubst subst_l ktv s',
1976 extendTCvSubst subst_r ktv t') }
1977
1978 lintCoercion (KindCo co)
1979 = do { (k1, k2, _, _, _) <- lintCoercion co
1980 ; return (liftedTypeKind, liftedTypeKind, k1, k2, Nominal) }
1981
1982 lintCoercion (SubCo co')
1983 = do { (k1,k2,s,t,r) <- lintCoercion co'
1984 ; lintRole co' Nominal r
1985 ; return (k1,k2,s,t,Representational) }
1986
1987 lintCoercion this@(AxiomRuleCo co cs)
1988 = do { eqs <- mapM lintCoercion cs
1989 ; lintRoles 0 (coaxrAsmpRoles co) eqs
1990 ; case coaxrProves co [ Pair l r | (_,_,l,r,_) <- eqs ] of
1991 Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
1992 Just (Pair l r) ->
1993 return (typeKind l, typeKind r, l, r, coaxrRole co) }
1994 where
1995 err m xs = failWithL $
1996 hang (text m) 2 $ vcat (text "Rule:" <+> ppr (coaxrName co) : xs)
1997
1998 lintRoles n (e : es) ((_,_,_,_,r) : rs)
1999 | e == r = lintRoles (n+1) es rs
2000 | otherwise = err "Argument roles mismatch"
2001 [ text "In argument:" <+> int (n+1)
2002 , text "Expected:" <+> ppr e
2003 , text "Found:" <+> ppr r ]
2004 lintRoles _ [] [] = return ()
2005 lintRoles n [] rs = err "Too many coercion arguments"
2006 [ text "Expected:" <+> int n
2007 , text "Provided:" <+> int (n + length rs) ]
2008
2009 lintRoles n es [] = err "Not enough coercion arguments"
2010 [ text "Expected:" <+> int (n + length es)
2011 , text "Provided:" <+> int n ]
2012
2013 lintCoercion (HoleCo h)
2014 = do { addErrL $ text "Unfilled coercion hole:" <+> ppr h
2015 ; lintCoercion (CoVarCo (coHoleCoVar h)) }
2016
2017
2018 ----------
2019 lintUnliftedCoVar :: CoVar -> LintM ()
2020 lintUnliftedCoVar cv
2021 = when (not (isUnliftedType (coVarKind cv))) $
2022 failWithL (text "Bad lifted equality:" <+> ppr cv
2023 <+> dcolon <+> ppr (coVarKind cv))
2024
2025 {-
2026 ************************************************************************
2027 * *
2028 \subsection[lint-monad]{The Lint monad}
2029 * *
2030 ************************************************************************
2031 -}
2032
2033 -- If you edit this type, you may need to update the GHC formalism
2034 -- See Note [GHC Formalism]
2035 data LintEnv
2036 = LE { le_flags :: LintFlags -- Linting the result of this pass
2037 , le_loc :: [LintLocInfo] -- Locations
2038
2039 , le_subst :: TCvSubst -- Current type substitution
2040 -- We also use le_subst to keep track of
2041 -- /all variables/ in scope, both Ids and TyVars
2042
2043 , le_joins :: IdSet -- Join points in scope that are valid
2044 -- A subset of the InScopeSet in le_subst
2045 -- See Note [Join points]
2046
2047 , le_dynflags :: DynFlags -- DynamicFlags
2048 }
2049
2050 data LintFlags
2051 = LF { lf_check_global_ids :: Bool -- See Note [Checking for global Ids]
2052 , lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers]
2053 , lf_check_static_ptrs :: StaticPtrCheck -- ^ See Note [Checking StaticPtrs]
2054 , lf_report_unsat_syns :: Bool -- ^ See Note [Linting type synonym applications]
2055 }
2056
2057 -- See Note [Checking StaticPtrs]
2058 data StaticPtrCheck
2059 = AllowAnywhere
2060 -- ^ Allow 'makeStatic' to occur anywhere.
2061 | AllowAtTopLevel
2062 -- ^ Allow 'makeStatic' calls at the top-level only.
2063 | RejectEverywhere
2064 -- ^ Reject any 'makeStatic' occurrence.
2065 deriving Eq
2066
2067 defaultLintFlags :: LintFlags
2068 defaultLintFlags = LF { lf_check_global_ids = False
2069 , lf_check_inline_loop_breakers = True
2070 , lf_check_static_ptrs = AllowAnywhere
2071 , lf_report_unsat_syns = True
2072 }
2073
2074 newtype LintM a =
2075 LintM { unLintM ::
2076 LintEnv ->
2077 WarnsAndErrs -> -- Warning and error messages so far
2078 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
2079
2080 type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)
2081
2082 {- Note [Checking for global Ids]
2083 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2084 Before CoreTidy, all locally-bound Ids must be LocalIds, even
2085 top-level ones. See Note [Exported LocalIds] and #9857.
2086
2087 Note [Checking StaticPtrs]
2088 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2089 See Note [Grand plan for static forms] in StaticPtrTable for an overview.
2090
2091 Every occurrence of the function 'makeStatic' should be moved to the
2092 top level by the FloatOut pass. It's vital that we don't have nested
2093 'makeStatic' occurrences after CorePrep, because we populate the Static
2094 Pointer Table from the top-level bindings. See SimplCore Note [Grand
2095 plan for static forms].
2096
2097 The linter checks that no occurrence is left behind, nested within an
2098 expression. The check is enabled only after the FloatOut, CorePrep,
2099 and CoreTidy passes and only if the module uses the StaticPointers
2100 language extension. Checking more often doesn't help since the condition
2101 doesn't hold until after the first FloatOut pass.
2102
2103 Note [Type substitution]
2104 ~~~~~~~~~~~~~~~~~~~~~~~~
2105 Why do we need a type substitution? Consider
2106 /\(a:*). \(x:a). /\(a:*). id a x
2107 This is ill typed, because (renaming variables) it is really
2108 /\(a:*). \(x:a). /\(b:*). id b x
2109 Hence, when checking an application, we can't naively compare x's type
2110 (at its binding site) with its expected type (at a use site). So we
2111 rename type binders as we go, maintaining a substitution.
2112
2113 The same substitution also supports let-type, current expressed as
2114 (/\(a:*). body) ty
2115 Here we substitute 'ty' for 'a' in 'body', on the fly.
2116
2117 Note [Linting type synonym applications]
2118 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2119 When linting a type-synonym, or type-family, application
2120 S ty1 .. tyn
2121 we behave as follows (#15057, #T15664):
2122
2123 * If lf_report_unsat_syns = True, and S has arity < n,
2124 complain about an unsaturated type synonym or type family
2125
2126 * Switch off lf_report_unsat_syns, and lint ty1 .. tyn.
2127
2128 Reason: catch out of scope variables or other ill-kinded gubbins,
2129 even if S discards that argument entirely. E.g. (#15012):
2130 type FakeOut a = Int
2131 type family TF a
2132 type instance TF Int = FakeOut a
2133 Here 'a' is out of scope; but if we expand FakeOut, we conceal
2134 that out-of-scope error.
2135
2136 Reason for switching off lf_report_unsat_syns: with
2137 LiberalTypeSynonyms, GHC allows unsaturated synonyms provided they
2138 are saturated when the type is expanded. Example
2139 type T f = f Int
2140 type S a = a -> a
2141 type Z = T S
2142 In Z's RHS, S appears unsaturated, but it is saturated when T is expanded.
2143
2144 * If lf_report_unsat_syns is on, expand the synonym application and
2145 lint the result. Reason: want to check that synonyms are saturated
2146 when the type is expanded.
2147 -}
2148
2149 instance Functor LintM where
2150 fmap = liftM
2151
2152 instance Applicative LintM where
2153 pure x = LintM $ \ _ errs -> (Just x, errs)
2154 (<*>) = ap
2155
2156 instance Monad LintM where
2157 #if !MIN_VERSION_base(4,13,0)
2158 fail = MonadFail.fail
2159 #endif
2160 m >>= k = LintM (\ env errs ->
2161 let (res, errs') = unLintM m env errs in
2162 case res of
2163 Just r -> unLintM (k r) env errs'
2164 Nothing -> (Nothing, errs'))
2165
2166 instance MonadFail.MonadFail LintM where
2167 fail err = failWithL (text err)
2168
2169 instance HasDynFlags LintM where
2170 getDynFlags = LintM (\ e errs -> (Just (le_dynflags e), errs))
2171
2172 data LintLocInfo
2173 = RhsOf Id -- The variable bound
2174 | LambdaBodyOf Id -- The lambda-binder
2175 | UnfoldingOf Id -- Unfolding of a binder
2176 | BodyOfLetRec [Id] -- One of the binders
2177 | CaseAlt CoreAlt -- Case alternative
2178 | CasePat CoreAlt -- The *pattern* of the case alternative
2179 | AnExpr CoreExpr -- Some expression
2180 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
2181 | TopLevelBindings
2182 | InType Type -- Inside a type
2183 | InCo Coercion -- Inside a coercion
2184
2185 initL :: DynFlags -> LintFlags -> InScopeSet
2186 -> LintM a -> WarnsAndErrs -- Warnings and errors
2187 initL dflags flags in_scope m
2188 = case unLintM m env (emptyBag, emptyBag) of
2189 (Just _, errs) -> errs
2190 (Nothing, errs@(_, e)) | not (isEmptyBag e) -> errs
2191 | otherwise -> pprPanic ("Bug in Lint: a failure occurred " ++
2192 "without reporting an error message") empty
2193 where
2194 env = LE { le_flags = flags
2195 , le_subst = mkEmptyTCvSubst in_scope
2196 , le_joins = emptyVarSet
2197 , le_loc = []
2198 , le_dynflags = dflags }
2199
2200 setReportUnsat :: Bool -> LintM a -> LintM a
2201 -- Switch off lf_report_unsat_syns
2202 setReportUnsat ru thing_inside
2203 = LintM $ \ env errs ->
2204 let env' = env { le_flags = (le_flags env) { lf_report_unsat_syns = ru } }
2205 in unLintM thing_inside env' errs
2206
2207 getLintFlags :: LintM LintFlags
2208 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
2209
2210 checkL :: Bool -> MsgDoc -> LintM ()
2211 checkL True _ = return ()
2212 checkL False msg = failWithL msg
2213
2214 -- like checkL, but relevant to type checking
2215 lintL :: Bool -> MsgDoc -> LintM ()
2216 lintL = checkL
2217
2218 checkWarnL :: Bool -> MsgDoc -> LintM ()
2219 checkWarnL True _ = return ()
2220 checkWarnL False msg = addWarnL msg
2221
2222 failWithL :: MsgDoc -> LintM a
2223 failWithL msg = LintM $ \ env (warns,errs) ->
2224 (Nothing, (warns, addMsg env errs msg))
2225
2226 addErrL :: MsgDoc -> LintM ()
2227 addErrL msg = LintM $ \ env (warns,errs) ->
2228 (Just (), (warns, addMsg env errs msg))
2229
2230 addWarnL :: MsgDoc -> LintM ()
2231 addWarnL msg = LintM $ \ env (warns,errs) ->
2232 (Just (), (addMsg env warns msg, errs))
2233
2234 addMsg :: LintEnv -> Bag MsgDoc -> MsgDoc -> Bag MsgDoc
2235 addMsg env msgs msg
2236 = ASSERT( notNull locs )
2237 msgs `snocBag` mk_msg msg
2238 where
2239 locs = le_loc env
2240 (loc, cxt1) = dumpLoc (head locs)
2241 cxts = [snd (dumpLoc loc) | loc <- locs]
2242 context = ifPprDebug (vcat (reverse cxts) $$ cxt1 $$
2243 text "Substitution:" <+> ppr (le_subst env))
2244 cxt1
2245
2246 mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
2247
2248 addLoc :: LintLocInfo -> LintM a -> LintM a
2249 addLoc extra_loc m
2250 = LintM $ \ env errs ->
2251 unLintM m (env { le_loc = extra_loc : le_loc env }) errs
2252
2253 inCasePat :: LintM Bool -- A slight hack; see the unique call site
2254 inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
2255 where
2256 is_case_pat (LE { le_loc = CasePat {} : _ }) = True
2257 is_case_pat _other = False
2258
2259 addInScopeVar :: Var -> LintM a -> LintM a
2260 addInScopeVar var m
2261 = LintM $ \ env errs ->
2262 unLintM m (env { le_subst = extendTCvInScope (le_subst env) var
2263 , le_joins = delVarSet (le_joins env) var
2264 }) errs
2265
2266 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
2267 extendSubstL tv ty m
2268 = LintM $ \ env errs ->
2269 unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
2270
2271 updateTCvSubst :: TCvSubst -> LintM a -> LintM a
2272 updateTCvSubst subst' m
2273 = LintM $ \ env errs -> unLintM m (env { le_subst = subst' }) errs
2274
2275 markAllJoinsBad :: LintM a -> LintM a
2276 markAllJoinsBad m
2277 = LintM $ \ env errs -> unLintM m (env { le_joins = emptyVarSet }) errs
2278
2279 markAllJoinsBadIf :: Bool -> LintM a -> LintM a
2280 markAllJoinsBadIf True m = markAllJoinsBad m
2281 markAllJoinsBadIf False m = m
2282
2283 addGoodJoins :: [Var] -> LintM a -> LintM a
2284 addGoodJoins vars thing_inside
2285 | null join_ids
2286 = thing_inside
2287 | otherwise
2288 = LintM $ \ env errs -> unLintM thing_inside (add_joins env) errs
2289 where
2290 add_joins env = env { le_joins = le_joins env `extendVarSetList` join_ids }
2291 join_ids = filter isJoinId vars
2292
2293 getValidJoins :: LintM IdSet
2294 getValidJoins = LintM (\ env errs -> (Just (le_joins env), errs))
2295
2296 getTCvSubst :: LintM TCvSubst
2297 getTCvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
2298
2299 getInScope :: LintM InScopeSet
2300 getInScope = LintM (\ env errs -> (Just (getTCvInScope $ le_subst env), errs))
2301
2302 applySubstTy :: InType -> LintM OutType
2303 applySubstTy ty = do { subst <- getTCvSubst; return (substTy subst ty) }
2304
2305 applySubstCo :: InCoercion -> LintM OutCoercion
2306 applySubstCo co = do { subst <- getTCvSubst; return (substCo subst co) }
2307
2308 lookupIdInScope :: Id -> LintM Id
2309 lookupIdInScope id_occ
2310 = do { subst <- getTCvSubst
2311 ; case lookupInScope (getTCvInScope subst) id_occ of
2312 Just id_bnd -> do { checkL (not (bad_global id_bnd)) global_in_scope
2313 ; return id_bnd }
2314 Nothing -> do { checkL (not is_local) local_out_of_scope
2315 ; return id_occ } }
2316 where
2317 is_local = mustHaveLocalBinding id_occ
2318 local_out_of_scope = text "Out of scope:" <+> pprBndr LetBind id_occ
2319 global_in_scope = hang (text "Occurrence is GlobalId, but binding is LocalId")
2320 2 (pprBndr LetBind id_occ)
2321 bad_global id_bnd = isGlobalId id_occ
2322 && isLocalId id_bnd
2323 && not (isWiredInName (idName id_occ))
2324 -- 'bad_global' checks for the case where an /occurrence/ is
2325 -- a GlobalId, but there is an enclosing binding fora a LocalId.
2326 -- NB: the in-scope variables are mostly LocalIds, checked by lintIdBndr,
2327 -- but GHCi adds GlobalIds from the interactive context. These
2328 -- are fine; hence the test (isLocalId id == isLocalId v)
2329 -- NB: when compiling Control.Exception.Base, things like absentError
2330 -- are defined locally, but appear in expressions as (global)
2331 -- wired-in Ids after worker/wrapper
2332 -- So we simply disable the test in this case
2333
2334 lookupJoinId :: Id -> LintM (Maybe JoinArity)
2335 -- Look up an Id which should be a join point, valid here
2336 -- If so, return its arity, if not return Nothing
2337 lookupJoinId id
2338 = do { join_set <- getValidJoins
2339 ; case lookupVarSet join_set id of
2340 Just id' -> return (isJoinId_maybe id')
2341 Nothing -> return Nothing }
2342
2343 lintTyCoVarInScope :: TyCoVar -> LintM ()
2344 lintTyCoVarInScope var
2345 = do { subst <- getTCvSubst
2346 ; lintL (var `isInScope` subst)
2347 (pprBndr LetBind var <+> text "is out of scope") }
2348
2349 ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
2350 -- check ty2 is subtype of ty1 (ie, has same structure but usage
2351 -- annotations need only be consistent, not equal)
2352 -- Assumes ty1,ty2 are have already had the substitution applied
2353 ensureEqTys ty1 ty2 msg = lintL (ty1 `eqType` ty2) msg
2354
2355 lintRole :: Outputable thing
2356 => thing -- where the role appeared
2357 -> Role -- expected
2358 -> Role -- actual
2359 -> LintM ()
2360 lintRole co r1 r2
2361 = lintL (r1 == r2)
2362 (text "Role incompatibility: expected" <+> ppr r1 <> comma <+>
2363 text "got" <+> ppr r2 $$
2364 text "in" <+> ppr co)
2365
2366 {-
2367 ************************************************************************
2368 * *
2369 \subsection{Error messages}
2370 * *
2371 ************************************************************************
2372 -}
2373
2374 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
2375
2376 dumpLoc (RhsOf v)
2377 = (getSrcLoc v, brackets (text "RHS of" <+> pp_binders [v]))
2378
2379 dumpLoc (LambdaBodyOf b)
2380 = (getSrcLoc b, brackets (text "in body of lambda with binder" <+> pp_binder b))
2381
2382 dumpLoc (UnfoldingOf b)
2383 = (getSrcLoc b, brackets (text "in the unfolding of" <+> pp_binder b))
2384
2385 dumpLoc (BodyOfLetRec [])
2386 = (noSrcLoc, brackets (text "In body of a letrec with no binders"))
2387
2388 dumpLoc (BodyOfLetRec bs@(_:_))
2389 = ( getSrcLoc (head bs), brackets (text "in body of letrec with binders" <+> pp_binders bs))
2390
2391 dumpLoc (AnExpr e)
2392 = (noSrcLoc, text "In the expression:" <+> ppr e)
2393
2394 dumpLoc (CaseAlt (con, args, _))
2395 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
2396
2397 dumpLoc (CasePat (con, args, _))
2398 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
2399
2400 dumpLoc (ImportedUnfolding locn)
2401 = (locn, brackets (text "in an imported unfolding"))
2402 dumpLoc TopLevelBindings
2403 = (noSrcLoc, Outputable.empty)
2404 dumpLoc (InType ty)
2405 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
2406 dumpLoc (InCo co)
2407 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
2408
2409 pp_binders :: [Var] -> SDoc
2410 pp_binders bs = sep (punctuate comma (map pp_binder bs))
2411
2412 pp_binder :: Var -> SDoc
2413 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
2414 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
2415
2416 ------------------------------------------------------
2417 -- Messages for case expressions
2418
2419 mkDefaultArgsMsg :: [Var] -> MsgDoc
2420 mkDefaultArgsMsg args
2421 = hang (text "DEFAULT case with binders")
2422 4 (ppr args)
2423
2424 mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
2425 mkCaseAltMsg e ty1 ty2
2426 = hang (text "Type of case alternatives not the same as the annotation on case:")
2427 4 (vcat [ text "Actual type:" <+> ppr ty1,
2428 text "Annotation on case:" <+> ppr ty2,
2429 text "Alt Rhs:" <+> ppr e ])
2430
2431 mkScrutMsg :: Id -> Type -> Type -> TCvSubst -> MsgDoc
2432 mkScrutMsg var var_ty scrut_ty subst
2433 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
2434 text "Result binder type:" <+> ppr var_ty,--(idType var),
2435 text "Scrutinee type:" <+> ppr scrut_ty,
2436 hsep [text "Current TCv subst", ppr subst]]
2437
2438 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
2439 mkNonDefltMsg e
2440 = hang (text "Case expression with DEFAULT not at the beginning") 4 (ppr e)
2441 mkNonIncreasingAltsMsg e
2442 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
2443
2444 nonExhaustiveAltsMsg :: CoreExpr -> MsgDoc
2445 nonExhaustiveAltsMsg e
2446 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
2447
2448 mkBadConMsg :: TyCon -> DataCon -> MsgDoc
2449 mkBadConMsg tycon datacon
2450 = vcat [
2451 text "In a case alternative, data constructor isn't in scrutinee type:",
2452 text "Scrutinee type constructor:" <+> ppr tycon,
2453 text "Data con:" <+> ppr datacon
2454 ]
2455
2456 mkBadPatMsg :: Type -> Type -> MsgDoc
2457 mkBadPatMsg con_result_ty scrut_ty
2458 = vcat [
2459 text "In a case alternative, pattern result type doesn't match scrutinee type:",
2460 text "Pattern result type:" <+> ppr con_result_ty,
2461 text "Scrutinee type:" <+> ppr scrut_ty
2462 ]
2463
2464 integerScrutinisedMsg :: MsgDoc
2465 integerScrutinisedMsg
2466 = text "In a LitAlt, the literal is lifted (probably Integer)"
2467
2468 mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
2469 mkBadAltMsg scrut_ty alt
2470 = vcat [ text "Data alternative when scrutinee is not a tycon application",
2471 text "Scrutinee type:" <+> ppr scrut_ty,
2472 text "Alternative:" <+> pprCoreAlt alt ]
2473
2474 mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc
2475 mkNewTyDataConAltMsg scrut_ty alt
2476 = vcat [ text "Data alternative for newtype datacon",
2477 text "Scrutinee type:" <+> ppr scrut_ty,
2478 text "Alternative:" <+> pprCoreAlt alt ]
2479
2480
2481 ------------------------------------------------------
2482 -- Other error messages
2483
2484 mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
2485 mkAppMsg fun_ty arg_ty arg
2486 = vcat [text "Argument value doesn't match argument type:",
2487 hang (text "Fun type:") 4 (ppr fun_ty),
2488 hang (text "Arg type:") 4 (ppr arg_ty),
2489 hang (text "Arg:") 4 (ppr arg)]
2490
2491 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
2492 mkNonFunAppMsg fun_ty arg_ty arg
2493 = vcat [text "Non-function type in function position",
2494 hang (text "Fun type:") 4 (ppr fun_ty),
2495 hang (text "Arg type:") 4 (ppr arg_ty),
2496 hang (text "Arg:") 4 (ppr arg)]
2497
2498 mkLetErr :: TyVar -> CoreExpr -> MsgDoc
2499 mkLetErr bndr rhs
2500 = vcat [text "Bad `let' binding:",
2501 hang (text "Variable:")
2502 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
2503 hang (text "Rhs:")
2504 4 (ppr rhs)]
2505
2506 mkTyAppMsg :: Type -> Type -> MsgDoc
2507 mkTyAppMsg ty arg_ty
2508 = vcat [text "Illegal type application:",
2509 hang (text "Exp type:")
2510 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
2511 hang (text "Arg type:")
2512 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
2513
2514 emptyRec :: CoreExpr -> MsgDoc
2515 emptyRec e = hang (text "Empty Rec binding:") 2 (ppr e)
2516
2517 mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc
2518 mkRhsMsg binder what ty
2519 = vcat
2520 [hsep [text "The type of this binder doesn't match the type of its" <+> what <> colon,
2521 ppr binder],
2522 hsep [text "Binder's type:", ppr (idType binder)],
2523 hsep [text "Rhs type:", ppr ty]]
2524
2525 mkLetAppMsg :: CoreExpr -> MsgDoc
2526 mkLetAppMsg e
2527 = hang (text "This argument does not satisfy the let/app invariant:")
2528 2 (ppr e)
2529
2530 badBndrTyMsg :: Id -> SDoc -> MsgDoc
2531 badBndrTyMsg binder what
2532 = vcat [ text "The type of this binder is" <+> what <> colon <+> ppr binder
2533 , text "Binder's type:" <+> ppr (idType binder) ]
2534
2535 mkStrictMsg :: Id -> MsgDoc
2536 mkStrictMsg binder
2537 = vcat [hsep [text "Recursive or top-level binder has strict demand info:",
2538 ppr binder],
2539 hsep [text "Binder's demand info:", ppr (idDemandInfo binder)]
2540 ]
2541
2542 mkNonTopExportedMsg :: Id -> MsgDoc
2543 mkNonTopExportedMsg binder
2544 = hsep [text "Non-top-level binder is marked as exported:", ppr binder]
2545
2546 mkNonTopExternalNameMsg :: Id -> MsgDoc
2547 mkNonTopExternalNameMsg binder
2548 = hsep [text "Non-top-level binder has an external name:", ppr binder]
2549
2550 mkTopNonLitStrMsg :: Id -> MsgDoc
2551 mkTopNonLitStrMsg binder
2552 = hsep [text "Top-level Addr# binder has a non-literal rhs:", ppr binder]
2553
2554 mkKindErrMsg :: TyVar -> Type -> MsgDoc
2555 mkKindErrMsg tyvar arg_ty
2556 = vcat [text "Kinds don't match in type application:",
2557 hang (text "Type variable:")
2558 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
2559 hang (text "Arg type:")
2560 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
2561
2562 mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> MsgDoc
2563 mkCastErr expr = mk_cast_err "expression" "type" (ppr expr)
2564
2565 mkCastTyErr :: Type -> Coercion -> Kind -> Kind -> MsgDoc
2566 mkCastTyErr ty = mk_cast_err "type" "kind" (ppr ty)
2567
2568 mk_cast_err :: String -- ^ What sort of casted thing this is
2569 -- (\"expression\" or \"type\").
2570 -> String -- ^ What sort of coercion is being used
2571 -- (\"type\" or \"kind\").
2572 -> SDoc -- ^ The thing being casted.
2573 -> Coercion -> Type -> Type -> MsgDoc
2574 mk_cast_err thing_str co_str pp_thing co from_ty thing_ty
2575 = vcat [from_msg <+> text "of Cast differs from" <+> co_msg
2576 <+> text "of" <+> enclosed_msg,
2577 from_msg <> colon <+> ppr from_ty,
2578 text (capitalise co_str) <+> text "of" <+> enclosed_msg <> colon
2579 <+> ppr thing_ty,
2580 text "Actual" <+> enclosed_msg <> colon <+> pp_thing,
2581 text "Coercion used in cast:" <+> ppr co
2582 ]
2583 where
2584 co_msg, from_msg, enclosed_msg :: SDoc
2585 co_msg = text co_str
2586 from_msg = text "From-" <> co_msg
2587 enclosed_msg = text "enclosed" <+> text thing_str
2588
2589 mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc
2590 mkBadUnivCoMsg lr co
2591 = text "Kind mismatch on the" <+> pprLeftOrRight lr <+>
2592 text "side of a UnivCo:" <+> ppr co
2593
2594 mkBadProofIrrelMsg :: Type -> Coercion -> SDoc
2595 mkBadProofIrrelMsg ty co
2596 = hang (text "Found a non-coercion in a proof-irrelevance UnivCo:")
2597 2 (vcat [ text "type:" <+> ppr ty
2598 , text "co:" <+> ppr co ])
2599
2600 mkBadTyVarMsg :: Var -> SDoc
2601 mkBadTyVarMsg tv
2602 = text "Non-tyvar used in TyVarTy:"
2603 <+> ppr tv <+> dcolon <+> ppr (varType tv)
2604
2605 mkBadJoinBindMsg :: Var -> SDoc
2606 mkBadJoinBindMsg var
2607 = vcat [ text "Bad join point binding:" <+> ppr var
2608 , text "Join points can be bound only by a non-top-level let" ]
2609
2610 mkInvalidJoinPointMsg :: Var -> Type -> SDoc
2611 mkInvalidJoinPointMsg var ty
2612 = hang (text "Join point has invalid type:")
2613 2 (ppr var <+> dcolon <+> ppr ty)
2614
2615 mkBadJoinArityMsg :: Var -> Int -> Int -> CoreExpr -> SDoc
2616 mkBadJoinArityMsg var ar nlams rhs
2617 = vcat [ text "Join point has too few lambdas",
2618 text "Join var:" <+> ppr var,
2619 text "Join arity:" <+> ppr ar,
2620 text "Number of lambdas:" <+> ppr nlams,
2621 text "Rhs = " <+> ppr rhs
2622 ]
2623
2624 invalidJoinOcc :: Var -> SDoc
2625 invalidJoinOcc var
2626 = vcat [ text "Invalid occurrence of a join variable:" <+> ppr var
2627 , text "The binder is either not a join point, or not valid here" ]
2628
2629 mkBadJumpMsg :: Var -> Int -> Int -> SDoc
2630 mkBadJumpMsg var ar nargs
2631 = vcat [ text "Join point invoked with wrong number of arguments",
2632 text "Join var:" <+> ppr var,
2633 text "Join arity:" <+> ppr ar,
2634 text "Number of arguments:" <+> int nargs ]
2635
2636 mkInconsistentRecMsg :: [Var] -> SDoc
2637 mkInconsistentRecMsg bndrs
2638 = vcat [ text "Recursive let binders mix values and join points",
2639 text "Binders:" <+> hsep (map ppr_with_details bndrs) ]
2640 where
2641 ppr_with_details bndr = ppr bndr <> ppr (idDetails bndr)
2642
2643 mkJoinBndrOccMismatchMsg :: Var -> JoinArity -> JoinArity -> SDoc
2644 mkJoinBndrOccMismatchMsg bndr join_arity_bndr join_arity_occ
2645 = vcat [ text "Mismatch in join point arity between binder and occurrence"
2646 , text "Var:" <+> ppr bndr
2647 , text "Arity at binding site:" <+> ppr join_arity_bndr
2648 , text "Arity at occurrence: " <+> ppr join_arity_occ ]
2649
2650 mkBndrOccTypeMismatchMsg :: Var -> Var -> OutType -> OutType -> SDoc
2651 mkBndrOccTypeMismatchMsg bndr var bndr_ty var_ty
2652 = vcat [ text "Mismatch in type between binder and occurrence"
2653 , text "Var:" <+> ppr bndr
2654 , text "Binder type:" <+> ppr bndr_ty
2655 , text "Occurrence type:" <+> ppr var_ty
2656 , text " Before subst:" <+> ppr (idType var) ]
2657
2658 mkBadJoinPointRuleMsg :: JoinId -> JoinArity -> CoreRule -> SDoc
2659 mkBadJoinPointRuleMsg bndr join_arity rule
2660 = vcat [ text "Join point has rule with wrong number of arguments"
2661 , text "Var:" <+> ppr bndr
2662 , text "Join arity:" <+> ppr join_arity
2663 , text "Rule:" <+> ppr rule ]
2664
2665 pprLeftOrRight :: LeftOrRight -> MsgDoc
2666 pprLeftOrRight CLeft = text "left"
2667 pprLeftOrRight CRight = text "right"
2668
2669 dupVars :: [NonEmpty Var] -> MsgDoc
2670 dupVars vars
2671 = hang (text "Duplicate variables brought into scope")
2672 2 (ppr (map toList vars))
2673
2674 dupExtVars :: [NonEmpty Name] -> MsgDoc
2675 dupExtVars vars
2676 = hang (text "Duplicate top-level variables with the same qualified name")
2677 2 (ppr (map toList vars))
2678
2679 {-
2680 ************************************************************************
2681 * *
2682 \subsection{Annotation Linting}
2683 * *
2684 ************************************************************************
2685 -}
2686
2687 -- | This checks whether a pass correctly looks through debug
2688 -- annotations (@SourceNote@). This works a bit different from other
2689 -- consistency checks: We check this by running the given task twice,
2690 -- noting all differences between the results.
2691 lintAnnots :: SDoc -> (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
2692 lintAnnots pname pass guts = do
2693 -- Run the pass as we normally would
2694 dflags <- getDynFlags
2695 when (gopt Opt_DoAnnotationLinting dflags) $
2696 liftIO $ Err.showPass dflags "Annotation linting - first run"
2697 nguts <- pass guts
2698 -- If appropriate re-run it without debug annotations to make sure
2699 -- that they made no difference.
2700 when (gopt Opt_DoAnnotationLinting dflags) $ do
2701 liftIO $ Err.showPass dflags "Annotation linting - second run"
2702 nguts' <- withoutAnnots pass guts
2703 -- Finally compare the resulting bindings
2704 liftIO $ Err.showPass dflags "Annotation linting - comparison"
2705 let binds = flattenBinds $ mg_binds nguts
2706 binds' = flattenBinds $ mg_binds nguts'
2707 (diffs,_) = diffBinds True (mkRnEnv2 emptyInScopeSet) binds binds'
2708 when (not (null diffs)) $ CoreMonad.putMsg $ vcat
2709 [ lint_banner "warning" pname
2710 , text "Core changes with annotations:"
2711 , withPprStyle (defaultDumpStyle dflags) $ nest 2 $ vcat diffs
2712 ]
2713 -- Return actual new guts
2714 return nguts
2715
2716 -- | Run the given pass without annotations. This means that we both
2717 -- set the debugLevel setting to 0 in the environment as well as all
2718 -- annotations from incoming modules.
2719 withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
2720 withoutAnnots pass guts = do
2721 -- Remove debug flag from environment.
2722 dflags <- getDynFlags
2723 let removeFlag env = env{ hsc_dflags = dflags{ debugLevel = 0} }
2724 withoutFlag corem =
2725 liftIO =<< runCoreM <$> fmap removeFlag getHscEnv <*> getRuleBase <*>
2726 getUniqueSupplyM <*> getModule <*>
2727 getVisibleOrphanMods <*>
2728 getPrintUnqualified <*> getSrcSpanM <*>
2729 pure corem
2730 -- Nuke existing ticks in module.
2731 -- TODO: Ticks in unfoldings. Maybe change unfolding so it removes
2732 -- them in absence of debugLevel > 0.
2733 let nukeTicks = stripTicksE (not . tickishIsCode)
2734 nukeAnnotsBind :: CoreBind -> CoreBind
2735 nukeAnnotsBind bind = case bind of
2736 Rec bs -> Rec $ map (\(b,e) -> (b, nukeTicks e)) bs
2737 NonRec b e -> NonRec b $ nukeTicks e
2738 nukeAnnotsMod mg@ModGuts{mg_binds=binds}
2739 = mg{mg_binds = map nukeAnnotsBind binds}
2740 -- Perform pass with all changes applied
2741 fmap fst $ withoutFlag $ pass (nukeAnnotsMod guts)