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