[Git][ghc/ghc][wip/T27078] Kill off the substitution in Lint
Simon Peyton Jones pushed to branch wip/T27078 at Glasgow Haskell Compiler / GHC Commits: 3d5c2a1d by Simon Peyton Jones at 2026-04-17T15:02:08+01:00 Kill off the substitution in Lint Now that we have invariant (NoTypeShadowing) we no longer need Lint to carry an ambient substitution. This makes it simpler and faster. A really worthwhile refactor. There are some knock-on effects * Linting join points after worker/wrapper. See Note [Join points and beta redexes] * Running a type substitution after the desugarer. See Note [Substituting type-lets] in the new module GHC.Core.SubstTypeLets Implements #27078 Most perf tests don't use Lint so we won't see a perf incresae. But T1969, which uses -O0 and Lint, gets 1.3% worse because it has to run the SubstTypeLets pass which is a somewhat expensive no-op Overall though compile-time allocations are down 0.1%. Metric Increase: T1969 - - - - - 9 changed files: - compiler/GHC/Core/Lint.hs - + compiler/GHC/Core/Lint/SubstTypeLets.hs - compiler/GHC/Core/Opt/OccurAnal.hs - compiler/GHC/Core/Opt/WorkWrap/Utils.hs - compiler/GHC/Core/Subst.hs - compiler/GHC/Driver/Config/Core/Lint.hs - compiler/ghc.cabal.in - testsuite/tests/corelint/LintEtaExpand.stderr - testsuite/tests/corelint/T21115b.stderr Changes: ===================================== compiler/GHC/Core/Lint.hs ===================================== @@ -18,7 +18,7 @@ module GHC.Core.Lint ( LintConfig (..), WarnsAndErrs, - lintCoreBindings', lintUnfolding, + lintCoreBindings, lintUnfolding, lintPassResult, lintExpr, lintAnnots, lintAxioms, @@ -46,6 +46,7 @@ import GHC.Core.FVs import GHC.Core.Utils import GHC.Core.Stats ( coreBindsStats ) import GHC.Core.DataCon +import GHC.Core.Lint.SubstTypeLets( substTypeLets ) import GHC.Core.Ppr import GHC.Core.Coercion import GHC.Core.Type as Type @@ -178,65 +179,7 @@ Note [Linting function types] All saturated applications of funTyCon are represented with the FunTy constructor. See Note [Function type constructors and FunTy] in GHC.Builtin.Types.Prim - We check this invariant in lintType. - -Note [Linting type lets] -~~~~~~~~~~~~~~~~~~~~~~~~ -In the desugarer, it's very very convenient to be able to say (in effect) - let a = Type Bool in - let x::a = True in <body> -That is, use a type let. See Note [Core type and coercion invariant] in "GHC.Core". -One place it is used is in mkWwBodies; see Note [Join points and beta-redexes] -in GHC.Core.Opt.WorkWrap.Utils. (Maybe there are other "clients" of this feature; I'm not sure). - -* Hence when linting <body> we need to remember that a=Int, else we - might reject a correct program. So we carry a type substitution (in - this example [a -> Bool]) and apply this substitution before - comparing types. In effect, in Lint, type equality is always - equality-modulo-le-subst. This is in the le_subst field of - LintEnv. But nota bene: - - (SI1) The le_subst substitution is applied to types and coercions only - - (SI2) The result of that substitution is used only to check for type - equality, to check well-typed-ness, /but is then discarded/. - The result of substitution does not outlive the CoreLint pass. - - (SI3) The InScopeSet of le_subst includes only TyVar and CoVar binders. - -* The function - lintInTy :: Type -> LintM (Type, Kind) - returns a substituted type. - -* When we encounter a binder (like x::a) we must apply the substitution - to the type of the binding variable. lintBinders does this. - -* Clearly we need to clone tyvar binders as we go. - -* But take care (#17590)! We must also clone CoVar binders: - let a = TYPE (ty |> cv) - in \cv -> blah - blindly substituting for `a` might capture `cv`. - -* Alas, when cloning a coercion variable we might choose a unique - that happens to clash with an inner Id, thus - \cv_66 -> let wild_X7 = blah in blah - We decide to clone `cv_66` because it's already in scope. Fine, - choose a new unique. Aha, X7 looks good. So we check the lambda - body with le_subst of [cv_66 :-> cv_X7] - - This is all fine, even though we use the same unique as wild_X7. - As (SI2) says, we do /not/ return a new lambda - (\cv_X7 -> let wild_X7 = blah in ...) - We simply use the le_subst substitution in types/coercions only, when - checking for equality. - -* We still need to check that Id occurrences are bound by some - enclosing binding. We do /not/ use the InScopeSet for the le_subst - for this purpose -- it contains only TyCoVars. Instead we have a separate - le_ids for the in-scope Id binders. - -Sigh. We might want to explore getting rid of type-let! +We check this invariant in lintType. Note [Bad unsafe coercion] ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -311,6 +254,7 @@ path does not result in allocation in the hot path. This can be surprisingly impactful. Changing `lint_app` reduced allocations for one test program I was looking at by ~4%. + ************************************************************************ * * Beginning and ending passes @@ -407,26 +351,37 @@ data LintPassResultConfig = LintPassResultConfig , lpr_platform :: !Platform , lpr_makeLintFlags :: !LintFlags , lpr_passPpr :: !SDoc + , lpr_preSubst :: !Bool -- True <=> run substTypeLets before linting + -- See Note [Substituting type-lets] , lpr_localsInScope :: ![Var] } lintPassResult :: Logger -> LintPassResultConfig -> CoreProgram -> IO () lintPassResult logger cfg binds - = do { let warns_and_errs = lintCoreBindings' - (LintConfig + = do { let lint_config = LintConfig { l_diagOpts = lpr_diagOpts cfg , l_platform = lpr_platform cfg , l_flags = lpr_makeLintFlags cfg , l_vars = lpr_localsInScope cfg - }) - binds + } + + -- Do the pre-substitution if necessary + -- See Note [Substituting type-lets] in GHC.Core.SubstTypeLets + -- especially wrinkle (STL2) + ; let binds1 | lpr_preSubst cfg = substTypeLets binds + | otherwise = binds + + -- Do the main Lint pass itself + ; let warns_and_errs = lintCoreBindings lint_config binds1 + + -- Report the results ; Err.showPass logger $ "Core Linted result of " ++ renderWithContext defaultSDocContext (lpr_passPpr cfg) ; displayLintResults logger (lpr_passPpr cfg) - (pprCoreBindings binds) warns_and_errs + (pprCoreBindings binds1) warns_and_errs } displayLintResults :: Logger @@ -456,11 +411,11 @@ lint_banner string pass = text "*** Core Lint" <+> text string <+> text "***" -- | Type-check a 'CoreProgram'. See Note [Core Lint guarantee]. -lintCoreBindings' :: LintConfig -> CoreProgram -> WarnsAndErrs +lintCoreBindings :: LintConfig -> CoreProgram -> WarnsAndErrs -- Returns (warnings, errors) -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] -lintCoreBindings' cfg binds +lintCoreBindings cfg binds = initL cfg $ addLoc TopLevelBindings $ do { -- Check that all top-level binders are distinct @@ -472,8 +427,7 @@ lintCoreBindings' cfg binds ; checkL (null ext_dups) (dupExtVars ext_dups) -- Typecheck the bindings - ; lintRecBindings TopLevel all_pairs $ \_ -> - return () } + ; lintRecBindings TopLevel all_pairs $ return () } where all_pairs = flattenBinds binds -- Put all the top-level binders in scope at the start @@ -555,28 +509,28 @@ Check a core binding, returning the list of variables bound. -- Let lintRecBindings :: TopLevelFlag -> [(Id, CoreExpr)] - -> ([OutId] -> LintM a) -> LintM (a, [UsageEnv]) + -> LintM a -> LintM (a, [UsageEnv]) lintRecBindings top_lvl pairs thing_inside - = lintIdBndrs top_lvl bndrs $ \ bndrs' -> - do { ues <- zipWithM lint_pair bndrs' rhss - ; a <- thing_inside bndrs' + = lintIdBndrs top_lvl bndrs $ + do { ues <- zipWithM lint_pair bndrs rhss + ; a <- thing_inside ; return (a, ues) } where (bndrs, rhss) = unzip pairs - lint_pair bndr' rhs - = addLoc (RhsOf bndr') $ - do { (rhs_ty, ue) <- lintRhs bndr' rhs -- Check the rhs - ; lintLetBind top_lvl Recursive bndr' rhs rhs_ty + lint_pair bndr rhs + = addLoc (RhsOf bndr) $ + do { (rhs_ty, ue) <- lintRhs bndr rhs -- Check the rhs + ; lintLetBind top_lvl Recursive bndr rhs rhs_ty ; return ue } -lintLetBody :: LintLocInfo -> [OutId] -> CoreExpr -> LintM (OutType, UsageEnv) +lintLetBody :: LintLocInfo -> [Id] -> CoreExpr -> LintM (Type, UsageEnv) lintLetBody loc bndrs body = do { (body_ty, body_ue) <- addLoc loc (lintCoreExpr body) ; mapM_ (lintJoinBndrType body_ty) bndrs ; return (body_ty, body_ue) } -lintLetBind :: TopLevelFlag -> RecFlag -> OutId - -> CoreExpr -> OutType -> LintM () +lintLetBind :: TopLevelFlag -> RecFlag -> Id + -> CoreExpr -> Type -> LintM () -- Binder's type, and the RHS, have already been linted -- This function checks other invariants lintLetBind top_lvl rec_flag binder rhs rhs_ty @@ -651,14 +605,17 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty _ -> return () - ; addLoc (RuleOf binder) $ mapM_ (lintCoreRule binder binder_ty) (idCoreRules binder) + -- Lint any RULES + ; addLoc (RuleOf binder) $ + mapM_ (lintCoreRule binder binder_ty) (idCoreRules binder) + -- Lint the unfolding + -- Do this here, not in lintIdBinder, so that all the + -- binders of the letrec group are in scope ; addLoc (UnfoldingOf binder) $ lintIdUnfolding binder binder_ty (idUnfolding binder) - ; return () } - -- We should check the unfolding, if any, but this is tricky because - -- the unfolding is a SimplifiableCoreExpr. Give up for now. + ; return () } -- | Checks the RHS of bindings. It only differs from 'lintCoreExpr' -- in that it doesn't reject occurrences of the function 'makeStatic' when they @@ -667,7 +624,7 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty -- join point. -- -- See Note [Checking StaticPtrs]. -lintRhs :: Id -> CoreExpr -> LintM (OutType, UsageEnv) +lintRhs :: Id -> CoreExpr -> LintM (Type, UsageEnv) -- NB: the Id can be Linted or not -- it's only used for -- its OccInfo and join-pointer-hood lintRhs bndr rhs @@ -682,7 +639,7 @@ lintRhs _bndr rhs = fmap lf_check_static_ptrs getLintFlags >>= go where -- Allow occurrences of 'makeStatic' at the top-level but produce errors -- otherwise. - go :: StaticPtrCheck -> LintM (OutType, UsageEnv) + go :: StaticPtrCheck -> LintM (Type, UsageEnv) go AllowAtTopLevel | (binders0, rhs') <- collectTyBinders rhs , Just (fun, t, info, e) <- collectMakeStaticArgs rhs' @@ -699,7 +656,7 @@ lintRhs _bndr rhs = fmap lf_check_static_ptrs getLintFlags >>= go -- | Lint the RHS of a join point with expected join arity of @n@ (see Note -- [Join points] in "GHC.Core"). -lintJoinLams :: JoinArity -> Maybe Id -> CoreExpr -> LintM (OutType, UsageEnv) +lintJoinLams :: JoinArity -> Maybe Id -> CoreExpr -> LintM (Type, UsageEnv) lintJoinLams join_arity enforce rhs = go join_arity rhs where @@ -715,17 +672,22 @@ lintIdUnfolding :: Id -> Type -> Unfolding -> LintM () lintIdUnfolding bndr bndr_ty uf | isStableUnfolding uf , Just rhs <- maybeUnfoldingTemplate uf - = noMultiplicityChecks $ -- Skip linearity checking for unfoldings - -- See Note [Linting linearity] - do { ty <- fst <$> (if isCompulsoryUnfolding uf - then noFixedRuntimeRepChecks $ lintRhs bndr rhs - -- ^^^^^^^^^^^^^^^^^^^^^^^ - -- See Note [Checking for representation polymorphism] - else lintRhs bndr rhs) - ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) } -lintIdUnfolding _ _ _ - = return () -- Do not Lint unstable unfoldings, because that leads - -- to exponential behaviour; c.f. GHC.Core.FVs.idUnfoldingVars + = suppress_rr_checks $ + noMultiplicityChecks $ -- Skip linearity checking for unfoldings + -- See Note [Linting linearity] + do { (unf_ty, _unf_ue) <- lintRhs bndr rhs + ; ensureEqTys bndr_ty unf_ty (mkRhsMsg bndr (text "unfolding") unf_ty) } + + | otherwise + = -- Do not Lint the body of an unstable unfolding, because that leads + -- to exponential behaviour; c.f. GHC.Core.FVs.idUnfoldingVars + return () + + where + -- See Note [Checking for representation polymorphism] + suppress_rr_checks thing_inside + | isCompulsoryUnfolding uf = noFixedRuntimeRepChecks thing_inside + | otherwise = thing_inside {- Note [Checking for INLINE loop breakers] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -887,13 +849,8 @@ suspicious and worth investigating if you have a seg-fault or bizarre behaviour. ************************************************************************ -} -lintCoreExpr :: InExpr -> LintM (OutType, UsageEnv) --- The returned type has the substitution from the monad --- already applied to it: --- lintCoreExpr e subst = exprType (subst e) --- --- The returned "type" can be a kind, if the expression is (Type ty) - +lintCoreExpr :: CoreExpr -> LintM (Type, UsageEnv) +-- The returned type is the type of the expression -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] @@ -920,7 +877,7 @@ lintCoreExpr (Cast expr co) ; lintCoercion co ; lintRole co Representational (coercionRole co) - ; Pair from_ty to_ty <- substCoKindM co + ; let Pair from_ty to_ty = coercionKind co ; checkValueType (typeKind to_ty) $ text "target of cast" <+> quotes (ppr co) ; ensureEqTys from_ty expr_ty (mkCastErr expr co from_ty expr_ty) @@ -934,27 +891,22 @@ lintCoreExpr (Tick tickish expr) lintCoreExpr (Let (NonRec tv (Type ty)) body) | isTyVar tv - = -- See Note [Linting type lets] - do { ty' <- lintTypeAndSubst ty - ; lintTyCoBndr tv $ \ tv' -> - do { addLoc (RhsOf tv) $ lintTyKind tv' ty' - -- Now extend the substitution so we - -- take advantage of it in the body - ; extendTvSubstL tv ty' $ - addLoc (BodyOfLet tv) $ - lintCoreExpr body } } + = do { lintType ty + ; lintTyCoBndr tv $ + do { addLoc (RhsOf tv) $ lintTyKind tv ty + ; addLoc (BodyOfLet tv) $ lintCoreExpr body } } lintCoreExpr (Let (NonRec bndr rhs) body) | isId bndr = do { -- First Lint the RHS, before bringing the binder into scope (rhs_ty, let_ue) <- lintRhs bndr rhs - -- See Note [Multiplicity of let binders] in Var + -- See Note [Multiplicity of let binders] in Var -- Now lint the binder - ; lintBinder LetBind bndr $ \bndr' -> - do { lintLetBind NotTopLevel NonRecursive bndr' rhs rhs_ty - ; addAliasUE bndr' let_ue $ - lintLetBody (BodyOfLet bndr') [bndr'] body } } + ; lintBinder LetBind bndr $ + do { lintLetBind NotTopLevel NonRecursive bndr rhs rhs_ty + ; addAliasUE bndr let_ue $ + lintLetBody (BodyOfLet bndr) [bndr] body } } | otherwise = failWithL (mkLetErr bndr rhs) -- Not quite accurate @@ -973,8 +925,8 @@ lintCoreExpr e@(Let (Rec pairs) body) -- See Note [Multiplicity of let binders] in Var ; ((body_type, body_ue), ues) <- - lintRecBindings NotTopLevel pairs $ \ bndrs' -> - lintLetBody (BodyOfLetRec bndrs') bndrs' body + lintRecBindings NotTopLevel pairs $ + lintLetBody (BodyOfLetRec bndrs) bndrs body ; return (body_type, body_ue `addUE` scaleUE ManyTy (foldr1WithDefault zeroUE addUE ues)) } where bndrs = map fst pairs @@ -986,7 +938,7 @@ lintCoreExpr e@(App _ _) -- N.B. we may have an over-saturated application of the form: -- runRW (\s -> \x -> ...) y , ty_arg1 : ty_arg2 : cont_arg : rest <- args - = do { let lint_rw_cont :: CoreArg -> Mult -> UsageEnv -> LintM (OutType, UsageEnv) + = do { let lint_rw_cont :: CoreArg -> Mult -> UsageEnv -> LintM (Type, UsageEnv) lint_rw_cont expr@(Lam _ _) mult fun_ue = do { (arg_ty, arg_ue) <- lintJoinLams 1 (Just fun) expr ; let app_ue = addUE fun_ue (scaleUE mult arg_ue) @@ -1036,74 +988,73 @@ lintCoreExpr (Type ty) lintCoreExpr (Coercion co) -- See Note [Coercions in terms] = do { addLoc (InCo co) $ lintCoercion co - ; ty <- substTyM (coercionType co) + ; let ty = coercionType co ; return (ty, zeroUE) } ---------------------- -lintIdOcc :: InId -> Int -- Number of arguments (type or value) being passed - -> LintM (OutType, UsageEnv) -- returns type of the *variable* -lintIdOcc in_id nargs - = addLoc (OccOf in_id) $ - do { checkL (isNonCoVarId in_id) - (text "Non term variable" <+> ppr in_id) +lintIdOcc :: Id -> Int -- Number of arguments (type or value) being passed + -> LintM (Type, UsageEnv) -- returns type of the *variable* +lintIdOcc id nargs + = addLoc (OccOf id) $ + do { checkL (isNonCoVarId id) + (text "Non term variable" <+> ppr id) -- See GHC.Core Note [Variable occurrences in Core] - -- Check that the type of the occurrence is the same - -- as the type of the binding site. The inScopeIds are - -- /un-substituted/, so this checks that the occurrence type - -- is identical to the binder type. - -- This makes things much easier for things like: - -- /\a. \(x::Maybe a). /\a. ...(x::Maybe a)... - -- The "::Maybe a" on the occurrence is referring to the /outer/ a. - -- If we compared /substituted/ types we'd risk comparing - -- (Maybe a) from the binding site with bogus (Maybe a1) from - -- the occurrence site. Comparing un-substituted types finesses - -- this altogether - ; out_ty <- lintVarOcc in_id + ; lintVarOcc id -- Check for a nested occurrence of the StaticPtr constructor. -- See Note [Checking StaticPtrs]. ; when (nargs /= 0) $ - checkL (idName in_id /= makeStaticName) $ + checkL (idName id /= makeStaticName) $ text "Found makeStatic nested in an expression" - ; checkDeadIdOcc in_id + ; checkDeadIdOcc id - ; case isDataConId_maybe in_id of + ; case isDataConId_maybe id of Nothing -> return () Just dc -> checkTypeDataConOcc "expression" dc - ; checkJoinOcc in_id nargs - ; usage <- varCallSiteUsage in_id - - ; return (out_ty, usage) } + ; checkJoinOcc id nargs + ; usage <- varCallSiteUsage id + ; return (idType id, usage) } +------------------ lintCoreFun :: CoreExpr - -> Int -- Number of arguments (type or val) being passed - -> LintM (OutType, UsageEnv) -- Returns type of the *function* + -> Int -- Number of arguments (type or val) being passed + -> LintM (Type, UsageEnv) -- Returns type of the *function* lintCoreFun (Var var) nargs = lintIdOcc var nargs lintCoreFun (Lam var body) nargs - -- Act like lintCoreExpr of Lam, but *don't* call markAllJoinsBad; - -- See Note [Beta redexes] + -- Act like lintCoreExpr of Lam, but *don't* necessarily call markAllJoinsBad; + -- See Note [Join points and beta-redexes] | nargs /= 0 = lintLambda var $ lintCoreFun body (nargs - 1) lintCoreFun expr nargs - = markAllJoinsBadIf (nargs /= 0) $ - -- See Note [Join points are less general than the paper] - lintCoreExpr expr + = do { mark_bad_joins + <- if nargs == 0 + then -- Saturated lambda + -- See Note [Join points and beta-redexes] + do { flags <- getLintFlags + ; return (not (lf_allow_beta_joins flags)) } + else -- Something else + -- See Note [Join points are less general than the paper] + return True + + ; markAllJoinsBadIf mark_bad_joins $ + lintCoreExpr expr } + ------------------ lintLambda :: Var -> LintM (Type, UsageEnv) -> LintM (Type, UsageEnv) lintLambda var lintBody = addLoc (LambdaBodyOf var) $ - lintBinder LambdaBind var $ \ var' -> + lintBinder LambdaBind var $ do { (body_ty, ue) <- lintBody - ; ue' <- checkLinearity ue var' - ; return (mkLamType var' body_ty, ue') } + ; ue' <- checkLinearity ue var + ; return (mkLamType var body_ty, ue') } ------------------ checkDeadIdOcc :: Id -> LintM () -- Occurrences of an Id should never be dead.... @@ -1117,8 +1068,8 @@ checkDeadIdOcc id = return () ------------------ -lintJoinBndrType :: OutType -- Type of the body - -> OutId -- Possibly a join Id +lintJoinBndrType :: Type -- Type of the body + -> Id -- Possibly a join Id -> LintM () -- Checks that the return type of a join Id matches the body -- E.g. join j x = rhs in body @@ -1337,8 +1288,55 @@ checkLinearity body_ue lam_var = return body_ue' Nothing -> return body_ue -- A type variable -{- Note [Linting join points with casts or ticks] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Join points and beta-redexes] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In the worker/wrapper pass, the worker invokes the original function by calling +it with arguments, thus producing a beta-redex for the simplifier to munch away: + + \x y z -> e => (\x y z -> e) wx wy wz + +But we need to take care if `e` invokes a join point. For example: + + join j1 x = ... + join j2 y = if y == 0 then 0 else j1 y +=> + join j1 x = ... + join $wj2 y# = (\y -> if y == 0 then 0 else jump j1 y) (I# y#) + join j2 y = case y of I# y# -> jump $wj2 y# + +Now the jump to `j1` is inside a lambda and inside an application. That is ill-typed +from Lint's point of view. And yet, after one round of simplification it'll all be +fine. + +You might wonder if we could use a `let` instead of a lambda for the worker: + + join $wj2 y# = let y = I# y# + in if y == 0 then 0 else jump j1 y + +That would solve the join-point problem, but it really doesn't work because + 1. The lets shadow each other + 2. In particular the invariant (NoTypeShadowing) is easily broken. + (We might have type lambdas of course.) + +In short, te lambda arguments should not "see" any of the lambda-bound +variables. + +So our solution is this: + +* Use straightforward applicaion in the worker-wrapper pass, creating a beta-redex. + See the call to `mkApps` in GHC.Core.Opt.WorkWrap.Utils.mkWwBodies. + +* Tell Lint not to complain about a join-point invocation hidden under a + saturated beta-redex. The code is rather simple: see `lintCoreFun`. + + We guard this with a Lint flag `lf_allow_beta_joins`. + +* Teach occurrence analysis that `j1` is still a join point, despite its + call being nested inside the beta-redex. See Note [occAnal for applications] + in GHC.Core.Opt.OccurAnal. + +Note [Linting join points with casts or ticks] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ As per Note [Join points, casts, and ticks] in GHC.Core, we have to be careful when a cast or tick occurs in between a join point binding and a corresponding join point occurrence. @@ -1409,33 +1407,6 @@ lose track of why an expression is bottom, so we shouldn't make too much fuss when that happens. -Note [Beta redexes] -~~~~~~~~~~~~~~~~~~~ -Consider: - - join j @x y z = ... in - (\@x y z -> jump j @x y z) @t e1 e2 - -This is clearly ill-typed, since the jump is inside both an application and a -lambda, either of which is enough to disqualify it as a tail call (see Note -[Invariants on join points] in GHC.Core). However, strictly from a -lambda-calculus perspective, the term doesn't go wrong---after the two beta -reductions, the jump *is* a tail call and everything is fine. - -Why would we want to allow this when we have let? One reason is that a compound -beta redex (that is, one with more than one argument) has different scoping -rules: naively reducing the above example using lets will capture any free -occurrence of y in e2. More fundamentally, type lets are tricky; many passes, -such as Float Out, tacitly assume that the incoming program's type lets have -all been dealt with by the simplifier. Thus we don't want to let-bind any types -in, say, GHC.Core.Subst.simpleOptPgm, which in some circumstances can run immediately -before Float Out. - -All that said, currently GHC.Core.Subst.simpleOptPgm is the only thing using this -loophole, doing so to avoid re-traversing large functions (beta-reducing a type -lambda without introducing a type let requires a substitution). TODO: Improve -simpleOptPgm so that we can forget all this ever happened. - ************************************************************************ * * \subsection[lintCoreArgs]{lintCoreArgs} @@ -1449,23 +1420,23 @@ subtype of the required type, as one would expect. -- Takes the functions type and arguments as argument. -- Returns the *result* of applying the function to arguments. -- e.g. f :: Int -> Bool -> Int would return `Int` as result type. -lintCoreArgs :: (OutType, UsageEnv) -> [InExpr] -> LintM (OutType, UsageEnv) +lintCoreArgs :: (Type, UsageEnv) -> [CoreExpr] -> LintM (Type, UsageEnv) lintCoreArgs (fun_ty, fun_ue) args - = lintApp (text "expression") - lintTyArg lintValArg fun_ty args fun_ue + = lintApp (text "expression") lintTyArg lintValArg fun_ty args fun_ue -lintTyArg :: InExpr -> LintM OutType +lintTyArg :: CoreExpr -> LintM Type -- Type argument lintTyArg (Type arg_ty) = do { checkL (not (isCoercionTy arg_ty)) (text "Unnecessary coercion-to-type injection:" <+> ppr arg_ty) - ; lintTypeAndSubst arg_ty } + ; lintType arg_ty + ; return arg_ty } lintTyArg arg = failWithL (hang (text "Expected type argument but found") 2 (ppr arg)) -lintValArg :: InExpr -> Mult -> UsageEnv -> LintM (OutType, UsageEnv) +lintValArg :: CoreExpr -> Mult -> UsageEnv -> LintM (Type, UsageEnv) lintValArg arg mult fun_ue = do { (arg_ty, arg_ue) <- markAllJoinsBad $ lintCoreExpr arg -- See Note [Representation polymorphism invariants] in GHC.Core @@ -1484,9 +1455,9 @@ lintValArg arg mult fun_ue ----------------- lintAltBinders :: UsageEnv - -> Var -- Case binder - -> OutType -- Scrutinee type - -> OutType -- Constructor type + -> Var -- Case binder + -> Type -- Scrutinee type + -> Type -- Constructor type -> [(Mult, OutVar)] -- Binders -> LintM UsageEnv -- If you edit this function, you may need to update the GHC formalism @@ -1505,6 +1476,7 @@ lintAltBinders rhs_ue case_bndr scrut_ty con_ty ((var_w, bndr):bndrs) ; rhs_ue' <- checkCaseLinearity rhs_ue case_bndr var_w bndr ; lintAltBinders rhs_ue' case_bndr scrut_ty con_ty' bndrs } + -- | Implements the case rules for linearity checkCaseLinearity :: UsageEnv -> Var -> Mult -> Var -> LintM UsageEnv checkCaseLinearity ue case_bndr var_w bndr = do @@ -1529,7 +1501,7 @@ checkCaseLinearity ue case_bndr var_w bndr = do ----------------- -lintTyApp :: OutType -> OutType -> LintM OutType +lintTyApp :: Type -> Type -> LintM Type lintTyApp fun_ty arg_ty | Just (tv,body_ty) <- splitForAllTyVar_maybe fun_ty = do { lintTyKind tv arg_ty @@ -1547,8 +1519,8 @@ lintTyApp fun_ty arg_ty -- | @lintValApp arg fun_ty arg_ty@ lints an application of @fun arg@ -- where @fun :: fun_ty@ and @arg :: arg_ty@, returning the type of the -- application. -lintValApp :: CoreExpr -> OutType -> OutType -> UsageEnv -> UsageEnv - -> LintM (OutType, UsageEnv) +lintValApp :: CoreExpr -> Type -> Type -> UsageEnv -> UsageEnv + -> LintM (Type, UsageEnv) lintValApp arg fun_ty arg_ty fun_ue arg_ue | Just (_, w, arg_ty', res_ty') <- splitFunTy_maybe fun_ty = do { ensureEqTys arg_ty' arg_ty (mkAppMsg arg_ty' arg_ty arg) @@ -1559,9 +1531,7 @@ lintValApp arg fun_ty arg_ty fun_ue arg_ue where err2 = mkNonFunAppMsg fun_ty arg_ty arg -lintTyKind :: OutTyVar -> OutType -> LintM () --- Both args have had substitution applied - +lintTyKind :: OutTyVar -> Type -> LintM () -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] lintTyKind tyvar arg_ty @@ -1579,36 +1549,36 @@ lintTyKind tyvar arg_ty ************************************************************************ -} -lintCaseExpr :: CoreExpr -> InId -> InType -> [CoreAlt] -> LintM (OutType, UsageEnv) +lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM (Type, UsageEnv) lintCaseExpr scrut case_bndr alt_ty alts = do { let e = Case scrut case_bndr alt_ty alts -- Just for error messages -- Check the scrutinee - ; (scrut_ty', scrut_ue) <- markAllJoinsBad $ lintCoreExpr scrut + ; (scrut_ty, scrut_ue) <- markAllJoinsBad $ lintCoreExpr scrut -- See Note [Join points are less general than the paper] -- in GHC.Core - ; alt_ty' <- addLoc (CaseTy scrut) $ lintValueType alt_ty + ; addLoc (CaseTy scrut) $ lintValueType alt_ty - ; checkCaseAlts e scrut scrut_ty' alts + ; checkCaseAlts e scrut scrut_ty alts -- Lint the case-binder. Must do this after linting the scrutinee -- because the case-binder isn't in scope in the scrutineex - ; lintBinder CaseBind case_bndr $ \case_bndr' -> + ; lintBinder CaseBind case_bndr $ -- Don't use lintIdBndr on case_bndr, because unboxed tuple is legitimate - do { let case_bndr_ty' = idType case_bndr' - scrut_mult = idMult case_bndr' + do { let case_bndr_ty = idType case_bndr + scrut_mult = idMult case_bndr - ; ensureEqTys case_bndr_ty' scrut_ty' (mkScrutMsg case_bndr case_bndr_ty' scrut_ty') + ; ensureEqTys case_bndr_ty scrut_ty (mkScrutMsg case_bndr case_bndr_ty scrut_ty) -- See GHC.Core Note [Case expression invariants] item (7) ; -- Check the alternatives - ; alt_ues <- mapM (lintCoreAlt case_bndr' scrut_ty' scrut_mult alt_ty') alts + ; alt_ues <- mapM (lintCoreAlt case_bndr scrut_ty scrut_mult alt_ty) alts ; let case_ue = (scaleUE scrut_mult scrut_ue) `addUE` supUEs alt_ues - ; return (alt_ty', case_ue) } } + ; return (alt_ty, case_ue) } } -checkCaseAlts :: InExpr -> InExpr -> OutType -> [CoreAlt] -> LintM () +checkCaseAlts :: CoreExpr -> CoreExpr -> Type -> [CoreAlt] -> LintM () -- a) Check that the alts are non-empty -- b1) Check that the DEFAULT comes first, if it exists -- b2) Check that the others are in increasing order @@ -1683,17 +1653,17 @@ checkCaseAlts e scrut scrut_ty alts is_lit_alt (Alt (LitAlt _) _ _) = True is_lit_alt _ = False -lintAltExpr :: CoreExpr -> OutType -> LintM UsageEnv +lintAltExpr :: CoreExpr -> Type -> LintM UsageEnv lintAltExpr expr ann_ty = do { (actual_ty, ue) <- lintCoreExpr expr ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) ; return ue } -- See GHC.Core Note [Case expression invariants] item (6) -lintCoreAlt :: OutId -- Case binder - -> OutType -- Type of scrutinee +lintCoreAlt :: Id -- Case binder + -> Type -- Type of scrutinee -> Mult -- Multiplicity of scrutinee - -> OutType -- Type of the alternative + -> Type -- Type of the alternative -> CoreAlt -> LintM UsageEnv -- If you edit this function, you may need to update the GHC formalism @@ -1738,11 +1708,11 @@ lintCoreAlt case_bndr scrut_ty _scrut_mult alt_ty alt@(Alt (DataAlt con) args rh ; multiplicities = map binderMult $ fst $ splitPiTys con_payload_ty } -- And now bring the new binders into scope - ; lintBinders CasePatBind args $ \ args' -> do + ; lintBinders CasePatBind args $ do { rhs_ue <- lintAltExpr rhs alt_ty ; rhs_ue' <- addLoc (CasePat alt) $ lintAltBinders rhs_ue case_bndr scrut_ty con_payload_ty - (zipEqual multiplicities args') + (zipEqual multiplicities args) ; return $ deleteUE rhs_ue' case_bndr } } @@ -1784,54 +1754,52 @@ lintLinearBinder doc actual_usage described_usage -} -- When we lint binders, we (one at a time and in order): --- 1. Lint var types or kinds (possibly substituting) --- 2. Add the binder to the in scope set, and if its a coercion var, --- we may extend the substitution to reflect its (possibly) new kind -lintBinders :: HasDebugCallStack => BindingSite -> [InVar] -> ([OutVar] -> LintM a) -> LintM a -lintBinders _ [] linterF = linterF [] -lintBinders site (var:vars) linterF = lintBinder site var $ \var' -> - lintBinders site vars $ \ vars' -> - linterF (var':vars') +-- 1. Lint var types or kinds +-- 2. Add the binder to the in scope set +lintBinders :: HasDebugCallStack => BindingSite -> [Var] -> LintM a -> LintM a +lintBinders _ [] linterF = linterF +lintBinders site (var:vars) linterF = lintBinder site var $ + lintBinders site vars $ + linterF -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] -lintBinder :: HasDebugCallStack => BindingSite -> InVar -> (OutVar -> LintM a) -> LintM a +lintBinder :: HasDebugCallStack => BindingSite -> Var -> LintM a -> LintM a lintBinder site var linterF | isTyCoVar var = lintTyCoBndr var linterF | otherwise = lintIdBndr NotTopLevel site var linterF -lintTyCoBndr :: HasDebugCallStack => TyCoVar -> (OutTyCoVar -> LintM a) -> LintM a +lintTyCoBndr :: HasDebugCallStack => TyCoVar -> LintM a -> LintM a lintTyCoBndr tcv thing_inside - = do { tcv_type' <- lintTypeAndSubst (varType tcv) - ; let tcv_kind' = typeKind tcv_type' + = do { let tcv_type = varType tcv + tcv_kind = typeKind tcv_type + ; lintType (varType tcv) -- See (FORALL1) and (FORALL2) in GHC.Core.Type ; if (isTyVar tcv) then -- Check that in (forall (a:ki). blah) we have ki:Type - lintL (isLiftedTypeKind tcv_kind') $ + lintL (isLiftedTypeKind tcv_kind) $ hang (text "TyVar whose kind does not have kind Type:") - 2 (ppr tcv <+> dcolon <+> ppr tcv_type' <+> dcolon <+> ppr tcv_kind') + 2 (ppr tcv <+> dcolon <+> ppr tcv_type <+> dcolon <+> ppr tcv_kind) else -- Check that in (forall (cv::ty). blah), -- then ty looks like (t1 ~# t2) - lintL (isCoVarType tcv_type') $ + lintL (isCoVarType tcv_type) $ text "CoVar with non-coercion type:" <+> pprTyVar tcv - ; addInScopeTyCoVar tcv tcv_type' thing_inside } + ; addInScopeTyCoVar tcv thing_inside } -lintIdBndrs :: forall a. TopLevelFlag -> [InId] -> ([OutId] -> LintM a) -> LintM a +lintIdBndrs :: forall a. TopLevelFlag -> [Id] -> LintM a -> LintM a lintIdBndrs top_lvl ids thing_inside = go ids thing_inside where - go :: [Id] -> ([Id] -> LintM a) -> LintM a - go [] thing_inside = thing_inside [] - go (id:ids) thing_inside = lintIdBndr top_lvl LetBind id $ \id' -> - go ids $ \ids' -> - thing_inside (id' : ids') + go :: [Id] -> LintM a -> LintM a + go [] thing_inside = thing_inside + go (id:ids) thing_inside = lintIdBndr top_lvl LetBind id $ + go ids $ + thing_inside lintIdBndr :: TopLevelFlag -> BindingSite - -> InVar -> (OutVar -> LintM a) -> LintM a --- Do substitution on the type of a binder and add the var with this --- new type to the in-scope set of the second argument + -> Var -> LintM a -> LintM a -- ToDo: lint its rules lintIdBndr top_lvl bind_site id thing_inside = assertPpr (isId id) (ppr id) $ @@ -1864,14 +1832,16 @@ lintIdBndr top_lvl bind_site id thing_inside ; lintL (not (isCoVarType id_ty)) (text "Non-CoVar has coercion type" <+> ppr id <+> dcolon <+> ppr id_ty) - -- Check that the lambda binder has no value or OtherCon unfolding. + -- Check that lambda-bound Ids have no unfolding; not even OtherCon -- See #21496 - ; lintL (not (bind_site == LambdaBind && isEvaldUnfolding (idUnfolding id))) - (text "Lambda binder with value or OtherCon unfolding.") + ; let unf = idUnfolding id + ; checkL (not (bind_site == LambdaBind && hasSomeUnfolding unf)) $ + hang (text "Lambda binder" <+> quotes (ppr id) <+> text "has an unfolding") + 2 (ppr unf) - ; out_ty <- addLoc (IdTy id) (lintValueType id_ty) + ; addLoc (IdTy id) (lintValueType id_ty) - ; addInScopeId id out_ty thing_inside } + ; addInScopeId id thing_inside } where id_ty = idType id @@ -1891,62 +1861,44 @@ lintIdBndr top_lvl bind_site id thing_inside {- Note [Linting types and coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Notice that - lintType :: InType -> LintM () - lintCoercion :: InCoercion -> LintM () + lintType :: Type -> LintM () + lintCoercion :: Coercion -> LintM () Neither returns anything. -If you need the kind of the type, then do `typeKind` and then apply -the ambient substitution using `substTyM`. Note that the substitution -empty unless there is shadowing or type-lets; and if the substitution is -empty, the `substTyM` is a no-op. - -It is better to take the kind and then substitute, rather than substitute -and then take the kind, becaues the kind is usually smaller. - -Note: you might wonder if we should apply the same logic to expressions. -Why do we have - lintExpr :: InExpr -> LintM OutType -Partly inertia; but also taking the type of an expresison involve looking -down a deep chain of let's, whereas that is not true of taking the kind -of a type. It'd be worth an experiment though. - -Historical note: in the olden days we had - lintType :: InType -> LintM OutType -but that burned a huge amount of allocation building an OutType that was -often discarded, or used only to get its kind. - -I also experimented with - lintType :: InType -> LintM OutKind -but that too was slower. It is also much simpler to return ()! If we -return the kind we have to duplicate the logic in `typeKind`; and it is -much worse for coercions. +Note: you might wonder why we have + lintExpr :: CoreExpr -> LintM Type + lintType :: Type -> LintM () + +That is, linting an expression yields its type, but linting a type does not +yield its kind. Partly inertia; but: + +* Taking the type of an expresison involves looking down a deep chain of let's, + whereas that is not true of taking the kind of a type. It'd be worth an + experiment though. + +* I did experiment with + lintType :: Type -> LintM Kind + but that too was slower. It is also much simpler to return ()! If we return + the kind we have to duplicate the logic in `typeKind`; and it is much worse + for coercions. -} -lintValueType :: Type -> LintM OutType +lintValueType :: Type -> LintM () -- Types only, not kinds --- Check the type, and apply the substitution to it --- See Note [Linting type lets] lintValueType ty = addLoc (InType ty) $ - do { ty' <- lintTypeAndSubst ty - ; let sk = typeKind ty' + do { lintType ty + ; let sk = typeKind ty ; lintL (isTYPEorCONSTRAINT sk) $ hang (text "Ill-kinded type:" <+> ppr ty) - 2 (text "has kind:" <+> ppr sk) - ; return ty' } + 2 (text "has kind:" <+> ppr sk)} checkTyCon :: TyCon -> LintM () checkTyCon tc = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc) ------------------- -lintTypeAndSubst :: InType -> LintM OutType -lintTypeAndSubst ty = do { lintType ty; substTyM ty } - -- In GHCi we may lint an expression with a free - -- type variable. Then it won't be in the - -- substitution, but it should be in scope - -lintType :: InType -> LintM () +lintType :: Type -> LintM () -- See Note [Linting types and coercions] -- -- If you edit this function, you may need to update the GHC formalism @@ -1956,8 +1908,7 @@ lintType (TyVarTy tv) = failWithL (mkBadTyVarMsg tv) | otherwise - = do { _ <- lintVarOcc tv - ; return () } + = lintVarOcc tv lintType ty@(AppTy t1 t2) | TyConApp {} <- t1 @@ -1965,7 +1916,7 @@ lintType ty@(AppTy t1 t2) | otherwise = do { let (fun_ty, arg_tys) = collect t1 [t2] ; lintType fun_ty - ; fun_kind <- substTyM (typeKind fun_ty) + ; let fun_kind = typeKind fun_ty ; lint_ty_app ty fun_kind arg_tys } where collect (AppTy f a) as = collect f (a:as) @@ -1997,21 +1948,21 @@ lintType ty@(FunTy af tw t1 t2) lintType ty@(ForAllTy {}) = go [] ty where - go :: [OutTyCoVar] -> InType -> LintM () + go :: [OutTyCoVar] -> Type -> LintM () -- Loop, collecting the forall-binders go tcvs ty@(ForAllTy (Bndr tcv _) body_ty) | not (isTyCoVar tcv) = failWithL (text "Non-TyVar or Non-CoVar bound in type:" <+> ppr ty) | otherwise - = lintTyCoBndr tcv $ \tcv' -> + = lintTyCoBndr tcv $ do { -- See GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy] -- Suspicious because it works on InTyCoVar; c.f. ForAllCo when (isCoVar tcv) $ lintL (anyFreeVarsOfType (== tcv) body_ty) $ text "Covar does not occur in the body:" <+> (ppr tcv $$ ppr body_ty) - ; go (tcv' : tcvs) body_ty } + ; go (tcv : tcvs) body_ty } go tcvs body_ty = do { lintType body_ty @@ -2019,7 +1970,7 @@ lintType ty@(ForAllTy {}) lintType (CastTy ty co) = do { lintType ty - ; ty_kind <- substTyM (typeKind ty) + ; let ty_kind = typeKind ty ; co_lk <- lintStarCoercion co ; ensureEqTys ty_kind co_lk (mkCastTyErr ty co ty_kind co_lk) } @@ -2027,14 +1978,14 @@ lintType (LitTy l) = lintTyLit l lintType (CoercionTy co) = lintCoercion co ----------------- -lintForAllBody :: [OutTyCoVar] -> InType -> LintM () +lintForAllBody :: [OutTyCoVar] -> Type -> LintM () -- Do the checks for the body of a forall-type lintForAllBody tcvs body_ty = do { -- For type variables, check for skolem escape -- See Note [Phantom type variables in kinds] in GHC.Core.Type -- The kind of (forall cv. th) is liftedTypeKind, so no -- need to check for skolem-escape in the CoVar case - body_kind <- substTyM (typeKind body_ty) + let body_kind = typeKind body_ty ; case occCheckExpand tcvs body_kind of Just {} -> return () Nothing -> failWithL $ @@ -2045,7 +1996,7 @@ lintForAllBody tcvs body_ty ; checkValueType body_kind (text "the body of forall:" <+> ppr body_ty) } ----------------- -lintTySynFamApp :: Bool -> InType -> TyCon -> [InType] -> LintM () +lintTySynFamApp :: Bool -> Type -> TyCon -> [Type] -> LintM () -- The TyCon is a type synonym or a type family (not a data family) -- See Note [Linting type synonym applications] -- c.f. GHC.Tc.Validity.check_syn_tc_app @@ -2071,21 +2022,21 @@ lintTySynFamApp report_unsat ty tc tys ----------------- -- Confirms that a kind is really TYPE r or Constraint -checkValueType :: OutKind -> SDoc -> LintM () +checkValueType :: Kind -> SDoc -> LintM () checkValueType kind doc = lintL (isTYPEorCONSTRAINT kind) (text "Non-Type-like kind when Type-like expected:" <+> ppr kind $$ text "when checking" <+> doc) ----------------- -lintArrow :: SDoc -> FunTyFlag -> InType -> InType -> InType -> LintM () +lintArrow :: SDoc -> FunTyFlag -> Type -> Type -> Type -> LintM () -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] lintArrow what af t1 t2 tw -- Eg lintArrow "type or kind `blah'" k1 k2 kw -- or lintArrow "coercion `blah'" k1 k2 kw - = do { k1 <- substTyM (typeKind t1) - ; k2 <- substTyM (typeKind t2) - ; kw <- substTyM (typeKind tw) + = do { let k1 = typeKind t1 + k2 = typeKind t2 + kw = typeKind tw ; unless (isTYPEorCONSTRAINT k1) (report (text "argument") t1 k1) ; unless (isTYPEorCONSTRAINT k2) (report (text "result") t2 k2) ; unless (isMultiplicityTy kw) (report (text "multiplicity") tw kw) @@ -2111,34 +2062,34 @@ lintTyLit (StrTyLit _) = return () lintTyLit (CharTyLit _) = return () ----------------- -lint_ty_app :: InType -> OutKind -> [InType] -> LintM () +lint_ty_app :: Type -> Kind -> [Type] -> LintM () lint_ty_app ty = lint_tyco_app (text "type" <+> quotes (ppr ty)) -lint_co_app :: HasDebugCallStack => Coercion -> OutKind -> [InType] -> LintM () +lint_co_app :: HasDebugCallStack => Coercion -> Kind -> [Type] -> LintM () lint_co_app co = lint_tyco_app (text "coercion" <+> quotes (ppr co)) -lint_tyco_app :: SDoc -> OutKind -> [InType] -> LintM () +lint_tyco_app :: SDoc -> Kind -> [Type] -> LintM () lint_tyco_app msg fun_kind arg_tys -- See Note [Avoiding compiler perf traps when constructing error messages.] - = do { _ <- lintApp msg (\ty -> do { lintType ty; substTyM ty }) - (\ty _ _ -> do { lintType ty; ki <- substTyM (typeKind ty); return (ki,()) }) - fun_kind arg_tys () + = do { _ <- lintApp msg (\ty -> do { lintType ty; return ty }) + (\ty _ _ -> do { lintType ty; return (typeKind ty,()) }) + fun_kind arg_tys () ; return () } ---------------- -lintApp :: forall in_a acc. Outputable in_a => +lintApp :: forall a acc. Outputable a => SDoc - -> (in_a -> LintM OutType) -- Lint the thing and return its value - -> (in_a -> Mult -> acc -> LintM (OutKind, acc)) -- Lint the thing and return its type - -> OutType - -> [in_a] -- The arguments, always "In" things - -> acc -- Used (only) for UsageEnv in /term/ applications - -> LintM (OutType,acc) + -> (a -> LintM Type) -- Lint the thing and return its value + -> (a -> Mult -> acc -> LintM (Kind, acc)) -- Lint the thing and return its type + -> Type + -> [a] -- The arguments + -> acc -- Used (only) for UsageEnv in /term/ applications + -> LintM (Type,acc) -- lintApp is a performance-critical function, which deals with multiple -- applications such as (/\a./\b./\c. expr) @ta @tb @tc -- When returning the type of this expression we want to avoid substituting a:=ta, -- and /then/ substituting b:=tb, etc. That's quadratic, and can be a huge --- perf hole. So we gather all the arguments [in_a], and then gather the +-- perf hole. So we gather all the arguments [a], and then gather the -- substitution incrementally in the `go` loop. -- -- lintApp is used: @@ -2158,7 +2109,7 @@ lintApp msg lint_forall_arg lint_arrow_arg !orig_fun_ty all_args acc ; let init_subst = mkEmptySubst in_scope - go :: Subst -> OutType -> acc -> [in_a] -> LintM (OutType, acc) + go :: Subst -> Type -> acc -> [a] -> LintM (Type, acc) -- The Subst applies (only) to the fun_ty -- c.f. GHC.Core.Type.piResultTys, which has a similar loop @@ -2202,7 +2153,7 @@ lintApp msg lint_forall_arg lint_arrow_arg !orig_fun_ty all_args acc -- explicitly and don't capture them as free variables. Otherwise this binder might -- become a thunk that get's allocated in the hot code path. -- See Note [Avoiding compiler perf traps when constructing error messages.] -lint_app_fail_msg :: (Outputable a2) => SDoc -> OutType -> a2 -> SDoc -> SDoc +lint_app_fail_msg :: (Outputable a2) => SDoc -> Type -> a2 -> SDoc -> SDoc lint_app_fail_msg msg kfn arg_tys extra = vcat [ hang (text "Application error in") 2 msg , nest 2 (text "Function type =" <+> ppr kfn) @@ -2215,7 +2166,7 @@ lint_app_fail_msg msg kfn arg_tys extra * * ********************************************************************* -} -lintCoreRule :: OutVar -> OutType -> CoreRule -> LintM () +lintCoreRule :: OutVar -> Type -> CoreRule -> LintM () lintCoreRule _ _ (BuiltinRule {}) = return () -- Don't bother @@ -2223,7 +2174,7 @@ lintCoreRule fun fun_ty rule@(Rule { ru_name = name, ru_bndrs = bndrs , ru_args = args, ru_rhs = rhs }) = noMultiplicityChecks $ -- Skip linearity checking for rules -- See Note [Linting linearity] - lintBinders LambdaBind bndrs $ \ _ -> + lintBinders LambdaBind bndrs $ do { (lhs_ty, _) <- lintCoreArgs (fun_ty, zeroUE) args ; (rhs_ty, _) <- case idJoinPointHood fun of JoinPoint join_arity @@ -2311,10 +2262,10 @@ Note [Join points and unfoldings/rules] in "GHC.Core.Opt.OccurAnal" for further {- Note [Asymptotic efficiency] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When linting coercions (and types actually) we return a linted -(substituted) coercion. Then we often have to take the coercionKind of -that returned coercion. If we get long chains, that can be asymptotically -inefficient, notably in +When linting coercions we traverse the coercion. Then we often have to take the +coercionKind of that returned coercion. If we get long chains, that can be +asymptotically inefficient, notably in + * TransCo * InstCo * SelCo (cf #9233) @@ -2326,30 +2277,23 @@ the bad perf bites us in practice. A solution would be to return the kind and role of the coercion, as well as the linted coercion. Or perhaps even *only* the kind and role, which is what used to happen. But that proved tricky and error prone -(#17923), so now we return the coercion. +(#17923). -} -- lintStarCoercion lints a coercion, confirming that its lh kind and -- its rh kind are both *; also ensures that the role is Nominal -- Returns the lh kind -lintStarCoercion :: InCoercion -> LintM OutType +lintStarCoercion :: Coercion -> LintM Type lintStarCoercion g = do { lintCoercion g - ; Pair t1 t2 <- substCoKindM g + ; let Pair t1 t2 = coercionKind g ; checkValueType (typeKind t1) (text "the kind of the left type in" <+> ppr g) ; checkValueType (typeKind t2) (text "the kind of the right type in" <+> ppr g) ; lintRole g Nominal (coercionRole g) ; return t1 } -substCoKindM :: InCoercion -> LintM (Pair OutType) -substCoKindM co - = do { let !(Pair lk rk) = coercionKind co - ; lk' <- substTyM lk - ; rk' <- substTyM rk - ; return (Pair lk' rk') } - -lintCoercion :: HasDebugCallStack => InCoercion -> LintM () +lintCoercion :: HasDebugCallStack => Coercion -> LintM () -- See Note [Linting types and coercions] -- -- If you edit this function, you may need to update the GHC formalism @@ -2361,7 +2305,7 @@ lintCoercion (CoVarCo cv) 2 (text "With offending type:" <+> ppr (varType cv))) | otherwise -- C.f. lintType (TyVarTy tv), which has better docs - = do { _ <- lintVarOcc cv; return () } + = lintVarOcc cv lintCoercion (Refl ty) = lintType ty lintCoercion (GRefl _r ty MRefl) = lintType ty @@ -2369,8 +2313,8 @@ lintCoercion (GRefl _r ty MRefl) = lintType ty lintCoercion (GRefl _r ty (MCo co)) = do { lintType ty ; lintCoercion co - ; tk <- substTyM (typeKind ty) - ; tl <- substTyM (coercionLKind co) + ; let tk = typeKind ty + tl = coercionLKind co ; ensureEqTys tk tl $ hang (text "GRefl coercion kind mis-match:" <+> ppr co) 2 (vcat [ppr ty, ppr tk, ppr tl]) @@ -2403,8 +2347,8 @@ lintCoercion co@(AppCo co1 co2) = do { lintCoercion co1 ; lintCoercion co2 ; let !(Pair lt1 rt1) = coercionKind co1 - ; lk1 <- substTyM (typeKind lt1) - ; rk1 <- substTyM (typeKind rt1) + lk1 = typeKind lt1 + rk1 = typeKind rt1 ; lint_co_app co lk1 [coercionLKind co2] ; lint_co_app co rk1 [coercionRKind co2] @@ -2421,7 +2365,7 @@ lintCoercion co@(ForAllCo {}) = do { _ <- go [] co; return () } where go :: [OutTyCoVar] -- Binders in reverse order - -> InCoercion -> LintM Role + -> Coercion -> LintM Role go tcvs co@(ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR , fco_kind = kind_mco, fco_body = body_co }) | not (isTyCoVar tcv) @@ -2431,15 +2375,15 @@ lintCoercion co@(ForAllCo {}) = do { mb_lk <- case kind_mco of MRefl -> return Nothing MCo kind_co -> Just <$> lintStarCoercion kind_co - ; lintTyCoBndr tcv $ \tcv' -> + ; lintTyCoBndr tcv $ do { case mb_lk of Nothing -> return () - Just lk -> ensureEqTys (varType tcv') lk $ + Just lk -> ensureEqTys (varType tcv) lk $ text "Kind mis-match in ForallCo" <+> ppr co -- I'm not very sure about this part, because it traverses body_co -- but at least it's on a cold path (a ForallCo for a CoVar) - -- Also it works on InTyCoVar and InCoercion, which is suspect + -- Also it works on InTyCoVar and Coercion, which is suspect ; when (isCoVar tcv) $ do { lintL (visL == coreTyLamForAllTyFlag && visR == coreTyLamForAllTyFlag) $ text "Invalid visibility flags in CoVar ForAllCo" <+> ppr co @@ -2448,7 +2392,7 @@ lintCoercion co@(ForAllCo {}) text "Covar can only appear in Refl and GRefl: " <+> ppr co } -- See (FC6) in Note [ForAllCo] in GHC.Core.TyCo.Rep - ; role <- go (tcv':tcvs) body_co + ; role <- go (tcv:tcvs) body_co ; when (role == Nominal) $ lintL (visL `eqForAllVis` visR) $ @@ -2505,8 +2449,8 @@ lintCoercion co@(UnivCo { uco_role = r, uco_prov = prov -- Check the to and from types ; lintType ty1 ; lintType ty2 - ; tk1 <- substTyM (typeKind ty1) - ; tk2 <- substTyM (typeKind ty2) + ; let tk1 = typeKind ty1 + tk2 = typeKind ty2 ; when (r /= Phantom && isTYPEorCONSTRAINT tk1 && isTYPEorCONSTRAINT tk2) (checkTypes ty1 ty2) @@ -2560,8 +2504,8 @@ lintCoercion (SymCo co) = lintCoercion co lintCoercion co@(TransCo co1 co2) = do { lintCoercion co1 ; lintCoercion co2 - ; rk1 <- substTyM (coercionRKind co1) - ; lk2 <- substTyM (coercionLKind co2) + ; let rk1 = coercionRKind co1 + lk2 = coercionLKind co2 ; ensureEqTys rk1 lk2 (hang (text "Trans coercion mis-match:" <+> ppr co) 2 (vcat [ppr (coercionKind co1), ppr (coercionKind co2)])) @@ -2569,7 +2513,7 @@ lintCoercion co@(TransCo co1 co2) lintCoercion the_co@(SelCo cs co) = do { lintCoercion co - ; Pair s t <- substCoKindM co + ; let Pair s t = coercionKind co ; if -- forall (both TyVar and CoVar) | Just _ <- splitForAllTyCoVar_maybe s @@ -2604,7 +2548,7 @@ lintCoercion the_co@(SelCo cs co) lintCoercion the_co@(LRCo _lr co) = do { lintCoercion co - ; Pair s t <- substCoKindM co + ; let Pair s t = coercionKind co ; lintRole co Nominal (coercionRole co) ; case (splitAppTy_maybe s, splitAppTy_maybe t) of (Just {}, Just {}) -> return () @@ -2618,14 +2562,12 @@ lintCoercion orig_co@(InstCo co arg) go (InstCo co arg) args = do { lintCoercion arg; go co (arg:args) } go co args = do { lintCoercion co ; let Pair lty rty = coercionKind co - ; lty' <- substTyM lty - ; rty' <- substTyM rty ; in_scope <- getInScope ; let subst = mkEmptySubst in_scope - ; go_args (subst, lty') (subst,rty') args } + ; go_args (subst, lty) (subst,rty) args } ------------- - go_args :: (Subst, OutType) -> (Subst,OutType) -> [InCoercion] + go_args :: (Subst, Type) -> (Subst,Type) -> [Coercion] -> LintM () go_args _ _ [] = return () @@ -2634,11 +2576,11 @@ lintCoercion orig_co@(InstCo co arg) ; go_args lty1 rty1 args } ------------- - go_arg :: (Subst, OutType) -> (Subst,OutType) -> InCoercion - -> LintM ((Subst,OutType), (Subst,OutType)) + go_arg :: (Subst, Type) -> (Subst,Type) -> Coercion + -> LintM ((Subst,Type), (Subst,Type)) go_arg (lsubst,lty) (rsubst,rty) arg = do { lintRole arg Nominal (coercionRole arg) - ; Pair arg_lty arg_rty <- substCoKindM arg + ; let Pair arg_lty arg_rty = coercionKind arg ; case (splitForAllTyCoVar_maybe lty, splitForAllTyCoVar_maybe rty) of -- forall over tvar @@ -2662,11 +2604,11 @@ lintCoercion orig_co@(InstCo co arg) lintCoercion this_co@(AxiomCo ax cos) = do { mapM_ lintCoercion cos ; lint_roles 0 (coAxiomRuleArgRoles ax) cos - ; prs <- mapM substCoKindM cos + ; let prs = map coercionKind cos ; lint_ax ax prs } where - lint_ax :: CoAxiomRule -> [Pair OutType] -> LintM () + lint_ax :: CoAxiomRule -> [Pair Type] -> LintM () lint_ax (BuiltInFamRew bif) prs = checkL (isJust (bifrw_proves bif prs)) bad_bif lint_ax (BuiltInFamInj bif) prs @@ -2754,8 +2696,8 @@ lintBranch this_co fam_tc branch arg_kinds = do { checkL (arg_kinds `equalLength` (ktvs ++ cvs)) $ (bad_ax this_co (text "lengths")) - ; subst <- getSubst - ; let empty_subst = zapSubst subst + ; in_scope <- getInScope + ; let empty_subst = mkEmptySubst in_scope ; _ <- foldlM check_ki (empty_subst, empty_subst) (zip (ktvs ++ cvs) arg_kinds) @@ -2880,12 +2822,12 @@ lint_axiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches lint_branch :: TyCon -> CoAxBranch -> LintM () lint_branch ax_tc (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs , cab_lhs = lhs_args, cab_rhs = rhs }) - = lintBinders LambdaBind (tvs ++ cvs) $ \_ -> + = lintBinders LambdaBind (tvs ++ cvs) $ do { let lhs = mkTyConApp ax_tc lhs_args ; lintType lhs ; lintType rhs - ; lhs_kind <- substTyM (typeKind lhs) - ; rhs_kind <- substTyM (typeKind rhs) + ; let lhs_kind = typeKind lhs + rhs_kind = typeKind rhs ; lintL (not (lhs_kind `typesAreApart` rhs_kind)) $ hang (text "Inhomogeneous axiom") 2 (text "lhs:" <+> ppr lhs <+> dcolon <+> ppr lhs_kind $$ @@ -2969,35 +2911,26 @@ type LintLevel = Int -- If you edit this type, you may need to update the GHC formalism -- See Note [GHC Formalism] data LintEnv - = LE { le_flags :: LintFlags -- Linting the result of this pass - , le_loc :: [LintLocInfo] -- Locations - - , le_subst :: Subst - -- Current substitution, for TyCoVars only. - -- Non-CoVar Ids don't appear in here, not even in the InScopeSet - -- Used for (a) cloning to avoid shadowing of TyCoVars, - -- so that eqType works ok - -- (b) substituting for let-bound tyvars, when we have - -- (let @a = Int -> Int in ...) - - , le_level :: LintLevel - , le_in_vars :: VarEnv (InVar, OutType, LintLevel) - -- Maps an InVar (i.e. its unique) to its binding InVar - -- and to its OutType - -- /All/ in-scope variables are here (term variables, - -- type variables, and coercion variables) - -- Used at an occurrence of the InVar + = LE { le_flags :: LintFlags -- Linting the result of this pass + , le_loc :: [LintLocInfo] -- Locations + , le_level :: LintLevel + , le_in_scope :: InScopeSet + + , le_vars :: VarEnv (Var, LintLevel) + -- Maps a Var (i.e. its unique) to its binding Var and level + -- /All/ in-scope variables are here (term variables, + -- type variables, and coercion variables) + -- So the domain is the same as the le_in_scope in-scope set + -- Used at an occurrence of the Var , le_joins :: UniqMap Id JoinOcc -- ^ Join points in scope that are valid - -- A subset of the InScopeSet in le_subst -- See Note [Join points] , le_ue_aliases :: NameEnv UsageEnv -- See Note [Linting linearity] -- Assigns usage environments to the alias-like binders, -- as found in non-recursive lets. - -- Domain is OutIds , le_platform :: Platform -- ^ Target platform , le_diagOpts :: DiagOpts -- ^ Target platform @@ -3011,7 +2944,8 @@ data LintFlags , lf_check_linearity :: Bool -- ^ See Note [Linting linearity] , lf_check_fixed_rep :: Bool -- ^ See Note [Checking for representation polymorphism] , lf_check_rubbish_lits :: Bool -- ^ See Note [Checking for rubbish literals] - , lf_allow_weak_joins :: Bool -- ^ See Note [Linting join points with casts or ticks] + , lf_allow_weak_joins :: Bool -- ^ See Note [Linting join points with casts or ticks] + , lf_allow_beta_joins :: Bool -- ^ See Note [Join points and beta-redexes] } -- See Note [Checking StaticPtrs] @@ -3078,20 +3012,6 @@ top-level bindings. See SimplCore Note [Grand plan for static forms]. The linter checks that no occurrence or `makeStatic` occurs nested. -Note [Type substitution] -~~~~~~~~~~~~~~~~~~~~~~~~ -Why do we need a type substitution? Consider - /\(a:*). \(x:a). /\(a:*). id a x -This is ill typed, because (renaming variables) it is really - /\(a:*). \(x:a). /\(b:*). id b x -Hence, when checking an application, we can't naively compare x's type -(at its binding site) with its expected type (at a use site). So we -rename type binders as we go, maintaining a substitution. - -The same substitution also supports let-type, current expressed as - (/\(a:*). body) ty -Here we substitute 'ty' for 'a' in 'body', on the fly. - Note [Linting type synonym applications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When linting a type-synonym, or type-family, application @@ -3353,12 +3273,12 @@ initL cfg m where vars = l_vars cfg init_level = 0 - env = LE { le_flags = l_flags cfg - , le_subst = mkEmptySubst (mkInScopeSetList vars) - , le_level = init_level - , le_in_vars = mkVarEnv [ (v,(v, varType v, init_level)) | v <- vars ] - , le_joins = emptyUniqMap - , le_loc = [] + env = LE { le_flags = l_flags cfg + , le_level = init_level + , le_vars = mkVarEnv [ (v,(v, init_level)) | v <- vars ] + , le_in_scope = mkInScopeSetList vars + , le_joins = emptyUniqMap + , le_loc = [] , le_ue_aliases = emptyNameEnv , le_platform = l_platform cfg , le_diagOpts = l_diagOpts cfg @@ -3421,8 +3341,7 @@ addMsg show_context env msgs msg loc_msgs :: [(SrcLoc, SDoc)] -- Innermost first loc_msgs = map dumpLoc (le_loc env) - cxt_doc = vcat [ vcat $ reverse $ map snd loc_msgs - , text "Substitution:" <+> ppr (le_subst env) ] + cxt_doc = vcat $ reverse $ map snd loc_msgs context | show_context = cxt_doc | otherwise = whenPprDebug cxt_doc @@ -3449,72 +3368,44 @@ inCasePat = LintM $ \ env errs -> fromBoxedLResult (Just (is_case_pat env), errs is_case_pat (LE { le_loc = CasePat {} : _ }) = True is_case_pat _other = False -addInScopeId :: InId -> OutType -> (OutId -> LintM a) -> LintM a +addInScopeId :: Id -> LintM a -> LintM a -- Unlike addInScopeTyCoVar, this function does no cloning; Ids never get cloned -addInScopeId in_id out_ty thing_inside +addInScopeId id thing_inside = LintM $ \ env errs -> - let !(out_id, env') = add env - in unLintM (thing_inside out_id) env' errs - + unLintM thing_inside (add env) errs where - add env@(LE { le_level = level, le_in_vars = id_vars, le_joins = valid_joins - , le_ue_aliases = aliases, le_subst = subst }) - = (out_id, env1) + add env@(LE { le_level = level, le_vars = id_vars, le_joins = valid_joins + , le_ue_aliases = aliases, le_in_scope = in_scope }) + = env { le_level = level1, le_vars = in_vars' + , le_in_scope = in_scope `extendInScopeSet` id + , le_joins = valid_joins', le_ue_aliases = aliases' } where level1 = level + 1 - env1 = env { le_level = level1, le_in_vars = in_vars' - , le_joins = valid_joins', le_ue_aliases = aliases' } - in_vars' = extendVarEnv id_vars in_id (in_id, out_ty, level1) - aliases' = delFromNameEnv aliases (idName in_id) + in_vars' = extendVarEnv id_vars id (id, level1) + aliases' = delFromNameEnv aliases (idName id) -- aliases': when shadowing an alias, we need to make sure the -- Id is no longer classified as such. E.g. -- let x = <e1> in case x of x { _DEFAULT -> <e2> } -- Occurrences of 'x' in e2 shouldn't count as occurrences of e1. - -- A very tiny optimisation, not sure if it's really worth it - -- Short-cut when the substitution is a no-op - out_id | isEmptyTCvSubst subst = in_id - | otherwise = setIdType in_id out_ty - valid_joins' - | isJoinId out_id = addToUniqMap valid_joins in_id NormalJoinOcc -- Overwrite with new arity - | otherwise = delFromUniqMap valid_joins in_id -- Remove any existing binding + | isJoinId id = addToUniqMap valid_joins id NormalJoinOcc -- Overwrite with new arity + | otherwise = delFromUniqMap valid_joins id -- Remove any existing binding -addInScopeTyCoVar :: InTyCoVar -> OutType -> (OutTyCoVar -> LintM a) -> LintM a +addInScopeTyCoVar :: TyCoVar -> LintM a -> LintM a -- This function clones to avoid shadowing of TyCoVars -addInScopeTyCoVar tcv tcv_type thing_inside - = LintM $ \ env@(LE { le_level = level, le_in_vars = in_vars, le_subst = subst }) errs -> - let (tcv', subst') = subst_bndr subst - level' = level + 1 +addInScopeTyCoVar tcv thing_inside + = LintM $ \ env@(LE { le_level = level, le_vars = in_vars + , le_in_scope = in_scope }) errs -> + let level' = level + 1 env' = env { le_level = level' - , le_in_vars = extendVarEnv in_vars tcv (tcv, tcv_type, level') - , le_subst = subst' } - in unLintM (thing_inside tcv') env' errs - where - subst_bndr subst - | isEmptyTCvSubst subst -- No change in kind - , not (tcv `elemInScopeSet` in_scope) -- Not already in scope - = -- Do not extend the substitution, just the in-scope set - (if (varType tcv `eqType` tcv_type) then (\x->x) else - pprTrace "addInScopeTyCoVar" ( - vcat [ text "tcv" <+> ppr tcv <+> dcolon <+> ppr (varType tcv) - , text "tcv_type" <+> ppr tcv_type ])) $ - (tcv, subst `extendSubstInScope` tcv) - - -- Clone, and extend the substitution - | let tcv' = uniqAway in_scope (setVarType tcv tcv_type) - = (tcv', extendTCvSubstWithClone subst tcv tcv') - where - in_scope = substInScopeSet subst - -getInVarEnv :: LintM (VarEnv (InId, OutType, LintLevel)) -getInVarEnv = LintM (\env errs -> fromBoxedLResult (Just (le_in_vars env), errs)) + , le_in_scope = in_scope `extendInScopeSet` tcv + , le_vars = extendVarEnv in_vars tcv (tcv, level') } + in unLintM thing_inside env' errs -extendTvSubstL :: TyVar -> Type -> LintM a -> LintM a -extendTvSubstL tv ty m - = LintM $ \ env errs -> - unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs +getInVarEnv :: LintM (VarEnv (Id, LintLevel)) +getInVarEnv = LintM (\env errs -> fromBoxedLResult (Just (le_vars env), errs)) markAllJoinsBad :: LintM a -> LintM a markAllJoinsBad m @@ -3549,54 +3440,42 @@ markAllJoinsBadIf False m = m getValidJoins :: LintM (UniqMap Id JoinOcc) getValidJoins = LintM (\ env errs -> fromBoxedLResult (Just (le_joins env), errs)) -getSubst :: LintM Subst -getSubst = LintM (\ env errs -> fromBoxedLResult (Just (le_subst env), errs)) - -substTyM :: InType -> LintM OutType --- Apply the substitution to the type --- The substitution is often empty, in which case it is a no-op -substTyM ty - = do { subst <- getSubst - ; return (substTy subst ty) } - getUEAliases :: LintM (NameEnv UsageEnv) getUEAliases = LintM (\ env errs -> fromBoxedLResult (Just (le_ue_aliases env), errs)) getInScope :: LintM InScopeSet -getInScope = LintM (\ env errs -> fromBoxedLResult (Just (substInScopeSet $ le_subst env), errs)) +getInScope = LintM (\ env errs -> fromBoxedLResult (Just (le_in_scope env), errs)) -lintVarOcc :: InVar -> LintM OutType +lintVarOcc :: Var -> LintM () -- Used at an occurrence of a variable: term variables, type variables, and coercion variables -- Checks -- - that it is in scope -- - that it is not a GlobalId bound by a LocalId --- - that the InType at the ocurrence matches the InType at the binding site +-- - that the Type at the ocurrence matches the Type at the binding site -- - that the variables free in its type are not shadowed at the occurrence site lintVarOcc v_occ | isGlobalId v_occ - = return (idType v_occ) + = return () | otherwise = do { in_var_env <- getInVarEnv ; case lookupVarEnv in_var_env v_occ of Nothing -> failWithL (text pp_what <+> quotes (ppr v_occ) <+> text "is out of scope") - Just (v_bndr, out_ty, bind_level) + Just (v_bndr, bind_level) -> do { let bndr_ty = idType v_bndr ; check_bad_global v_bndr ; check_occ_type_match bndr_ty - ; check_occ_type_scope in_var_env bndr_ty bind_level - ; return out_ty } - + ; check_occ_type_scope in_var_env bndr_ty bind_level } } where - occ_ty :: InType + occ_ty :: Type occ_ty = idType v_occ pp_what | isTyVar v_occ = "The type variable" | isCoVar v_occ = "The coercion variable" | otherwise = "The value variable" - check_bad_global :: InVar -> LintM () + check_bad_global :: Var -> LintM () -- 'check_bad_global' checks for the case where an /occurrence/ is -- a GlobalId, but there is an enclosing binding for a LocalId. -- NB: the in-scope variables are mostly LocalIds, checked by lintIdBndr, @@ -3616,26 +3495,26 @@ lintVarOcc v_occ | otherwise = return () - check_occ_type_match :: InType -> LintM () + check_occ_type_match :: Type -> LintM () -- Check that the type in /binder/ and the type in the /occurrence/ are the same check_occ_type_match bndr_ty - = ensureEqTys bndr_ty occ_ty $ -- Compares InTypes + = ensureEqTys bndr_ty occ_ty $ -- Compares Types mkBndrOccTypeMismatchMsg v_occ bndr_ty occ_ty - check_occ_type_scope :: VarEnv (InVar,OutType,LintLevel) -> InType -> LintLevel -> LintM () + check_occ_type_scope :: VarEnv (Var,LintLevel) -> Type -> LintLevel -> LintM () -- Check that the free vars of the binder's type -- are not shadowed at the occurrence site check_occ_type_scope in_var_env bndr_ty bind_level = checkL (null bad_fvs) $ mkBndrOccFreeVarMsg v_occ occ_ty bad_fvs where - bad_fvs :: [InVar] + bad_fvs :: [Var] bad_fvs = filter is_bad (tyCoVarsOfTypeList bndr_ty) - is_bad :: InVar -> Bool + is_bad :: Var -> Bool -- True of a variable bound inside bind_level is_bad v = case lookupVarEnv in_var_env v of - Just (_, _, v_level) -> v_level > bind_level + Just (_, v_level) -> v_level > bind_level Nothing -> True lookupJoinId :: Id -> LintM (Maybe (JoinArity, JoinOcc)) @@ -3647,21 +3526,21 @@ lookupJoinId id Just join_occ -> return $ Just (idJoinArity id, join_occ) Nothing -> return Nothing } -addAliasUE :: OutId -> UsageEnv -> LintM a -> LintM a +addAliasUE :: Id -> UsageEnv -> LintM a -> LintM a addAliasUE id ue thing_inside = LintM $ \ env errs -> let new_ue_aliases = extendNameEnv (le_ue_aliases env) (getName id) ue in unLintM thing_inside (env { le_ue_aliases = new_ue_aliases }) errs -varCallSiteUsage :: OutId -> LintM UsageEnv +varCallSiteUsage :: Id -> LintM UsageEnv varCallSiteUsage id = do m <- getUEAliases return $ case lookupNameEnv m (getName id) of Nothing -> singleUsageUE id Just id_ue -> id_ue -ensureEqTys :: OutType -> OutType -> SDoc -> LintM () +ensureEqTys :: Type -> Type -> SDoc -> LintM () -- check ty2 is subtype of ty1 (ie, has same structure but usage -- annotations need only be consistent, not equal) -- Assumes ty1,ty2 are have already had the substitution applied @@ -3885,7 +3764,7 @@ mkLetErr bndr rhs hang (text "Rhs:") 4 (ppr rhs)] -mkTyAppMsg :: OutType -> Type -> SDoc +mkTyAppMsg :: Type -> Type -> SDoc mkTyAppMsg ty arg_ty = vcat [text "Illegal type application:", hang (text "Function type:") @@ -4006,13 +3885,13 @@ mkJoinBndrOccMismatchMsg bndr join_arity_bndr join_arity_occ , text "Arity at binding site:" <+> ppr join_arity_bndr , text "Arity at occurrence: " <+> ppr join_arity_occ ] -mkBndrOccTypeMismatchMsg :: InVar -> InType -> InType -> SDoc +mkBndrOccTypeMismatchMsg :: Var -> Type -> Type -> SDoc mkBndrOccTypeMismatchMsg var bndr_ty occ_ty = vcat [ text "Mismatch in type between binder and occurrence" , text "Binder: " <+> ppr var <+> dcolon <+> ppr bndr_ty , text "Occurrence:" <+> ppr var <+> dcolon <+> ppr occ_ty ] -mkBndrOccFreeVarMsg :: InVar -> InType -> [TyCoVar] -> SDoc +mkBndrOccFreeVarMsg :: Var -> Type -> [TyCoVar] -> SDoc mkBndrOccFreeVarMsg var occ_ty bad_tvs = vcat [ text "Free vars of type are shadowed:" <+> ppr bad_tvs , text "Occurrence:" <+> ppr var <+> dcolon <+> ppr occ_ty ] ===================================== compiler/GHC/Core/Lint/SubstTypeLets.hs ===================================== @@ -0,0 +1,140 @@ +{- +(c) The University of Glasgow 2006 +(c) The GRASP/AQUA Project, Glasgow University, 1993-1998 +-} + +module GHC.Core.Lint.SubstTypeLets( + substTypeLets + ) where + +import GHC.Prelude + +import GHC.Core +import GHC.Core.Subst +import GHC.Core.Utils( mkInScopeSetBndrs ) + +import GHC.Types.Var + +import GHC.Utils.Misc( mapSnd ) +import GHC.Utils.Outputable +import GHC.Utils.Panic + +{- Note [Substituting type-lets] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When desugaring pattern matching we really, really need non-Lint-acceptable type-lets. +Suppose we have + f (MkT a (Just a (x::a)) (y::a)) = rhs1 + f (MkT b (Nothing b) (z::b)) = rhs2 +where + MkT :: ∀ a. Maybe a -> a -> T + +We desugar this to + f x = case x of + MkT w (v :: Maybe w) (p:w) + -> let { a=w, b=w } + in let { y:a=p, z:b=p } + in case v of + Just a (x:a) -> rhs1 [y::a] + Nothing b -> rhs2 [z::b] + +Look at those type-lets { a=w, b=w }. They make the type variables in the +/two/ separately-typechecked clauses for `f` line up with the /single/ pattern +match on `x`, which binds the type variable `w`. + +Key point: the body of the let is only type-correct /after/ substituting +a:=w, b:=w. Even the next let, { y:a=p } isn't type-correct without that +substitution, because (p:w). + +So the `substTypeLets` pass does this: + - It runs as part of Lint, as a pre-pass before the main Lint + - It runs only when we are Linting the output of the desugarer + - The result of substTypeLets is discarded after linting + +When it finds a nested type-let + let @a = ty in body +it substitutes a:=ty in `body` + +Wrinkles + +(STL1) It only substitutes /nested/ type-lets, not top level. + +(STL2) You might think that we'd run it unconditionally, after desugaring. But actually, + the Simplifier (or SimpleOpt) will deal with these type-lets, so it is just Lint + that we must placate. We don't want to incur the cost of this pass except when + we are Linting. + + TL;DR: we do substTypeLets as a pre-pass to the Lint pass that immediately follows + desugaring. See `GHC.Core.lintPassResult`, and the `lpr_preSubst` field in + `LintPassResultConfig`. + +(STL3) Should `substTypeLets` process (stable) unfoldings? It does not need to + because all unfoldings have `simpleOptExpr` applied to them, so the tricky + type-lets will already be substituted. + + Of course we stil need to apply the current substitution, but that is done + automatically by `substBndr`. +-} + +substTypeLets :: CoreProgram -> CoreProgram +substTypeLets binds = map stl_top binds + where + stl_top (NonRec b r) = NonRec b (stlExpr empty_subst r) + stl_top (Rec prs) = Rec (mapSnd (stlExpr empty_subst) prs) + + empty_subst = mkEmptySubst $ + mkInScopeSetBndrs binds + +---------------------- +stlBind :: Subst -> CoreBind -> (Subst, CoreBind) +stlBind subst (Rec prs) + = assertPpr (not (any isTyVar bndrs)) (ppr prs) $ + (subst', Rec prs') + where + (bndrs,rhss) = unzip prs + (subst', bndrs') = substRecBndrs subst bndrs + -- substRecBndrs: see (STL3) in Note [Substituting type-lets] + rhss' = map (stlExpr subst') rhss + prs' = bndrs' `zip` rhss' + +stlBind subst (NonRec bndr rhs) + = (subst', NonRec bndr' (stlExpr subst rhs)) + where + (subst', bndr') = substBndr subst bndr + -- substBndr: see (STL3) in Note [Substituting type-lets] + +---------------------- +stlExpr :: Subst -> CoreExpr -> CoreExpr + +stlExpr subst (Let (NonRec tv (Type ty)) body) + = -- This equation is the main payload of the entire pass! + stlExpr (extendTvSubst subst tv (substTy subst ty)) body + +stlExpr subst (Let bind body) + = Let bind' (stlExpr subst' body) + where + (subst', bind') = stlBind subst bind + +stlExpr subst (Lam bndr body) + = Lam bndr' (stlExpr subst' body) + where + (subst', bndr') = substBndr subst bndr + +stlExpr subst (Case scrut bndr ty alts) + = Case (stlExpr subst scrut) bndr' (substTy subst ty) + (map stl_alt alts) + where + (subst', bndr') = substBndr subst bndr + + stl_alt (Alt con bndrs rhs) + = Alt con bndrs' (stlExpr subst'' rhs) + where + (subst'', bndrs') = substBndrs subst' bndrs + +-- Simple cases +stlExpr _ (Lit l) = Lit l +stlExpr subst (Var v) = lookupIdSubst subst v +stlExpr subst (App e1 e2) = App (stlExpr subst e1) (stlExpr subst e2) +stlExpr subst (Type ty) = Type (substTy subst ty) +stlExpr subst (Tick t e) = Tick (substTickish subst t) (stlExpr subst e) +stlExpr subst (Cast e co) = Cast (stlExpr subst e) (substCo subst co) +stlExpr subst (Coercion co) = Coercion (substCo subst co) ===================================== compiler/GHC/Core/Opt/OccurAnal.hs ===================================== @@ -2676,6 +2676,8 @@ occAnalArgs :: OccEnv -> CoreExpr -> [CoreExpr] -> WithUsageDetails CoreExpr -- The `fun` argument is just an accumulating parameter, -- the base for building the application we return +-- +-- We have applied markAllNonTail to the returned usage-details occAnalArgs env fun args one_shots = go emptyDetails fun args one_shots where @@ -2686,7 +2688,9 @@ occAnalArgs env fun args one_shots encl | Var f <- fun, isDeadEndSig (idDmdSig f) = OccScrut | otherwise = OccVanilla - go uds fun [] _ = WUD uds fun + go uds fun [] _ = WUD (markAllNonTail uds) fun + -- markAllNonTail: calls in arguments are not tail calls! + go uds fun (arg:args) one_shots = go (uds `andUDs` arg_uds) (fun `App` arg') args one_shots' where @@ -2778,8 +2782,7 @@ occAnalApp env (Var fun_id, args, ticks) all_uds = fun_uds `andUDs` final_args_uds - !final_args_uds = markAllNonTail $ - markAllInsideLamIf (isRhsEnv env && is_exp) $ + !final_args_uds = markAllInsideLamIf (isRhsEnv env && is_exp) $ -- isRhsEnv: see Note [OccEncl] args_uds -- We mark the free vars of the argument of a constructor or PAP @@ -2809,20 +2812,27 @@ occAnalApp env (Var fun_id, args, ticks) -- See Note [Sources of one-shot information], bullet point A'] occAnalApp env (fun, args, ticks) - = let app_out = mkTicks ticks app' - in WUD (markAllNonTail (fun_uds `andUDs` args_uds)) app_out - + = WUD (fun_uds `andUDs` args_uds) (mkTicks ticks app') where !(WUD args_uds app') = occAnalArgs env fun' args [] - !(WUD fun_uds fun') = occAnal (addAppCtxt env args) fun - -- The addAppCtxt is a bit cunning. One iteration of the simplifier - -- often leaves behind beta redexes like - -- (\x y -> e) a1 a2 - -- Here we would like to mark x,y as one-shot, and treat the whole - -- thing much like a let. We do this by pushing some OneShotLam items - -- onto the context stack. + !(WUD fun_uds fun') = go_fun env fun args + + -- See (A2) in Note [occAnal for applications] + go_fun env (Lam bndr body) (_ : args) + = addInScopeOne env bndr $ \ env' -> + let !(WUD body_uds body') = go_fun env' body args + !bndr' = tagLamBinder body_uds bndr + in WUD body_uds (Lam bndr' body') + go_fun env fun args + | null args + = occAnal env fun + | otherwise + = let !env' = addAppCtxt env args + !(WUD fun_uds fun') = occAnal env' fun + in WUD (markAllNonTail fun_uds) fun' addAppCtxt :: OccEnv -> [Arg CoreBndr] -> OccEnv +-- See (A3) in Note [occAnal for applications] addAppCtxt env@(OccEnv { occ_one_shots = ctxt }) args | n_val_args > 0 = env { occ_one_shots = replicate n_val_args OneShotLam ++ ctxt @@ -2834,8 +2844,40 @@ addAppCtxt env@(OccEnv { occ_one_shots = ctxt }) args where n_val_args = valArgCount args +{- Note [occAnal for applications] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +One iteration of the simplifier sometimes leaves behind beta redexes like + (\x y -> e) a1 a2 +This happens particularly in worker/wrapper; see Note [Join points and beta-redexes] +in GHC.Core.Lint. In these cases there are three things we want to take care of +in the occurrence analyser: + +(A1) We don't want to mark variables inside `e` as `InsideLam`; that would just + delay inlining them for another iteration of the Simplifier. + +(A2) If there is a join-point invocation inside `e`, we don't want to complain about + lost join points. See Note [Join points and beta-redexes] in GHC.Core.Lint for + more detail. + +(A3) Suppose we have something like + (case e of (a,b) -> (\x.blah) |> co) arg + which can happen during 'gentle' simplification when we don't do case-of-case, + not push arguments into cases. Then we'd still like to mark that lambda + as one-shot, so that things can get inlined inside it. We can to this + by pushing OneShotLam items onto the context stack. + + Live example: `read_tup4` in test CoOpt_Read. + +How we address these: + +* (A2): we focus narrowly on visible beta-redexes ((\x.e) arg), since that + is what is needed for Note [Join points and beta-redexes]. We do this + via the `go_fun` loop in `occAnalApp`. + +* (A1) and (A3): for visible beta-redexes, the `go_fun` loop does the job. + But for less-visible ones, like in (A3) we push `OneShotLam` items onto + the context stack, in `addAppCtxt`. -{- Note [Sources of one-shot information] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The occurrence analyser obtains one-shot-lambda information from two sources: ===================================== compiler/GHC/Core/Opt/WorkWrap/Utils.hs ===================================== @@ -241,10 +241,10 @@ mkWwBodies opts fun_id ww_arity arg_vars res_ty demands res_cpr = (work_args, work_args, work_marks) call_work work_fn = mkVarApps (Var work_fn) work_call_args - call_rhs fn_rhs = mkAppsBeta fn_rhs fn_args - -- See Note [Join points and beta-redexes] + call_rhs fn_rhs = mkApps fn_rhs fn_args + -- See Note [Join points and beta-redexes] in GHC.Core.Lint wrapper_body = mkLams cloned_arg_vars . wrap_fn_cpr . wrap_fn_str . call_work - -- See Note [Call-by-value for worker args] + -- See Note [Call-by-value for worker args] work_seq_str_flds = mkStrictFieldSeqs (zip work_lam_args work_call_str) worker_body = mkLams work_lam_args . work_seq_str_flds . work_fn_cpr . call_rhs worker_args_dmds= [ idDemandInfo v | v <- work_call_args, isId v] @@ -280,14 +280,6 @@ mkWwBodies opts fun_id ww_arity arg_vars res_ty demands res_cpr arity_ok | isJoinId fun_id = ww_arity <= n_dmds | otherwise = ww_arity == n_dmds --- | Version of 'GHC.Core.mkApps' that does beta reduction on-the-fly. --- PRECONDITION: The arg expressions are not free in any of the lambdas binders. -mkAppsBeta :: CoreExpr -> [CoreArg] -> CoreExpr --- The precondition holds for our call site in mkWwBodies, because all the FVs --- of as are either cloned_arg_vars (and thus fresh) or fresh worker args. -mkAppsBeta (Lam b body) (a:as) = bindNonRec b a $! mkAppsBeta body as -mkAppsBeta f as = mkApps f as - -- See Note [Limit w/w arity] isWorkerSmallEnough :: Int -> Int -> [Var] -> Bool isWorkerSmallEnough max_worker_args old_n_args vars @@ -525,36 +517,6 @@ Solution is simple: put the void argument /last/: c.f Note [SpecConstr void argument insertion] in GHC.Core.Opt.SpecConstr -Note [Join points and beta-redexes] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Originally, the worker would invoke the original function by calling it with -arguments, thus producing a beta-redex for the simplifier to munch away: - - \x y z -> e => (\x y z -> e) wx wy wz - -Now that we have special rules about join points, however, this is Not Good if -the original function is itself a join point, as then it may contain invocations -of other join points: - - join j1 x = ... - join j2 y = if y == 0 then 0 else j1 y - - => - - join j1 x = ... - join $wj2 y# = let wy = I# y# in (\y -> if y == 0 then 0 else jump j1 y) wy - join j2 y = case y of I# y# -> jump $wj2 y# - -There can't be an intervening lambda between a join point's declaration and its -occurrences, so $wj2 here is wrong. But of course, this is easy enough to fix: - - ... - let join $wj2 y# = let wy = I# y# in let y = wy in if y == 0 then 0 else j1 y - ... - -Hence we simply do the beta-reduction here. (This would be harder if we had to -worry about hygiene, but luckily wy is freshly generated.) - Note [Freshen WW arguments] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ When we do a worker/wrapper split, we must freshen the arg vars of the original ===================================== compiler/GHC/Core/Subst.hs ===================================== @@ -13,7 +13,8 @@ module GHC.Core.Subst ( -- ** Substituting into expressions and related types deShadowBinds, substRuleInfo, substRulesForImportedIds, - substTyUnchecked, substCo, substExpr, substExprSC, substBind, substBindSC, + substTy, substTyUnchecked, substCo, + substExpr, substExprSC, substBind, substBindSC, substUnfolding, substUnfoldingSC, lookupIdSubst, lookupIdSubst_maybe, substIdType, substIdOcc, substTickish, substDVarSet, substIdInfo, @@ -42,8 +43,7 @@ import GHC.Core.FVs import GHC.Core.Seq import GHC.Core.Utils - -- We are defining local versions -import GHC.Core.Type hiding ( substTy ) +import GHC.Core.Type import GHC.Core.Coercion( mkCoVarCo, substCoVarBndr ) import GHC.Core.TyCo.FVs ===================================== compiler/GHC/Driver/Config/Core/Lint.hs ===================================== @@ -1,7 +1,6 @@ module GHC.Driver.Config.Core.Lint ( endPass , endPassHscEnvIO - , lintCoreBindings , initEndPassConfig , initLintPassResultConfig , initLintConfig @@ -50,16 +49,6 @@ endPassHscEnvIO hsc_env name_ppr_ctx pass binds rules binds rules } --- | Type-check a 'CoreProgram'. See Note [Core Lint guarantee]. -lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> WarnsAndErrs -lintCoreBindings dflags coreToDo vars -- binds - = lintCoreBindings' $ LintConfig - { l_diagOpts = initDiagOpts dflags - , l_platform = targetPlatform dflags - , l_flags = perPassFlags dflags coreToDo - , l_vars = vars - } - initEndPassConfig :: DynFlags -> [Var] -> NamePprCtx -> CoreToDo -> EndPassConfig initEndPassConfig dflags extra_vars name_ppr_ctx pass = EndPassConfig { ep_dumpCoreSizes = not (gopt Opt_SuppressCoreSizes dflags) @@ -104,10 +93,17 @@ initLintPassResultConfig dflags extra_vars pass = LintPassResultConfig { lpr_diagOpts = initDiagOpts dflags , lpr_platform = targetPlatform dflags , lpr_makeLintFlags = perPassFlags dflags pass - , lpr_passPpr = ppr pass + , lpr_passPpr = ppr pass + , lpr_preSubst = doPreSubst pass , lpr_localsInScope = extra_vars } +doPreSubst :: CoreToDo -> Bool +doPreSubst CoreDesugar = True -- Output of desugarer, /before/ running any optimisation, + -- not even simpleOpt. See Note Note [Substituting type-lets] + -- in GHC.Core.SubstTypeLets +doPreSubst _ = False + perPassFlags :: DynFlags -> CoreToDo -> LintFlags perPassFlags dflags pass = (defaultLintFlags dflags) @@ -116,7 +112,8 @@ perPassFlags dflags pass , lf_check_static_ptrs = check_static_ptrs , lf_check_linearity = check_linearity , lf_check_rubbish_lits = check_rubbish - , lf_allow_weak_joins = allow_weak_joins } + , lf_allow_weak_joins = allow_weak_joins + , lf_allow_beta_joins = allow_beta_joins } where -- See Note [Checking for global Ids] check_globals = case pass of @@ -158,6 +155,11 @@ perPassFlags dflags pass CorePrep -> True _ -> False + -- See Note [Join points and beta-redexes] in GHC.Core.Lint + allow_beta_joins = case pass of + CoreDoWorkerWrapper -> True + _ -> False + initLintConfig :: DynFlags -> [Var] -> LintConfig initLintConfig dflags vars =LintConfig { l_diagOpts = initDiagOpts dflags @@ -175,4 +177,5 @@ defaultLintFlags dflags = LF { lf_check_global_ids = False , lf_check_fixed_rep = True , lf_check_rubbish_lits = True , lf_allow_weak_joins = False + , lf_allow_beta_joins = False } ===================================== compiler/ghc.cabal.in ===================================== @@ -361,6 +361,7 @@ Library GHC.Core.InstEnv GHC.Core.Lint GHC.Core.Lint.Interactive + GHC.Core.Lint.SubstTypeLets GHC.Core.LateCC GHC.Core.LateCC.Types GHC.Core.LateCC.TopLevelBinds ===================================== testsuite/tests/corelint/LintEtaExpand.stderr ===================================== @@ -1,32 +1,16 @@ <no location info>: warning: • The first argument of ‘coerce’ does not have a fixed runtime representation: a :: TYPE k - Substitution: <InScope = {a q} - IdSubst = [] - TvSubst = [] - CvSubst = []> in coerce BAD 1 <no location info>: warning: • The first argument of ‘coerce’ does not have a fixed runtime representation: ‘q’ is not concrete. - Substitution: <InScope = {a q} - IdSubst = [] - TvSubst = [] - CvSubst = []> in coerce BAD 2 <no location info>: warning: • The result of the first argument of the primop ‘catch#’ does not have a fixed runtime representation: a :: TYPE q - Substitution: <InScope = {a q} - IdSubst = [] - TvSubst = [] - CvSubst = []> in catch# BAD 1 <no location info>: warning: • The result of the first argument of the primop ‘catch#’ does not have a fixed runtime representation: ‘q’ is not concrete. - Substitution: <InScope = {a q} - IdSubst = [] - TvSubst = [] - CvSubst = []> in catch# BAD 2 ===================================== testsuite/tests/corelint/T21115b.stderr ===================================== @@ -6,10 +6,6 @@ T21115b.hs:9:1: warning: In the body of lambda with binder ds :: Double# In the body of a let with binder fail :: (# #) -> Int# In the body of a let with binder fail :: (# #) -> Int# - Substitution: <InScope = {} - IdSubst = [] - TvSubst = [] - CvSubst = []> *** Offending Program *** Rec { $trModule = Module (TrNameS "main"#) (TrNameS "T21115b"#) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3d5c2a1d6748ca82d85dfed368315612... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3d5c2a1d6748ca82d85dfed368315612... You're receiving this email because of your account on gitlab.haskell.org.
participants (1)
-
Simon Peyton Jones (＠simonpj)