Use the in_scope set in lint_app
[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 = do { in_scope <- getInScope
1140 -- We need the in_scope set to satisfy the invariant in
1141 -- Note [The substitution invariant] in TyCoRep
1142 ; foldlM (go_app in_scope) kfn kas }
1143 where
1144 fail_msg = vcat [ hang (text "Kind application error in") 2 doc
1145 , nest 2 (text "Function kind =" <+> ppr kfn)
1146 , nest 2 (text "Arg kinds =" <+> ppr kas) ]
1147
1148 go_app in_scope kfn ka
1149 | Just kfn' <- coreView kfn
1150 = go_app in_scope kfn' ka
1151
1152 go_app _ (ForAllTy (Anon kfa) kfb) (_,ka)
1153 = do { unless (ka `eqType` kfa) (addErrL fail_msg)
1154 ; return kfb }
1155
1156 go_app in_scope (ForAllTy (Named kv _vis) kfn) (ta,ka)
1157 = do { unless (ka `eqType` tyVarKind kv) (addErrL fail_msg)
1158 ; return (substTyWithInScope in_scope [kv] [ta] kfn) }
1159
1160 go_app _ _ _ = failWithL fail_msg
1161
1162 {- *********************************************************************
1163 * *
1164 Linting rules
1165 * *
1166 ********************************************************************* -}
1167
1168 lintCoreRule :: OutType -> CoreRule -> LintM ()
1169 lintCoreRule _ (BuiltinRule {})
1170 = return () -- Don't bother
1171
1172 lintCoreRule fun_ty (Rule { ru_name = name, ru_bndrs = bndrs
1173 , ru_args = args, ru_rhs = rhs })
1174 = lintBinders bndrs $ \ _ ->
1175 do { lhs_ty <- foldM lintCoreArg fun_ty args
1176 ; rhs_ty <- lintCoreExpr rhs
1177 ; ensureEqTys lhs_ty rhs_ty $
1178 (rule_doc <+> vcat [ text "lhs type:" <+> ppr lhs_ty
1179 , text "rhs type:" <+> ppr rhs_ty ])
1180 ; let bad_bndrs = filterOut (`elemVarSet` exprsFreeVars args) bndrs
1181 ; checkL (null bad_bndrs)
1182 (rule_doc <+> text "unbound" <+> ppr bad_bndrs)
1183 -- See Note [Linting rules]
1184 }
1185 where
1186 rule_doc = text "Rule" <+> doubleQuotes (ftext name) <> colon
1187
1188 {- Note [Linting rules]
1189 ~~~~~~~~~~~~~~~~~~~~~~~
1190 It's very bad if simplifying a rule means that one of the template
1191 variables (ru_bndrs) becomes not-mentioned in the template argumments
1192 (ru_args). How can that happen? Well, in Trac #10602, SpecConstr
1193 stupidly constructed a rule like
1194
1195 forall x,c1,c2.
1196 f (x |> c1 |> c2) = ....
1197
1198 But simplExpr collapses those coercions into one. (Indeed in
1199 Trac #10602, it collapsed to the identity and was removed altogether.)
1200
1201 We don't have a great story for what to do here, but at least
1202 this check will nail it.
1203 -}
1204
1205 {-
1206 ************************************************************************
1207 * *
1208 Linting coercions
1209 * *
1210 ************************************************************************
1211 -}
1212
1213 lintInCo :: InCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
1214 -- Check the coercion, and apply the substitution to it
1215 -- See Note [Linting type lets]
1216 lintInCo co
1217 = addLoc (InCo co) $
1218 do { co' <- applySubstCo co
1219 ; lintCoercion co' }
1220
1221 -- lints a coercion, confirming that its lh kind and its rh kind are both *
1222 -- also ensures that the role is Nominal
1223 lintStarCoercion :: OutCoercion -> LintM (LintedType, LintedType)
1224 lintStarCoercion g
1225 = do { (k1, k2, t1, t2, r) <- lintCoercion g
1226 ; lintStar (text "the kind of the left type in" <+> ppr g) k1
1227 ; lintStar (text "the kind of the right type in" <+> ppr g) k2
1228 ; lintRole g Nominal r
1229 ; return (t1, t2) }
1230
1231 lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
1232 -- Check the kind of a coercion term, returning the kind
1233 -- Post-condition: the returned OutTypes are lint-free
1234
1235 -- If you edit this function, you may need to update the GHC formalism
1236 -- See Note [GHC Formalism]
1237 lintCoercion (Refl r ty)
1238 = do { k <- lintType ty
1239 ; return (k, k, ty, ty, r) }
1240
1241 lintCoercion co@(TyConAppCo r tc cos)
1242 | tc `hasKey` funTyConKey
1243 , [co1,co2] <- cos
1244 = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
1245 ; (k2,k'2,s2,t2,r2) <- lintCoercion co2
1246 ; k <- lintArrow (text "coercion" <+> quotes (ppr co)) k1 k2
1247 ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2
1248 ; lintRole co1 r r1
1249 ; lintRole co2 r r2
1250 ; return (k, k', mkFunTy s1 s2, mkFunTy t1 t2, r) }
1251
1252 | Just {} <- synTyConDefn_maybe tc
1253 = failWithL (text "Synonym in TyConAppCo:" <+> ppr co)
1254
1255 | otherwise
1256 = do { checkTyCon tc
1257 ; (k's, ks, ss, ts, rs) <- mapAndUnzip5M lintCoercion cos
1258 ; k' <- lint_co_app co (tyConKind tc) (ss `zip` k's)
1259 ; k <- lint_co_app co (tyConKind tc) (ts `zip` ks)
1260 ; _ <- zipWith3M lintRole cos (tyConRolesX r tc) rs
1261 ; return (k', k, mkTyConApp tc ss, mkTyConApp tc ts, r) }
1262
1263 lintCoercion co@(AppCo co1 co2)
1264 | TyConAppCo {} <- co1
1265 = failWithL (text "TyConAppCo to the left of AppCo:" <+> ppr co)
1266 | Refl _ (TyConApp {}) <- co1
1267 = failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co)
1268 | otherwise
1269 = do { (k1,k2,s1,s2,r1) <- lintCoercion co1
1270 ; (k'1, k'2, t1, t2, r2) <- lintCoercion co2
1271 ; k3 <- lint_co_app co k1 [(t1,k'1)]
1272 ; k4 <- lint_co_app co k2 [(t2,k'2)]
1273 ; if r1 == Phantom
1274 then lintL (r2 == Phantom || r2 == Nominal)
1275 (text "Second argument in AppCo cannot be R:" $$
1276 ppr co)
1277 else lintRole co Nominal r2
1278 ; return (k3, k4, mkAppTy s1 t1, mkAppTy s2 t2, r1) }
1279
1280 ----------
1281 lintCoercion (ForAllCo tv1 kind_co co)
1282 = do { (_, k2) <- lintStarCoercion kind_co
1283 ; let tv2 = setTyVarKind tv1 k2
1284 ; (k3, k4, t1, t2, r) <- addInScopeVar tv1 $ lintCoercion co
1285 ; let tyl = mkNamedForAllTy tv1 Invisible t1
1286 tyr = mkNamedForAllTy tv2 Invisible $
1287 substTyWith [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo kind_co] t2
1288 ; return (k3, k4, tyl, tyr, r) }
1289
1290 lintCoercion (CoVarCo cv)
1291 | not (isCoVar cv)
1292 = failWithL (hang (text "Bad CoVarCo:" <+> ppr cv)
1293 2 (text "With offending type:" <+> ppr (varType cv)))
1294 | otherwise
1295 = do { lintTyCoVarInScope cv
1296 ; cv' <- lookupIdInScope cv
1297 ; lintUnliftedCoVar cv
1298 ; return $ coVarKindsTypesRole cv' }
1299
1300 -- See Note [Bad unsafe coercion]
1301 lintCoercion co@(UnivCo prov r ty1 ty2)
1302 = do { k1 <- lintType ty1
1303 ; k2 <- lintType ty2
1304 ; case prov of
1305 UnsafeCoerceProv -> return () -- no extra checks
1306
1307 PhantomProv kco -> do { lintRole co Phantom r
1308 ; check_kinds kco k1 k2 }
1309
1310 ProofIrrelProv kco -> do { lintL (isCoercionTy ty1) $
1311 mkBadProofIrrelMsg ty1 co
1312 ; lintL (isCoercionTy ty2) $
1313 mkBadProofIrrelMsg ty2 co
1314 ; check_kinds kco k1 k2 }
1315
1316 PluginProv _ -> return () -- no extra checks
1317 HoleProv h -> addErrL $
1318 text "Unfilled coercion hole:" <+> ppr h
1319
1320 ; when (r /= Phantom && classifiesTypeWithValues k1
1321 && classifiesTypeWithValues k2)
1322 (checkTypes ty1 ty2)
1323 ; return (k1, k2, ty1, ty2, r) }
1324 where
1325 report s = hang (text $ "Unsafe coercion between " ++ s)
1326 2 (vcat [ text "From:" <+> ppr ty1
1327 , text " To:" <+> ppr ty2])
1328 isUnBoxed :: PrimRep -> Bool
1329 isUnBoxed PtrRep = False
1330 isUnBoxed _ = True
1331 checkTypes t1 t2
1332 = case (repType t1, repType t2) of
1333 (UnaryRep _, UnaryRep _) ->
1334 validateCoercion (typePrimRep t1)
1335 (typePrimRep t2)
1336 (UbxTupleRep rep1, UbxTupleRep rep2) -> do
1337 checkWarnL (length rep1 == length rep2)
1338 (report "unboxed tuples of different length")
1339 zipWithM_ checkTypes rep1 rep2
1340 _ -> addWarnL (report "unboxed tuple and ordinary type")
1341 validateCoercion :: PrimRep -> PrimRep -> LintM ()
1342 validateCoercion rep1 rep2
1343 = do { dflags <- getDynFlags
1344 ; checkWarnL (isUnBoxed rep1 == isUnBoxed rep2)
1345 (report "unboxed and boxed value")
1346 ; checkWarnL (TyCon.primRepSizeW dflags rep1
1347 == TyCon.primRepSizeW dflags rep2)
1348 (report "unboxed values of different size")
1349 ; let fl = liftM2 (==) (TyCon.primRepIsFloat rep1)
1350 (TyCon.primRepIsFloat rep2)
1351 ; case fl of
1352 Nothing -> addWarnL (report "vector types")
1353 Just False -> addWarnL (report "float and integral values")
1354 _ -> return ()
1355 }
1356
1357 check_kinds kco k1 k2 = do { (k1', k2') <- lintStarCoercion kco
1358 ; ensureEqTys k1 k1' (mkBadUnivCoMsg CLeft co)
1359 ; ensureEqTys k2 k2' (mkBadUnivCoMsg CRight co) }
1360
1361
1362 lintCoercion (SymCo co)
1363 = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
1364 ; return (k2, k1, ty2, ty1, r) }
1365
1366 lintCoercion co@(TransCo co1 co2)
1367 = do { (k1a, _k1b, ty1a, ty1b, r1) <- lintCoercion co1
1368 ; (_k2a, k2b, ty2a, ty2b, r2) <- lintCoercion co2
1369 ; ensureEqTys ty1b ty2a
1370 (hang (text "Trans coercion mis-match:" <+> ppr co)
1371 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
1372 ; lintRole co r1 r2
1373 ; return (k1a, k2b, ty1a, ty2b, r1) }
1374
1375 lintCoercion the_co@(NthCo n co)
1376 = do { (_, _, s, t, r) <- lintCoercion co
1377 ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
1378 { (Just (tv_s, _ty_s), Just (tv_t, _ty_t))
1379 | n == 0
1380 -> return (ks, kt, ts, tt, Nominal)
1381 where
1382 ts = tyVarKind tv_s
1383 tt = tyVarKind tv_t
1384 ks = typeKind ts
1385 kt = typeKind tt
1386
1387 ; _ -> case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
1388 { (Just (tc_s, tys_s), Just (tc_t, tys_t))
1389 | tc_s == tc_t
1390 , isInjectiveTyCon tc_s r
1391 -- see Note [NthCo and newtypes] in TyCoRep
1392 , tys_s `equalLength` tys_t
1393 , n < length tys_s
1394 -> return (ks, kt, ts, tt, tr)
1395 where
1396 ts = getNth tys_s n
1397 tt = getNth tys_t n
1398 tr = nthRole r tc_s n
1399 ks = typeKind ts
1400 kt = typeKind tt
1401
1402 ; _ -> failWithL (hang (text "Bad getNth:")
1403 2 (ppr the_co $$ ppr s $$ ppr t)) }}}
1404
1405 lintCoercion the_co@(LRCo lr co)
1406 = do { (_,_,s,t,r) <- lintCoercion co
1407 ; lintRole co Nominal r
1408 ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
1409 (Just s_pr, Just t_pr)
1410 -> return (ks_pick, kt_pick, s_pick, t_pick, Nominal)
1411 where
1412 s_pick = pickLR lr s_pr
1413 t_pick = pickLR lr t_pr
1414 ks_pick = typeKind s_pick
1415 kt_pick = typeKind t_pick
1416
1417 _ -> failWithL (hang (text "Bad LRCo:")
1418 2 (ppr the_co $$ ppr s $$ ppr t)) }
1419
1420 lintCoercion (InstCo co arg)
1421 = do { (k3, k4, t1',t2', r) <- lintCoercion co
1422 ; (k1',k2',s1,s2, r') <- lintCoercion arg
1423 ; lintRole arg Nominal r'
1424 ; case (splitForAllTy_maybe t1', splitForAllTy_maybe t2') of
1425 (Just (tv1,t1), Just (tv2,t2))
1426 | k1' `eqType` tyVarKind tv1
1427 , k2' `eqType` tyVarKind tv2
1428 -> return (k3, k4,
1429 substTyWith [tv1] [s1] t1,
1430 substTyWith [tv2] [s2] t2, r)
1431 | otherwise
1432 -> failWithL (text "Kind mis-match in inst coercion")
1433 _ -> failWithL (text "Bad argument of inst") }
1434
1435 lintCoercion co@(AxiomInstCo con ind cos)
1436 = do { unless (0 <= ind && ind < numBranches (coAxiomBranches con))
1437 (bad_ax (text "index out of range"))
1438 ; let CoAxBranch { cab_tvs = ktvs
1439 , cab_cvs = cvs
1440 , cab_roles = roles
1441 , cab_lhs = lhs
1442 , cab_rhs = rhs } = coAxiomNthBranch con ind
1443 ; unless (length ktvs + length cvs == length cos) $
1444 bad_ax (text "lengths")
1445 ; subst <- getTCvSubst
1446 ; let empty_subst = zapTCvSubst subst
1447 ; (subst_l, subst_r) <- foldlM check_ki
1448 (empty_subst, empty_subst)
1449 (zip3 (ktvs ++ cvs) roles cos)
1450 ; let lhs' = substTys subst_l lhs
1451 rhs' = substTy subst_r rhs
1452 ; case checkAxInstCo co of
1453 Just bad_branch -> bad_ax $ text "inconsistent with" <+>
1454 pprCoAxBranch con bad_branch
1455 Nothing -> return ()
1456 ; let s2 = mkTyConApp (coAxiomTyCon con) lhs'
1457 ; return (typeKind s2, typeKind rhs', s2, rhs', coAxiomRole con) }
1458 where
1459 bad_ax what = addErrL (hang (text "Bad axiom application" <+> parens what)
1460 2 (ppr co))
1461
1462 check_ki (subst_l, subst_r) (ktv, role, arg)
1463 = do { (k', k'', s', t', r) <- lintCoercion arg
1464 ; lintRole arg role r
1465 ; let ktv_kind_l = substTy subst_l (tyVarKind ktv)
1466 ktv_kind_r = substTy subst_r (tyVarKind ktv)
1467 ; unless (k' `eqType` ktv_kind_l)
1468 (bad_ax (text "check_ki1" <+> vcat [ ppr co, ppr k', ppr ktv, ppr ktv_kind_l ] ))
1469 ; unless (k'' `eqType` ktv_kind_r)
1470 (bad_ax (text "check_ki2" <+> vcat [ ppr co, ppr k'', ppr ktv, ppr ktv_kind_r ] ))
1471 ; return (extendTCvSubst subst_l ktv s',
1472 extendTCvSubst subst_r ktv t') }
1473
1474 lintCoercion (CoherenceCo co1 co2)
1475 = do { (_, k2, t1, t2, r) <- lintCoercion co1
1476 ; let lhsty = mkCastTy t1 co2
1477 ; k1' <- lintType lhsty
1478 ; return (k1', k2, lhsty, t2, r) }
1479
1480 lintCoercion (KindCo co)
1481 = do { (k1, k2, _, _, _) <- lintCoercion co
1482 ; return (liftedTypeKind, liftedTypeKind, k1, k2, Nominal) }
1483
1484 lintCoercion (SubCo co')
1485 = do { (k1,k2,s,t,r) <- lintCoercion co'
1486 ; lintRole co' Nominal r
1487 ; return (k1,k2,s,t,Representational) }
1488
1489 lintCoercion this@(AxiomRuleCo co cs)
1490 = do { eqs <- mapM lintCoercion cs
1491 ; lintRoles 0 (coaxrAsmpRoles co) eqs
1492 ; case coaxrProves co [ Pair l r | (_,_,l,r,_) <- eqs ] of
1493 Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
1494 Just (Pair l r) ->
1495 return (typeKind l, typeKind r, l, r, coaxrRole co) }
1496 where
1497 err m xs = failWithL $
1498 hang (text m) 2 $ vcat (text "Rule:" <+> ppr (coaxrName co) : xs)
1499
1500 lintRoles n (e : es) ((_,_,_,_,r) : rs)
1501 | e == r = lintRoles (n+1) es rs
1502 | otherwise = err "Argument roles mismatch"
1503 [ text "In argument:" <+> int (n+1)
1504 , text "Expected:" <+> ppr e
1505 , text "Found:" <+> ppr r ]
1506 lintRoles _ [] [] = return ()
1507 lintRoles n [] rs = err "Too many coercion arguments"
1508 [ text "Expected:" <+> int n
1509 , text "Provided:" <+> int (n + length rs) ]
1510
1511 lintRoles n es [] = err "Not enough coercion arguments"
1512 [ text "Expected:" <+> int (n + length es)
1513 , text "Provided:" <+> int n ]
1514
1515 ----------
1516 lintUnliftedCoVar :: CoVar -> LintM ()
1517 lintUnliftedCoVar cv
1518 = when (not (isUnliftedType (coVarKind cv))) $
1519 failWithL (text "Bad lifted equality:" <+> ppr cv
1520 <+> dcolon <+> ppr (coVarKind cv))
1521
1522 {-
1523 ************************************************************************
1524 * *
1525 \subsection[lint-monad]{The Lint monad}
1526 * *
1527 ************************************************************************
1528 -}
1529
1530 -- If you edit this type, you may need to update the GHC formalism
1531 -- See Note [GHC Formalism]
1532 data LintEnv
1533 = LE { le_flags :: LintFlags -- Linting the result of this pass
1534 , le_loc :: [LintLocInfo] -- Locations
1535 , le_subst :: TCvSubst -- Current type substitution; we also use this
1536 -- to keep track of all the variables in scope,
1537 -- both Ids and TyVars
1538 , le_dynflags :: DynFlags -- DynamicFlags
1539 }
1540
1541 data LintFlags
1542 = LF { lf_check_global_ids :: Bool -- See Note [Checking for global Ids]
1543 , lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers]
1544 }
1545
1546 defaultLintFlags :: LintFlags
1547 defaultLintFlags = LF { lf_check_global_ids = False
1548 , lf_check_inline_loop_breakers = True }
1549
1550 newtype LintM a =
1551 LintM { unLintM ::
1552 LintEnv ->
1553 WarnsAndErrs -> -- Error and warning messages so far
1554 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
1555
1556 type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)
1557
1558 {- Note [Checking for global Ids]
1559 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1560 Before CoreTidy, all locally-bound Ids must be LocalIds, even
1561 top-level ones. See Note [Exported LocalIds] and Trac #9857.
1562
1563 Note [Type substitution]
1564 ~~~~~~~~~~~~~~~~~~~~~~~~
1565 Why do we need a type substitution? Consider
1566 /\(a:*). \(x:a). /\(a:*). id a x
1567 This is ill typed, because (renaming variables) it is really
1568 /\(a:*). \(x:a). /\(b:*). id b x
1569 Hence, when checking an application, we can't naively compare x's type
1570 (at its binding site) with its expected type (at a use site). So we
1571 rename type binders as we go, maintaining a substitution.
1572
1573 The same substitution also supports let-type, current expressed as
1574 (/\(a:*). body) ty
1575 Here we substitute 'ty' for 'a' in 'body', on the fly.
1576 -}
1577
1578 instance Functor LintM where
1579 fmap = liftM
1580
1581 instance Applicative LintM where
1582 pure x = LintM $ \ _ errs -> (Just x, errs)
1583 (<*>) = ap
1584
1585 instance Monad LintM where
1586 fail err = failWithL (text err)
1587 m >>= k = LintM (\ env errs ->
1588 let (res, errs') = unLintM m env errs in
1589 case res of
1590 Just r -> unLintM (k r) env errs'
1591 Nothing -> (Nothing, errs'))
1592
1593 #if __GLASGOW_HASKELL__ > 710
1594 instance MonadFail.MonadFail LintM where
1595 fail err = failWithL (text err)
1596 #endif
1597
1598 instance HasDynFlags LintM where
1599 getDynFlags = LintM (\ e errs -> (Just (le_dynflags e), errs))
1600
1601 data LintLocInfo
1602 = RhsOf Id -- The variable bound
1603 | LambdaBodyOf Id -- The lambda-binder
1604 | BodyOfLetRec [Id] -- One of the binders
1605 | CaseAlt CoreAlt -- Case alternative
1606 | CasePat CoreAlt -- The *pattern* of the case alternative
1607 | AnExpr CoreExpr -- Some expression
1608 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
1609 | TopLevelBindings
1610 | InType Type -- Inside a type
1611 | InCo Coercion -- Inside a coercion
1612
1613 initL :: DynFlags -> LintFlags -> LintM a -> WarnsAndErrs -- Errors and warnings
1614 initL dflags flags m
1615 = case unLintM m env (emptyBag, emptyBag) of
1616 (_, errs) -> errs
1617 where
1618 env = LE { le_flags = flags, le_subst = emptyTCvSubst, le_loc = [], le_dynflags = dflags }
1619
1620 getLintFlags :: LintM LintFlags
1621 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
1622
1623 checkL :: Bool -> MsgDoc -> LintM ()
1624 checkL True _ = return ()
1625 checkL False msg = failWithL msg
1626
1627 -- like checkL, but relevant to type checking
1628 lintL :: Bool -> MsgDoc -> LintM ()
1629 lintL = checkL
1630
1631 checkWarnL :: Bool -> MsgDoc -> LintM ()
1632 checkWarnL True _ = return ()
1633 checkWarnL False msg = addWarnL msg
1634
1635 failWithL :: MsgDoc -> LintM a
1636 failWithL msg = LintM $ \ env (warns,errs) ->
1637 (Nothing, (warns, addMsg env errs msg))
1638
1639 addErrL :: MsgDoc -> LintM ()
1640 addErrL msg = LintM $ \ env (warns,errs) ->
1641 (Just (), (warns, addMsg env errs msg))
1642
1643 addWarnL :: MsgDoc -> LintM ()
1644 addWarnL msg = LintM $ \ env (warns,errs) ->
1645 (Just (), (addMsg env warns msg, errs))
1646
1647 addMsg :: LintEnv -> Bag MsgDoc -> MsgDoc -> Bag MsgDoc
1648 addMsg env msgs msg
1649 = ASSERT( notNull locs )
1650 msgs `snocBag` mk_msg msg
1651 where
1652 locs = le_loc env
1653 (loc, cxt1) = dumpLoc (head locs)
1654 cxts = [snd (dumpLoc loc) | loc <- locs]
1655 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
1656 text "Substitution:" <+> ppr (le_subst env)
1657 | otherwise = cxt1
1658
1659 mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
1660
1661 addLoc :: LintLocInfo -> LintM a -> LintM a
1662 addLoc extra_loc m
1663 = LintM $ \ env errs ->
1664 unLintM m (env { le_loc = extra_loc : le_loc env }) errs
1665
1666 inCasePat :: LintM Bool -- A slight hack; see the unique call site
1667 inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
1668 where
1669 is_case_pat (LE { le_loc = CasePat {} : _ }) = True
1670 is_case_pat _other = False
1671
1672 addInScopeVars :: [Var] -> LintM a -> LintM a
1673 addInScopeVars vars m
1674 = LintM $ \ env errs ->
1675 unLintM m (env { le_subst = extendTCvInScopeList (le_subst env) vars })
1676 errs
1677
1678 addInScopeVar :: Var -> LintM a -> LintM a
1679 addInScopeVar var m
1680 = LintM $ \ env errs ->
1681 unLintM m (env { le_subst = extendTCvInScope (le_subst env) var }) errs
1682
1683 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
1684 extendSubstL tv ty m
1685 = LintM $ \ env errs ->
1686 unLintM m (env { le_subst = Type.extendTCvSubst (le_subst env) tv ty }) errs
1687
1688 updateTCvSubst :: TCvSubst -> LintM a -> LintM a
1689 updateTCvSubst subst' m
1690 = LintM $ \ env errs -> unLintM m (env { le_subst = subst' }) errs
1691
1692 getTCvSubst :: LintM TCvSubst
1693 getTCvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
1694
1695 getInScope :: LintM InScopeSet
1696 getInScope = LintM (\ env errs -> (Just (getTCvInScope $ le_subst env), errs))
1697
1698 applySubstTy :: InType -> LintM OutType
1699 applySubstTy ty = do { subst <- getTCvSubst; return (substTy subst ty) }
1700
1701 applySubstCo :: InCoercion -> LintM OutCoercion
1702 applySubstCo co = do { subst <- getTCvSubst; return (substCo subst co) }
1703
1704 lookupIdInScope :: Id -> LintM Id
1705 lookupIdInScope id
1706 | not (mustHaveLocalBinding id)
1707 = return id -- An imported Id
1708 | otherwise
1709 = do { subst <- getTCvSubst
1710 ; case lookupInScope (getTCvInScope subst) id of
1711 Just v -> return v
1712 Nothing -> do { addErrL out_of_scope
1713 ; return id } }
1714 where
1715 out_of_scope = pprBndr LetBind id <+> text "is out of scope"
1716
1717
1718 oneTupleDataConId :: Id -- Should not happen
1719 oneTupleDataConId = dataConWorkId (tupleDataCon Boxed 1)
1720
1721 lintTyCoVarInScope :: Var -> LintM ()
1722 lintTyCoVarInScope v = lintInScope (text "is out of scope") v
1723
1724 lintInScope :: SDoc -> Var -> LintM ()
1725 lintInScope loc_msg var =
1726 do { subst <- getTCvSubst
1727 ; lintL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
1728 (hsep [pprBndr LetBind var, loc_msg]) }
1729
1730 ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
1731 -- check ty2 is subtype of ty1 (ie, has same structure but usage
1732 -- annotations need only be consistent, not equal)
1733 -- Assumes ty1,ty2 are have alrady had the substitution applied
1734 ensureEqTys ty1 ty2 msg = lintL (ty1 `eqType` ty2) msg
1735
1736 lintRole :: Outputable thing
1737 => thing -- where the role appeared
1738 -> Role -- expected
1739 -> Role -- actual
1740 -> LintM ()
1741 lintRole co r1 r2
1742 = lintL (r1 == r2)
1743 (text "Role incompatibility: expected" <+> ppr r1 <> comma <+>
1744 text "got" <+> ppr r2 $$
1745 text "in" <+> ppr co)
1746
1747 {-
1748 ************************************************************************
1749 * *
1750 \subsection{Error messages}
1751 * *
1752 ************************************************************************
1753 -}
1754
1755 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
1756
1757 dumpLoc (RhsOf v)
1758 = (getSrcLoc v, brackets (text "RHS of" <+> pp_binders [v]))
1759
1760 dumpLoc (LambdaBodyOf b)
1761 = (getSrcLoc b, brackets (text "in body of lambda with binder" <+> pp_binder b))
1762
1763 dumpLoc (BodyOfLetRec [])
1764 = (noSrcLoc, brackets (text "In body of a letrec with no binders"))
1765
1766 dumpLoc (BodyOfLetRec bs@(_:_))
1767 = ( getSrcLoc (head bs), brackets (text "in body of letrec with binders" <+> pp_binders bs))
1768
1769 dumpLoc (AnExpr e)
1770 = (noSrcLoc, text "In the expression:" <+> ppr e)
1771
1772 dumpLoc (CaseAlt (con, args, _))
1773 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1774
1775 dumpLoc (CasePat (con, args, _))
1776 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1777
1778 dumpLoc (ImportedUnfolding locn)
1779 = (locn, brackets (text "in an imported unfolding"))
1780 dumpLoc TopLevelBindings
1781 = (noSrcLoc, Outputable.empty)
1782 dumpLoc (InType ty)
1783 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1784 dumpLoc (InCo co)
1785 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
1786
1787 pp_binders :: [Var] -> SDoc
1788 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1789
1790 pp_binder :: Var -> SDoc
1791 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1792 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1793
1794 ------------------------------------------------------
1795 -- Messages for case expressions
1796
1797 mkDefaultArgsMsg :: [Var] -> MsgDoc
1798 mkDefaultArgsMsg args
1799 = hang (text "DEFAULT case with binders")
1800 4 (ppr args)
1801
1802 mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
1803 mkCaseAltMsg e ty1 ty2
1804 = hang (text "Type of case alternatives not the same as the annotation on case:")
1805 4 (vcat [ppr ty1, ppr ty2, ppr e])
1806
1807 mkScrutMsg :: Id -> Type -> Type -> TCvSubst -> MsgDoc
1808 mkScrutMsg var var_ty scrut_ty subst
1809 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1810 text "Result binder type:" <+> ppr var_ty,--(idType var),
1811 text "Scrutinee type:" <+> ppr scrut_ty,
1812 hsep [text "Current TCv subst", ppr subst]]
1813
1814 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
1815 mkNonDefltMsg e
1816 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1817 mkNonIncreasingAltsMsg e
1818 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1819
1820 nonExhaustiveAltsMsg :: CoreExpr -> MsgDoc
1821 nonExhaustiveAltsMsg e
1822 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1823
1824 mkBadConMsg :: TyCon -> DataCon -> MsgDoc
1825 mkBadConMsg tycon datacon
1826 = vcat [
1827 text "In a case alternative, data constructor isn't in scrutinee type:",
1828 text "Scrutinee type constructor:" <+> ppr tycon,
1829 text "Data con:" <+> ppr datacon
1830 ]
1831
1832 mkBadPatMsg :: Type -> Type -> MsgDoc
1833 mkBadPatMsg con_result_ty scrut_ty
1834 = vcat [
1835 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1836 text "Pattern result type:" <+> ppr con_result_ty,
1837 text "Scrutinee type:" <+> ppr scrut_ty
1838 ]
1839
1840 integerScrutinisedMsg :: MsgDoc
1841 integerScrutinisedMsg
1842 = text "In a LitAlt, the literal is lifted (probably Integer)"
1843
1844 mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
1845 mkBadAltMsg scrut_ty alt
1846 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1847 text "Scrutinee type:" <+> ppr scrut_ty,
1848 text "Alternative:" <+> pprCoreAlt alt ]
1849
1850 mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc
1851 mkNewTyDataConAltMsg scrut_ty alt
1852 = vcat [ text "Data alternative for newtype datacon",
1853 text "Scrutinee type:" <+> ppr scrut_ty,
1854 text "Alternative:" <+> pprCoreAlt alt ]
1855
1856
1857 ------------------------------------------------------
1858 -- Other error messages
1859
1860 mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1861 mkAppMsg fun_ty arg_ty arg
1862 = vcat [text "Argument value doesn't match argument type:",
1863 hang (text "Fun type:") 4 (ppr fun_ty),
1864 hang (text "Arg type:") 4 (ppr arg_ty),
1865 hang (text "Arg:") 4 (ppr arg)]
1866
1867 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
1868 mkNonFunAppMsg fun_ty arg_ty arg
1869 = vcat [text "Non-function type in function position",
1870 hang (text "Fun type:") 4 (ppr fun_ty),
1871 hang (text "Arg type:") 4 (ppr arg_ty),
1872 hang (text "Arg:") 4 (ppr arg)]
1873
1874 mkLetErr :: TyVar -> CoreExpr -> MsgDoc
1875 mkLetErr bndr rhs
1876 = vcat [text "Bad `let' binding:",
1877 hang (text "Variable:")
1878 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
1879 hang (text "Rhs:")
1880 4 (ppr rhs)]
1881
1882 mkTyAppMsg :: Type -> Type -> MsgDoc
1883 mkTyAppMsg ty arg_ty
1884 = vcat [text "Illegal type application:",
1885 hang (text "Exp type:")
1886 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1887 hang (text "Arg type:")
1888 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1889
1890 mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc
1891 mkRhsMsg binder what ty
1892 = vcat
1893 [hsep [text "The type of this binder doesn't match the type of its" <+> what <> colon,
1894 ppr binder],
1895 hsep [text "Binder's type:", ppr (idType binder)],
1896 hsep [text "Rhs type:", ppr ty]]
1897
1898 mkLetAppMsg :: CoreExpr -> MsgDoc
1899 mkLetAppMsg e
1900 = hang (text "This argument does not satisfy the let/app invariant:")
1901 2 (ppr e)
1902
1903 mkRhsPrimMsg :: Id -> CoreExpr -> MsgDoc
1904 mkRhsPrimMsg binder _rhs
1905 = vcat [hsep [text "The type of this binder is primitive:",
1906 ppr binder],
1907 hsep [text "Binder's type:", ppr (idType binder)]
1908 ]
1909
1910 mkStrictMsg :: Id -> MsgDoc
1911 mkStrictMsg binder
1912 = vcat [hsep [text "Recursive or top-level binder has strict demand info:",
1913 ppr binder],
1914 hsep [text "Binder's demand info:", ppr (idDemandInfo binder)]
1915 ]
1916
1917 mkNonTopExportedMsg :: Id -> MsgDoc
1918 mkNonTopExportedMsg binder
1919 = hsep [text "Non-top-level binder is marked as exported:", ppr binder]
1920
1921 mkNonTopExternalNameMsg :: Id -> MsgDoc
1922 mkNonTopExternalNameMsg binder
1923 = hsep [text "Non-top-level binder has an external name:", ppr binder]
1924
1925 mkKindErrMsg :: TyVar -> Type -> MsgDoc
1926 mkKindErrMsg tyvar arg_ty
1927 = vcat [text "Kinds don't match in type application:",
1928 hang (text "Type variable:")
1929 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1930 hang (text "Arg type:")
1931 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1932
1933 {- Not needed now
1934 mkArityMsg :: Id -> MsgDoc
1935 mkArityMsg binder
1936 = vcat [hsep [text "Demand type has",
1937 ppr (dmdTypeDepth dmd_ty),
1938 text "arguments, rhs has",
1939 ppr (idArity binder),
1940 text "arguments,",
1941 ppr binder],
1942 hsep [text "Binder's strictness signature:", ppr dmd_ty]
1943
1944 ]
1945 where (StrictSig dmd_ty) = idStrictness binder
1946 -}
1947 mkCastErr :: Outputable casted => casted -> Coercion -> Type -> Type -> MsgDoc
1948 mkCastErr expr co from_ty expr_ty
1949 = vcat [text "From-type of Cast differs from type of enclosed expression",
1950 text "From-type:" <+> ppr from_ty,
1951 text "Type of enclosed expr:" <+> ppr expr_ty,
1952 text "Actual enclosed expr:" <+> ppr expr,
1953 text "Coercion used in cast:" <+> ppr co
1954 ]
1955
1956 mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc
1957 mkBadUnivCoMsg lr co
1958 = text "Kind mismatch on the" <+> pprLeftOrRight lr <+>
1959 text "side of a UnivCo:" <+> ppr co
1960
1961 mkBadProofIrrelMsg :: Type -> Coercion -> SDoc
1962 mkBadProofIrrelMsg ty co
1963 = hang (text "Found a non-coercion in a proof-irrelevance UnivCo:")
1964 2 (vcat [ text "type:" <+> ppr ty
1965 , text "co:" <+> ppr co ])
1966
1967 mkBadTyVarMsg :: Var -> SDoc
1968 mkBadTyVarMsg tv
1969 = text "Non-tyvar used in TyVarTy:"
1970 <+> ppr tv <+> dcolon <+> ppr (varType tv)
1971
1972 pprLeftOrRight :: LeftOrRight -> MsgDoc
1973 pprLeftOrRight CLeft = text "left"
1974 pprLeftOrRight CRight = text "right"
1975
1976 dupVars :: [[Var]] -> MsgDoc
1977 dupVars vars
1978 = hang (text "Duplicate variables brought into scope")
1979 2 (ppr vars)
1980
1981 dupExtVars :: [[Name]] -> MsgDoc
1982 dupExtVars vars
1983 = hang (text "Duplicate top-level variables with the same qualified name")
1984 2 (ppr vars)
1985
1986 {-
1987 ************************************************************************
1988 * *
1989 \subsection{Annotation Linting}
1990 * *
1991 ************************************************************************
1992 -}
1993
1994 -- | This checks whether a pass correctly looks through debug
1995 -- annotations (@SourceNote@). This works a bit different from other
1996 -- consistency checks: We check this by running the given task twice,
1997 -- noting all differences between the results.
1998 lintAnnots :: SDoc -> (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
1999 lintAnnots pname pass guts = do
2000 -- Run the pass as we normally would
2001 dflags <- getDynFlags
2002 when (gopt Opt_DoAnnotationLinting dflags) $
2003 liftIO $ Err.showPass dflags "Annotation linting - first run"
2004 nguts <- pass guts
2005 -- If appropriate re-run it without debug annotations to make sure
2006 -- that they made no difference.
2007 when (gopt Opt_DoAnnotationLinting dflags) $ do
2008 liftIO $ Err.showPass dflags "Annotation linting - second run"
2009 nguts' <- withoutAnnots pass guts
2010 -- Finally compare the resulting bindings
2011 liftIO $ Err.showPass dflags "Annotation linting - comparison"
2012 let binds = flattenBinds $ mg_binds nguts
2013 binds' = flattenBinds $ mg_binds nguts'
2014 (diffs,_) = diffBinds True (mkRnEnv2 emptyInScopeSet) binds binds'
2015 when (not (null diffs)) $ CoreMonad.putMsg $ vcat
2016 [ lint_banner "warning" pname
2017 , text "Core changes with annotations:"
2018 , withPprStyle defaultDumpStyle $ nest 2 $ vcat diffs
2019 ]
2020 -- Return actual new guts
2021 return nguts
2022
2023 -- | Run the given pass without annotations. This means that we both
2024 -- set the debugLevel setting to 0 in the environment as well as all
2025 -- annotations from incoming modules.
2026 withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
2027 withoutAnnots pass guts = do
2028 -- Remove debug flag from environment.
2029 dflags <- getDynFlags
2030 let removeFlag env = env{ hsc_dflags = dflags{ debugLevel = 0} }
2031 withoutFlag corem =
2032 liftIO =<< runCoreM <$> fmap removeFlag getHscEnv <*> getRuleBase <*>
2033 getUniqueSupplyM <*> getModule <*>
2034 getVisibleOrphanMods <*>
2035 getPrintUnqualified <*> getSrcSpanM <*>
2036 pure corem
2037 -- Nuke existing ticks in module.
2038 -- TODO: Ticks in unfoldings. Maybe change unfolding so it removes
2039 -- them in absence of debugLevel > 0.
2040 let nukeTicks = stripTicksE (not . tickishIsCode)
2041 nukeAnnotsBind :: CoreBind -> CoreBind
2042 nukeAnnotsBind bind = case bind of
2043 Rec bs -> Rec $ map (\(b,e) -> (b, nukeTicks e)) bs
2044 NonRec b e -> NonRec b $ nukeTicks e
2045 nukeAnnotsMod mg@ModGuts{mg_binds=binds}
2046 = mg{mg_binds = map nukeAnnotsBind binds}
2047 -- Perform pass with all changes applied
2048 fmap fst $ withoutFlag $ pass (nukeAnnotsMod guts)