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