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