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