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