GitLab

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

78434e8c

by Simon Peyton Jones at 2026-04-17T22:30:38-04: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)
 (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)
 (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)
 (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")
 (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:")
 (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

 +{-
 +(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

  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

  <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"#)