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