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