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