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