never executed always true always false
1 {-# LANGUAGE DeriveFunctor #-}
2 {-# LANGUAGE MultiWayIf #-}
3 {-# LANGUAGE ScopedTypeVariables #-}
4
5 {-
6 (c) The University of Glasgow 2006
7 (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
8
9
10 A ``lint'' pass to check for Core correctness.
11 See Note [Core Lint guarantee].
12 -}
13
14 module GHC.Core.Lint (
15 lintCoreBindings, lintUnfolding,
16 lintPassResult, lintInteractiveExpr, lintExpr,
17 lintAnnots, lintAxioms,
18
19 interactiveInScope,
20
21 -- ** Debug output
22 endPass, endPassIO,
23 displayLintResults, dumpPassResult
24 ) where
25
26 import GHC.Prelude
27
28 import GHC.Driver.Session
29 import GHC.Driver.Ppr
30 import GHC.Driver.Env
31 import GHC.Driver.Config.Diagnostic
32
33 import GHC.Tc.Utils.TcType ( isFloatingTy, isTyFamFree )
34 import GHC.Unit.Module.ModGuts
35 import GHC.Runtime.Context
36
37 import GHC.Core
38 import GHC.Core.FVs
39 import GHC.Core.Utils
40 import GHC.Core.Stats ( coreBindsStats )
41 import GHC.Core.Opt.Monad
42 import GHC.Core.DataCon
43 import GHC.Core.Ppr
44 import GHC.Core.Coercion
45 import GHC.Core.Type as Type
46 import GHC.Core.Multiplicity
47 import GHC.Core.UsageEnv
48 import GHC.Core.TyCo.Rep -- checks validity of types/coercions
49 import GHC.Core.TyCo.Subst
50 import GHC.Core.TyCo.FVs
51 import GHC.Core.TyCo.Ppr ( pprTyVar, pprTyVars )
52 import GHC.Core.TyCon as TyCon
53 import GHC.Core.Coercion.Axiom
54 import GHC.Core.Unify
55 import GHC.Core.InstEnv ( instanceDFunId )
56 import GHC.Core.Coercion.Opt ( checkAxInstCo )
57 import GHC.Core.Opt.Arity ( typeArity )
58
59 import GHC.Types.Literal
60 import GHC.Types.Var as Var
61 import GHC.Types.Var.Env
62 import GHC.Types.Var.Set
63 import GHC.Types.Unique.Set( nonDetEltsUniqSet )
64 import GHC.Types.Name
65 import GHC.Types.Name.Env
66 import GHC.Types.Id
67 import GHC.Types.Id.Info
68 import GHC.Types.SrcLoc
69 import GHC.Types.Tickish
70 import GHC.Types.RepType
71 import GHC.Types.Basic
72 import GHC.Types.Demand ( splitDmdSig, isDeadEndDiv )
73 import GHC.Types.TypeEnv
74
75 import GHC.Builtin.Names
76 import GHC.Builtin.Types.Prim
77 import GHC.Builtin.Types ( multiplicityTy )
78
79 import GHC.Data.Bag
80 import GHC.Data.List.SetOps
81
82 import GHC.Utils.Monad
83 import GHC.Utils.Outputable as Outputable
84 import GHC.Utils.Panic
85 import GHC.Utils.Constants (debugIsOn)
86 import GHC.Utils.Misc
87 import GHC.Utils.Trace
88 import GHC.Utils.Error
89 import qualified GHC.Utils.Error as Err
90 import GHC.Utils.Logger
91
92 import Control.Monad
93 import Data.Foldable ( toList )
94 import Data.List.NonEmpty ( NonEmpty(..), groupWith )
95 import Data.List ( partition )
96 import Data.Maybe
97 import GHC.Data.Pair
98 import qualified GHC.LanguageExtensions as LangExt
99
100 {-
101 Note [Core Lint guarantee]
102 ~~~~~~~~~~~~~~~~~~~~~~~~~~
103 Core Lint is the type-checker for Core. Using it, we get the following guarantee:
104
105 If all of:
106 1. Core Lint passes,
107 2. there are no unsafe coercions (i.e. unsafeEqualityProof),
108 3. all plugin-supplied coercions (i.e. PluginProv) are valid, and
109 4. all case-matches are complete
110 then running the compiled program will not seg-fault, assuming no bugs downstream
111 (e.g. in the code generator). This guarantee is quite powerful, in that it allows us
112 to decouple the safety of the resulting program from the type inference algorithm.
113
114 However, do note point (4) above. Core Lint does not check for incomplete case-matches;
115 see Note [Case expression invariants] in GHC.Core, invariant (4). As explained there,
116 an incomplete case-match might slip by Core Lint and cause trouble at runtime.
117
118 Note [GHC Formalism]
119 ~~~~~~~~~~~~~~~~~~~~
120 This file implements the type-checking algorithm for System FC, the "official"
121 name of the Core language. Type safety of FC is heart of the claim that
122 executables produced by GHC do not have segmentation faults. Thus, it is
123 useful to be able to reason about System FC independently of reading the code.
124 To this purpose, there is a document core-spec.pdf built in docs/core-spec that
125 contains a formalism of the types and functions dealt with here. If you change
126 just about anything in this file or you change other types/functions throughout
127 the Core language (all signposted to this note), you should update that
128 formalism. See docs/core-spec/README for more info about how to do so.
129
130 Note [check vs lint]
131 ~~~~~~~~~~~~~~~~~~~~
132 This file implements both a type checking algorithm and also general sanity
133 checking. For example, the "sanity checking" checks for TyConApp on the left
134 of an AppTy, which should never happen. These sanity checks don't really
135 affect any notion of type soundness. Yet, it is convenient to do the sanity
136 checks at the same time as the type checks. So, we use the following naming
137 convention:
138
139 - Functions that begin with 'lint'... are involved in type checking. These
140 functions might also do some sanity checking.
141
142 - Functions that begin with 'check'... are *not* involved in type checking.
143 They exist only for sanity checking.
144
145 Issues surrounding variable naming, shadowing, and such are considered *not*
146 to be part of type checking, as the formalism omits these details.
147
148 Summary of checks
149 ~~~~~~~~~~~~~~~~~
150 Checks that a set of core bindings is well-formed. The PprStyle and String
151 just control what we print in the event of an error. The Bool value
152 indicates whether we have done any specialisation yet (in which case we do
153 some extra checks).
154
155 We check for
156 (a) type errors
157 (b) Out-of-scope type variables
158 (c) Out-of-scope local variables
159 (d) Ill-kinded types
160 (e) Incorrect unsafe coercions
161
162 If we have done specialisation the we check that there are
163 (a) No top-level bindings of primitive (unboxed type)
164
165 Note [Linting function types]
166 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
167 As described in Note [Representation of function types], all saturated
168 applications of funTyCon are represented with the FunTy constructor. We check
169 this invariant in lintType.
170
171 Note [Linting type lets]
172 ~~~~~~~~~~~~~~~~~~~~~~~~
173 In the desugarer, it's very very convenient to be able to say (in effect)
174 let a = Type Bool in
175 let x::a = True in <body>
176 That is, use a type let. See Note [Core type and coercion invariant] in "GHC.Core".
177 One place it is used is in mkWorkerArgs; see Note [Join points and beta-redexes]
178 in GHC.Core.Opt.WorkWrap.Utils. (Maybe there are other "clients" of this feature; I'm not sure).
179
180 * Hence when linting <body> we need to remember that a=Int, else we
181 might reject a correct program. So we carry a type substitution (in
182 this example [a -> Bool]) and apply this substitution before
183 comparing types. In effect, in Lint, type equality is always
184 equality-modulo-le-subst. This is in the le_subst field of
185 LintEnv. But nota bene:
186
187 (SI1) The le_subst substitution is applied to types and coercions only
188
189 (SI2) The result of that substitution is used only to check for type
190 equality, to check well-typed-ness, /but is then discarded/.
191 The result of substittion does not outlive the CoreLint pass.
192
193 (SI3) The InScopeSet of le_subst includes only TyVar and CoVar binders.
194
195 * The function
196 lintInTy :: Type -> LintM (Type, Kind)
197 returns a substituted type.
198
199 * When we encounter a binder (like x::a) we must apply the substitution
200 to the type of the binding variable. lintBinders does this.
201
202 * Clearly we need to clone tyvar binders as we go.
203
204 * But take care (#17590)! We must also clone CoVar binders:
205 let a = TYPE (ty |> cv)
206 in \cv -> blah
207 blindly substituting for `a` might capture `cv`.
208
209 * Alas, when cloning a coercion variable we might choose a unique
210 that happens to clash with an inner Id, thus
211 \cv_66 -> let wild_X7 = blah in blah
212 We decide to clone `cv_66` because it's already in scope. Fine,
213 choose a new unique. Aha, X7 looks good. So we check the lambda
214 body with le_subst of [cv_66 :-> cv_X7]
215
216 This is all fine, even though we use the same unique as wild_X7.
217 As (SI2) says, we do /not/ return a new lambda
218 (\cv_X7 -> let wild_X7 = blah in ...)
219 We simply use the le_subst substitution in types/coercions only, when
220 checking for equality.
221
222 * We still need to check that Id occurrences are bound by some
223 enclosing binding. We do /not/ use the InScopeSet for the le_subst
224 for this purpose -- it contains only TyCoVars. Instead we have a separate
225 le_ids for the in-scope Id binders.
226
227 Sigh. We might want to explore getting rid of type-let!
228
229 Note [Bad unsafe coercion]
230 ~~~~~~~~~~~~~~~~~~~~~~~~~~
231 For discussion see https://gitlab.haskell.org/ghc/ghc/wikis/bad-unsafe-coercions
232 Linter introduces additional rules that checks improper coercion between
233 different types, called bad coercions. Following coercions are forbidden:
234
235 (a) coercions between boxed and unboxed values;
236 (b) coercions between unlifted values of the different sizes, here
237 active size is checked, i.e. size of the actual value but not
238 the space allocated for value;
239 (c) coercions between floating and integral boxed values, this check
240 is not yet supported for unboxed tuples, as no semantics were
241 specified for that;
242 (d) coercions from / to vector type
243 (e) If types are unboxed tuples then tuple (# A_1,..,A_n #) can be
244 coerced to (# B_1,..,B_m #) if n=m and for each pair A_i, B_i rules
245 (a-e) holds.
246
247 Note [Join points]
248 ~~~~~~~~~~~~~~~~~~
249 We check the rules listed in Note [Invariants on join points] in GHC.Core. The
250 only one that causes any difficulty is the first: All occurrences must be tail
251 calls. To this end, along with the in-scope set, we remember in le_joins the
252 subset of in-scope Ids that are valid join ids. For example:
253
254 join j x = ... in
255 case e of
256 A -> jump j y -- good
257 B -> case (jump j z) of -- BAD
258 C -> join h = jump j w in ... -- good
259 D -> let x = jump j v in ... -- BAD
260
261 A join point remains valid in case branches, so when checking the A
262 branch, j is still valid. When we check the scrutinee of the inner
263 case, however, we set le_joins to empty, and catch the
264 error. Similarly, join points can occur free in RHSes of other join
265 points but not the RHSes of value bindings (thunks and functions).
266
267 ************************************************************************
268 * *
269 Beginning and ending passes
270 * *
271 ************************************************************************
272
273 These functions are not CoreM monad stuff, but they probably ought to
274 be, and it makes a convenient place for them. They print out stuff
275 before and after core passes, and do Core Lint when necessary.
276 -}
277
278 endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> CoreM ()
279 endPass pass binds rules
280 = do { hsc_env <- getHscEnv
281 ; print_unqual <- getPrintUnqualified
282 ; liftIO $ endPassIO hsc_env print_unqual pass binds rules }
283
284 endPassIO :: HscEnv -> PrintUnqualified
285 -> CoreToDo -> CoreProgram -> [CoreRule] -> IO ()
286 -- Used by the IO-is CorePrep too
287 endPassIO hsc_env print_unqual pass binds rules
288 = do { dumpPassResult logger dump_core_sizes print_unqual mb_flag
289 (showSDoc dflags (ppr pass)) (pprPassDetails pass) binds rules
290 ; lintPassResult hsc_env pass binds }
291 where
292 dump_core_sizes = not (gopt Opt_SuppressCoreSizes dflags)
293 logger = hsc_logger hsc_env
294 dflags = hsc_dflags hsc_env
295 mb_flag = case coreDumpFlag pass of
296 Just flag | logHasDumpFlag logger flag -> Just flag
297 | logHasDumpFlag logger Opt_D_verbose_core2core -> Just flag
298 _ -> Nothing
299
300 dumpPassResult :: Logger
301 -> Bool -- dump core sizes?
302 -> PrintUnqualified
303 -> Maybe DumpFlag -- Just df => show details in a file whose
304 -- name is specified by df
305 -> String -- Header
306 -> SDoc -- Extra info to appear after header
307 -> CoreProgram -> [CoreRule]
308 -> IO ()
309 dumpPassResult logger dump_core_sizes unqual mb_flag hdr extra_info binds rules
310 = do { forM_ mb_flag $ \flag -> do
311 logDumpFile logger (mkDumpStyle unqual) flag hdr FormatCore dump_doc
312
313 -- Report result size
314 -- This has the side effect of forcing the intermediate to be evaluated
315 -- if it's not already forced by a -ddump flag.
316 ; Err.debugTraceMsg logger 2 size_doc
317 }
318
319 where
320 size_doc = sep [text "Result size of" <+> text hdr, nest 2 (equals <+> ppr (coreBindsStats binds))]
321
322 dump_doc = vcat [ nest 2 extra_info
323 , size_doc
324 , blankLine
325 , if dump_core_sizes
326 then pprCoreBindingsWithSize binds
327 else pprCoreBindings binds
328 , ppUnless (null rules) pp_rules ]
329 pp_rules = vcat [ blankLine
330 , text "------ Local rules for imported ids --------"
331 , pprRules rules ]
332
333 coreDumpFlag :: CoreToDo -> Maybe DumpFlag
334 coreDumpFlag (CoreDoSimplify {}) = Just Opt_D_verbose_core2core
335 coreDumpFlag (CoreDoPluginPass {}) = Just Opt_D_verbose_core2core
336 coreDumpFlag CoreDoFloatInwards = Just Opt_D_verbose_core2core
337 coreDumpFlag (CoreDoFloatOutwards {}) = Just Opt_D_verbose_core2core
338 coreDumpFlag CoreLiberateCase = Just Opt_D_verbose_core2core
339 coreDumpFlag CoreDoStaticArgs = Just Opt_D_verbose_core2core
340 coreDumpFlag CoreDoCallArity = Just Opt_D_dump_call_arity
341 coreDumpFlag CoreDoExitify = Just Opt_D_dump_exitify
342 coreDumpFlag CoreDoDemand = Just Opt_D_dump_stranal
343 coreDumpFlag CoreDoCpr = Just Opt_D_dump_cpranal
344 coreDumpFlag CoreDoWorkerWrapper = Just Opt_D_dump_worker_wrapper
345 coreDumpFlag CoreDoSpecialising = Just Opt_D_dump_spec
346 coreDumpFlag CoreDoSpecConstr = Just Opt_D_dump_spec
347 coreDumpFlag CoreCSE = Just Opt_D_dump_cse
348 coreDumpFlag CoreDesugar = Just Opt_D_dump_ds_preopt
349 coreDumpFlag CoreDesugarOpt = Just Opt_D_dump_ds
350 coreDumpFlag CoreTidy = Just Opt_D_dump_simpl
351 coreDumpFlag CorePrep = Just Opt_D_dump_prep
352 coreDumpFlag CoreOccurAnal = Just Opt_D_dump_occur_anal
353
354 coreDumpFlag CoreAddCallerCcs = Nothing
355 coreDumpFlag CoreDoPrintCore = Nothing
356 coreDumpFlag (CoreDoRuleCheck {}) = Nothing
357 coreDumpFlag CoreDoNothing = Nothing
358 coreDumpFlag (CoreDoPasses {}) = Nothing
359
360 {-
361 ************************************************************************
362 * *
363 Top-level interfaces
364 * *
365 ************************************************************************
366 -}
367
368 lintPassResult :: HscEnv -> CoreToDo -> CoreProgram -> IO ()
369 lintPassResult hsc_env pass binds
370 | not (gopt Opt_DoCoreLinting dflags)
371 = return ()
372 | otherwise
373 = do { let warns_and_errs = lintCoreBindings dflags pass (interactiveInScope $ hsc_IC hsc_env) binds
374 ; Err.showPass logger ("Core Linted result of " ++ showPpr dflags pass)
375 ; displayLintResults logger (showLintWarnings pass) (ppr pass)
376 (pprCoreBindings binds) warns_and_errs }
377 where
378 dflags = hsc_dflags hsc_env
379 logger = hsc_logger hsc_env
380
381 displayLintResults :: Logger
382 -> Bool -- ^ If 'True', display linter warnings.
383 -- If 'False', ignore linter warnings.
384 -> SDoc -- ^ The source of the linted program
385 -> SDoc -- ^ The linted program, pretty-printed
386 -> WarnsAndErrs
387 -> IO ()
388 displayLintResults logger display_warnings pp_what pp_pgm (warns, errs)
389 | not (isEmptyBag errs)
390 = do { logMsg logger Err.MCDump noSrcSpan
391 $ withPprStyle defaultDumpStyle
392 (vcat [ lint_banner "errors" pp_what, Err.pprMessageBag errs
393 , text "*** Offending Program ***"
394 , pp_pgm
395 , text "*** End of Offense ***" ])
396 ; Err.ghcExit logger 1 }
397
398 | not (isEmptyBag warns)
399 , log_enable_debug (logFlags logger)
400 , display_warnings
401 -- If the Core linter encounters an error, output to stderr instead of
402 -- stdout (#13342)
403 = logMsg logger Err.MCInfo noSrcSpan
404 $ withPprStyle defaultDumpStyle
405 (lint_banner "warnings" pp_what $$ Err.pprMessageBag (mapBag ($$ blankLine) warns))
406
407 | otherwise = return ()
408
409 lint_banner :: String -> SDoc -> SDoc
410 lint_banner string pass = text "*** Core Lint" <+> text string
411 <+> text ": in result of" <+> pass
412 <+> text "***"
413
414 showLintWarnings :: CoreToDo -> Bool
415 -- Disable Lint warnings on the first simplifier pass, because
416 -- there may be some INLINE knots still tied, which is tiresomely noisy
417 showLintWarnings (CoreDoSimplify _ (SimplMode { sm_phase = InitialPhase })) = False
418 showLintWarnings _ = True
419
420 lintInteractiveExpr :: SDoc -- ^ The source of the linted expression
421 -> HscEnv -> CoreExpr -> IO ()
422 lintInteractiveExpr what hsc_env expr
423 | not (gopt Opt_DoCoreLinting dflags)
424 = return ()
425 | Just err <- lintExpr dflags (interactiveInScope $ hsc_IC hsc_env) expr
426 = displayLintResults logger False what (pprCoreExpr expr) (emptyBag, err)
427 | otherwise
428 = return ()
429 where
430 dflags = hsc_dflags hsc_env
431 logger = hsc_logger hsc_env
432
433 interactiveInScope :: InteractiveContext -> [Var]
434 -- In GHCi we may lint expressions, or bindings arising from 'deriving'
435 -- clauses, that mention variables bound in the interactive context.
436 -- These are Local things (see Note [Interactively-bound Ids in GHCi] in GHC.Runtime.Context).
437 -- So we have to tell Lint about them, lest it reports them as out of scope.
438 --
439 -- We do this by find local-named things that may appear free in interactive
440 -- context. This function is pretty revolting and quite possibly not quite right.
441 -- When we are not in GHCi, the interactive context (hsc_IC hsc_env) is empty
442 -- so this is a (cheap) no-op.
443 --
444 -- See #8215 for an example
445 interactiveInScope ictxt
446 = tyvars ++ ids
447 where
448 -- C.f. GHC.Tc.Module.setInteractiveContext, Desugar.deSugarExpr
449 (cls_insts, _fam_insts) = ic_instances ictxt
450 te1 = mkTypeEnvWithImplicits (ic_tythings ictxt)
451 te = extendTypeEnvWithIds te1 (map instanceDFunId cls_insts)
452 ids = typeEnvIds te
453 tyvars = tyCoVarsOfTypesList $ map idType ids
454 -- Why the type variables? How can the top level envt have free tyvars?
455 -- I think it's because of the GHCi debugger, which can bind variables
456 -- f :: [t] -> [t]
457 -- where t is a RuntimeUnk (see TcType)
458
459 -- | Type-check a 'CoreProgram'. See Note [Core Lint guarantee].
460 lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> WarnsAndErrs
461 -- Returns (warnings, errors)
462 -- If you edit this function, you may need to update the GHC formalism
463 -- See Note [GHC Formalism]
464 lintCoreBindings dflags pass local_in_scope binds
465 = initL dflags flags local_in_scope $
466 addLoc TopLevelBindings $
467 do { checkL (null dups) (dupVars dups)
468 ; checkL (null ext_dups) (dupExtVars ext_dups)
469 ; lintRecBindings TopLevel all_pairs $ \_ ->
470 return () }
471 where
472 all_pairs = flattenBinds binds
473 -- Put all the top-level binders in scope at the start
474 -- This is because rewrite rules can bring something
475 -- into use 'unexpectedly'; see Note [Glomming] in "GHC.Core.Opt.OccurAnal"
476 binders = map fst all_pairs
477
478 flags = (defaultLintFlags dflags)
479 { lf_check_global_ids = check_globals
480 , lf_check_inline_loop_breakers = check_lbs
481 , lf_check_static_ptrs = check_static_ptrs
482 , lf_check_linearity = check_linearity
483 , lf_check_fixed_rep = check_fixed_rep }
484
485 -- In the output of the desugarer, before optimisation,
486 -- we have eta-expanded data constructors with representation-polymorphic
487 -- bindings; so we switch off the representation-polymorphism checks.
488 -- The very simple optimiser will beta-reduce them away.
489 -- See Note [Checking representation-polymorphic data constructors]
490 -- in GHC.HsToCore.Expr.
491 check_fixed_rep = case pass of
492 CoreDesugar -> False
493 _ -> True
494
495 -- See Note [Checking for global Ids]
496 check_globals = case pass of
497 CoreTidy -> False
498 CorePrep -> False
499 _ -> True
500
501 -- See Note [Checking for INLINE loop breakers]
502 check_lbs = case pass of
503 CoreDesugar -> False
504 CoreDesugarOpt -> False
505 _ -> True
506
507 -- See Note [Checking StaticPtrs]
508 check_static_ptrs | not (xopt LangExt.StaticPointers dflags) = AllowAnywhere
509 | otherwise = case pass of
510 CoreDoFloatOutwards _ -> AllowAtTopLevel
511 CoreTidy -> RejectEverywhere
512 CorePrep -> AllowAtTopLevel
513 _ -> AllowAnywhere
514
515 -- See Note [Linting linearity]
516 check_linearity = gopt Opt_DoLinearCoreLinting dflags || (
517 case pass of
518 CoreDesugar -> True
519 _ -> False)
520
521 (_, dups) = removeDups compare binders
522
523 -- dups_ext checks for names with different uniques
524 -- but the same External name M.n. We don't
525 -- allow this at top level:
526 -- M.n{r3} = ...
527 -- M.n{r29} = ...
528 -- because they both get the same linker symbol
529 ext_dups = snd (removeDups ord_ext (map Var.varName binders))
530 ord_ext n1 n2 | Just m1 <- nameModule_maybe n1
531 , Just m2 <- nameModule_maybe n2
532 = compare (m1, nameOccName n1) (m2, nameOccName n2)
533 | otherwise = LT
534
535 {-
536 ************************************************************************
537 * *
538 \subsection[lintUnfolding]{lintUnfolding}
539 * *
540 ************************************************************************
541
542 Note [Linting Unfoldings from Interfaces]
543 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
544 We use this to check all top-level unfoldings that come in from interfaces
545 (it is very painful to catch errors otherwise).
546
547 We do not need to call lintUnfolding on unfoldings that are nested within
548 top-level unfoldings; they are linted when we lint the top-level unfolding;
549 hence the `TopLevelFlag` on `tcPragExpr` in GHC.IfaceToCore.
550
551 -}
552
553 lintUnfolding :: Bool -- True <=> is a compulsory unfolding
554 -> DynFlags
555 -> SrcLoc
556 -> VarSet -- Treat these as in scope
557 -> CoreExpr
558 -> Maybe (Bag SDoc) -- Nothing => OK
559
560 lintUnfolding is_compulsory dflags locn var_set expr
561 | isEmptyBag errs = Nothing
562 | otherwise = Just errs
563 where
564 vars = nonDetEltsUniqSet var_set
565 (_warns, errs) = initL dflags (defaultLintFlags dflags) vars $
566 if is_compulsory
567 -- See Note [Checking for representation polymorphism]
568 then noFixedRuntimeRepChecks linter
569 else linter
570 linter = addLoc (ImportedUnfolding locn) $
571 lintCoreExpr expr
572
573 lintExpr :: DynFlags
574 -> [Var] -- Treat these as in scope
575 -> CoreExpr
576 -> Maybe (Bag SDoc) -- Nothing => OK
577
578 lintExpr dflags vars expr
579 | isEmptyBag errs = Nothing
580 | otherwise = Just errs
581 where
582 (_warns, errs) = initL dflags (defaultLintFlags dflags) vars linter
583 linter = addLoc TopLevelBindings $
584 lintCoreExpr expr
585
586 {-
587 ************************************************************************
588 * *
589 \subsection[lintCoreBinding]{lintCoreBinding}
590 * *
591 ************************************************************************
592
593 Check a core binding, returning the list of variables bound.
594 -}
595
596 -- Returns a UsageEnv because this function is called in lintCoreExpr for
597 -- Let
598
599 lintRecBindings :: TopLevelFlag -> [(Id, CoreExpr)]
600 -> ([LintedId] -> LintM a) -> LintM (a, [UsageEnv])
601 lintRecBindings top_lvl pairs thing_inside
602 = lintIdBndrs top_lvl bndrs $ \ bndrs' ->
603 do { ues <- zipWithM lint_pair bndrs' rhss
604 ; a <- thing_inside bndrs'
605 ; return (a, ues) }
606 where
607 (bndrs, rhss) = unzip pairs
608 lint_pair bndr' rhs
609 = addLoc (RhsOf bndr') $
610 do { (rhs_ty, ue) <- lintRhs bndr' rhs -- Check the rhs
611 ; lintLetBind top_lvl Recursive bndr' rhs rhs_ty
612 ; return ue }
613
614 lintLetBody :: [LintedId] -> CoreExpr -> LintM (LintedType, UsageEnv)
615 lintLetBody bndrs body
616 = do { (body_ty, body_ue) <- addLoc (BodyOfLetRec bndrs) (lintCoreExpr body)
617 ; mapM_ (lintJoinBndrType body_ty) bndrs
618 ; return (body_ty, body_ue) }
619
620 lintLetBind :: TopLevelFlag -> RecFlag -> LintedId
621 -> CoreExpr -> LintedType -> LintM ()
622 -- Binder's type, and the RHS, have already been linted
623 -- This function checks other invariants
624 lintLetBind top_lvl rec_flag binder rhs rhs_ty
625 = do { let binder_ty = idType binder
626 ; ensureEqTys binder_ty rhs_ty (mkRhsMsg binder (text "RHS") rhs_ty)
627
628 -- If the binding is for a CoVar, the RHS should be (Coercion co)
629 -- See Note [Core type and coercion invariant] in GHC.Core
630 ; checkL (not (isCoVar binder) || isCoArg rhs)
631 (mkLetErr binder rhs)
632
633 -- Check the let/app invariant
634 -- See Note [Core let/app invariant] in GHC.Core
635 ; checkL ( isJoinId binder
636 || not (isUnliftedType binder_ty)
637 || (isNonRec rec_flag && exprOkForSpeculation rhs)
638 || isDataConWorkId binder || isDataConWrapId binder -- until #17521 is fixed
639 || exprIsTickedString rhs)
640 (badBndrTyMsg binder (text "unlifted"))
641
642 -- Check that if the binder is at the top level and has type Addr#,
643 -- that it is a string literal, see
644 -- Note [Core top-level string literals].
645 ; checkL (not (isTopLevel top_lvl && binder_ty `eqType` addrPrimTy)
646 || exprIsTickedString rhs)
647 (mkTopNonLitStrMsg binder)
648
649 ; flags <- getLintFlags
650
651 -- Check that a join-point binder has a valid type
652 -- NB: lintIdBinder has checked that it is not top-level bound
653 ; case isJoinId_maybe binder of
654 Nothing -> return ()
655 Just arity -> checkL (isValidJoinPointType arity binder_ty)
656 (mkInvalidJoinPointMsg binder binder_ty)
657
658 ; when (lf_check_inline_loop_breakers flags
659 && isStableUnfolding (realIdUnfolding binder)
660 && isStrongLoopBreaker (idOccInfo binder)
661 && isInlinePragma (idInlinePragma binder))
662 (addWarnL (text "INLINE binder is (non-rule) loop breaker:" <+> ppr binder))
663 -- Only non-rule loop breakers inhibit inlining
664
665 -- We used to check that the dmdTypeDepth of a demand signature never
666 -- exceeds idArity, but that is an unnecessary complication, see
667 -- Note [idArity varies independently of dmdTypeDepth] in GHC.Core.Opt.DmdAnal
668
669 -- Check that the binder's arity is within the bounds imposed by
670 -- the type and the strictness signature. See Note [exprArity invariant]
671 -- and Note [Trimming arity]
672 ; checkL (typeArity (idType binder) `lengthAtLeast` idArity binder)
673 (text "idArity" <+> ppr (idArity binder) <+>
674 text "exceeds typeArity" <+>
675 ppr (length (typeArity (idType binder))) <> colon <+>
676 ppr binder)
677
678 ; case splitDmdSig (idDmdSig binder) of
679 (demands, result_info) | isDeadEndDiv result_info ->
680 checkL (demands `lengthAtLeast` idArity binder)
681 (text "idArity" <+> ppr (idArity binder) <+>
682 text "exceeds arity imposed by the strictness signature" <+>
683 ppr (idDmdSig binder) <> colon <+>
684 ppr binder)
685 _ -> return ()
686
687 ; addLoc (RuleOf binder) $ mapM_ (lintCoreRule binder binder_ty) (idCoreRules binder)
688
689 ; addLoc (UnfoldingOf binder) $
690 lintIdUnfolding binder binder_ty (idUnfolding binder)
691 ; return () }
692
693 -- We should check the unfolding, if any, but this is tricky because
694 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
695
696 -- | Checks the RHS of bindings. It only differs from 'lintCoreExpr'
697 -- in that it doesn't reject occurrences of the function 'makeStatic' when they
698 -- appear at the top level and @lf_check_static_ptrs == AllowAtTopLevel@, and
699 -- for join points, it skips the outer lambdas that take arguments to the
700 -- join point.
701 --
702 -- See Note [Checking StaticPtrs].
703 lintRhs :: Id -> CoreExpr -> LintM (LintedType, UsageEnv)
704 -- NB: the Id can be Linted or not -- it's only used for
705 -- its OccInfo and join-pointer-hood
706 lintRhs bndr rhs
707 | Just arity <- isJoinId_maybe bndr
708 = lintJoinLams arity (Just bndr) rhs
709 | AlwaysTailCalled arity <- tailCallInfo (idOccInfo bndr)
710 = lintJoinLams arity Nothing rhs
711
712 -- Allow applications of the data constructor @StaticPtr@ at the top
713 -- but produce errors otherwise.
714 lintRhs _bndr rhs = fmap lf_check_static_ptrs getLintFlags >>= go
715 where
716 -- Allow occurrences of 'makeStatic' at the top-level but produce errors
717 -- otherwise.
718 go :: StaticPtrCheck -> LintM (OutType, UsageEnv)
719 go AllowAtTopLevel
720 | (binders0, rhs') <- collectTyBinders rhs
721 , Just (fun, t, info, e) <- collectMakeStaticArgs rhs'
722 = markAllJoinsBad $
723 foldr
724 -- imitate @lintCoreExpr (Lam ...)@
725 lintLambda
726 -- imitate @lintCoreExpr (App ...)@
727 (do fun_ty_ue <- lintCoreExpr fun
728 lintCoreArgs fun_ty_ue [Type t, info, e]
729 )
730 binders0
731 go _ = markAllJoinsBad $ lintCoreExpr rhs
732
733 -- | Lint the RHS of a join point with expected join arity of @n@ (see Note
734 -- [Join points] in "GHC.Core").
735 lintJoinLams :: JoinArity -> Maybe Id -> CoreExpr -> LintM (LintedType, UsageEnv)
736 lintJoinLams join_arity enforce rhs
737 = go join_arity rhs
738 where
739 go 0 expr = lintCoreExpr expr
740 go n (Lam var body) = lintLambda var $ go (n-1) body
741 go n expr | Just bndr <- enforce -- Join point with too few RHS lambdas
742 = failWithL $ mkBadJoinArityMsg bndr join_arity n rhs
743 | otherwise -- Future join point, not yet eta-expanded
744 = markAllJoinsBad $ lintCoreExpr expr
745 -- Body of lambda is not a tail position
746
747 lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
748 lintIdUnfolding bndr bndr_ty uf
749 | isStableUnfolding uf
750 , Just rhs <- maybeUnfoldingTemplate uf
751 = do { ty <- fst <$> (if isCompulsoryUnfolding uf
752 then noFixedRuntimeRepChecks $ lintRhs bndr rhs
753 -- ^^^^^^^^^^^^^^^^^^^^^^^
754 -- See Note [Checking for representation polymorphism]
755 else lintRhs bndr rhs)
756 ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) }
757 lintIdUnfolding _ _ _
758 = return () -- Do not Lint unstable unfoldings, because that leads
759 -- to exponential behaviour; c.f. GHC.Core.FVs.idUnfoldingVars
760
761 {-
762 Note [Checking for INLINE loop breakers]
763 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
764 It's very suspicious if a strong loop breaker is marked INLINE.
765
766 However, the desugarer generates instance methods with INLINE pragmas
767 that form a mutually recursive group. Only after a round of
768 simplification are they unravelled. So we suppress the test for
769 the desugarer.
770
771 Note [Checking for representation polymorphism]
772 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
773 We ordinarily want to check for bad representation polymorphism. See
774 Note [Representation polymorphism invariants] in GHC.Core. However, we do *not*
775 want to do this in a compulsory unfolding. Compulsory unfoldings arise
776 only internally, for things like newtype wrappers, dictionaries, and
777 (notably) unsafeCoerce#. These might legitimately be representation-polymorphic;
778 indeed representation-polyorphic unfoldings are a primary reason for the
779 very existence of compulsory unfoldings (we can't compile code for
780 the original, representation-polymorphic, binding).
781
782 It is vitally important that we do representation polymorphism checks *after*
783 performing the unfolding, but not beforehand. This is all safe because
784 we will check any unfolding after it has been unfolded; checking the
785 unfolding beforehand is merely an optimization, and one that actively
786 hurts us here.
787
788 Note [Linting of runRW#]
789 ~~~~~~~~~~~~~~~~~~~~~~~~
790 runRW# has some very special behavior (see Note [runRW magic] in
791 GHC.CoreToStg.Prep) which CoreLint must accommodate, by allowing
792 join points in its argument. For example, this is fine:
793
794 join j x = ...
795 in runRW# (\s. case v of
796 A -> j 3
797 B -> j 4)
798
799 Usually those calls to the join point 'j' would not be valid tail calls,
800 because they occur in a function argument. But in the case of runRW#
801 they are fine, because runRW# (\s.e) behaves operationally just like e.
802 (runRW# is ultimately inlined in GHC.CoreToStg.Prep.)
803
804 In the case that the continuation is /not/ a lambda we simply disable this
805 special behaviour. For example, this is /not/ fine:
806
807 join j = ...
808 in runRW# @r @ty (jump j)
809
810
811
812 ************************************************************************
813 * *
814 \subsection[lintCoreExpr]{lintCoreExpr}
815 * *
816 ************************************************************************
817 -}
818
819 -- Linted things: substitution applied, and type is linted
820 type LintedType = Type
821 type LintedKind = Kind
822 type LintedCoercion = Coercion
823 type LintedTyCoVar = TyCoVar
824 type LintedId = Id
825
826 -- | Lint an expression cast through the given coercion, returning the type
827 -- resulting from the cast.
828 lintCastExpr :: CoreExpr -> LintedType -> Coercion -> LintM LintedType
829 lintCastExpr expr expr_ty co
830 = do { co' <- lintCoercion co
831 ; let (Pair from_ty to_ty, role) = coercionKindRole co'
832 ; checkValueType to_ty $
833 text "target of cast" <+> quotes (ppr co')
834 ; lintRole co' Representational role
835 ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
836 ; return to_ty }
837
838 lintCoreExpr :: CoreExpr -> LintM (LintedType, UsageEnv)
839 -- The returned type has the substitution from the monad
840 -- already applied to it:
841 -- lintCoreExpr e subst = exprType (subst e)
842 --
843 -- The returned "type" can be a kind, if the expression is (Type ty)
844
845 -- If you edit this function, you may need to update the GHC formalism
846 -- See Note [GHC Formalism]
847
848 lintCoreExpr (Var var)
849 = lintIdOcc var 0
850
851 lintCoreExpr (Lit lit)
852 = return (literalType lit, zeroUE)
853
854 lintCoreExpr (Cast expr co)
855 = do (expr_ty, ue) <- markAllJoinsBad $ lintCoreExpr expr
856 to_ty <- lintCastExpr expr expr_ty co
857 return (to_ty, ue)
858
859 lintCoreExpr (Tick tickish expr)
860 = do case tickish of
861 Breakpoint _ _ ids -> forM_ ids $ \id -> do
862 checkDeadIdOcc id
863 lookupIdInScope id
864 _ -> return ()
865 markAllJoinsBadIf block_joins $ lintCoreExpr expr
866 where
867 block_joins = not (tickish `tickishScopesLike` SoftScope)
868 -- TODO Consider whether this is the correct rule. It is consistent with
869 -- the simplifier's behaviour - cost-centre-scoped ticks become part of
870 -- the continuation, and thus they behave like part of an evaluation
871 -- context, but soft-scoped and non-scoped ticks simply wrap the result
872 -- (see Simplify.simplTick).
873
874 lintCoreExpr (Let (NonRec tv (Type ty)) body)
875 | isTyVar tv
876 = -- See Note [Linting type lets]
877 do { ty' <- lintType ty
878 ; lintTyBndr tv $ \ tv' ->
879 do { addLoc (RhsOf tv) $ lintTyKind tv' ty'
880 -- Now extend the substitution so we
881 -- take advantage of it in the body
882 ; extendTvSubstL tv ty' $
883 addLoc (BodyOfLetRec [tv]) $
884 lintCoreExpr body } }
885
886 lintCoreExpr (Let (NonRec bndr rhs) body)
887 | isId bndr
888 = do { -- First Lint the RHS, before bringing the binder into scope
889 (rhs_ty, let_ue) <- lintRhs bndr rhs
890
891 -- See Note [Multiplicity of let binders] in Var
892 -- Now lint the binder
893 ; lintBinder LetBind bndr $ \bndr' ->
894 do { lintLetBind NotTopLevel NonRecursive bndr' rhs rhs_ty
895 ; addAliasUE bndr let_ue (lintLetBody [bndr'] body) } }
896
897 | otherwise
898 = failWithL (mkLetErr bndr rhs) -- Not quite accurate
899
900 lintCoreExpr e@(Let (Rec pairs) body)
901 = do { -- Check that the list of pairs is non-empty
902 checkL (not (null pairs)) (emptyRec e)
903
904 -- Check that there are no duplicated binders
905 ; let (_, dups) = removeDups compare bndrs
906 ; checkL (null dups) (dupVars dups)
907
908 -- Check that either all the binders are joins, or none
909 ; checkL (all isJoinId bndrs || all (not . isJoinId) bndrs) $
910 mkInconsistentRecMsg bndrs
911
912 -- See Note [Multiplicity of let binders] in Var
913 ; ((body_type, body_ue), ues) <-
914 lintRecBindings NotTopLevel pairs $ \ bndrs' ->
915 lintLetBody bndrs' body
916 ; return (body_type, body_ue `addUE` scaleUE Many (foldr1 addUE ues)) }
917 where
918 bndrs = map fst pairs
919
920 lintCoreExpr e@(App _ _)
921 | Var fun <- fun
922 , fun `hasKey` runRWKey
923 -- N.B. we may have an over-saturated application of the form:
924 -- runRW (\s -> \x -> ...) y
925 , ty_arg1 : ty_arg2 : arg3 : rest <- args
926 = do { fun_pair1 <- lintCoreArg (idType fun, zeroUE) ty_arg1
927 ; (fun_ty2, ue2) <- lintCoreArg fun_pair1 ty_arg2
928 -- See Note [Linting of runRW#]
929 ; let lintRunRWCont :: CoreArg -> LintM (LintedType, UsageEnv)
930 lintRunRWCont expr@(Lam _ _) =
931 lintJoinLams 1 (Just fun) expr
932 lintRunRWCont other = markAllJoinsBad $ lintCoreExpr other
933 -- TODO: Look through ticks?
934 ; (arg3_ty, ue3) <- lintRunRWCont arg3
935 ; app_ty <- lintValApp arg3 fun_ty2 arg3_ty ue2 ue3
936 ; lintCoreArgs app_ty rest }
937
938 | otherwise
939 = do { pair <- lintCoreFun fun (length args)
940 ; lintCoreArgs pair args }
941 where
942 (fun, args) = collectArgs e
943
944 lintCoreExpr (Lam var expr)
945 = markAllJoinsBad $
946 lintLambda var $ lintCoreExpr expr
947
948 lintCoreExpr (Case scrut var alt_ty alts)
949 = lintCaseExpr scrut var alt_ty alts
950
951 -- This case can't happen; linting types in expressions gets routed through
952 -- lintCoreArgs
953 lintCoreExpr (Type ty)
954 = failWithL (text "Type found as expression" <+> ppr ty)
955
956 lintCoreExpr (Coercion co)
957 = do { co' <- addLoc (InCo co) $
958 lintCoercion co
959 ; return (coercionType co', zeroUE) }
960
961 ----------------------
962 lintIdOcc :: Var -> Int -- Number of arguments (type or value) being passed
963 -> LintM (LintedType, UsageEnv) -- returns type of the *variable*
964 lintIdOcc var nargs
965 = addLoc (OccOf var) $
966 do { checkL (isNonCoVarId var)
967 (text "Non term variable" <+> ppr var)
968 -- See GHC.Core Note [Variable occurrences in Core]
969
970 -- Check that the type of the occurrence is the same
971 -- as the type of the binding site. The inScopeIds are
972 -- /un-substituted/, so this checks that the occurrence type
973 -- is identical to the binder type.
974 -- This makes things much easier for things like:
975 -- /\a. \(x::Maybe a). /\a. ...(x::Maybe a)...
976 -- The "::Maybe a" on the occurrence is referring to the /outer/ a.
977 -- If we compared /substituted/ types we'd risk comparing
978 -- (Maybe a) from the binding site with bogus (Maybe a1) from
979 -- the occurrence site. Comparing un-substituted types finesses
980 -- this altogether
981 ; (bndr, linted_bndr_ty) <- lookupIdInScope var
982 ; let occ_ty = idType var
983 bndr_ty = idType bndr
984 ; ensureEqTys occ_ty bndr_ty $
985 mkBndrOccTypeMismatchMsg bndr var bndr_ty occ_ty
986
987 -- Check for a nested occurrence of the StaticPtr constructor.
988 -- See Note [Checking StaticPtrs].
989 ; lf <- getLintFlags
990 ; when (nargs /= 0 && lf_check_static_ptrs lf /= AllowAnywhere) $
991 checkL (idName var /= makeStaticName) $
992 text "Found makeStatic nested in an expression"
993
994 ; checkDeadIdOcc var
995 ; checkJoinOcc var nargs
996
997 ; usage <- varCallSiteUsage var
998
999 ; return (linted_bndr_ty, usage) }
1000
1001 lintCoreFun :: CoreExpr
1002 -> Int -- Number of arguments (type or val) being passed
1003 -> LintM (LintedType, UsageEnv) -- Returns type of the *function*
1004 lintCoreFun (Var var) nargs
1005 = lintIdOcc var nargs
1006
1007 lintCoreFun (Lam var body) nargs
1008 -- Act like lintCoreExpr of Lam, but *don't* call markAllJoinsBad; see
1009 -- Note [Beta redexes]
1010 | nargs /= 0
1011 = lintLambda var $ lintCoreFun body (nargs - 1)
1012
1013 lintCoreFun expr nargs
1014 = markAllJoinsBadIf (nargs /= 0) $
1015 -- See Note [Join points are less general than the paper]
1016 lintCoreExpr expr
1017 ------------------
1018 lintLambda :: Var -> LintM (Type, UsageEnv) -> LintM (Type, UsageEnv)
1019 lintLambda var lintBody =
1020 addLoc (LambdaBodyOf var) $
1021 lintBinder LambdaBind var $ \ var' ->
1022 do { (body_ty, ue) <- lintBody
1023 ; ue' <- checkLinearity ue var'
1024 ; return (mkLamType var' body_ty, ue') }
1025 ------------------
1026 checkDeadIdOcc :: Id -> LintM ()
1027 -- Occurrences of an Id should never be dead....
1028 -- except when we are checking a case pattern
1029 checkDeadIdOcc id
1030 | isDeadOcc (idOccInfo id)
1031 = do { in_case <- inCasePat
1032 ; checkL in_case
1033 (text "Occurrence of a dead Id" <+> ppr id) }
1034 | otherwise
1035 = return ()
1036
1037 ------------------
1038 lintJoinBndrType :: LintedType -- Type of the body
1039 -> LintedId -- Possibly a join Id
1040 -> LintM ()
1041 -- Checks that the return type of a join Id matches the body
1042 -- E.g. join j x = rhs in body
1043 -- The type of 'rhs' must be the same as the type of 'body'
1044 lintJoinBndrType body_ty bndr
1045 | Just arity <- isJoinId_maybe bndr
1046 , let bndr_ty = idType bndr
1047 , (bndrs, res) <- splitPiTys bndr_ty
1048 = checkL (length bndrs >= arity
1049 && body_ty `eqType` mkPiTys (drop arity bndrs) res) $
1050 hang (text "Join point returns different type than body")
1051 2 (vcat [ text "Join bndr:" <+> ppr bndr <+> dcolon <+> ppr (idType bndr)
1052 , text "Join arity:" <+> ppr arity
1053 , text "Body type:" <+> ppr body_ty ])
1054 | otherwise
1055 = return ()
1056
1057 checkJoinOcc :: Id -> JoinArity -> LintM ()
1058 -- Check that if the occurrence is a JoinId, then so is the
1059 -- binding site, and it's a valid join Id
1060 checkJoinOcc var n_args
1061 | Just join_arity_occ <- isJoinId_maybe var
1062 = do { mb_join_arity_bndr <- lookupJoinId var
1063 ; case mb_join_arity_bndr of {
1064 Nothing -> -- Binder is not a join point
1065 do { join_set <- getValidJoins
1066 ; addErrL (text "join set " <+> ppr join_set $$
1067 invalidJoinOcc var) } ;
1068
1069 Just join_arity_bndr ->
1070
1071 do { checkL (join_arity_bndr == join_arity_occ) $
1072 -- Arity differs at binding site and occurrence
1073 mkJoinBndrOccMismatchMsg var join_arity_bndr join_arity_occ
1074
1075 ; checkL (n_args == join_arity_occ) $
1076 -- Arity doesn't match #args
1077 mkBadJumpMsg var join_arity_occ n_args } } }
1078
1079 | otherwise
1080 = return ()
1081
1082 -- Check that the usage of var is consistent with var itself, and pop the var
1083 -- from the usage environment (this is important because of shadowing).
1084 checkLinearity :: UsageEnv -> Var -> LintM UsageEnv
1085 checkLinearity body_ue lam_var =
1086 case varMultMaybe lam_var of
1087 Just mult -> do ensureSubUsage lhs mult (err_msg mult)
1088 return $ deleteUE body_ue lam_var
1089 Nothing -> return body_ue -- A type variable
1090 where
1091 lhs = lookupUE body_ue lam_var
1092 err_msg mult = text "Linearity failure in lambda:" <+> ppr lam_var
1093 $$ ppr lhs <+> text "⊈" <+> ppr mult
1094
1095 {-
1096 Note [No alternatives lint check]
1097 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1098 Case expressions with no alternatives are odd beasts, and it would seem
1099 like they would worth be looking at in the linter (cf #10180). We
1100 used to check two things:
1101
1102 * exprIsHNF is false: it would *seem* to be terribly wrong if
1103 the scrutinee was already in head normal form.
1104
1105 * exprIsDeadEnd is true: we should be able to see why GHC believes the
1106 scrutinee is diverging for sure.
1107
1108 It was already known that the second test was not entirely reliable.
1109 Unfortunately (#13990), the first test turned out not to be reliable
1110 either. Getting the checks right turns out to be somewhat complicated.
1111
1112 For example, suppose we have (comment 8)
1113
1114 data T a where
1115 TInt :: T Int
1116
1117 absurdTBool :: T Bool -> a
1118 absurdTBool v = case v of
1119
1120 data Foo = Foo !(T Bool)
1121
1122 absurdFoo :: Foo -> a
1123 absurdFoo (Foo x) = absurdTBool x
1124
1125 GHC initially accepts the empty case because of the GADT conditions. But then
1126 we inline absurdTBool, getting
1127
1128 absurdFoo (Foo x) = case x of
1129
1130 x is in normal form (because the Foo constructor is strict) but the
1131 case is empty. To avoid this problem, GHC would have to recognize
1132 that matching on Foo x is already absurd, which is not so easy.
1133
1134 More generally, we don't really know all the ways that GHC can
1135 lose track of why an expression is bottom, so we shouldn't make too
1136 much fuss when that happens.
1137
1138
1139 Note [Beta redexes]
1140 ~~~~~~~~~~~~~~~~~~~
1141 Consider:
1142
1143 join j @x y z = ... in
1144 (\@x y z -> jump j @x y z) @t e1 e2
1145
1146 This is clearly ill-typed, since the jump is inside both an application and a
1147 lambda, either of which is enough to disqualify it as a tail call (see Note
1148 [Invariants on join points] in GHC.Core). However, strictly from a
1149 lambda-calculus perspective, the term doesn't go wrong---after the two beta
1150 reductions, the jump *is* a tail call and everything is fine.
1151
1152 Why would we want to allow this when we have let? One reason is that a compound
1153 beta redex (that is, one with more than one argument) has different scoping
1154 rules: naively reducing the above example using lets will capture any free
1155 occurrence of y in e2. More fundamentally, type lets are tricky; many passes,
1156 such as Float Out, tacitly assume that the incoming program's type lets have
1157 all been dealt with by the simplifier. Thus we don't want to let-bind any types
1158 in, say, GHC.Core.Subst.simpleOptPgm, which in some circumstances can run immediately
1159 before Float Out.
1160
1161 All that said, currently GHC.Core.Subst.simpleOptPgm is the only thing using this
1162 loophole, doing so to avoid re-traversing large functions (beta-reducing a type
1163 lambda without introducing a type let requires a substitution). TODO: Improve
1164 simpleOptPgm so that we can forget all this ever happened.
1165
1166 ************************************************************************
1167 * *
1168 \subsection[lintCoreArgs]{lintCoreArgs}
1169 * *
1170 ************************************************************************
1171
1172 The basic version of these functions checks that the argument is a
1173 subtype of the required type, as one would expect.
1174 -}
1175
1176
1177 lintCoreArgs :: (LintedType, UsageEnv) -> [CoreArg] -> LintM (LintedType, UsageEnv)
1178 lintCoreArgs (fun_ty, fun_ue) args = foldM lintCoreArg (fun_ty, fun_ue) args
1179
1180 lintCoreArg :: (LintedType, UsageEnv) -> CoreArg -> LintM (LintedType, UsageEnv)
1181 lintCoreArg (fun_ty, ue) (Type arg_ty)
1182 = do { checkL (not (isCoercionTy arg_ty))
1183 (text "Unnecessary coercion-to-type injection:"
1184 <+> ppr arg_ty)
1185 ; arg_ty' <- lintType arg_ty
1186 ; res <- lintTyApp fun_ty arg_ty'
1187 ; return (res, ue) }
1188
1189 lintCoreArg (fun_ty, fun_ue) arg
1190 = do { (arg_ty, arg_ue) <- markAllJoinsBad $ lintCoreExpr arg
1191 -- See Note [Representation polymorphism invariants] in GHC.Core
1192 ; flags <- getLintFlags
1193
1194 ; when (lf_check_fixed_rep flags) $
1195 -- Only do these checks if lf_check_fixed_rep is on,
1196 -- because otherwise isUnliftedType panics
1197 do { checkL (typeHasFixedRuntimeRep arg_ty)
1198 (text "Argument does not have a fixed runtime representation"
1199 <+> ppr arg <+> dcolon
1200 <+> parens (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty)))
1201
1202 ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
1203 (mkLetAppMsg arg) }
1204
1205 ; lintValApp arg fun_ty arg_ty fun_ue arg_ue }
1206
1207 -----------------
1208 lintAltBinders :: UsageEnv
1209 -> Var -- Case binder
1210 -> LintedType -- Scrutinee type
1211 -> LintedType -- Constructor type
1212 -> [(Mult, OutVar)] -- Binders
1213 -> LintM UsageEnv
1214 -- If you edit this function, you may need to update the GHC formalism
1215 -- See Note [GHC Formalism]
1216 lintAltBinders rhs_ue _case_bndr scrut_ty con_ty []
1217 = do { ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
1218 ; return rhs_ue }
1219 lintAltBinders rhs_ue case_bndr scrut_ty con_ty ((var_w, bndr):bndrs)
1220 | isTyVar bndr
1221 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
1222 ; lintAltBinders rhs_ue case_bndr scrut_ty con_ty' bndrs }
1223 | otherwise
1224 = do { (con_ty', _) <- lintValApp (Var bndr) con_ty (idType bndr) zeroUE zeroUE
1225 -- We can pass zeroUE to lintValApp because we ignore its usage
1226 -- calculation and compute it in the call for checkCaseLinearity below.
1227 ; rhs_ue' <- checkCaseLinearity rhs_ue case_bndr var_w bndr
1228 ; lintAltBinders rhs_ue' case_bndr scrut_ty con_ty' bndrs }
1229
1230 -- | Implements the case rules for linearity
1231 checkCaseLinearity :: UsageEnv -> Var -> Mult -> Var -> LintM UsageEnv
1232 checkCaseLinearity ue case_bndr var_w bndr = do
1233 ensureSubUsage lhs rhs err_msg
1234 lintLinearBinder (ppr bndr) (case_bndr_w `mkMultMul` var_w) (varMult bndr)
1235 return $ deleteUE ue bndr
1236 where
1237 lhs = bndr_usage `addUsage` (var_w `scaleUsage` case_bndr_usage)
1238 rhs = case_bndr_w `mkMultMul` var_w
1239 err_msg = (text "Linearity failure in variable:" <+> ppr bndr
1240 $$ ppr lhs <+> text "⊈" <+> ppr rhs
1241 $$ text "Computed by:"
1242 <+> text "LHS:" <+> lhs_formula
1243 <+> text "RHS:" <+> rhs_formula)
1244 lhs_formula = ppr bndr_usage <+> text "+"
1245 <+> parens (ppr case_bndr_usage <+> text "*" <+> ppr var_w)
1246 rhs_formula = ppr case_bndr_w <+> text "*" <+> ppr var_w
1247 case_bndr_w = varMult case_bndr
1248 case_bndr_usage = lookupUE ue case_bndr
1249 bndr_usage = lookupUE ue bndr
1250
1251
1252
1253 -----------------
1254 lintTyApp :: LintedType -> LintedType -> LintM LintedType
1255 lintTyApp fun_ty arg_ty
1256 | Just (tv,body_ty) <- splitForAllTyCoVar_maybe fun_ty
1257 = do { lintTyKind tv arg_ty
1258 ; in_scope <- getInScope
1259 -- substTy needs the set of tyvars in scope to avoid generating
1260 -- uniques that are already in scope.
1261 -- See Note [The substitution invariant] in GHC.Core.TyCo.Subst
1262 ; return (substTyWithInScope in_scope [tv] [arg_ty] body_ty) }
1263
1264 | otherwise
1265 = failWithL (mkTyAppMsg fun_ty arg_ty)
1266
1267 -----------------
1268
1269 -- | @lintValApp arg fun_ty arg_ty@ lints an application of @fun arg@
1270 -- where @fun :: fun_ty@ and @arg :: arg_ty@, returning the type of the
1271 -- application.
1272 lintValApp :: CoreExpr -> LintedType -> LintedType -> UsageEnv -> UsageEnv -> LintM (LintedType, UsageEnv)
1273 lintValApp arg fun_ty arg_ty fun_ue arg_ue
1274 | Just (w, arg_ty', res_ty') <- splitFunTy_maybe fun_ty
1275 = do { ensureEqTys arg_ty' arg_ty err1
1276 ; let app_ue = addUE fun_ue (scaleUE w arg_ue)
1277 ; return (res_ty', app_ue) }
1278 | otherwise
1279 = failWithL err2
1280 where
1281 err1 = mkAppMsg fun_ty arg_ty arg
1282 err2 = mkNonFunAppMsg fun_ty arg_ty arg
1283
1284 lintTyKind :: OutTyVar -> LintedType -> LintM ()
1285 -- Both args have had substitution applied
1286
1287 -- If you edit this function, you may need to update the GHC formalism
1288 -- See Note [GHC Formalism]
1289 lintTyKind tyvar arg_ty
1290 = unless (arg_kind `eqType` tyvar_kind) $
1291 addErrL (mkKindErrMsg tyvar arg_ty $$ (text "Linted Arg kind:" <+> ppr arg_kind))
1292 where
1293 tyvar_kind = tyVarKind tyvar
1294 arg_kind = typeKind arg_ty
1295
1296 {-
1297 ************************************************************************
1298 * *
1299 \subsection[lintCoreAlts]{lintCoreAlts}
1300 * *
1301 ************************************************************************
1302 -}
1303
1304 lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM (LintedType, UsageEnv)
1305 lintCaseExpr scrut var alt_ty alts =
1306 do { let e = Case scrut var alt_ty alts -- Just for error messages
1307
1308 -- Check the scrutinee
1309 ; (scrut_ty, scrut_ue) <- markAllJoinsBad $ lintCoreExpr scrut
1310 -- See Note [Join points are less general than the paper]
1311 -- in GHC.Core
1312 ; let scrut_mult = varMult var
1313
1314 ; alt_ty <- addLoc (CaseTy scrut) $
1315 lintValueType alt_ty
1316 ; var_ty <- addLoc (IdTy var) $
1317 lintValueType (idType var)
1318
1319 -- We used to try to check whether a case expression with no
1320 -- alternatives was legitimate, but this didn't work.
1321 -- See Note [No alternatives lint check] for details.
1322
1323 -- Check that the scrutinee is not a floating-point type
1324 -- if there are any literal alternatives
1325 -- See GHC.Core Note [Case expression invariants] item (5)
1326 -- See Note [Rules for floating-point comparisons] in GHC.Core.Opt.ConstantFold
1327 ; let isLitPat (Alt (LitAlt _) _ _) = True
1328 isLitPat _ = False
1329 ; checkL (not $ isFloatingTy scrut_ty && any isLitPat alts)
1330 (text "Lint warning: Scrutinising floating-point expression with literal pattern in case analysis (see #9238)."
1331 $$ text "scrut" <+> ppr scrut)
1332
1333 ; case tyConAppTyCon_maybe (idType var) of
1334 Just tycon
1335 | debugIsOn
1336 , isAlgTyCon tycon
1337 , not (isAbstractTyCon tycon)
1338 , null (tyConDataCons tycon)
1339 , not (exprIsDeadEnd scrut)
1340 -> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
1341 -- This can legitimately happen for type families
1342 $ return ()
1343 _otherwise -> return ()
1344
1345 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
1346
1347 ; subst <- getTCvSubst
1348 ; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
1349 -- See GHC.Core Note [Case expression invariants] item (7)
1350
1351 ; lintBinder CaseBind var $ \_ ->
1352 do { -- Check the alternatives
1353 ; alt_ues <- mapM (lintCoreAlt var scrut_ty scrut_mult alt_ty) alts
1354 ; let case_ue = (scaleUE scrut_mult scrut_ue) `addUE` supUEs alt_ues
1355 ; checkCaseAlts e scrut_ty alts
1356 ; return (alt_ty, case_ue) } }
1357
1358 checkCaseAlts :: CoreExpr -> LintedType -> [CoreAlt] -> LintM ()
1359 -- a) Check that the alts are non-empty
1360 -- b1) Check that the DEFAULT comes first, if it exists
1361 -- b2) Check that the others are in increasing order
1362 -- c) Check that there's a default for infinite types
1363 -- NB: Algebraic cases are not necessarily exhaustive, because
1364 -- the simplifier correctly eliminates case that can't
1365 -- possibly match.
1366
1367 checkCaseAlts e ty alts =
1368 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
1369 -- See GHC.Core Note [Case expression invariants] item (2)
1370
1371 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
1372 -- See GHC.Core Note [Case expression invariants] item (3)
1373
1374 -- For types Int#, Word# with an infinite (well, large!) number of
1375 -- possible values, there should usually be a DEFAULT case
1376 -- But (see Note [Empty case alternatives] in GHC.Core) it's ok to
1377 -- have *no* case alternatives.
1378 -- In effect, this is a kind of partial test. I suppose it's possible
1379 -- that we might *know* that 'x' was 1 or 2, in which case
1380 -- case x of { 1 -> e1; 2 -> e2 }
1381 -- would be fine.
1382 ; checkL (isJust maybe_deflt || not is_infinite_ty || null alts)
1383 (nonExhaustiveAltsMsg e) }
1384 where
1385 (con_alts, maybe_deflt) = findDefault alts
1386
1387 -- Check that successive alternatives have strictly increasing tags
1388 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
1389 increasing_tag _ = True
1390
1391 non_deflt (Alt DEFAULT _ _) = False
1392 non_deflt _ = True
1393
1394 is_infinite_ty = case tyConAppTyCon_maybe ty of
1395 Nothing -> False
1396 Just tycon -> isPrimTyCon tycon
1397
1398 lintAltExpr :: CoreExpr -> LintedType -> LintM UsageEnv
1399 lintAltExpr expr ann_ty
1400 = do { (actual_ty, ue) <- lintCoreExpr expr
1401 ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty)
1402 ; return ue }
1403 -- See GHC.Core Note [Case expression invariants] item (6)
1404
1405 lintCoreAlt :: Var -- Case binder
1406 -> LintedType -- Type of scrutinee
1407 -> Mult -- Multiplicity of scrutinee
1408 -> LintedType -- Type of the alternative
1409 -> CoreAlt
1410 -> LintM UsageEnv
1411 -- If you edit this function, you may need to update the GHC formalism
1412 -- See Note [GHC Formalism]
1413 lintCoreAlt _ _ _ alt_ty (Alt DEFAULT args rhs) =
1414 do { lintL (null args) (mkDefaultArgsMsg args)
1415 ; lintAltExpr rhs alt_ty }
1416
1417 lintCoreAlt _case_bndr scrut_ty _ alt_ty (Alt (LitAlt lit) args rhs)
1418 | litIsLifted lit
1419 = failWithL integerScrutinisedMsg
1420 | otherwise
1421 = do { lintL (null args) (mkDefaultArgsMsg args)
1422 ; ensureEqTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
1423 ; lintAltExpr rhs alt_ty }
1424 where
1425 lit_ty = literalType lit
1426
1427 lintCoreAlt case_bndr scrut_ty _scrut_mult alt_ty alt@(Alt (DataAlt con) args rhs)
1428 | isNewTyCon (dataConTyCon con)
1429 = zeroUE <$ addErrL (mkNewTyDataConAltMsg scrut_ty alt)
1430 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
1431 = addLoc (CaseAlt alt) $ do
1432 { -- First instantiate the universally quantified
1433 -- type variables of the data constructor
1434 -- We've already check
1435 lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
1436 ; let { con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys
1437 ; binderMult (Named _) = Many
1438 ; binderMult (Anon _ st) = scaledMult st
1439 -- See Note [Validating multiplicities in a case]
1440 ; multiplicities = map binderMult $ fst $ splitPiTys con_payload_ty }
1441
1442 -- And now bring the new binders into scope
1443 ; lintBinders CasePatBind args $ \ args' -> do
1444 {
1445 rhs_ue <- lintAltExpr rhs alt_ty
1446 ; rhs_ue' <- addLoc (CasePat alt) (lintAltBinders rhs_ue case_bndr scrut_ty con_payload_ty (zipEqual "lintCoreAlt" multiplicities args'))
1447 ; return $ deleteUE rhs_ue' case_bndr
1448 }
1449 }
1450
1451 | otherwise -- Scrut-ty is wrong shape
1452 = zeroUE <$ addErrL (mkBadAltMsg scrut_ty alt)
1453
1454 {-
1455 Note [Validating multiplicities in a case]
1456 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1457 Suppose 'MkT :: a %m -> T m a'.
1458 If we are validating 'case (x :: T Many a) of MkT y -> ...',
1459 we have to substitute m := Many in the type of MkT - in particular,
1460 y can be used Many times and that expression would still be linear in x.
1461 We do this by looking at con_payload_ty, which is the type of the datacon
1462 applied to the surrounding arguments.
1463 Testcase: linear/should_compile/MultConstructor
1464
1465 Data constructors containing existential tyvars will then have
1466 Named binders, which are always multiplicity Many.
1467 Testcase: indexed-types/should_compile/GADT1
1468 -}
1469
1470 lintLinearBinder :: SDoc -> Mult -> Mult -> LintM ()
1471 lintLinearBinder doc actual_usage described_usage
1472 = ensureSubMult actual_usage described_usage err_msg
1473 where
1474 err_msg = (text "Multiplicity of variable does not agree with its context"
1475 $$ doc
1476 $$ ppr actual_usage
1477 $$ text "Annotation:" <+> ppr described_usage)
1478
1479 {-
1480 ************************************************************************
1481 * *
1482 \subsection[lint-types]{Types}
1483 * *
1484 ************************************************************************
1485 -}
1486
1487 -- When we lint binders, we (one at a time and in order):
1488 -- 1. Lint var types or kinds (possibly substituting)
1489 -- 2. Add the binder to the in scope set, and if its a coercion var,
1490 -- we may extend the substitution to reflect its (possibly) new kind
1491 lintBinders :: BindingSite -> [Var] -> ([Var] -> LintM a) -> LintM a
1492 lintBinders _ [] linterF = linterF []
1493 lintBinders site (var:vars) linterF = lintBinder site var $ \var' ->
1494 lintBinders site vars $ \ vars' ->
1495 linterF (var':vars')
1496
1497 -- If you edit this function, you may need to update the GHC formalism
1498 -- See Note [GHC Formalism]
1499 lintBinder :: BindingSite -> Var -> (Var -> LintM a) -> LintM a
1500 lintBinder site var linterF
1501 | isTyCoVar var = lintTyCoBndr var linterF
1502 | otherwise = lintIdBndr NotTopLevel site var linterF
1503
1504 lintTyBndr :: TyVar -> (LintedTyCoVar -> LintM a) -> LintM a
1505 lintTyBndr = lintTyCoBndr -- We could specialise it, I guess
1506
1507 -- lintCoBndr :: CoVar -> (LintedTyCoVar -> LintM a) -> LintM a
1508 -- lintCoBndr = lintTyCoBndr -- We could specialise it, I guess
1509
1510 lintTyCoBndr :: TyCoVar -> (LintedTyCoVar -> LintM a) -> LintM a
1511 lintTyCoBndr tcv thing_inside
1512 = do { subst <- getTCvSubst
1513 ; kind' <- lintType (varType tcv)
1514 ; let tcv' = uniqAway (getTCvInScope subst) $
1515 setVarType tcv kind'
1516 subst' = extendTCvSubstWithClone subst tcv tcv'
1517 ; when (isCoVar tcv) $
1518 lintL (isCoVarType kind')
1519 (text "CoVar with non-coercion type:" <+> pprTyVar tcv)
1520 ; updateTCvSubst subst' (thing_inside tcv') }
1521
1522 lintIdBndrs :: forall a. TopLevelFlag -> [Id] -> ([LintedId] -> LintM a) -> LintM a
1523 lintIdBndrs top_lvl ids thing_inside
1524 = go ids thing_inside
1525 where
1526 go :: [Id] -> ([Id] -> LintM a) -> LintM a
1527 go [] thing_inside = thing_inside []
1528 go (id:ids) thing_inside = lintIdBndr top_lvl LetBind id $ \id' ->
1529 go ids $ \ids' ->
1530 thing_inside (id' : ids')
1531
1532 lintIdBndr :: TopLevelFlag -> BindingSite
1533 -> InVar -> (OutVar -> LintM a) -> LintM a
1534 -- Do substitution on the type of a binder and add the var with this
1535 -- new type to the in-scope set of the second argument
1536 -- ToDo: lint its rules
1537 lintIdBndr top_lvl bind_site id thing_inside
1538 = assertPpr (isId id) (ppr id) $
1539 do { flags <- getLintFlags
1540 ; checkL (not (lf_check_global_ids flags) || isLocalId id)
1541 (text "Non-local Id binder" <+> ppr id)
1542 -- See Note [Checking for global Ids]
1543
1544 -- Check that if the binder is nested, it is not marked as exported
1545 ; checkL (not (isExportedId id) || is_top_lvl)
1546 (mkNonTopExportedMsg id)
1547
1548 -- Check that if the binder is nested, it does not have an external name
1549 ; checkL (not (isExternalName (Var.varName id)) || is_top_lvl)
1550 (mkNonTopExternalNameMsg id)
1551
1552 -- See Note [Representation polymorphism invariants] in GHC.Core
1553 ; lintL (isJoinId id || not (lf_check_fixed_rep flags)
1554 || typeHasFixedRuntimeRep id_ty) $
1555 text "Binder does not have a fixed runtime representation:" <+> ppr id <+> dcolon <+>
1556 parens (ppr id_ty <+> dcolon <+> ppr (typeKind id_ty))
1557
1558 -- Check that a join-id is a not-top-level let-binding
1559 ; when (isJoinId id) $
1560 checkL (not is_top_lvl && is_let_bind) $
1561 mkBadJoinBindMsg id
1562
1563 -- Check that the Id does not have type (t1 ~# t2) or (t1 ~R# t2);
1564 -- if so, it should be a CoVar, and checked by lintCoVarBndr
1565 ; lintL (not (isCoVarType id_ty))
1566 (text "Non-CoVar has coercion type" <+> ppr id <+> dcolon <+> ppr id_ty)
1567
1568 ; linted_ty <- addLoc (IdTy id) (lintValueType id_ty)
1569
1570 ; addInScopeId id linted_ty $
1571 thing_inside (setIdType id linted_ty) }
1572 where
1573 id_ty = idType id
1574
1575 is_top_lvl = isTopLevel top_lvl
1576 is_let_bind = case bind_site of
1577 LetBind -> True
1578 _ -> False
1579
1580 {-
1581 %************************************************************************
1582 %* *
1583 Types
1584 %* *
1585 %************************************************************************
1586 -}
1587
1588 lintValueType :: Type -> LintM LintedType
1589 -- Types only, not kinds
1590 -- Check the type, and apply the substitution to it
1591 -- See Note [Linting type lets]
1592 lintValueType ty
1593 = addLoc (InType ty) $
1594 do { ty' <- lintType ty
1595 ; let sk = typeKind ty'
1596 ; lintL (classifiesTypeWithValues sk) $
1597 hang (text "Ill-kinded type:" <+> ppr ty)
1598 2 (text "has kind:" <+> ppr sk)
1599 ; return ty' }
1600
1601 checkTyCon :: TyCon -> LintM ()
1602 checkTyCon tc
1603 = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
1604
1605 -------------------
1606 lintType :: Type -> LintM LintedType
1607
1608 -- If you edit this function, you may need to update the GHC formalism
1609 -- See Note [GHC Formalism]
1610 lintType (TyVarTy tv)
1611 | not (isTyVar tv)
1612 = failWithL (mkBadTyVarMsg tv)
1613
1614 | otherwise
1615 = do { subst <- getTCvSubst
1616 ; case lookupTyVar subst tv of
1617 Just linted_ty -> return linted_ty
1618
1619 -- In GHCi we may lint an expression with a free
1620 -- type variable. Then it won't be in the
1621 -- substitution, but it should be in scope
1622 Nothing | tv `isInScope` subst
1623 -> return (TyVarTy tv)
1624 | otherwise
1625 -> failWithL $
1626 hang (text "The type variable" <+> pprBndr LetBind tv)
1627 2 (text "is out of scope")
1628 }
1629
1630 lintType ty@(AppTy t1 t2)
1631 | TyConApp {} <- t1
1632 = failWithL $ text "TyConApp to the left of AppTy:" <+> ppr ty
1633 | otherwise
1634 = do { t1' <- lintType t1
1635 ; t2' <- lintType t2
1636 ; lint_ty_app ty (typeKind t1') [t2']
1637 ; return (AppTy t1' t2') }
1638
1639 lintType ty@(TyConApp tc tys)
1640 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
1641 = do { report_unsat <- lf_report_unsat_syns <$> getLintFlags
1642 ; lintTySynFamApp report_unsat ty tc tys }
1643
1644 | isFunTyCon tc
1645 , tys `lengthIs` 5
1646 -- We should never see a saturated application of funTyCon; such
1647 -- applications should be represented with the FunTy constructor.
1648 -- See Note [Linting function types] and
1649 -- Note [Representation of function types].
1650 = failWithL (hang (text "Saturated application of (->)") 2 (ppr ty))
1651
1652 | otherwise -- Data types, data families, primitive types
1653 = do { checkTyCon tc
1654 ; tys' <- mapM lintType tys
1655 ; lint_ty_app ty (tyConKind tc) tys'
1656 ; return (TyConApp tc tys') }
1657
1658 -- arrows can related *unlifted* kinds, so this has to be separate from
1659 -- a dependent forall.
1660 lintType ty@(FunTy af tw t1 t2)
1661 = do { t1' <- lintType t1
1662 ; t2' <- lintType t2
1663 ; tw' <- lintType tw
1664 ; lintArrow (text "type or kind" <+> quotes (ppr ty)) t1' t2' tw'
1665 ; return (FunTy af tw' t1' t2') }
1666
1667 lintType ty@(ForAllTy (Bndr tcv vis) body_ty)
1668 | not (isTyCoVar tcv)
1669 = failWithL (text "Non-Tyvar or Non-Covar bound in type:" <+> ppr ty)
1670 | otherwise
1671 = lintTyCoBndr tcv $ \tcv' ->
1672 do { body_ty' <- lintType body_ty
1673 ; lintForAllBody tcv' body_ty'
1674
1675 ; when (isCoVar tcv) $
1676 lintL (tcv `elemVarSet` tyCoVarsOfType body_ty) $
1677 text "Covar does not occur in the body:" <+> (ppr tcv $$ ppr body_ty)
1678 -- See GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy]
1679 -- and cf GHC.Core.Coercion Note [Unused coercion variable in ForAllCo]
1680
1681 ; return (ForAllTy (Bndr tcv' vis) body_ty') }
1682
1683 lintType ty@(LitTy l)
1684 = do { lintTyLit l; return ty }
1685
1686 lintType (CastTy ty co)
1687 = do { ty' <- lintType ty
1688 ; co' <- lintStarCoercion co
1689 ; let tyk = typeKind ty'
1690 cok = coercionLKind co'
1691 ; ensureEqTys tyk cok (mkCastTyErr ty co tyk cok)
1692 ; return (CastTy ty' co') }
1693
1694 lintType (CoercionTy co)
1695 = do { co' <- lintCoercion co
1696 ; return (CoercionTy co') }
1697
1698 -----------------
1699 lintForAllBody :: LintedTyCoVar -> LintedType -> LintM ()
1700 -- Do the checks for the body of a forall-type
1701 lintForAllBody tcv body_ty
1702 = do { checkValueType body_ty (text "the body of forall:" <+> ppr body_ty)
1703
1704 -- For type variables, check for skolem escape
1705 -- See Note [Phantom type variables in kinds] in GHC.Core.Type
1706 -- The kind of (forall cv. th) is liftedTypeKind, so no
1707 -- need to check for skolem-escape in the CoVar case
1708 ; let body_kind = typeKind body_ty
1709 ; when (isTyVar tcv) $
1710 case occCheckExpand [tcv] body_kind of
1711 Just {} -> return ()
1712 Nothing -> failWithL $
1713 hang (text "Variable escape in forall:")
1714 2 (vcat [ text "tyvar:" <+> ppr tcv
1715 , text "type:" <+> ppr body_ty
1716 , text "kind:" <+> ppr body_kind ])
1717 }
1718
1719 -----------------
1720 lintTySynFamApp :: Bool -> InType -> TyCon -> [InType] -> LintM LintedType
1721 -- The TyCon is a type synonym or a type family (not a data family)
1722 -- See Note [Linting type synonym applications]
1723 -- c.f. GHC.Tc.Validity.check_syn_tc_app
1724 lintTySynFamApp report_unsat ty tc tys
1725 | report_unsat -- Report unsaturated only if report_unsat is on
1726 , tys `lengthLessThan` tyConArity tc
1727 = failWithL (hang (text "Un-saturated type application") 2 (ppr ty))
1728
1729 -- Deal with type synonyms
1730 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
1731 , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
1732 = do { -- Kind-check the argument types, but without reporting
1733 -- un-saturated type families/synonyms
1734 tys' <- setReportUnsat False (mapM lintType tys)
1735
1736 ; when report_unsat $
1737 do { _ <- lintType expanded_ty
1738 ; return () }
1739
1740 ; lint_ty_app ty (tyConKind tc) tys'
1741 ; return (TyConApp tc tys') }
1742
1743 -- Otherwise this must be a type family
1744 | otherwise
1745 = do { tys' <- mapM lintType tys
1746 ; lint_ty_app ty (tyConKind tc) tys'
1747 ; return (TyConApp tc tys') }
1748
1749 -----------------
1750 -- Confirms that a type is really TYPE r or Constraint
1751 checkValueType :: LintedType -> SDoc -> LintM ()
1752 checkValueType ty doc
1753 = lintL (classifiesTypeWithValues kind)
1754 (text "Non-Type-like kind when Type-like expected:" <+> ppr kind $$
1755 text "when checking" <+> doc)
1756 where
1757 kind = typeKind ty
1758
1759 -----------------
1760 lintArrow :: SDoc -> LintedType -> LintedType -> LintedType -> LintM ()
1761 -- If you edit this function, you may need to update the GHC formalism
1762 -- See Note [GHC Formalism]
1763 lintArrow what t1 t2 tw -- Eg lintArrow "type or kind `blah'" k1 k2 kw
1764 -- or lintArrow "coercion `blah'" k1 k2 kw
1765 = do { unless (classifiesTypeWithValues k1) (addErrL (msg (text "argument") k1))
1766 ; unless (classifiesTypeWithValues k2) (addErrL (msg (text "result") k2))
1767 ; unless (isMultiplicityTy kw) (addErrL (msg (text "multiplicity") kw)) }
1768 where
1769 k1 = typeKind t1
1770 k2 = typeKind t2
1771 kw = typeKind tw
1772 msg ar k
1773 = vcat [ hang (text "Ill-kinded" <+> ar)
1774 2 (text "in" <+> what)
1775 , what <+> text "kind:" <+> ppr k ]
1776
1777 -----------------
1778 lint_ty_app :: Type -> LintedKind -> [LintedType] -> LintM ()
1779 lint_ty_app ty k tys
1780 = lint_app (text "type" <+> quotes (ppr ty)) k tys
1781
1782 ----------------
1783 lint_co_app :: Coercion -> LintedKind -> [LintedType] -> LintM ()
1784 lint_co_app ty k tys
1785 = lint_app (text "coercion" <+> quotes (ppr ty)) k tys
1786
1787 ----------------
1788 lintTyLit :: TyLit -> LintM ()
1789 lintTyLit (NumTyLit n)
1790 | n >= 0 = return ()
1791 | otherwise = failWithL msg
1792 where msg = text "Negative type literal:" <+> integer n
1793 lintTyLit (StrTyLit _) = return ()
1794 lintTyLit (CharTyLit _) = return ()
1795
1796 lint_app :: SDoc -> LintedKind -> [LintedType] -> LintM ()
1797 -- (lint_app d fun_kind arg_tys)
1798 -- We have an application (f arg_ty1 .. arg_tyn),
1799 -- where f :: fun_kind
1800
1801 -- If you edit this function, you may need to update the GHC formalism
1802 -- See Note [GHC Formalism]
1803 lint_app doc kfn arg_tys
1804 = do { in_scope <- getInScope
1805 -- We need the in_scope set to satisfy the invariant in
1806 -- Note [The substitution invariant] in GHC.Core.TyCo.Subst
1807 ; _ <- foldlM (go_app in_scope) kfn arg_tys
1808 ; return () }
1809 where
1810 fail_msg extra = vcat [ hang (text "Kind application error in") 2 doc
1811 , nest 2 (text "Function kind =" <+> ppr kfn)
1812 , nest 2 (text "Arg types =" <+> ppr arg_tys)
1813 , extra ]
1814
1815 go_app in_scope kfn ta
1816 | Just kfn' <- coreView kfn
1817 = go_app in_scope kfn' ta
1818
1819 go_app _ fun_kind@(FunTy _ _ kfa kfb) ta
1820 = do { let ka = typeKind ta
1821 ; unless (ka `eqType` kfa) $
1822 addErrL (fail_msg (text "Fun:" <+> (ppr fun_kind $$ ppr ta <+> dcolon <+> ppr ka)))
1823 ; return kfb }
1824
1825 go_app in_scope (ForAllTy (Bndr kv _vis) kfn) ta
1826 = do { let kv_kind = varType kv
1827 ka = typeKind ta
1828 ; unless (ka `eqType` kv_kind) $
1829 addErrL (fail_msg (text "Forall:" <+> (ppr kv $$ ppr kv_kind $$
1830 ppr ta <+> dcolon <+> ppr ka)))
1831 ; return $ substTy (extendTCvSubst (mkEmptyTCvSubst in_scope) kv ta) kfn }
1832
1833 go_app _ kfn ta
1834 = failWithL (fail_msg (text "Not a fun:" <+> (ppr kfn $$ ppr ta)))
1835
1836 {- *********************************************************************
1837 * *
1838 Linting rules
1839 * *
1840 ********************************************************************* -}
1841
1842 lintCoreRule :: OutVar -> LintedType -> CoreRule -> LintM ()
1843 lintCoreRule _ _ (BuiltinRule {})
1844 = return () -- Don't bother
1845
1846 lintCoreRule fun fun_ty rule@(Rule { ru_name = name, ru_bndrs = bndrs
1847 , ru_args = args, ru_rhs = rhs })
1848 = lintBinders LambdaBind bndrs $ \ _ ->
1849 do { (lhs_ty, _) <- lintCoreArgs (fun_ty, zeroUE) args
1850 ; (rhs_ty, _) <- case isJoinId_maybe fun of
1851 Just join_arity
1852 -> do { checkL (args `lengthIs` join_arity) $
1853 mkBadJoinPointRuleMsg fun join_arity rule
1854 -- See Note [Rules for join points]
1855 ; lintCoreExpr rhs }
1856 _ -> markAllJoinsBad $ lintCoreExpr rhs
1857 ; ensureEqTys lhs_ty rhs_ty $
1858 (rule_doc <+> vcat [ text "lhs type:" <+> ppr lhs_ty
1859 , text "rhs type:" <+> ppr rhs_ty
1860 , text "fun_ty:" <+> ppr fun_ty ])
1861 ; let bad_bndrs = filter is_bad_bndr bndrs
1862
1863 ; checkL (null bad_bndrs)
1864 (rule_doc <+> text "unbound" <+> ppr bad_bndrs)
1865 -- See Note [Linting rules]
1866 }
1867 where
1868 rule_doc = text "Rule" <+> doubleQuotes (ftext name) <> colon
1869
1870 lhs_fvs = exprsFreeVars args
1871 rhs_fvs = exprFreeVars rhs
1872
1873 is_bad_bndr :: Var -> Bool
1874 -- See Note [Unbound RULE binders] in GHC.Core.Rules
1875 is_bad_bndr bndr = not (bndr `elemVarSet` lhs_fvs)
1876 && bndr `elemVarSet` rhs_fvs
1877 && isNothing (isReflCoVar_maybe bndr)
1878
1879
1880 {- Note [Linting rules]
1881 ~~~~~~~~~~~~~~~~~~~~~~~
1882 It's very bad if simplifying a rule means that one of the template
1883 variables (ru_bndrs) that /is/ mentioned on the RHS becomes
1884 not-mentioned in the LHS (ru_args). How can that happen? Well, in #10602,
1885 SpecConstr stupidly constructed a rule like
1886
1887 forall x,c1,c2.
1888 f (x |> c1 |> c2) = ....
1889
1890 But simplExpr collapses those coercions into one. (Indeed in #10602,
1891 it collapsed to the identity and was removed altogether.)
1892
1893 We don't have a great story for what to do here, but at least
1894 this check will nail it.
1895
1896 NB (#11643): it's possible that a variable listed in the
1897 binders becomes not-mentioned on both LHS and RHS. Here's a silly
1898 example:
1899 RULE forall x y. f (g x y) = g (x+1) (y-1)
1900 And suppose worker/wrapper decides that 'x' is Absent. Then
1901 we'll end up with
1902 RULE forall x y. f ($gw y) = $gw (x+1)
1903 This seems sufficiently obscure that there isn't enough payoff to
1904 try to trim the forall'd binder list.
1905
1906 Note [Rules for join points]
1907 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1908
1909 A join point cannot be partially applied. However, the left-hand side of a rule
1910 for a join point is effectively a *pattern*, not a piece of code, so there's an
1911 argument to be made for allowing a situation like this:
1912
1913 join $sj :: Int -> Int -> String
1914 $sj n m = ...
1915 j :: forall a. Eq a => a -> a -> String
1916 {-# RULES "SPEC j" jump j @ Int $dEq = jump $sj #-}
1917 j @a $dEq x y = ...
1918
1919 Applying this rule can't turn a well-typed program into an ill-typed one, so
1920 conceivably we could allow it. But we can always eta-expand such an
1921 "undersaturated" rule (see 'GHC.Core.Opt.Arity.etaExpandToJoinPointRule'), and in fact
1922 the simplifier would have to in order to deal with the RHS. So we take a
1923 conservative view and don't allow undersaturated rules for join points. See
1924 Note [Rules and join points] in "GHC.Core.Opt.OccurAnal" for further discussion.
1925 -}
1926
1927 {-
1928 ************************************************************************
1929 * *
1930 Linting coercions
1931 * *
1932 ************************************************************************
1933 -}
1934
1935 {- Note [Asymptotic efficiency]
1936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1937 When linting coercions (and types actually) we return a linted
1938 (substituted) coercion. Then we often have to take the coercionKind of
1939 that returned coercion. If we get long chains, that can be asymptotically
1940 inefficient, notably in
1941 * TransCo
1942 * InstCo
1943 * NthCo (cf #9233)
1944 * LRCo
1945
1946 But the code is simple. And this is only Lint. Let's wait to see if
1947 the bad perf bites us in practice.
1948
1949 A solution would be to return the kind and role of the coercion,
1950 as well as the linted coercion. Or perhaps even *only* the kind and role,
1951 which is what used to happen. But that proved tricky and error prone
1952 (#17923), so now we return the coercion.
1953 -}
1954
1955
1956 -- lints a coercion, confirming that its lh kind and its rh kind are both *
1957 -- also ensures that the role is Nominal
1958 lintStarCoercion :: InCoercion -> LintM LintedCoercion
1959 lintStarCoercion g
1960 = do { g' <- lintCoercion g
1961 ; let Pair t1 t2 = coercionKind g'
1962 ; checkValueType t1 (text "the kind of the left type in" <+> ppr g)
1963 ; checkValueType t2 (text "the kind of the right type in" <+> ppr g)
1964 ; lintRole g Nominal (coercionRole g)
1965 ; return g' }
1966
1967 lintCoercion :: InCoercion -> LintM LintedCoercion
1968 -- If you edit this function, you may need to update the GHC formalism
1969 -- See Note [GHC Formalism]
1970
1971 lintCoercion (CoVarCo cv)
1972 | not (isCoVar cv)
1973 = failWithL (hang (text "Bad CoVarCo:" <+> ppr cv)
1974 2 (text "With offending type:" <+> ppr (varType cv)))
1975
1976 | otherwise
1977 = do { subst <- getTCvSubst
1978 ; case lookupCoVar subst cv of
1979 Just linted_co -> return linted_co ;
1980 Nothing
1981 | cv `isInScope` subst
1982 -> return (CoVarCo cv)
1983 | otherwise
1984 ->
1985 -- lintCoBndr always extends the substitition
1986 failWithL $
1987 hang (text "The coercion variable" <+> pprBndr LetBind cv)
1988 2 (text "is out of scope")
1989 }
1990
1991
1992 lintCoercion (Refl ty)
1993 = do { ty' <- lintType ty
1994 ; return (Refl ty') }
1995
1996 lintCoercion (GRefl r ty MRefl)
1997 = do { ty' <- lintType ty
1998 ; return (GRefl r ty' MRefl) }
1999
2000 lintCoercion (GRefl r ty (MCo co))
2001 = do { ty' <- lintType ty
2002 ; co' <- lintCoercion co
2003 ; let tk = typeKind ty'
2004 tl = coercionLKind co'
2005 ; ensureEqTys tk tl $
2006 hang (text "GRefl coercion kind mis-match:" <+> ppr co)
2007 2 (vcat [ppr ty', ppr tk, ppr tl])
2008 ; lintRole co' Nominal (coercionRole co')
2009 ; return (GRefl r ty' (MCo co')) }
2010
2011 lintCoercion co@(TyConAppCo r tc cos)
2012 | tc `hasKey` funTyConKey
2013 , [_w, _rep1,_rep2,_co1,_co2] <- cos
2014 = failWithL (text "Saturated TyConAppCo (->):" <+> ppr co)
2015 -- All saturated TyConAppCos should be FunCos
2016
2017 | Just {} <- synTyConDefn_maybe tc
2018 = failWithL (text "Synonym in TyConAppCo:" <+> ppr co)
2019
2020 | otherwise
2021 = do { checkTyCon tc
2022 ; cos' <- mapM lintCoercion cos
2023 ; let (co_kinds, co_roles) = unzip (map coercionKindRole cos')
2024 ; lint_co_app co (tyConKind tc) (map pFst co_kinds)
2025 ; lint_co_app co (tyConKind tc) (map pSnd co_kinds)
2026 ; zipWithM_ (lintRole co) (tyConRolesX r tc) co_roles
2027 ; return (TyConAppCo r tc cos') }
2028
2029 lintCoercion co@(AppCo co1 co2)
2030 | TyConAppCo {} <- co1
2031 = failWithL (text "TyConAppCo to the left of AppCo:" <+> ppr co)
2032 | Just (TyConApp {}, _) <- isReflCo_maybe co1
2033 = failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co)
2034 | otherwise
2035 = do { co1' <- lintCoercion co1
2036 ; co2' <- lintCoercion co2
2037 ; let (Pair lk1 rk1, r1) = coercionKindRole co1'
2038 (Pair lk2 rk2, r2) = coercionKindRole co2'
2039 ; lint_co_app co (typeKind lk1) [lk2]
2040 ; lint_co_app co (typeKind rk1) [rk2]
2041
2042 ; if r1 == Phantom
2043 then lintL (r2 == Phantom || r2 == Nominal)
2044 (text "Second argument in AppCo cannot be R:" $$
2045 ppr co)
2046 else lintRole co Nominal r2
2047
2048 ; return (AppCo co1' co2') }
2049
2050 ----------
2051 lintCoercion co@(ForAllCo tcv kind_co body_co)
2052 | not (isTyCoVar tcv)
2053 = failWithL (text "Non tyco binder in ForAllCo:" <+> ppr co)
2054 | otherwise
2055 = do { kind_co' <- lintStarCoercion kind_co
2056 ; lintTyCoBndr tcv $ \tcv' ->
2057 do { body_co' <- lintCoercion body_co
2058 ; ensureEqTys (varType tcv') (coercionLKind kind_co') $
2059 text "Kind mis-match in ForallCo" <+> ppr co
2060
2061 -- Assuming kind_co :: k1 ~ k2
2062 -- Need to check that
2063 -- (forall (tcv:k1). lty) and
2064 -- (forall (tcv:k2). rty[(tcv:k2) |> sym kind_co/tcv])
2065 -- are both well formed. Easiest way is to call lintForAllBody
2066 -- for each; there is actually no need to do the funky substitution
2067 ; let Pair lty rty = coercionKind body_co'
2068 ; lintForAllBody tcv' lty
2069 ; lintForAllBody tcv' rty
2070
2071 ; when (isCoVar tcv) $
2072 lintL (almostDevoidCoVarOfCo tcv body_co) $
2073 text "Covar can only appear in Refl and GRefl: " <+> ppr co
2074 -- See "last wrinkle" in GHC.Core.Coercion
2075 -- Note [Unused coercion variable in ForAllCo]
2076 -- and c.f. GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy]
2077
2078 ; return (ForAllCo tcv' kind_co' body_co') } }
2079
2080 lintCoercion co@(FunCo r cow co1 co2)
2081 = do { co1' <- lintCoercion co1
2082 ; co2' <- lintCoercion co2
2083 ; cow' <- lintCoercion cow
2084 ; let Pair lt1 rt1 = coercionKind co1
2085 Pair lt2 rt2 = coercionKind co2
2086 Pair ltw rtw = coercionKind cow
2087 ; lintArrow (text "coercion" <+> quotes (ppr co)) lt1 lt2 ltw
2088 ; lintArrow (text "coercion" <+> quotes (ppr co)) rt1 rt2 rtw
2089 ; lintRole co1 r (coercionRole co1)
2090 ; lintRole co2 r (coercionRole co2)
2091 ; ensureEqTys (typeKind ltw) multiplicityTy (text "coercion" <> quotes (ppr co))
2092 ; ensureEqTys (typeKind rtw) multiplicityTy (text "coercion" <> quotes (ppr co))
2093 ; let expected_mult_role = case r of
2094 Phantom -> Phantom
2095 _ -> Nominal
2096 ; lintRole cow expected_mult_role (coercionRole cow)
2097 ; return (FunCo r cow' co1' co2') }
2098
2099 -- See Note [Bad unsafe coercion]
2100 lintCoercion co@(UnivCo prov r ty1 ty2)
2101 = do { ty1' <- lintType ty1
2102 ; ty2' <- lintType ty2
2103 ; let k1 = typeKind ty1'
2104 k2 = typeKind ty2'
2105 ; prov' <- lint_prov k1 k2 prov
2106
2107 ; when (r /= Phantom && classifiesTypeWithValues k1
2108 && classifiesTypeWithValues k2)
2109 (checkTypes ty1 ty2)
2110
2111 ; return (UnivCo prov' r ty1' ty2') }
2112 where
2113 report s = hang (text $ "Unsafe coercion: " ++ s)
2114 2 (vcat [ text "From:" <+> ppr ty1
2115 , text " To:" <+> ppr ty2])
2116 isUnBoxed :: PrimRep -> Bool
2117 isUnBoxed = not . isGcPtrRep
2118
2119 -- see #9122 for discussion of these checks
2120 checkTypes t1 t2
2121 | allow_ill_kinded_univ_co prov
2122 = return () -- Skip kind checks
2123 | otherwise
2124 = do { checkWarnL fixed_rep_1
2125 (report "left-hand type does not have a fixed runtime representation")
2126 ; checkWarnL fixed_rep_2
2127 (report "right-hand type does not have a fixed runtime representation")
2128 ; when (fixed_rep_1 && fixed_rep_2) $
2129 do { checkWarnL (reps1 `equalLength` reps2)
2130 (report "between values with different # of reps")
2131 ; zipWithM_ validateCoercion reps1 reps2 }}
2132 where
2133 fixed_rep_1 = typeHasFixedRuntimeRep t1
2134 fixed_rep_2 = typeHasFixedRuntimeRep t2
2135
2136 -- don't look at these unless lev_poly1/2 are False
2137 -- Otherwise, we get #13458
2138 reps1 = typePrimRep t1
2139 reps2 = typePrimRep t2
2140
2141 -- CorePrep deliberately makes ill-kinded casts
2142 -- e.g (case error @Int "blah" of {}) :: Int#
2143 -- ==> (error @Int "blah") |> Unsafe Int Int#
2144 -- See Note [Unsafe coercions] in GHC.Core.CoreToStg.Prep
2145 allow_ill_kinded_univ_co (CorePrepProv homo_kind) = not homo_kind
2146 allow_ill_kinded_univ_co _ = False
2147
2148 validateCoercion :: PrimRep -> PrimRep -> LintM ()
2149 validateCoercion rep1 rep2
2150 = do { platform <- targetPlatform <$> getDynFlags
2151 ; checkWarnL (isUnBoxed rep1 == isUnBoxed rep2)
2152 (report "between unboxed and boxed value")
2153 ; checkWarnL (TyCon.primRepSizeB platform rep1
2154 == TyCon.primRepSizeB platform rep2)
2155 (report "between unboxed values of different size")
2156 ; let fl = liftM2 (==) (TyCon.primRepIsFloat rep1)
2157 (TyCon.primRepIsFloat rep2)
2158 ; case fl of
2159 Nothing -> addWarnL (report "between vector types")
2160 Just False -> addWarnL (report "between float and integral values")
2161 _ -> return ()
2162 }
2163
2164 lint_prov k1 k2 (PhantomProv kco)
2165 = do { kco' <- lintStarCoercion kco
2166 ; lintRole co Phantom r
2167 ; check_kinds kco' k1 k2
2168 ; return (PhantomProv kco') }
2169
2170 lint_prov k1 k2 (ProofIrrelProv kco)
2171 = do { lintL (isCoercionTy ty1) (mkBadProofIrrelMsg ty1 co)
2172 ; lintL (isCoercionTy ty2) (mkBadProofIrrelMsg ty2 co)
2173 ; kco' <- lintStarCoercion kco
2174 ; check_kinds kco k1 k2
2175 ; return (ProofIrrelProv kco') }
2176
2177 lint_prov _ _ prov@(PluginProv _) = return prov
2178 lint_prov _ _ prov@(CorePrepProv _) = return prov
2179
2180 check_kinds kco k1 k2
2181 = do { let Pair k1' k2' = coercionKind kco
2182 ; ensureEqTys k1 k1' (mkBadUnivCoMsg CLeft co)
2183 ; ensureEqTys k2 k2' (mkBadUnivCoMsg CRight co) }
2184
2185
2186 lintCoercion (SymCo co)
2187 = do { co' <- lintCoercion co
2188 ; return (SymCo co') }
2189
2190 lintCoercion co@(TransCo co1 co2)
2191 = do { co1' <- lintCoercion co1
2192 ; co2' <- lintCoercion co2
2193 ; let ty1b = coercionRKind co1'
2194 ty2a = coercionLKind co2'
2195 ; ensureEqTys ty1b ty2a
2196 (hang (text "Trans coercion mis-match:" <+> ppr co)
2197 2 (vcat [ppr (coercionKind co1'), ppr (coercionKind co2')]))
2198 ; lintRole co (coercionRole co1) (coercionRole co2)
2199 ; return (TransCo co1' co2') }
2200
2201 lintCoercion the_co@(NthCo r0 n co)
2202 = do { co' <- lintCoercion co
2203 ; let (Pair s t, r) = coercionKindRole co'
2204 ; case (splitForAllTyCoVar_maybe s, splitForAllTyCoVar_maybe t) of
2205 { (Just _, Just _)
2206 -- works for both tyvar and covar
2207 | n == 0
2208 , (isForAllTy_ty s && isForAllTy_ty t)
2209 || (isForAllTy_co s && isForAllTy_co t)
2210 -> do { lintRole the_co Nominal r0
2211 ; return (NthCo r0 n co') }
2212
2213 ; _ -> case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
2214 { (Just (tc_s, tys_s), Just (tc_t, tys_t))
2215 | tc_s == tc_t
2216 , isInjectiveTyCon tc_s r
2217 -- see Note [NthCo and newtypes] in GHC.Core.TyCo.Rep
2218 , tys_s `equalLength` tys_t
2219 , tys_s `lengthExceeds` n
2220 -> do { lintRole the_co tr r0
2221 ; return (NthCo r0 n co') }
2222 where
2223 tr = nthRole r tc_s n
2224
2225 ; _ -> failWithL (hang (text "Bad getNth:")
2226 2 (ppr the_co $$ ppr s $$ ppr t)) }}}
2227
2228 lintCoercion the_co@(LRCo lr co)
2229 = do { co' <- lintCoercion co
2230 ; let Pair s t = coercionKind co'
2231 r = coercionRole co'
2232 ; lintRole co Nominal r
2233 ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
2234 (Just _, Just _) -> return (LRCo lr co')
2235 _ -> failWithL (hang (text "Bad LRCo:")
2236 2 (ppr the_co $$ ppr s $$ ppr t)) }
2237
2238 lintCoercion (InstCo co arg)
2239 = do { co' <- lintCoercion co
2240 ; arg' <- lintCoercion arg
2241 ; let Pair t1 t2 = coercionKind co'
2242 Pair s1 s2 = coercionKind arg'
2243
2244 ; lintRole arg Nominal (coercionRole arg')
2245
2246 ; case (splitForAllTyVar_maybe t1, splitForAllTyVar_maybe t2) of
2247 -- forall over tvar
2248 { (Just (tv1,_), Just (tv2,_))
2249 | typeKind s1 `eqType` tyVarKind tv1
2250 , typeKind s2 `eqType` tyVarKind tv2
2251 -> return (InstCo co' arg')
2252 | otherwise
2253 -> failWithL (text "Kind mis-match in inst coercion1" <+> ppr co)
2254
2255 ; _ -> case (splitForAllCoVar_maybe t1, splitForAllCoVar_maybe t2) of
2256 -- forall over covar
2257 { (Just (cv1, _), Just (cv2, _))
2258 | typeKind s1 `eqType` varType cv1
2259 , typeKind s2 `eqType` varType cv2
2260 , CoercionTy _ <- s1
2261 , CoercionTy _ <- s2
2262 -> return (InstCo co' arg')
2263 | otherwise
2264 -> failWithL (text "Kind mis-match in inst coercion2" <+> ppr co)
2265
2266 ; _ -> failWithL (text "Bad argument of inst") }}}
2267
2268 lintCoercion co@(AxiomInstCo con ind cos)
2269 = do { unless (0 <= ind && ind < numBranches (coAxiomBranches con))
2270 (bad_ax (text "index out of range"))
2271 ; let CoAxBranch { cab_tvs = ktvs
2272 , cab_cvs = cvs
2273 , cab_roles = roles } = coAxiomNthBranch con ind
2274 ; unless (cos `equalLength` (ktvs ++ cvs)) $
2275 bad_ax (text "lengths")
2276 ; cos' <- mapM lintCoercion cos
2277 ; subst <- getTCvSubst
2278 ; let empty_subst = zapTCvSubst subst
2279 ; _ <- foldlM check_ki (empty_subst, empty_subst)
2280 (zip3 (ktvs ++ cvs) roles cos')
2281 ; let fam_tc = coAxiomTyCon con
2282 ; case checkAxInstCo co of
2283 Just bad_branch -> bad_ax $ text "inconsistent with" <+>
2284 pprCoAxBranch fam_tc bad_branch
2285 Nothing -> return ()
2286 ; return (AxiomInstCo con ind cos') }
2287 where
2288 bad_ax what = addErrL (hang (text "Bad axiom application" <+> parens what)
2289 2 (ppr co))
2290
2291 check_ki (subst_l, subst_r) (ktv, role, arg')
2292 = do { let Pair s' t' = coercionKind arg'
2293 sk' = typeKind s'
2294 tk' = typeKind t'
2295 ; lintRole arg' role (coercionRole arg')
2296 ; let ktv_kind_l = substTy subst_l (tyVarKind ktv)
2297 ktv_kind_r = substTy subst_r (tyVarKind ktv)
2298 ; unless (sk' `eqType` ktv_kind_l)
2299 (bad_ax (text "check_ki1" <+> vcat [ ppr co, ppr sk', ppr ktv, ppr ktv_kind_l ] ))
2300 ; unless (tk' `eqType` ktv_kind_r)
2301 (bad_ax (text "check_ki2" <+> vcat [ ppr co, ppr tk', ppr ktv, ppr ktv_kind_r ] ))
2302 ; return (extendTCvSubst subst_l ktv s',
2303 extendTCvSubst subst_r ktv t') }
2304
2305 lintCoercion (KindCo co)
2306 = do { co' <- lintCoercion co
2307 ; return (KindCo co') }
2308
2309 lintCoercion (SubCo co')
2310 = do { co' <- lintCoercion co'
2311 ; lintRole co' Nominal (coercionRole co')
2312 ; return (SubCo co') }
2313
2314 lintCoercion this@(AxiomRuleCo ax cos)
2315 = do { cos' <- mapM lintCoercion cos
2316 ; lint_roles 0 (coaxrAsmpRoles ax) cos'
2317 ; case coaxrProves ax (map coercionKind cos') of
2318 Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
2319 Just _ -> return (AxiomRuleCo ax cos') }
2320 where
2321 err :: forall a. String -> [SDoc] -> LintM a
2322 err m xs = failWithL $
2323 hang (text m) 2 $ vcat (text "Rule:" <+> ppr (coaxrName ax) : xs)
2324
2325 lint_roles n (e : es) (co : cos)
2326 | e == coercionRole co = lint_roles (n+1) es cos
2327 | otherwise = err "Argument roles mismatch"
2328 [ text "In argument:" <+> int (n+1)
2329 , text "Expected:" <+> ppr e
2330 , text "Found:" <+> ppr (coercionRole co) ]
2331 lint_roles _ [] [] = return ()
2332 lint_roles n [] rs = err "Too many coercion arguments"
2333 [ text "Expected:" <+> int n
2334 , text "Provided:" <+> int (n + length rs) ]
2335
2336 lint_roles n es [] = err "Not enough coercion arguments"
2337 [ text "Expected:" <+> int (n + length es)
2338 , text "Provided:" <+> int n ]
2339
2340 lintCoercion (HoleCo h)
2341 = do { addErrL $ text "Unfilled coercion hole:" <+> ppr h
2342 ; lintCoercion (CoVarCo (coHoleCoVar h)) }
2343
2344 {-
2345 ************************************************************************
2346 * *
2347 Axioms
2348 * *
2349 ************************************************************************
2350 -}
2351
2352 lintAxioms :: Logger
2353 -> DynFlags
2354 -> SDoc -- ^ The source of the linted axioms
2355 -> [CoAxiom Branched]
2356 -> IO ()
2357 lintAxioms logger dflags what axioms =
2358 displayLintResults logger True what (vcat $ map pprCoAxiom axioms) $
2359 initL dflags (defaultLintFlags dflags) [] $
2360 do { mapM_ lint_axiom axioms
2361 ; let axiom_groups = groupWith coAxiomTyCon axioms
2362 ; mapM_ lint_axiom_group axiom_groups }
2363
2364 lint_axiom :: CoAxiom Branched -> LintM ()
2365 lint_axiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches
2366 , co_ax_role = ax_role })
2367 = addLoc (InAxiom ax) $
2368 do { mapM_ (lint_branch tc) branch_list
2369 ; extra_checks }
2370 where
2371 branch_list = fromBranches branches
2372
2373 extra_checks
2374 | isNewTyCon tc
2375 = do { CoAxBranch { cab_tvs = tvs
2376 , cab_eta_tvs = eta_tvs
2377 , cab_cvs = cvs
2378 , cab_roles = roles
2379 , cab_lhs = lhs_tys }
2380 <- case branch_list of
2381 [branch] -> return branch
2382 _ -> failWithL (text "multi-branch axiom with newtype")
2383 ; let ax_lhs = mkInfForAllTys tvs $
2384 mkTyConApp tc lhs_tys
2385 nt_tvs = takeList tvs (tyConTyVars tc)
2386 -- axiom may be eta-reduced: Note [Newtype eta] in GHC.Core.TyCon
2387 nt_lhs = mkInfForAllTys nt_tvs $
2388 mkTyConApp tc (mkTyVarTys nt_tvs)
2389 -- See Note [Newtype eta] in GHC.Core.TyCon
2390 ; lintL (ax_lhs `eqType` nt_lhs)
2391 (text "Newtype axiom LHS does not match newtype definition")
2392 ; lintL (null cvs)
2393 (text "Newtype axiom binds coercion variables")
2394 ; lintL (null eta_tvs) -- See Note [Eta reduction for data families]
2395 -- which is not about newtype axioms
2396 (text "Newtype axiom has eta-tvs")
2397 ; lintL (ax_role == Representational)
2398 (text "Newtype axiom role not representational")
2399 ; lintL (roles `equalLength` tvs)
2400 (text "Newtype axiom roles list is the wrong length." $$
2401 text "roles:" <+> sep (map ppr roles))
2402 ; lintL (roles == takeList roles (tyConRoles tc))
2403 (vcat [ text "Newtype axiom roles do not match newtype tycon's."
2404 , text "axiom roles:" <+> sep (map ppr roles)
2405 , text "tycon roles:" <+> sep (map ppr (tyConRoles tc)) ])
2406 }
2407
2408 | isFamilyTyCon tc
2409 = do { if | isTypeFamilyTyCon tc
2410 -> lintL (ax_role == Nominal)
2411 (text "type family axiom is not nominal")
2412
2413 | isDataFamilyTyCon tc
2414 -> lintL (ax_role == Representational)
2415 (text "data family axiom is not representational")
2416
2417 | otherwise
2418 -> addErrL (text "A family TyCon is neither a type family nor a data family:" <+> ppr tc)
2419
2420 ; mapM_ (lint_family_branch tc) branch_list }
2421
2422 | otherwise
2423 = addErrL (text "Axiom tycon is neither a newtype nor a family.")
2424
2425 lint_branch :: TyCon -> CoAxBranch -> LintM ()
2426 lint_branch ax_tc (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
2427 , cab_lhs = lhs_args, cab_rhs = rhs })
2428 = lintBinders LambdaBind (tvs ++ cvs) $ \_ ->
2429 do { let lhs = mkTyConApp ax_tc lhs_args
2430 ; lhs' <- lintType lhs
2431 ; rhs' <- lintType rhs
2432 ; let lhs_kind = typeKind lhs'
2433 rhs_kind = typeKind rhs'
2434 ; lintL (lhs_kind `eqType` rhs_kind) $
2435 hang (text "Inhomogeneous axiom")
2436 2 (text "lhs:" <+> ppr lhs <+> dcolon <+> ppr lhs_kind $$
2437 text "rhs:" <+> ppr rhs <+> dcolon <+> ppr rhs_kind) }
2438
2439 -- these checks do not apply to newtype axioms
2440 lint_family_branch :: TyCon -> CoAxBranch -> LintM ()
2441 lint_family_branch fam_tc br@(CoAxBranch { cab_tvs = tvs
2442 , cab_eta_tvs = eta_tvs
2443 , cab_cvs = cvs
2444 , cab_roles = roles
2445 , cab_lhs = lhs
2446 , cab_incomps = incomps })
2447 = do { lintL (isDataFamilyTyCon fam_tc || null eta_tvs)
2448 (text "Type family axiom has eta-tvs")
2449 ; lintL (all (`elemVarSet` tyCoVarsOfTypes lhs) tvs)
2450 (text "Quantified variable in family axiom unused in LHS")
2451 ; lintL (all isTyFamFree lhs)
2452 (text "Type family application on LHS of family axiom")
2453 ; lintL (all (== Nominal) roles)
2454 (text "Non-nominal role in family axiom" $$
2455 text "roles:" <+> sep (map ppr roles))
2456 ; lintL (null cvs)
2457 (text "Coercion variables bound in family axiom")
2458 ; forM_ incomps $ \ br' ->
2459 lintL (not (compatible_branches br br')) $
2460 text "Incorrect incompatible branch:" <+> ppr br' }
2461
2462 lint_axiom_group :: NonEmpty (CoAxiom Branched) -> LintM ()
2463 lint_axiom_group (_ :| []) = return ()
2464 lint_axiom_group (ax :| axs)
2465 = do { lintL (isOpenFamilyTyCon tc)
2466 (text "Non-open-family with multiple axioms")
2467 ; let all_pairs = [ (ax1, ax2) | ax1 <- all_axs
2468 , ax2 <- all_axs ]
2469 ; mapM_ (lint_axiom_pair tc) all_pairs }
2470 where
2471 all_axs = ax : axs
2472 tc = coAxiomTyCon ax
2473
2474 lint_axiom_pair :: TyCon -> (CoAxiom Branched, CoAxiom Branched) -> LintM ()
2475 lint_axiom_pair tc (ax1, ax2)
2476 | Just br1@(CoAxBranch { cab_tvs = tvs1
2477 , cab_lhs = lhs1
2478 , cab_rhs = rhs1 }) <- coAxiomSingleBranch_maybe ax1
2479 , Just br2@(CoAxBranch { cab_tvs = tvs2
2480 , cab_lhs = lhs2
2481 , cab_rhs = rhs2 }) <- coAxiomSingleBranch_maybe ax2
2482 = lintL (compatible_branches br1 br2) $
2483 vcat [ hsep [ text "Axioms", ppr ax1, text "and", ppr ax2
2484 , text "are incompatible" ]
2485 , text "tvs1 =" <+> pprTyVars tvs1
2486 , text "lhs1 =" <+> ppr (mkTyConApp tc lhs1)
2487 , text "rhs1 =" <+> ppr rhs1
2488 , text "tvs2 =" <+> pprTyVars tvs2
2489 , text "lhs2 =" <+> ppr (mkTyConApp tc lhs2)
2490 , text "rhs2 =" <+> ppr rhs2 ]
2491
2492 | otherwise
2493 = addErrL (text "Open type family axiom has more than one branch: either" <+>
2494 ppr ax1 <+> text "or" <+> ppr ax2)
2495
2496 compatible_branches :: CoAxBranch -> CoAxBranch -> Bool
2497 -- True <=> branches are compatible. See Note [Compatibility] in GHC.Core.FamInstEnv.
2498 compatible_branches (CoAxBranch { cab_tvs = tvs1
2499 , cab_lhs = lhs1
2500 , cab_rhs = rhs1 })
2501 (CoAxBranch { cab_tvs = tvs2
2502 , cab_lhs = lhs2
2503 , cab_rhs = rhs2 })
2504 = -- we need to freshen ax2 w.r.t. ax1
2505 -- do this by pretending tvs1 are in scope when processing tvs2
2506 let in_scope = mkInScopeSet (mkVarSet tvs1)
2507 subst0 = mkEmptyTCvSubst in_scope
2508 (subst, _) = substTyVarBndrs subst0 tvs2
2509 lhs2' = substTys subst lhs2
2510 rhs2' = substTy subst rhs2
2511 in
2512 case tcUnifyTys alwaysBindFun lhs1 lhs2' of
2513 Just unifying_subst -> substTy unifying_subst rhs1 `eqType`
2514 substTy unifying_subst rhs2'
2515 Nothing -> True
2516
2517 {-
2518 ************************************************************************
2519 * *
2520 \subsection[lint-monad]{The Lint monad}
2521 * *
2522 ************************************************************************
2523 -}
2524
2525 -- If you edit this type, you may need to update the GHC formalism
2526 -- See Note [GHC Formalism]
2527 data LintEnv
2528 = LE { le_flags :: LintFlags -- Linting the result of this pass
2529 , le_loc :: [LintLocInfo] -- Locations
2530
2531 , le_subst :: TCvSubst -- Current TyCo substitution
2532 -- See Note [Linting type lets]
2533 -- /Only/ substitutes for type variables;
2534 -- but might clone CoVars
2535 -- We also use le_subst to keep track of
2536 -- in-scope TyVars and CoVars (but not Ids)
2537 -- Range of the TCvSubst is LintedType/LintedCo
2538
2539 , le_ids :: VarEnv (Id, LintedType) -- In-scope Ids
2540 -- Used to check that occurrences have an enclosing binder.
2541 -- The Id is /pre-substitution/, used to check that
2542 -- the occurrence has an identical type to the binder
2543 -- The LintedType is used to return the type of the occurrence,
2544 -- without having to lint it again.
2545
2546 , le_joins :: IdSet -- Join points in scope that are valid
2547 -- A subset of the InScopeSet in le_subst
2548 -- See Note [Join points]
2549
2550 , le_dynflags :: DynFlags -- DynamicFlags
2551 , le_ue_aliases :: NameEnv UsageEnv -- Assigns usage environments to the
2552 -- alias-like binders, as found in
2553 -- non-recursive lets.
2554 }
2555
2556 data LintFlags
2557 = LF { lf_check_global_ids :: Bool -- See Note [Checking for global Ids]
2558 , lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers]
2559 , lf_check_static_ptrs :: StaticPtrCheck -- ^ See Note [Checking StaticPtrs]
2560 , lf_report_unsat_syns :: Bool -- ^ See Note [Linting type synonym applications]
2561 , lf_check_linearity :: Bool -- ^ See Note [Linting linearity]
2562 , lf_check_fixed_rep :: Bool -- See Note [Checking for representation polymorphism]
2563 }
2564
2565 -- See Note [Checking StaticPtrs]
2566 data StaticPtrCheck
2567 = AllowAnywhere
2568 -- ^ Allow 'makeStatic' to occur anywhere.
2569 | AllowAtTopLevel
2570 -- ^ Allow 'makeStatic' calls at the top-level only.
2571 | RejectEverywhere
2572 -- ^ Reject any 'makeStatic' occurrence.
2573 deriving Eq
2574
2575 defaultLintFlags :: DynFlags -> LintFlags
2576 defaultLintFlags dflags = LF { lf_check_global_ids = False
2577 , lf_check_inline_loop_breakers = True
2578 , lf_check_static_ptrs = AllowAnywhere
2579 , lf_check_linearity = gopt Opt_DoLinearCoreLinting dflags
2580 , lf_report_unsat_syns = True
2581 , lf_check_fixed_rep = True
2582 }
2583
2584 newtype LintM a =
2585 LintM { unLintM ::
2586 LintEnv ->
2587 WarnsAndErrs -> -- Warning and error messages so far
2588 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
2589 deriving (Functor)
2590
2591 type WarnsAndErrs = (Bag SDoc, Bag SDoc)
2592
2593 {- Note [Checking for global Ids]
2594 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2595 Before CoreTidy, all locally-bound Ids must be LocalIds, even
2596 top-level ones. See Note [Exported LocalIds] and #9857.
2597
2598 Note [Checking StaticPtrs]
2599 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2600 See Note [Grand plan for static forms] in GHC.Iface.Tidy.StaticPtrTable for an overview.
2601
2602 Every occurrence of the function 'makeStatic' should be moved to the
2603 top level by the FloatOut pass. It's vital that we don't have nested
2604 'makeStatic' occurrences after CorePrep, because we populate the Static
2605 Pointer Table from the top-level bindings. See SimplCore Note [Grand
2606 plan for static forms].
2607
2608 The linter checks that no occurrence is left behind, nested within an
2609 expression. The check is enabled only after the FloatOut, CorePrep,
2610 and CoreTidy passes and only if the module uses the StaticPointers
2611 language extension. Checking more often doesn't help since the condition
2612 doesn't hold until after the first FloatOut pass.
2613
2614 Note [Type substitution]
2615 ~~~~~~~~~~~~~~~~~~~~~~~~
2616 Why do we need a type substitution? Consider
2617 /\(a:*). \(x:a). /\(a:*). id a x
2618 This is ill typed, because (renaming variables) it is really
2619 /\(a:*). \(x:a). /\(b:*). id b x
2620 Hence, when checking an application, we can't naively compare x's type
2621 (at its binding site) with its expected type (at a use site). So we
2622 rename type binders as we go, maintaining a substitution.
2623
2624 The same substitution also supports let-type, current expressed as
2625 (/\(a:*). body) ty
2626 Here we substitute 'ty' for 'a' in 'body', on the fly.
2627
2628 Note [Linting type synonym applications]
2629 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2630 When linting a type-synonym, or type-family, application
2631 S ty1 .. tyn
2632 we behave as follows (#15057, #T15664):
2633
2634 * If lf_report_unsat_syns = True, and S has arity < n,
2635 complain about an unsaturated type synonym or type family
2636
2637 * Switch off lf_report_unsat_syns, and lint ty1 .. tyn.
2638
2639 Reason: catch out of scope variables or other ill-kinded gubbins,
2640 even if S discards that argument entirely. E.g. (#15012):
2641 type FakeOut a = Int
2642 type family TF a
2643 type instance TF Int = FakeOut a
2644 Here 'a' is out of scope; but if we expand FakeOut, we conceal
2645 that out-of-scope error.
2646
2647 Reason for switching off lf_report_unsat_syns: with
2648 LiberalTypeSynonyms, GHC allows unsaturated synonyms provided they
2649 are saturated when the type is expanded. Example
2650 type T f = f Int
2651 type S a = a -> a
2652 type Z = T S
2653 In Z's RHS, S appears unsaturated, but it is saturated when T is expanded.
2654
2655 * If lf_report_unsat_syns is on, expand the synonym application and
2656 lint the result. Reason: want to check that synonyms are saturated
2657 when the type is expanded.
2658
2659 Note [Linting linearity]
2660 ~~~~~~~~~~~~~~~~~~~~~~~~
2661 There is one known optimisations that have not yet been updated
2662 to work with Linear Lint:
2663
2664 * Optimisations can create a letrec which uses a variable linearly, e.g.
2665 letrec f True = f False
2666 f False = x
2667 in f True
2668 uses 'x' linearly, but this is not seen by the linter.
2669 Plan: make let-bound variables remember the usage environment.
2670 See ticket #18694.
2671
2672 We plan to fix this issue in the very near future.
2673 For now, -dcore-lint enables only linting output of the desugarer,
2674 and full Linear Lint has to be enabled separately with -dlinear-core-lint.
2675 Ticket #19165 concerns enabling Linear Lint with -dcore-lint.
2676 -}
2677
2678 instance Applicative LintM where
2679 pure x = LintM $ \ _ errs -> (Just x, errs)
2680 (<*>) = ap
2681
2682 instance Monad LintM where
2683 m >>= k = LintM (\ env errs ->
2684 let (res, errs') = unLintM m env errs in
2685 case res of
2686 Just r -> unLintM (k r) env errs'
2687 Nothing -> (Nothing, errs'))
2688
2689 instance MonadFail LintM where
2690 fail err = failWithL (text err)
2691
2692 instance HasDynFlags LintM where
2693 getDynFlags = LintM (\ e errs -> (Just (le_dynflags e), errs))
2694
2695 data LintLocInfo
2696 = RhsOf Id -- The variable bound
2697 | OccOf Id -- Occurrence of id
2698 | LambdaBodyOf Id -- The lambda-binder
2699 | RuleOf Id -- Rules attached to a binder
2700 | UnfoldingOf Id -- Unfolding of a binder
2701 | BodyOfLetRec [Id] -- One of the binders
2702 | CaseAlt CoreAlt -- Case alternative
2703 | CasePat CoreAlt -- The *pattern* of the case alternative
2704 | CaseTy CoreExpr -- The type field of a case expression
2705 -- with this scrutinee
2706 | IdTy Id -- The type field of an Id binder
2707 | AnExpr CoreExpr -- Some expression
2708 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
2709 | TopLevelBindings
2710 | InType Type -- Inside a type
2711 | InCo Coercion -- Inside a coercion
2712 | InAxiom (CoAxiom Branched) -- Inside a CoAxiom
2713
2714 initL :: DynFlags -> LintFlags -> [Var]
2715 -> LintM a -> WarnsAndErrs -- Warnings and errors
2716 initL dflags flags vars m
2717 = case unLintM m env (emptyBag, emptyBag) of
2718 (Just _, errs) -> errs
2719 (Nothing, errs@(_, e)) | not (isEmptyBag e) -> errs
2720 | otherwise -> pprPanic ("Bug in Lint: a failure occurred " ++
2721 "without reporting an error message") empty
2722 where
2723 (tcvs, ids) = partition isTyCoVar vars
2724 env = LE { le_flags = flags
2725 , le_subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet tcvs))
2726 , le_ids = mkVarEnv [(id, (id,idType id)) | id <- ids]
2727 , le_joins = emptyVarSet
2728 , le_loc = []
2729 , le_dynflags = dflags
2730 , le_ue_aliases = emptyNameEnv }
2731
2732 setReportUnsat :: Bool -> LintM a -> LintM a
2733 -- Switch off lf_report_unsat_syns
2734 setReportUnsat ru thing_inside
2735 = LintM $ \ env errs ->
2736 let env' = env { le_flags = (le_flags env) { lf_report_unsat_syns = ru } }
2737 in unLintM thing_inside env' errs
2738
2739 -- See Note [Checking for representation polymorphism]
2740 noFixedRuntimeRepChecks :: LintM a -> LintM a
2741 noFixedRuntimeRepChecks thing_inside
2742 = LintM $ \env errs ->
2743 let env' = env { le_flags = (le_flags env) { lf_check_fixed_rep = False } }
2744 in unLintM thing_inside env' errs
2745
2746 getLintFlags :: LintM LintFlags
2747 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
2748
2749 checkL :: Bool -> SDoc -> LintM ()
2750 checkL True _ = return ()
2751 checkL False msg = failWithL msg
2752
2753 -- like checkL, but relevant to type checking
2754 lintL :: Bool -> SDoc -> LintM ()
2755 lintL = checkL
2756
2757 checkWarnL :: Bool -> SDoc -> LintM ()
2758 checkWarnL True _ = return ()
2759 checkWarnL False msg = addWarnL msg
2760
2761 failWithL :: SDoc -> LintM a
2762 failWithL msg = LintM $ \ env (warns,errs) ->
2763 (Nothing, (warns, addMsg True env errs msg))
2764
2765 addErrL :: SDoc -> LintM ()
2766 addErrL msg = LintM $ \ env (warns,errs) ->
2767 (Just (), (warns, addMsg True env errs msg))
2768
2769 addWarnL :: SDoc -> LintM ()
2770 addWarnL msg = LintM $ \ env (warns,errs) ->
2771 (Just (), (addMsg False env warns msg, errs))
2772
2773 addMsg :: Bool -> LintEnv -> Bag SDoc -> SDoc -> Bag SDoc
2774 addMsg is_error env msgs msg
2775 = assertPpr (notNull loc_msgs) msg $
2776 msgs `snocBag` mk_msg msg
2777 where
2778 loc_msgs :: [(SrcLoc, SDoc)] -- Innermost first
2779 loc_msgs = map dumpLoc (le_loc env)
2780
2781 cxt_doc = vcat [ vcat $ reverse $ map snd loc_msgs
2782 , text "Substitution:" <+> ppr (le_subst env) ]
2783 context | is_error = cxt_doc
2784 | otherwise = whenPprDebug cxt_doc
2785 -- Print voluminous info for Lint errors
2786 -- but not for warnings
2787
2788 msg_span = case [ span | (loc,_) <- loc_msgs
2789 , let span = srcLocSpan loc
2790 , isGoodSrcSpan span ] of
2791 [] -> noSrcSpan
2792 (s:_) -> s
2793 !diag_opts = initDiagOpts (le_dynflags env)
2794 mk_msg msg = mkLocMessage (mkMCDiagnostic diag_opts WarningWithoutFlag) msg_span
2795 (msg $$ context)
2796
2797 addLoc :: LintLocInfo -> LintM a -> LintM a
2798 addLoc extra_loc m
2799 = LintM $ \ env errs ->
2800 unLintM m (env { le_loc = extra_loc : le_loc env }) errs
2801
2802 inCasePat :: LintM Bool -- A slight hack; see the unique call site
2803 inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
2804 where
2805 is_case_pat (LE { le_loc = CasePat {} : _ }) = True
2806 is_case_pat _other = False
2807
2808 addInScopeId :: Id -> LintedType -> LintM a -> LintM a
2809 addInScopeId id linted_ty m
2810 = LintM $ \ env@(LE { le_ids = id_set, le_joins = join_set }) errs ->
2811 unLintM m (env { le_ids = extendVarEnv id_set id (id, linted_ty)
2812 , le_joins = add_joins join_set }) errs
2813 where
2814 add_joins join_set
2815 | isJoinId id = extendVarSet join_set id -- Overwrite with new arity
2816 | otherwise = delVarSet join_set id -- Remove any existing binding
2817
2818 getInScopeIds :: LintM (VarEnv (Id,LintedType))
2819 getInScopeIds = LintM (\env errs -> (Just (le_ids env), errs))
2820
2821 extendTvSubstL :: TyVar -> Type -> LintM a -> LintM a
2822 extendTvSubstL tv ty m
2823 = LintM $ \ env errs ->
2824 unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
2825
2826 updateTCvSubst :: TCvSubst -> LintM a -> LintM a
2827 updateTCvSubst subst' m
2828 = LintM $ \ env errs -> unLintM m (env { le_subst = subst' }) errs
2829
2830 markAllJoinsBad :: LintM a -> LintM a
2831 markAllJoinsBad m
2832 = LintM $ \ env errs -> unLintM m (env { le_joins = emptyVarSet }) errs
2833
2834 markAllJoinsBadIf :: Bool -> LintM a -> LintM a
2835 markAllJoinsBadIf True m = markAllJoinsBad m
2836 markAllJoinsBadIf False m = m
2837
2838 getValidJoins :: LintM IdSet
2839 getValidJoins = LintM (\ env errs -> (Just (le_joins env), errs))
2840
2841 getTCvSubst :: LintM TCvSubst
2842 getTCvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
2843
2844 getUEAliases :: LintM (NameEnv UsageEnv)
2845 getUEAliases = LintM (\ env errs -> (Just (le_ue_aliases env), errs))
2846
2847 getInScope :: LintM InScopeSet
2848 getInScope = LintM (\ env errs -> (Just (getTCvInScope $ le_subst env), errs))
2849
2850 lookupIdInScope :: Id -> LintM (Id, LintedType)
2851 lookupIdInScope id_occ
2852 = do { in_scope_ids <- getInScopeIds
2853 ; case lookupVarEnv in_scope_ids id_occ of
2854 Just (id_bndr, linted_ty)
2855 -> do { checkL (not (bad_global id_bndr)) global_in_scope
2856 ; return (id_bndr, linted_ty) }
2857 Nothing -> do { checkL (not is_local) local_out_of_scope
2858 ; return (id_occ, idType id_occ) } }
2859 -- We don't bother to lint the type
2860 -- of global (i.e. imported) Ids
2861 where
2862 is_local = mustHaveLocalBinding id_occ
2863 local_out_of_scope = text "Out of scope:" <+> pprBndr LetBind id_occ
2864 global_in_scope = hang (text "Occurrence is GlobalId, but binding is LocalId")
2865 2 (pprBndr LetBind id_occ)
2866 bad_global id_bnd = isGlobalId id_occ
2867 && isLocalId id_bnd
2868 && not (isWiredIn id_occ)
2869 -- 'bad_global' checks for the case where an /occurrence/ is
2870 -- a GlobalId, but there is an enclosing binding fora a LocalId.
2871 -- NB: the in-scope variables are mostly LocalIds, checked by lintIdBndr,
2872 -- but GHCi adds GlobalIds from the interactive context. These
2873 -- are fine; hence the test (isLocalId id == isLocalId v)
2874 -- NB: when compiling Control.Exception.Base, things like absentError
2875 -- are defined locally, but appear in expressions as (global)
2876 -- wired-in Ids after worker/wrapper
2877 -- So we simply disable the test in this case
2878
2879 lookupJoinId :: Id -> LintM (Maybe JoinArity)
2880 -- Look up an Id which should be a join point, valid here
2881 -- If so, return its arity, if not return Nothing
2882 lookupJoinId id
2883 = do { join_set <- getValidJoins
2884 ; case lookupVarSet join_set id of
2885 Just id' -> return (isJoinId_maybe id')
2886 Nothing -> return Nothing }
2887
2888 addAliasUE :: Id -> UsageEnv -> LintM a -> LintM a
2889 addAliasUE id ue thing_inside = LintM $ \ env errs ->
2890 let new_ue_aliases =
2891 extendNameEnv (le_ue_aliases env) (getName id) ue
2892 in
2893 unLintM thing_inside (env { le_ue_aliases = new_ue_aliases }) errs
2894
2895 varCallSiteUsage :: Id -> LintM UsageEnv
2896 varCallSiteUsage id =
2897 do m <- getUEAliases
2898 return $ case lookupNameEnv m (getName id) of
2899 Nothing -> unitUE id One
2900 Just id_ue -> id_ue
2901
2902 ensureEqTys :: LintedType -> LintedType -> SDoc -> LintM ()
2903 -- check ty2 is subtype of ty1 (ie, has same structure but usage
2904 -- annotations need only be consistent, not equal)
2905 -- Assumes ty1,ty2 are have already had the substitution applied
2906 ensureEqTys ty1 ty2 msg = lintL (ty1 `eqType` ty2) msg
2907
2908 ensureSubUsage :: Usage -> Mult -> SDoc -> LintM ()
2909 ensureSubUsage Bottom _ _ = return ()
2910 ensureSubUsage Zero described_mult err_msg = ensureSubMult Many described_mult err_msg
2911 ensureSubUsage (MUsage m) described_mult err_msg = ensureSubMult m described_mult err_msg
2912
2913 ensureSubMult :: Mult -> Mult -> SDoc -> LintM ()
2914 ensureSubMult actual_usage described_usage err_msg = do
2915 flags <- getLintFlags
2916 when (lf_check_linearity flags) $ case actual_usage' `submult` described_usage' of
2917 Submult -> return ()
2918 Unknown -> case isMultMul actual_usage' of
2919 Just (m1, m2) -> ensureSubMult m1 described_usage' err_msg >>
2920 ensureSubMult m2 described_usage' err_msg
2921 Nothing -> when (not (actual_usage' `eqType` described_usage')) (addErrL err_msg)
2922
2923 where actual_usage' = normalize actual_usage
2924 described_usage' = normalize described_usage
2925
2926 normalize :: Mult -> Mult
2927 normalize m = case isMultMul m of
2928 Just (m1, m2) -> mkMultMul (normalize m1) (normalize m2)
2929 Nothing -> m
2930
2931 lintRole :: Outputable thing
2932 => thing -- where the role appeared
2933 -> Role -- expected
2934 -> Role -- actual
2935 -> LintM ()
2936 lintRole co r1 r2
2937 = lintL (r1 == r2)
2938 (text "Role incompatibility: expected" <+> ppr r1 <> comma <+>
2939 text "got" <+> ppr r2 $$
2940 text "in" <+> ppr co)
2941
2942 {-
2943 ************************************************************************
2944 * *
2945 \subsection{Error messages}
2946 * *
2947 ************************************************************************
2948 -}
2949
2950 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
2951
2952 dumpLoc (RhsOf v)
2953 = (getSrcLoc v, text "In the RHS of" <+> pp_binders [v])
2954
2955 dumpLoc (OccOf v)
2956 = (getSrcLoc v, text "In an occurrence of" <+> pp_binder v)
2957
2958 dumpLoc (LambdaBodyOf b)
2959 = (getSrcLoc b, text "In the body of lambda with binder" <+> pp_binder b)
2960
2961 dumpLoc (RuleOf b)
2962 = (getSrcLoc b, text "In a rule attached to" <+> pp_binder b)
2963
2964 dumpLoc (UnfoldingOf b)
2965 = (getSrcLoc b, text "In the unfolding of" <+> pp_binder b)
2966
2967 dumpLoc (BodyOfLetRec [])
2968 = (noSrcLoc, text "In body of a letrec with no binders")
2969
2970 dumpLoc (BodyOfLetRec bs@(_:_))
2971 = ( getSrcLoc (head bs), text "In the body of letrec with binders" <+> pp_binders bs)
2972
2973 dumpLoc (AnExpr e)
2974 = (noSrcLoc, text "In the expression:" <+> ppr e)
2975
2976 dumpLoc (CaseAlt (Alt con args _))
2977 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
2978
2979 dumpLoc (CasePat (Alt con args _))
2980 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
2981
2982 dumpLoc (CaseTy scrut)
2983 = (noSrcLoc, hang (text "In the result-type of a case with scrutinee:")
2984 2 (ppr scrut))
2985
2986 dumpLoc (IdTy b)
2987 = (getSrcLoc b, text "In the type of a binder:" <+> ppr b)
2988
2989 dumpLoc (ImportedUnfolding locn)
2990 = (locn, text "In an imported unfolding")
2991 dumpLoc TopLevelBindings
2992 = (noSrcLoc, Outputable.empty)
2993 dumpLoc (InType ty)
2994 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
2995 dumpLoc (InCo co)
2996 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
2997 dumpLoc (InAxiom ax)
2998 = (getSrcLoc ax_name, text "In the coercion axiom" <+> ppr ax_name <+> dcolon <+> pp_ax)
2999 where
3000 CoAxiom { co_ax_name = ax_name
3001 , co_ax_tc = tc
3002 , co_ax_role = ax_role
3003 , co_ax_branches = branches } = ax
3004 branch_list = fromBranches branches
3005
3006 pp_ax
3007 | [branch] <- branch_list
3008 = pp_branch branch
3009
3010 | otherwise
3011 = braces $ vcat (map pp_branch branch_list)
3012
3013 pp_branch (CoAxBranch { cab_tvs = tvs
3014 , cab_cvs = cvs
3015 , cab_lhs = lhs_tys
3016 , cab_rhs = rhs_ty })
3017 = sep [ brackets (pprWithCommas pprTyVar (tvs ++ cvs)) <> dot
3018 , ppr (mkTyConApp tc lhs_tys)
3019 , text "~_" <> pp_role ax_role
3020 , ppr rhs_ty ]
3021
3022 pp_role Nominal = text "N"
3023 pp_role Representational = text "R"
3024 pp_role Phantom = text "P"
3025
3026 pp_binders :: [Var] -> SDoc
3027 pp_binders bs = sep (punctuate comma (map pp_binder bs))
3028
3029 pp_binder :: Var -> SDoc
3030 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
3031 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
3032
3033 ------------------------------------------------------
3034 -- Messages for case expressions
3035
3036 mkDefaultArgsMsg :: [Var] -> SDoc
3037 mkDefaultArgsMsg args
3038 = hang (text "DEFAULT case with binders")
3039 4 (ppr args)
3040
3041 mkCaseAltMsg :: CoreExpr -> Type -> Type -> SDoc
3042 mkCaseAltMsg e ty1 ty2
3043 = hang (text "Type of case alternatives not the same as the annotation on case:")
3044 4 (vcat [ text "Actual type:" <+> ppr ty1,
3045 text "Annotation on case:" <+> ppr ty2,
3046 text "Alt Rhs:" <+> ppr e ])
3047
3048 mkScrutMsg :: Id -> Type -> Type -> TCvSubst -> SDoc
3049 mkScrutMsg var var_ty scrut_ty subst
3050 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
3051 text "Result binder type:" <+> ppr var_ty,--(idType var),
3052 text "Scrutinee type:" <+> ppr scrut_ty,
3053 hsep [text "Current TCv subst", ppr subst]]
3054
3055 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> SDoc
3056 mkNonDefltMsg e
3057 = hang (text "Case expression with DEFAULT not at the beginning") 4 (ppr e)
3058 mkNonIncreasingAltsMsg e
3059 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
3060
3061 nonExhaustiveAltsMsg :: CoreExpr -> SDoc
3062 nonExhaustiveAltsMsg e
3063 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
3064
3065 mkBadConMsg :: TyCon -> DataCon -> SDoc
3066 mkBadConMsg tycon datacon
3067 = vcat [
3068 text "In a case alternative, data constructor isn't in scrutinee type:",
3069 text "Scrutinee type constructor:" <+> ppr tycon,
3070 text "Data con:" <+> ppr datacon
3071 ]
3072
3073 mkBadPatMsg :: Type -> Type -> SDoc
3074 mkBadPatMsg con_result_ty scrut_ty
3075 = vcat [
3076 text "In a case alternative, pattern result type doesn't match scrutinee type:",
3077 text "Pattern result type:" <+> ppr con_result_ty,
3078 text "Scrutinee type:" <+> ppr scrut_ty
3079 ]
3080
3081 integerScrutinisedMsg :: SDoc
3082 integerScrutinisedMsg
3083 = text "In a LitAlt, the literal is lifted (probably Integer)"
3084
3085 mkBadAltMsg :: Type -> CoreAlt -> SDoc
3086 mkBadAltMsg scrut_ty alt
3087 = vcat [ text "Data alternative when scrutinee is not a tycon application",
3088 text "Scrutinee type:" <+> ppr scrut_ty,
3089 text "Alternative:" <+> pprCoreAlt alt ]
3090
3091 mkNewTyDataConAltMsg :: Type -> CoreAlt -> SDoc
3092 mkNewTyDataConAltMsg scrut_ty alt
3093 = vcat [ text "Data alternative for newtype datacon",
3094 text "Scrutinee type:" <+> ppr scrut_ty,
3095 text "Alternative:" <+> pprCoreAlt alt ]
3096
3097
3098 ------------------------------------------------------
3099 -- Other error messages
3100
3101 mkAppMsg :: Type -> Type -> CoreExpr -> SDoc
3102 mkAppMsg fun_ty arg_ty arg
3103 = vcat [text "Argument value doesn't match argument type:",
3104 hang (text "Fun type:") 4 (ppr fun_ty),
3105 hang (text "Arg type:") 4 (ppr arg_ty),
3106 hang (text "Arg:") 4 (ppr arg)]
3107
3108 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> SDoc
3109 mkNonFunAppMsg fun_ty arg_ty arg
3110 = vcat [text "Non-function type in function position",
3111 hang (text "Fun type:") 4 (ppr fun_ty),
3112 hang (text "Arg type:") 4 (ppr arg_ty),
3113 hang (text "Arg:") 4 (ppr arg)]
3114
3115 mkLetErr :: TyVar -> CoreExpr -> SDoc
3116 mkLetErr bndr rhs
3117 = vcat [text "Bad `let' binding:",
3118 hang (text "Variable:")
3119 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
3120 hang (text "Rhs:")
3121 4 (ppr rhs)]
3122
3123 mkTyAppMsg :: Type -> Type -> SDoc
3124 mkTyAppMsg ty arg_ty
3125 = vcat [text "Illegal type application:",
3126 hang (text "Exp type:")
3127 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
3128 hang (text "Arg type:")
3129 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
3130
3131 emptyRec :: CoreExpr -> SDoc
3132 emptyRec e = hang (text "Empty Rec binding:") 2 (ppr e)
3133
3134 mkRhsMsg :: Id -> SDoc -> Type -> SDoc
3135 mkRhsMsg binder what ty
3136 = vcat
3137 [hsep [text "The type of this binder doesn't match the type of its" <+> what <> colon,
3138 ppr binder],
3139 hsep [text "Binder's type:", ppr (idType binder)],
3140 hsep [text "Rhs type:", ppr ty]]
3141
3142 mkLetAppMsg :: CoreExpr -> SDoc
3143 mkLetAppMsg e
3144 = hang (text "This argument does not satisfy the let/app invariant:")
3145 2 (ppr e)
3146
3147 badBndrTyMsg :: Id -> SDoc -> SDoc
3148 badBndrTyMsg binder what
3149 = vcat [ text "The type of this binder is" <+> what <> colon <+> ppr binder
3150 , text "Binder's type:" <+> ppr (idType binder) ]
3151
3152 mkNonTopExportedMsg :: Id -> SDoc
3153 mkNonTopExportedMsg binder
3154 = hsep [text "Non-top-level binder is marked as exported:", ppr binder]
3155
3156 mkNonTopExternalNameMsg :: Id -> SDoc
3157 mkNonTopExternalNameMsg binder
3158 = hsep [text "Non-top-level binder has an external name:", ppr binder]
3159
3160 mkTopNonLitStrMsg :: Id -> SDoc
3161 mkTopNonLitStrMsg binder
3162 = hsep [text "Top-level Addr# binder has a non-literal rhs:", ppr binder]
3163
3164 mkKindErrMsg :: TyVar -> Type -> SDoc
3165 mkKindErrMsg tyvar arg_ty
3166 = vcat [text "Kinds don't match in type application:",
3167 hang (text "Type variable:")
3168 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
3169 hang (text "Arg type:")
3170 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
3171
3172 mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> SDoc
3173 mkCastErr expr = mk_cast_err "expression" "type" (ppr expr)
3174
3175 mkCastTyErr :: Type -> Coercion -> Kind -> Kind -> SDoc
3176 mkCastTyErr ty = mk_cast_err "type" "kind" (ppr ty)
3177
3178 mk_cast_err :: String -- ^ What sort of casted thing this is
3179 -- (\"expression\" or \"type\").
3180 -> String -- ^ What sort of coercion is being used
3181 -- (\"type\" or \"kind\").
3182 -> SDoc -- ^ The thing being casted.
3183 -> Coercion -> Type -> Type -> SDoc
3184 mk_cast_err thing_str co_str pp_thing co from_ty thing_ty
3185 = vcat [from_msg <+> text "of Cast differs from" <+> co_msg
3186 <+> text "of" <+> enclosed_msg,
3187 from_msg <> colon <+> ppr from_ty,
3188 text (capitalise co_str) <+> text "of" <+> enclosed_msg <> colon
3189 <+> ppr thing_ty,
3190 text "Actual" <+> enclosed_msg <> colon <+> pp_thing,
3191 text "Coercion used in cast:" <+> ppr co
3192 ]
3193 where
3194 co_msg, from_msg, enclosed_msg :: SDoc
3195 co_msg = text co_str
3196 from_msg = text "From-" <> co_msg
3197 enclosed_msg = text "enclosed" <+> text thing_str
3198
3199 mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc
3200 mkBadUnivCoMsg lr co
3201 = text "Kind mismatch on the" <+> pprLeftOrRight lr <+>
3202 text "side of a UnivCo:" <+> ppr co
3203
3204 mkBadProofIrrelMsg :: Type -> Coercion -> SDoc
3205 mkBadProofIrrelMsg ty co
3206 = hang (text "Found a non-coercion in a proof-irrelevance UnivCo:")
3207 2 (vcat [ text "type:" <+> ppr ty
3208 , text "co:" <+> ppr co ])
3209
3210 mkBadTyVarMsg :: Var -> SDoc
3211 mkBadTyVarMsg tv
3212 = text "Non-tyvar used in TyVarTy:"
3213 <+> ppr tv <+> dcolon <+> ppr (varType tv)
3214
3215 mkBadJoinBindMsg :: Var -> SDoc
3216 mkBadJoinBindMsg var
3217 = vcat [ text "Bad join point binding:" <+> ppr var
3218 , text "Join points can be bound only by a non-top-level let" ]
3219
3220 mkInvalidJoinPointMsg :: Var -> Type -> SDoc
3221 mkInvalidJoinPointMsg var ty
3222 = hang (text "Join point has invalid type:")
3223 2 (ppr var <+> dcolon <+> ppr ty)
3224
3225 mkBadJoinArityMsg :: Var -> Int -> Int -> CoreExpr -> SDoc
3226 mkBadJoinArityMsg var ar n rhs
3227 = vcat [ text "Join point has too few lambdas",
3228 text "Join var:" <+> ppr var,
3229 text "Join arity:" <+> ppr ar,
3230 text "Number of lambdas:" <+> ppr (ar - n),
3231 text "Rhs = " <+> ppr rhs
3232 ]
3233
3234 invalidJoinOcc :: Var -> SDoc
3235 invalidJoinOcc var
3236 = vcat [ text "Invalid occurrence of a join variable:" <+> ppr var
3237 , text "The binder is either not a join point, or not valid here" ]
3238
3239 mkBadJumpMsg :: Var -> Int -> Int -> SDoc
3240 mkBadJumpMsg var ar nargs
3241 = vcat [ text "Join point invoked with wrong number of arguments",
3242 text "Join var:" <+> ppr var,
3243 text "Join arity:" <+> ppr ar,
3244 text "Number of arguments:" <+> int nargs ]
3245
3246 mkInconsistentRecMsg :: [Var] -> SDoc
3247 mkInconsistentRecMsg bndrs
3248 = vcat [ text "Recursive let binders mix values and join points",
3249 text "Binders:" <+> hsep (map ppr_with_details bndrs) ]
3250 where
3251 ppr_with_details bndr = ppr bndr <> ppr (idDetails bndr)
3252
3253 mkJoinBndrOccMismatchMsg :: Var -> JoinArity -> JoinArity -> SDoc
3254 mkJoinBndrOccMismatchMsg bndr join_arity_bndr join_arity_occ
3255 = vcat [ text "Mismatch in join point arity between binder and occurrence"
3256 , text "Var:" <+> ppr bndr
3257 , text "Arity at binding site:" <+> ppr join_arity_bndr
3258 , text "Arity at occurrence: " <+> ppr join_arity_occ ]
3259
3260 mkBndrOccTypeMismatchMsg :: Var -> Var -> LintedType -> LintedType -> SDoc
3261 mkBndrOccTypeMismatchMsg bndr var bndr_ty var_ty
3262 = vcat [ text "Mismatch in type between binder and occurrence"
3263 , text "Binder:" <+> ppr bndr <+> dcolon <+> ppr bndr_ty
3264 , text "Occurrence:" <+> ppr var <+> dcolon <+> ppr var_ty
3265 , text " Before subst:" <+> ppr (idType var) ]
3266
3267 mkBadJoinPointRuleMsg :: JoinId -> JoinArity -> CoreRule -> SDoc
3268 mkBadJoinPointRuleMsg bndr join_arity rule
3269 = vcat [ text "Join point has rule with wrong number of arguments"
3270 , text "Var:" <+> ppr bndr
3271 , text "Join arity:" <+> ppr join_arity
3272 , text "Rule:" <+> ppr rule ]
3273
3274 pprLeftOrRight :: LeftOrRight -> SDoc
3275 pprLeftOrRight CLeft = text "left"
3276 pprLeftOrRight CRight = text "right"
3277
3278 dupVars :: [NonEmpty Var] -> SDoc
3279 dupVars vars
3280 = hang (text "Duplicate variables brought into scope")
3281 2 (ppr (map toList vars))
3282
3283 dupExtVars :: [NonEmpty Name] -> SDoc
3284 dupExtVars vars
3285 = hang (text "Duplicate top-level variables with the same qualified name")
3286 2 (ppr (map toList vars))
3287
3288 {-
3289 ************************************************************************
3290 * *
3291 \subsection{Annotation Linting}
3292 * *
3293 ************************************************************************
3294 -}
3295
3296 -- | This checks whether a pass correctly looks through debug
3297 -- annotations (@SourceNote@). This works a bit different from other
3298 -- consistency checks: We check this by running the given task twice,
3299 -- noting all differences between the results.
3300 lintAnnots :: SDoc -> (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
3301 lintAnnots pname pass guts = {-# SCC "lintAnnots" #-} do
3302 -- Run the pass as we normally would
3303 dflags <- getDynFlags
3304 logger <- getLogger
3305 when (gopt Opt_DoAnnotationLinting dflags) $
3306 liftIO $ Err.showPass logger "Annotation linting - first run"
3307 nguts <- pass guts
3308 -- If appropriate re-run it without debug annotations to make sure
3309 -- that they made no difference.
3310 when (gopt Opt_DoAnnotationLinting dflags) $ do
3311 liftIO $ Err.showPass logger "Annotation linting - second run"
3312 nguts' <- withoutAnnots pass guts
3313 -- Finally compare the resulting bindings
3314 liftIO $ Err.showPass logger "Annotation linting - comparison"
3315 let binds = flattenBinds $ mg_binds nguts
3316 binds' = flattenBinds $ mg_binds nguts'
3317 (diffs,_) = diffBinds True (mkRnEnv2 emptyInScopeSet) binds binds'
3318 when (not (null diffs)) $ GHC.Core.Opt.Monad.putMsg $ vcat
3319 [ lint_banner "warning" pname
3320 , text "Core changes with annotations:"
3321 , withPprStyle defaultDumpStyle $ nest 2 $ vcat diffs
3322 ]
3323 -- Return actual new guts
3324 return nguts
3325
3326 -- | Run the given pass without annotations. This means that we both
3327 -- set the debugLevel setting to 0 in the environment as well as all
3328 -- annotations from incoming modules.
3329 withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
3330 withoutAnnots pass guts = do
3331 -- Remove debug flag from environment.
3332 dflags <- getDynFlags
3333 let removeFlag env = hscSetFlags (dflags { debugLevel = 0}) env
3334 withoutFlag corem =
3335 -- TODO: supply tag here as well ?
3336 liftIO =<< runCoreM <$> fmap removeFlag getHscEnv <*> getRuleBase <*>
3337 getUniqMask <*> getModule <*>
3338 getVisibleOrphanMods <*>
3339 getPrintUnqualified <*> getSrcSpanM <*>
3340 pure corem
3341 -- Nuke existing ticks in module.
3342 -- TODO: Ticks in unfoldings. Maybe change unfolding so it removes
3343 -- them in absence of debugLevel > 0.
3344 let nukeTicks = stripTicksE (not . tickishIsCode)
3345 nukeAnnotsBind :: CoreBind -> CoreBind
3346 nukeAnnotsBind bind = case bind of
3347 Rec bs -> Rec $ map (\(b,e) -> (b, nukeTicks e)) bs
3348 NonRec b e -> NonRec b $ nukeTicks e
3349 nukeAnnotsMod mg@ModGuts{mg_binds=binds}
3350 = mg{mg_binds = map nukeAnnotsBind binds}
3351 -- Perform pass with all changes applied
3352 fmap fst $ withoutFlag $ pass (nukeAnnotsMod guts)