CoreLint: Use size-annotated ppr variant
[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 {-# OPTIONS_GHC -fprof-auto #-}
11
12 module CoreLint (
13 lintCoreBindings, lintUnfolding,
14 lintPassResult, lintInteractiveExpr, lintExpr,
15 lintAnnots,
16
17 -- ** Debug output
18 CoreLint.showPass, showPassIO, endPass, endPassIO,
19 dumpPassResult,
20 CoreLint.dumpIfSet,
21 ) where
22
23 #include "HsVersions.h"
24
25 import CoreSyn
26 import CoreFVs
27 import CoreUtils
28 import CoreStats ( coreBindsStats )
29 import CoreMonad
30 import Bag
31 import Literal
32 import DataCon
33 import TysWiredIn
34 import TysPrim
35 import Var
36 import VarEnv
37 import VarSet
38 import Name
39 import Id
40 import PprCore
41 import ErrUtils
42 import Coercion
43 import SrcLoc
44 import Kind
45 import Type
46 import TypeRep
47 import TyCon
48 import CoAxiom
49 import BasicTypes
50 import ErrUtils as Err
51 import StaticFlags
52 import ListSetOps
53 import PrelNames
54 import Outputable
55 import FastString
56 import Util
57 import InstEnv ( instanceDFunId )
58 import OptCoercion ( checkAxInstCo )
59 import UniqSupply
60 import CoreArity ( typeArity )
61 import Demand ( splitStrictSig, isBotRes )
62
63 import HscTypes
64 import DynFlags
65 import Control.Monad
66 import MonadUtils
67 import Data.Maybe
68 import Pair
69
70 {-
71 Note [GHC Formalism]
72 ~~~~~~~~~~~~~~~~~~~~
73 This file implements the type-checking algorithm for System FC, the "official"
74 name of the Core language. Type safety of FC is heart of the claim that
75 executables produced by GHC do not have segmentation faults. Thus, it is
76 useful to be able to reason about System FC independently of reading the code.
77 To this purpose, there is a document ghc.pdf built in docs/core-spec that
78 contains a formalism of the types and functions dealt with here. If you change
79 just about anything in this file or you change other types/functions throughout
80 the Core language (all signposted to this note), you should update that
81 formalism. See docs/core-spec/README for more info about how to do so.
82
83 Summary of checks
84 ~~~~~~~~~~~~~~~~~
85 Checks that a set of core bindings is well-formed. The PprStyle and String
86 just control what we print in the event of an error. The Bool value
87 indicates whether we have done any specialisation yet (in which case we do
88 some extra checks).
89
90 We check for
91 (a) type errors
92 (b) Out-of-scope type variables
93 (c) Out-of-scope local variables
94 (d) Ill-kinded types
95 (e) Incorrect unsafe coercions
96
97 If we have done specialisation the we check that there are
98 (a) No top-level bindings of primitive (unboxed type)
99
100 Outstanding issues:
101
102 -- Things are *not* OK if:
103 --
104 -- * Unsaturated type app before specialisation has been done;
105 --
106 -- * Oversaturated type app after specialisation (eta reduction
107 -- may well be happening...);
108
109
110 Note [Linting type lets]
111 ~~~~~~~~~~~~~~~~~~~~~~~~
112 In the desugarer, it's very very convenient to be able to say (in effect)
113 let a = Type Int in <body>
114 That is, use a type let. See Note [Type let] in CoreSyn.
115
116 However, when linting <body> we need to remember that a=Int, else we might
117 reject a correct program. So we carry a type substitution (in this example
118 [a -> Int]) and apply this substitution before comparing types. The functin
119 lintInTy :: Type -> LintM Type
120 returns a substituted type; that's the only reason it returns anything.
121
122 When we encounter a binder (like x::a) we must apply the substitution
123 to the type of the binding variable. lintBinders does this.
124
125 For Ids, the type-substituted Id is added to the in_scope set (which
126 itself is part of the TvSubst we are carrying down), and when we
127 find an occurrence of an Id, we fetch it from the in-scope set.
128
129 Note [Bad unsafe coercion]
130 ~~~~~~~~~~~~~~~~~~~~~~~~~~
131
132 For discussion see https://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions
133 Linter introduces additional rules that checks improper coercion between
134 different types, called bad coercions. Following coercions are forbidden:
135
136 (a) coercions between boxed and unboxed values;
137 (b) coercions between unlifted values of the different sizes, here
138 active size is checked, i.e. size of the actual value but not
139 the space allocated for value;
140 (c) coercions between floating and integral boxed values, this check
141 is not yet supported for unboxed tuples, as no semantics were
142 specified for that;
143 (d) coercions from / to vector type
144 (e) If types are unboxed tuples then tuple (# A_1,..,A_n #) can be
145 coerced to (# B_1,..,B_m #) if n=m and for each pair A_i, B_i rules
146 (a-e) holds.
147
148 ************************************************************************
149 * *
150 Beginning and ending passes
151 * *
152 ************************************************************************
153
154 These functions are not CoreM monad stuff, but they probably ought to
155 be, and it makes a conveneint place. place for them. They print out
156 stuff before and after core passes, and do Core Lint when necessary.
157 -}
158
159 showPass :: CoreToDo -> CoreM ()
160 showPass pass = do { dflags <- getDynFlags
161 ; liftIO $ showPassIO dflags pass }
162
163 showPassIO :: DynFlags -> CoreToDo -> IO ()
164 showPassIO dflags pass = Err.showPass dflags (showPpr dflags pass)
165
166 endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> CoreM ()
167 endPass pass binds rules
168 = do { hsc_env <- getHscEnv
169 ; print_unqual <- getPrintUnqualified
170 ; liftIO $ endPassIO hsc_env print_unqual pass binds rules }
171
172 endPassIO :: HscEnv -> PrintUnqualified
173 -> CoreToDo -> CoreProgram -> [CoreRule] -> IO ()
174 -- Used by the IO-is CorePrep too
175 endPassIO hsc_env print_unqual pass binds rules
176 = do { dumpPassResult dflags print_unqual mb_flag
177 (ppr pass) (pprPassDetails pass) binds rules
178 ; lintPassResult hsc_env pass binds }
179 where
180 dflags = hsc_dflags hsc_env
181 mb_flag = case coreDumpFlag pass of
182 Just flag | dopt flag dflags -> Just flag
183 | dopt Opt_D_verbose_core2core dflags -> Just flag
184 _ -> Nothing
185
186 dumpIfSet :: DynFlags -> Bool -> CoreToDo -> SDoc -> SDoc -> IO ()
187 dumpIfSet dflags dump_me pass extra_info doc
188 = Err.dumpIfSet dflags dump_me (showSDoc dflags (ppr pass <+> extra_info)) doc
189
190 dumpPassResult :: DynFlags
191 -> PrintUnqualified
192 -> Maybe DumpFlag -- Just df => show details in a file whose
193 -- name is specified by df
194 -> SDoc -- Header
195 -> SDoc -- Extra info to appear after header
196 -> CoreProgram -> [CoreRule]
197 -> IO ()
198 dumpPassResult dflags unqual mb_flag hdr extra_info binds rules
199 | Just flag <- mb_flag
200 = Err.dumpSDoc dflags unqual flag (showSDoc dflags hdr) dump_doc
201
202 | otherwise
203 = Err.debugTraceMsg dflags 2 size_doc
204 -- Report result size
205 -- This has the side effect of forcing the intermediate to be evaluated
206
207 where
208 size_doc = sep [text "Result size of" <+> hdr, nest 2 (equals <+> ppr (coreBindsStats binds))]
209
210 dump_doc = vcat [ nest 2 extra_info
211 , size_doc
212 , blankLine
213 , pprCoreBindingsWithSize binds
214 , ppUnless (null rules) pp_rules ]
215 pp_rules = vcat [ blankLine
216 , ptext (sLit "------ Local rules for imported ids --------")
217 , pprRules rules ]
218
219 coreDumpFlag :: CoreToDo -> Maybe DumpFlag
220 coreDumpFlag (CoreDoSimplify {}) = Just Opt_D_verbose_core2core
221 coreDumpFlag (CoreDoPluginPass {}) = Just Opt_D_verbose_core2core
222 coreDumpFlag CoreDoFloatInwards = Just Opt_D_verbose_core2core
223 coreDumpFlag (CoreDoFloatOutwards {}) = Just Opt_D_verbose_core2core
224 coreDumpFlag CoreLiberateCase = Just Opt_D_verbose_core2core
225 coreDumpFlag CoreDoStaticArgs = Just Opt_D_verbose_core2core
226 coreDumpFlag CoreDoCallArity = Just Opt_D_dump_call_arity
227 coreDumpFlag CoreDoStrictness = Just Opt_D_dump_stranal
228 coreDumpFlag CoreDoWorkerWrapper = Just Opt_D_dump_worker_wrapper
229 coreDumpFlag CoreDoSpecialising = Just Opt_D_dump_spec
230 coreDumpFlag CoreDoSpecConstr = Just Opt_D_dump_spec
231 coreDumpFlag CoreCSE = Just Opt_D_dump_cse
232 coreDumpFlag CoreDoVectorisation = Just Opt_D_dump_vect
233 coreDumpFlag CoreDesugar = Just Opt_D_dump_ds
234 coreDumpFlag CoreDesugarOpt = Just Opt_D_dump_ds
235 coreDumpFlag CoreTidy = Just Opt_D_dump_simpl
236 coreDumpFlag CorePrep = Just Opt_D_dump_prep
237
238 coreDumpFlag CoreDoPrintCore = Nothing
239 coreDumpFlag (CoreDoRuleCheck {}) = Nothing
240 coreDumpFlag CoreDoNothing = Nothing
241 coreDumpFlag (CoreDoPasses {}) = Nothing
242
243 {-
244 ************************************************************************
245 * *
246 Top-level interfaces
247 * *
248 ************************************************************************
249 -}
250
251 lintPassResult :: HscEnv -> CoreToDo -> CoreProgram -> IO ()
252 lintPassResult hsc_env pass binds
253 | not (gopt Opt_DoCoreLinting dflags)
254 = return ()
255 | otherwise
256 = do { let (warns, errs) = lintCoreBindings dflags pass (interactiveInScope hsc_env) binds
257 ; Err.showPass dflags ("Core Linted result of " ++ showPpr dflags pass)
258 ; displayLintResults dflags pass warns errs binds }
259 where
260 dflags = hsc_dflags hsc_env
261
262 displayLintResults :: DynFlags -> CoreToDo
263 -> Bag Err.MsgDoc -> Bag Err.MsgDoc -> CoreProgram
264 -> IO ()
265 displayLintResults dflags pass warns errs binds
266 | not (isEmptyBag errs)
267 = do { log_action dflags dflags Err.SevDump noSrcSpan defaultDumpStyle
268 (vcat [ lint_banner "errors" (ppr pass), Err.pprMessageBag errs
269 , ptext (sLit "*** Offending Program ***")
270 , pprCoreBindings binds
271 , ptext (sLit "*** End of Offense ***") ])
272 ; Err.ghcExit dflags 1 }
273
274 | not (isEmptyBag warns)
275 , not opt_NoDebugOutput
276 , showLintWarnings pass
277 = log_action dflags dflags Err.SevDump noSrcSpan defaultDumpStyle
278 (lint_banner "warnings" (ppr pass) $$ Err.pprMessageBag warns)
279
280 | otherwise = return ()
281 where
282
283 lint_banner :: String -> SDoc -> SDoc
284 lint_banner string pass = ptext (sLit "*** Core Lint") <+> text string
285 <+> ptext (sLit ": in result of") <+> pass
286 <+> ptext (sLit "***")
287
288 showLintWarnings :: CoreToDo -> Bool
289 -- Disable Lint warnings on the first simplifier pass, because
290 -- there may be some INLINE knots still tied, which is tiresomely noisy
291 showLintWarnings (CoreDoSimplify _ (SimplMode { sm_phase = InitialPhase })) = False
292 showLintWarnings _ = True
293
294 lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO ()
295 lintInteractiveExpr what hsc_env expr
296 | not (gopt Opt_DoCoreLinting dflags)
297 = return ()
298 | Just err <- lintExpr dflags (interactiveInScope hsc_env) expr
299 = do { display_lint_err err
300 ; Err.ghcExit dflags 1 }
301 | otherwise
302 = return ()
303 where
304 dflags = hsc_dflags hsc_env
305
306 display_lint_err err
307 = do { log_action dflags dflags Err.SevDump noSrcSpan defaultDumpStyle
308 (vcat [ lint_banner "errors" (text what)
309 , err
310 , ptext (sLit "*** Offending Program ***")
311 , pprCoreExpr expr
312 , ptext (sLit "*** End of Offense ***") ])
313 ; Err.ghcExit dflags 1 }
314
315 interactiveInScope :: HscEnv -> [Var]
316 -- In GHCi we may lint expressions, or bindings arising from 'deriving'
317 -- clauses, that mention variables bound in the interactive context.
318 -- These are Local things (see Note [Interactively-bound Ids in GHCi] in HscTypes).
319 -- So we have to tell Lint about them, lest it reports them as out of scope.
320 --
321 -- We do this by find local-named things that may appear free in interactive
322 -- context. This function is pretty revolting and quite possibly not quite right.
323 -- When we are not in GHCi, the interactive context (hsc_IC hsc_env) is empty
324 -- so this is a (cheap) no-op.
325 --
326 -- See Trac #8215 for an example
327 interactiveInScope hsc_env
328 = varSetElems tyvars ++ ids
329 where
330 -- C.f. TcRnDriver.setInteractiveContext, Desugar.deSugarExpr
331 ictxt = hsc_IC hsc_env
332 (cls_insts, _fam_insts) = ic_instances ictxt
333 te1 = mkTypeEnvWithImplicits (ic_tythings ictxt)
334 te = extendTypeEnvWithIds te1 (map instanceDFunId cls_insts)
335 ids = typeEnvIds te
336 tyvars = mapUnionVarSet (tyVarsOfType . idType) ids
337 -- Why the type variables? How can the top level envt have free tyvars?
338 -- I think it's because of the GHCi debugger, which can bind variables
339 -- f :: [t] -> [t]
340 -- where t is a RuntimeUnk (see TcType)
341
342 lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
343 -- Returns (warnings, errors)
344 -- If you edit this function, you may need to update the GHC formalism
345 -- See Note [GHC Formalism]
346 lintCoreBindings dflags pass local_in_scope binds
347 = initL dflags flags $
348 addLoc TopLevelBindings $
349 addInScopeVars local_in_scope $
350 addInScopeVars binders $
351 -- Put all the top-level binders in scope at the start
352 -- This is because transformation rules can bring something
353 -- into use 'unexpectedly'
354 do { checkL (null dups) (dupVars dups)
355 ; checkL (null ext_dups) (dupExtVars ext_dups)
356 ; mapM lint_bind binds }
357 where
358 flags = LF { lf_check_global_ids = check_globals
359 , lf_check_inline_loop_breakers = check_lbs }
360
361 -- See Note [Checking for global Ids]
362 check_globals = case pass of
363 CoreTidy -> False
364 CorePrep -> False
365 _ -> True
366
367 -- See Note [Checking for INLINE loop breakers]
368 check_lbs = case pass of
369 CoreDesugar -> False
370 CoreDesugarOpt -> False
371 _ -> True
372
373 binders = bindersOfBinds binds
374 (_, dups) = removeDups compare binders
375
376 -- dups_ext checks for names with different uniques
377 -- but but the same External name M.n. We don't
378 -- allow this at top level:
379 -- M.n{r3} = ...
380 -- M.n{r29} = ...
381 -- because they both get the same linker symbol
382 ext_dups = snd (removeDups ord_ext (map Var.varName binders))
383 ord_ext n1 n2 | Just m1 <- nameModule_maybe n1
384 , Just m2 <- nameModule_maybe n2
385 = compare (m1, nameOccName n1) (m2, nameOccName n2)
386 | otherwise = LT
387
388 -- If you edit this function, you may need to update the GHC formalism
389 -- See Note [GHC Formalism]
390 lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
391 lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
392
393 {-
394 ************************************************************************
395 * *
396 \subsection[lintUnfolding]{lintUnfolding}
397 * *
398 ************************************************************************
399
400 We use this to check all unfoldings that come in from interfaces
401 (it is very painful to catch errors otherwise):
402 -}
403
404 lintUnfolding :: DynFlags
405 -> SrcLoc
406 -> [Var] -- Treat these as in scope
407 -> CoreExpr
408 -> Maybe MsgDoc -- Nothing => OK
409
410 lintUnfolding dflags locn vars expr
411 | isEmptyBag errs = Nothing
412 | otherwise = Just (pprMessageBag errs)
413 where
414 (_warns, errs) = initL dflags defaultLintFlags linter
415 linter = addLoc (ImportedUnfolding locn) $
416 addInScopeVars vars $
417 lintCoreExpr expr
418
419 lintExpr :: DynFlags
420 -> [Var] -- Treat these as in scope
421 -> CoreExpr
422 -> Maybe MsgDoc -- Nothing => OK
423
424 lintExpr dflags vars expr
425 | isEmptyBag errs = Nothing
426 | otherwise = Just (pprMessageBag errs)
427 where
428 (_warns, errs) = initL dflags defaultLintFlags linter
429 linter = addLoc TopLevelBindings $
430 addInScopeVars vars $
431 lintCoreExpr expr
432
433 {-
434 ************************************************************************
435 * *
436 \subsection[lintCoreBinding]{lintCoreBinding}
437 * *
438 ************************************************************************
439
440 Check a core binding, returning the list of variables bound.
441 -}
442
443 lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
444 -- If you edit this function, you may need to update the GHC formalism
445 -- See Note [GHC Formalism]
446 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
447 = addLoc (RhsOf binder) $
448 -- Check the rhs
449 do { ty <- lintCoreExpr rhs
450 ; lintBinder binder -- Check match to RHS type
451 ; binder_ty <- applySubstTy (idType binder)
452 ; checkTys binder_ty ty (mkRhsMsg binder (ptext (sLit "RHS")) ty)
453
454 -- Check the let/app invariant
455 -- See Note [CoreSyn let/app invariant] in CoreSyn
456 ; checkL (not (isUnLiftedType binder_ty)
457 || (isNonRec rec_flag && exprOkForSpeculation rhs))
458 (mkRhsPrimMsg binder rhs)
459
460 -- Check that if the binder is top-level or recursive, it's not demanded
461 ; checkL (not (isStrictId binder)
462 || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
463 (mkStrictMsg binder)
464
465 -- Check that if the binder is local, it is not marked as exported
466 ; checkL (not (isExportedId binder) || isTopLevel top_lvl_flag)
467 (mkNonTopExportedMsg binder)
468
469 -- Check that if the binder is local, it does not have an external name
470 ; checkL (not (isExternalName (Var.varName binder)) || isTopLevel top_lvl_flag)
471 (mkNonTopExternalNameMsg binder)
472
473 ; flags <- getLintFlags
474 ; when (lf_check_inline_loop_breakers flags
475 && isStrongLoopBreaker (idOccInfo binder)
476 && isInlinePragma (idInlinePragma binder))
477 (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
478 -- Only non-rule loop breakers inhibit inlining
479
480 -- Check whether arity and demand type are consistent (only if demand analysis
481 -- already happened)
482 --
483 -- Note (Apr 2014): this is actually ok. See Note [Demand analysis for trivial right-hand sides]
484 -- in DmdAnal. After eta-expansion in CorePrep the rhs is no longer trivial.
485 -- ; let dmdTy = idStrictness binder
486 -- ; checkL (case dmdTy of
487 -- StrictSig dmd_ty -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs)
488 -- (mkArityMsg binder)
489
490 -- Check that the binder's arity is within the bounds imposed by
491 -- the type and the strictness signature. See Note [exprArity invariant]
492 -- and Note [Trimming arity]
493 ; checkL (idArity binder <= length (typeArity (idType binder)))
494 (ptext (sLit "idArity") <+> ppr (idArity binder) <+>
495 ptext (sLit "exceeds typeArity") <+>
496 ppr (length (typeArity (idType binder))) <> colon <+>
497 ppr binder)
498
499 ; case splitStrictSig (idStrictness binder) of
500 (demands, result_info) | isBotRes result_info ->
501 checkL (idArity binder <= length demands)
502 (ptext (sLit "idArity") <+> ppr (idArity binder) <+>
503 ptext (sLit "exceeds arity imposed by the strictness signature") <+>
504 ppr (idStrictness binder) <> colon <+>
505 ppr binder)
506 _ -> return ()
507
508 ; mapM_ (lintCoreRule binder_ty) (idCoreRules binder)
509 ; lintIdUnfolding binder binder_ty (idUnfolding binder) }
510
511 -- We should check the unfolding, if any, but this is tricky because
512 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
513 where
514 -- If you edit this function, you may need to update the GHC formalism
515 -- See Note [GHC Formalism]
516 lintBinder var | isId var = lintIdBndr var $ \_ -> (return ())
517 | otherwise = return ()
518
519 lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
520 lintIdUnfolding bndr bndr_ty (CoreUnfolding { uf_tmpl = rhs, uf_src = src })
521 | isStableSource src
522 = do { ty <- lintCoreExpr rhs
523 ; checkTys bndr_ty ty (mkRhsMsg bndr (ptext (sLit "unfolding")) ty) }
524 lintIdUnfolding _ _ _
525 = return () -- Do not Lint unstable unfoldings, becuase that leads
526 -- to exponential behaviour; c.f. CoreFVs.idUnfoldingVars
527
528 {-
529 Note [Checking for INLINE loop breakers]
530 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
531 It's very suspicious if a strong loop breaker is marked INLINE.
532
533 However, the desugarer generates instance methods with INLINE pragmas
534 that form a mutually recursive group. Only after a round of
535 simplification are they unravelled. So we suppress the test for
536 the desugarer.
537
538 ************************************************************************
539 * *
540 \subsection[lintCoreExpr]{lintCoreExpr}
541 * *
542 ************************************************************************
543 -}
544
545 --type InKind = Kind -- Substitution not yet applied
546 type InType = Type
547 type InCoercion = Coercion
548 type InVar = Var
549 type InTyVar = TyVar
550
551 type OutKind = Kind -- Substitution has been applied to this,
552 -- but has not been linted yet
553 type LintedKind = Kind -- Substitution applied, and type is linted
554
555 type OutType = Type -- Substitution has been applied to this,
556 -- but has not been linted yet
557
558 type LintedType = Type -- Substitution applied, and type is linted
559
560 type OutCoercion = Coercion
561 type OutVar = Var
562 type OutTyVar = TyVar
563
564 lintCoreExpr :: CoreExpr -> LintM OutType
565 -- The returned type has the substitution from the monad
566 -- already applied to it:
567 -- lintCoreExpr e subst = exprType (subst e)
568 --
569 -- The returned "type" can be a kind, if the expression is (Type ty)
570
571 -- If you edit this function, you may need to update the GHC formalism
572 -- See Note [GHC Formalism]
573 lintCoreExpr (Var var)
574 = do { checkL (not (var == oneTupleDataConId))
575 (ptext (sLit "Illegal one-tuple"))
576
577 ; checkL (isId var && not (isCoVar var))
578 (ptext (sLit "Non term variable") <+> ppr var)
579
580 ; checkDeadIdOcc var
581 ; var' <- lookupIdInScope var
582 ; return (idType var') }
583
584 lintCoreExpr (Lit lit)
585 = return (literalType lit)
586
587 lintCoreExpr (Cast expr co)
588 = do { expr_ty <- lintCoreExpr expr
589 ; co' <- applySubstCo co
590 ; (_, from_ty, to_ty, r) <- lintCoercion co'
591 ; checkRole co' Representational r
592 ; checkTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
593 ; return to_ty }
594
595 lintCoreExpr (Tick (Breakpoint _ ids) expr)
596 = do forM_ ids $ \id -> do
597 checkDeadIdOcc id
598 lookupIdInScope id
599 lintCoreExpr expr
600
601 lintCoreExpr (Tick _other_tickish expr)
602 = lintCoreExpr expr
603
604 lintCoreExpr (Let (NonRec tv (Type ty)) body)
605 | isTyVar tv
606 = -- See Note [Linting type lets]
607 do { ty' <- applySubstTy ty
608 ; lintTyBndr tv $ \ tv' ->
609 do { addLoc (RhsOf tv) $ checkTyKind tv' ty'
610 -- Now extend the substitution so we
611 -- take advantage of it in the body
612 ; extendSubstL tv' ty' $
613 addLoc (BodyOfLetRec [tv]) $
614 lintCoreExpr body } }
615
616 lintCoreExpr (Let (NonRec bndr rhs) body)
617 | isId bndr
618 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
619 ; addLoc (BodyOfLetRec [bndr])
620 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
621
622 | otherwise
623 = failWithL (mkLetErr bndr rhs) -- Not quite accurate
624
625 lintCoreExpr (Let (Rec pairs) body)
626 = lintAndScopeIds bndrs $ \_ ->
627 do { checkL (null dups) (dupVars dups)
628 ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
629 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
630 where
631 bndrs = map fst pairs
632 (_, dups) = removeDups compare bndrs
633
634 lintCoreExpr e@(App _ _)
635 = do { fun_ty <- lintCoreExpr fun
636 ; addLoc (AnExpr e) $ foldM lintCoreArg fun_ty args }
637 where
638 (fun, args) = collectArgs e
639
640 lintCoreExpr (Lam var expr)
641 = addLoc (LambdaBodyOf var) $
642 lintBinder var $ \ var' ->
643 do { body_ty <- lintCoreExpr expr
644 ; if isId var' then
645 return (mkFunTy (idType var') body_ty)
646 else
647 return (mkForAllTy var' body_ty)
648 }
649 -- The applySubstTy is needed to apply the subst to var
650
651 lintCoreExpr e@(Case scrut var alt_ty alts) =
652 -- Check the scrutinee
653 do { scrut_ty <- lintCoreExpr scrut
654 ; alt_ty <- lintInTy alt_ty
655 ; var_ty <- lintInTy (idType var)
656
657 -- See Note [No alternatives lint check]
658 ; when (null alts) $
659 do { checkL (not (exprIsHNF scrut))
660 (ptext (sLit "No alternatives for a case scrutinee in head-normal form:") <+> ppr scrut)
661 ; checkL (exprIsBottom scrut)
662 (ptext (sLit "No alternatives for a case scrutinee not known to diverge for sure:") <+> ppr scrut)
663 }
664
665 ; case tyConAppTyCon_maybe (idType var) of
666 Just tycon
667 | debugIsOn &&
668 isAlgTyCon tycon &&
669 not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
670 null (tyConDataCons tycon) ->
671 pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
672 -- This can legitimately happen for type families
673 $ return ()
674 _otherwise -> return ()
675
676 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
677
678 ; subst <- getTvSubst
679 ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
680
681 ; lintAndScopeId var $ \_ ->
682 do { -- Check the alternatives
683 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
684 ; checkCaseAlts e scrut_ty alts
685 ; return alt_ty } }
686
687 -- This case can't happen; linting types in expressions gets routed through
688 -- lintCoreArgs
689 lintCoreExpr (Type ty)
690 = failWithL (ptext (sLit "Type found as expression") <+> ppr ty)
691
692 lintCoreExpr (Coercion co)
693 = do { (_kind, ty1, ty2, role) <- lintInCo co
694 ; return (mkCoercionType role ty1 ty2) }
695
696 {-
697 Note [Kind instantiation in coercions]
698 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
699 Consider the following coercion axiom:
700 ax_co [(k_ag :: BOX), (f_aa :: k_ag -> Constraint)] :: T k_ag f_aa ~ f_aa
701
702 Consider the following instantiation:
703 ax_co <* -> *> <Monad>
704
705 We need to split the co_ax_tvs into kind and type variables in order
706 to find out the coercion kind instantiations. Those can only be Refl
707 since we don't have kind coercions. This is just a way to represent
708 kind instantiation.
709
710 We use the number of kind variables to know how to split the coercions
711 instantiations between kind coercions and type coercions. We lint the
712 kind coercions and produce the following substitution which is to be
713 applied in the type variables:
714 k_ag ~~> * -> *
715
716 Note [No alternatives lint check]
717 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
718 Case expressions with no alternatives are odd beasts, and worth looking at
719 in the linter (cf Trac #10180). We check two things:
720
721 * exprIsHNF is false: certainly, it would be terribly wrong if the
722 scrutinee was already in head normal form.
723
724 * exprIsBottom is true: we should be able to see why GHC believes the
725 scrutinee is diverging for sure.
726
727 In principle, the first check is redundant: exprIsBottom == True will
728 always imply exprIsHNF == False. But the first check is reliable: If
729 exprIsHNF == True, then there definitely is a problem (exprIsHNF errs
730 on the right side). If the second check triggers then it may be the
731 case that the compiler got smarter elsewhere, and the empty case is
732 correct, but that exprIsBottom is unable to see it. In particular, the
733 empty-type check in exprIsBottom is an approximation. Therefore, this
734 check is not fully reliable, and we keep both around.
735
736 ************************************************************************
737 * *
738 \subsection[lintCoreArgs]{lintCoreArgs}
739 * *
740 ************************************************************************
741
742 The basic version of these functions checks that the argument is a
743 subtype of the required type, as one would expect.
744 -}
745
746 lintCoreArg :: OutType -> CoreArg -> LintM OutType
747 lintCoreArg fun_ty (Type arg_ty)
748 = do { arg_ty' <- applySubstTy arg_ty
749 ; lintTyApp fun_ty arg_ty' }
750
751 lintCoreArg fun_ty arg
752 = do { arg_ty <- lintCoreExpr arg
753 ; checkL (not (isUnLiftedType arg_ty) || exprOkForSpeculation arg)
754 (mkLetAppMsg arg)
755 ; lintValApp arg fun_ty arg_ty }
756
757 -----------------
758 lintAltBinders :: OutType -- Scrutinee type
759 -> OutType -- Constructor type
760 -> [OutVar] -- Binders
761 -> LintM ()
762 -- If you edit this function, you may need to update the GHC formalism
763 -- See Note [GHC Formalism]
764 lintAltBinders scrut_ty con_ty []
765 = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
766 lintAltBinders scrut_ty con_ty (bndr:bndrs)
767 | isTyVar bndr
768 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
769 ; lintAltBinders scrut_ty con_ty' bndrs }
770 | otherwise
771 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
772 ; lintAltBinders scrut_ty con_ty' bndrs }
773
774 -----------------
775 lintTyApp :: OutType -> OutType -> LintM OutType
776 lintTyApp fun_ty arg_ty
777 | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
778 , isTyVar tyvar
779 = do { checkTyKind tyvar arg_ty
780 ; return (substTyWith [tyvar] [arg_ty] body_ty) }
781
782 | otherwise
783 = failWithL (mkTyAppMsg fun_ty arg_ty)
784
785 -----------------
786 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
787 lintValApp arg fun_ty arg_ty
788 | Just (arg,res) <- splitFunTy_maybe fun_ty
789 = do { checkTys arg arg_ty err1
790 ; return res }
791 | otherwise
792 = failWithL err2
793 where
794 err1 = mkAppMsg fun_ty arg_ty arg
795 err2 = mkNonFunAppMsg fun_ty arg_ty arg
796
797 checkTyKind :: OutTyVar -> OutType -> LintM ()
798 -- Both args have had substitution applied
799
800 -- If you edit this function, you may need to update the GHC formalism
801 -- See Note [GHC Formalism]
802 checkTyKind tyvar arg_ty
803 | isSuperKind tyvar_kind -- kind forall
804 = lintKind arg_ty
805 -- Arg type might be boxed for a function with an uncommitted
806 -- tyvar; notably this is used so that we can give
807 -- error :: forall a:*. String -> a
808 -- and then apply it to both boxed and unboxed types.
809 | otherwise -- type forall
810 = do { arg_kind <- lintType arg_ty
811 ; unless (arg_kind `isSubKind` tyvar_kind)
812 (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
813 where
814 tyvar_kind = tyVarKind tyvar
815
816 checkDeadIdOcc :: Id -> LintM ()
817 -- Occurrences of an Id should never be dead....
818 -- except when we are checking a case pattern
819 checkDeadIdOcc id
820 | isDeadOcc (idOccInfo id)
821 = do { in_case <- inCasePat
822 ; checkL in_case
823 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
824 | otherwise
825 = return ()
826
827 {-
828 ************************************************************************
829 * *
830 \subsection[lintCoreAlts]{lintCoreAlts}
831 * *
832 ************************************************************************
833 -}
834
835 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
836 -- a) Check that the alts are non-empty
837 -- b1) Check that the DEFAULT comes first, if it exists
838 -- b2) Check that the others are in increasing order
839 -- c) Check that there's a default for infinite types
840 -- NB: Algebraic cases are not necessarily exhaustive, because
841 -- the simplifer correctly eliminates case that can't
842 -- possibly match.
843
844 checkCaseAlts e ty alts =
845 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
846 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
847
848 -- For types Int#, Word# with an infinite (well, large!) number of
849 -- possible values, there should usually be a DEFAULT case
850 -- But (see Note [Empty case alternatives] in CoreSyn) it's ok to
851 -- have *no* case alternatives.
852 -- In effect, this is a kind of partial test. I suppose it's possible
853 -- that we might *know* that 'x' was 1 or 2, in which case
854 -- case x of { 1 -> e1; 2 -> e2 }
855 -- would be fine.
856 ; checkL (isJust maybe_deflt || not is_infinite_ty || null alts)
857 (nonExhaustiveAltsMsg e) }
858 where
859 (con_alts, maybe_deflt) = findDefault alts
860
861 -- Check that successive alternatives have increasing tags
862 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
863 increasing_tag _ = True
864
865 non_deflt (DEFAULT, _, _) = False
866 non_deflt _ = True
867
868 is_infinite_ty = case tyConAppTyCon_maybe ty of
869 Nothing -> False
870 Just tycon -> isPrimTyCon tycon
871
872 checkAltExpr :: CoreExpr -> OutType -> LintM ()
873 checkAltExpr expr ann_ty
874 = do { actual_ty <- lintCoreExpr expr
875 ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
876
877 lintCoreAlt :: OutType -- Type of scrutinee
878 -> OutType -- Type of the alternative
879 -> CoreAlt
880 -> LintM ()
881 -- If you edit this function, you may need to update the GHC formalism
882 -- See Note [GHC Formalism]
883 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
884 do { checkL (null args) (mkDefaultArgsMsg args)
885 ; checkAltExpr rhs alt_ty }
886
887 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
888 | litIsLifted lit
889 = failWithL integerScrutinisedMsg
890 | otherwise
891 = do { checkL (null args) (mkDefaultArgsMsg args)
892 ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
893 ; checkAltExpr rhs alt_ty }
894 where
895 lit_ty = literalType lit
896
897 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
898 | isNewTyCon (dataConTyCon con)
899 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
900 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
901 = addLoc (CaseAlt alt) $ do
902 { -- First instantiate the universally quantified
903 -- type variables of the data constructor
904 -- We've already check
905 checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
906 ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
907
908 -- And now bring the new binders into scope
909 ; lintBinders args $ \ args' -> do
910 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
911 ; checkAltExpr rhs alt_ty } }
912
913 | otherwise -- Scrut-ty is wrong shape
914 = addErrL (mkBadAltMsg scrut_ty alt)
915
916 {-
917 ************************************************************************
918 * *
919 \subsection[lint-types]{Types}
920 * *
921 ************************************************************************
922 -}
923
924 -- When we lint binders, we (one at a time and in order):
925 -- 1. Lint var types or kinds (possibly substituting)
926 -- 2. Add the binder to the in scope set, and if its a coercion var,
927 -- we may extend the substitution to reflect its (possibly) new kind
928 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
929 lintBinders [] linterF = linterF []
930 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
931 lintBinders vars $ \ vars' ->
932 linterF (var':vars')
933
934 -- If you edit this function, you may need to update the GHC formalism
935 -- See Note [GHC Formalism]
936 lintBinder :: Var -> (Var -> LintM a) -> LintM a
937 lintBinder var linterF
938 | isId var = lintIdBndr var linterF
939 | otherwise = lintTyBndr var linterF
940
941 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
942 lintTyBndr tv thing_inside
943 = do { subst <- getTvSubst
944 ; let (subst', tv') = Type.substTyVarBndr subst tv
945 ; lintTyBndrKind tv'
946 ; updateTvSubst subst' (thing_inside tv') }
947
948 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
949 -- Do substitution on the type of a binder and add the var with this
950 -- new type to the in-scope set of the second argument
951 -- ToDo: lint its rules
952
953 lintIdBndr id linterF
954 = do { lintAndScopeId id $ \id' -> linterF id' }
955
956 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
957 lintAndScopeIds ids linterF
958 = go ids
959 where
960 go [] = linterF []
961 go (id:ids) = lintAndScopeId id $ \id ->
962 lintAndScopeIds ids $ \ids ->
963 linterF (id:ids)
964
965 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
966 lintAndScopeId id linterF
967 = do { flags <- getLintFlags
968 ; checkL (not (lf_check_global_ids flags) || isLocalId id)
969 (ptext (sLit "Non-local Id binder") <+> ppr id)
970 -- See Note [Checking for global Ids]
971 ; ty <- lintInTy (idType id)
972 ; let id' = setIdType id ty
973 ; addInScopeVar id' $ (linterF id') }
974
975 {-
976 ************************************************************************
977 * *
978 Types and kinds
979 * *
980 ************************************************************************
981
982 We have a single linter for types and kinds. That is convenient
983 because sometimes it's not clear whether the thing we are looking
984 at is a type or a kind.
985 -}
986
987 lintInTy :: InType -> LintM LintedType
988 -- Types only, not kinds
989 -- Check the type, and apply the substitution to it
990 -- See Note [Linting type lets]
991 lintInTy ty
992 = addLoc (InType ty) $
993 do { ty' <- applySubstTy ty
994 ; _k <- lintType ty'
995 ; return ty' }
996
997 -------------------
998 lintTyBndrKind :: OutTyVar -> LintM ()
999 -- Handles both type and kind foralls.
1000 lintTyBndrKind tv = lintKind (tyVarKind tv)
1001
1002 -------------------
1003 lintType :: OutType -> LintM LintedKind
1004 -- The returned Kind has itself been linted
1005
1006 -- If you edit this function, you may need to update the GHC formalism
1007 -- See Note [GHC Formalism]
1008 lintType (TyVarTy tv)
1009 = do { checkTyCoVarInScope tv
1010 ; return (tyVarKind tv) }
1011 -- We checked its kind when we added it to the envt
1012
1013 lintType ty@(AppTy t1 t2)
1014 = do { k1 <- lintType t1
1015 ; k2 <- lintType t2
1016 ; lint_ty_app ty k1 [(t2,k2)] }
1017
1018 lintType ty@(FunTy t1 t2) -- (->) has two different rules, for types and kinds
1019 = do { k1 <- lintType t1
1020 ; k2 <- lintType t2
1021 ; lintArrow (ptext (sLit "type or kind") <+> quotes (ppr ty)) k1 k2 }
1022
1023 lintType ty@(TyConApp tc tys)
1024 | Just ty' <- coreView ty
1025 = lintType ty' -- Expand type synonyms, so that we do not bogusly complain
1026 -- about un-saturated type synonyms
1027
1028 | isUnLiftedTyCon tc || isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
1029 -- See Note [The kind invariant] in TypeRep
1030 -- Also type synonyms and type families
1031 , length tys < tyConArity tc
1032 = failWithL (hang (ptext (sLit "Un-saturated type application")) 2 (ppr ty))
1033
1034 | otherwise
1035 = do { ks <- mapM lintType tys
1036 ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
1037
1038 lintType (ForAllTy tv ty)
1039 = do { lintTyBndrKind tv
1040 ; addInScopeVar tv (lintType ty) }
1041
1042 lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
1043
1044 lintKind :: OutKind -> LintM ()
1045 -- If you edit this function, you may need to update the GHC formalism
1046 -- See Note [GHC Formalism]
1047 lintKind k = do { sk <- lintType k
1048 ; unless (isSuperKind sk)
1049 (addErrL (hang (ptext (sLit "Ill-kinded kind:") <+> ppr k)
1050 2 (ptext (sLit "has kind:") <+> ppr sk))) }
1051
1052 lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
1053 -- If you edit this function, you may need to update the GHC formalism
1054 -- See Note [GHC Formalism]
1055 lintArrow what k1 k2 -- Eg lintArrow "type or kind `blah'" k1 k2
1056 -- or lintarrow "coercion `blah'" k1 k2
1057 | isSuperKind k1
1058 = return superKind
1059 | otherwise
1060 = do { unless (okArrowArgKind k1) (addErrL (msg (ptext (sLit "argument")) k1))
1061 ; unless (okArrowResultKind k2) (addErrL (msg (ptext (sLit "result")) k2))
1062 ; return liftedTypeKind }
1063 where
1064 msg ar k
1065 = vcat [ hang (ptext (sLit "Ill-kinded") <+> ar)
1066 2 (ptext (sLit "in") <+> what)
1067 , what <+> ptext (sLit "kind:") <+> ppr k ]
1068
1069 lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
1070 lint_ty_app ty k tys
1071 = lint_app (ptext (sLit "type") <+> quotes (ppr ty)) k tys
1072
1073 ----------------
1074 lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
1075 lint_co_app ty k tys
1076 = lint_app (ptext (sLit "coercion") <+> quotes (ppr ty)) k tys
1077
1078 ----------------
1079 lintTyLit :: TyLit -> LintM ()
1080 lintTyLit (NumTyLit n)
1081 | n >= 0 = return ()
1082 | otherwise = failWithL msg
1083 where msg = ptext (sLit "Negative type literal:") <+> integer n
1084 lintTyLit (StrTyLit _) = return ()
1085
1086 lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
1087 -- (lint_app d fun_kind arg_tys)
1088 -- We have an application (f arg_ty1 .. arg_tyn),
1089 -- where f :: fun_kind
1090 -- Takes care of linting the OutTypes
1091
1092 -- If you edit this function, you may need to update the GHC formalism
1093 -- See Note [GHC Formalism]
1094 lint_app doc kfn kas
1095 = foldlM go_app kfn kas
1096 where
1097 fail_msg = vcat [ hang (ptext (sLit "Kind application error in")) 2 doc
1098 , nest 2 (ptext (sLit "Function kind =") <+> ppr kfn)
1099 , nest 2 (ptext (sLit "Arg kinds =") <+> ppr kas) ]
1100
1101 go_app kfn ka
1102 | Just kfn' <- coreView kfn
1103 = go_app kfn' ka
1104
1105 go_app (FunTy kfa kfb) (_,ka)
1106 = do { unless (ka `isSubKind` kfa) (addErrL fail_msg)
1107 ; return kfb }
1108
1109 go_app (ForAllTy kv kfn) (ta,ka)
1110 = do { unless (ka `isSubKind` tyVarKind kv) (addErrL fail_msg)
1111 ; return (substKiWith [kv] [ta] kfn) }
1112
1113 go_app _ _ = failWithL fail_msg
1114
1115 {- *********************************************************************
1116 * *
1117 Linting rules
1118 * *
1119 ********************************************************************* -}
1120
1121 lintCoreRule :: OutType -> CoreRule -> LintM ()
1122 lintCoreRule _ (BuiltinRule {})
1123 = return () -- Don't bother
1124
1125 lintCoreRule fun_ty (Rule { ru_name = name, ru_bndrs = bndrs
1126 , ru_args = args, ru_rhs = rhs })
1127 = lintBinders bndrs $ \ _ ->
1128 do { lhs_ty <- foldM lintCoreArg fun_ty args
1129 ; rhs_ty <- lintCoreExpr rhs
1130 ; checkTys lhs_ty rhs_ty $
1131 (rule_doc <+> vcat [ ptext (sLit "lhs type:") <+> ppr lhs_ty
1132 , ptext (sLit "rhs type:") <+> ppr rhs_ty ])
1133 ; let bad_bndrs = filterOut (`elemVarSet` exprsFreeVars args) bndrs
1134 ; checkL (null bad_bndrs)
1135 (rule_doc <+> ptext (sLit "unbound") <+> ppr bad_bndrs)
1136 -- See Note [Linting rules]
1137 }
1138 where
1139 rule_doc = ptext (sLit "Rule") <+> doubleQuotes (ftext name) <> colon
1140
1141 {- Note [Linting rules]
1142 ~~~~~~~~~~~~~~~~~~~~~~~
1143 It's very bad if simplifying a rule means that one of the template
1144 variables (ru_bndrs) becomes not-mentioned in the template argumments
1145 (ru_args). How can that happen? Well, in Trac #10602, SpecConstr
1146 stupidly constructed a rule like
1147
1148 forall x,c1,c2.
1149 f (x |> c1 |> c2) = ....
1150
1151 But simplExpr collapses those coercions into one. (Indeed in
1152 Trac #10602, it collapsed to the identity and was removed altogether.)
1153
1154 We don't have a great story for what to do here, but at least
1155 this check will nail it.
1156 -}
1157
1158 {-
1159 ************************************************************************
1160 * *
1161 Linting coercions
1162 * *
1163 ************************************************************************
1164 -}
1165
1166 lintInCo :: InCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
1167 -- Check the coercion, and apply the substitution to it
1168 -- See Note [Linting type lets]
1169 lintInCo co
1170 = addLoc (InCo co) $
1171 do { co' <- applySubstCo co
1172 ; lintCoercion co' }
1173
1174 lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
1175 -- Check the kind of a coercion term, returning the kind
1176 -- Post-condition: the returned OutTypes are lint-free
1177 -- and have the same kind as each other
1178
1179 -- If you edit this function, you may need to update the GHC formalism
1180 -- See Note [GHC Formalism]
1181 lintCoercion (Refl r ty)
1182 = do { k <- lintType ty
1183 ; return (k, ty, ty, r) }
1184
1185 lintCoercion co@(TyConAppCo r tc cos)
1186 | tc `hasKey` funTyConKey
1187 , [co1,co2] <- cos
1188 = do { (k1,s1,t1,r1) <- lintCoercion co1
1189 ; (k2,s2,t2,r2) <- lintCoercion co2
1190 ; rk <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k1 k2
1191 ; checkRole co1 r r1
1192 ; checkRole co2 r r2
1193 ; return (rk, mkFunTy s1 s2, mkFunTy t1 t2, r) }
1194
1195 | Just {} <- synTyConDefn_maybe tc
1196 = failWithL (ptext (sLit "Synonym in TyConAppCo:") <+> ppr co)
1197
1198 | otherwise
1199 = do { (ks,ss,ts,rs) <- mapAndUnzip4M lintCoercion cos
1200 ; rk <- lint_co_app co (tyConKind tc) (ss `zip` ks)
1201 ; _ <- zipWith3M checkRole cos (tyConRolesX r tc) rs
1202 ; return (rk, mkTyConApp tc ss, mkTyConApp tc ts, r) }
1203
1204 lintCoercion co@(AppCo co1 co2)
1205 = do { (k1,s1,t1,r1) <- lintCoercion co1
1206 ; (k2,s2,t2,r2) <- lintCoercion co2
1207 ; rk <- lint_co_app co k1 [(s2,k2)]
1208 ; if r1 == Phantom
1209 then checkL (r2 == Phantom || r2 == Nominal)
1210 (ptext (sLit "Second argument in AppCo cannot be R:") $$
1211 ppr co)
1212 else checkRole co Nominal r2
1213 ; return (rk, mkAppTy s1 s2, mkAppTy t1 t2, r1) }
1214
1215 lintCoercion (ForAllCo tv co)
1216 = do { lintTyBndrKind tv
1217 ; (k, s, t, r) <- addInScopeVar tv (lintCoercion co)
1218 ; return (k, mkForAllTy tv s, mkForAllTy tv t, r) }
1219
1220 lintCoercion (CoVarCo cv)
1221 | not (isCoVar cv)
1222 = failWithL (hang (ptext (sLit "Bad CoVarCo:") <+> ppr cv)
1223 2 (ptext (sLit "With offending type:") <+> ppr (varType cv)))
1224 | otherwise
1225 = do { checkTyCoVarInScope cv
1226 ; cv' <- lookupIdInScope cv
1227 ; let (s,t) = coVarKind cv'
1228 k = typeKind s
1229 r = coVarRole cv'
1230 ; when (isSuperKind k) $
1231 do { checkL (r == Nominal) (hang (ptext (sLit "Non-nominal kind equality"))
1232 2 (ppr cv))
1233 ; checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality"))
1234 2 (ppr cv)) }
1235 ; return (k, s, t, r) }
1236
1237 -- See Note [Bad unsafe coercion]
1238 lintCoercion (UnivCo _prov r ty1 ty2)
1239 = do { k1 <- lintType ty1
1240 ; k2 <- lintType ty2
1241 -- ; unless (k1 `eqKind` k2) $
1242 -- failWithL (hang (ptext (sLit "Unsafe coercion changes kind"))
1243 -- 2 (ppr co))
1244 ; when (r /= Phantom && isSubOpenTypeKind k1 && isSubOpenTypeKind k2)
1245 (checkTypes ty1 ty2)
1246 ; return (k1, ty1, ty2, r) }
1247 where
1248 report s = hang (text $ "Unsafe coercion between " ++ s)
1249 2 (vcat [ text "From:" <+> ppr ty1
1250 , text " To:" <+> ppr ty2])
1251 isUnBoxed :: PrimRep -> Bool
1252 isUnBoxed PtrRep = False
1253 isUnBoxed _ = True
1254 checkTypes t1 t2
1255 = case (repType t1, repType t2) of
1256 (UnaryRep _, UnaryRep _) ->
1257 validateCoercion (typePrimRep t1)
1258 (typePrimRep t2)
1259 (UbxTupleRep rep1, UbxTupleRep rep2) -> do
1260 checkWarnL (length rep1 == length rep2)
1261 (report "unboxed tuples of different length")
1262 zipWithM_ checkTypes rep1 rep2
1263 _ -> addWarnL (report "unboxed tuple and ordinary type")
1264 validateCoercion :: PrimRep -> PrimRep -> LintM ()
1265 validateCoercion rep1 rep2
1266 = do { dflags <- getDynFlags
1267 ; checkWarnL (isUnBoxed rep1 == isUnBoxed rep2)
1268 (report "unboxed and boxed value")
1269 ; checkWarnL (TyCon.primRepSizeW dflags rep1
1270 == TyCon.primRepSizeW dflags rep2)
1271 (report "unboxed values of different size")
1272 ; let fl = liftM2 (==) (TyCon.primRepIsFloat rep1)
1273 (TyCon.primRepIsFloat rep2)
1274 ; case fl of
1275 Nothing -> addWarnL (report "vector types")
1276 Just False -> addWarnL (report "float and integral values")
1277 _ -> return ()
1278 }
1279
1280 lintCoercion (SymCo co)
1281 = do { (k, ty1, ty2, r) <- lintCoercion co
1282 ; return (k, ty2, ty1, r) }
1283
1284 lintCoercion co@(TransCo co1 co2)
1285 = do { (k1, ty1a, ty1b, r1) <- lintCoercion co1
1286 ; (_, ty2a, ty2b, r2) <- lintCoercion co2
1287 ; checkL (ty1b `eqType` ty2a)
1288 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
1289 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
1290 ; checkRole co r1 r2
1291 ; return (k1, ty1a, ty2b, r1) }
1292
1293 lintCoercion the_co@(NthCo n co)
1294 = do { (_,s,t,r) <- lintCoercion co
1295 ; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
1296 (Just (tc_s, tys_s), Just (tc_t, tys_t))
1297 | tc_s == tc_t
1298 , isInjectiveTyCon tc_s r
1299 -- see Note [NthCo and newtypes] in Coercion
1300 , tys_s `equalLength` tys_t
1301 , n < length tys_s
1302 -> return (ks, ts, tt, tr)
1303 where
1304 ts = getNth tys_s n
1305 tt = getNth tys_t n
1306 tr = nthRole r tc_s n
1307 ks = typeKind ts
1308
1309 _ -> failWithL (hang (ptext (sLit "Bad getNth:"))
1310 2 (ppr the_co $$ ppr s $$ ppr t)) }
1311
1312 lintCoercion the_co@(LRCo lr co)
1313 = do { (_,s,t,r) <- lintCoercion co
1314 ; checkRole co Nominal r
1315 ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
1316 (Just s_pr, Just t_pr)
1317 -> return (k, s_pick, t_pick, Nominal)
1318 where
1319 s_pick = pickLR lr s_pr
1320 t_pick = pickLR lr t_pr
1321 k = typeKind s_pick
1322
1323 _ -> failWithL (hang (ptext (sLit "Bad LRCo:"))
1324 2 (ppr the_co $$ ppr s $$ ppr t)) }
1325
1326 lintCoercion (InstCo co arg_ty)
1327 = do { (k,s,t,r) <- lintCoercion co
1328 ; arg_kind <- lintType arg_ty
1329 ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
1330 (Just (tv1,ty1), Just (tv2,ty2))
1331 | arg_kind `isSubKind` tyVarKind tv1
1332 -> return (k, substTyWith [tv1] [arg_ty] ty1,
1333 substTyWith [tv2] [arg_ty] ty2, r)
1334 | otherwise
1335 -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
1336 _ -> failWithL (ptext (sLit "Bad argument of inst")) }
1337
1338 lintCoercion co@(AxiomInstCo con ind cos)
1339 = do { unless (0 <= ind && ind < brListLength (coAxiomBranches con))
1340 (bad_ax (ptext (sLit "index out of range")))
1341 -- See Note [Kind instantiation in coercions]
1342 ; let CoAxBranch { cab_tvs = ktvs
1343 , cab_roles = roles
1344 , cab_lhs = lhs
1345 , cab_rhs = rhs } = coAxiomNthBranch con ind
1346 ; unless (equalLength ktvs cos) (bad_ax (ptext (sLit "lengths")))
1347 ; in_scope <- getInScope
1348 ; let empty_subst = mkTvSubst in_scope emptyTvSubstEnv
1349 ; (subst_l, subst_r) <- foldlM check_ki
1350 (empty_subst, empty_subst)
1351 (zip3 ktvs roles cos)
1352 ; let lhs' = Type.substTys subst_l lhs
1353 rhs' = Type.substTy subst_r rhs
1354 ; case checkAxInstCo co of
1355 Just bad_branch -> bad_ax $ ptext (sLit "inconsistent with") <+> (pprCoAxBranch (coAxiomTyCon con) bad_branch)
1356 Nothing -> return ()
1357 ; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs', coAxiomRole con) }
1358 where
1359 bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what)
1360 2 (ppr co))
1361
1362 check_ki (subst_l, subst_r) (ktv, role, co)
1363 = do { (k, t1, t2, r) <- lintCoercion co
1364 ; checkRole co role r
1365 ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)
1366 -- Using subst_l is ok, because subst_l and subst_r
1367 -- must agree on kind equalities
1368 ; unless (k `isSubKind` ktv_kind)
1369 (bad_ax (ptext (sLit "check_ki2") <+> vcat [ ppr co, ppr k, ppr ktv, ppr ktv_kind ] ))
1370 ; return (Type.extendTvSubst subst_l ktv t1,
1371 Type.extendTvSubst subst_r ktv t2) }
1372
1373 lintCoercion co@(SubCo co')
1374 = do { (k,s,t,r) <- lintCoercion co'
1375 ; checkRole co Nominal r
1376 ; return (k,s,t,Representational) }
1377
1378
1379 lintCoercion this@(AxiomRuleCo co ts cs)
1380 = do _ks <- mapM lintType ts
1381 eqs <- mapM lintCoercion cs
1382
1383 let tyNum = length ts
1384
1385 case compare (coaxrTypeArity co) tyNum of
1386 EQ -> return ()
1387 LT -> err "Too many type arguments"
1388 [ txt "expected" <+> int (coaxrTypeArity co)
1389 , txt "provided" <+> int tyNum ]
1390 GT -> err "Not enough type arguments"
1391 [ txt "expected" <+> int (coaxrTypeArity co)
1392 , txt "provided" <+> int tyNum ]
1393 checkRoles 0 (coaxrAsmpRoles co) eqs
1394
1395 case coaxrProves co ts [ Pair l r | (_,l,r,_) <- eqs ] of
1396 Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
1397 Just (Pair l r) ->
1398 do kL <- lintType l
1399 kR <- lintType r
1400 unless (eqKind kL kR)
1401 $ err "Kind error in CoAxiomRule"
1402 [ppr kL <+> txt "/=" <+> ppr kR]
1403 return (kL, l, r, coaxrRole co)
1404 where
1405 txt = ptext . sLit
1406 err m xs = failWithL $
1407 hang (txt m) 2 $ vcat (txt "Rule:" <+> ppr (coaxrName co) : xs)
1408
1409 checkRoles n (e : es) ((_,_,_,r) : rs)
1410 | e == r = checkRoles (n+1) es rs
1411 | otherwise = err "Argument roles mismatch"
1412 [ txt "In argument:" <+> int (n+1)
1413 , txt "Expected:" <+> ppr e
1414 , txt "Found:" <+> ppr r ]
1415 checkRoles _ [] [] = return ()
1416 checkRoles n [] rs = err "Too many coercion arguments"
1417 [ txt "Expected:" <+> int n
1418 , txt "Provided:" <+> int (n + length rs) ]
1419
1420 checkRoles n es [] = err "Not enough coercion arguments"
1421 [ txt "Expected:" <+> int (n + length es)
1422 , txt "Provided:" <+> int n ]
1423
1424 {-
1425 ************************************************************************
1426 * *
1427 \subsection[lint-monad]{The Lint monad}
1428 * *
1429 ************************************************************************
1430 -}
1431
1432 -- If you edit this type, you may need to update the GHC formalism
1433 -- See Note [GHC Formalism]
1434 data LintEnv
1435 = LE { le_flags :: LintFlags -- Linting the result of this pass
1436 , le_loc :: [LintLocInfo] -- Locations
1437 , le_subst :: TvSubst -- Current type substitution; we also use this
1438 -- to keep track of all the variables in scope,
1439 -- both Ids and TyVars
1440 , le_dynflags :: DynFlags -- DynamicFlags
1441 }
1442
1443 data LintFlags
1444 = LF { lf_check_global_ids :: Bool -- See Note [Checking for global Ids]
1445 , lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers]
1446 }
1447
1448 defaultLintFlags :: LintFlags
1449 defaultLintFlags = LF { lf_check_global_ids = False
1450 , lf_check_inline_loop_breakers = True }
1451
1452 newtype LintM a =
1453 LintM { unLintM ::
1454 LintEnv ->
1455 WarnsAndErrs -> -- Error and warning messages so far
1456 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
1457
1458 type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)
1459
1460 {- Note [Checking for global Ids]
1461 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1462 Before CoreTidy, all locally-bound Ids must be LocalIds, even
1463 top-level ones. See Note [Exported LocalIds] and Trac #9857.
1464
1465 Note [Type substitution]
1466 ~~~~~~~~~~~~~~~~~~~~~~~~
1467 Why do we need a type substitution? Consider
1468 /\(a:*). \(x:a). /\(a:*). id a x
1469 This is ill typed, because (renaming variables) it is really
1470 /\(a:*). \(x:a). /\(b:*). id b x
1471 Hence, when checking an application, we can't naively compare x's type
1472 (at its binding site) with its expected type (at a use site). So we
1473 rename type binders as we go, maintaining a substitution.
1474
1475 The same substitution also supports let-type, current expressed as
1476 (/\(a:*). body) ty
1477 Here we substitute 'ty' for 'a' in 'body', on the fly.
1478 -}
1479
1480 instance Functor LintM where
1481 fmap = liftM
1482
1483 instance Applicative LintM where
1484 pure = return
1485 (<*>) = ap
1486
1487 instance Monad LintM where
1488 return x = LintM (\ _ errs -> (Just x, errs))
1489 fail err = failWithL (text err)
1490 m >>= k = LintM (\ env errs ->
1491 let (res, errs') = unLintM m env errs in
1492 case res of
1493 Just r -> unLintM (k r) env errs'
1494 Nothing -> (Nothing, errs'))
1495
1496 instance HasDynFlags LintM where
1497 getDynFlags = LintM (\ e errs -> (Just (le_dynflags e), errs))
1498
1499 data LintLocInfo
1500 = RhsOf Id -- The variable bound
1501 | LambdaBodyOf Id -- The lambda-binder
1502 | BodyOfLetRec [Id] -- One of the binders
1503 | CaseAlt CoreAlt -- Case alternative
1504 | CasePat CoreAlt -- The *pattern* of the case alternative
1505 | AnExpr CoreExpr -- Some expression
1506 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
1507 | TopLevelBindings
1508 | InType Type -- Inside a type
1509 | InCo Coercion -- Inside a coercion
1510
1511 initL :: DynFlags -> LintFlags -> LintM a -> WarnsAndErrs -- Errors and warnings
1512 initL dflags flags m
1513 = case unLintM m env (emptyBag, emptyBag) of
1514 (_, errs) -> errs
1515 where
1516 env = LE { le_flags = flags, le_subst = emptyTvSubst, le_loc = [], le_dynflags = dflags }
1517
1518 getLintFlags :: LintM LintFlags
1519 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
1520
1521 checkL :: Bool -> MsgDoc -> LintM ()
1522 checkL True _ = return ()
1523 checkL False msg = failWithL msg
1524
1525 checkWarnL :: Bool -> MsgDoc -> LintM ()
1526 checkWarnL True _ = return ()
1527 checkWarnL False msg = addWarnL msg
1528
1529 failWithL :: MsgDoc -> LintM a
1530 failWithL msg = LintM $ \ env (warns,errs) ->
1531 (Nothing, (warns, addMsg env errs msg))
1532
1533 addErrL :: MsgDoc -> LintM ()
1534 addErrL msg = LintM $ \ env (warns,errs) ->
1535 (Just (), (warns, addMsg env errs msg))
1536
1537 addWarnL :: MsgDoc -> LintM ()
1538 addWarnL msg = LintM $ \ env (warns,errs) ->
1539 (Just (), (addMsg env warns msg, errs))
1540
1541 addMsg :: LintEnv -> Bag MsgDoc -> MsgDoc -> Bag MsgDoc
1542 addMsg env msgs msg
1543 = ASSERT( notNull locs )
1544 msgs `snocBag` mk_msg msg
1545 where
1546 locs = le_loc env
1547 (loc, cxt1) = dumpLoc (head locs)
1548 cxts = [snd (dumpLoc loc) | loc <- locs]
1549 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
1550 ptext (sLit "Substitution:") <+> ppr (le_subst env)
1551 | otherwise = cxt1
1552
1553 mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
1554
1555 addLoc :: LintLocInfo -> LintM a -> LintM a
1556 addLoc extra_loc m
1557 = LintM $ \ env errs ->
1558 unLintM m (env { le_loc = extra_loc : le_loc env }) errs
1559
1560 inCasePat :: LintM Bool -- A slight hack; see the unique call site
1561 inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
1562 where
1563 is_case_pat (LE { le_loc = CasePat {} : _ }) = True
1564 is_case_pat _other = False
1565
1566 addInScopeVars :: [Var] -> LintM a -> LintM a
1567 addInScopeVars vars m
1568 = LintM $ \ env errs ->
1569 unLintM m (env { le_subst = extendTvInScopeList (le_subst env) vars })
1570 errs
1571
1572 addInScopeVar :: Var -> LintM a -> LintM a
1573 addInScopeVar var m
1574 = LintM $ \ env errs ->
1575 unLintM m (env { le_subst = extendTvInScope (le_subst env) var }) errs
1576
1577 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
1578 extendSubstL tv ty m
1579 = LintM $ \ env errs ->
1580 unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
1581
1582 updateTvSubst :: TvSubst -> LintM a -> LintM a
1583 updateTvSubst subst' m
1584 = LintM $ \ env errs -> unLintM m (env { le_subst = subst' }) errs
1585
1586 getTvSubst :: LintM TvSubst
1587 getTvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
1588
1589 getInScope :: LintM InScopeSet
1590 getInScope = LintM (\ env errs -> (Just (getTvInScope (le_subst env)), errs))
1591
1592 applySubstTy :: InType -> LintM OutType
1593 applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
1594
1595 applySubstCo :: InCoercion -> LintM OutCoercion
1596 applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
1597
1598 lookupIdInScope :: Id -> LintM Id
1599 lookupIdInScope id
1600 | not (mustHaveLocalBinding id)
1601 = return id -- An imported Id
1602 | otherwise
1603 = do { subst <- getTvSubst
1604 ; case lookupInScope (getTvInScope subst) id of
1605 Just v -> return v
1606 Nothing -> do { addErrL out_of_scope
1607 ; return id } }
1608 where
1609 out_of_scope = pprBndr LetBind id <+> ptext (sLit "is out of scope")
1610
1611
1612 oneTupleDataConId :: Id -- Should not happen
1613 oneTupleDataConId = dataConWorkId (tupleDataCon Boxed 1)
1614
1615 checkTyCoVarInScope :: Var -> LintM ()
1616 checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
1617
1618 checkInScope :: SDoc -> Var -> LintM ()
1619 checkInScope loc_msg var =
1620 do { subst <- getTvSubst
1621 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
1622 (hsep [pprBndr LetBind var, loc_msg]) }
1623
1624 checkTys :: OutType -> OutType -> MsgDoc -> LintM ()
1625 -- check ty2 is subtype of ty1 (ie, has same structure but usage
1626 -- annotations need only be consistent, not equal)
1627 -- Assumes ty1,ty2 are have alrady had the substitution applied
1628 checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
1629
1630 checkRole :: Coercion
1631 -> Role -- expected
1632 -> Role -- actual
1633 -> LintM ()
1634 checkRole co r1 r2
1635 = checkL (r1 == r2)
1636 (ptext (sLit "Role incompatibility: expected") <+> ppr r1 <> comma <+>
1637 ptext (sLit "got") <+> ppr r2 $$
1638 ptext (sLit "in") <+> ppr co)
1639
1640 {-
1641 ************************************************************************
1642 * *
1643 \subsection{Error messages}
1644 * *
1645 ************************************************************************
1646 -}
1647
1648 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
1649
1650 dumpLoc (RhsOf v)
1651 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
1652
1653 dumpLoc (LambdaBodyOf b)
1654 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
1655
1656 dumpLoc (BodyOfLetRec [])
1657 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
1658
1659 dumpLoc (BodyOfLetRec bs@(_:_))
1660 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
1661
1662 dumpLoc (AnExpr e)
1663 = (noSrcLoc, text "In the expression:" <+> ppr e)
1664
1665 dumpLoc (CaseAlt (con, args, _))
1666 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1667
1668 dumpLoc (CasePat (con, args, _))
1669 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1670
1671 dumpLoc (ImportedUnfolding locn)
1672 = (locn, brackets (ptext (sLit "in an imported unfolding")))
1673 dumpLoc TopLevelBindings
1674 = (noSrcLoc, Outputable.empty)
1675 dumpLoc (InType ty)
1676 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1677 dumpLoc (InCo co)
1678 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
1679
1680 pp_binders :: [Var] -> SDoc
1681 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1682
1683 pp_binder :: Var -> SDoc
1684 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1685 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1686
1687 ------------------------------------------------------
1688 -- Messages for case expressions
1689
1690 mkDefaultArgsMsg :: [Var] -> MsgDoc
1691 mkDefaultArgsMsg args
1692 = hang (text "DEFAULT case with binders")
1693 4 (ppr args)
1694
1695 mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
1696 mkCaseAltMsg e ty1 ty2
1697 = hang (text "Type of case alternatives not the same as the annotation on case:")
1698 4 (vcat [ppr ty1, ppr ty2, ppr e])
1699
1700 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> MsgDoc
1701 mkScrutMsg var var_ty scrut_ty subst
1702 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1703 text "Result binder type:" <+> ppr var_ty,--(idType var),
1704 text "Scrutinee type:" <+> ppr scrut_ty,
1705 hsep [ptext (sLit "Current TV subst"), ppr subst]]
1706
1707 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
1708 mkNonDefltMsg e
1709 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1710 mkNonIncreasingAltsMsg e
1711 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1712
1713 nonExhaustiveAltsMsg :: CoreExpr -> MsgDoc
1714 nonExhaustiveAltsMsg e
1715 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1716
1717 mkBadConMsg :: TyCon -> DataCon -> MsgDoc
1718 mkBadConMsg tycon datacon
1719 = vcat [
1720 text "In a case alternative, data constructor isn't in scrutinee type:",
1721 text "Scrutinee type constructor:" <+> ppr tycon,
1722 text "Data con:" <+> ppr datacon
1723 ]
1724
1725 mkBadPatMsg :: Type -> Type -> MsgDoc
1726 mkBadPatMsg con_result_ty scrut_ty
1727 = vcat [
1728 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1729 text "Pattern result type:" <+> ppr con_result_ty,
1730 text "Scrutinee type:" <+> ppr scrut_ty
1731 ]
1732
1733 integerScrutinisedMsg :: MsgDoc
1734 integerScrutinisedMsg
1735 = text "In a LitAlt, the literal is lifted (probably Integer)"
1736
1737 mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
1738 mkBadAltMsg scrut_ty alt
1739 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1740 text "Scrutinee type:" <+> ppr scrut_ty,
1741 text "Alternative:" <+> pprCoreAlt alt ]
1742
1743 mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc
1744 mkNewTyDataConAltMsg scrut_ty alt
1745 = vcat [ text "Data alternative for newtype datacon",
1746 text "Scrutinee type:" <+> ppr scrut_ty,
1747 text "Alternative:" <+> pprCoreAlt alt ]
1748
1749
1750 ------------------------------------------------------
1751 -- Other error messages
1752
1753 mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1754 mkAppMsg fun_ty arg_ty arg
1755 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1756 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1757 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1758 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1759
1760 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1761 mkNonFunAppMsg fun_ty arg_ty arg
1762 = vcat [ptext (sLit "Non-function type in function position"),
1763 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1764 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1765 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1766
1767 mkLetErr :: TyVar -> CoreExpr -> MsgDoc
1768 mkLetErr bndr rhs
1769 = vcat [ptext (sLit "Bad `let' binding:"),
1770 hang (ptext (sLit "Variable:"))
1771 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
1772 hang (ptext (sLit "Rhs:"))
1773 4 (ppr rhs)]
1774
1775 mkTyAppMsg :: Type -> Type -> MsgDoc
1776 mkTyAppMsg ty arg_ty
1777 = vcat [text "Illegal type application:",
1778 hang (ptext (sLit "Exp type:"))
1779 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1780 hang (ptext (sLit "Arg type:"))
1781 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1782
1783 mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc
1784 mkRhsMsg binder what ty
1785 = vcat
1786 [hsep [ptext (sLit "The type of this binder doesn't match the type of its") <+> what <> colon,
1787 ppr binder],
1788 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1789 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1790
1791 mkLetAppMsg :: CoreExpr -> MsgDoc
1792 mkLetAppMsg e
1793 = hang (ptext (sLit "This argument does not satisfy the let/app invariant:"))
1794 2 (ppr e)
1795
1796 mkRhsPrimMsg :: Id -> CoreExpr -> MsgDoc
1797 mkRhsPrimMsg binder _rhs
1798 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1799 ppr binder],
1800 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1801 ]
1802
1803 mkStrictMsg :: Id -> MsgDoc
1804 mkStrictMsg binder
1805 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1806 ppr binder],
1807 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1808 ]
1809
1810 mkNonTopExportedMsg :: Id -> MsgDoc
1811 mkNonTopExportedMsg binder
1812 = hsep [ptext (sLit "Non-top-level binder is marked as exported:"), ppr binder]
1813
1814 mkNonTopExternalNameMsg :: Id -> MsgDoc
1815 mkNonTopExternalNameMsg binder
1816 = hsep [ptext (sLit "Non-top-level binder has an external name:"), ppr binder]
1817
1818 mkKindErrMsg :: TyVar -> Type -> MsgDoc
1819 mkKindErrMsg tyvar arg_ty
1820 = vcat [ptext (sLit "Kinds don't match in type application:"),
1821 hang (ptext (sLit "Type variable:"))
1822 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1823 hang (ptext (sLit "Arg type:"))
1824 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1825
1826 {- Not needed now
1827 mkArityMsg :: Id -> MsgDoc
1828 mkArityMsg binder
1829 = vcat [hsep [ptext (sLit "Demand type has"),
1830 ppr (dmdTypeDepth dmd_ty),
1831 ptext (sLit "arguments, rhs has"),
1832 ppr (idArity binder),
1833 ptext (sLit "arguments,"),
1834 ppr binder],
1835 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1836
1837 ]
1838 where (StrictSig dmd_ty) = idStrictness binder
1839 -}
1840 mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> MsgDoc
1841 mkCastErr expr co from_ty expr_ty
1842 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1843 ptext (sLit "From-type:") <+> ppr from_ty,
1844 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty,
1845 ptext (sLit "Actual enclosed expr:") <+> ppr expr,
1846 ptext (sLit "Coercion used in cast:") <+> ppr co
1847 ]
1848
1849 dupVars :: [[Var]] -> MsgDoc
1850 dupVars vars
1851 = hang (ptext (sLit "Duplicate variables brought into scope"))
1852 2 (ppr vars)
1853
1854 dupExtVars :: [[Name]] -> MsgDoc
1855 dupExtVars vars
1856 = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))
1857 2 (ppr vars)
1858
1859 {-
1860 ************************************************************************
1861 * *
1862 \subsection{Annotation Linting}
1863 * *
1864 ************************************************************************
1865 -}
1866
1867 -- | This checks whether a pass correctly looks through debug
1868 -- annotations (@SourceNote@). This works a bit different from other
1869 -- consistency checks: We check this by running the given task twice,
1870 -- noting all differences between the results.
1871 lintAnnots :: SDoc -> (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
1872 lintAnnots pname pass guts = do
1873 -- Run the pass as we normally would
1874 dflags <- getDynFlags
1875 when (gopt Opt_DoAnnotationLinting dflags) $
1876 liftIO $ Err.showPass dflags "Annotation linting - first run"
1877 nguts <- pass guts
1878 -- If appropriate re-run it without debug annotations to make sure
1879 -- that they made no difference.
1880 when (gopt Opt_DoAnnotationLinting dflags) $ do
1881 liftIO $ Err.showPass dflags "Annotation linting - second run"
1882 nguts' <- withoutAnnots pass guts
1883 -- Finally compare the resulting bindings
1884 liftIO $ Err.showPass dflags "Annotation linting - comparison"
1885 let binds = flattenBinds $ mg_binds nguts
1886 binds' = flattenBinds $ mg_binds nguts'
1887 (diffs,_) = diffBinds True (mkRnEnv2 emptyInScopeSet) binds binds'
1888 when (not (null diffs)) $ CoreMonad.putMsg $ vcat
1889 [ lint_banner "warning" pname
1890 , text "Core changes with annotations:"
1891 , withPprStyle defaultDumpStyle $ nest 2 $ vcat diffs
1892 ]
1893 -- Return actual new guts
1894 return nguts
1895
1896 -- | Run the given pass without annotations. This means that we both
1897 -- remove the @Opt_Debug@ flag from the environment as well as all
1898 -- annotations from incoming modules.
1899 withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
1900 withoutAnnots pass guts = do
1901 -- Remove debug flag from environment.
1902 dflags <- getDynFlags
1903 let removeFlag env = env{hsc_dflags = gopt_unset dflags Opt_Debug}
1904 withoutFlag corem =
1905 liftIO =<< runCoreM <$> fmap removeFlag getHscEnv <*> getRuleBase <*>
1906 getUniqueSupplyM <*> getModule <*>
1907 getVisibleOrphanMods <*>
1908 getPrintUnqualified <*> pure corem
1909 -- Nuke existing ticks in module.
1910 -- TODO: Ticks in unfoldings. Maybe change unfolding so it removes
1911 -- them in absence of @Opt_Debug@?
1912 let nukeTicks = stripTicksE (not . tickishIsCode)
1913 nukeAnnotsBind :: CoreBind -> CoreBind
1914 nukeAnnotsBind bind = case bind of
1915 Rec bs -> Rec $ map (\(b,e) -> (b, nukeTicks e)) bs
1916 NonRec b e -> NonRec b $ nukeTicks e
1917 nukeAnnotsMod mg@ModGuts{mg_binds=binds}
1918 = mg{mg_binds = map nukeAnnotsBind binds}
1919 -- Perform pass with all changes applied
1920 fmap fst $ withoutFlag $ pass (nukeAnnotsMod guts)