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