Add -fcross-module-specialise flag
[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 binder_ty
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 -- Check whether binder's specialisations contain any out-of-scope variables
473 ; mapM_ (checkBndrIdInScope binder) bndr_vars
474
475 ; flags <- getLintFlags
476 ; when (lf_check_inline_loop_breakers flags
477 && isStrongLoopBreaker (idOccInfo binder)
478 && isInlinePragma (idInlinePragma binder))
479 (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
480 -- Only non-rule loop breakers inhibit inlining
481
482 -- Check whether arity and demand type are consistent (only if demand analysis
483 -- already happened)
484 --
485 -- Note (Apr 2014): this is actually ok. See Note [Demand analysis for trivial right-hand sides]
486 -- in DmdAnal. After eta-expansion in CorePrep the rhs is no longer trivial.
487 -- ; let dmdTy = idStrictness binder
488 -- ; checkL (case dmdTy of
489 -- StrictSig dmd_ty -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs)
490 -- (mkArityMsg binder)
491
492 -- Check that the binder's arity is within the bounds imposed by
493 -- the type and the strictness signature. See Note [exprArity invariant]
494 -- and Note [Trimming arity]
495 ; checkL (idArity binder <= length (typeArity (idType binder)))
496 (ptext (sLit "idArity") <+> ppr (idArity binder) <+>
497 ptext (sLit "exceeds typeArity") <+>
498 ppr (length (typeArity (idType binder))) <> colon <+>
499 ppr binder)
500
501 ; case splitStrictSig (idStrictness binder) of
502 (demands, result_info) | isBotRes result_info ->
503 checkL (idArity binder <= length demands)
504 (ptext (sLit "idArity") <+> ppr (idArity binder) <+>
505 ptext (sLit "exceeds arity imposed by the strictness signature") <+>
506 ppr (idStrictness binder) <> colon <+>
507 ppr binder)
508 _ -> return ()
509
510 ; lintIdUnfolding binder binder_ty (idUnfolding binder) }
511
512 -- We should check the unfolding, if any, but this is tricky because
513 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
514 where
515 binder_ty = idType binder
516 bndr_vars = varSetElems (idFreeVars binder)
517
518 -- If you edit this function, you may need to update the GHC formalism
519 -- See Note [GHC Formalism]
520 lintBinder var | isId var = lintIdBndr var $ \_ -> (return ())
521 | otherwise = return ()
522
523 lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
524 lintIdUnfolding bndr bndr_ty (CoreUnfolding { uf_tmpl = rhs, uf_src = src })
525 | isStableSource src
526 = do { ty <- lintCoreExpr rhs
527 ; checkTys bndr_ty ty (mkRhsMsg bndr (ptext (sLit "unfolding")) ty) }
528 lintIdUnfolding _ _ _
529 = return () -- We could check more
530
531 {-
532 Note [Checking for INLINE loop breakers]
533 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
534 It's very suspicious if a strong loop breaker is marked INLINE.
535
536 However, the desugarer generates instance methods with INLINE pragmas
537 that form a mutually recursive group. Only after a round of
538 simplification are they unravelled. So we suppress the test for
539 the desugarer.
540
541 ************************************************************************
542 * *
543 \subsection[lintCoreExpr]{lintCoreExpr}
544 * *
545 ************************************************************************
546 -}
547
548 --type InKind = Kind -- Substitution not yet applied
549 type InType = Type
550 type InCoercion = Coercion
551 type InVar = Var
552 type InTyVar = TyVar
553
554 type OutKind = Kind -- Substitution has been applied to this,
555 -- but has not been linted yet
556 type LintedKind = Kind -- Substitution applied, and type is linted
557
558 type OutType = Type -- Substitution has been applied to this,
559 -- but has not been linted yet
560
561 type LintedType = Type -- Substitution applied, and type is linted
562
563 type OutCoercion = Coercion
564 type OutVar = Var
565 type OutTyVar = TyVar
566
567 lintCoreExpr :: CoreExpr -> LintM OutType
568 -- The returned type has the substitution from the monad
569 -- already applied to it:
570 -- lintCoreExpr e subst = exprType (subst e)
571 --
572 -- The returned "type" can be a kind, if the expression is (Type ty)
573
574 -- If you edit this function, you may need to update the GHC formalism
575 -- See Note [GHC Formalism]
576 lintCoreExpr (Var var)
577 = do { checkL (not (var == oneTupleDataConId))
578 (ptext (sLit "Illegal one-tuple"))
579
580 ; checkL (isId var && not (isCoVar var))
581 (ptext (sLit "Non term variable") <+> ppr var)
582
583 ; checkDeadIdOcc var
584 ; var' <- lookupIdInScope var
585 ; return (idType var') }
586
587 lintCoreExpr (Lit lit)
588 = return (literalType lit)
589
590 lintCoreExpr (Cast expr co)
591 = do { expr_ty <- lintCoreExpr expr
592 ; co' <- applySubstCo co
593 ; (_, from_ty, to_ty, r) <- lintCoercion co'
594 ; checkRole co' Representational r
595 ; checkTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
596 ; return to_ty }
597
598 lintCoreExpr (Tick (Breakpoint _ ids) expr)
599 = do forM_ ids $ \id -> do
600 checkDeadIdOcc id
601 lookupIdInScope id
602 lintCoreExpr expr
603
604 lintCoreExpr (Tick _other_tickish expr)
605 = lintCoreExpr expr
606
607 lintCoreExpr (Let (NonRec tv (Type ty)) body)
608 | isTyVar tv
609 = -- See Note [Linting type lets]
610 do { ty' <- applySubstTy ty
611 ; lintTyBndr tv $ \ tv' ->
612 do { addLoc (RhsOf tv) $ checkTyKind tv' ty'
613 -- Now extend the substitution so we
614 -- take advantage of it in the body
615 ; extendSubstL tv' ty' $
616 addLoc (BodyOfLetRec [tv]) $
617 lintCoreExpr body } }
618
619 lintCoreExpr (Let (NonRec bndr rhs) body)
620 | isId bndr
621 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
622 ; addLoc (BodyOfLetRec [bndr])
623 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
624
625 | otherwise
626 = failWithL (mkLetErr bndr rhs) -- Not quite accurate
627
628 lintCoreExpr (Let (Rec pairs) body)
629 = lintAndScopeIds bndrs $ \_ ->
630 do { checkL (null dups) (dupVars dups)
631 ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
632 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
633 where
634 bndrs = map fst pairs
635 (_, dups) = removeDups compare bndrs
636
637 lintCoreExpr e@(App _ _)
638 = do { fun_ty <- lintCoreExpr fun
639 ; addLoc (AnExpr e) $ foldM lintCoreArg fun_ty args }
640 where
641 (fun, args) = collectArgs e
642
643 lintCoreExpr (Lam var expr)
644 = addLoc (LambdaBodyOf var) $
645 lintBinder var $ \ var' ->
646 do { body_ty <- lintCoreExpr expr
647 ; if isId var' then
648 return (mkFunTy (idType var') body_ty)
649 else
650 return (mkForAllTy var' body_ty)
651 }
652 -- The applySubstTy is needed to apply the subst to var
653
654 lintCoreExpr e@(Case scrut var alt_ty alts) =
655 -- Check the scrutinee
656 do { scrut_ty <- lintCoreExpr scrut
657 ; alt_ty <- lintInTy alt_ty
658 ; var_ty <- lintInTy (idType var)
659
660 -- See Note [No alternatives lint check]
661 ; when (null alts) $
662 do { checkL (not (exprIsHNF scrut))
663 (ptext (sLit "No alternatives for a case scrutinee in head-normal form:") <+> ppr scrut)
664 ; checkL (exprIsBottom scrut)
665 (ptext (sLit "No alternatives for a case scrutinee not known to diverge for sure:") <+> ppr scrut)
666 }
667
668 ; case tyConAppTyCon_maybe (idType var) of
669 Just tycon
670 | debugIsOn &&
671 isAlgTyCon tycon &&
672 not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
673 null (tyConDataCons tycon) ->
674 pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
675 -- This can legitimately happen for type families
676 $ return ()
677 _otherwise -> return ()
678
679 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
680
681 ; subst <- getTvSubst
682 ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
683
684 ; lintAndScopeId var $ \_ ->
685 do { -- Check the alternatives
686 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
687 ; checkCaseAlts e scrut_ty alts
688 ; return alt_ty } }
689
690 -- This case can't happen; linting types in expressions gets routed through
691 -- lintCoreArgs
692 lintCoreExpr (Type ty)
693 = pprPanic "lintCoreExpr" (ppr ty)
694
695 lintCoreExpr (Coercion co)
696 = do { (_kind, ty1, ty2, role) <- lintInCo co
697 ; return (mkCoercionType role ty1 ty2) }
698
699 {-
700 Note [Kind instantiation in coercions]
701 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
702 Consider the following coercion axiom:
703 ax_co [(k_ag :: BOX), (f_aa :: k_ag -> Constraint)] :: T k_ag f_aa ~ f_aa
704
705 Consider the following instantiation:
706 ax_co <* -> *> <Monad>
707
708 We need to split the co_ax_tvs into kind and type variables in order
709 to find out the coercion kind instantiations. Those can only be Refl
710 since we don't have kind coercions. This is just a way to represent
711 kind instantiation.
712
713 We use the number of kind variables to know how to split the coercions
714 instantiations between kind coercions and type coercions. We lint the
715 kind coercions and produce the following substitution which is to be
716 applied in the type variables:
717 k_ag ~~> * -> *
718
719 Note [No alternatives lint check]
720 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
721 Case expressions with no alternatives are odd beasts, and worth looking at
722 in the linter (cf Trac #10180). We check two things:
723
724 * exprIsHNF is false: certainly, it would be terribly wrong if the
725 scrutinee was already in head normal form.
726
727 * exprIsBottom is true: we should be able to see why GHC believes the
728 scrutinee is diverging for sure.
729
730 In principle, the first check is redundant: exprIsBottom == True will
731 always imply exprIsHNF == False. But the first check is reliable: If
732 exprIsHNF == True, then there definitely is a problem (exprIsHNF errs
733 on the right side). If the second check triggers then it may be the
734 case that the compiler got smarter elsewhere, and the empty case is
735 correct, but that exprIsBottom is unable to see it. In particular, the
736 empty-type check in exprIsBottom is an approximation. Therefore, this
737 check is not fully reliable, and we keep both around.
738
739 ************************************************************************
740 * *
741 \subsection[lintCoreArgs]{lintCoreArgs}
742 * *
743 ************************************************************************
744
745 The basic version of these functions checks that the argument is a
746 subtype of the required type, as one would expect.
747 -}
748
749 lintCoreArg :: OutType -> CoreArg -> LintM OutType
750 lintCoreArg fun_ty (Type arg_ty)
751 = do { arg_ty' <- applySubstTy arg_ty
752 ; lintTyApp fun_ty arg_ty' }
753
754 lintCoreArg fun_ty arg
755 = do { arg_ty <- lintCoreExpr arg
756 ; checkL (not (isUnLiftedType arg_ty) || exprOkForSpeculation arg)
757 (mkLetAppMsg arg)
758 ; lintValApp arg fun_ty arg_ty }
759
760 -----------------
761 lintAltBinders :: OutType -- Scrutinee type
762 -> OutType -- Constructor type
763 -> [OutVar] -- Binders
764 -> LintM ()
765 -- If you edit this function, you may need to update the GHC formalism
766 -- See Note [GHC Formalism]
767 lintAltBinders scrut_ty con_ty []
768 = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
769 lintAltBinders scrut_ty con_ty (bndr:bndrs)
770 | isTyVar bndr
771 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
772 ; lintAltBinders scrut_ty con_ty' bndrs }
773 | otherwise
774 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
775 ; lintAltBinders scrut_ty con_ty' bndrs }
776
777 -----------------
778 lintTyApp :: OutType -> OutType -> LintM OutType
779 lintTyApp fun_ty arg_ty
780 | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
781 , isTyVar tyvar
782 = do { checkTyKind tyvar arg_ty
783 ; return (substTyWith [tyvar] [arg_ty] body_ty) }
784
785 | otherwise
786 = failWithL (mkTyAppMsg fun_ty arg_ty)
787
788 -----------------
789 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
790 lintValApp arg fun_ty arg_ty
791 | Just (arg,res) <- splitFunTy_maybe fun_ty
792 = do { checkTys arg arg_ty err1
793 ; return res }
794 | otherwise
795 = failWithL err2
796 where
797 err1 = mkAppMsg fun_ty arg_ty arg
798 err2 = mkNonFunAppMsg fun_ty arg_ty arg
799
800 checkTyKind :: OutTyVar -> OutType -> LintM ()
801 -- Both args have had substitution applied
802
803 -- If you edit this function, you may need to update the GHC formalism
804 -- See Note [GHC Formalism]
805 checkTyKind tyvar arg_ty
806 | isSuperKind tyvar_kind -- kind forall
807 = lintKind arg_ty
808 -- Arg type might be boxed for a function with an uncommitted
809 -- tyvar; notably this is used so that we can give
810 -- error :: forall a:*. String -> a
811 -- and then apply it to both boxed and unboxed types.
812 | otherwise -- type forall
813 = do { arg_kind <- lintType arg_ty
814 ; unless (arg_kind `isSubKind` tyvar_kind)
815 (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
816 where
817 tyvar_kind = tyVarKind tyvar
818
819 checkDeadIdOcc :: Id -> LintM ()
820 -- Occurrences of an Id should never be dead....
821 -- except when we are checking a case pattern
822 checkDeadIdOcc id
823 | isDeadOcc (idOccInfo id)
824 = do { in_case <- inCasePat
825 ; checkL in_case
826 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
827 | otherwise
828 = return ()
829
830 {-
831 ************************************************************************
832 * *
833 \subsection[lintCoreAlts]{lintCoreAlts}
834 * *
835 ************************************************************************
836 -}
837
838 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
839 -- a) Check that the alts are non-empty
840 -- b1) Check that the DEFAULT comes first, if it exists
841 -- b2) Check that the others are in increasing order
842 -- c) Check that there's a default for infinite types
843 -- NB: Algebraic cases are not necessarily exhaustive, because
844 -- the simplifer correctly eliminates case that can't
845 -- possibly match.
846
847 checkCaseAlts e ty alts =
848 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
849 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
850
851 -- For types Int#, Word# with an infinite (well, large!) number of
852 -- possible values, there should usually be a DEFAULT case
853 -- But (see Note [Empty case alternatives] in CoreSyn) it's ok to
854 -- have *no* case alternatives.
855 -- In effect, this is a kind of partial test. I suppose it's possible
856 -- that we might *know* that 'x' was 1 or 2, in which case
857 -- case x of { 1 -> e1; 2 -> e2 }
858 -- would be fine.
859 ; checkL (isJust maybe_deflt || not is_infinite_ty || null alts)
860 (nonExhaustiveAltsMsg e) }
861 where
862 (con_alts, maybe_deflt) = findDefault alts
863
864 -- Check that successive alternatives have increasing tags
865 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
866 increasing_tag _ = True
867
868 non_deflt (DEFAULT, _, _) = False
869 non_deflt _ = True
870
871 is_infinite_ty = case tyConAppTyCon_maybe ty of
872 Nothing -> False
873 Just tycon -> isPrimTyCon tycon
874
875 checkAltExpr :: CoreExpr -> OutType -> LintM ()
876 checkAltExpr expr ann_ty
877 = do { actual_ty <- lintCoreExpr expr
878 ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
879
880 lintCoreAlt :: OutType -- Type of scrutinee
881 -> OutType -- Type of the alternative
882 -> CoreAlt
883 -> LintM ()
884 -- If you edit this function, you may need to update the GHC formalism
885 -- See Note [GHC Formalism]
886 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
887 do { checkL (null args) (mkDefaultArgsMsg args)
888 ; checkAltExpr rhs alt_ty }
889
890 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
891 | litIsLifted lit
892 = failWithL integerScrutinisedMsg
893 | otherwise
894 = do { checkL (null args) (mkDefaultArgsMsg args)
895 ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
896 ; checkAltExpr rhs alt_ty }
897 where
898 lit_ty = literalType lit
899
900 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
901 | isNewTyCon (dataConTyCon con)
902 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
903 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
904 = addLoc (CaseAlt alt) $ do
905 { -- First instantiate the universally quantified
906 -- type variables of the data constructor
907 -- We've already check
908 checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
909 ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
910
911 -- And now bring the new binders into scope
912 ; lintBinders args $ \ args' -> do
913 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
914 ; checkAltExpr rhs alt_ty } }
915
916 | otherwise -- Scrut-ty is wrong shape
917 = addErrL (mkBadAltMsg scrut_ty alt)
918
919 {-
920 ************************************************************************
921 * *
922 \subsection[lint-types]{Types}
923 * *
924 ************************************************************************
925 -}
926
927 -- When we lint binders, we (one at a time and in order):
928 -- 1. Lint var types or kinds (possibly substituting)
929 -- 2. Add the binder to the in scope set, and if its a coercion var,
930 -- we may extend the substitution to reflect its (possibly) new kind
931 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
932 lintBinders [] linterF = linterF []
933 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
934 lintBinders vars $ \ vars' ->
935 linterF (var':vars')
936
937 -- If you edit this function, you may need to update the GHC formalism
938 -- See Note [GHC Formalism]
939 lintBinder :: Var -> (Var -> LintM a) -> LintM a
940 lintBinder var linterF
941 | isId var = lintIdBndr var linterF
942 | otherwise = lintTyBndr var linterF
943
944 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
945 lintTyBndr tv thing_inside
946 = do { subst <- getTvSubst
947 ; let (subst', tv') = Type.substTyVarBndr subst tv
948 ; lintTyBndrKind tv'
949 ; updateTvSubst subst' (thing_inside tv') }
950
951 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
952 -- Do substitution on the type of a binder and add the var with this
953 -- new type to the in-scope set of the second argument
954 -- ToDo: lint its rules
955
956 lintIdBndr id linterF
957 = do { lintAndScopeId id $ \id' -> linterF id' }
958
959 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
960 lintAndScopeIds ids linterF
961 = go ids
962 where
963 go [] = linterF []
964 go (id:ids) = lintAndScopeId id $ \id ->
965 lintAndScopeIds ids $ \ids ->
966 linterF (id:ids)
967
968 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
969 lintAndScopeId id linterF
970 = do { flags <- getLintFlags
971 ; checkL (not (lf_check_global_ids flags) || isLocalId id)
972 (ptext (sLit "Non-local Id binder") <+> ppr id)
973 -- See Note [Checking for global Ids]
974 ; ty <- lintInTy (idType id)
975 ; let id' = setIdType id ty
976 ; addInScopeVar id' $ (linterF id') }
977
978 {-
979 ************************************************************************
980 * *
981 Types and kinds
982 * *
983 ************************************************************************
984
985 We have a single linter for types and kinds. That is convenient
986 because sometimes it's not clear whether the thing we are looking
987 at is a type or a kind.
988 -}
989
990 lintInTy :: InType -> LintM LintedType
991 -- Types only, not kinds
992 -- Check the type, and apply the substitution to it
993 -- See Note [Linting type lets]
994 lintInTy ty
995 = addLoc (InType ty) $
996 do { ty' <- applySubstTy ty
997 ; _k <- lintType ty'
998 ; return ty' }
999
1000 -------------------
1001 lintTyBndrKind :: OutTyVar -> LintM ()
1002 -- Handles both type and kind foralls.
1003 lintTyBndrKind tv = lintKind (tyVarKind tv)
1004
1005 -------------------
1006 lintType :: OutType -> LintM LintedKind
1007 -- The returned Kind has itself been linted
1008
1009 -- If you edit this function, you may need to update the GHC formalism
1010 -- See Note [GHC Formalism]
1011 lintType (TyVarTy tv)
1012 = do { checkTyCoVarInScope tv
1013 ; return (tyVarKind tv) }
1014 -- We checked its kind when we added it to the envt
1015
1016 lintType ty@(AppTy t1 t2)
1017 = do { k1 <- lintType t1
1018 ; k2 <- lintType t2
1019 ; lint_ty_app ty k1 [(t2,k2)] }
1020
1021 lintType ty@(FunTy t1 t2) -- (->) has two different rules, for types and kinds
1022 = do { k1 <- lintType t1
1023 ; k2 <- lintType t2
1024 ; lintArrow (ptext (sLit "type or kind") <+> quotes (ppr ty)) k1 k2 }
1025
1026 lintType ty@(TyConApp tc tys)
1027 | Just ty' <- coreView ty
1028 = lintType ty' -- Expand type synonyms, so that we do not bogusly complain
1029 -- about un-saturated type synonyms
1030
1031 | isUnLiftedTyCon tc || isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
1032 -- See Note [The kind invariant] in TypeRep
1033 -- Also type synonyms and type families
1034 , length tys < tyConArity tc
1035 = failWithL (hang (ptext (sLit "Un-saturated type application")) 2 (ppr ty))
1036
1037 | otherwise
1038 = do { ks <- mapM lintType tys
1039 ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
1040
1041 lintType (ForAllTy tv ty)
1042 = do { lintTyBndrKind tv
1043 ; addInScopeVar tv (lintType ty) }
1044
1045 lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
1046
1047 lintKind :: OutKind -> LintM ()
1048 -- If you edit this function, you may need to update the GHC formalism
1049 -- See Note [GHC Formalism]
1050 lintKind k = do { sk <- lintType k
1051 ; unless (isSuperKind sk)
1052 (addErrL (hang (ptext (sLit "Ill-kinded kind:") <+> ppr k)
1053 2 (ptext (sLit "has kind:") <+> ppr sk))) }
1054
1055 lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
1056 -- If you edit this function, you may need to update the GHC formalism
1057 -- See Note [GHC Formalism]
1058 lintArrow what k1 k2 -- Eg lintArrow "type or kind `blah'" k1 k2
1059 -- or lintarrow "coercion `blah'" k1 k2
1060 | isSuperKind k1
1061 = return superKind
1062 | otherwise
1063 = do { unless (okArrowArgKind k1) (addErrL (msg (ptext (sLit "argument")) k1))
1064 ; unless (okArrowResultKind k2) (addErrL (msg (ptext (sLit "result")) k2))
1065 ; return liftedTypeKind }
1066 where
1067 msg ar k
1068 = vcat [ hang (ptext (sLit "Ill-kinded") <+> ar)
1069 2 (ptext (sLit "in") <+> what)
1070 , what <+> ptext (sLit "kind:") <+> ppr k ]
1071
1072 lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
1073 lint_ty_app ty k tys
1074 = lint_app (ptext (sLit "type") <+> quotes (ppr ty)) k tys
1075
1076 ----------------
1077 lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
1078 lint_co_app ty k tys
1079 = lint_app (ptext (sLit "coercion") <+> quotes (ppr ty)) k tys
1080
1081 ----------------
1082 lintTyLit :: TyLit -> LintM ()
1083 lintTyLit (NumTyLit n)
1084 | n >= 0 = return ()
1085 | otherwise = failWithL msg
1086 where msg = ptext (sLit "Negative type literal:") <+> integer n
1087 lintTyLit (StrTyLit _) = return ()
1088
1089 lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
1090 -- (lint_app d fun_kind arg_tys)
1091 -- We have an application (f arg_ty1 .. arg_tyn),
1092 -- where f :: fun_kind
1093 -- Takes care of linting the OutTypes
1094
1095 -- If you edit this function, you may need to update the GHC formalism
1096 -- See Note [GHC Formalism]
1097 lint_app doc kfn kas
1098 = foldlM go_app kfn kas
1099 where
1100 fail_msg = vcat [ hang (ptext (sLit "Kind application error in")) 2 doc
1101 , nest 2 (ptext (sLit "Function kind =") <+> ppr kfn)
1102 , nest 2 (ptext (sLit "Arg kinds =") <+> ppr kas) ]
1103
1104 go_app kfn ka
1105 | Just kfn' <- coreView kfn
1106 = go_app kfn' ka
1107
1108 go_app (FunTy kfa kfb) (_,ka)
1109 = do { unless (ka `isSubKind` kfa) (addErrL fail_msg)
1110 ; return kfb }
1111
1112 go_app (ForAllTy kv kfn) (ta,ka)
1113 = do { unless (ka `isSubKind` tyVarKind kv) (addErrL fail_msg)
1114 ; return (substKiWith [kv] [ta] kfn) }
1115
1116 go_app _ _ = failWithL fail_msg
1117
1118 {-
1119 ************************************************************************
1120 * *
1121 Linting coercions
1122 * *
1123 ************************************************************************
1124 -}
1125
1126 lintInCo :: InCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
1127 -- Check the coercion, and apply the substitution to it
1128 -- See Note [Linting type lets]
1129 lintInCo co
1130 = addLoc (InCo co) $
1131 do { co' <- applySubstCo co
1132 ; lintCoercion co' }
1133
1134 lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
1135 -- Check the kind of a coercion term, returning the kind
1136 -- Post-condition: the returned OutTypes are lint-free
1137 -- and have the same kind as each other
1138
1139 -- If you edit this function, you may need to update the GHC formalism
1140 -- See Note [GHC Formalism]
1141 lintCoercion (Refl r ty)
1142 = do { k <- lintType ty
1143 ; return (k, ty, ty, r) }
1144
1145 lintCoercion co@(TyConAppCo r tc cos)
1146 | tc `hasKey` funTyConKey
1147 , [co1,co2] <- cos
1148 = do { (k1,s1,t1,r1) <- lintCoercion co1
1149 ; (k2,s2,t2,r2) <- lintCoercion co2
1150 ; rk <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k1 k2
1151 ; checkRole co1 r r1
1152 ; checkRole co2 r r2
1153 ; return (rk, mkFunTy s1 s2, mkFunTy t1 t2, r) }
1154
1155 | Just {} <- synTyConDefn_maybe tc
1156 = failWithL (ptext (sLit "Synonym in TyConAppCo:") <+> ppr co)
1157
1158 | otherwise
1159 = do { (ks,ss,ts,rs) <- mapAndUnzip4M lintCoercion cos
1160 ; rk <- lint_co_app co (tyConKind tc) (ss `zip` ks)
1161 ; _ <- zipWith3M checkRole cos (tyConRolesX r tc) rs
1162 ; return (rk, mkTyConApp tc ss, mkTyConApp tc ts, r) }
1163
1164 lintCoercion co@(AppCo co1 co2)
1165 = do { (k1,s1,t1,r1) <- lintCoercion co1
1166 ; (k2,s2,t2,r2) <- lintCoercion co2
1167 ; rk <- lint_co_app co k1 [(s2,k2)]
1168 ; if r1 == Phantom
1169 then checkL (r2 == Phantom || r2 == Nominal)
1170 (ptext (sLit "Second argument in AppCo cannot be R:") $$
1171 ppr co)
1172 else checkRole co Nominal r2
1173 ; return (rk, mkAppTy s1 s2, mkAppTy t1 t2, r1) }
1174
1175 lintCoercion (ForAllCo tv co)
1176 = do { lintTyBndrKind tv
1177 ; (k, s, t, r) <- addInScopeVar tv (lintCoercion co)
1178 ; return (k, mkForAllTy tv s, mkForAllTy tv t, r) }
1179
1180 lintCoercion (CoVarCo cv)
1181 | not (isCoVar cv)
1182 = failWithL (hang (ptext (sLit "Bad CoVarCo:") <+> ppr cv)
1183 2 (ptext (sLit "With offending type:") <+> ppr (varType cv)))
1184 | otherwise
1185 = do { checkTyCoVarInScope cv
1186 ; cv' <- lookupIdInScope cv
1187 ; let (s,t) = coVarKind cv'
1188 k = typeKind s
1189 r = coVarRole cv'
1190 ; when (isSuperKind k) $
1191 do { checkL (r == Nominal) (hang (ptext (sLit "Non-nominal kind equality"))
1192 2 (ppr cv))
1193 ; checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality"))
1194 2 (ppr cv)) }
1195 ; return (k, s, t, r) }
1196
1197 -- See Note [Bad unsafe coercion]
1198 lintCoercion (UnivCo _prov r ty1 ty2)
1199 = do { k1 <- lintType ty1
1200 ; k2 <- lintType ty2
1201 -- ; unless (k1 `eqKind` k2) $
1202 -- failWithL (hang (ptext (sLit "Unsafe coercion changes kind"))
1203 -- 2 (ppr co))
1204 ; when (r /= Phantom && isSubOpenTypeKind k1 && isSubOpenTypeKind k2)
1205 (checkTypes ty1 ty2)
1206 ; return (k1, ty1, ty2, r) }
1207 where
1208 report s = hang (text $ "Unsafe coercion between " ++ s)
1209 2 (vcat [ text "From:" <+> ppr ty1
1210 , text " To:" <+> ppr ty2])
1211 isUnBoxed :: PrimRep -> Bool
1212 isUnBoxed PtrRep = False
1213 isUnBoxed _ = True
1214 checkTypes t1 t2
1215 = case (repType t1, repType t2) of
1216 (UnaryRep _, UnaryRep _) ->
1217 validateCoercion (typePrimRep t1)
1218 (typePrimRep t2)
1219 (UbxTupleRep rep1, UbxTupleRep rep2) -> do
1220 checkWarnL (length rep1 == length rep2)
1221 (report "unboxed tuples of different length")
1222 zipWithM_ checkTypes rep1 rep2
1223 _ -> addWarnL (report "unboxed tuple and ordinary type")
1224 validateCoercion :: PrimRep -> PrimRep -> LintM ()
1225 validateCoercion rep1 rep2
1226 = do { dflags <- getDynFlags
1227 ; checkWarnL (isUnBoxed rep1 == isUnBoxed rep2)
1228 (report "unboxed and boxed value")
1229 ; checkWarnL (TyCon.primRepSizeW dflags rep1
1230 == TyCon.primRepSizeW dflags rep2)
1231 (report "unboxed values of different size")
1232 ; let fl = liftM2 (==) (TyCon.primRepIsFloat rep1)
1233 (TyCon.primRepIsFloat rep2)
1234 ; case fl of
1235 Nothing -> addWarnL (report "vector types")
1236 Just False -> addWarnL (report "float and integral values")
1237 _ -> return ()
1238 }
1239
1240 lintCoercion (SymCo co)
1241 = do { (k, ty1, ty2, r) <- lintCoercion co
1242 ; return (k, ty2, ty1, r) }
1243
1244 lintCoercion co@(TransCo co1 co2)
1245 = do { (k1, ty1a, ty1b, r1) <- lintCoercion co1
1246 ; (_, ty2a, ty2b, r2) <- lintCoercion co2
1247 ; checkL (ty1b `eqType` ty2a)
1248 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
1249 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
1250 ; checkRole co r1 r2
1251 ; return (k1, ty1a, ty2b, r1) }
1252
1253 lintCoercion the_co@(NthCo n co)
1254 = do { (_,s,t,r) <- lintCoercion co
1255 ; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
1256 (Just (tc_s, tys_s), Just (tc_t, tys_t))
1257 | tc_s == tc_t
1258 , isInjectiveTyCon tc_s r
1259 -- see Note [NthCo and newtypes] in Coercion
1260 , tys_s `equalLength` tys_t
1261 , n < length tys_s
1262 -> return (ks, ts, tt, tr)
1263 where
1264 ts = getNth tys_s n
1265 tt = getNth tys_t n
1266 tr = nthRole r tc_s n
1267 ks = typeKind ts
1268
1269 _ -> failWithL (hang (ptext (sLit "Bad getNth:"))
1270 2 (ppr the_co $$ ppr s $$ ppr t)) }
1271
1272 lintCoercion the_co@(LRCo lr co)
1273 = do { (_,s,t,r) <- lintCoercion co
1274 ; checkRole co Nominal r
1275 ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
1276 (Just s_pr, Just t_pr)
1277 -> return (k, s_pick, t_pick, Nominal)
1278 where
1279 s_pick = pickLR lr s_pr
1280 t_pick = pickLR lr t_pr
1281 k = typeKind s_pick
1282
1283 _ -> failWithL (hang (ptext (sLit "Bad LRCo:"))
1284 2 (ppr the_co $$ ppr s $$ ppr t)) }
1285
1286 lintCoercion (InstCo co arg_ty)
1287 = do { (k,s,t,r) <- lintCoercion co
1288 ; arg_kind <- lintType arg_ty
1289 ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
1290 (Just (tv1,ty1), Just (tv2,ty2))
1291 | arg_kind `isSubKind` tyVarKind tv1
1292 -> return (k, substTyWith [tv1] [arg_ty] ty1,
1293 substTyWith [tv2] [arg_ty] ty2, r)
1294 | otherwise
1295 -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
1296 _ -> failWithL (ptext (sLit "Bad argument of inst")) }
1297
1298 lintCoercion co@(AxiomInstCo con ind cos)
1299 = do { unless (0 <= ind && ind < brListLength (coAxiomBranches con))
1300 (bad_ax (ptext (sLit "index out of range")))
1301 -- See Note [Kind instantiation in coercions]
1302 ; let CoAxBranch { cab_tvs = ktvs
1303 , cab_roles = roles
1304 , cab_lhs = lhs
1305 , cab_rhs = rhs } = coAxiomNthBranch con ind
1306 ; unless (equalLength ktvs cos) (bad_ax (ptext (sLit "lengths")))
1307 ; in_scope <- getInScope
1308 ; let empty_subst = mkTvSubst in_scope emptyTvSubstEnv
1309 ; (subst_l, subst_r) <- foldlM check_ki
1310 (empty_subst, empty_subst)
1311 (zip3 ktvs roles cos)
1312 ; let lhs' = Type.substTys subst_l lhs
1313 rhs' = Type.substTy subst_r rhs
1314 ; case checkAxInstCo co of
1315 Just bad_branch -> bad_ax $ ptext (sLit "inconsistent with") <+> (pprCoAxBranch (coAxiomTyCon con) bad_branch)
1316 Nothing -> return ()
1317 ; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs', coAxiomRole con) }
1318 where
1319 bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what)
1320 2 (ppr co))
1321
1322 check_ki (subst_l, subst_r) (ktv, role, co)
1323 = do { (k, t1, t2, r) <- lintCoercion co
1324 ; checkRole co role r
1325 ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)
1326 -- Using subst_l is ok, because subst_l and subst_r
1327 -- must agree on kind equalities
1328 ; unless (k `isSubKind` ktv_kind)
1329 (bad_ax (ptext (sLit "check_ki2") <+> vcat [ ppr co, ppr k, ppr ktv, ppr ktv_kind ] ))
1330 ; return (Type.extendTvSubst subst_l ktv t1,
1331 Type.extendTvSubst subst_r ktv t2) }
1332
1333 lintCoercion co@(SubCo co')
1334 = do { (k,s,t,r) <- lintCoercion co'
1335 ; checkRole co Nominal r
1336 ; return (k,s,t,Representational) }
1337
1338
1339 lintCoercion this@(AxiomRuleCo co ts cs)
1340 = do _ks <- mapM lintType ts
1341 eqs <- mapM lintCoercion cs
1342
1343 let tyNum = length ts
1344
1345 case compare (coaxrTypeArity co) tyNum of
1346 EQ -> return ()
1347 LT -> err "Too many type arguments"
1348 [ txt "expected" <+> int (coaxrTypeArity co)
1349 , txt "provided" <+> int tyNum ]
1350 GT -> err "Not enough type arguments"
1351 [ txt "expected" <+> int (coaxrTypeArity co)
1352 , txt "provided" <+> int tyNum ]
1353 checkRoles 0 (coaxrAsmpRoles co) eqs
1354
1355 case coaxrProves co ts [ Pair l r | (_,l,r,_) <- eqs ] of
1356 Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
1357 Just (Pair l r) ->
1358 do kL <- lintType l
1359 kR <- lintType r
1360 unless (eqKind kL kR)
1361 $ err "Kind error in CoAxiomRule"
1362 [ppr kL <+> txt "/=" <+> ppr kR]
1363 return (kL, l, r, coaxrRole co)
1364 where
1365 txt = ptext . sLit
1366 err m xs = failWithL $
1367 hang (txt m) 2 $ vcat (txt "Rule:" <+> ppr (coaxrName co) : xs)
1368
1369 checkRoles n (e : es) ((_,_,_,r) : rs)
1370 | e == r = checkRoles (n+1) es rs
1371 | otherwise = err "Argument roles mismatch"
1372 [ txt "In argument:" <+> int (n+1)
1373 , txt "Expected:" <+> ppr e
1374 , txt "Found:" <+> ppr r ]
1375 checkRoles _ [] [] = return ()
1376 checkRoles n [] rs = err "Too many coercion arguments"
1377 [ txt "Expected:" <+> int n
1378 , txt "Provided:" <+> int (n + length rs) ]
1379
1380 checkRoles n es [] = err "Not enough coercion arguments"
1381 [ txt "Expected:" <+> int (n + length es)
1382 , txt "Provided:" <+> int n ]
1383
1384 {-
1385 ************************************************************************
1386 * *
1387 \subsection[lint-monad]{The Lint monad}
1388 * *
1389 ************************************************************************
1390 -}
1391
1392 -- If you edit this type, you may need to update the GHC formalism
1393 -- See Note [GHC Formalism]
1394 data LintEnv
1395 = LE { le_flags :: LintFlags -- Linting the result of this pass
1396 , le_loc :: [LintLocInfo] -- Locations
1397 , le_subst :: TvSubst -- Current type substitution; we also use this
1398 -- to keep track of all the variables in scope,
1399 -- both Ids and TyVars
1400 , le_dynflags :: DynFlags -- DynamicFlags
1401 }
1402
1403 data LintFlags
1404 = LF { lf_check_global_ids :: Bool -- See Note [Checking for global Ids]
1405 , lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers]
1406 }
1407
1408 defaultLintFlags :: LintFlags
1409 defaultLintFlags = LF { lf_check_global_ids = False
1410 , lf_check_inline_loop_breakers = True }
1411
1412 newtype LintM a =
1413 LintM { unLintM ::
1414 LintEnv ->
1415 WarnsAndErrs -> -- Error and warning messages so far
1416 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
1417
1418 type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)
1419
1420 {- Note [Checking for global Ids]
1421 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1422 Before CoreTidy, all locally-bound Ids must be LocalIds, even
1423 top-level ones. See Note [Exported LocalIds] and Trac #9857.
1424
1425 Note [Type substitution]
1426 ~~~~~~~~~~~~~~~~~~~~~~~~
1427 Why do we need a type substitution? Consider
1428 /\(a:*). \(x:a). /\(a:*). id a x
1429 This is ill typed, because (renaming variables) it is really
1430 /\(a:*). \(x:a). /\(b:*). id b x
1431 Hence, when checking an application, we can't naively compare x's type
1432 (at its binding site) with its expected type (at a use site). So we
1433 rename type binders as we go, maintaining a substitution.
1434
1435 The same substitution also supports let-type, current expressed as
1436 (/\(a:*). body) ty
1437 Here we substitute 'ty' for 'a' in 'body', on the fly.
1438 -}
1439
1440 instance Functor LintM where
1441 fmap = liftM
1442
1443 instance Applicative LintM where
1444 pure = return
1445 (<*>) = ap
1446
1447 instance Monad LintM where
1448 return x = LintM (\ _ errs -> (Just x, errs))
1449 fail err = failWithL (text err)
1450 m >>= k = LintM (\ env errs ->
1451 let (res, errs') = unLintM m env errs in
1452 case res of
1453 Just r -> unLintM (k r) env errs'
1454 Nothing -> (Nothing, errs'))
1455
1456 instance HasDynFlags LintM where
1457 getDynFlags = LintM (\ e errs -> (Just (le_dynflags e), errs))
1458
1459 data LintLocInfo
1460 = RhsOf Id -- The variable bound
1461 | LambdaBodyOf Id -- The lambda-binder
1462 | BodyOfLetRec [Id] -- One of the binders
1463 | CaseAlt CoreAlt -- Case alternative
1464 | CasePat CoreAlt -- The *pattern* of the case alternative
1465 | AnExpr CoreExpr -- Some expression
1466 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
1467 | TopLevelBindings
1468 | InType Type -- Inside a type
1469 | InCo Coercion -- Inside a coercion
1470
1471 initL :: DynFlags -> LintFlags -> LintM a -> WarnsAndErrs -- Errors and warnings
1472 initL dflags flags m
1473 = case unLintM m env (emptyBag, emptyBag) of
1474 (_, errs) -> errs
1475 where
1476 env = LE { le_flags = flags, le_subst = emptyTvSubst, le_loc = [], le_dynflags = dflags }
1477
1478 getLintFlags :: LintM LintFlags
1479 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
1480
1481 checkL :: Bool -> MsgDoc -> LintM ()
1482 checkL True _ = return ()
1483 checkL False msg = failWithL msg
1484
1485 checkWarnL :: Bool -> MsgDoc -> LintM ()
1486 checkWarnL True _ = return ()
1487 checkWarnL False msg = addWarnL msg
1488
1489 failWithL :: MsgDoc -> LintM a
1490 failWithL msg = LintM $ \ env (warns,errs) ->
1491 (Nothing, (warns, addMsg env errs msg))
1492
1493 addErrL :: MsgDoc -> LintM ()
1494 addErrL msg = LintM $ \ env (warns,errs) ->
1495 (Just (), (warns, addMsg env errs msg))
1496
1497 addWarnL :: MsgDoc -> LintM ()
1498 addWarnL msg = LintM $ \ env (warns,errs) ->
1499 (Just (), (addMsg env warns msg, errs))
1500
1501 addMsg :: LintEnv -> Bag MsgDoc -> MsgDoc -> Bag MsgDoc
1502 addMsg env msgs msg
1503 = ASSERT( notNull locs )
1504 msgs `snocBag` mk_msg msg
1505 where
1506 locs = le_loc env
1507 (loc, cxt1) = dumpLoc (head locs)
1508 cxts = [snd (dumpLoc loc) | loc <- locs]
1509 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
1510 ptext (sLit "Substitution:") <+> ppr (le_subst env)
1511 | otherwise = cxt1
1512
1513 mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
1514
1515 addLoc :: LintLocInfo -> LintM a -> LintM a
1516 addLoc extra_loc m
1517 = LintM $ \ env errs ->
1518 unLintM m (env { le_loc = extra_loc : le_loc env }) errs
1519
1520 inCasePat :: LintM Bool -- A slight hack; see the unique call site
1521 inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
1522 where
1523 is_case_pat (LE { le_loc = CasePat {} : _ }) = True
1524 is_case_pat _other = False
1525
1526 addInScopeVars :: [Var] -> LintM a -> LintM a
1527 addInScopeVars vars m
1528 = LintM $ \ env errs ->
1529 unLintM m (env { le_subst = extendTvInScopeList (le_subst env) vars })
1530 errs
1531
1532 addInScopeVar :: Var -> LintM a -> LintM a
1533 addInScopeVar var m
1534 = LintM $ \ env errs ->
1535 unLintM m (env { le_subst = extendTvInScope (le_subst env) var }) errs
1536
1537 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
1538 extendSubstL tv ty m
1539 = LintM $ \ env errs ->
1540 unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
1541
1542 updateTvSubst :: TvSubst -> LintM a -> LintM a
1543 updateTvSubst subst' m
1544 = LintM $ \ env errs -> unLintM m (env { le_subst = subst' }) errs
1545
1546 getTvSubst :: LintM TvSubst
1547 getTvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
1548
1549 getInScope :: LintM InScopeSet
1550 getInScope = LintM (\ env errs -> (Just (getTvInScope (le_subst env)), errs))
1551
1552 applySubstTy :: InType -> LintM OutType
1553 applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
1554
1555 applySubstCo :: InCoercion -> LintM OutCoercion
1556 applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
1557
1558 lookupIdInScope :: Id -> LintM Id
1559 lookupIdInScope id
1560 | not (mustHaveLocalBinding id)
1561 = return id -- An imported Id
1562 | otherwise
1563 = do { subst <- getTvSubst
1564 ; case lookupInScope (getTvInScope subst) id of
1565 Just v -> return v
1566 Nothing -> do { addErrL out_of_scope
1567 ; return id } }
1568 where
1569 out_of_scope = pprBndr LetBind id <+> ptext (sLit "is out of scope")
1570
1571
1572 oneTupleDataConId :: Id -- Should not happen
1573 oneTupleDataConId = dataConWorkId (tupleDataCon Boxed 1)
1574
1575 checkBndrIdInScope :: Var -> Var -> LintM ()
1576 checkBndrIdInScope binder id
1577 = checkInScope msg id
1578 where
1579 msg = ptext (sLit "is out of scope inside info for") <+>
1580 ppr binder
1581
1582 checkTyCoVarInScope :: Var -> LintM ()
1583 checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
1584
1585 checkInScope :: SDoc -> Var -> LintM ()
1586 checkInScope loc_msg var =
1587 do { subst <- getTvSubst
1588 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
1589 (hsep [pprBndr LetBind var, loc_msg]) }
1590
1591 checkTys :: OutType -> OutType -> MsgDoc -> LintM ()
1592 -- check ty2 is subtype of ty1 (ie, has same structure but usage
1593 -- annotations need only be consistent, not equal)
1594 -- Assumes ty1,ty2 are have alrady had the substitution applied
1595 checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
1596
1597 checkRole :: Coercion
1598 -> Role -- expected
1599 -> Role -- actual
1600 -> LintM ()
1601 checkRole co r1 r2
1602 = checkL (r1 == r2)
1603 (ptext (sLit "Role incompatibility: expected") <+> ppr r1 <> comma <+>
1604 ptext (sLit "got") <+> ppr r2 $$
1605 ptext (sLit "in") <+> ppr co)
1606
1607 {-
1608 ************************************************************************
1609 * *
1610 \subsection{Error messages}
1611 * *
1612 ************************************************************************
1613 -}
1614
1615 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
1616
1617 dumpLoc (RhsOf v)
1618 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
1619
1620 dumpLoc (LambdaBodyOf b)
1621 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
1622
1623 dumpLoc (BodyOfLetRec [])
1624 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
1625
1626 dumpLoc (BodyOfLetRec bs@(_:_))
1627 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
1628
1629 dumpLoc (AnExpr e)
1630 = (noSrcLoc, text "In the expression:" <+> ppr e)
1631
1632 dumpLoc (CaseAlt (con, args, _))
1633 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1634
1635 dumpLoc (CasePat (con, args, _))
1636 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1637
1638 dumpLoc (ImportedUnfolding locn)
1639 = (locn, brackets (ptext (sLit "in an imported unfolding")))
1640 dumpLoc TopLevelBindings
1641 = (noSrcLoc, Outputable.empty)
1642 dumpLoc (InType ty)
1643 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1644 dumpLoc (InCo co)
1645 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
1646
1647 pp_binders :: [Var] -> SDoc
1648 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1649
1650 pp_binder :: Var -> SDoc
1651 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1652 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1653
1654 ------------------------------------------------------
1655 -- Messages for case expressions
1656
1657 mkDefaultArgsMsg :: [Var] -> MsgDoc
1658 mkDefaultArgsMsg args
1659 = hang (text "DEFAULT case with binders")
1660 4 (ppr args)
1661
1662 mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
1663 mkCaseAltMsg e ty1 ty2
1664 = hang (text "Type of case alternatives not the same as the annotation on case:")
1665 4 (vcat [ppr ty1, ppr ty2, ppr e])
1666
1667 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> MsgDoc
1668 mkScrutMsg var var_ty scrut_ty subst
1669 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1670 text "Result binder type:" <+> ppr var_ty,--(idType var),
1671 text "Scrutinee type:" <+> ppr scrut_ty,
1672 hsep [ptext (sLit "Current TV subst"), ppr subst]]
1673
1674 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
1675 mkNonDefltMsg e
1676 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1677 mkNonIncreasingAltsMsg e
1678 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1679
1680 nonExhaustiveAltsMsg :: CoreExpr -> MsgDoc
1681 nonExhaustiveAltsMsg e
1682 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1683
1684 mkBadConMsg :: TyCon -> DataCon -> MsgDoc
1685 mkBadConMsg tycon datacon
1686 = vcat [
1687 text "In a case alternative, data constructor isn't in scrutinee type:",
1688 text "Scrutinee type constructor:" <+> ppr tycon,
1689 text "Data con:" <+> ppr datacon
1690 ]
1691
1692 mkBadPatMsg :: Type -> Type -> MsgDoc
1693 mkBadPatMsg con_result_ty scrut_ty
1694 = vcat [
1695 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1696 text "Pattern result type:" <+> ppr con_result_ty,
1697 text "Scrutinee type:" <+> ppr scrut_ty
1698 ]
1699
1700 integerScrutinisedMsg :: MsgDoc
1701 integerScrutinisedMsg
1702 = text "In a LitAlt, the literal is lifted (probably Integer)"
1703
1704 mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
1705 mkBadAltMsg scrut_ty alt
1706 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1707 text "Scrutinee type:" <+> ppr scrut_ty,
1708 text "Alternative:" <+> pprCoreAlt alt ]
1709
1710 mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc
1711 mkNewTyDataConAltMsg scrut_ty alt
1712 = vcat [ text "Data alternative for newtype datacon",
1713 text "Scrutinee type:" <+> ppr scrut_ty,
1714 text "Alternative:" <+> pprCoreAlt alt ]
1715
1716
1717 ------------------------------------------------------
1718 -- Other error messages
1719
1720 mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1721 mkAppMsg fun_ty arg_ty arg
1722 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1723 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1724 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1725 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1726
1727 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1728 mkNonFunAppMsg fun_ty arg_ty arg
1729 = vcat [ptext (sLit "Non-function type in function position"),
1730 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1731 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1732 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1733
1734 mkLetErr :: TyVar -> CoreExpr -> MsgDoc
1735 mkLetErr bndr rhs
1736 = vcat [ptext (sLit "Bad `let' binding:"),
1737 hang (ptext (sLit "Variable:"))
1738 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
1739 hang (ptext (sLit "Rhs:"))
1740 4 (ppr rhs)]
1741
1742 mkTyAppMsg :: Type -> Type -> MsgDoc
1743 mkTyAppMsg ty arg_ty
1744 = vcat [text "Illegal type application:",
1745 hang (ptext (sLit "Exp type:"))
1746 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1747 hang (ptext (sLit "Arg type:"))
1748 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1749
1750 mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc
1751 mkRhsMsg binder what ty
1752 = vcat
1753 [hsep [ptext (sLit "The type of this binder doesn't match the type of its") <+> what <> colon,
1754 ppr binder],
1755 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1756 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1757
1758 mkLetAppMsg :: CoreExpr -> MsgDoc
1759 mkLetAppMsg e
1760 = hang (ptext (sLit "This argument does not satisfy the let/app invariant:"))
1761 2 (ppr e)
1762
1763 mkRhsPrimMsg :: Id -> CoreExpr -> MsgDoc
1764 mkRhsPrimMsg binder _rhs
1765 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1766 ppr binder],
1767 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1768 ]
1769
1770 mkStrictMsg :: Id -> MsgDoc
1771 mkStrictMsg binder
1772 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1773 ppr binder],
1774 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1775 ]
1776
1777 mkNonTopExportedMsg :: Id -> MsgDoc
1778 mkNonTopExportedMsg binder
1779 = hsep [ptext (sLit "Non-top-level binder is marked as exported:"), ppr binder]
1780
1781 mkNonTopExternalNameMsg :: Id -> MsgDoc
1782 mkNonTopExternalNameMsg binder
1783 = hsep [ptext (sLit "Non-top-level binder has an external name:"), ppr binder]
1784
1785 mkKindErrMsg :: TyVar -> Type -> MsgDoc
1786 mkKindErrMsg tyvar arg_ty
1787 = vcat [ptext (sLit "Kinds don't match in type application:"),
1788 hang (ptext (sLit "Type variable:"))
1789 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1790 hang (ptext (sLit "Arg type:"))
1791 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1792
1793 {- Not needed now
1794 mkArityMsg :: Id -> MsgDoc
1795 mkArityMsg binder
1796 = vcat [hsep [ptext (sLit "Demand type has"),
1797 ppr (dmdTypeDepth dmd_ty),
1798 ptext (sLit "arguments, rhs has"),
1799 ppr (idArity binder),
1800 ptext (sLit "arguments,"),
1801 ppr binder],
1802 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1803
1804 ]
1805 where (StrictSig dmd_ty) = idStrictness binder
1806 -}
1807 mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> MsgDoc
1808 mkCastErr expr co from_ty expr_ty
1809 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1810 ptext (sLit "From-type:") <+> ppr from_ty,
1811 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty,
1812 ptext (sLit "Actual enclosed expr:") <+> ppr expr,
1813 ptext (sLit "Coercion used in cast:") <+> ppr co
1814 ]
1815
1816 dupVars :: [[Var]] -> MsgDoc
1817 dupVars vars
1818 = hang (ptext (sLit "Duplicate variables brought into scope"))
1819 2 (ppr vars)
1820
1821 dupExtVars :: [[Name]] -> MsgDoc
1822 dupExtVars vars
1823 = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))
1824 2 (ppr vars)
1825
1826 {-
1827 ************************************************************************
1828 * *
1829 \subsection{Annotation Linting}
1830 * *
1831 ************************************************************************
1832 -}
1833
1834 -- | This checks whether a pass correctly looks through debug
1835 -- annotations (@SourceNote@). This works a bit different from other
1836 -- consistency checks: We check this by running the given task twice,
1837 -- noting all differences between the results.
1838 lintAnnots :: SDoc -> (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
1839 lintAnnots pname pass guts = do
1840 -- Run the pass as we normally would
1841 dflags <- getDynFlags
1842 when (gopt Opt_DoAnnotationLinting dflags) $
1843 liftIO $ Err.showPass dflags "Annotation linting - first run"
1844 nguts <- pass guts
1845 -- If appropriate re-run it without debug annotations to make sure
1846 -- that they made no difference.
1847 when (gopt Opt_DoAnnotationLinting dflags) $ do
1848 liftIO $ Err.showPass dflags "Annotation linting - second run"
1849 nguts' <- withoutAnnots pass guts
1850 -- Finally compare the resulting bindings
1851 liftIO $ Err.showPass dflags "Annotation linting - comparison"
1852 let binds = flattenBinds $ mg_binds nguts
1853 binds' = flattenBinds $ mg_binds nguts'
1854 (diffs,_) = diffBinds True (mkRnEnv2 emptyInScopeSet) binds binds'
1855 when (not (null diffs)) $ CoreMonad.putMsg $ vcat
1856 [ lint_banner "warning" pname
1857 , text "Core changes with annotations:"
1858 , withPprStyle defaultDumpStyle $ nest 2 $ vcat diffs
1859 ]
1860 -- Return actual new guts
1861 return nguts
1862
1863 -- | Run the given pass without annotations. This means that we both
1864 -- remove the @Opt_Debug@ flag from the environment as well as all
1865 -- annotations from incoming modules.
1866 withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
1867 withoutAnnots pass guts = do
1868 -- Remove debug flag from environment.
1869 dflags <- getDynFlags
1870 let removeFlag env = env{hsc_dflags = gopt_unset dflags Opt_Debug}
1871 withoutFlag corem =
1872 liftIO =<< runCoreM <$> fmap removeFlag getHscEnv <*> getRuleBase <*>
1873 getUniqueSupplyM <*> getModule <*>
1874 getVisibleOrphanMods <*>
1875 getPrintUnqualified <*> pure corem
1876 -- Nuke existing ticks in module.
1877 -- TODO: Ticks in unfoldings. Maybe change unfolding so it removes
1878 -- them in absence of @Opt_Debug@?
1879 let nukeTicks = stripTicksE (not . tickishIsCode)
1880 nukeAnnotsBind :: CoreBind -> CoreBind
1881 nukeAnnotsBind bind = case bind of
1882 Rec bs -> Rec $ map (\(b,e) -> (b, nukeTicks e)) bs
1883 NonRec b e -> NonRec b $ nukeTicks e
1884 nukeAnnotsMod mg@ModGuts{mg_binds=binds}
1885 = mg{mg_binds = map nukeAnnotsBind binds}
1886 -- Perform pass with all changes applied
1887 fmap fst $ withoutFlag $ pass (nukeAnnotsMod guts)