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