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