73e93eaf3575d94bd5282b6f1ed59740747f07da
[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 , Just (fun, args) <- collectStaticPtrSatArgs rhs'
556 = flip fix binders0 $ \loopBinders binders -> case binders of
557 -- imitate @lintCoreExpr (Lam ...)@
558 var : vars -> addLoc (LambdaBodyOf var) $
559 lintBinder var $ \var' ->
560 do { body_ty <- loopBinders vars
561 ; return $ mkLamType var' body_ty }
562 -- imitate @lintCoreExpr (App ...)@
563 [] -> do
564 fun_ty <- lintCoreExpr fun
565 addLoc (AnExpr rhs') $ foldM lintCoreArg fun_ty args
566 -- Rejects applications of the data constructor @StaticPtr@ if it finds any.
567 lintRhs rhs = lintCoreExpr rhs
568
569 lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
570 lintIdUnfolding bndr bndr_ty (CoreUnfolding { uf_tmpl = rhs, uf_src = src })
571 | isStableSource src
572 = do { ty <- lintCoreExpr rhs
573 ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) }
574 lintIdUnfolding _ _ _
575 = return () -- Do not Lint unstable unfoldings, because that leads
576 -- to exponential behaviour; c.f. CoreFVs.idUnfoldingVars
577
578 {-
579 Note [Checking for INLINE loop breakers]
580 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
581 It's very suspicious if a strong loop breaker is marked INLINE.
582
583 However, the desugarer generates instance methods with INLINE pragmas
584 that form a mutually recursive group. Only after a round of
585 simplification are they unravelled. So we suppress the test for
586 the desugarer.
587
588 ************************************************************************
589 * *
590 \subsection[lintCoreExpr]{lintCoreExpr}
591 * *
592 ************************************************************************
593 -}
594
595 type InType = Type
596 type InCoercion = Coercion
597 type InVar = Var
598 type InTyVar = Var
599 type InCoVar = Var
600
601 type OutType = Type -- Substitution has been applied to this,
602 -- but has not been linted yet
603 type OutKind = Kind
604
605 type LintedType = Type -- Substitution applied, and type is linted
606 type LintedKind = Kind
607
608 type OutCoercion = Coercion
609 type OutVar = Var
610 type OutTyVar = TyVar
611 type OutCoVar = Var
612
613 lintCoreExpr :: CoreExpr -> LintM OutType
614 -- The returned type has the substitution from the monad
615 -- already applied to it:
616 -- lintCoreExpr e subst = exprType (subst e)
617 --
618 -- The returned "type" can be a kind, if the expression is (Type ty)
619
620 -- If you edit this function, you may need to update the GHC formalism
621 -- See Note [GHC Formalism]
622 lintCoreExpr (Var var)
623 = do { checkL (isNonCoVarId var)
624 (text "Non term variable" <+> ppr var)
625
626 ; checkDeadIdOcc var
627 ; var' <- lookupIdInScope var
628 ; return (idType var') }
629
630 lintCoreExpr (Lit lit)
631 = return (literalType lit)
632
633 lintCoreExpr (Cast expr co)
634 = do { expr_ty <- lintCoreExpr expr
635 ; co' <- applySubstCo co
636 ; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
637 ; lintL (classifiesTypeWithValues k2)
638 (text "Target of cast not # or *:" <+> ppr co)
639 ; lintRole co' Representational r
640 ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
641 ; return to_ty }
642
643 lintCoreExpr (Tick (Breakpoint _ ids) expr)
644 = do forM_ ids $ \id -> do
645 checkDeadIdOcc id
646 lookupIdInScope id
647 lintCoreExpr expr
648
649 lintCoreExpr (Tick _other_tickish expr)
650 = lintCoreExpr expr
651
652 lintCoreExpr (Let (NonRec tv (Type ty)) body)
653 | isTyVar tv
654 = -- See Note [Linting type lets]
655 do { ty' <- applySubstTy ty
656 ; lintTyBndr tv $ \ tv' ->
657 do { addLoc (RhsOf tv) $ lintTyKind tv' ty'
658 -- Now extend the substitution so we
659 -- take advantage of it in the body
660 ; extendSubstL tv' ty' $
661 addLoc (BodyOfLetRec [tv]) $
662 lintCoreExpr body } }
663
664 lintCoreExpr (Let (NonRec bndr rhs) body)
665 | isId bndr
666 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
667 ; addLoc (BodyOfLetRec [bndr])
668 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
669
670 | otherwise
671 = failWithL (mkLetErr bndr rhs) -- Not quite accurate
672
673 lintCoreExpr (Let (Rec pairs) body)
674 = lintAndScopeIds bndrs $ \_ ->
675 do { checkL (null dups) (dupVars dups)
676 ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
677 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
678 where
679 bndrs = map fst pairs
680 (_, dups) = removeDups compare bndrs
681
682 lintCoreExpr e@(App _ _)
683 = do lf <- getLintFlags
684 -- Check for a nested occurrence of the StaticPtr constructor.
685 -- See Note [Checking StaticPtrs].
686 case fun of
687 Var b | lf_check_static_ptrs lf
688 , Just con <- isDataConId_maybe b
689 , dataConName con == staticPtrDataConName
690 -> do
691 failWithL $ text "Found StaticPtr nested in an expression: " <+>
692 ppr e
693 _ -> go
694 where
695 go = do { fun_ty <- lintCoreExpr fun
696 ; addLoc (AnExpr e) $ foldM lintCoreArg fun_ty args }
697
698 (fun, args) = collectArgs e
699
700 lintCoreExpr (Lam var expr)
701 = addLoc (LambdaBodyOf var) $
702 lintBinder var $ \ var' ->
703 do { body_ty <- lintCoreExpr expr
704 ; return $ mkLamType var' body_ty }
705
706 lintCoreExpr e@(Case scrut var alt_ty alts) =
707 -- Check the scrutinee
708 do { let scrut_diverges = exprIsBottom scrut
709 ; scrut_ty <- lintCoreExpr scrut
710 ; (alt_ty, _) <- lintInTy alt_ty
711 ; (var_ty, _) <- lintInTy (idType var)
712
713 -- See Note [No alternatives lint check]
714 ; when (null alts) $
715 do { checkL (not (exprIsHNF scrut))
716 (text "No alternatives for a case scrutinee in head-normal form:" <+> ppr scrut)
717 ; checkL scrut_diverges
718 (text "No alternatives for a case scrutinee not known to diverge for sure:" <+> ppr scrut)
719 }
720
721 -- See Note [Rules for floating-point comparisons] in PrelRules
722 ; let isLitPat (LitAlt _, _ , _) = True
723 isLitPat _ = False
724 ; checkL (not $ isFloatingTy scrut_ty && any isLitPat alts)
725 (ptext (sLit $ "Lint warning: Scrutinising floating-point " ++
726 "expression with literal pattern in case " ++
727 "analysis (see Trac #9238).")
728 $$ text "scrut" <+> ppr scrut)
729
730 ; case tyConAppTyCon_maybe (idType var) of
731 Just tycon
732 | debugIsOn
733 , isAlgTyCon tycon
734 , not (isAbstractTyCon tycon)
735 , null (tyConDataCons tycon)
736 , not scrut_diverges
737 -> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
738 -- This can legitimately happen for type families
739 $ return ()
740 _otherwise -> return ()
741
742 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
743
744 ; subst <- getTCvSubst
745 ; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
746
747 ; lintAndScopeId var $ \_ ->
748 do { -- Check the alternatives
749 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
750 ; checkCaseAlts e scrut_ty alts
751 ; return alt_ty } }
752
753 -- This case can't happen; linting types in expressions gets routed through
754 -- lintCoreArgs
755 lintCoreExpr (Type ty)
756 = failWithL (text "Type found as expression" <+> ppr ty)
757
758 lintCoreExpr (Coercion co)
759 = do { (k1, k2, ty1, ty2, role) <- lintInCo co
760 ; return (mkHeteroCoercionType role k1 k2 ty1 ty2) }
761
762 {-
763 Note [No alternatives lint check]
764 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
765 Case expressions with no alternatives are odd beasts, and worth looking at
766 in the linter (cf Trac #10180). We check two things:
767
768 * exprIsHNF is false: certainly, it would be terribly wrong if the
769 scrutinee was already in head normal form.
770
771 * exprIsBottom is true: we should be able to see why GHC believes the
772 scrutinee is diverging for sure.
773
774 In principle, the first check is redundant: exprIsBottom == True will
775 always imply exprIsHNF == False. But the first check is reliable: If
776 exprIsHNF == True, then there definitely is a problem (exprIsHNF errs
777 on the right side). If the second check triggers then it may be the
778 case that the compiler got smarter elsewhere, and the empty case is
779 correct, but that exprIsBottom is unable to see it. In particular, the
780 empty-type check in exprIsBottom is an approximation. Therefore, this
781 check is not fully reliable, and we keep both around.
782
783 ************************************************************************
784 * *
785 \subsection[lintCoreArgs]{lintCoreArgs}
786 * *
787 ************************************************************************
788
789 The basic version of these functions checks that the argument is a
790 subtype of the required type, as one would expect.
791 -}
792
793 lintCoreArg :: OutType -> CoreArg -> LintM OutType
794 lintCoreArg fun_ty (Type arg_ty)
795 = do { checkL (not (isCoercionTy arg_ty))
796 (text "Unnecessary coercion-to-type injection:"
797 <+> ppr arg_ty)
798 ; arg_ty' <- applySubstTy arg_ty
799 ; lintTyApp fun_ty arg_ty' }
800
801 lintCoreArg fun_ty arg
802 = do { arg_ty <- lintCoreExpr arg
803 ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
804 (mkLetAppMsg arg)
805 ; lintValApp arg fun_ty arg_ty }
806
807 -----------------
808 lintAltBinders :: OutType -- Scrutinee type
809 -> OutType -- Constructor type
810 -> [OutVar] -- Binders
811 -> LintM ()
812 -- If you edit this function, you may need to update the GHC formalism
813 -- See Note [GHC Formalism]
814 lintAltBinders scrut_ty con_ty []
815 = ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
816 lintAltBinders scrut_ty con_ty (bndr:bndrs)
817 | isTyVar bndr
818 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
819 ; lintAltBinders scrut_ty con_ty' bndrs }
820 | otherwise
821 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
822 ; lintAltBinders scrut_ty con_ty' bndrs }
823
824 -----------------
825 lintTyApp :: OutType -> OutType -> LintM OutType
826 lintTyApp fun_ty arg_ty
827 | Just (tv,body_ty) <- splitForAllTy_maybe fun_ty
828 = do { lintTyKind tv arg_ty
829 ; in_scope <- getInScope
830 -- substTy needs the set of tyvars in scope to avoid generating
831 -- uniques that are already in scope.
832 -- See Note [The substitution invariant] in TyCoRep
833 ; return (substTyWithInScope in_scope [tv] [arg_ty] body_ty) }
834
835 | otherwise
836 = failWithL (mkTyAppMsg fun_ty arg_ty)
837
838 -----------------
839 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
840 lintValApp arg fun_ty arg_ty
841 | Just (arg,res) <- splitFunTy_maybe fun_ty
842 = do { ensureEqTys arg arg_ty err1
843 ; return res }
844 | otherwise
845 = failWithL err2
846 where
847 err1 = mkAppMsg fun_ty arg_ty arg
848 err2 = mkNonFunAppMsg fun_ty arg_ty arg
849
850 lintTyKind :: OutTyVar -> OutType -> LintM ()
851 -- Both args have had substitution applied
852
853 -- If you edit this function, you may need to update the GHC formalism
854 -- See Note [GHC Formalism]
855 lintTyKind tyvar arg_ty
856 -- Arg type might be boxed for a function with an uncommitted
857 -- tyvar; notably this is used so that we can give
858 -- error :: forall a:*. String -> a
859 -- and then apply it to both boxed and unboxed types.
860 = do { arg_kind <- lintType arg_ty
861 ; unless (arg_kind `eqType` tyvar_kind)
862 (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
863 where
864 tyvar_kind = tyVarKind tyvar
865
866 checkDeadIdOcc :: Id -> LintM ()
867 -- Occurrences of an Id should never be dead....
868 -- except when we are checking a case pattern
869 checkDeadIdOcc id
870 | isDeadOcc (idOccInfo id)
871 = do { in_case <- inCasePat
872 ; checkL in_case
873 (text "Occurrence of a dead Id" <+> ppr id) }
874 | otherwise
875 = return ()
876
877 {-
878 ************************************************************************
879 * *
880 \subsection[lintCoreAlts]{lintCoreAlts}
881 * *
882 ************************************************************************
883 -}
884
885 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
886 -- a) Check that the alts are non-empty
887 -- b1) Check that the DEFAULT comes first, if it exists
888 -- b2) Check that the others are in increasing order
889 -- c) Check that there's a default for infinite types
890 -- NB: Algebraic cases are not necessarily exhaustive, because
891 -- the simplifier correctly eliminates case that can't
892 -- possibly match.
893
894 checkCaseAlts e ty alts =
895 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
896 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
897
898 -- For types Int#, Word# with an infinite (well, large!) number of
899 -- possible values, there should usually be a DEFAULT case
900 -- But (see Note [Empty case alternatives] in CoreSyn) it's ok to
901 -- have *no* case alternatives.
902 -- In effect, this is a kind of partial test. I suppose it's possible
903 -- that we might *know* that 'x' was 1 or 2, in which case
904 -- case x of { 1 -> e1; 2 -> e2 }
905 -- would be fine.
906 ; checkL (isJust maybe_deflt || not is_infinite_ty || null alts)
907 (nonExhaustiveAltsMsg e) }
908 where
909 (con_alts, maybe_deflt) = findDefault alts
910
911 -- Check that successive alternatives have increasing tags
912 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
913 increasing_tag _ = True
914
915 non_deflt (DEFAULT, _, _) = False
916 non_deflt _ = True
917
918 is_infinite_ty = case tyConAppTyCon_maybe ty of
919 Nothing -> False
920 Just tycon -> isPrimTyCon tycon
921
922 lintAltExpr :: CoreExpr -> OutType -> LintM ()
923 lintAltExpr expr ann_ty
924 = do { actual_ty <- lintCoreExpr expr
925 ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
926
927 lintCoreAlt :: OutType -- Type of scrutinee
928 -> OutType -- Type of the alternative
929 -> CoreAlt
930 -> LintM ()
931 -- If you edit this function, you may need to update the GHC formalism
932 -- See Note [GHC Formalism]
933 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
934 do { lintL (null args) (mkDefaultArgsMsg args)
935 ; lintAltExpr rhs alt_ty }
936
937 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
938 | litIsLifted lit
939 = failWithL integerScrutinisedMsg
940 | otherwise
941 = do { lintL (null args) (mkDefaultArgsMsg args)
942 ; ensureEqTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
943 ; lintAltExpr rhs alt_ty }
944 where
945 lit_ty = literalType lit
946
947 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
948 | isNewTyCon (dataConTyCon con)
949 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
950 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
951 = addLoc (CaseAlt alt) $ do
952 { -- First instantiate the universally quantified
953 -- type variables of the data constructor
954 -- We've already check
955 lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
956 ; let con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys
957
958 -- And now bring the new binders into scope
959 ; lintBinders args $ \ args' -> do
960 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
961 ; lintAltExpr rhs alt_ty } }
962
963 | otherwise -- Scrut-ty is wrong shape
964 = addErrL (mkBadAltMsg scrut_ty alt)
965
966 {-
967 ************************************************************************
968 * *
969 \subsection[lint-types]{Types}
970 * *
971 ************************************************************************
972 -}
973
974 -- When we lint binders, we (one at a time and in order):
975 -- 1. Lint var types or kinds (possibly substituting)
976 -- 2. Add the binder to the in scope set, and if its a coercion var,
977 -- we may extend the substitution to reflect its (possibly) new kind
978 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
979 lintBinders [] linterF = linterF []
980 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
981 lintBinders vars $ \ vars' ->
982 linterF (var':vars')
983
984 -- If you edit this function, you may need to update the GHC formalism
985 -- See Note [GHC Formalism]
986 lintBinder :: Var -> (Var -> LintM a) -> LintM a
987 lintBinder var linterF
988 | isTyVar var = lintTyBndr var linterF
989 | isCoVar var = lintCoBndr var linterF
990 | otherwise = lintIdBndr var linterF
991
992 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
993 lintTyBndr tv thing_inside
994 = do { subst <- getTCvSubst
995 ; let (subst', tv') = substTyVarBndr subst tv
996 ; lintKind (varType tv')
997 ; updateTCvSubst subst' (thing_inside tv') }
998
999 lintCoBndr :: InCoVar -> (OutCoVar -> LintM a) -> LintM a
1000 lintCoBndr cv thing_inside
1001 = do { subst <- getTCvSubst
1002 ; let (subst', cv') = substCoVarBndr subst cv
1003 ; lintKind (varType cv')
1004 ; lintL (isCoercionType (varType cv'))
1005 (text "CoVar with non-coercion type:" <+> pprTvBndr cv)
1006 ; updateTCvSubst subst' (thing_inside cv') }
1007
1008 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
1009 -- Do substitution on the type of a binder and add the var with this
1010 -- new type to the in-scope set of the second argument
1011 -- ToDo: lint its rules
1012
1013 lintIdBndr id linterF
1014 = do { lintAndScopeId id $ \id' -> linterF id' }
1015
1016 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
1017 lintAndScopeIds ids linterF
1018 = go ids
1019 where
1020 go [] = linterF []
1021 go (id:ids) = lintAndScopeId id $ \id ->
1022 lintAndScopeIds ids $ \ids ->
1023 linterF (id:ids)
1024
1025 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
1026 lintAndScopeId id linterF
1027 = do { flags <- getLintFlags
1028 ; checkL (not (lf_check_global_ids flags) || isLocalId id)
1029 (text "Non-local Id binder" <+> ppr id)
1030 -- See Note [Checking for global Ids]
1031 ; (ty, k) <- lintInTy (idType id)
1032 ; lintL (not (isRuntimeRepPolymorphic k))
1033 (text "RuntimeRep-polymorphic binder:" <+>
1034 (ppr id <+> dcolon <+> parens (ppr ty <+> dcolon <+> ppr k)))
1035 ; let id' = setIdType id ty
1036 ; addInScopeVar id' $ (linterF id') }
1037
1038 {-
1039 %************************************************************************
1040 %* *
1041 Types
1042 %* *
1043 %************************************************************************
1044 -}
1045
1046 lintInTy :: InType -> LintM (LintedType, LintedKind)
1047 -- Types only, not kinds
1048 -- Check the type, and apply the substitution to it
1049 -- See Note [Linting type lets]
1050 lintInTy ty
1051 = addLoc (InType ty) $
1052 do { ty' <- applySubstTy ty
1053 ; k <- lintType ty'
1054 ; lintKind k
1055 ; return (ty', k) }
1056
1057 checkTyCon :: TyCon -> LintM ()
1058 checkTyCon tc
1059 = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
1060
1061 -------------------
1062 lintType :: OutType -> LintM LintedKind
1063 -- The returned Kind has itself been linted
1064
1065 -- If you edit this function, you may need to update the GHC formalism
1066 -- See Note [GHC Formalism]
1067 lintType (TyVarTy tv)
1068 = do { checkL (isTyVar tv) (mkBadTyVarMsg tv)
1069 ; lintTyCoVarInScope tv
1070 ; return (tyVarKind tv) }
1071 -- We checked its kind when we added it to the envt
1072
1073 lintType ty@(AppTy t1 t2)
1074 | TyConApp {} <- t1
1075 = failWithL $ text "TyConApp to the left of AppTy:" <+> ppr ty
1076 | otherwise
1077 = do { k1 <- lintType t1
1078 ; k2 <- lintType t2
1079 ; lint_ty_app ty k1 [(t2,k2)] }
1080
1081 lintType ty@(TyConApp tc tys)
1082 | Just ty' <- coreView ty
1083 = lintType ty' -- Expand type synonyms, so that we do not bogusly complain
1084 -- about un-saturated type synonyms
1085
1086 | isUnliftedTyCon tc || isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
1087 -- Also type synonyms and type families
1088 , length tys < tyConArity tc
1089 = failWithL (hang (text "Un-saturated type application") 2 (ppr ty))
1090
1091 | otherwise
1092 = do { checkTyCon tc
1093 ; ks <- mapM lintType tys
1094 ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
1095
1096 -- arrows can related *unlifted* kinds, so this has to be separate from
1097 -- a dependent forall.
1098 lintType ty@(FunTy t1 t2)
1099 = do { k1 <- lintType t1
1100 ; k2 <- lintType t2
1101 ; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 }
1102
1103 lintType t@(ForAllTy (TvBndr tv _vis) ty)
1104 = do { lintL (isTyVar tv) (text "Covar bound in type:" <+> ppr t)
1105 ; lintTyBndr tv $ \tv' ->
1106 do { k <- lintType ty
1107 ; lintL (not (tv' `elemVarSet` tyCoVarsOfType k))
1108 (text "Variable escape in forall:" <+> ppr t)
1109 ; lintL (classifiesTypeWithValues k)
1110 (text "Non-* and non-# kind in forall:" <+> ppr t)
1111 ; return k }}
1112
1113 lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
1114
1115 lintType (CastTy ty co)
1116 = do { k1 <- lintType ty
1117 ; (k1', k2) <- lintStarCoercion co
1118 ; ensureEqTys k1 k1' (mkCastErr ty co k1' k1)
1119 ; return k2 }
1120
1121 lintType (CoercionTy co)
1122 = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
1123 ; return $ mkHeteroCoercionType r k1 k2 ty1 ty2 }
1124
1125 lintKind :: OutKind -> LintM ()
1126 -- If you edit this function, you may need to update the GHC formalism
1127 -- See Note [GHC Formalism]
1128 lintKind k = do { sk <- lintType k
1129 ; unless ((isStarKind sk) || (isUnliftedTypeKind sk))
1130 (addErrL (hang (text "Ill-kinded kind:" <+> ppr k)
1131 2 (text "has kind:" <+> ppr sk))) }
1132
1133 -- confirms that a type is really *
1134 lintStar :: SDoc -> OutKind -> LintM ()
1135 lintStar doc k
1136 = lintL (classifiesTypeWithValues k)
1137 (text "Non-*-like kind when *-like expected:" <+> ppr k $$
1138 text "when checking" <+> doc)
1139
1140 lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
1141 -- If you edit this function, you may need to update the GHC formalism
1142 -- See Note [GHC Formalism]
1143 lintArrow what k1 k2 -- Eg lintArrow "type or kind `blah'" k1 k2
1144 -- or lintarrow "coercion `blah'" k1 k2
1145 = do { unless (okArrowArgKind k1) (addErrL (msg (text "argument") k1))
1146 ; unless (okArrowResultKind k2) (addErrL (msg (text "result") k2))
1147 ; return liftedTypeKind }
1148 where
1149 msg ar k
1150 = vcat [ hang (text "Ill-kinded" <+> ar)
1151 2 (text "in" <+> what)
1152 , what <+> text "kind:" <+> ppr k ]
1153
1154 lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
1155 lint_ty_app ty k tys
1156 = lint_app (text "type" <+> quotes (ppr ty)) k tys
1157
1158 ----------------
1159 lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
1160 lint_co_app ty k tys
1161 = lint_app (text "coercion" <+> quotes (ppr ty)) k tys
1162
1163 ----------------
1164 lintTyLit :: TyLit -> LintM ()
1165 lintTyLit (NumTyLit n)
1166 | n >= 0 = return ()
1167 | otherwise = failWithL msg
1168 where msg = text "Negative type literal:" <+> integer n
1169 lintTyLit (StrTyLit _) = return ()
1170
1171 lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
1172 -- (lint_app d fun_kind arg_tys)
1173 -- We have an application (f arg_ty1 .. arg_tyn),
1174 -- where f :: fun_kind
1175 -- Takes care of linting the OutTypes
1176
1177 -- If you edit this function, you may need to update the GHC formalism
1178 -- See Note [GHC Formalism]
1179 lint_app doc kfn kas
1180 = do { in_scope <- getInScope
1181 -- We need the in_scope set to satisfy the invariant in
1182 -- Note [The substitution invariant] in TyCoRep
1183 ; foldlM (go_app in_scope) kfn kas }
1184 where
1185 fail_msg = vcat [ hang (text "Kind application error in") 2 doc
1186 , nest 2 (text "Function kind =" <+> ppr kfn)
1187 , nest 2 (text "Arg kinds =" <+> ppr kas) ]
1188
1189 go_app in_scope kfn ka
1190 | Just kfn' <- coreView kfn
1191 = go_app in_scope kfn' ka
1192
1193 go_app _ (FunTy kfa kfb) (_,ka)
1194 = do { unless (ka `eqType` kfa) (addErrL fail_msg)
1195 ; return kfb }
1196
1197 go_app in_scope (ForAllTy (TvBndr kv _vis) kfn) (ta,ka)
1198 = do { unless (ka `eqType` tyVarKind kv) (addErrL fail_msg)
1199 ; return (substTyWithInScope in_scope [kv] [ta] kfn) }
1200
1201 go_app _ _ _ = failWithL fail_msg
1202
1203 {- *********************************************************************
1204 * *
1205 Linting rules
1206 * *
1207 ********************************************************************* -}
1208
1209 lintCoreRule :: OutType -> CoreRule -> LintM ()
1210 lintCoreRule _ (BuiltinRule {})
1211 = return () -- Don't bother
1212
1213 lintCoreRule fun_ty (Rule { ru_name = name, ru_bndrs = bndrs
1214 , ru_args = args, ru_rhs = rhs })
1215 = lintBinders bndrs $ \ _ ->
1216 do { lhs_ty <- foldM lintCoreArg fun_ty args
1217 ; rhs_ty <- lintCoreExpr rhs
1218 ; ensureEqTys lhs_ty rhs_ty $
1219 (rule_doc <+> vcat [ text "lhs type:" <+> ppr lhs_ty
1220 , text "rhs type:" <+> ppr rhs_ty ])
1221 ; let bad_bndrs = filterOut (`elemVarSet` exprsFreeVars args) $
1222 filter (`elemVarSet` exprFreeVars rhs) $
1223 bndrs
1224
1225 ; checkL (null bad_bndrs)
1226 (rule_doc <+> text "unbound" <+> ppr bad_bndrs)
1227 -- See Note [Linting rules]
1228 }
1229 where
1230 rule_doc = text "Rule" <+> doubleQuotes (ftext name) <> colon
1231
1232 {- Note [Linting rules]
1233 ~~~~~~~~~~~~~~~~~~~~~~~
1234 It's very bad if simplifying a rule means that one of the template
1235 variables (ru_bndrs) that /is/ mentioned on the RHS becomes
1236 not-mentioned in the LHS (ru_args). How can that happen? Well, in
1237 Trac #10602, SpecConstr stupidly constructed a rule like
1238
1239 forall x,c1,c2.
1240 f (x |> c1 |> c2) = ....
1241
1242 But simplExpr collapses those coercions into one. (Indeed in
1243 Trac #10602, it collapsed to the identity and was removed altogether.)
1244
1245 We don't have a great story for what to do here, but at least
1246 this check will nail it.
1247
1248 NB (Trac #11643): it's possible that a variable listed in the
1249 binders becomes not-mentioned on both LHS and RHS. Here's a silly
1250 example:
1251 RULE forall x y. f (g x y) = g (x+1 (y-1)
1252 And suppose worker/wrapper decides that 'x' is Absent. Then
1253 we'll end up with
1254 RULE forall x y. f ($gw y) = $gw (x+1)
1255 This seems sufficiently obscure that there isn't enough payoff to
1256 try to trim the forall'd binder list.
1257 -}
1258
1259 {-
1260 ************************************************************************
1261 * *
1262 Linting coercions
1263 * *
1264 ************************************************************************
1265 -}
1266
1267 lintInCo :: InCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
1268 -- Check the coercion, and apply the substitution to it
1269 -- See Note [Linting type lets]
1270 lintInCo co
1271 = addLoc (InCo co) $
1272 do { co' <- applySubstCo co
1273 ; lintCoercion co' }
1274
1275 -- lints a coercion, confirming that its lh kind and its rh kind are both *
1276 -- also ensures that the role is Nominal
1277 lintStarCoercion :: OutCoercion -> LintM (LintedType, LintedType)
1278 lintStarCoercion g
1279 = do { (k1, k2, t1, t2, r) <- lintCoercion g
1280 ; lintStar (text "the kind of the left type in" <+> ppr g) k1
1281 ; lintStar (text "the kind of the right type in" <+> ppr g) k2
1282 ; lintRole g Nominal r
1283 ; return (t1, t2) }
1284
1285 lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
1286 -- Check the kind of a coercion term, returning the kind
1287 -- Post-condition: the returned OutTypes are lint-free
1288 --
1289 -- If lintCorecion co = (k1, k2, s1, s2, r)
1290 -- then co :: s1 ~r s2
1291 -- s1 :: k2
1292 -- s2 :: k2
1293
1294 -- If you edit this function, you may need to update the GHC formalism
1295 -- See Note [GHC Formalism]
1296 lintCoercion (Refl r ty)
1297 = do { k <- lintType ty
1298 ; return (k, k, ty, ty, r) }
1299
1300 lintCoercion co@(TyConAppCo r tc cos)
1301 | tc `hasKey` funTyConKey
1302 , [co1,co2] <- cos
1303 = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
1304 ; (k2,k'2,s2,t2,r2) <- lintCoercion co2
1305 ; k <- lintArrow (text "coercion" <+> quotes (ppr co)) k1 k2
1306 ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2
1307 ; lintRole co1 r r1
1308 ; lintRole co2 r r2
1309 ; return (k, k', mkFunTy s1 s2, mkFunTy t1 t2, r) }
1310
1311 | Just {} <- synTyConDefn_maybe tc
1312 = failWithL (text "Synonym in TyConAppCo:" <+> ppr co)
1313
1314 | otherwise
1315 = do { checkTyCon tc
1316 ; (k's, ks, ss, ts, rs) <- mapAndUnzip5M lintCoercion cos
1317 ; k' <- lint_co_app co (tyConKind tc) (ss `zip` k's)
1318 ; k <- lint_co_app co (tyConKind tc) (ts `zip` ks)
1319 ; _ <- zipWith3M lintRole cos (tyConRolesX r tc) rs
1320 ; return (k', k, mkTyConApp tc ss, mkTyConApp tc ts, r) }
1321
1322 lintCoercion co@(AppCo co1 co2)
1323 | TyConAppCo {} <- co1
1324 = failWithL (text "TyConAppCo to the left of AppCo:" <+> ppr co)
1325 | Refl _ (TyConApp {}) <- co1
1326 = failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co)
1327 | otherwise
1328 = do { (k1, k2, s1, s2, r1) <- lintCoercion co1
1329 ; (k'1, k'2, t1, t2, r2) <- lintCoercion co2
1330 ; k3 <- lint_co_app co k1 [(t1,k'1)]
1331 ; k4 <- lint_co_app co k2 [(t2,k'2)]
1332 ; if r1 == Phantom
1333 then lintL (r2 == Phantom || r2 == Nominal)
1334 (text "Second argument in AppCo cannot be R:" $$
1335 ppr co)
1336 else lintRole co Nominal r2
1337 ; return (k3, k4, mkAppTy s1 t1, mkAppTy s2 t2, r1) }
1338
1339 ----------
1340 lintCoercion (ForAllCo tv1 kind_co co)
1341 = do { (_, k2) <- lintStarCoercion kind_co
1342 ; let tv2 = setTyVarKind tv1 k2
1343 ; addInScopeVar tv1 $
1344 do {
1345 ; (k3, k4, t1, t2, r) <- lintCoercion co
1346 ; in_scope <- getInScope
1347 ; let tyl = mkInvForAllTy tv1 t1
1348 subst = mkTvSubst in_scope $
1349 -- We need both the free vars of the `t2` and the
1350 -- free vars of the range of the substitution in
1351 -- scope. All the free vars of `t2` and `kind_co` should
1352 -- already be in `in_scope`, because they've been
1353 -- linted and `tv2` has the same unique as `tv1`.
1354 -- See Note [The substitution invariant]
1355 unitVarEnv tv1 (TyVarTy tv2 `mkCastTy` mkSymCo kind_co)
1356 tyr = mkInvForAllTy tv2 $
1357 substTy subst t2
1358 ; return (k3, k4, tyl, tyr, r) } }
1359
1360 lintCoercion (CoVarCo cv)
1361 | not (isCoVar cv)
1362 = failWithL (hang (text "Bad CoVarCo:" <+> ppr cv)
1363 2 (text "With offending type:" <+> ppr (varType cv)))
1364 | otherwise
1365 = do { lintTyCoVarInScope cv
1366 ; cv' <- lookupIdInScope cv
1367 ; lintUnliftedCoVar cv
1368 ; return $ coVarKindsTypesRole cv' }
1369
1370 -- See Note [Bad unsafe coercion]
1371 lintCoercion co@(UnivCo prov r ty1 ty2)
1372 = do { k1 <- lintType ty1
1373 ; k2 <- lintType ty2
1374 ; case prov of
1375 UnsafeCoerceProv -> return () -- no extra checks
1376
1377 PhantomProv kco -> do { lintRole co Phantom r
1378 ; check_kinds kco k1 k2 }
1379
1380 ProofIrrelProv kco -> do { lintL (isCoercionTy ty1) $
1381 mkBadProofIrrelMsg ty1 co
1382 ; lintL (isCoercionTy ty2) $
1383 mkBadProofIrrelMsg ty2 co
1384 ; check_kinds kco k1 k2 }
1385
1386 PluginProv _ -> return () -- no extra checks
1387 HoleProv h -> addErrL $
1388 text "Unfilled coercion hole:" <+> ppr h
1389
1390 ; when (r /= Phantom && classifiesTypeWithValues k1
1391 && classifiesTypeWithValues k2)
1392 (checkTypes ty1 ty2)
1393 ; return (k1, k2, ty1, ty2, r) }
1394 where
1395 report s = hang (text $ "Unsafe coercion between " ++ s)
1396 2 (vcat [ text "From:" <+> ppr ty1
1397 , text " To:" <+> ppr ty2])
1398 isUnBoxed :: PrimRep -> Bool
1399 isUnBoxed PtrRep = False
1400 isUnBoxed _ = True
1401 checkTypes t1 t2
1402 = case (repType t1, repType t2) of
1403 (UnaryRep _, UnaryRep _) ->
1404 validateCoercion (typePrimRep t1)
1405 (typePrimRep t2)
1406 (UbxTupleRep rep1, UbxTupleRep rep2) -> do
1407 checkWarnL (length rep1 == length rep2)
1408 (report "unboxed tuples of different length")
1409 zipWithM_ checkTypes rep1 rep2
1410 _ -> addWarnL (report "unboxed tuple and ordinary type")
1411 validateCoercion :: PrimRep -> PrimRep -> LintM ()
1412 validateCoercion rep1 rep2
1413 = do { dflags <- getDynFlags
1414 ; checkWarnL (isUnBoxed rep1 == isUnBoxed rep2)
1415 (report "unboxed and boxed value")
1416 ; checkWarnL (TyCon.primRepSizeW dflags rep1
1417 == TyCon.primRepSizeW dflags rep2)
1418 (report "unboxed values of different size")
1419 ; let fl = liftM2 (==) (TyCon.primRepIsFloat rep1)
1420 (TyCon.primRepIsFloat rep2)
1421 ; case fl of
1422 Nothing -> addWarnL (report "vector types")
1423 Just False -> addWarnL (report "float and integral values")
1424 _ -> return ()
1425 }
1426
1427 check_kinds kco k1 k2 = do { (k1', k2') <- lintStarCoercion kco
1428 ; ensureEqTys k1 k1' (mkBadUnivCoMsg CLeft co)
1429 ; ensureEqTys k2 k2' (mkBadUnivCoMsg CRight co) }
1430
1431
1432 lintCoercion (SymCo co)
1433 = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
1434 ; return (k2, k1, ty2, ty1, r) }
1435
1436 lintCoercion co@(TransCo co1 co2)
1437 = do { (k1a, _k1b, ty1a, ty1b, r1) <- lintCoercion co1
1438 ; (_k2a, k2b, ty2a, ty2b, r2) <- lintCoercion co2
1439 ; ensureEqTys ty1b ty2a
1440 (hang (text "Trans coercion mis-match:" <+> ppr co)
1441 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
1442 ; lintRole co r1 r2
1443 ; return (k1a, k2b, ty1a, ty2b, r1) }
1444
1445 lintCoercion the_co@(NthCo n co)
1446 = do { (_, _, s, t, r) <- lintCoercion co
1447 ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
1448 { (Just (tv_s, _ty_s), Just (tv_t, _ty_t))
1449 | n == 0
1450 -> return (ks, kt, ts, tt, Nominal)
1451 where
1452 ts = tyVarKind tv_s
1453 tt = tyVarKind tv_t
1454 ks = typeKind ts
1455 kt = typeKind tt
1456
1457 ; _ -> case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
1458 { (Just (tc_s, tys_s), Just (tc_t, tys_t))
1459 | tc_s == tc_t
1460 , isInjectiveTyCon tc_s r
1461 -- see Note [NthCo and newtypes] in TyCoRep
1462 , tys_s `equalLength` tys_t
1463 , n < length tys_s
1464 -> return (ks, kt, ts, tt, tr)
1465 where
1466 ts = getNth tys_s n
1467 tt = getNth tys_t n
1468 tr = nthRole r tc_s n
1469 ks = typeKind ts
1470 kt = typeKind tt
1471
1472 ; _ -> failWithL (hang (text "Bad getNth:")
1473 2 (ppr the_co $$ ppr s $$ ppr t)) }}}
1474
1475 lintCoercion the_co@(LRCo lr co)
1476 = do { (_,_,s,t,r) <- lintCoercion co
1477 ; lintRole co Nominal r
1478 ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
1479 (Just s_pr, Just t_pr)
1480 -> return (ks_pick, kt_pick, s_pick, t_pick, Nominal)
1481 where
1482 s_pick = pickLR lr s_pr
1483 t_pick = pickLR lr t_pr
1484 ks_pick = typeKind s_pick
1485 kt_pick = typeKind t_pick
1486
1487 _ -> failWithL (hang (text "Bad LRCo:")
1488 2 (ppr the_co $$ ppr s $$ ppr t)) }
1489
1490 lintCoercion (InstCo co arg)
1491 = do { (k3, k4, t1',t2', r) <- lintCoercion co
1492 ; (k1',k2',s1,s2, r') <- lintCoercion arg
1493 ; lintRole arg Nominal r'
1494 ; case (splitForAllTy_maybe t1', splitForAllTy_maybe t2') of
1495 (Just (tv1,t1), Just (tv2,t2))
1496 | k1' `eqType` tyVarKind tv1
1497 , k2' `eqType` tyVarKind tv2
1498 -> return (k3, k4,
1499 substTyWith [tv1] [s1] t1,
1500 substTyWith [tv2] [s2] t2, r)
1501 | otherwise
1502 -> failWithL (text "Kind mis-match in inst coercion")
1503 _ -> failWithL (text "Bad argument of inst") }
1504
1505 lintCoercion co@(AxiomInstCo con ind cos)
1506 = do { unless (0 <= ind && ind < numBranches (coAxiomBranches con))
1507 (bad_ax (text "index out of range"))
1508 ; let CoAxBranch { cab_tvs = ktvs
1509 , cab_cvs = cvs
1510 , cab_roles = roles
1511 , cab_lhs = lhs
1512 , cab_rhs = rhs } = coAxiomNthBranch con ind
1513 ; unless (length ktvs + length cvs == length cos) $
1514 bad_ax (text "lengths")
1515 ; subst <- getTCvSubst
1516 ; let empty_subst = zapTCvSubst subst
1517 ; (subst_l, subst_r) <- foldlM check_ki
1518 (empty_subst, empty_subst)
1519 (zip3 (ktvs ++ cvs) roles cos)
1520 ; let lhs' = substTys subst_l lhs
1521 rhs' = substTy subst_r rhs
1522 ; case checkAxInstCo co of
1523 Just bad_branch -> bad_ax $ text "inconsistent with" <+>
1524 pprCoAxBranch con bad_branch
1525 Nothing -> return ()
1526 ; let s2 = mkTyConApp (coAxiomTyCon con) lhs'
1527 ; return (typeKind s2, typeKind rhs', s2, rhs', coAxiomRole con) }
1528 where
1529 bad_ax what = addErrL (hang (text "Bad axiom application" <+> parens what)
1530 2 (ppr co))
1531
1532 check_ki (subst_l, subst_r) (ktv, role, arg)
1533 = do { (k', k'', s', t', r) <- lintCoercion arg
1534 ; lintRole arg role r
1535 ; let ktv_kind_l = substTy subst_l (tyVarKind ktv)
1536 ktv_kind_r = substTy subst_r (tyVarKind ktv)
1537 ; unless (k' `eqType` ktv_kind_l)
1538 (bad_ax (text "check_ki1" <+> vcat [ ppr co, ppr k', ppr ktv, ppr ktv_kind_l ] ))
1539 ; unless (k'' `eqType` ktv_kind_r)
1540 (bad_ax (text "check_ki2" <+> vcat [ ppr co, ppr k'', ppr ktv, ppr ktv_kind_r ] ))
1541 ; return (extendTCvSubst subst_l ktv s',
1542 extendTCvSubst subst_r ktv t') }
1543
1544 lintCoercion (CoherenceCo co1 co2)
1545 = do { (_, k2, t1, t2, r) <- lintCoercion co1
1546 ; let lhsty = mkCastTy t1 co2
1547 ; k1' <- lintType lhsty
1548 ; return (k1', k2, lhsty, t2, r) }
1549
1550 lintCoercion (KindCo co)
1551 = do { (k1, k2, _, _, _) <- lintCoercion co
1552 ; return (liftedTypeKind, liftedTypeKind, k1, k2, Nominal) }
1553
1554 lintCoercion (SubCo co')
1555 = do { (k1,k2,s,t,r) <- lintCoercion co'
1556 ; lintRole co' Nominal r
1557 ; return (k1,k2,s,t,Representational) }
1558
1559 lintCoercion this@(AxiomRuleCo co cs)
1560 = do { eqs <- mapM lintCoercion cs
1561 ; lintRoles 0 (coaxrAsmpRoles co) eqs
1562 ; case coaxrProves co [ Pair l r | (_,_,l,r,_) <- eqs ] of
1563 Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
1564 Just (Pair l r) ->
1565 return (typeKind l, typeKind r, l, r, coaxrRole co) }
1566 where
1567 err m xs = failWithL $
1568 hang (text m) 2 $ vcat (text "Rule:" <+> ppr (coaxrName co) : xs)
1569
1570 lintRoles n (e : es) ((_,_,_,_,r) : rs)
1571 | e == r = lintRoles (n+1) es rs
1572 | otherwise = err "Argument roles mismatch"
1573 [ text "In argument:" <+> int (n+1)
1574 , text "Expected:" <+> ppr e
1575 , text "Found:" <+> ppr r ]
1576 lintRoles _ [] [] = return ()
1577 lintRoles n [] rs = err "Too many coercion arguments"
1578 [ text "Expected:" <+> int n
1579 , text "Provided:" <+> int (n + length rs) ]
1580
1581 lintRoles n es [] = err "Not enough coercion arguments"
1582 [ text "Expected:" <+> int (n + length es)
1583 , text "Provided:" <+> int n ]
1584
1585 ----------
1586 lintUnliftedCoVar :: CoVar -> LintM ()
1587 lintUnliftedCoVar cv
1588 = when (not (isUnliftedType (coVarKind cv))) $
1589 failWithL (text "Bad lifted equality:" <+> ppr cv
1590 <+> dcolon <+> ppr (coVarKind cv))
1591
1592 {-
1593 ************************************************************************
1594 * *
1595 \subsection[lint-monad]{The Lint monad}
1596 * *
1597 ************************************************************************
1598 -}
1599
1600 -- If you edit this type, you may need to update the GHC formalism
1601 -- See Note [GHC Formalism]
1602 data LintEnv
1603 = LE { le_flags :: LintFlags -- Linting the result of this pass
1604 , le_loc :: [LintLocInfo] -- Locations
1605 , le_subst :: TCvSubst -- Current type substitution; we also use this
1606 -- to keep track of all the variables in scope,
1607 -- both Ids and TyVars
1608 , le_dynflags :: DynFlags -- DynamicFlags
1609 }
1610
1611 data LintFlags
1612 = LF { lf_check_global_ids :: Bool -- See Note [Checking for global Ids]
1613 , lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers]
1614 , lf_check_static_ptrs :: Bool -- See Note [Checking StaticPtrs]
1615 }
1616
1617 defaultLintFlags :: LintFlags
1618 defaultLintFlags = LF { lf_check_global_ids = False
1619 , lf_check_inline_loop_breakers = True
1620 , lf_check_static_ptrs = False
1621 }
1622
1623 newtype LintM a =
1624 LintM { unLintM ::
1625 LintEnv ->
1626 WarnsAndErrs -> -- Error and warning messages so far
1627 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
1628
1629 type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)
1630
1631 {- Note [Checking for global Ids]
1632 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1633 Before CoreTidy, all locally-bound Ids must be LocalIds, even
1634 top-level ones. See Note [Exported LocalIds] and Trac #9857.
1635
1636 Note [Checking StaticPtrs]
1637 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1638 See SimplCore Note [Grand plan for static forms] for an overview.
1639
1640 Every occurrence of the data constructor @StaticPtr@ should be moved
1641 to the top level by the FloatOut pass. It's vital that we don't have
1642 nested StaticPtr uses after CorePrep, because we populate the Static
1643 Pointer Table from the top-level bindings. See SimplCore Note [Grand
1644 plan for static forms].
1645
1646 The linter checks that no occurrence is left behind, nested within an
1647 expression. The check is enabled only:
1648
1649 * After the FloatOut, CorePrep, and CoreTidy passes.
1650 We could check more often, but the condition doesn't hold until
1651 after the first FloatOut pass.
1652
1653 * When the module uses the StaticPointers language extension. This is
1654 a little hack. This optimization arose from the need to compile
1655 GHC.StaticPtr, which otherwise would be rejected because of the
1656 following binding for the StaticPtr data constructor itself:
1657
1658 StaticPtr = \a b1 b2 b3 b4 -> StaticPtr a b1 b2 b3 b4
1659
1660 which contains an application of `StaticPtr` nested within the
1661 lambda abstractions. This binding is injected by CorePrep.
1662
1663 Note that GHC.StaticPtr is itself compiled without -XStaticPointers.
1664
1665 Note [Type substitution]
1666 ~~~~~~~~~~~~~~~~~~~~~~~~
1667 Why do we need a type substitution? Consider
1668 /\(a:*). \(x:a). /\(a:*). id a x
1669 This is ill typed, because (renaming variables) it is really
1670 /\(a:*). \(x:a). /\(b:*). id b x
1671 Hence, when checking an application, we can't naively compare x's type
1672 (at its binding site) with its expected type (at a use site). So we
1673 rename type binders as we go, maintaining a substitution.
1674
1675 The same substitution also supports let-type, current expressed as
1676 (/\(a:*). body) ty
1677 Here we substitute 'ty' for 'a' in 'body', on the fly.
1678 -}
1679
1680 instance Functor LintM where
1681 fmap = liftM
1682
1683 instance Applicative LintM where
1684 pure x = LintM $ \ _ errs -> (Just x, errs)
1685 (<*>) = ap
1686
1687 instance Monad LintM where
1688 fail err = failWithL (text err)
1689 m >>= k = LintM (\ env errs ->
1690 let (res, errs') = unLintM m env errs in
1691 case res of
1692 Just r -> unLintM (k r) env errs'
1693 Nothing -> (Nothing, errs'))
1694
1695 #if __GLASGOW_HASKELL__ > 710
1696 instance MonadFail.MonadFail LintM where
1697 fail err = failWithL (text err)
1698 #endif
1699
1700 instance HasDynFlags LintM where
1701 getDynFlags = LintM (\ e errs -> (Just (le_dynflags e), errs))
1702
1703 data LintLocInfo
1704 = RhsOf Id -- The variable bound
1705 | LambdaBodyOf Id -- The lambda-binder
1706 | BodyOfLetRec [Id] -- One of the binders
1707 | CaseAlt CoreAlt -- Case alternative
1708 | CasePat CoreAlt -- The *pattern* of the case alternative
1709 | AnExpr CoreExpr -- Some expression
1710 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
1711 | TopLevelBindings
1712 | InType Type -- Inside a type
1713 | InCo Coercion -- Inside a coercion
1714
1715 initL :: DynFlags -> LintFlags -> LintM a -> WarnsAndErrs -- Errors and warnings
1716 initL dflags flags m
1717 = case unLintM m env (emptyBag, emptyBag) of
1718 (_, errs) -> errs
1719 where
1720 env = LE { le_flags = flags, le_subst = emptyTCvSubst, le_loc = [], le_dynflags = dflags }
1721
1722 getLintFlags :: LintM LintFlags
1723 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
1724
1725 checkL :: Bool -> MsgDoc -> LintM ()
1726 checkL True _ = return ()
1727 checkL False msg = failWithL msg
1728
1729 -- like checkL, but relevant to type checking
1730 lintL :: Bool -> MsgDoc -> LintM ()
1731 lintL = checkL
1732
1733 checkWarnL :: Bool -> MsgDoc -> LintM ()
1734 checkWarnL True _ = return ()
1735 checkWarnL False msg = addWarnL msg
1736
1737 failWithL :: MsgDoc -> LintM a
1738 failWithL msg = LintM $ \ env (warns,errs) ->
1739 (Nothing, (warns, addMsg env errs msg))
1740
1741 addErrL :: MsgDoc -> LintM ()
1742 addErrL msg = LintM $ \ env (warns,errs) ->
1743 (Just (), (warns, addMsg env errs msg))
1744
1745 addWarnL :: MsgDoc -> LintM ()
1746 addWarnL msg = LintM $ \ env (warns,errs) ->
1747 (Just (), (addMsg env warns msg, errs))
1748
1749 addMsg :: LintEnv -> Bag MsgDoc -> MsgDoc -> Bag MsgDoc
1750 addMsg env msgs msg
1751 = ASSERT( notNull locs )
1752 msgs `snocBag` mk_msg msg
1753 where
1754 locs = le_loc env
1755 (loc, cxt1) = dumpLoc (head locs)
1756 cxts = [snd (dumpLoc loc) | loc <- locs]
1757 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
1758 text "Substitution:" <+> ppr (le_subst env)
1759 | otherwise = cxt1
1760
1761 mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
1762
1763 addLoc :: LintLocInfo -> LintM a -> LintM a
1764 addLoc extra_loc m
1765 = LintM $ \ env errs ->
1766 unLintM m (env { le_loc = extra_loc : le_loc env }) errs
1767
1768 inCasePat :: LintM Bool -- A slight hack; see the unique call site
1769 inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
1770 where
1771 is_case_pat (LE { le_loc = CasePat {} : _ }) = True
1772 is_case_pat _other = False
1773
1774 addInScopeVars :: [Var] -> LintM a -> LintM a
1775 addInScopeVars vars m
1776 = LintM $ \ env errs ->
1777 unLintM m (env { le_subst = extendTCvInScopeList (le_subst env) vars })
1778 errs
1779
1780 addInScopeVarSet :: VarSet -> LintM a -> LintM a
1781 addInScopeVarSet vars m
1782 = LintM $ \ env errs ->
1783 unLintM m (env { le_subst = extendTCvInScopeSet (le_subst env) vars })
1784 errs
1785
1786 addInScopeVar :: Var -> LintM a -> LintM a
1787 addInScopeVar var m
1788 = LintM $ \ env errs ->
1789 unLintM m (env { le_subst = extendTCvInScope (le_subst env) var }) errs
1790
1791 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
1792 extendSubstL tv ty m
1793 = LintM $ \ env errs ->
1794 unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
1795
1796 updateTCvSubst :: TCvSubst -> LintM a -> LintM a
1797 updateTCvSubst subst' m
1798 = LintM $ \ env errs -> unLintM m (env { le_subst = subst' }) errs
1799
1800 getTCvSubst :: LintM TCvSubst
1801 getTCvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
1802
1803 getInScope :: LintM InScopeSet
1804 getInScope = LintM (\ env errs -> (Just (getTCvInScope $ le_subst env), errs))
1805
1806 applySubstTy :: InType -> LintM OutType
1807 applySubstTy ty = do { subst <- getTCvSubst; return (substTy subst ty) }
1808
1809 applySubstCo :: InCoercion -> LintM OutCoercion
1810 applySubstCo co = do { subst <- getTCvSubst; return (substCo subst co) }
1811
1812 lookupIdInScope :: Id -> LintM Id
1813 lookupIdInScope id
1814 | not (mustHaveLocalBinding id)
1815 = return id -- An imported Id
1816 | otherwise
1817 = do { subst <- getTCvSubst
1818 ; case lookupInScope (getTCvInScope subst) id of
1819 Just v -> return v
1820 Nothing -> do { addErrL out_of_scope
1821 ; return id } }
1822 where
1823 out_of_scope = pprBndr LetBind id <+> text "is out of scope"
1824
1825 lintTyCoVarInScope :: Var -> LintM ()
1826 lintTyCoVarInScope v = lintInScope (text "is out of scope") v
1827
1828 lintInScope :: SDoc -> Var -> LintM ()
1829 lintInScope loc_msg var =
1830 do { subst <- getTCvSubst
1831 ; lintL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
1832 (hsep [pprBndr LetBind var, loc_msg]) }
1833
1834 ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
1835 -- check ty2 is subtype of ty1 (ie, has same structure but usage
1836 -- annotations need only be consistent, not equal)
1837 -- Assumes ty1,ty2 are have alrady had the substitution applied
1838 ensureEqTys ty1 ty2 msg = lintL (ty1 `eqType` ty2) msg
1839
1840 lintRole :: Outputable thing
1841 => thing -- where the role appeared
1842 -> Role -- expected
1843 -> Role -- actual
1844 -> LintM ()
1845 lintRole co r1 r2
1846 = lintL (r1 == r2)
1847 (text "Role incompatibility: expected" <+> ppr r1 <> comma <+>
1848 text "got" <+> ppr r2 $$
1849 text "in" <+> ppr co)
1850
1851 {-
1852 ************************************************************************
1853 * *
1854 \subsection{Error messages}
1855 * *
1856 ************************************************************************
1857 -}
1858
1859 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
1860
1861 dumpLoc (RhsOf v)
1862 = (getSrcLoc v, brackets (text "RHS of" <+> pp_binders [v]))
1863
1864 dumpLoc (LambdaBodyOf b)
1865 = (getSrcLoc b, brackets (text "in body of lambda with binder" <+> pp_binder b))
1866
1867 dumpLoc (BodyOfLetRec [])
1868 = (noSrcLoc, brackets (text "In body of a letrec with no binders"))
1869
1870 dumpLoc (BodyOfLetRec bs@(_:_))
1871 = ( getSrcLoc (head bs), brackets (text "in body of letrec with binders" <+> pp_binders bs))
1872
1873 dumpLoc (AnExpr e)
1874 = (noSrcLoc, text "In the expression:" <+> ppr e)
1875
1876 dumpLoc (CaseAlt (con, args, _))
1877 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1878
1879 dumpLoc (CasePat (con, args, _))
1880 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1881
1882 dumpLoc (ImportedUnfolding locn)
1883 = (locn, brackets (text "in an imported unfolding"))
1884 dumpLoc TopLevelBindings
1885 = (noSrcLoc, Outputable.empty)
1886 dumpLoc (InType ty)
1887 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1888 dumpLoc (InCo co)
1889 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
1890
1891 pp_binders :: [Var] -> SDoc
1892 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1893
1894 pp_binder :: Var -> SDoc
1895 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1896 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1897
1898 ------------------------------------------------------
1899 -- Messages for case expressions
1900
1901 mkDefaultArgsMsg :: [Var] -> MsgDoc
1902 mkDefaultArgsMsg args
1903 = hang (text "DEFAULT case with binders")
1904 4 (ppr args)
1905
1906 mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
1907 mkCaseAltMsg e ty1 ty2
1908 = hang (text "Type of case alternatives not the same as the annotation on case:")
1909 4 (vcat [ text "Actual type:" <+> ppr ty1,
1910 text "Annotation on case:" <+> ppr ty2,
1911 text "Alt Rhs:" <+> ppr e ])
1912
1913 mkScrutMsg :: Id -> Type -> Type -> TCvSubst -> MsgDoc
1914 mkScrutMsg var var_ty scrut_ty subst
1915 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1916 text "Result binder type:" <+> ppr var_ty,--(idType var),
1917 text "Scrutinee type:" <+> ppr scrut_ty,
1918 hsep [text "Current TCv subst", ppr subst]]
1919
1920 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
1921 mkNonDefltMsg e
1922 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1923 mkNonIncreasingAltsMsg e
1924 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1925
1926 nonExhaustiveAltsMsg :: CoreExpr -> MsgDoc
1927 nonExhaustiveAltsMsg e
1928 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1929
1930 mkBadConMsg :: TyCon -> DataCon -> MsgDoc
1931 mkBadConMsg tycon datacon
1932 = vcat [
1933 text "In a case alternative, data constructor isn't in scrutinee type:",
1934 text "Scrutinee type constructor:" <+> ppr tycon,
1935 text "Data con:" <+> ppr datacon
1936 ]
1937
1938 mkBadPatMsg :: Type -> Type -> MsgDoc
1939 mkBadPatMsg con_result_ty scrut_ty
1940 = vcat [
1941 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1942 text "Pattern result type:" <+> ppr con_result_ty,
1943 text "Scrutinee type:" <+> ppr scrut_ty
1944 ]
1945
1946 integerScrutinisedMsg :: MsgDoc
1947 integerScrutinisedMsg
1948 = text "In a LitAlt, the literal is lifted (probably Integer)"
1949
1950 mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
1951 mkBadAltMsg scrut_ty alt
1952 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1953 text "Scrutinee type:" <+> ppr scrut_ty,
1954 text "Alternative:" <+> pprCoreAlt alt ]
1955
1956 mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc
1957 mkNewTyDataConAltMsg scrut_ty alt
1958 = vcat [ text "Data alternative for newtype datacon",
1959 text "Scrutinee type:" <+> ppr scrut_ty,
1960 text "Alternative:" <+> pprCoreAlt alt ]
1961
1962
1963 ------------------------------------------------------
1964 -- Other error messages
1965
1966 mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1967 mkAppMsg fun_ty arg_ty arg
1968 = vcat [text "Argument value doesn't match argument type:",
1969 hang (text "Fun type:") 4 (ppr fun_ty),
1970 hang (text "Arg type:") 4 (ppr arg_ty),
1971 hang (text "Arg:") 4 (ppr arg)]
1972
1973 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1974 mkNonFunAppMsg fun_ty arg_ty arg
1975 = vcat [text "Non-function type in function position",
1976 hang (text "Fun type:") 4 (ppr fun_ty),
1977 hang (text "Arg type:") 4 (ppr arg_ty),
1978 hang (text "Arg:") 4 (ppr arg)]
1979
1980 mkLetErr :: TyVar -> CoreExpr -> MsgDoc
1981 mkLetErr bndr rhs
1982 = vcat [text "Bad `let' binding:",
1983 hang (text "Variable:")
1984 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
1985 hang (text "Rhs:")
1986 4 (ppr rhs)]
1987
1988 mkTyAppMsg :: Type -> Type -> MsgDoc
1989 mkTyAppMsg ty arg_ty
1990 = vcat [text "Illegal type application:",
1991 hang (text "Exp type:")
1992 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1993 hang (text "Arg type:")
1994 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1995
1996 mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc
1997 mkRhsMsg binder what ty
1998 = vcat
1999 [hsep [text "The type of this binder doesn't match the type of its" <+> what <> colon,
2000 ppr binder],
2001 hsep [text "Binder's type:", ppr (idType binder)],
2002 hsep [text "Rhs type:", ppr ty]]
2003
2004 mkLetAppMsg :: CoreExpr -> MsgDoc
2005 mkLetAppMsg e
2006 = hang (text "This argument does not satisfy the let/app invariant:")
2007 2 (ppr e)
2008
2009 mkRhsPrimMsg :: Id -> CoreExpr -> MsgDoc
2010 mkRhsPrimMsg binder _rhs
2011 = vcat [hsep [text "The type of this binder is primitive:",
2012 ppr binder],
2013 hsep [text "Binder's type:", ppr (idType binder)]
2014 ]
2015
2016 mkStrictMsg :: Id -> MsgDoc
2017 mkStrictMsg binder
2018 = vcat [hsep [text "Recursive or top-level binder has strict demand info:",
2019 ppr binder],
2020 hsep [text "Binder's demand info:", ppr (idDemandInfo binder)]
2021 ]
2022
2023 mkNonTopExportedMsg :: Id -> MsgDoc
2024 mkNonTopExportedMsg binder
2025 = hsep [text "Non-top-level binder is marked as exported:", ppr binder]
2026
2027 mkNonTopExternalNameMsg :: Id -> MsgDoc
2028 mkNonTopExternalNameMsg binder
2029 = hsep [text "Non-top-level binder has an external name:", ppr binder]
2030
2031 mkKindErrMsg :: TyVar -> Type -> MsgDoc
2032 mkKindErrMsg tyvar arg_ty
2033 = vcat [text "Kinds don't match in type application:",
2034 hang (text "Type variable:")
2035 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
2036 hang (text "Arg type:")
2037 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
2038
2039 {- Not needed now
2040 mkArityMsg :: Id -> MsgDoc
2041 mkArityMsg binder
2042 = vcat [hsep [text "Demand type has",
2043 ppr (dmdTypeDepth dmd_ty),
2044 text "arguments, rhs has",
2045 ppr (idArity binder),
2046 text "arguments,",
2047 ppr binder],
2048 hsep [text "Binder's strictness signature:", ppr dmd_ty]
2049
2050 ]
2051 where (StrictSig dmd_ty) = idStrictness binder
2052 -}
2053 mkCastErr :: Outputable casted => casted -> Coercion -> Type -> Type -> MsgDoc
2054 mkCastErr expr co from_ty expr_ty
2055 = vcat [text "From-type of Cast differs from type of enclosed expression",
2056 text "From-type:" <+> ppr from_ty,
2057 text "Type of enclosed expr:" <+> ppr expr_ty,
2058 text "Actual enclosed expr:" <+> ppr expr,
2059 text "Coercion used in cast:" <+> ppr co
2060 ]
2061
2062 mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc
2063 mkBadUnivCoMsg lr co
2064 = text "Kind mismatch on the" <+> pprLeftOrRight lr <+>
2065 text "side of a UnivCo:" <+> ppr co
2066
2067 mkBadProofIrrelMsg :: Type -> Coercion -> SDoc
2068 mkBadProofIrrelMsg ty co
2069 = hang (text "Found a non-coercion in a proof-irrelevance UnivCo:")
2070 2 (vcat [ text "type:" <+> ppr ty
2071 , text "co:" <+> ppr co ])
2072
2073 mkBadTyVarMsg :: Var -> SDoc
2074 mkBadTyVarMsg tv
2075 = text "Non-tyvar used in TyVarTy:"
2076 <+> ppr tv <+> dcolon <+> ppr (varType tv)
2077
2078 pprLeftOrRight :: LeftOrRight -> MsgDoc
2079 pprLeftOrRight CLeft = text "left"
2080 pprLeftOrRight CRight = text "right"
2081
2082 dupVars :: [[Var]] -> MsgDoc
2083 dupVars vars
2084 = hang (text "Duplicate variables brought into scope")
2085 2 (ppr vars)
2086
2087 dupExtVars :: [[Name]] -> MsgDoc
2088 dupExtVars vars
2089 = hang (text "Duplicate top-level variables with the same qualified name")
2090 2 (ppr vars)
2091
2092 {-
2093 ************************************************************************
2094 * *
2095 \subsection{Annotation Linting}
2096 * *
2097 ************************************************************************
2098 -}
2099
2100 -- | This checks whether a pass correctly looks through debug
2101 -- annotations (@SourceNote@). This works a bit different from other
2102 -- consistency checks: We check this by running the given task twice,
2103 -- noting all differences between the results.
2104 lintAnnots :: SDoc -> (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
2105 lintAnnots pname pass guts = do
2106 -- Run the pass as we normally would
2107 dflags <- getDynFlags
2108 when (gopt Opt_DoAnnotationLinting dflags) $
2109 liftIO $ Err.showPass dflags "Annotation linting - first run"
2110 nguts <- pass guts
2111 -- If appropriate re-run it without debug annotations to make sure
2112 -- that they made no difference.
2113 when (gopt Opt_DoAnnotationLinting dflags) $ do
2114 liftIO $ Err.showPass dflags "Annotation linting - second run"
2115 nguts' <- withoutAnnots pass guts
2116 -- Finally compare the resulting bindings
2117 liftIO $ Err.showPass dflags "Annotation linting - comparison"
2118 let binds = flattenBinds $ mg_binds nguts
2119 binds' = flattenBinds $ mg_binds nguts'
2120 (diffs,_) = diffBinds True (mkRnEnv2 emptyInScopeSet) binds binds'
2121 when (not (null diffs)) $ CoreMonad.putMsg $ vcat
2122 [ lint_banner "warning" pname
2123 , text "Core changes with annotations:"
2124 , withPprStyle defaultDumpStyle $ nest 2 $ vcat diffs
2125 ]
2126 -- Return actual new guts
2127 return nguts
2128
2129 -- | Run the given pass without annotations. This means that we both
2130 -- set the debugLevel setting to 0 in the environment as well as all
2131 -- annotations from incoming modules.
2132 withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
2133 withoutAnnots pass guts = do
2134 -- Remove debug flag from environment.
2135 dflags <- getDynFlags
2136 let removeFlag env = env{ hsc_dflags = dflags{ debugLevel = 0} }
2137 withoutFlag corem =
2138 liftIO =<< runCoreM <$> fmap removeFlag getHscEnv <*> getRuleBase <*>
2139 getUniqueSupplyM <*> getModule <*>
2140 getVisibleOrphanMods <*>
2141 getPrintUnqualified <*> getSrcSpanM <*>
2142 pure corem
2143 -- Nuke existing ticks in module.
2144 -- TODO: Ticks in unfoldings. Maybe change unfolding so it removes
2145 -- them in absence of debugLevel > 0.
2146 let nukeTicks = stripTicksE (not . tickishIsCode)
2147 nukeAnnotsBind :: CoreBind -> CoreBind
2148 nukeAnnotsBind bind = case bind of
2149 Rec bs -> Rec $ map (\(b,e) -> (b, nukeTicks e)) bs
2150 NonRec b e -> NonRec b $ nukeTicks e
2151 nukeAnnotsMod mg@ModGuts{mg_binds=binds}
2152 = mg{mg_binds = map nukeAnnotsBind binds}
2153 -- Perform pass with all changes applied
2154 fmap fst $ withoutFlag $ pass (nukeAnnotsMod guts)