1{- 2(c) The University of Glasgow 2006 3(c) The GRASP/AQUA Project, Glasgow University, 1993-1998 4 5 6A ``lint'' pass to check for Core correctness. 7See Note [Core Lint guarantee]. 8-} 9 10{-# LANGUAGE CPP #-} 11{-# LANGUAGE DeriveFunctor #-} 12 13module CoreLint ( 14 lintCoreBindings, lintUnfolding, 15 lintPassResult, lintInteractiveExpr, lintExpr, 16 lintAnnots, lintTypes, 17 18 -- ** Debug output 19 endPass, endPassIO, 20 dumpPassResult, 21 CoreLint.dumpIfSet, 22 ) where 23 24#include "HsVersions.h" 25 26import GhcPrelude 27 28import CoreSyn 29import CoreFVs 30import CoreUtils 31import CoreStats ( coreBindsStats ) 32import CoreMonad 33import Bag 34import Literal 35import DataCon 36import TysWiredIn 37import TysPrim 38import TcType ( isFloatingTy ) 39import Var 40import VarEnv 41import VarSet 42import Name 43import Id 44import IdInfo 45import PprCore 46import ErrUtils 47import Coercion 48import SrcLoc 49import Type 50import RepType 51import TyCoRep -- checks validity of types/coercions 52import TyCoSubst 53import TyCoFVs 54import TyCoPpr ( pprTyVar ) 55import TyCon 56import CoAxiom 57import BasicTypes 58import ErrUtils as Err 59import ListSetOps 60import PrelNames 61import Outputable 62import FastString 63import Util 64import InstEnv ( instanceDFunId ) 65import OptCoercion ( checkAxInstCo ) 66import CoreArity ( typeArity ) 67import Demand ( splitStrictSig, isBotRes ) 68 69import HscTypes 70import DynFlags 71import Control.Monad 72import qualified Control.Monad.Fail as MonadFail 73import MonadUtils 74import Data.Foldable ( toList ) 75import Data.List.NonEmpty ( NonEmpty ) 76import Data.Maybe 77import Pair 78import qualified GHC.LanguageExtensions as LangExt 79 80{- 81Note [Core Lint guarantee] 82~~~~~~~~~~~~~~~~~~~~~~~~~~ 83Core Lint is the type-checker for Core. Using it, we get the following guarantee: 84 85If all of: 861. Core Lint passes, 872. there are no unsafe coercions (i.e. UnsafeCoerceProv), 883. all plugin-supplied coercions (i.e. PluginProv) are valid, and 894. all case-matches are complete 90then running the compiled program will not seg-fault, assuming no bugs downstream 91(e.g. in the code generator). This guarantee is quite powerful, in that it allows us 92to decouple the safety of the resulting program from the type inference algorithm. 93 94However, do note point (4) above. Core Lint does not check for incomplete case-matches; 95see Note [Case expression invariants] in CoreSyn, invariant (4). As explained there, 96an incomplete case-match might slip by Core Lint and cause trouble at runtime. 97 98Note [GHC Formalism] 99~~~~~~~~~~~~~~~~~~~~ 100This file implements the type-checking algorithm for System FC, the "official" 101name of the Core language. Type safety of FC is heart of the claim that 102executables produced by GHC do not have segmentation faults. Thus, it is 103useful to be able to reason about System FC independently of reading the code. 104To this purpose, there is a document core-spec.pdf built in docs/core-spec that 105contains a formalism of the types and functions dealt with here. If you change 106just about anything in this file or you change other types/functions throughout 107the Core language (all signposted to this note), you should update that 108formalism. See docs/core-spec/README for more info about how to do so. 109 110Note [check vs lint] 111~~~~~~~~~~~~~~~~~~~~ 112This file implements both a type checking algorithm and also general sanity 113checking. For example, the "sanity checking" checks for TyConApp on the left 114of an AppTy, which should never happen. These sanity checks don't really 115affect any notion of type soundness. Yet, it is convenient to do the sanity 116checks at the same time as the type checks. So, we use the following naming 117convention: 118 119- Functions that begin with 'lint'... are involved in type checking. These 120 functions might also do some sanity checking. 121 122- Functions that begin with 'check'... are *not* involved in type checking. 123 They exist only for sanity checking. 124 125Issues surrounding variable naming, shadowing, and such are considered *not* 126to be part of type checking, as the formalism omits these details. 127 128Summary of checks 129~~~~~~~~~~~~~~~~~ 130Checks that a set of core bindings is well-formed. The PprStyle and String 131just control what we print in the event of an error. The Bool value 132indicates whether we have done any specialisation yet (in which case we do 133some extra checks). 134 135We check for 136 (a) type errors 137 (b) Out-of-scope type variables 138 (c) Out-of-scope local variables 139 (d) Ill-kinded types 140 (e) Incorrect unsafe coercions 141 142If we have done specialisation the we check that there are 143 (a) No top-level bindings of primitive (unboxed type) 144 145Outstanding issues: 146 147 -- Things are *not* OK if: 148 -- 149 -- * Unsaturated type app before specialisation has been done; 150 -- 151 -- * Oversaturated type app after specialisation (eta reduction 152 -- may well be happening...); 153 154 155Note [Linting function types] 156~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 157As described in Note [Representation of function types], all saturated 158applications of funTyCon are represented with the FunTy constructor. We check 159this invariant in lintType. 160 161Note [Linting type lets] 162~~~~~~~~~~~~~~~~~~~~~~~~ 163In the desugarer, it's very very convenient to be able to say (in effect) 164 let a = Type Int in <body> 165That is, use a type let. See Note [Type let] in CoreSyn. 166 167However, when linting <body> we need to remember that a=Int, else we might 168reject a correct program. So we carry a type substitution (in this example 169[a -> Int]) and apply this substitution before comparing types. The functin 170 lintInTy :: Type -> LintM (Type, Kind) 171returns a substituted type. 172 173When we encounter a binder (like x::a) we must apply the substitution 174to the type of the binding variable. lintBinders does this. 175 176For Ids, the type-substituted Id is added to the in_scope set (which 177itself is part of the TCvSubst we are carrying down), and when we 178find an occurrence of an Id, we fetch it from the in-scope set. 179 180Note [Bad unsafe coercion] 181~~~~~~~~~~~~~~~~~~~~~~~~~~ 182For discussion see https://gitlab.haskell.org/ghc/ghc/wikis/bad-unsafe-coercions 183Linter introduces additional rules that checks improper coercion between 184different types, called bad coercions. Following coercions are forbidden: 185 186 (a) coercions between boxed and unboxed values; 187 (b) coercions between unlifted values of the different sizes, here 188 active size is checked, i.e. size of the actual value but not 189 the space allocated for value; 190 (c) coercions between floating and integral boxed values, this check 191 is not yet supported for unboxed tuples, as no semantics were 192 specified for that; 193 (d) coercions from / to vector type 194 (e) If types are unboxed tuples then tuple (# A_1,..,A_n #) can be 195 coerced to (# B_1,..,B_m #) if n=m and for each pair A_i, B_i rules 196 (a-e) holds. 197 198Note [Join points] 199~~~~~~~~~~~~~~~~~~ 200We check the rules listed in Note [Invariants on join points] in CoreSyn. The 201only one that causes any difficulty is the first: All occurrences must be tail 202calls. To this end, along with the in-scope set, we remember in le_joins the 203subset of in-scope Ids that are valid join ids. For example: 204 205 join j x = ... in 206 case e of 207 A -> jump j y -- good 208 B -> case (jump j z) of -- BAD 209 C -> join h = jump j w in ... -- good 210 D -> let x = jump j v in ... -- BAD 211 212A join point remains valid in case branches, so when checking the A 213branch, j is still valid. When we check the scrutinee of the inner 214case, however, we set le_joins to empty, and catch the 215error. Similarly, join points can occur free in RHSes of other join 216points but not the RHSes of value bindings (thunks and functions). 217 218************************************************************************ 219* * 220 Beginning and ending passes 221* * 222************************************************************************ 223 224These functions are not CoreM monad stuff, but they probably ought to 225be, and it makes a convenient place for them. They print out stuff 226before and after core passes, and do Core Lint when necessary. 227-} 228 229endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> CoreM () 230endPass pass binds rules 231 = do { hsc_env <- getHscEnv 232 ; print_unqual <- getPrintUnqualified 233 ; liftIO $ endPassIO hsc_env print_unqual pass binds rules } 234 235endPassIO :: HscEnv -> PrintUnqualified 236 -> CoreToDo -> CoreProgram -> [CoreRule] -> IO () 237-- Used by the IO-is CorePrep too 238endPassIO hsc_env print_unqual pass binds rules 239 = do { dumpPassResult dflags print_unqual mb_flag 240 (ppr pass) (pprPassDetails pass) binds rules 241 ; lintPassResult hsc_env pass binds } 242 where 243 dflags = hsc_dflags hsc_env 244 mb_flag = case coreDumpFlag pass of 245 Just flag | dopt flag dflags -> Just flag 246 | dopt Opt_D_verbose_core2core dflags -> Just flag 247 _ -> Nothing 248 249dumpIfSet :: DynFlags -> Bool -> CoreToDo -> SDoc -> SDoc -> IO () 250dumpIfSet dflags dump_me pass extra_info doc 251 = Err.dumpIfSet dflags dump_me (showSDoc dflags (ppr pass <+> extra_info)) doc 252 253dumpPassResult :: DynFlags 254 -> PrintUnqualified 255 -> Maybe DumpFlag -- Just df => show details in a file whose 256 -- name is specified by df 257 -> SDoc -- Header 258 -> SDoc -- Extra info to appear after header 259 -> CoreProgram -> [CoreRule] 260 -> IO () 261dumpPassResult dflags unqual mb_flag hdr extra_info binds rules 262 = do { forM_ mb_flag $ \flag -> 263 Err.dumpSDoc dflags unqual flag (showSDoc dflags hdr) dump_doc 264 265 -- Report result size 266 -- This has the side effect of forcing the intermediate to be evaluated 267 -- if it's not already forced by a -ddump flag. 268 ; Err.debugTraceMsg dflags 2 size_doc 269 } 270 271 where 272 size_doc = sep [text "Result size of" <+> hdr, nest 2 (equals <+> ppr (coreBindsStats binds))] 273 274 dump_doc = vcat [ nest 2 extra_info 275 , size_doc 276 , blankLine 277 , pprCoreBindingsWithSize binds 278 , ppUnless (null rules) pp_rules ] 279 pp_rules = vcat [ blankLine 280 , text "------ Local rules for imported ids --------" 281 , pprRules rules ] 282 283coreDumpFlag :: CoreToDo -> Maybe DumpFlag 284coreDumpFlag (CoreDoSimplify {}) = Just Opt_D_verbose_core2core 285coreDumpFlag (CoreDoPluginPass {}) = Just Opt_D_verbose_core2core 286coreDumpFlag CoreDoFloatInwards = Just Opt_D_verbose_core2core 287coreDumpFlag (CoreDoFloatOutwards {}) = Just Opt_D_verbose_core2core 288coreDumpFlag CoreLiberateCase = Just Opt_D_verbose_core2core 289coreDumpFlag CoreDoStaticArgs = Just Opt_D_verbose_core2core 290coreDumpFlag CoreDoCallArity = Just Opt_D_dump_call_arity 291coreDumpFlag CoreDoExitify = Just Opt_D_dump_exitify 292coreDumpFlag CoreDoStrictness = Just Opt_D_dump_stranal 293coreDumpFlag CoreDoWorkerWrapper = Just Opt_D_dump_worker_wrapper 294coreDumpFlag CoreDoSpecialising = Just Opt_D_dump_spec 295coreDumpFlag CoreDoSpecConstr = Just Opt_D_dump_spec 296coreDumpFlag CoreCSE = Just Opt_D_dump_cse 297coreDumpFlag CoreDesugar = Just Opt_D_dump_ds_preopt 298coreDumpFlag CoreDesugarOpt = Just Opt_D_dump_ds 299coreDumpFlag CoreTidy = Just Opt_D_dump_simpl 300coreDumpFlag CorePrep = Just Opt_D_dump_prep 301coreDumpFlag CoreOccurAnal = Just Opt_D_dump_occur_anal 302 303coreDumpFlag CoreDoPrintCore = Nothing 304coreDumpFlag (CoreDoRuleCheck {}) = Nothing 305coreDumpFlag CoreDoNothing = Nothing 306coreDumpFlag (CoreDoPasses {}) = Nothing 307 308{- 309************************************************************************ 310* * 311 Top-level interfaces 312* * 313************************************************************************ 314-} 315 316lintPassResult :: HscEnv -> CoreToDo -> CoreProgram -> IO () 317lintPassResult hsc_env pass binds 318 | not (gopt Opt_DoCoreLinting dflags) 319 = return () 320 | otherwise 321 = do { let (warns, errs) = lintCoreBindings dflags pass (interactiveInScope hsc_env) binds 322 ; Err.showPass dflags ("Core Linted result of " ++ showPpr dflags pass) 323 ; displayLintResults dflags pass warns errs binds } 324 where 325 dflags = hsc_dflags hsc_env 326 327displayLintResults :: DynFlags -> CoreToDo 328 -> Bag Err.MsgDoc -> Bag Err.MsgDoc -> CoreProgram 329 -> IO () 330displayLintResults dflags pass warns errs binds 331 | not (isEmptyBag errs) 332 = do { putLogMsg dflags NoReason Err.SevDump noSrcSpan 333 (defaultDumpStyle dflags) 334 (vcat [ lint_banner "errors" (ppr pass), Err.pprMessageBag errs 335 , text "*** Offending Program ***" 336 , pprCoreBindings binds 337 , text "*** End of Offense ***" ]) 338 ; Err.ghcExit dflags 1 } 339 340 | not (isEmptyBag warns) 341 , not (hasNoDebugOutput dflags) 342 , showLintWarnings pass 343 -- If the Core linter encounters an error, output to stderr instead of 344 -- stdout (#13342) 345 = putLogMsg dflags NoReason Err.SevInfo noSrcSpan 346 (defaultDumpStyle dflags) 347 (lint_banner "warnings" (ppr pass) $$ Err.pprMessageBag (mapBag ($$ blankLine) warns)) 348 349 | otherwise = return () 350 where 351 352lint_banner :: String -> SDoc -> SDoc 353lint_banner string pass = text "*** Core Lint" <+> text string 354 <+> text ": in result of" <+> pass 355 <+> text "***" 356 357showLintWarnings :: CoreToDo -> Bool 358-- Disable Lint warnings on the first simplifier pass, because 359-- there may be some INLINE knots still tied, which is tiresomely noisy 360showLintWarnings (CoreDoSimplify _ (SimplMode { sm_phase = InitialPhase })) = False 361showLintWarnings _ = True 362 363lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO () 364lintInteractiveExpr what hsc_env expr 365 | not (gopt Opt_DoCoreLinting dflags) 366 = return () 367 | Just err <- lintExpr dflags (interactiveInScope hsc_env) expr 368 = do { display_lint_err err 369 ; Err.ghcExit dflags 1 } 370 | otherwise 371 = return () 372 where 373 dflags = hsc_dflags hsc_env 374 375 display_lint_err err 376 = do { putLogMsg dflags NoReason Err.SevDump 377 noSrcSpan (defaultDumpStyle dflags) 378 (vcat [ lint_banner "errors" (text what) 379 , err 380 , text "*** Offending Program ***" 381 , pprCoreExpr expr 382 , text "*** End of Offense ***" ]) 383 ; Err.ghcExit dflags 1 } 384 385interactiveInScope :: HscEnv -> [Var] 386-- In GHCi we may lint expressions, or bindings arising from 'deriving' 387-- clauses, that mention variables bound in the interactive context. 388-- These are Local things (see Note [Interactively-bound Ids in GHCi] in HscTypes). 389-- So we have to tell Lint about them, lest it reports them as out of scope. 390-- 391-- We do this by find local-named things that may appear free in interactive 392-- context. This function is pretty revolting and quite possibly not quite right. 393-- When we are not in GHCi, the interactive context (hsc_IC hsc_env) is empty 394-- so this is a (cheap) no-op. 395-- 396-- See #8215 for an example 397interactiveInScope hsc_env 398 = tyvars ++ ids 399 where 400 -- C.f. TcRnDriver.setInteractiveContext, Desugar.deSugarExpr 401 ictxt = hsc_IC hsc_env 402 (cls_insts, _fam_insts) = ic_instances ictxt 403 te1 = mkTypeEnvWithImplicits (ic_tythings ictxt) 404 te = extendTypeEnvWithIds te1 (map instanceDFunId cls_insts) 405 ids = typeEnvIds te 406 tyvars = tyCoVarsOfTypesList $ map idType ids 407 -- Why the type variables? How can the top level envt have free tyvars? 408 -- I think it's because of the GHCi debugger, which can bind variables 409 -- f :: [t] -> [t] 410 -- where t is a RuntimeUnk (see TcType) 411 412-- | Type-check a 'CoreProgram'. See Note [Core Lint guarantee]. 413lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc) 414-- Returns (warnings, errors) 415-- If you edit this function, you may need to update the GHC formalism 416-- See Note [GHC Formalism] 417lintCoreBindings dflags pass local_in_scope binds 418 = initL dflags flags in_scope_set $ 419 addLoc TopLevelBindings $ 420 lintLetBndrs TopLevel binders $ 421 -- Put all the top-level binders in scope at the start 422 -- This is because transformation rules can bring something 423 -- into use 'unexpectedly' 424 do { checkL (null dups) (dupVars dups) 425 ; checkL (null ext_dups) (dupExtVars ext_dups) 426 ; mapM lint_bind binds } 427 where 428 in_scope_set = mkInScopeSet (mkVarSet local_in_scope) 429 430 flags = defaultLintFlags 431 { lf_check_global_ids = check_globals 432 , lf_check_inline_loop_breakers = check_lbs 433 , lf_check_static_ptrs = check_static_ptrs } 434 435 -- See Note [Checking for global Ids] 436 check_globals = case pass of 437 CoreTidy -> False 438 CorePrep -> False 439 _ -> True 440 441 -- See Note [Checking for INLINE loop breakers] 442 check_lbs = case pass of 443 CoreDesugar -> False 444 CoreDesugarOpt -> False 445 _ -> True 446 447 -- See Note [Checking StaticPtrs] 448 check_static_ptrs | not (xopt LangExt.StaticPointers dflags) = AllowAnywhere 449 | otherwise = case pass of 450 CoreDoFloatOutwards _ -> AllowAtTopLevel 451 CoreTidy -> RejectEverywhere 452 CorePrep -> AllowAtTopLevel 453 _ -> AllowAnywhere 454 455 binders = bindersOfBinds binds 456 (_, dups) = removeDups compare binders 457 458 -- dups_ext checks for names with different uniques 459 -- but but the same External name M.n. We don't 460 -- allow this at top level: 461 -- M.n{r3} = ... 462 -- M.n{r29} = ... 463 -- because they both get the same linker symbol 464 ext_dups = snd (removeDups ord_ext (map Var.varName binders)) 465 ord_ext n1 n2 | Just m1 <- nameModule_maybe n1 466 , Just m2 <- nameModule_maybe n2 467 = compare (m1, nameOccName n1) (m2, nameOccName n2) 468 | otherwise = LT 469 470 -- If you edit this function, you may need to update the GHC formalism 471 -- See Note [GHC Formalism] 472 lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs 473 lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs) 474 475{- 476************************************************************************ 477* * 478\subsection[lintUnfolding]{lintUnfolding} 479* * 480************************************************************************ 481 482Note [Linting Unfoldings from Interfaces] 483~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 484 485We use this to check all top-level unfoldings that come in from interfaces 486(it is very painful to catch errors otherwise). 487 488We do not need to call lintUnfolding on unfoldings that are nested within 489top-level unfoldings; they are linted when we lint the top-level unfolding; 490hence the `TopLevelFlag` on `tcPragExpr` in TcIface. 491 492-} 493 494lintUnfolding :: DynFlags 495 -> SrcLoc 496 -> VarSet -- Treat these as in scope 497 -> CoreExpr 498 -> Maybe MsgDoc -- Nothing => OK 499 500lintUnfolding dflags locn vars expr 501 | isEmptyBag errs = Nothing 502 | otherwise = Just (pprMessageBag errs) 503 where 504 in_scope = mkInScopeSet vars 505 (_warns, errs) = initL dflags defaultLintFlags in_scope linter 506 linter = addLoc (ImportedUnfolding locn) $ 507 lintCoreExpr expr 508 509lintExpr :: DynFlags 510 -> [Var] -- Treat these as in scope 511 -> CoreExpr 512 -> Maybe MsgDoc -- Nothing => OK 513 514lintExpr dflags vars expr 515 | isEmptyBag errs = Nothing 516 | otherwise = Just (pprMessageBag errs) 517 where 518 in_scope = mkInScopeSet (mkVarSet vars) 519 (_warns, errs) = initL dflags defaultLintFlags in_scope linter 520 linter = addLoc TopLevelBindings $ 521 lintCoreExpr expr 522 523{- 524************************************************************************ 525* * 526\subsection[lintCoreBinding]{lintCoreBinding} 527* * 528************************************************************************ 529 530Check a core binding, returning the list of variables bound. 531-} 532 533lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM () 534-- If you edit this function, you may need to update the GHC formalism 535-- See Note [GHC Formalism] 536lintSingleBinding top_lvl_flag rec_flag (binder,rhs) 537 = addLoc (RhsOf binder) $ 538 -- Check the rhs 539 do { ty <- lintRhs binder rhs 540 ; binder_ty <- applySubstTy (idType binder) 541 ; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty) 542 543 -- If the binding is for a CoVar, the RHS should be (Coercion co) 544 -- See Note [CoreSyn type and coercion invariant] in CoreSyn 545 ; checkL (not (isCoVar binder) || isCoArg rhs) 546 (mkLetErr binder rhs) 547 548 -- Check that it's not levity-polymorphic 549 -- Do this first, because otherwise isUnliftedType panics 550 -- Annoyingly, this duplicates the test in lintIdBdr, 551 -- because for non-rec lets we call lintSingleBinding first 552 ; checkL (isJoinId binder || not (isTypeLevPoly binder_ty)) 553 (badBndrTyMsg binder (text "levity-polymorphic")) 554 555 -- Check the let/app invariant 556 -- See Note [CoreSyn let/app invariant] in CoreSyn 557 ; checkL ( isJoinId binder 558 || not (isUnliftedType binder_ty) 559 || (isNonRec rec_flag && exprOkForSpeculation rhs) 560 || exprIsTickedString rhs) 561 (badBndrTyMsg binder (text "unlifted")) 562 563 -- Check that if the binder is top-level or recursive, it's not 564 -- demanded. Primitive string literals are exempt as there is no 565 -- computation to perform, see Note [CoreSyn top-level string literals]. 566 ; checkL (not (isStrictId binder) 567 || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)) 568 || exprIsTickedString rhs) 569 (mkStrictMsg binder) 570 571 -- Check that if the binder is at the top level and has type Addr#, 572 -- that it is a string literal, see 573 -- Note [CoreSyn top-level string literals]. 574 ; checkL (not (isTopLevel top_lvl_flag && binder_ty `eqType` addrPrimTy) 575 || exprIsTickedString rhs) 576 (mkTopNonLitStrMsg binder) 577 578 ; flags <- getLintFlags 579 580 -- Check that a join-point binder has a valid type 581 -- NB: lintIdBinder has checked that it is not top-level bound 582 ; case isJoinId_maybe binder of 583 Nothing -> return () 584 Just arity -> checkL (isValidJoinPointType arity binder_ty) 585 (mkInvalidJoinPointMsg binder binder_ty) 586 587 ; when (lf_check_inline_loop_breakers flags 588 && isStableUnfolding (realIdUnfolding binder) 589 && isStrongLoopBreaker (idOccInfo binder) 590 && isInlinePragma (idInlinePragma binder)) 591 (addWarnL (text "INLINE binder is (non-rule) loop breaker:" <+> ppr binder)) 592 -- Only non-rule loop breakers inhibit inlining 593 594 -- We used to check that the dmdTypeDepth of a demand signature never 595 -- exceeds idArity, but that is an unnecessary complication, see 596 -- Note [idArity varies independently of dmdTypeDepth] in DmdAnal 597 598 -- Check that the binder's arity is within the bounds imposed by 599 -- the type and the strictness signature. See Note [exprArity invariant] 600 -- and Note [Trimming arity] 601 ; checkL (typeArity (idType binder) `lengthAtLeast` idArity binder) 602 (text "idArity" <+> ppr (idArity binder) <+> 603 text "exceeds typeArity" <+> 604 ppr (length (typeArity (idType binder))) <> colon <+> 605 ppr binder) 606 607 ; case splitStrictSig (idStrictness binder) of 608 (demands, result_info) | isBotRes result_info -> 609 checkL (demands `lengthAtLeast` idArity binder) 610 (text "idArity" <+> ppr (idArity binder) <+> 611 text "exceeds arity imposed by the strictness signature" <+> 612 ppr (idStrictness binder) <> colon <+> 613 ppr binder) 614 _ -> return () 615 616 ; mapM_ (lintCoreRule binder binder_ty) (idCoreRules binder) 617 618 ; addLoc (UnfoldingOf binder) $ 619 lintIdUnfolding binder binder_ty (idUnfolding binder) } 620 621 -- We should check the unfolding, if any, but this is tricky because 622 -- the unfolding is a SimplifiableCoreExpr. Give up for now. 623 624-- | Checks the RHS of bindings. It only differs from 'lintCoreExpr' 625-- in that it doesn't reject occurrences of the function 'makeStatic' when they 626-- appear at the top level and @lf_check_static_ptrs == AllowAtTopLevel@, and 627-- for join points, it skips the outer lambdas that take arguments to the 628-- join point. 629-- 630-- See Note [Checking StaticPtrs]. 631lintRhs :: Id -> CoreExpr -> LintM OutType 632lintRhs bndr rhs 633 | Just arity <- isJoinId_maybe bndr 634 = lint_join_lams arity arity True rhs 635 | AlwaysTailCalled arity <- tailCallInfo (idOccInfo bndr) 636 = lint_join_lams arity arity False rhs 637 where 638 lint_join_lams 0 _ _ rhs 639 = lintCoreExpr rhs 640 641 lint_join_lams n tot enforce (Lam var expr) 642 = addLoc (LambdaBodyOf var) $ 643 lintBinder LambdaBind var $ \ var' -> 644 do { body_ty <- lint_join_lams (n-1) tot enforce expr 645 ; return $ mkLamType var' body_ty } 646 647 lint_join_lams n tot True _other 648 = failWithL $ mkBadJoinArityMsg bndr tot (tot-n) rhs 649 lint_join_lams _ _ False rhs 650 = markAllJoinsBad $ lintCoreExpr rhs 651 -- Future join point, not yet eta-expanded 652 -- Body is not a tail position 653 654-- Allow applications of the data constructor @StaticPtr@ at the top 655-- but produce errors otherwise. 656lintRhs _bndr rhs = fmap lf_check_static_ptrs getLintFlags >>= go 657 where 658 -- Allow occurrences of 'makeStatic' at the top-level but produce errors 659 -- otherwise. 660 go AllowAtTopLevel 661 | (binders0, rhs') <- collectTyBinders rhs 662 , Just (fun, t, info, e) <- collectMakeStaticArgs rhs' 663 = markAllJoinsBad $ 664 foldr 665 -- imitate @lintCoreExpr (Lam ...)@ 666 (\var loopBinders -> 667 addLoc (LambdaBodyOf var) $ 668 lintBinder LambdaBind var $ \var' -> 669 do { body_ty <- loopBinders 670 ; return $ mkLamType var' body_ty } 671 ) 672 -- imitate @lintCoreExpr (App ...)@ 673 (do fun_ty <- lintCoreExpr fun 674 lintCoreArgs fun_ty [Type t, info, e] 675 ) 676 binders0 677 go _ = markAllJoinsBad $ lintCoreExpr rhs 678 679lintIdUnfolding :: Id -> Type -> Unfolding -> LintM () 680lintIdUnfolding bndr bndr_ty uf 681 | isStableUnfolding uf 682 , Just rhs <- maybeUnfoldingTemplate uf 683 = do { ty <- lintRhs bndr rhs 684 ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) } 685lintIdUnfolding _ _ _ 686 = return () -- Do not Lint unstable unfoldings, because that leads 687 -- to exponential behaviour; c.f. CoreFVs.idUnfoldingVars 688 689{- 690Note [Checking for INLINE loop breakers] 691~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 692It's very suspicious if a strong loop breaker is marked INLINE. 693 694However, the desugarer generates instance methods with INLINE pragmas 695that form a mutually recursive group. Only after a round of 696simplification are they unravelled. So we suppress the test for 697the desugarer. 698 699************************************************************************ 700* * 701\subsection[lintCoreExpr]{lintCoreExpr} 702* * 703************************************************************************ 704-} 705 706-- For OutType, OutKind, the substitution has been applied, 707-- but has not been linted yet 708 709type LintedType = Type -- Substitution applied, and type is linted 710type LintedKind = Kind 711 712lintCoreExpr :: CoreExpr -> LintM OutType 713-- The returned type has the substitution from the monad 714-- already applied to it: 715-- lintCoreExpr e subst = exprType (subst e) 716-- 717-- The returned "type" can be a kind, if the expression is (Type ty) 718 719-- If you edit this function, you may need to update the GHC formalism 720-- See Note [GHC Formalism] 721lintCoreExpr (Var var) 722 = lintVarOcc var 0 723 724lintCoreExpr (Lit lit) 725 = return (literalType lit) 726 727lintCoreExpr (Cast expr co) 728 = do { expr_ty <- markAllJoinsBad $ lintCoreExpr expr 729 ; co' <- applySubstCo co 730 ; (_, k2, from_ty, to_ty, r) <- lintCoercion co' 731 ; checkValueKind k2 (text "target of cast" <+> quotes (ppr co)) 732 ; lintRole co' Representational r 733 ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty) 734 ; return to_ty } 735 736lintCoreExpr (Tick tickish expr) 737 = do case tickish of 738 Breakpoint _ ids -> forM_ ids $ \id -> do 739 checkDeadIdOcc id 740 lookupIdInScope id 741 _ -> return () 742 markAllJoinsBadIf block_joins $ lintCoreExpr expr 743 where 744 block_joins = not (tickish `tickishScopesLike` SoftScope) 745 -- TODO Consider whether this is the correct rule. It is consistent with 746 -- the simplifier's behaviour - cost-centre-scoped ticks become part of 747 -- the continuation, and thus they behave like part of an evaluation 748 -- context, but soft-scoped and non-scoped ticks simply wrap the result 749 -- (see Simplify.simplTick). 750 751lintCoreExpr (Let (NonRec tv (Type ty)) body) 752 | isTyVar tv 753 = -- See Note [Linting type lets] 754 do { ty' <- applySubstTy ty 755 ; lintTyBndr tv $ \ tv' -> 756 do { addLoc (RhsOf tv) $ lintTyKind tv' ty' 757 -- Now extend the substitution so we 758 -- take advantage of it in the body 759 ; extendSubstL tv ty' $ 760 addLoc (BodyOfLetRec [tv]) $ 761 lintCoreExpr body } } 762 763lintCoreExpr (Let (NonRec bndr rhs) body) 764 | isId bndr 765 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs) 766 ; addLoc (BodyOfLetRec [bndr]) 767 (lintBinder LetBind bndr $ \_ -> 768 addGoodJoins [bndr] $ 769 lintCoreExpr body) } 770 771 | otherwise 772 = failWithL (mkLetErr bndr rhs) -- Not quite accurate 773 774lintCoreExpr e@(Let (Rec pairs) body) 775 = lintLetBndrs NotTopLevel bndrs $ 776 addGoodJoins bndrs $ 777 do { -- Check that the list of pairs is non-empty 778 checkL (not (null pairs)) (emptyRec e) 779 780 -- Check that there are no duplicated binders 781 ; checkL (null dups) (dupVars dups) 782 783 -- Check that either all the binders are joins, or none 784 ; checkL (all isJoinId bndrs || all (not . isJoinId) bndrs) $ 785 mkInconsistentRecMsg bndrs 786 787 ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs 788 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) } 789 where 790 bndrs = map fst pairs 791 (_, dups) = removeDups compare bndrs 792 793lintCoreExpr e@(App _ _) 794 = do { fun_ty <- lintCoreFun fun (length args) 795 ; lintCoreArgs fun_ty args } 796 where 797 (fun, args) = collectArgs e 798 799lintCoreExpr (Lam var expr) 800 = addLoc (LambdaBodyOf var) $ 801 markAllJoinsBad $ 802 lintBinder LambdaBind var $ \ var' -> 803 do { body_ty <- lintCoreExpr expr 804 ; return $ mkLamType var' body_ty } 805 806lintCoreExpr (Case scrut var alt_ty alts) 807 = lintCaseExpr scrut var alt_ty alts 808 809-- This case can't happen; linting types in expressions gets routed through 810-- lintCoreArgs 811lintCoreExpr (Type ty) 812 = failWithL (text "Type found as expression" <+> ppr ty) 813 814lintCoreExpr (Coercion co) 815 = do { (k1, k2, ty1, ty2, role) <- lintInCo co 816 ; return (mkHeteroCoercionType role k1 k2 ty1 ty2) } 817 818---------------------- 819lintVarOcc :: Var -> Int -- Number of arguments (type or value) being passed 820 -> LintM Type -- returns type of the *variable* 821lintVarOcc var nargs 822 = do { checkL (isNonCoVarId var) 823 (text "Non term variable" <+> ppr var) 824 -- See CoreSyn Note [Variable occurrences in Core] 825 826 -- Cneck that the type of the occurrence is the same 827 -- as the type of the binding site 828 ; ty <- applySubstTy (idType var) 829 ; var' <- lookupIdInScope var 830 ; let ty' = idType var' 831 ; ensureEqTys ty ty' $ mkBndrOccTypeMismatchMsg var' var ty' ty 832 833 -- Check for a nested occurrence of the StaticPtr constructor. 834 -- See Note [Checking StaticPtrs]. 835 ; lf <- getLintFlags 836 ; when (nargs /= 0 && lf_check_static_ptrs lf /= AllowAnywhere) $ 837 checkL (idName var /= makeStaticName) $ 838 text "Found makeStatic nested in an expression" 839 840 ; checkDeadIdOcc var 841 ; checkJoinOcc var nargs 842 843 ; return (idType var') } 844 845lintCoreFun :: CoreExpr 846 -> Int -- Number of arguments (type or val) being passed 847 -> LintM Type -- Returns type of the *function* 848lintCoreFun (Var var) nargs 849 = lintVarOcc var nargs 850 851lintCoreFun (Lam var body) nargs 852 -- Act like lintCoreExpr of Lam, but *don't* call markAllJoinsBad; see 853 -- Note [Beta redexes] 854 | nargs /= 0 855 = addLoc (LambdaBodyOf var) $ 856 lintBinder LambdaBind var $ \ var' -> 857 do { body_ty <- lintCoreFun body (nargs - 1) 858 ; return $ mkLamType var' body_ty } 859 860lintCoreFun expr nargs 861 = markAllJoinsBadIf (nargs /= 0) $ 862 -- See Note [Join points are less general than the paper] 863 lintCoreExpr expr 864 865------------------ 866checkDeadIdOcc :: Id -> LintM () 867-- Occurrences of an Id should never be dead.... 868-- except when we are checking a case pattern 869checkDeadIdOcc id 870 | isDeadOcc (idOccInfo id) 871 = do { in_case <- inCasePat 872 ; checkL in_case 873 (text "Occurrence of a dead Id" <+> ppr id) } 874 | otherwise 875 = return () 876 877------------------ 878checkJoinOcc :: Id -> JoinArity -> LintM () 879-- Check that if the occurrence is a JoinId, then so is the 880-- binding site, and it's a valid join Id 881checkJoinOcc var n_args 882 | Just join_arity_occ <- isJoinId_maybe var 883 = do { mb_join_arity_bndr <- lookupJoinId var 884 ; case mb_join_arity_bndr of { 885 Nothing -> -- Binder is not a join point 886 addErrL (invalidJoinOcc var) ; 887 888 Just join_arity_bndr -> 889 890 do { checkL (join_arity_bndr == join_arity_occ) $ 891 -- Arity differs at binding site and occurrence 892 mkJoinBndrOccMismatchMsg var join_arity_bndr join_arity_occ 893 894 ; checkL (n_args == join_arity_occ) $ 895 -- Arity doesn't match #args 896 mkBadJumpMsg var join_arity_occ n_args } } } 897 898 | otherwise 899 = return () 900 901{- 902Note [No alternatives lint check] 903~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 904Case expressions with no alternatives are odd beasts, and it would seem 905like they would worth be looking at in the linter (cf #10180). We 906used to check two things: 907 908* exprIsHNF is false: it would *seem* to be terribly wrong if 909 the scrutinee was already in head normal form. 910 911* exprIsBottom is true: we should be able to see why GHC believes the 912 scrutinee is diverging for sure. 913 914It was already known that the second test was not entirely reliable. 915Unfortunately (#13990), the first test turned out not to be reliable 916either. Getting the checks right turns out to be somewhat complicated. 917 918For example, suppose we have (comment 8) 919 920 data T a where 921 TInt :: T Int 922 923 absurdTBool :: T Bool -> a 924 absurdTBool v = case v of 925 926 data Foo = Foo !(T Bool) 927 928 absurdFoo :: Foo -> a 929 absurdFoo (Foo x) = absurdTBool x 930 931GHC initially accepts the empty case because of the GADT conditions. But then 932we inline absurdTBool, getting 933 934 absurdFoo (Foo x) = case x of 935 936x is in normal form (because the Foo constructor is strict) but the 937case is empty. To avoid this problem, GHC would have to recognize 938that matching on Foo x is already absurd, which is not so easy. 939 940More generally, we don't really know all the ways that GHC can 941lose track of why an expression is bottom, so we shouldn't make too 942much fuss when that happens. 943 944 945Note [Beta redexes] 946~~~~~~~~~~~~~~~~~~~ 947Consider: 948 949 join j @x y z = ... in 950 (\@x y z -> jump j @x y z) @t e1 e2 951 952This is clearly ill-typed, since the jump is inside both an application and a 953lambda, either of which is enough to disqualify it as a tail call (see Note 954[Invariants on join points] in CoreSyn). However, strictly from a 955lambda-calculus perspective, the term doesn't go wrong---after the two beta 956reductions, the jump *is* a tail call and everything is fine. 957 958Why would we want to allow this when we have let? One reason is that a compound 959beta redex (that is, one with more than one argument) has different scoping 960rules: naively reducing the above example using lets will capture any free 961occurrence of y in e2. More fundamentally, type lets are tricky; many passes, 962such as Float Out, tacitly assume that the incoming program's type lets have 963all been dealt with by the simplifier. Thus we don't want to let-bind any types 964in, say, CoreSubst.simpleOptPgm, which in some circumstances can run immediately 965before Float Out. 966 967All that said, currently CoreSubst.simpleOptPgm is the only thing using this 968loophole, doing so to avoid re-traversing large functions (beta-reducing a type 969lambda without introducing a type let requires a substitution). TODO: Improve 970simpleOptPgm so that we can forget all this ever happened. 971 972************************************************************************ 973* * 974\subsection[lintCoreArgs]{lintCoreArgs} 975* * 976************************************************************************ 977 978The basic version of these functions checks that the argument is a 979subtype of the required type, as one would expect. 980-} 981 982 983lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType 984lintCoreArgs fun_ty args = foldM lintCoreArg fun_ty args 985 986lintCoreArg :: OutType -> CoreArg -> LintM OutType 987lintCoreArg fun_ty (Type arg_ty) 988 = do { checkL (not (isCoercionTy arg_ty)) 989 (text "Unnecessary coercion-to-type injection:" 990 <+> ppr arg_ty) 991 ; arg_ty' <- applySubstTy arg_ty 992 ; lintTyApp fun_ty arg_ty' } 993 994lintCoreArg fun_ty arg 995 = do { arg_ty <- markAllJoinsBad $ lintCoreExpr arg 996 -- See Note [Levity polymorphism invariants] in CoreSyn 997 ; lintL (not (isTypeLevPoly arg_ty)) 998 (text "Levity-polymorphic argument:" <+> 999 (ppr arg <+> dcolon <+> parens (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty)))) 1000 -- check for levity polymorphism first, because otherwise isUnliftedType panics 1001 1002 ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg) 1003 (mkLetAppMsg arg) 1004 ; lintValApp arg fun_ty arg_ty } 1005 1006----------------- 1007lintAltBinders :: OutType -- Scrutinee type 1008 -> OutType -- Constructor type 1009 -> [OutVar] -- Binders 1010 -> LintM () 1011-- If you edit this function, you may need to update the GHC formalism 1012-- See Note [GHC Formalism] 1013lintAltBinders scrut_ty con_ty [] 1014 = ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty) 1015lintAltBinders scrut_ty con_ty (bndr:bndrs) 1016 | isTyVar bndr 1017 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr) 1018 ; lintAltBinders scrut_ty con_ty' bndrs } 1019 | otherwise 1020 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr) 1021 ; lintAltBinders scrut_ty con_ty' bndrs } 1022 1023----------------- 1024lintTyApp :: OutType -> OutType -> LintM OutType 1025lintTyApp fun_ty arg_ty 1026 | Just (tv,body_ty) <- splitForAllTy_maybe fun_ty 1027 = do { lintTyKind tv arg_ty 1028 ; in_scope <- getInScope 1029 -- substTy needs the set of tyvars in scope to avoid generating 1030 -- uniques that are already in scope. 1031 -- See Note [The substitution invariant] in TyCoSubst 1032 ; return (substTyWithInScope in_scope [tv] [arg_ty] body_ty) } 1033 1034 | otherwise 1035 = failWithL (mkTyAppMsg fun_ty arg_ty) 1036 1037----------------- 1038lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType 1039lintValApp arg fun_ty arg_ty 1040 | Just (arg,res) <- splitFunTy_maybe fun_ty 1041 = do { ensureEqTys arg arg_ty err1 1042 ; return res } 1043 | otherwise 1044 = failWithL err2 1045 where 1046 err1 = mkAppMsg fun_ty arg_ty arg 1047 err2 = mkNonFunAppMsg fun_ty arg_ty arg 1048 1049lintTyKind :: OutTyVar -> OutType -> LintM () 1050-- Both args have had substitution applied 1051 1052-- If you edit this function, you may need to update the GHC formalism 1053-- See Note [GHC Formalism] 1054lintTyKind tyvar arg_ty 1055 -- Arg type might be boxed for a function with an uncommitted 1056 -- tyvar; notably this is used so that we can give 1057 -- error :: forall a:*. String -> a 1058 -- and then apply it to both boxed and unboxed types. 1059 = do { arg_kind <- lintType arg_ty 1060 ; unless (arg_kind `eqType` tyvar_kind) 1061 (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "Linted Arg kind:" <+> ppr arg_kind))) } 1062 where 1063 tyvar_kind = tyVarKind tyvar 1064 1065{- 1066************************************************************************ 1067* * 1068\subsection[lintCoreAlts]{lintCoreAlts} 1069* * 1070************************************************************************ 1071-} 1072 1073lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM OutType 1074lintCaseExpr scrut var alt_ty alts = 1075 do { let e = Case scrut var alt_ty alts -- Just for error messages 1076 1077 -- Check the scrutinee 1078 ; scrut_ty <- markAllJoinsBad $ lintCoreExpr scrut 1079 -- See Note [Join points are less general than the paper] 1080 -- in CoreSyn 1081 1082 ; (alt_ty, _) <- addLoc (CaseTy scrut) $ 1083 lintInTy alt_ty 1084 ; (var_ty, _) <- addLoc (IdTy var) $ 1085 lintInTy (idType var) 1086 1087 -- We used to try to check whether a case expression with no 1088 -- alternatives was legitimate, but this didn't work. 1089 -- See Note [No alternatives lint check] for details. 1090 1091 -- Check that the scrutinee is not a floating-point type 1092 -- if there are any literal alternatives 1093 -- See CoreSyn Note [Case expression invariants] item (5) 1094 -- See Note [Rules for floating-point comparisons] in PrelRules 1095 ; let isLitPat (LitAlt _, _ , _) = True 1096 isLitPat _ = False 1097 ; checkL (not $ isFloatingTy scrut_ty && any isLitPat alts) 1098 (ptext (sLit $ "Lint warning: Scrutinising floating-point " ++ 1099 "expression with literal pattern in case " ++ 1100 "analysis (see #9238).") 1101 $$ text "scrut" <+> ppr scrut) 1102 1103 ; case tyConAppTyCon_maybe (idType var) of 1104 Just tycon 1105 | debugIsOn 1106 , isAlgTyCon tycon 1107 , not (isAbstractTyCon tycon) 1108 , null (tyConDataCons tycon) 1109 , not (exprIsBottom scrut) 1110 -> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var)) 1111 -- This can legitimately happen for type families 1112 $ return () 1113 _otherwise -> return () 1114 1115 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate 1116 1117 ; subst <- getTCvSubst 1118 ; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst) 1119 -- See CoreSyn Note [Case expression invariants] item (7) 1120 1121 ; lintBinder CaseBind var $ \_ -> 1122 do { -- Check the alternatives 1123 mapM_ (lintCoreAlt scrut_ty alt_ty) alts 1124 ; checkCaseAlts e scrut_ty alts 1125 ; return alt_ty } } 1126 1127checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM () 1128-- a) Check that the alts are non-empty 1129-- b1) Check that the DEFAULT comes first, if it exists 1130-- b2) Check that the others are in increasing order 1131-- c) Check that there's a default for infinite types 1132-- NB: Algebraic cases are not necessarily exhaustive, because 1133-- the simplifier correctly eliminates case that can't 1134-- possibly match. 1135 1136checkCaseAlts e ty alts = 1137 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e) 1138 -- See CoreSyn Note [Case expression invariants] item (2) 1139 1140 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e) 1141 -- See CoreSyn Note [Case expression invariants] item (3) 1142 1143 -- For types Int#, Word# with an infinite (well, large!) number of 1144 -- possible values, there should usually be a DEFAULT case 1145 -- But (see Note [Empty case alternatives] in CoreSyn) it's ok to 1146 -- have *no* case alternatives. 1147 -- In effect, this is a kind of partial test. I suppose it's possible 1148 -- that we might *know* that 'x' was 1 or 2, in which case 1149 -- case x of { 1 -> e1; 2 -> e2 } 1150 -- would be fine. 1151 ; checkL (isJust maybe_deflt || not is_infinite_ty || null alts) 1152 (nonExhaustiveAltsMsg e) } 1153 where 1154 (con_alts, maybe_deflt) = findDefault alts 1155 1156 -- Check that successive alternatives have strictly increasing tags 1157 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest 1158 increasing_tag _ = True 1159 1160 non_deflt (DEFAULT, _, _) = False 1161 non_deflt _ = True 1162 1163 is_infinite_ty = case tyConAppTyCon_maybe ty of 1164 Nothing -> False 1165 Just tycon -> isPrimTyCon tycon 1166 1167lintAltExpr :: CoreExpr -> OutType -> LintM () 1168lintAltExpr expr ann_ty 1169 = do { actual_ty <- lintCoreExpr expr 1170 ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) } 1171 -- See CoreSyn Note [Case expression invariants] item (6) 1172 1173lintCoreAlt :: OutType -- Type of scrutinee 1174 -> OutType -- Type of the alternative 1175 -> CoreAlt 1176 -> LintM () 1177-- If you edit this function, you may need to update the GHC formalism 1178-- See Note [GHC Formalism] 1179lintCoreAlt _ alt_ty (DEFAULT, args, rhs) = 1180 do { lintL (null args) (mkDefaultArgsMsg args) 1181 ; lintAltExpr rhs alt_ty } 1182 1183lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) 1184 | litIsLifted lit 1185 = failWithL integerScrutinisedMsg 1186 | otherwise 1187 = do { lintL (null args) (mkDefaultArgsMsg args) 1188 ; ensureEqTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty) 1189 ; lintAltExpr rhs alt_ty } 1190 where 1191 lit_ty = literalType lit 1192 1193lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs) 1194 | isNewTyCon (dataConTyCon con) 1195 = addErrL (mkNewTyDataConAltMsg scrut_ty alt) 1196 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty 1197 = addLoc (CaseAlt alt) $ do 1198 { -- First instantiate the universally quantified 1199 -- type variables of the data constructor 1200 -- We've already check 1201 lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con) 1202 ; let con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys 1203 1204 -- And now bring the new binders into scope 1205 ; lintBinders CasePatBind args $ \ args' -> do 1206 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args') 1207 ; lintAltExpr rhs alt_ty } } 1208 1209 | otherwise -- Scrut-ty is wrong shape 1210 = addErrL (mkBadAltMsg scrut_ty alt) 1211 1212{- 1213************************************************************************ 1214* * 1215\subsection[lint-types]{Types} 1216* * 1217************************************************************************ 1218-} 1219 1220-- When we lint binders, we (one at a time and in order): 1221-- 1. Lint var types or kinds (possibly substituting) 1222-- 2. Add the binder to the in scope set, and if its a coercion var, 1223-- we may extend the substitution to reflect its (possibly) new kind 1224lintBinders :: BindingSite -> [Var] -> ([Var] -> LintM a) -> LintM a 1225lintBinders _ [] linterF = linterF [] 1226lintBinders site (var:vars) linterF = lintBinder site var $ \var' -> 1227 lintBinders site vars $ \ vars' -> 1228 linterF (var':vars') 1229 1230-- If you edit this function, you may need to update the GHC formalism 1231-- See Note [GHC Formalism] 1232lintBinder :: BindingSite -> Var -> (Var -> LintM a) -> LintM a 1233lintBinder site var linterF 1234 | isTyVar var = lintTyBndr var linterF 1235 | isCoVar var = lintCoBndr var linterF 1236 | otherwise = lintIdBndr NotTopLevel site var linterF 1237 1238lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a 1239lintTyBndr tv thing_inside 1240 = do { subst <- getTCvSubst 1241 ; let (subst', tv') = substTyVarBndr subst tv 1242 ; lintKind (varType tv') 1243 ; updateTCvSubst subst' (thing_inside tv') } 1244 1245lintCoBndr :: InCoVar -> (OutCoVar -> LintM a) -> LintM a 1246lintCoBndr cv thing_inside 1247 = do { subst <- getTCvSubst 1248 ; let (subst', cv') = substCoVarBndr subst cv 1249 ; lintKind (varType cv') 1250 ; lintL (isCoVarType (varType cv')) 1251 (text "CoVar with non-coercion type:" <+> pprTyVar cv) 1252 ; updateTCvSubst subst' (thing_inside cv') } 1253 1254lintLetBndrs :: TopLevelFlag -> [Var] -> LintM a -> LintM a 1255lintLetBndrs top_lvl ids linterF 1256 = go ids 1257 where 1258 go [] = linterF 1259 go (id:ids) = lintIdBndr top_lvl LetBind id $ \_ -> 1260 go ids 1261 1262lintIdBndr :: TopLevelFlag -> BindingSite 1263 -> InVar -> (OutVar -> LintM a) -> LintM a 1264-- Do substitution on the type of a binder and add the var with this 1265-- new type to the in-scope set of the second argument 1266-- ToDo: lint its rules 1267lintIdBndr top_lvl bind_site id linterF 1268 = ASSERT2( isId id, ppr id ) 1269 do { flags <- getLintFlags 1270 ; checkL (not (lf_check_global_ids flags) || isLocalId id) 1271 (text "Non-local Id binder" <+> ppr id) 1272 -- See Note [Checking for global Ids] 1273 1274 -- Check that if the binder is nested, it is not marked as exported 1275 ; checkL (not (isExportedId id) || is_top_lvl) 1276 (mkNonTopExportedMsg id) 1277 1278 -- Check that if the binder is nested, it does not have an external name 1279 ; checkL (not (isExternalName (Var.varName id)) || is_top_lvl) 1280 (mkNonTopExternalNameMsg id) 1281 1282 ; (ty, k) <- addLoc (IdTy id) $ 1283 lintInTy (idType id) 1284 1285 -- See Note [Levity polymorphism invariants] in CoreSyn 1286 ; lintL (isJoinId id || not (isKindLevPoly k)) 1287 (text "Levity-polymorphic binder:" <+> 1288 (ppr id <+> dcolon <+> parens (ppr ty <+> dcolon <+> ppr k))) 1289 1290 -- Check that a join-id is a not-top-level let-binding 1291 ; when (isJoinId id) $ 1292 checkL (not is_top_lvl && is_let_bind) $ 1293 mkBadJoinBindMsg id 1294 1295 -- Check that the Id does not have type (t1 ~# t2) or (t1 ~R# t2); 1296 -- if so, it should be a CoVar, and checked by lintCoVarBndr 1297 ; lintL (not (isCoVarType ty)) 1298 (text "Non-CoVar has coercion type" <+> ppr id <+> dcolon <+> ppr ty) 1299 1300 ; let id' = setIdType id ty 1301 ; addInScopeVar id' $ (linterF id') } 1302 where 1303 is_top_lvl = isTopLevel top_lvl 1304 is_let_bind = case bind_site of 1305 LetBind -> True 1306 _ -> False 1307 1308{- 1309%************************************************************************ 1310%* * 1311 Types 1312%* * 1313%************************************************************************ 1314-} 1315 1316lintTypes :: DynFlags 1317 -> [TyCoVar] -- Treat these as in scope 1318 -> [Type] 1319 -> Maybe MsgDoc -- Nothing => OK 1320lintTypes dflags vars tys 1321 | isEmptyBag errs = Nothing 1322 | otherwise = Just (pprMessageBag errs) 1323 where 1324 in_scope = emptyInScopeSet 1325 (_warns, errs) = initL dflags defaultLintFlags in_scope linter 1326 linter = lintBinders LambdaBind vars $ \_ -> 1327 mapM_ lintInTy tys 1328 1329lintInTy :: InType -> LintM (LintedType, LintedKind) 1330-- Types only, not kinds 1331-- Check the type, and apply the substitution to it 1332-- See Note [Linting type lets] 1333lintInTy ty 1334 = addLoc (InType ty) $ 1335 do { ty' <- applySubstTy ty 1336 ; k <- lintType ty' 1337 ; lintKind k -- The kind returned by lintType is already 1338 -- a LintedKind but we also want to check that 1339 -- k :: *, which lintKind does 1340 ; return (ty', k) } 1341 1342checkTyCon :: TyCon -> LintM () 1343checkTyCon tc 1344 = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc) 1345 1346------------------- 1347lintType :: OutType -> LintM LintedKind 1348-- The returned Kind has itself been linted 1349 1350-- If you edit this function, you may need to update the GHC formalism 1351-- See Note [GHC Formalism] 1352lintType (TyVarTy tv) 1353 = do { checkL (isTyVar tv) (mkBadTyVarMsg tv) 1354 ; lintTyCoVarInScope tv 1355 ; return (tyVarKind tv) } 1356 -- We checked its kind when we added it to the envt 1357 1358lintType ty@(AppTy t1 t2) 1359 | TyConApp {} <- t1 1360 = failWithL $ text "TyConApp to the left of AppTy:" <+> ppr ty 1361 | otherwise 1362 = do { k1 <- lintType t1 1363 ; k2 <- lintType t2 1364 ; lint_ty_app ty k1 [(t2,k2)] } 1365 1366lintType ty@(TyConApp tc tys) 1367 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc 1368 = do { report_unsat <- lf_report_unsat_syns <$> getLintFlags 1369 ; lintTySynFamApp report_unsat ty tc tys } 1370 1371 | isFunTyCon tc 1372 , tys `lengthIs` 4 1373 -- We should never see a saturated application of funTyCon; such 1374 -- applications should be represented with the FunTy constructor. 1375 -- See Note [Linting function types] and 1376 -- Note [Representation of function types]. 1377 = failWithL (hang (text "Saturated application of (->)") 2 (ppr ty)) 1378 1379 | otherwise -- Data types, data families, primitive types 1380 = do { checkTyCon tc 1381 ; ks <- mapM lintType tys 1382 ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) } 1383 1384-- arrows can related *unlifted* kinds, so this has to be separate from 1385-- a dependent forall. 1386lintType ty@(FunTy _ t1 t2) 1387 = do { k1 <- lintType t1 1388 ; k2 <- lintType t2 1389 ; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 } 1390 1391lintType t@(ForAllTy (Bndr tv _vis) ty) 1392 -- forall over types 1393 | isTyVar tv 1394 = lintTyBndr tv $ \tv' -> 1395 do { k <- lintType ty 1396 ; checkValueKind k (text "the body of forall:" <+> ppr t) 1397 ; case occCheckExpand [tv'] k of -- See Note [Stupid type synonyms] 1398 Just k' -> return k' 1399 Nothing -> failWithL (hang (text "Variable escape in forall:") 1400 2 (vcat [ text "type:" <+> ppr t 1401 , text "kind:" <+> ppr k ])) 1402 } 1403 1404lintType t@(ForAllTy (Bndr cv _vis) ty) 1405 -- forall over coercions 1406 = do { lintL (isCoVar cv) 1407 (text "Non-Tyvar or Non-Covar bound in type:" <+> ppr t) 1408 ; lintL (cv `elemVarSet` tyCoVarsOfType ty) 1409 (text "Covar does not occur in the body:" <+> ppr t) 1410 ; lintCoBndr cv $ \_ -> 1411 do { k <- lintType ty 1412 ; checkValueKind k (text "the body of forall:" <+> ppr t) 1413 ; return liftedTypeKind 1414 -- We don't check variable escape here. Namely, k could refer to cv' 1415 -- See Note [NthCo and newtypes] in TyCoRep 1416 }} 1417 1418lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty) 1419 1420lintType (CastTy ty co) 1421 = do { k1 <- lintType ty 1422 ; (k1', k2) <- lintStarCoercion co 1423 ; ensureEqTys k1 k1' (mkCastTyErr ty co k1' k1) 1424 ; return k2 } 1425 1426lintType (CoercionTy co) 1427 = do { (k1, k2, ty1, ty2, r) <- lintCoercion co 1428 ; return $ mkHeteroCoercionType r k1 k2 ty1 ty2 } 1429 1430{- Note [Stupid type synonyms] 1431~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1432Consider (#14939) 1433 type Alg cls ob = ob 1434 f :: forall (cls :: * -> Constraint) (b :: Alg cls *). b 1435 1436Here 'cls' appears free in b's kind, which would usually be illegal 1437(because in (forall a. ty), ty's kind should not mention 'a'). But 1438#in this case (Alg cls *) = *, so all is well. Currently we allow 1439this, and make Lint expand synonyms where necessary to make it so. 1440 1441c.f. TcUnify.occCheckExpand and CoreUtils.coreAltsType which deal 1442with the same problem. A single systematic solution eludes me. 1443-} 1444 1445----------------- 1446lintTySynFamApp :: Bool -> Type -> TyCon -> [Type] -> LintM LintedKind 1447-- The TyCon is a type synonym or a type family (not a data family) 1448-- See Note [Linting type synonym applications] 1449-- c.f. TcValidity.check_syn_tc_app 1450lintTySynFamApp report_unsat ty tc tys 1451 | report_unsat -- Report unsaturated only if report_unsat is on 1452 , tys `lengthLessThan` tyConArity tc 1453 = failWithL (hang (text "Un-saturated type application") 2 (ppr ty)) 1454 1455 -- Deal with type synonyms 1456 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys 1457 , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys' 1458 = do { -- Kind-check the argument types, but without reporting 1459 -- un-saturated type families/synonyms 1460 ks <- setReportUnsat False (mapM lintType tys) 1461 1462 ; when report_unsat $ 1463 do { _ <- lintType expanded_ty 1464 ; return () } 1465 1466 ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) } 1467 1468 -- Otherwise this must be a type family 1469 | otherwise 1470 = do { ks <- mapM lintType tys 1471 ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) } 1472 1473----------------- 1474lintKind :: OutKind -> LintM () 1475-- If you edit this function, you may need to update the GHC formalism 1476-- See Note [GHC Formalism] 1477lintKind k = do { sk <- lintType k 1478 ; unless (classifiesTypeWithValues sk) 1479 (addErrL (hang (text "Ill-kinded kind:" <+> ppr k) 1480 2 (text "has kind:" <+> ppr sk))) } 1481 1482----------------- 1483-- Confirms that a type is really *, #, Constraint etc 1484checkValueKind :: OutKind -> SDoc -> LintM () 1485checkValueKind k doc 1486 = lintL (classifiesTypeWithValues k) 1487 (text "Non-*-like kind when *-like expected:" <+> ppr k $$ 1488 text "when checking" <+> doc) 1489 1490----------------- 1491lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind 1492-- If you edit this function, you may need to update the GHC formalism 1493-- See Note [GHC Formalism] 1494lintArrow what k1 k2 -- Eg lintArrow "type or kind `blah'" k1 k2 1495 -- or lintarrow "coercion `blah'" k1 k2 1496 = do { unless (classifiesTypeWithValues k1) (addErrL (msg (text "argument") k1)) 1497 ; unless (classifiesTypeWithValues k2) (addErrL (msg (text "result") k2)) 1498 ; return liftedTypeKind } 1499 where 1500 msg ar k 1501 = vcat [ hang (text "Ill-kinded" <+> ar) 1502 2 (text "in" <+> what) 1503 , what <+> text "kind:" <+> ppr k ] 1504 1505----------------- 1506lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind 1507lint_ty_app ty k tys 1508 = lint_app (text "type" <+> quotes (ppr ty)) k tys 1509 1510---------------- 1511lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind 1512lint_co_app ty k tys 1513 = lint_app (text "coercion" <+> quotes (ppr ty)) k tys 1514 1515---------------- 1516lintTyLit :: TyLit -> LintM () 1517lintTyLit (NumTyLit n) 1518 | n >= 0 = return () 1519 | otherwise = failWithL msg 1520 where msg = text "Negative type literal:" <+> integer n 1521lintTyLit (StrTyLit _) = return () 1522 1523lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind 1524-- (lint_app d fun_kind arg_tys) 1525-- We have an application (f arg_ty1 .. arg_tyn), 1526-- where f :: fun_kind 1527-- Takes care of linting the OutTypes 1528 1529-- If you edit this function, you may need to update the GHC formalism 1530-- See Note [GHC Formalism] 1531lint_app doc kfn kas 1532 = do { in_scope <- getInScope 1533 -- We need the in_scope set to satisfy the invariant in 1534 -- Note [The substitution invariant] in TyCoSubst 1535 ; foldlM (go_app in_scope) kfn kas } 1536 where 1537 fail_msg extra = vcat [ hang (text "Kind application error in") 2 doc 1538 , nest 2 (text "Function kind =" <+> ppr kfn) 1539 , nest 2 (text "Arg kinds =" <+> ppr kas) 1540 , extra ] 1541 1542 go_app in_scope kfn tka 1543 | Just kfn' <- coreView kfn 1544 = go_app in_scope kfn' tka 1545 1546 go_app _ (FunTy _ kfa kfb) tka@(_,ka) 1547 = do { unless (ka `eqType` kfa) $ 1548 addErrL (fail_msg (text "Fun:" <+> (ppr kfa $$ ppr tka))) 1549 ; return kfb } 1550 1551 go_app in_scope (ForAllTy (Bndr kv _vis) kfn) tka@(ta,ka) 1552 = do { let kv_kind = varType kv 1553 ; unless (ka `eqType` kv_kind) $ 1554 addErrL (fail_msg (text "Forall:" <+> (ppr kv $$ ppr kv_kind $$ ppr tka))) 1555 ; return $ substTy (extendTCvSubst (mkEmptyTCvSubst in_scope) kv ta) kfn } 1556 1557 go_app _ kfn ka 1558 = failWithL (fail_msg (text "Not a fun:" <+> (ppr kfn $$ ppr ka))) 1559 1560{- ********************************************************************* 1561* * 1562 Linting rules 1563* * 1564********************************************************************* -} 1565 1566lintCoreRule :: OutVar -> OutType -> CoreRule -> LintM () 1567lintCoreRule _ _ (BuiltinRule {}) 1568 = return () -- Don't bother 1569 1570lintCoreRule fun fun_ty rule@(Rule { ru_name = name, ru_bndrs = bndrs 1571 , ru_args = args, ru_rhs = rhs }) 1572 = lintBinders LambdaBind bndrs $ \ _ -> 1573 do { lhs_ty <- lintCoreArgs fun_ty args 1574 ; rhs_ty <- case isJoinId_maybe fun of 1575 Just join_arity 1576 -> do { checkL (args `lengthIs` join_arity) $ 1577 mkBadJoinPointRuleMsg fun join_arity rule 1578 -- See Note [Rules for join points] 1579 ; lintCoreExpr rhs } 1580 _ -> markAllJoinsBad $ lintCoreExpr rhs 1581 ; ensureEqTys lhs_ty rhs_ty $ 1582 (rule_doc <+> vcat [ text "lhs type:" <+> ppr lhs_ty 1583 , text "rhs type:" <+> ppr rhs_ty 1584 , text "fun_ty:" <+> ppr fun_ty ]) 1585 ; let bad_bndrs = filter is_bad_bndr bndrs 1586 1587 ; checkL (null bad_bndrs) 1588 (rule_doc <+> text "unbound" <+> ppr bad_bndrs) 1589 -- See Note [Linting rules] 1590 } 1591 where 1592 rule_doc = text "Rule" <+> doubleQuotes (ftext name) <> colon 1593 1594 lhs_fvs = exprsFreeVars args 1595 rhs_fvs = exprFreeVars rhs 1596 1597 is_bad_bndr :: Var -> Bool 1598 -- See Note [Unbound RULE binders] in Rules 1599 is_bad_bndr bndr = not (bndr `elemVarSet` lhs_fvs) 1600 && bndr `elemVarSet` rhs_fvs 1601 && isNothing (isReflCoVar_maybe bndr) 1602 1603 1604{- Note [Linting rules] 1605~~~~~~~~~~~~~~~~~~~~~~~ 1606It's very bad if simplifying a rule means that one of the template 1607variables (ru_bndrs) that /is/ mentioned on the RHS becomes 1608not-mentioned in the LHS (ru_args). How can that happen? Well, in 1609#10602, SpecConstr stupidly constructed a rule like 1610 1611 forall x,c1,c2. 1612 f (x |> c1 |> c2) = .... 1613 1614But simplExpr collapses those coercions into one. (Indeed in 1615#10602, it collapsed to the identity and was removed altogether.) 1616 1617We don't have a great story for what to do here, but at least 1618this check will nail it. 1619 1620NB (#11643): it's possible that a variable listed in the 1621binders becomes not-mentioned on both LHS and RHS. Here's a silly 1622example: 1623 RULE forall x y. f (g x y) = g (x+1) (y-1) 1624And suppose worker/wrapper decides that 'x' is Absent. Then 1625we'll end up with 1626 RULE forall x y. f ($gw y) = $gw (x+1) 1627This seems sufficiently obscure that there isn't enough payoff to 1628try to trim the forall'd binder list. 1629 1630Note [Rules for join points] 1631~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1632 1633A join point cannot be partially applied. However, the left-hand side of a rule 1634for a join point is effectively a *pattern*, not a piece of code, so there's an 1635argument to be made for allowing a situation like this: 1636 1637 join $sj :: Int -> Int -> String 1638 $sj n m = ... 1639 j :: forall a. Eq a => a -> a -> String 1640 {-# RULES "SPEC j" jump j @ Int $dEq = jump $sj #-} 1641 j @a $dEq x y = ... 1642 1643Applying this rule can't turn a well-typed program into an ill-typed one, so 1644conceivably we could allow it. But we can always eta-expand such an 1645"undersaturated" rule (see 'CoreArity.etaExpandToJoinPointRule'), and in fact 1646the simplifier would have to in order to deal with the RHS. So we take a 1647conservative view and don't allow undersaturated rules for join points. See 1648Note [Rules and join points] in OccurAnal for further discussion. 1649-} 1650 1651{- 1652************************************************************************ 1653* * 1654 Linting coercions 1655* * 1656************************************************************************ 1657-} 1658 1659lintInCo :: InCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role) 1660-- Check the coercion, and apply the substitution to it 1661-- See Note [Linting type lets] 1662lintInCo co 1663 = addLoc (InCo co) $ 1664 do { co' <- applySubstCo co 1665 ; lintCoercion co' } 1666 1667-- lints a coercion, confirming that its lh kind and its rh kind are both * 1668-- also ensures that the role is Nominal 1669lintStarCoercion :: OutCoercion -> LintM (LintedType, LintedType) 1670lintStarCoercion g 1671 = do { (k1, k2, t1, t2, r) <- lintCoercion g 1672 ; checkValueKind k1 (text "the kind of the left type in" <+> ppr g) 1673 ; checkValueKind k2 (text "the kind of the right type in" <+> ppr g) 1674 ; lintRole g Nominal r 1675 ; return (t1, t2) } 1676 1677lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role) 1678-- Check the kind of a coercion term, returning the kind 1679-- Post-condition: the returned OutTypes are lint-free 1680-- 1681-- If lintCoercion co = (k1, k2, s1, s2, r) 1682-- then co :: s1 ~r s2 1683-- s1 :: k1 1684-- s2 :: k2 1685 1686-- If you edit this function, you may need to update the GHC formalism 1687-- See Note [GHC Formalism] 1688lintCoercion (Refl ty) 1689 = do { k <- lintType ty 1690 ; return (k, k, ty, ty, Nominal) } 1691 1692lintCoercion (GRefl r ty MRefl) 1693 = do { k <- lintType ty 1694 ; return (k, k, ty, ty, r) } 1695 1696lintCoercion (GRefl r ty (MCo co)) 1697 = do { k <- lintType ty 1698 ; (_, _, k1, k2, r') <- lintCoercion co 1699 ; ensureEqTys k k1 1700 (hang (text "GRefl coercion kind mis-match:" <+> ppr co) 1701 2 (vcat [ppr ty, ppr k, ppr k1])) 1702 ; lintRole co Nominal r' 1703 ; return (k1, k2, ty, mkCastTy ty co, r) } 1704 1705lintCoercion co@(TyConAppCo r tc cos) 1706 | tc `hasKey` funTyConKey 1707 , [_rep1,_rep2,_co1,_co2] <- cos 1708 = do { failWithL (text "Saturated TyConAppCo (->):" <+> ppr co) 1709 } -- All saturated TyConAppCos should be FunCos 1710 1711 | Just {} <- synTyConDefn_maybe tc 1712 = failWithL (text "Synonym in TyConAppCo:" <+> ppr co) 1713 1714 | otherwise 1715 = do { checkTyCon tc 1716 ; (k's, ks, ss, ts, rs) <- mapAndUnzip5M lintCoercion cos 1717 ; k' <- lint_co_app co (tyConKind tc) (ss `zip` k's) 1718 ; k <- lint_co_app co (tyConKind tc) (ts `zip` ks) 1719 ; _ <- zipWith3M lintRole cos (tyConRolesX r tc) rs 1720 ; return (k', k, mkTyConApp tc ss, mkTyConApp tc ts, r) } 1721 1722lintCoercion co@(AppCo co1 co2) 1723 | TyConAppCo {} <- co1 1724 = failWithL (text "TyConAppCo to the left of AppCo:" <+> ppr co) 1725 | Just (TyConApp {}, _) <- isReflCo_maybe co1 1726 = failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co) 1727 | otherwise 1728 = do { (k1, k2, s1, s2, r1) <- lintCoercion co1 1729 ; (k'1, k'2, t1, t2, r2) <- lintCoercion co2 1730 ; k3 <- lint_co_app co k1 [(t1,k'1)] 1731 ; k4 <- lint_co_app co k2 [(t2,k'2)] 1732 ; if r1 == Phantom 1733 then lintL (r2 == Phantom || r2 == Nominal) 1734 (text "Second argument in AppCo cannot be R:" $$ 1735 ppr co) 1736 else lintRole co Nominal r2 1737 ; return (k3, k4, mkAppTy s1 t1, mkAppTy s2 t2, r1) } 1738 1739---------- 1740lintCoercion (ForAllCo tv1 kind_co co) 1741 -- forall over types 1742 | isTyVar tv1 1743 = do { (_, k2) <- lintStarCoercion kind_co 1744 ; let tv2 = setTyVarKind tv1 k2 1745 ; addInScopeVar tv1 $ 1746 do { 1747 ; (k3, k4, t1, t2, r) <- lintCoercion co 1748 ; in_scope <- getInScope 1749 ; let tyl = mkInvForAllTy tv1 t1 1750 subst = mkTvSubst in_scope $ 1751 -- We need both the free vars of the `t2` and the 1752 -- free vars of the range of the substitution in 1753 -- scope. All the free vars of `t2` and `kind_co` should 1754 -- already be in `in_scope`, because they've been 1755 -- linted and `tv2` has the same unique as `tv1`. 1756 -- See Note [The substitution invariant] in TyCoSubst. 1757 unitVarEnv tv1 (TyVarTy tv2 `mkCastTy` mkSymCo kind_co) 1758 tyr = mkInvForAllTy tv2 $ 1759 substTy subst t2 1760 ; return (k3, k4, tyl, tyr, r) } } 1761 1762lintCoercion (ForAllCo cv1 kind_co co) 1763 -- forall over coercions 1764 = ASSERT( isCoVar cv1 ) 1765 do { lintL (almostDevoidCoVarOfCo cv1 co) 1766 (text "Covar can only appear in Refl and GRefl: " <+> ppr co) 1767 ; (_, k2) <- lintStarCoercion kind_co 1768 ; let cv2 = setVarType cv1 k2 1769 ; addInScopeVar cv1 $ 1770 do { 1771 ; (k3, k4, t1, t2, r) <- lintCoercion co 1772 ; checkValueKind k3 (text "the body of a ForAllCo over covar:" <+> ppr co) 1773 ; checkValueKind k4 (text "the body of a ForAllCo over covar:" <+> ppr co) 1774 -- See Note [Weird typing rule for ForAllTy] in Type 1775 ; in_scope <- getInScope 1776 ; let tyl = mkTyCoInvForAllTy cv1 t1 1777 r2 = coVarRole cv1 1778 kind_co' = downgradeRole r2 Nominal kind_co 1779 eta1 = mkNthCo r2 2 kind_co' 1780 eta2 = mkNthCo r2 3 kind_co' 1781 subst = mkCvSubst in_scope $ 1782 -- We need both the free vars of the `t2` and the 1783 -- free vars of the range of the substitution in 1784 -- scope. All the free vars of `t2` and `kind_co` should 1785 -- already be in `in_scope`, because they've been 1786 -- linted and `cv2` has the same unique as `cv1`. 1787 -- See Note [The substitution invariant] in TyCoSubst. 1788 unitVarEnv cv1 (eta1 `mkTransCo` (mkCoVarCo cv2) 1789 `mkTransCo` (mkSymCo eta2)) 1790 tyr = mkTyCoInvForAllTy cv2 $ 1791 substTy subst t2 1792 ; return (liftedTypeKind, liftedTypeKind, tyl, tyr, r) } } 1793 -- See Note [Weird typing rule for ForAllTy] in Type 1794 1795lintCoercion co@(FunCo r co1 co2) 1796 = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1 1797 ; (k2,k'2,s2,t2,r2) <- lintCoercion co2 1798 ; k <- lintArrow (text "coercion" <+> quotes (ppr co)) k1 k2 1799 ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2 1800 ; lintRole co1 r r1 1801 ; lintRole co2 r r2 1802 ; return (k, k', mkVisFunTy s1 s2, mkVisFunTy t1 t2, r) } 1803 1804lintCoercion (CoVarCo cv) 1805 | not (isCoVar cv) 1806 = failWithL (hang (text "Bad CoVarCo:" <+> ppr cv) 1807 2 (text "With offending type:" <+> ppr (varType cv))) 1808 | otherwise 1809 = do { lintTyCoVarInScope cv 1810 ; cv' <- lookupIdInScope cv 1811 ; lintUnliftedCoVar cv 1812 ; return $ coVarKindsTypesRole cv' } 1813 1814-- See Note [Bad unsafe coercion] 1815lintCoercion co@(UnivCo prov r ty1 ty2) 1816 = do { k1 <- lintType ty1 1817 ; k2 <- lintType ty2 1818 ; case prov of 1819 UnsafeCoerceProv -> return () -- no extra checks 1820 1821 PhantomProv kco -> do { lintRole co Phantom r 1822 ; check_kinds kco k1 k2 } 1823 1824 ProofIrrelProv kco -> do { lintL (isCoercionTy ty1) $ 1825 mkBadProofIrrelMsg ty1 co 1826 ; lintL (isCoercionTy ty2) $ 1827 mkBadProofIrrelMsg ty2 co 1828 ; check_kinds kco k1 k2 } 1829 1830 PluginProv _ -> return () -- no extra checks 1831 1832 ; when (r /= Phantom && classifiesTypeWithValues k1 1833 && classifiesTypeWithValues k2) 1834 (checkTypes ty1 ty2) 1835 ; return (k1, k2, ty1, ty2, r) } 1836 where 1837 report s = hang (text $ "Unsafe coercion: " ++ s) 1838 2 (vcat [ text "From:" <+> ppr ty1 1839 , text " To:" <+> ppr ty2]) 1840 isUnBoxed :: PrimRep -> Bool 1841 isUnBoxed = not . isGcPtrRep 1842 1843 -- see #9122 for discussion of these checks 1844 checkTypes t1 t2 1845 = do { checkWarnL (not lev_poly1) 1846 (report "left-hand type is levity-polymorphic") 1847 ; checkWarnL (not lev_poly2) 1848 (report "right-hand type is levity-polymorphic") 1849 ; when (not (lev_poly1 || lev_poly2)) $ 1850 do { checkWarnL (reps1 `equalLength` reps2) 1851 (report "between values with different # of reps") 1852 ; zipWithM_ validateCoercion reps1 reps2 }} 1853 where 1854 lev_poly1 = isTypeLevPoly t1 1855 lev_poly2 = isTypeLevPoly t2 1856 1857 -- don't look at these unless lev_poly1/2 are False 1858 -- Otherwise, we get #13458 1859 reps1 = typePrimRep t1 1860 reps2 = typePrimRep t2 1861 1862 validateCoercion :: PrimRep -> PrimRep -> LintM () 1863 validateCoercion rep1 rep2 1864 = do { dflags <- getDynFlags 1865 ; checkWarnL (isUnBoxed rep1 == isUnBoxed rep2) 1866 (report "between unboxed and boxed value") 1867 ; checkWarnL (TyCon.primRepSizeB dflags rep1 1868 == TyCon.primRepSizeB dflags rep2) 1869 (report "between unboxed values of different size") 1870 ; let fl = liftM2 (==) (TyCon.primRepIsFloat rep1) 1871 (TyCon.primRepIsFloat rep2) 1872 ; case fl of 1873 Nothing -> addWarnL (report "between vector types") 1874 Just False -> addWarnL (report "between float and integral values") 1875 _ -> return () 1876 } 1877 1878 check_kinds kco k1 k2 = do { (k1', k2') <- lintStarCoercion kco 1879 ; ensureEqTys k1 k1' (mkBadUnivCoMsg CLeft co) 1880 ; ensureEqTys k2 k2' (mkBadUnivCoMsg CRight co) } 1881 1882 1883lintCoercion (SymCo co) 1884 = do { (k1, k2, ty1, ty2, r) <- lintCoercion co 1885 ; return (k2, k1, ty2, ty1, r) } 1886 1887lintCoercion co@(TransCo co1 co2) 1888 = do { (k1a, _k1b, ty1a, ty1b, r1) <- lintCoercion co1 1889 ; (_k2a, k2b, ty2a, ty2b, r2) <- lintCoercion co2 1890 ; ensureEqTys ty1b ty2a 1891 (hang (text "Trans coercion mis-match:" <+> ppr co) 1892 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b])) 1893 ; lintRole co r1 r2 1894 ; return (k1a, k2b, ty1a, ty2b, r1) } 1895 1896lintCoercion the_co@(NthCo r0 n co) 1897 = do { (_, _, s, t, r) <- lintCoercion co 1898 ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of 1899 { (Just (tcv_s, _ty_s), Just (tcv_t, _ty_t)) 1900 -- works for both tyvar and covar 1901 | n == 0 1902 , (isForAllTy_ty s && isForAllTy_ty t) 1903 || (isForAllTy_co s && isForAllTy_co t) 1904 -> do { lintRole the_co Nominal r0 1905 ; return (ks, kt, ts, tt, r0) } 1906 where 1907 ts = varType tcv_s 1908 tt = varType tcv_t 1909 ks = typeKind ts 1910 kt = typeKind tt 1911 1912 ; _ -> case (splitTyConApp_maybe s, splitTyConApp_maybe t) of 1913 { (Just (tc_s, tys_s), Just (tc_t, tys_t)) 1914 | tc_s == tc_t 1915 , isInjectiveTyCon tc_s r 1916 -- see Note [NthCo and newtypes] in TyCoRep 1917 , tys_s `equalLength` tys_t 1918 , tys_s `lengthExceeds` n 1919 -> do { lintRole the_co tr r0 1920 ; return (ks, kt, ts, tt, r0) } 1921 where 1922 ts = getNth tys_s n 1923 tt = getNth tys_t n 1924 tr = nthRole r tc_s n 1925 ks = typeKind ts 1926 kt = typeKind tt 1927 1928 ; _ -> failWithL (hang (text "Bad getNth:") 1929 2 (ppr the_co $$ ppr s $$ ppr t)) }}} 1930 1931lintCoercion the_co@(LRCo lr co) 1932 = do { (_,_,s,t,r) <- lintCoercion co 1933 ; lintRole co Nominal r 1934 ; case (splitAppTy_maybe s, splitAppTy_maybe t) of 1935 (Just s_pr, Just t_pr) 1936 -> return (ks_pick, kt_pick, s_pick, t_pick, Nominal) 1937 where 1938 s_pick = pickLR lr s_pr 1939 t_pick = pickLR lr t_pr 1940 ks_pick = typeKind s_pick 1941 kt_pick = typeKind t_pick 1942 1943 _ -> failWithL (hang (text "Bad LRCo:") 1944 2 (ppr the_co $$ ppr s $$ ppr t)) } 1945 1946lintCoercion (InstCo co arg) 1947 = do { (k3, k4, t1',t2', r) <- lintCoercion co 1948 ; (k1',k2',s1,s2, r') <- lintCoercion arg 1949 ; lintRole arg Nominal r' 1950 ; in_scope <- getInScope 1951 ; case (splitForAllTy_ty_maybe t1', splitForAllTy_ty_maybe t2') of 1952 -- forall over tvar 1953 { (Just (tv1,t1), Just (tv2,t2)) 1954 | k1' `eqType` tyVarKind tv1 1955 , k2' `eqType` tyVarKind tv2 1956 -> return (k3, k4, 1957 substTyWithInScope in_scope [tv1] [s1] t1, 1958 substTyWithInScope in_scope [tv2] [s2] t2, r) 1959 | otherwise 1960 -> failWithL (text "Kind mis-match in inst coercion") 1961 ; _ -> case (splitForAllTy_co_maybe t1', splitForAllTy_co_maybe t2') of 1962 -- forall over covar 1963 { (Just (cv1, t1), Just (cv2, t2)) 1964 | k1' `eqType` varType cv1 1965 , k2' `eqType` varType cv2 1966 , CoercionTy s1' <- s1 1967 , CoercionTy s2' <- s2 1968 -> do { return $ 1969 (liftedTypeKind, liftedTypeKind 1970 -- See Note [Weird typing rule for ForAllTy] in Type 1971 , substTy (mkCvSubst in_scope $ unitVarEnv cv1 s1') t1 1972 , substTy (mkCvSubst in_scope $ unitVarEnv cv2 s2') t2 1973 , r) } 1974 | otherwise 1975 -> failWithL (text "Kind mis-match in inst coercion") 1976 ; _ -> failWithL (text "Bad argument of inst") }}} 1977 1978lintCoercion co@(AxiomInstCo con ind cos) 1979 = do { unless (0 <= ind && ind < numBranches (coAxiomBranches con)) 1980 (bad_ax (text "index out of range")) 1981 ; let CoAxBranch { cab_tvs = ktvs 1982 , cab_cvs = cvs 1983 , cab_roles = roles 1984 , cab_lhs = lhs 1985 , cab_rhs = rhs } = coAxiomNthBranch con ind 1986 ; unless (cos `equalLength` (ktvs ++ cvs)) $ 1987 bad_ax (text "lengths") 1988 ; subst <- getTCvSubst 1989 ; let empty_subst = zapTCvSubst subst 1990 ; (subst_l, subst_r) <- foldlM check_ki 1991 (empty_subst, empty_subst) 1992 (zip3 (ktvs ++ cvs) roles cos) 1993 ; let lhs' = substTys subst_l lhs 1994 rhs' = substTy subst_r rhs 1995 fam_tc = coAxiomTyCon con 1996 ; case checkAxInstCo co of 1997 Just bad_branch -> bad_ax $ text "inconsistent with" <+> 1998 pprCoAxBranch fam_tc bad_branch 1999 Nothing -> return () 2000 ; let s2 = mkTyConApp fam_tc lhs' 2001 ; return (typeKind s2, typeKind rhs', s2, rhs', coAxiomRole con) } 2002 where 2003 bad_ax what = addErrL (hang (text "Bad axiom application" <+> parens what) 2004 2 (ppr co)) 2005 2006 check_ki (subst_l, subst_r) (ktv, role, arg) 2007 = do { (k', k'', s', t', r) <- lintCoercion arg 2008 ; lintRole arg role r 2009 ; let ktv_kind_l = substTy subst_l (tyVarKind ktv) 2010 ktv_kind_r = substTy subst_r (tyVarKind ktv) 2011 ; unless (k' `eqType` ktv_kind_l) 2012 (bad_ax (text "check_ki1" <+> vcat [ ppr co, ppr k', ppr ktv, ppr ktv_kind_l ] )) 2013 ; unless (k'' `eqType` ktv_kind_r) 2014 (bad_ax (text "check_ki2" <+> vcat [ ppr co, ppr k'', ppr ktv, ppr ktv_kind_r ] )) 2015 ; return (extendTCvSubst subst_l ktv s', 2016 extendTCvSubst subst_r ktv t') } 2017 2018lintCoercion (KindCo co) 2019 = do { (k1, k2, _, _, _) <- lintCoercion co 2020 ; return (liftedTypeKind, liftedTypeKind, k1, k2, Nominal) } 2021 2022lintCoercion (SubCo co') 2023 = do { (k1,k2,s,t,r) <- lintCoercion co' 2024 ; lintRole co' Nominal r 2025 ; return (k1,k2,s,t,Representational) } 2026 2027lintCoercion this@(AxiomRuleCo co cs) 2028 = do { eqs <- mapM lintCoercion cs 2029 ; lintRoles 0 (coaxrAsmpRoles co) eqs 2030 ; case coaxrProves co [ Pair l r | (_,_,l,r,_) <- eqs ] of 2031 Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ] 2032 Just (Pair l r) -> 2033 return (typeKind l, typeKind r, l, r, coaxrRole co) } 2034 where 2035 err m xs = failWithL $ 2036 hang (text m) 2 $ vcat (text "Rule:" <+> ppr (coaxrName co) : xs) 2037 2038 lintRoles n (e : es) ((_,_,_,_,r) : rs) 2039 | e == r = lintRoles (n+1) es rs 2040 | otherwise = err "Argument roles mismatch" 2041 [ text "In argument:" <+> int (n+1) 2042 , text "Expected:" <+> ppr e 2043 , text "Found:" <+> ppr r ] 2044 lintRoles _ [] [] = return () 2045 lintRoles n [] rs = err "Too many coercion arguments" 2046 [ text "Expected:" <+> int n 2047 , text "Provided:" <+> int (n + length rs) ] 2048 2049 lintRoles n es [] = err "Not enough coercion arguments" 2050 [ text "Expected:" <+> int (n + length es) 2051 , text "Provided:" <+> int n ] 2052 2053lintCoercion (HoleCo h) 2054 = do { addErrL $ text "Unfilled coercion hole:" <+> ppr h 2055 ; lintCoercion (CoVarCo (coHoleCoVar h)) } 2056 2057 2058---------- 2059lintUnliftedCoVar :: CoVar -> LintM () 2060lintUnliftedCoVar cv 2061 = when (not (isUnliftedType (coVarKind cv))) $ 2062 failWithL (text "Bad lifted equality:" <+> ppr cv 2063 <+> dcolon <+> ppr (coVarKind cv)) 2064 2065{- 2066************************************************************************ 2067* * 2068\subsection[lint-monad]{The Lint monad} 2069* * 2070************************************************************************ 2071-} 2072 2073-- If you edit this type, you may need to update the GHC formalism 2074-- See Note [GHC Formalism] 2075data LintEnv 2076 = LE { le_flags :: LintFlags -- Linting the result of this pass 2077 , le_loc :: [LintLocInfo] -- Locations 2078 2079 , le_subst :: TCvSubst -- Current type substitution 2080 -- We also use le_subst to keep track of 2081 -- /all variables/ in scope, both Ids and TyVars 2082 2083 , le_joins :: IdSet -- Join points in scope that are valid 2084 -- A subset of the InScopeSet in le_subst 2085 -- See Note [Join points] 2086 2087 , le_dynflags :: DynFlags -- DynamicFlags 2088 } 2089 2090data LintFlags 2091 = LF { lf_check_global_ids :: Bool -- See Note [Checking for global Ids] 2092 , lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers] 2093 , lf_check_static_ptrs :: StaticPtrCheck -- ^ See Note [Checking StaticPtrs] 2094 , lf_report_unsat_syns :: Bool -- ^ See Note [Linting type synonym applications] 2095 } 2096 2097-- See Note [Checking StaticPtrs] 2098data StaticPtrCheck 2099 = AllowAnywhere 2100 -- ^ Allow 'makeStatic' to occur anywhere. 2101 | AllowAtTopLevel 2102 -- ^ Allow 'makeStatic' calls at the top-level only. 2103 | RejectEverywhere 2104 -- ^ Reject any 'makeStatic' occurrence. 2105 deriving Eq 2106 2107defaultLintFlags :: LintFlags 2108defaultLintFlags = LF { lf_check_global_ids = False 2109 , lf_check_inline_loop_breakers = True 2110 , lf_check_static_ptrs = AllowAnywhere 2111 , lf_report_unsat_syns = True 2112 } 2113 2114newtype LintM a = 2115 LintM { unLintM :: 2116 LintEnv -> 2117 WarnsAndErrs -> -- Warning and error messages so far 2118 (Maybe a, WarnsAndErrs) } -- Result and messages (if any) 2119 deriving (Functor) 2120 2121type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc) 2122 2123{- Note [Checking for global Ids] 2124~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2125Before CoreTidy, all locally-bound Ids must be LocalIds, even 2126top-level ones. See Note [Exported LocalIds] and #9857. 2127 2128Note [Checking StaticPtrs] 2129~~~~~~~~~~~~~~~~~~~~~~~~~~ 2130See Note [Grand plan for static forms] in StaticPtrTable for an overview. 2131 2132Every occurrence of the function 'makeStatic' should be moved to the 2133top level by the FloatOut pass. It's vital that we don't have nested 2134'makeStatic' occurrences after CorePrep, because we populate the Static 2135Pointer Table from the top-level bindings. See SimplCore Note [Grand 2136plan for static forms]. 2137 2138The linter checks that no occurrence is left behind, nested within an 2139expression. The check is enabled only after the FloatOut, CorePrep, 2140and CoreTidy passes and only if the module uses the StaticPointers 2141language extension. Checking more often doesn't help since the condition 2142doesn't hold until after the first FloatOut pass. 2143 2144Note [Type substitution] 2145~~~~~~~~~~~~~~~~~~~~~~~~ 2146Why do we need a type substitution? Consider 2147 /\(a:*). \(x:a). /\(a:*). id a x 2148This is ill typed, because (renaming variables) it is really 2149 /\(a:*). \(x:a). /\(b:*). id b x 2150Hence, when checking an application, we can't naively compare x's type 2151(at its binding site) with its expected type (at a use site). So we 2152rename type binders as we go, maintaining a substitution. 2153 2154The same substitution also supports let-type, current expressed as 2155 (/\(a:*). body) ty 2156Here we substitute 'ty' for 'a' in 'body', on the fly. 2157 2158Note [Linting type synonym applications] 2159~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2160When linting a type-synonym, or type-family, application 2161 S ty1 .. tyn 2162we behave as follows (#15057, #T15664): 2163 2164* If lf_report_unsat_syns = True, and S has arity < n, 2165 complain about an unsaturated type synonym or type family 2166 2167* Switch off lf_report_unsat_syns, and lint ty1 .. tyn. 2168 2169 Reason: catch out of scope variables or other ill-kinded gubbins, 2170 even if S discards that argument entirely. E.g. (#15012): 2171 type FakeOut a = Int 2172 type family TF a 2173 type instance TF Int = FakeOut a 2174 Here 'a' is out of scope; but if we expand FakeOut, we conceal 2175 that out-of-scope error. 2176 2177 Reason for switching off lf_report_unsat_syns: with 2178 LiberalTypeSynonyms, GHC allows unsaturated synonyms provided they 2179 are saturated when the type is expanded. Example 2180 type T f = f Int 2181 type S a = a -> a 2182 type Z = T S 2183 In Z's RHS, S appears unsaturated, but it is saturated when T is expanded. 2184 2185* If lf_report_unsat_syns is on, expand the synonym application and 2186 lint the result. Reason: want to check that synonyms are saturated 2187 when the type is expanded. 2188-} 2189 2190instance Applicative LintM where 2191 pure x = LintM $ \ _ errs -> (Just x, errs) 2192 (<*>) = ap 2193 2194instance Monad LintM where 2195#if !MIN_VERSION_base(4,13,0) 2196 fail = MonadFail.fail 2197#endif 2198 m >>= k = LintM (\ env errs -> 2199 let (res, errs') = unLintM m env errs in 2200 case res of 2201 Just r -> unLintM (k r) env errs' 2202 Nothing -> (Nothing, errs')) 2203 2204instance MonadFail.MonadFail LintM where 2205 fail err = failWithL (text err) 2206 2207instance HasDynFlags LintM where 2208 getDynFlags = LintM (\ e errs -> (Just (le_dynflags e), errs)) 2209 2210data LintLocInfo 2211 = RhsOf Id -- The variable bound 2212 | LambdaBodyOf Id -- The lambda-binder 2213 | UnfoldingOf Id -- Unfolding of a binder 2214 | BodyOfLetRec [Id] -- One of the binders 2215 | CaseAlt CoreAlt -- Case alternative 2216 | CasePat CoreAlt -- The *pattern* of the case alternative 2217 | CaseTy CoreExpr -- The type field of a case expression 2218 -- with this scrutinee 2219 | IdTy Id -- The type field of an Id binder 2220 | AnExpr CoreExpr -- Some expression 2221 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which) 2222 | TopLevelBindings 2223 | InType Type -- Inside a type 2224 | InCo Coercion -- Inside a coercion 2225 2226initL :: DynFlags -> LintFlags -> InScopeSet 2227 -> LintM a -> WarnsAndErrs -- Warnings and errors 2228initL dflags flags in_scope m 2229 = case unLintM m env (emptyBag, emptyBag) of 2230 (Just _, errs) -> errs 2231 (Nothing, errs@(_, e)) | not (isEmptyBag e) -> errs 2232 | otherwise -> pprPanic ("Bug in Lint: a failure occurred " ++ 2233 "without reporting an error message") empty 2234 where 2235 env = LE { le_flags = flags 2236 , le_subst = mkEmptyTCvSubst in_scope 2237 , le_joins = emptyVarSet 2238 , le_loc = [] 2239 , le_dynflags = dflags } 2240 2241setReportUnsat :: Bool -> LintM a -> LintM a 2242-- Switch off lf_report_unsat_syns 2243setReportUnsat ru thing_inside 2244 = LintM $ \ env errs -> 2245 let env' = env { le_flags = (le_flags env) { lf_report_unsat_syns = ru } } 2246 in unLintM thing_inside env' errs 2247 2248getLintFlags :: LintM LintFlags 2249getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs) 2250 2251checkL :: Bool -> MsgDoc -> LintM () 2252checkL True _ = return () 2253checkL False msg = failWithL msg 2254 2255-- like checkL, but relevant to type checking 2256lintL :: Bool -> MsgDoc -> LintM () 2257lintL = checkL 2258 2259checkWarnL :: Bool -> MsgDoc -> LintM () 2260checkWarnL True _ = return () 2261checkWarnL False msg = addWarnL msg 2262 2263failWithL :: MsgDoc -> LintM a 2264failWithL msg = LintM $ \ env (warns,errs) -> 2265 (Nothing, (warns, addMsg True env errs msg)) 2266 2267addErrL :: MsgDoc -> LintM () 2268addErrL msg = LintM $ \ env (warns,errs) -> 2269 (Just (), (warns, addMsg True env errs msg)) 2270 2271addWarnL :: MsgDoc -> LintM () 2272addWarnL msg = LintM $ \ env (warns,errs) -> 2273 (Just (), (addMsg False env warns msg, errs)) 2274 2275addMsg :: Bool -> LintEnv -> Bag MsgDoc -> MsgDoc -> Bag MsgDoc 2276addMsg is_error env msgs msg 2277 = ASSERT( notNull loc_msgs ) 2278 msgs `snocBag` mk_msg msg 2279 where 2280 loc_msgs :: [(SrcLoc, SDoc)] -- Innermost first 2281 loc_msgs = map dumpLoc (le_loc env) 2282 2283 cxt_doc = vcat [ vcat $ reverse $ map snd loc_msgs 2284 , text "Substitution:" <+> ppr (le_subst env) ] 2285 context | is_error = cxt_doc 2286 | otherwise = whenPprDebug cxt_doc 2287 -- Print voluminous info for Lint errors 2288 -- but not for warnings 2289 2290 msg_span = case [ span | (loc,_) <- loc_msgs 2291 , let span = srcLocSpan loc 2292 , isGoodSrcSpan span ] of 2293 [] -> noSrcSpan 2294 (s:_) -> s 2295 mk_msg msg = mkLocMessage SevWarning msg_span 2296 (msg $$ context) 2297 2298addLoc :: LintLocInfo -> LintM a -> LintM a 2299addLoc extra_loc m 2300 = LintM $ \ env errs -> 2301 unLintM m (env { le_loc = extra_loc : le_loc env }) errs 2302 2303inCasePat :: LintM Bool -- A slight hack; see the unique call site 2304inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs) 2305 where 2306 is_case_pat (LE { le_loc = CasePat {} : _ }) = True 2307 is_case_pat _other = False 2308 2309addInScopeVar :: Var -> LintM a -> LintM a 2310addInScopeVar var m 2311 = LintM $ \ env errs -> 2312 unLintM m (env { le_subst = extendTCvInScope (le_subst env) var 2313 , le_joins = delVarSet (le_joins env) var 2314 }) errs 2315 2316extendSubstL :: TyVar -> Type -> LintM a -> LintM a 2317extendSubstL tv ty m 2318 = LintM $ \ env errs -> 2319 unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs 2320 2321updateTCvSubst :: TCvSubst -> LintM a -> LintM a 2322updateTCvSubst subst' m 2323 = LintM $ \ env errs -> unLintM m (env { le_subst = subst' }) errs 2324 2325markAllJoinsBad :: LintM a -> LintM a 2326markAllJoinsBad m 2327 = LintM $ \ env errs -> unLintM m (env { le_joins = emptyVarSet }) errs 2328 2329markAllJoinsBadIf :: Bool -> LintM a -> LintM a 2330markAllJoinsBadIf True m = markAllJoinsBad m 2331markAllJoinsBadIf False m = m 2332 2333addGoodJoins :: [Var] -> LintM a -> LintM a 2334addGoodJoins vars thing_inside 2335 = LintM $ \ env errs -> unLintM thing_inside (add_joins env) errs 2336 where 2337 add_joins env = env { le_joins = le_joins env `extendVarSetList` join_ids } 2338 join_ids = filter isJoinId vars 2339 2340getValidJoins :: LintM IdSet 2341getValidJoins = LintM (\ env errs -> (Just (le_joins env), errs)) 2342 2343getTCvSubst :: LintM TCvSubst 2344getTCvSubst = LintM (\ env errs -> (Just (le_subst env), errs)) 2345 2346getInScope :: LintM InScopeSet 2347getInScope = LintM (\ env errs -> (Just (getTCvInScope $ le_subst env), errs)) 2348 2349applySubstTy :: InType -> LintM OutType 2350applySubstTy ty = do { subst <- getTCvSubst; return (substTy subst ty) } 2351 2352applySubstCo :: InCoercion -> LintM OutCoercion 2353applySubstCo co = do { subst <- getTCvSubst; return (substCo subst co) } 2354 2355lookupIdInScope :: Id -> LintM Id 2356lookupIdInScope id_occ 2357 = do { subst <- getTCvSubst 2358 ; case lookupInScope (getTCvInScope subst) id_occ of 2359 Just id_bnd -> do { checkL (not (bad_global id_bnd)) global_in_scope 2360 ; return id_bnd } 2361 Nothing -> do { checkL (not is_local) local_out_of_scope 2362 ; return id_occ } } 2363 where 2364 is_local = mustHaveLocalBinding id_occ 2365 local_out_of_scope = text "Out of scope:" <+> pprBndr LetBind id_occ 2366 global_in_scope = hang (text "Occurrence is GlobalId, but binding is LocalId") 2367 2 (pprBndr LetBind id_occ) 2368 bad_global id_bnd = isGlobalId id_occ 2369 && isLocalId id_bnd 2370 && not (isWiredInName (idName id_occ)) 2371 -- 'bad_global' checks for the case where an /occurrence/ is 2372 -- a GlobalId, but there is an enclosing binding fora a LocalId. 2373 -- NB: the in-scope variables are mostly LocalIds, checked by lintIdBndr, 2374 -- but GHCi adds GlobalIds from the interactive context. These 2375 -- are fine; hence the test (isLocalId id == isLocalId v) 2376 -- NB: when compiling Control.Exception.Base, things like absentError 2377 -- are defined locally, but appear in expressions as (global) 2378 -- wired-in Ids after worker/wrapper 2379 -- So we simply disable the test in this case 2380 2381lookupJoinId :: Id -> LintM (Maybe JoinArity) 2382-- Look up an Id which should be a join point, valid here 2383-- If so, return its arity, if not return Nothing 2384lookupJoinId id 2385 = do { join_set <- getValidJoins 2386 ; case lookupVarSet join_set id of 2387 Just id' -> return (isJoinId_maybe id') 2388 Nothing -> return Nothing } 2389 2390lintTyCoVarInScope :: TyCoVar -> LintM () 2391lintTyCoVarInScope var 2392 = do { subst <- getTCvSubst 2393 ; lintL (var `isInScope` subst) 2394 (hang (text "The variable" <+> pprBndr LetBind var) 2395 2 (text "is out of scope")) } 2396 2397ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM () 2398-- check ty2 is subtype of ty1 (ie, has same structure but usage 2399-- annotations need only be consistent, not equal) 2400-- Assumes ty1,ty2 are have already had the substitution applied 2401ensureEqTys ty1 ty2 msg = lintL (ty1 `eqType` ty2) msg 2402 2403lintRole :: Outputable thing 2404 => thing -- where the role appeared 2405 -> Role -- expected 2406 -> Role -- actual 2407 -> LintM () 2408lintRole co r1 r2 2409 = lintL (r1 == r2) 2410 (text "Role incompatibility: expected" <+> ppr r1 <> comma <+> 2411 text "got" <+> ppr r2 $$ 2412 text "in" <+> ppr co) 2413 2414{- 2415************************************************************************ 2416* * 2417\subsection{Error messages} 2418* * 2419************************************************************************ 2420-} 2421 2422dumpLoc :: LintLocInfo -> (SrcLoc, SDoc) 2423 2424dumpLoc (RhsOf v) 2425 = (getSrcLoc v, text "In the RHS of" <+> pp_binders [v]) 2426 2427dumpLoc (LambdaBodyOf b) 2428 = (getSrcLoc b, text "In the body of lambda with binder" <+> pp_binder b) 2429 2430dumpLoc (UnfoldingOf b) 2431 = (getSrcLoc b, text "In the unfolding of" <+> pp_binder b) 2432 2433dumpLoc (BodyOfLetRec []) 2434 = (noSrcLoc, text "In body of a letrec with no binders") 2435 2436dumpLoc (BodyOfLetRec bs@(_:_)) 2437 = ( getSrcLoc (head bs), text "In the body of letrec with binders" <+> pp_binders bs) 2438 2439dumpLoc (AnExpr e) 2440 = (noSrcLoc, text "In the expression:" <+> ppr e) 2441 2442dumpLoc (CaseAlt (con, args, _)) 2443 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args)) 2444 2445dumpLoc (CasePat (con, args, _)) 2446 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args)) 2447 2448dumpLoc (CaseTy scrut) 2449 = (noSrcLoc, hang (text "In the result-type of a case with scrutinee:") 2450 2 (ppr scrut)) 2451 2452dumpLoc (IdTy b) 2453 = (getSrcLoc b, text "In the type of a binder:" <+> ppr b) 2454 2455dumpLoc (ImportedUnfolding locn) 2456 = (locn, text "In an imported unfolding") 2457dumpLoc TopLevelBindings 2458 = (noSrcLoc, Outputable.empty) 2459dumpLoc (InType ty) 2460 = (noSrcLoc, text "In the type" <+> quotes (ppr ty)) 2461dumpLoc (InCo co) 2462 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co)) 2463 2464pp_binders :: [Var] -> SDoc 2465pp_binders bs = sep (punctuate comma (map pp_binder bs)) 2466 2467pp_binder :: Var -> SDoc 2468pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)] 2469 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)] 2470 2471------------------------------------------------------ 2472-- Messages for case expressions 2473 2474mkDefaultArgsMsg :: [Var] -> MsgDoc 2475mkDefaultArgsMsg args 2476 = hang (text "DEFAULT case with binders") 2477 4 (ppr args) 2478 2479mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc 2480mkCaseAltMsg e ty1 ty2 2481 = hang (text "Type of case alternatives not the same as the annotation on case:") 2482 4 (vcat [ text "Actual type:" <+> ppr ty1, 2483 text "Annotation on case:" <+> ppr ty2, 2484 text "Alt Rhs:" <+> ppr e ]) 2485 2486mkScrutMsg :: Id -> Type -> Type -> TCvSubst -> MsgDoc 2487mkScrutMsg var var_ty scrut_ty subst 2488 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var, 2489 text "Result binder type:" <+> ppr var_ty,--(idType var), 2490 text "Scrutinee type:" <+> ppr scrut_ty, 2491 hsep [text "Current TCv subst", ppr subst]] 2492 2493mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc 2494mkNonDefltMsg e 2495 = hang (text "Case expression with DEFAULT not at the beginning") 4 (ppr e) 2496mkNonIncreasingAltsMsg e 2497 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e) 2498 2499nonExhaustiveAltsMsg :: CoreExpr -> MsgDoc 2500nonExhaustiveAltsMsg e 2501 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e) 2502 2503mkBadConMsg :: TyCon -> DataCon -> MsgDoc 2504mkBadConMsg tycon datacon 2505 = vcat [ 2506 text "In a case alternative, data constructor isn't in scrutinee type:", 2507 text "Scrutinee type constructor:" <+> ppr tycon, 2508 text "Data con:" <+> ppr datacon 2509 ] 2510 2511mkBadPatMsg :: Type -> Type -> MsgDoc 2512mkBadPatMsg con_result_ty scrut_ty 2513 = vcat [ 2514 text "In a case alternative, pattern result type doesn't match scrutinee type:", 2515 text "Pattern result type:" <+> ppr con_result_ty, 2516 text "Scrutinee type:" <+> ppr scrut_ty 2517 ] 2518 2519integerScrutinisedMsg :: MsgDoc 2520integerScrutinisedMsg 2521 = text "In a LitAlt, the literal is lifted (probably Integer)" 2522 2523mkBadAltMsg :: Type -> CoreAlt -> MsgDoc 2524mkBadAltMsg scrut_ty alt 2525 = vcat [ text "Data alternative when scrutinee is not a tycon application", 2526 text "Scrutinee type:" <+> ppr scrut_ty, 2527 text "Alternative:" <+> pprCoreAlt alt ] 2528 2529mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc 2530mkNewTyDataConAltMsg scrut_ty alt 2531 = vcat [ text "Data alternative for newtype datacon", 2532 text "Scrutinee type:" <+> ppr scrut_ty, 2533 text "Alternative:" <+> pprCoreAlt alt ] 2534 2535 2536------------------------------------------------------ 2537-- Other error messages 2538 2539mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc 2540mkAppMsg fun_ty arg_ty arg 2541 = vcat [text "Argument value doesn't match argument type:", 2542 hang (text "Fun type:") 4 (ppr fun_ty), 2543 hang (text "Arg type:") 4 (ppr arg_ty), 2544 hang (text "Arg:") 4 (ppr arg)] 2545 2546mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc 2547mkNonFunAppMsg fun_ty arg_ty arg 2548 = vcat [text "Non-function type in function position", 2549 hang (text "Fun type:") 4 (ppr fun_ty), 2550 hang (text "Arg type:") 4 (ppr arg_ty), 2551 hang (text "Arg:") 4 (ppr arg)] 2552 2553mkLetErr :: TyVar -> CoreExpr -> MsgDoc 2554mkLetErr bndr rhs 2555 = vcat [text "Bad `let' binding:", 2556 hang (text "Variable:") 2557 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)), 2558 hang (text "Rhs:") 2559 4 (ppr rhs)] 2560 2561mkTyAppMsg :: Type -> Type -> MsgDoc 2562mkTyAppMsg ty arg_ty 2563 = vcat [text "Illegal type application:", 2564 hang (text "Exp type:") 2565 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)), 2566 hang (text "Arg type:") 2567 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))] 2568 2569emptyRec :: CoreExpr -> MsgDoc 2570emptyRec e = hang (text "Empty Rec binding:") 2 (ppr e) 2571 2572mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc 2573mkRhsMsg binder what ty 2574 = vcat 2575 [hsep [text "The type of this binder doesn't match the type of its" <+> what <> colon, 2576 ppr binder], 2577 hsep [text "Binder's type:", ppr (idType binder)], 2578 hsep [text "Rhs type:", ppr ty]] 2579 2580mkLetAppMsg :: CoreExpr -> MsgDoc 2581mkLetAppMsg e 2582 = hang (text "This argument does not satisfy the let/app invariant:") 2583 2 (ppr e) 2584 2585badBndrTyMsg :: Id -> SDoc -> MsgDoc 2586badBndrTyMsg binder what 2587 = vcat [ text "The type of this binder is" <+> what <> colon <+> ppr binder 2588 , text "Binder's type:" <+> ppr (idType binder) ] 2589 2590mkStrictMsg :: Id -> MsgDoc 2591mkStrictMsg binder 2592 = vcat [hsep [text "Recursive or top-level binder has strict demand info:", 2593 ppr binder], 2594 hsep [text "Binder's demand info:", ppr (idDemandInfo binder)] 2595 ] 2596 2597mkNonTopExportedMsg :: Id -> MsgDoc 2598mkNonTopExportedMsg binder 2599 = hsep [text "Non-top-level binder is marked as exported:", ppr binder] 2600 2601mkNonTopExternalNameMsg :: Id -> MsgDoc 2602mkNonTopExternalNameMsg binder 2603 = hsep [text "Non-top-level binder has an external name:", ppr binder] 2604 2605mkTopNonLitStrMsg :: Id -> MsgDoc 2606mkTopNonLitStrMsg binder 2607 = hsep [text "Top-level Addr# binder has a non-literal rhs:", ppr binder] 2608 2609mkKindErrMsg :: TyVar -> Type -> MsgDoc 2610mkKindErrMsg tyvar arg_ty 2611 = vcat [text "Kinds don't match in type application:", 2612 hang (text "Type variable:") 2613 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)), 2614 hang (text "Arg type:") 2615 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))] 2616 2617mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> MsgDoc 2618mkCastErr expr = mk_cast_err "expression" "type" (ppr expr) 2619 2620mkCastTyErr :: Type -> Coercion -> Kind -> Kind -> MsgDoc 2621mkCastTyErr ty = mk_cast_err "type" "kind" (ppr ty) 2622 2623mk_cast_err :: String -- ^ What sort of casted thing this is 2624 -- (\"expression\" or \"type\"). 2625 -> String -- ^ What sort of coercion is being used 2626 -- (\"type\" or \"kind\"). 2627 -> SDoc -- ^ The thing being casted. 2628 -> Coercion -> Type -> Type -> MsgDoc 2629mk_cast_err thing_str co_str pp_thing co from_ty thing_ty 2630 = vcat [from_msg <+> text "of Cast differs from" <+> co_msg 2631 <+> text "of" <+> enclosed_msg, 2632 from_msg <> colon <+> ppr from_ty, 2633 text (capitalise co_str) <+> text "of" <+> enclosed_msg <> colon 2634 <+> ppr thing_ty, 2635 text "Actual" <+> enclosed_msg <> colon <+> pp_thing, 2636 text "Coercion used in cast:" <+> ppr co 2637 ] 2638 where 2639 co_msg, from_msg, enclosed_msg :: SDoc 2640 co_msg = text co_str 2641 from_msg = text "From-" <> co_msg 2642 enclosed_msg = text "enclosed" <+> text thing_str 2643 2644mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc 2645mkBadUnivCoMsg lr co 2646 = text "Kind mismatch on the" <+> pprLeftOrRight lr <+> 2647 text "side of a UnivCo:" <+> ppr co 2648 2649mkBadProofIrrelMsg :: Type -> Coercion -> SDoc 2650mkBadProofIrrelMsg ty co 2651 = hang (text "Found a non-coercion in a proof-irrelevance UnivCo:") 2652 2 (vcat [ text "type:" <+> ppr ty 2653 , text "co:" <+> ppr co ]) 2654 2655mkBadTyVarMsg :: Var -> SDoc 2656mkBadTyVarMsg tv 2657 = text "Non-tyvar used in TyVarTy:" 2658 <+> ppr tv <+> dcolon <+> ppr (varType tv) 2659 2660mkBadJoinBindMsg :: Var -> SDoc 2661mkBadJoinBindMsg var 2662 = vcat [ text "Bad join point binding:" <+> ppr var 2663 , text "Join points can be bound only by a non-top-level let" ] 2664 2665mkInvalidJoinPointMsg :: Var -> Type -> SDoc 2666mkInvalidJoinPointMsg var ty 2667 = hang (text "Join point has invalid type:") 2668 2 (ppr var <+> dcolon <+> ppr ty) 2669 2670mkBadJoinArityMsg :: Var -> Int -> Int -> CoreExpr -> SDoc 2671mkBadJoinArityMsg var ar nlams rhs 2672 = vcat [ text "Join point has too few lambdas", 2673 text "Join var:" <+> ppr var, 2674 text "Join arity:" <+> ppr ar, 2675 text "Number of lambdas:" <+> ppr nlams, 2676 text "Rhs = " <+> ppr rhs 2677 ] 2678 2679invalidJoinOcc :: Var -> SDoc 2680invalidJoinOcc var 2681 = vcat [ text "Invalid occurrence of a join variable:" <+> ppr var 2682 , text "The binder is either not a join point, or not valid here" ] 2683 2684mkBadJumpMsg :: Var -> Int -> Int -> SDoc 2685mkBadJumpMsg var ar nargs 2686 = vcat [ text "Join point invoked with wrong number of arguments", 2687 text "Join var:" <+> ppr var, 2688 text "Join arity:" <+> ppr ar, 2689 text "Number of arguments:" <+> int nargs ] 2690 2691mkInconsistentRecMsg :: [Var] -> SDoc 2692mkInconsistentRecMsg bndrs 2693 = vcat [ text "Recursive let binders mix values and join points", 2694 text "Binders:" <+> hsep (map ppr_with_details bndrs) ] 2695 where 2696 ppr_with_details bndr = ppr bndr <> ppr (idDetails bndr) 2697 2698mkJoinBndrOccMismatchMsg :: Var -> JoinArity -> JoinArity -> SDoc 2699mkJoinBndrOccMismatchMsg bndr join_arity_bndr join_arity_occ 2700 = vcat [ text "Mismatch in join point arity between binder and occurrence" 2701 , text "Var:" <+> ppr bndr 2702 , text "Arity at binding site:" <+> ppr join_arity_bndr 2703 , text "Arity at occurrence: " <+> ppr join_arity_occ ] 2704 2705mkBndrOccTypeMismatchMsg :: Var -> Var -> OutType -> OutType -> SDoc 2706mkBndrOccTypeMismatchMsg bndr var bndr_ty var_ty 2707 = vcat [ text "Mismatch in type between binder and occurrence" 2708 , text "Var:" <+> ppr bndr 2709 , text "Binder type:" <+> ppr bndr_ty 2710 , text "Occurrence type:" <+> ppr var_ty 2711 , text " Before subst:" <+> ppr (idType var) ] 2712 2713mkBadJoinPointRuleMsg :: JoinId -> JoinArity -> CoreRule -> SDoc 2714mkBadJoinPointRuleMsg bndr join_arity rule 2715 = vcat [ text "Join point has rule with wrong number of arguments" 2716 , text "Var:" <+> ppr bndr 2717 , text "Join arity:" <+> ppr join_arity 2718 , text "Rule:" <+> ppr rule ] 2719 2720pprLeftOrRight :: LeftOrRight -> MsgDoc 2721pprLeftOrRight CLeft = text "left" 2722pprLeftOrRight CRight = text "right" 2723 2724dupVars :: [NonEmpty Var] -> MsgDoc 2725dupVars vars 2726 = hang (text "Duplicate variables brought into scope") 2727 2 (ppr (map toList vars)) 2728 2729dupExtVars :: [NonEmpty Name] -> MsgDoc 2730dupExtVars vars 2731 = hang (text "Duplicate top-level variables with the same qualified name") 2732 2 (ppr (map toList vars)) 2733 2734{- 2735************************************************************************ 2736* * 2737\subsection{Annotation Linting} 2738* * 2739************************************************************************ 2740-} 2741 2742-- | This checks whether a pass correctly looks through debug 2743-- annotations (@SourceNote@). This works a bit different from other 2744-- consistency checks: We check this by running the given task twice, 2745-- noting all differences between the results. 2746lintAnnots :: SDoc -> (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts 2747lintAnnots pname pass guts = do 2748 -- Run the pass as we normally would 2749 dflags <- getDynFlags 2750 when (gopt Opt_DoAnnotationLinting dflags) $ 2751 liftIO $ Err.showPass dflags "Annotation linting - first run" 2752 nguts <- pass guts 2753 -- If appropriate re-run it without debug annotations to make sure 2754 -- that they made no difference. 2755 when (gopt Opt_DoAnnotationLinting dflags) $ do 2756 liftIO $ Err.showPass dflags "Annotation linting - second run" 2757 nguts' <- withoutAnnots pass guts 2758 -- Finally compare the resulting bindings 2759 liftIO $ Err.showPass dflags "Annotation linting - comparison" 2760 let binds = flattenBinds $ mg_binds nguts 2761 binds' = flattenBinds $ mg_binds nguts' 2762 (diffs,_) = diffBinds True (mkRnEnv2 emptyInScopeSet) binds binds' 2763 when (not (null diffs)) $ CoreMonad.putMsg $ vcat 2764 [ lint_banner "warning" pname 2765 , text "Core changes with annotations:" 2766 , withPprStyle (defaultDumpStyle dflags) $ nest 2 $ vcat diffs 2767 ] 2768 -- Return actual new guts 2769 return nguts 2770 2771-- | Run the given pass without annotations. This means that we both 2772-- set the debugLevel setting to 0 in the environment as well as all 2773-- annotations from incoming modules. 2774withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts 2775withoutAnnots pass guts = do 2776 -- Remove debug flag from environment. 2777 dflags <- getDynFlags 2778 let removeFlag env = env{ hsc_dflags = dflags{ debugLevel = 0} } 2779 withoutFlag corem = 2780 -- TODO: supply tag here as well ? 2781 liftIO =<< runCoreM <$> fmap removeFlag getHscEnv <*> getRuleBase <*> 2782 getUniqMask <*> getModule <*> 2783 getVisibleOrphanMods <*> 2784 getPrintUnqualified <*> getSrcSpanM <*> 2785 pure corem 2786 -- Nuke existing ticks in module. 2787 -- TODO: Ticks in unfoldings. Maybe change unfolding so it removes 2788 -- them in absence of debugLevel > 0. 2789 let nukeTicks = stripTicksE (not . tickishIsCode) 2790 nukeAnnotsBind :: CoreBind -> CoreBind 2791 nukeAnnotsBind bind = case bind of 2792 Rec bs -> Rec $ map (\(b,e) -> (b, nukeTicks e)) bs 2793 NonRec b e -> NonRec b $ nukeTicks e 2794 nukeAnnotsMod mg@ModGuts{mg_binds=binds} 2795 = mg{mg_binds = map nukeAnnotsBind binds} 2796 -- Perform pass with all changes applied 2797 fmap fst $ withoutFlag $ pass (nukeAnnotsMod guts) 2798