From 59202c800f2c97c16906120ab2561f6e1556e4af Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sebastian.graf@kit.edu>
Date: Fri, 31 Mar 2023 17:35:22 +0200
Subject: [PATCH] CorePrep: Eliminate EmptyCase and unsafeEqualityProof in
 CoreToStg instead

We eliminate EmptyCase by way of `coreToStg (Case e _ _ []) = coreToStg e` now.
The main reason is that it plays far better in conjunction with eta expansion
(as we aim to do for arguments in CorePrep, #23083), because we can discard
any arguments, `(case e of {}) eta == case e of {}`, whereas in `(e |> co) eta`
it's impossible to discard the argument.

We do also give the same treatment to unsafeCoerce proofs and treat them as
trivial iff their RHS is trivial.

It is also both much simpler to describe than the previous mechanism of emitting
an unsafe coercion and simpler to implement, removing quite a bit of commentary
and `CorePrepProv`.

In the ghc/alloc perf test `LargeRecord`, we introduce an additional Simplifier
iteration due to #17910. E.g., FloatOut produces a binding
```
lvl_s6uK [Occ=Once1] :: GHC.Types.Int
[LclId]
lvl_s6uK = GHC.Types.I# 2#

lvl_s6uL [Occ=Once1] :: GHC.Types.Any
[LclId]
lvl_s6uL
  = case Unsafe.Coerce.unsafeEqualityProof ... of
    { Unsafe.Coerce.UnsafeRefl v2_i6tr -> lvl_s6uK `cast` (... v2_i6tr ...)
    }
```
That occurs once and hence is pre-inlined unconditionally in the next Simplifier
pass. It's non-trivial to find a way around that, but not really harmful
otherwise. Hence we accept a 1.2% increase on some architectures.

Metric Increase:
    LargeRecord
---
 compiler/GHC/Core.hs                    |  10 +-
 compiler/GHC/Core/Coercion.hs           |   4 -
 compiler/GHC/Core/Coercion/Opt.hs       |   1 -
 compiler/GHC/Core/FVs.hs                |   2 -
 compiler/GHC/Core/Lint.hs               |  13 +-
 compiler/GHC/Core/Opt/SetLevels.hs      |  27 ++-
 compiler/GHC/Core/Opt/Simplify/Utils.hs |  12 ++
 compiler/GHC/Core/TyCo/FVs.hs           |   9 +-
 compiler/GHC/Core/TyCo/Rep.hs           |   7 -
 compiler/GHC/Core/TyCo/Subst.hs         |   1 -
 compiler/GHC/Core/TyCo/Tidy.hs          |   1 -
 compiler/GHC/Core/Type.hs               |   2 -
 compiler/GHC/Core/Unfold.hs             |  13 +-
 compiler/GHC/Core/Utils.hs              |  34 +++-
 compiler/GHC/CoreToIface.hs             |   1 -
 compiler/GHC/CoreToStg.hs               | 111 +++++-----
 compiler/GHC/CoreToStg/Prep.hs          | 256 ++++--------------------
 compiler/GHC/Iface/Syntax.hs            |   1 -
 compiler/GHC/Iface/Type.hs              |   9 -
 compiler/GHC/IfaceToCore.hs             |   1 -
 compiler/GHC/StgToCmm/Expr.hs           |   3 +-
 compiler/GHC/Tc/TyCl/Utils.hs           |   1 -
 compiler/GHC/Tc/Utils/TcMType.hs        |   1 -
 compiler/GHC/Utils/Trace.hs             |   4 +
 libraries/base/Unsafe/Coerce.hs         |  40 ++--
 25 files changed, 201 insertions(+), 363 deletions(-)

diff --git a/compiler/GHC/Core.hs b/compiler/GHC/Core.hs
index 0aa89011ca50..f856b5133293 100644
--- a/compiler/GHC/Core.hs
+++ b/compiler/GHC/Core.hs
@@ -725,9 +725,13 @@ this exhaustive list can be empty!
   its scrutinee is (see GHC.Core.Utils.exprIsTrivial).  This is actually
   important; see Note [Empty case is trivial] in GHC.Core.Utils
 
-* An empty case is replaced by its scrutinee during the CoreToStg
-  conversion; remember STG is un-typed, so there is no need for
-  the empty case to do the type conversion.
+* We lower empty cases in GHC.CoreToStg.coreToStgExpr to an eval on the
+  scrutinee.
+
+Historical Note: We used to lower EmptyCase in CorePrep by way of an
+unsafeCoercion on the scrutinee, but that yielded panics in CodeGen when
+we were beginning to eta expand in arguments, plus required to mess with
+heterogenously-kinded coercions. It's simpler to stick to it just a bit longer.
 
 Note [Join points]
 ~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 9000e7a399e9..5f842bb66d49 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -1395,8 +1395,6 @@ setNominalRole_maybe r co
       | case prov of PhantomProv _    -> False  -- should always be phantom
                      ProofIrrelProv _ -> True   -- it's always safe
                      PluginProv _     -> False  -- who knows? This choice is conservative.
-
-                     CorePrepProv _   -> True
       = Just $ UnivCo prov Nominal co1 co2
     setNominalRole_maybe_helper _ = Nothing
 
@@ -1522,7 +1520,6 @@ promoteCoercion co = case co of
     UnivCo (PhantomProv kco)    _ _ _ -> kco
     UnivCo (ProofIrrelProv kco) _ _ _ -> kco
     UnivCo (PluginProv _)       _ _ _ -> mkKindCo co
-    UnivCo (CorePrepProv _)     _ _ _ -> mkKindCo co
 
     SymCo g
       -> mkSymCo (promoteCoercion g)
@@ -2346,7 +2343,6 @@ seqProv :: UnivCoProvenance -> ()
 seqProv (PhantomProv co)    = seqCo co
 seqProv (ProofIrrelProv co) = seqCo co
 seqProv (PluginProv _)      = ()
-seqProv (CorePrepProv _)    = ()
 
 seqCos :: [Coercion] -> ()
 seqCos []       = ()
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 44a381259801..3ffbcecda4de 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -630,7 +630,6 @@ opt_univ env sym prov role oty1 oty2
 #endif
       ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
       PluginProv _       -> prov
-      CorePrepProv _     -> prov
 
 -------------
 opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
diff --git a/compiler/GHC/Core/FVs.hs b/compiler/GHC/Core/FVs.hs
index 225bc0596029..2c268e878a2a 100644
--- a/compiler/GHC/Core/FVs.hs
+++ b/compiler/GHC/Core/FVs.hs
@@ -411,7 +411,6 @@ orphNamesOfProv :: UnivCoProvenance -> NameSet
 orphNamesOfProv (PhantomProv co)    = orphNamesOfCo co
 orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co
 orphNamesOfProv (PluginProv _)      = emptyNameSet
-orphNamesOfProv (CorePrepProv _)    = emptyNameSet
 
 orphNamesOfCos :: [Coercion] -> NameSet
 orphNamesOfCos = orphNamesOfThings orphNamesOfCo
@@ -799,4 +798,3 @@ freeVars = go
 
     go (Type ty)     = (tyCoVarsOfTypeDSet ty, AnnType ty)
     go (Coercion co) = (tyCoVarsOfCoDSet co, AnnCoercion co)
-
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index e889564715e3..e0a816e24f1d 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -2398,9 +2398,6 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
 
        -- see #9122 for discussion of these checks
      checkTypes t1 t2
-       | allow_ill_kinded_univ_co prov
-       = return ()  -- Skip kind checks
-       | otherwise
        = do { checkWarnL fixed_rep_1
                          (report "left-hand type does not have a fixed runtime representation")
             ; checkWarnL fixed_rep_2
@@ -2418,13 +2415,6 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
          reps1 = typePrimRep t1
          reps2 = typePrimRep t2
 
-     -- CorePrep deliberately makes ill-kinded casts
-     --  e.g (case error @Int "blah" of {}) :: Int#
-     --     ==> (error @Int "blah") |> Unsafe Int Int#
-     -- See Note [Unsafe coercions] in GHC.Core.CoreToStg.Prep
-     allow_ill_kinded_univ_co (CorePrepProv homo_kind) = not homo_kind
-     allow_ill_kinded_univ_co _                        = False
-
      validateCoercion :: PrimRep -> PrimRep -> LintM ()
      validateCoercion rep1 rep2
        = do { platform <- getPlatform
@@ -2454,8 +2444,7 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
             ; check_kinds kco k1 k2
             ; return (ProofIrrelProv kco') }
 
-     lint_prov _ _ prov@(PluginProv _)   = return prov
-     lint_prov _ _ prov@(CorePrepProv _) = return prov
+     lint_prov _ _ prov@(PluginProv _) = return prov
 
      check_kinds kco k1 k2
        = do { let Pair k1' k2' = coercionKind kco
diff --git a/compiler/GHC/Core/Opt/SetLevels.hs b/compiler/GHC/Core/Opt/SetLevels.hs
index 185da7df526e..93e9bf073ef7 100644
--- a/compiler/GHC/Core/Opt/SetLevels.hs
+++ b/compiler/GHC/Core/Opt/SetLevels.hs
@@ -1041,18 +1041,25 @@ notWorthFloating :: CoreExpr -> [Var] -> Bool
 notWorthFloating e abs_vars
   = go e (count isId abs_vars)
   where
-    go (Var {}) n    = n >= 0
-    go (Lit lit) n   = assert (n==0) $
-                       litIsTrivial lit   -- Note [Floating literals]
-    go (Tick t e) n  = not (tickishIsCode t) && go e n
-    go (Cast e _)  n = go e n
+    go (Var {}) n               = n >= 0
+    go (Lit lit) n              = assert (n==0) $
+                                  litIsTrivial lit   -- Note [Floating literals]
+    go (Type {}) _              = True
+    go (Coercion {}) _          = True
     go (App e arg) n
        -- See Note [Floating applications to coercions]
-       | Type {} <- arg    = go e n
-       | n==0              = False
-       | exprIsTrivial arg = go e (n-1)
-       | otherwise         = False
-    go _ _                 = False
+       | not (isRuntimeArg arg) = go e n
+       | n==0                   = False
+       | exprIsTrivial arg      = go e (n-1) -- NB: exprIsTrivial arg = go arg 0
+       | otherwise              = False
+    go (Tick t e) n             = not (tickishIsCode t) && go e n
+    go (Cast e _)  n            = go e n
+    go (Case e b _ as) n
+      | null as
+      = go e n     -- See Note [Empty case is trivial]
+      | Just rhs <- isUnsafeEqualityCase e b as
+      = go rhs n   -- See (U2) of Note [Implementing unsafeCoerce] in base:Unsafe.Coerce
+    go _ _                      = False
 
 {-
 Note [Floating literals]
diff --git a/compiler/GHC/Core/Opt/Simplify/Utils.hs b/compiler/GHC/Core/Opt/Simplify/Utils.hs
index c56d86d6ceff..1dd4881355f9 100644
--- a/compiler/GHC/Core/Opt/Simplify/Utils.hs
+++ b/compiler/GHC/Core/Opt/Simplify/Utils.hs
@@ -1471,6 +1471,18 @@ preInlineUnconditionally env top_lvl bndr rhs rhs_env
     -- simplifications).  Until phase zero we take no special notice of
     -- top level things, but then we become more leery about inlining
     -- them.
+    --
+    -- What exactly to check in `early_phase` above is the subject of #17910.
+    --
+    -- !10088 introduced an additional Simplifier iteration in LargeRecord
+    -- because we first FloatOut `case unsafeEqualityProof of ... -> I# 2#`
+    -- (a non-trivial value) which we immediately inline back in.
+    -- Ideally, we'd never have inlined it because the binding turns out to
+    -- be expandable; unfortunately we need an iteration of the Simplifier to
+    -- attach the proper unfolding and can't check isExpandableUnfolding right
+    -- here.
+    -- (Nor can we check for `exprIsExpandable rhs`, because that needs to look
+    -- at the non-existent unfolding for the `I# 2#` which is also floated out.)
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index 3dd1759a347a..14bf82e170f9 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -661,7 +661,6 @@ tyCoFVsOfProv :: UnivCoProvenance -> FV
 tyCoFVsOfProv (PhantomProv co)    fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfProv (PluginProv _)      fv_cand in_scope acc = emptyFV fv_cand in_scope acc
-tyCoFVsOfProv (CorePrepProv _)    fv_cand in_scope acc = emptyFV fv_cand in_scope acc
 
 tyCoFVsOfCos :: [Coercion] -> FV
 tyCoFVsOfCos []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
@@ -731,8 +730,7 @@ almost_devoid_co_var_of_prov (PhantomProv co) cv
   = almost_devoid_co_var_of_co co cv
 almost_devoid_co_var_of_prov (ProofIrrelProv co) cv
   = almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_prov (PluginProv _)   _ = True
-almost_devoid_co_var_of_prov (CorePrepProv _) _ = True
+almost_devoid_co_var_of_prov (PluginProv _) _ = True
 
 almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
 almost_devoid_co_var_of_type (TyVarTy _) _ = True
@@ -1132,9 +1130,6 @@ tyConsOfType ty
      go_prov (PhantomProv co)    = go_co co
      go_prov (ProofIrrelProv co) = go_co co
      go_prov (PluginProv _)      = emptyUniqSet
-     go_prov (CorePrepProv _)    = emptyUniqSet
-        -- this last case can happen from the tyConsOfType used from
-        -- checkTauTvUpdate
 
      go_cos cos   = foldr (unionUniqSets . go_co)  emptyUniqSet cos
 
@@ -1346,5 +1341,3 @@ occCheckExpand vs_to_avoid ty
     go_prov cxt (PhantomProv co)    = PhantomProv <$> go_co cxt co
     go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
     go_prov _   p@(PluginProv _)    = return p
-    go_prov _   p@(CorePrepProv _)  = return p
-
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index af86de998f5b..f85ca8f90f0a 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -1529,17 +1529,12 @@ data UnivCoProvenance
   | PluginProv String  -- ^ From a plugin, which asserts that this coercion
                        --   is sound. The string is for the use of the plugin.
 
-  | CorePrepProv       -- See Note [Unsafe coercions] in GHC.Core.CoreToStg.Prep
-      Bool   -- True  <=> the UnivCo must be homogeneously kinded
-             -- False <=> allow hetero-kinded, e.g. Int ~ Int#
-
   deriving Data.Data
 
 instance Outputable UnivCoProvenance where
   ppr (PhantomProv _)    = text "(phantom)"
   ppr (ProofIrrelProv _) = text "(proof irrel.)"
   ppr (PluginProv str)   = parens (text "plugin" <+> brackets (text str))
-  ppr (CorePrepProv _)   = text "(CorePrep)"
 
 -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
 data CoercionHole
@@ -1861,7 +1856,6 @@ foldTyCo (TyCoFolder { tcf_view       = view
     go_prov env (PhantomProv co)    = go_co env co
     go_prov env (ProofIrrelProv co) = go_co env co
     go_prov _   (PluginProv _)      = mempty
-    go_prov _   (CorePrepProv _)    = mempty
 
 -- | A view function that looks through nothing.
 noView :: Type -> Maybe Type
@@ -1928,7 +1922,6 @@ provSize :: UnivCoProvenance -> Int
 provSize (PhantomProv co)    = 1 + coercionSize co
 provSize (ProofIrrelProv co) = 1 + coercionSize co
 provSize (PluginProv _)      = 1
-provSize (CorePrepProv _)    = 1
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs
index 0d41fd566089..72faaaa5d2df 100644
--- a/compiler/GHC/Core/TyCo/Subst.hs
+++ b/compiler/GHC/Core/TyCo/Subst.hs
@@ -913,7 +913,6 @@ subst_co subst co
     go_prov (PhantomProv kco)    = PhantomProv (go kco)
     go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
     go_prov p@(PluginProv _)     = p
-    go_prov p@(CorePrepProv _)   = p
 
     -- See Note [Substituting in a coercion hole]
     go_hole h@(CoercionHole { ch_co_var = cv })
diff --git a/compiler/GHC/Core/TyCo/Tidy.hs b/compiler/GHC/Core/TyCo/Tidy.hs
index e5e091a30af9..0dabaa5e2fd3 100644
--- a/compiler/GHC/Core/TyCo/Tidy.hs
+++ b/compiler/GHC/Core/TyCo/Tidy.hs
@@ -253,7 +253,6 @@ tidyCo env@(_, subst) co
     go_prov (PhantomProv co)    = PhantomProv $! go co
     go_prov (ProofIrrelProv co) = ProofIrrelProv $! go co
     go_prov p@(PluginProv _)    = p
-    go_prov p@(CorePrepProv _)  = p
 
 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
 tidyCos env = strictMap (tidyCo env)
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index cd2e19590443..9c1b40394858 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -583,7 +583,6 @@ expandTypeSynonyms ty
     go_prov subst (PhantomProv co)    = PhantomProv (go_co subst co)
     go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
     go_prov _     p@(PluginProv _)    = p
-    go_prov _     p@(CorePrepProv _)  = p
 
       -- the "False" and "const" are to accommodate the type of
       -- substForAllCoBndrUsing, which is general enough to
@@ -1003,7 +1002,6 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
     go_prov !env (PhantomProv co)    = PhantomProv <$> go_co env co
     go_prov !env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
     go_prov !_   p@(PluginProv _)    = return p
-    go_prov !_   p@(CorePrepProv _)  = return p
 
 
 {- *********************************************************************
diff --git a/compiler/GHC/Core/Unfold.hs b/compiler/GHC/Core/Unfold.hs
index ec75efa7d3f1..aee2ea557547 100644
--- a/compiler/GHC/Core/Unfold.hs
+++ b/compiler/GHC/Core/Unfold.hs
@@ -231,8 +231,11 @@ inlineBoringOk e
                         , exprIsTrivial a  = go (credit-1) f
     go credit (Tick _ e)                   = go credit e -- dubious
     go credit (Cast e _)                   = go credit e
-    go credit (Case scrut _ _ [Alt _ _ rhs]) -- See Note [Inline unsafeCoerce]
-      | isUnsafeEqualityProof scrut        = go credit rhs
+    go credit (Case e b _ alts)
+      | null alts
+      = go credit e   -- EmptyCase is like e
+      | Just rhs <- isUnsafeEqualityCase e b alts
+      = go credit rhs -- See Note [Inline unsafeCoerce]
     go _      (Var {})                     = boringCxtOk
     go _      (Lit l)                      = litIsTrivial l && boringCxtOk
     go _      _                            = boringCxtNotOk
@@ -286,7 +289,7 @@ calcUnfoldingGuidance opts is_top_bottoming expr
 We really want to inline unsafeCoerce, even when applied to boring
 arguments.  It doesn't look as if its RHS is smaller than the call
    unsafeCoerce x = case unsafeEqualityProof @a @b of UnsafeRefl -> x
-but that case is discarded -- see Note [Implementing unsafeCoerce]
+but that case is discarded in CoreToStg -- see Note [Implementing unsafeCoerce]
 in base:Unsafe.Coerce.
 
 Moreover, if we /don't/ inline it, we may be left with
@@ -294,7 +297,9 @@ Moreover, if we /don't/ inline it, we may be left with
 which will build a thunk -- bad, bad, bad.
 
 Conclusion: we really want inlineBoringOk to be True of the RHS of
-unsafeCoerce.  This is (U4) in Note [Implementing unsafeCoerce].
+unsafeCoerce. And it really is, because we regard
+  case unsafeEqualityProof @a @b of UnsafeRefl -> rhs
+as trivial iff rhs is. This is (U4) in Note [Implementing unsafeCoerce].
 
 Note [Computing the size of an expression]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index 1a4a23362360..a166292bd0f5 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -60,7 +60,7 @@ module GHC.Core.Utils (
         mkStrictFieldSeqs, shouldStrictifyIdForCbv, shouldUseCbvForId,
 
         -- * unsafeEqualityProof
-        isUnsafeEqualityProof,
+        isUnsafeEqualityCase,
 
         -- * Dumping stuff
         dumpIdInfoOfProgram
@@ -80,7 +80,7 @@ import GHC.Core.Reduction
 import GHC.Core.TyCon
 import GHC.Core.Multiplicity
 
-import GHC.Builtin.Names ( makeStaticName, unsafeEqualityProofIdKey )
+import GHC.Builtin.Names ( makeStaticName, unsafeEqualityProofIdKey, unsafeReflDataConKey )
 import GHC.Builtin.PrimOps
 
 import GHC.Types.Var
@@ -1068,6 +1068,9 @@ trivial_expr_fold :: (Id -> r) -> (Literal -> r) -> r -> r -> CoreExpr -> r
 -- * `case e of {}` an empty case
 trivial_expr_fold k_id k_lit k_triv k_not_triv = go
   where
+    -- If you change this function, be sure to change SetLevels.notWorthFloating
+    -- as well!
+    -- (Or yet better: Come up with a way to share code with this function.)
     go (Var v)                            = k_id v  -- See Note [Variables are trivial]
     go (Lit l)    | litIsTrivial l        = k_lit l
     go (Type _)                           = k_triv
@@ -1076,7 +1079,11 @@ trivial_expr_fold k_id k_lit k_triv k_not_triv = go
     go (Lam b e)  | not (isRuntimeVar b)  = go e
     go (Tick t e) | not (tickishIsCode t) = go e              -- See Note [Tick trivial]
     go (Cast e _)                         = go e
-    go (Case e _ _ [])                    = go e              -- See Note [Empty case is trivial]
+    go (Case e b _ as)
+      | null as
+      = go e     -- See Note [Empty case is trivial]
+      | Just rhs <- isUnsafeEqualityCase e b as
+      = go rhs   -- See (U2) of Note [Implementing unsafeCoerce] in base:Unsafe.Coerce
     go _                                  = k_not_triv
 
 exprIsTrivial :: CoreExpr -> Bool
@@ -1707,7 +1714,7 @@ altsAreExhaustive :: [Alt b] -> Bool
 -- True  <=> the case alternatives are definitely exhaustive
 -- False <=> they may or may not be
 altsAreExhaustive []
-  = False    -- Should not happen
+  = True    -- The scrutinee never returns; see Note [Empty case alternatives] in GHC.Core
 altsAreExhaustive (Alt con1 _ _ : alts)
   = case con1 of
       DEFAULT   -> True
@@ -2692,11 +2699,20 @@ wantCbvForId cbv_for_strict v
 *                                                                      *
 ********************************************************************* -}
 
-isUnsafeEqualityProof :: CoreExpr -> Bool
+isUnsafeEqualityCase :: CoreExpr -> Id -> [CoreAlt] -> Maybe CoreExpr
 -- See (U3) and (U4) in
 -- Note [Implementing unsafeCoerce] in base:Unsafe.Coerce
-isUnsafeEqualityProof e
-  | Var v `App` Type _ `App` Type _ `App` Type _ <- e
-  = v `hasKey` unsafeEqualityProofIdKey
+isUnsafeEqualityCase scrut bndr alts
+  | [Alt ac _ rhs] <- alts
+  , DataAlt dc <- ac
+  , dc `hasKey` unsafeReflDataConKey
+  , isDeadBinder bndr
+      -- We can only discard the case if the case-binder is dead
+      -- It usually is, but see #18227
+  , Var v `App` _ `App` _ `App` _ <- scrut
+  , v `hasKey` unsafeEqualityProofIdKey
+      -- Check that the scrutinee really is unsafeEqualityProof
+      -- and not, say, error
+  = Just rhs
   | otherwise
-  = False
+  = Nothing
diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs
index 2a231741281c..70be311e8187 100644
--- a/compiler/GHC/CoreToIface.hs
+++ b/compiler/GHC/CoreToIface.hs
@@ -322,7 +322,6 @@ toIfaceCoercionX fr co
     go_prov (PhantomProv co)    = IfacePhantomProv (go co)
     go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
     go_prov (PluginProv str)    = IfacePluginProv str
-    go_prov (CorePrepProv b)    = IfaceCorePrepProv b
 
 toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
 toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
diff --git a/compiler/GHC/CoreToStg.hs b/compiler/GHC/CoreToStg.hs
index fee9a8ac37ef..2d62d4698798 100644
--- a/compiler/GHC/CoreToStg.hs
+++ b/compiler/GHC/CoreToStg.hs
@@ -19,8 +19,7 @@ module GHC.CoreToStg ( CoreToStgOpts (..), coreToStg ) where
 import GHC.Prelude
 
 import GHC.Core
-import GHC.Core.Utils   ( exprType, findDefault, isJoinBind
-                        , exprIsTickedString_maybe )
+import GHC.Core.Utils
 import GHC.Core.Opt.Arity   ( manifestArity )
 import GHC.Core.Type
 import GHC.Core.TyCon
@@ -49,7 +48,7 @@ import GHC.Unit.Module
 import GHC.Data.FastString
 import GHC.Platform        ( Platform )
 import GHC.Platform.Ways
-import GHC.Builtin.PrimOps ( PrimCall(..), primOpWrapperId )
+import GHC.Builtin.PrimOps
 
 import GHC.Utils.Outputable
 import GHC.Utils.Monad
@@ -430,30 +429,23 @@ coreToStgExpr (Cast expr _)
   = coreToStgExpr expr
 
 -- Cases require a little more real work.
-
-{-
-coreToStgExpr (Case scrut _ _ [])
+coreToStgExpr (Case scrut bndr _ alts)
+  | null alts
+  -- See Note [Empty case alternatives] in GHC.Core If the case
+  -- alternatives are empty, the scrutinee must diverge or raise an
+  -- exception, so we can just dive into it.
+  --
+  -- Of course this may seg-fault if the scrutinee *does* return.  A
+  -- belt-and-braces approach would be to move this case into the
+  -- code generator, and put a return point anyway that calls a
+  -- runtime system error function.
   = coreToStgExpr scrut
-    -- See Note [Empty case alternatives] in GHC.Core If the case
-    -- alternatives are empty, the scrutinee must diverge or raise an
-    -- exception, so we can just dive into it.
-    --
-    -- Of course this may seg-fault if the scrutinee *does* return.  A
-    -- belt-and-braces approach would be to move this case into the
-    -- code generator, and put a return point anyway that calls a
-    -- runtime system error function.
-
-coreToStgExpr e0@(Case scrut bndr _ [alt]) = do
-  | isUnsafeEqualityProof scrut
-  , isDeadBinder bndr -- We can only discard the case if the case-binder is dead
-                      -- It usually is, but see #18227
-  , (_,_,rhs) <- alt
+
+  | Just rhs <- isUnsafeEqualityCase scrut bndr alts
+  -- See (U2) in Note [Implementing unsafeCoerce] in base:Unsafe.Coerce
   = coreToStgExpr rhs
-    -- See (U2) in Note [Implementing unsafeCoerce] in base:Unsafe.Coerce
--}
 
--- The normal case for case-expressions
-coreToStgExpr (Case scrut bndr _ alts)
+  | otherwise
   = do { scrut2 <- coreToStgExpr scrut
        ; alts2 <- extendVarEnvCts [(bndr, LambdaBound)] (mapM vars_alt alts)
        ; return (StgCase scrut2 bndr (mkStgAltType bndr alts) alts2) }
@@ -574,6 +566,15 @@ coreToStgApp f args ticks = do
 -- This is the guy that turns applications into A-normal form
 -- ---------------------------------------------------------------------------
 
+getStgArgFromTrivialArg :: HasDebugCallStack => CoreArg -> StgArg
+-- A (non-erased) trivial CoreArg corresponds to an atomic StgArg.
+-- CoreArgs may not immediately look trivial, e.g., `case e of {}` or
+-- `case unsafeequalityProof of UnsafeRefl -> e` might intervene.
+-- Good thing we can just call `trivial_expr_fold` here.
+getStgArgFromTrivialArg e = trivial_expr_fold StgVarArg StgLitArg panic panic e
+  where
+    panic = pprPanic "getStgArgFromTrivialArg" (ppr e)
+
 coreToStgArgs :: [CoreArg] -> CtsM ([StgArg], [StgTickish])
 coreToStgArgs []
   = return ([], [])
@@ -586,42 +587,29 @@ coreToStgArgs (Coercion _ : args) -- Coercion argument; See Note [Coercion token
   = do { (args', ts) <- coreToStgArgs args
        ; return (StgVarArg coercionTokenId : args', ts) }
 
-coreToStgArgs (Tick t e : args)
-  = assert (not (tickishIsCode t)) $
-    do { (args', ts) <- coreToStgArgs (e : args)
-       ; let !t' = coreToStgTick (exprType e) t
-       ; return (args', t':ts) }
-
 coreToStgArgs (arg : args) = do         -- Non-type argument
     (stg_args, ticks) <- coreToStgArgs args
-    arg' <- coreToStgExpr arg
-    let
-        (aticks, arg'') = stripStgTicksTop tickishFloatable arg'
-        stg_arg = case arg'' of
-           StgApp v []                  -> StgVarArg v
-           StgConApp con _ [] _         -> StgVarArg (dataConWorkId con)
-           StgOpApp (StgPrimOp op) [] _ -> StgVarArg (primOpWrapperId op)
-           StgLit lit                   -> StgLitArg lit
-           _ -> pprPanic "coreToStgArgs" (ppr arg $$ pprStgExpr panicStgPprOpts arg' $$ pprStgExpr panicStgPprOpts arg'')
-
-        -- WARNING: what if we have an argument like (v `cast` co)
-        --          where 'co' changes the representation type?
-        --          (This really only happens if co is unsafe.)
-        -- Then all the getArgAmode stuff in CgBindery will set the
-        -- cg_rep of the CgIdInfo based on the type of v, rather
-        -- than the type of 'co'.
-        -- This matters particularly when the function is a primop
-        -- or foreign call.
-        -- Wanted: a better solution than this hacky warning
-
+    -- We know that `arg` must be trivial, but it may contain Ticks.
+    -- Example from test case `decodeMyStack`:
+    --   $ @... ((src<decodeMyStack.hs:18:26-28> Data.Tuple.snd) @Int @[..])
+    -- Note that unfortunately the Tick is not at the top.
+    -- So we'll traverse the expression twice:
+    --   * Once with `stripTicksT` (which collects *all* ticks from the expression)
+    --   * and another time with `getStgArgFromTrivialArg`.
+    -- Since the argument is trivial, the only place the Tick can occur is
+    -- somehow wrapping a variable (give or take type args, as above).
     platform <- getPlatform
-    let
-        arg_rep = typePrimRep (exprType arg)
-        stg_arg_rep = typePrimRep (stgArgType stg_arg)
+    let arg_ty = exprType arg
+        ticks' = map (coreToStgTick arg_ty) (stripTicksT (not . tickishIsCode) arg)
+        arg' = getStgArgFromTrivialArg arg
+        arg_rep = typePrimRep arg_ty
+        stg_arg_rep = typePrimRep (stgArgType arg')
         bad_args = not (primRepsCompatible platform arg_rep stg_arg_rep)
 
-    warnPprTrace bad_args "Dangerous-looking argument. Probable cause: bad unsafeCoerce#" (ppr arg) $
-     return (stg_arg : stg_args, ticks ++ aticks)
+    massertPpr (length ticks' <= 1) (text "More than one Tick in trivial arg:" <+> ppr arg)
+    warnPprTraceM bad_args "Dangerous-looking argument. Probable cause: bad unsafeCoerce#" (ppr arg)
+
+    return (arg' : stg_args, ticks' ++ ticks)
 
 coreToStgTick :: Type -- type of the ticked expression
               -> CoreTickish
@@ -959,6 +947,9 @@ myCollectBinders expr
 
 -- | If the argument expression is (potential chain of) 'App', return the head
 -- of the app chain, and collect ticks/args along the chain.
+-- INVARIANT: If the app head is trivial, return the atomic Var/Lit that was
+-- wrapped in casts, empty case, ticks, etc.
+-- So keep in sync with 'exprIsTrivial'.
 myCollectArgs :: HasDebugCallStack => CoreExpr -> (CoreExpr, [CoreArg], [CoreTickish])
 myCollectArgs expr
   = go expr [] []
@@ -970,8 +961,16 @@ myCollectArgs expr
                                 -- See Note [Ticks in applications]
                                 go e as (t:ts) -- ticks can appear in type apps
     go (Cast e _)       as ts = go e as ts
+    go (Case e b _ alts) as ts  -- Just like in exprIsTrivial!
+                                -- Otherwise we fall over in case we encounter
+                                -- `(case f a of {}) b` in the future.
+       | null alts
+       = assertPpr (null as) (ppr e $$ ppr as $$ ppr expr) $
+                   go e [] ts -- NB: Empty case discards arguments
+       | Just rhs <- isUnsafeEqualityCase e b alts
+       = go rhs as ts         -- Discards unsafeCoerce in App heads
     go (Lam b e)        as ts
-       | isTyVar b            = go e as ts -- Note [Collect args]
+       | isTyVar b            = go e (drop 1 as) ts -- Note [Collect args]
     go e                as ts = (e, as, ts)
 
 {- Note [Collect args]
diff --git a/compiler/GHC/CoreToStg/Prep.hs b/compiler/GHC/CoreToStg/Prep.hs
index 6b310095f0ff..6d1d3afe2380 100644
--- a/compiler/GHC/CoreToStg/Prep.hs
+++ b/compiler/GHC/CoreToStg/Prep.hs
@@ -40,12 +40,10 @@ import GHC.Core.Coercion
 import GHC.Core.TyCon
 import GHC.Core.DataCon
 import GHC.Core.Opt.OccurAnal
-import GHC.Core.TyCo.Rep( UnivCoProvenance(..) )
 
 import GHC.Data.Maybe
 import GHC.Data.OrdList
 import GHC.Data.FastString
-import GHC.Data.Pair
 import GHC.Data.Graph.UnVar
 
 import GHC.Utils.Error
@@ -71,7 +69,6 @@ import GHC.Types.TyThing
 import GHC.Types.Unique.Supply
 
 import Data.List        ( unfoldr )
-import Data.Functor.Identity
 import Control.Monad
 
 {-
@@ -142,10 +139,7 @@ The goal of this pass is to prepare for code generation.
     profiling mode. We have to do this here because we won't have unfoldings
     after this pass (see `trimUnfolding` and Note [Drop unfoldings and rules].
 
-12. Eliminate case clutter in favour of unsafe coercions.
-    See Note [Unsafe coercions]
-
-13. Eliminate some magic Ids, specifically
+12. Eliminate some magic Ids, specifically
      runRW# (\s. e)  ==>  e[readWorldId/s]
              lazy e  ==>  e (see Note [lazyId magic] in GHC.Types.Id.Make)
          noinline e  ==>  e
@@ -157,48 +151,6 @@ This is all done modulo type applications and abstractions, so that
 when type erasure is done for conversion to STG, we don't end up with
 any trivial or useless bindings.
 
-Note [Unsafe coercions]
-~~~~~~~~~~~~~~~~~~~~~~~
-CorePrep does these two transformations:
-
-1. Convert empty case to cast with an unsafe coercion
-          (case e of {}) ===>  e |> unsafe-co
-   See Note [Empty case alternatives] in GHC.Core: if the case
-   alternatives are empty, the scrutinee must diverge or raise an
-   exception, so we can just dive into it.
-
-   Of course, if the scrutinee *does* return, we may get a seg-fault.
-   A belt-and-braces approach would be to persist empty-alternative
-   cases to code generator, and put a return point anyway that calls a
-   runtime system error function.
-
-   Notice that eliminating empty case can lead to an ill-kinded coercion
-       case error @Int "foo" of {}  :: Int#
-       ===> error @Int "foo" |> unsafe-co
-       where unsafe-co :: Int ~ Int#
-   But that's fine because the expression diverges anyway. And it's
-   no different to what happened before.
-
-2. Eliminate unsafeEqualityProof in favour of an unsafe coercion
-           case unsafeEqualityProof of UnsafeRefl g -> e
-           ===>  e[unsafe-co/g]
-   See (U2) in Note [Implementing unsafeCoerce] in base:Unsafe.Coerce
-
-   Note that this requires us to substitute 'unsafe-co' for 'g', and
-   that is the main (current) reason for cpe_tyco_env in CorePrepEnv.
-   Tiresome, but not difficult.
-
-These transformations get rid of "case clutter", leaving only casts.
-We are doing no further significant transformations, so the reasons
-for the case forms have disappeared. And it is extremely helpful for
-the ANF-ery, CoreToStg, and backends, if trivial expressions really do
-look trivial. #19700 was an example.
-
-In both cases, the "unsafe-co" is just (UnivCo ty1 ty2 (CorePrepProv b)),
-The boolean 'b' says whether the unsafe coercion is supposed to be
-kind-homogeneous (yes for (2), no for (1).  This information is used
-/only/ by Lint.
-
 Note [CorePrep invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 Here is the syntax of the Core produced by CorePrep:
@@ -789,10 +741,10 @@ cpeRhsE :: CorePrepEnv -> CoreExpr -> UniqSM (Floats, CpeRhs)
 -- For example
 --      f (g x)   ===>   ([v = g x], f v)
 
-cpeRhsE env (Type ty)
-  = return (emptyFloats, Type (cpSubstTy env ty))
-cpeRhsE env (Coercion co)
-  = return (emptyFloats, Coercion (cpSubstCo env co))
+cpeRhsE _ (Type ty)
+  = return (emptyFloats, Type ty)
+cpeRhsE _ (Coercion co)
+  = return (emptyFloats, Coercion co)
 cpeRhsE env expr@(Lit (LitNumber nt i))
    = case cp_convertNumLit (cpe_config env) nt i of
       Nothing -> return (emptyFloats, expr)
@@ -826,7 +778,7 @@ cpeRhsE env (Tick tickish expr)
 
 cpeRhsE env (Cast expr co)
    = do { (floats, expr') <- cpeRhsE env expr
-        ; return (floats, Cast expr' (cpSubstCo env co)) }
+        ; return (floats, Cast expr' co) }
 
 cpeRhsE env expr@(Lam {})
    = do { let (bndrs,body) = collectBinders expr
@@ -834,35 +786,36 @@ cpeRhsE env expr@(Lam {})
         ; body' <- cpeBodyNF env' body
         ; return (emptyFloats, mkLams bndrs' body') }
 
--- Eliminate empty case
--- See Note [Unsafe coercions]
-cpeRhsE env (Case scrut _ ty [])
-  = do { (floats, scrut') <- cpeRhsE env scrut
-       ; let ty'       = cpSubstTy env ty
-             scrut_ty' = exprType scrut'
-             co'       = mkUnivCo prov Representational scrut_ty' ty'
-             prov      = CorePrepProv False
-               -- False says that the kinds of two types may differ
-               -- E.g. we might cast Int to Int#.  This is fine
-               -- because the scrutinee is guaranteed to diverge
-
-       ; return (floats, Cast scrut' co') }
-   -- This can give rise to
-   --   Warning: Unsafe coercion: between unboxed and boxed value
-   -- but it's fine because 'scrut' diverges
-
--- Eliminate unsafeEqualityProof
--- See Note [Unsafe coercions]
-cpeRhsE env (Case scrut bndr _ alts)
-  | isUnsafeEqualityProof scrut
-  , isDeadBinder bndr -- We can only discard the case if the case-binder
-                      -- is dead.  It usually is, but see #18227
-  , [Alt _ [co_var] rhs] <- alts
-  , let Pair ty1 ty2 = coVarTypes co_var
-        the_co = mkUnivCo prov Nominal (cpSubstTy env ty1) (cpSubstTy env ty2)
-        prov   = CorePrepProv True  -- True <=> kind homogeneous
-        env'   = extendCoVarEnv env co_var the_co
-  = cpeRhsE env' rhs
+cpeRhsE env (Case scrut bndr _ alts@[Alt con bs _])
+  -- See (U3) in Note [Implementing unsafeCoerce]
+  -- We need make the Case float, otherwise we get
+  --   let x = case ... of UnsafeRefl co ->
+  --           let y = expr in
+  --           K y
+  --   in f x
+  -- instead of
+  --   case ... of UnsafeRefl co ->
+  --   let y = expr in
+  --   let x = K y
+  --   in f x
+  -- Note that `x` is a value here. This is visible in the GHCi debugger tests
+  -- (such as `print003`).
+  | Just rhs <- isUnsafeEqualityCase scrut bndr alts
+  = do { (floats_scrut, scrut) <- cpeBody env scrut
+       ; (env, bndr) <- cpCloneBndr env bndr
+       ; (env, bs) <- cpCloneBndrs env bs
+         -- Up until here this should do exactly the same as the regular code
+         -- path of `cpeRhsE Case{}`.
+       ; (floats_rhs, rhs) <- cpeBody env rhs
+         -- ... but we want to float `floats_rhs` as in (U3) so that rhs' might
+         -- become a value
+       ; let case_float = FloatCase scrut bndr con bs True
+         -- NB: True <=> ok-for-spec; it is OK to "evaluate" the proof eagerly.
+         --     Usually there's the danger that we float the unsafeCoerce out of
+         --     a branching Case alt. Not so here, because the regular code path
+         --     for `cpeRhsE Case{}` will not float out of alts.
+             floats = addFloat floats_scrut case_float `appendFloats` floats_rhs
+       ; return (floats, rhs) }
 
 cpeRhsE env (Case scrut bndr ty alts)
   = do { (floats, scrut') <- cpeBody env scrut
@@ -1209,14 +1162,10 @@ cpeApp top_env expr
             in rebuild_app' env (a : as) tick_fun floats ss rt_ticks req_depth
 
       CpeApp (Type arg_ty)
-        -> rebuild_app' env as (App fun' (Type arg_ty')) floats ss rt_ticks req_depth
-        where
-          arg_ty' = cpSubstTy env arg_ty
+        -> rebuild_app' env as (App fun' (Type arg_ty)) floats ss rt_ticks req_depth
 
       CpeApp (Coercion co)
-        -> rebuild_app' env as (App fun' (Coercion co')) floats (drop 1 ss) rt_ticks req_depth
-        where
-            co' = cpSubstCo env co
+        -> rebuild_app' env as (App fun' (Coercion co)) floats (drop 1 ss) rt_ticks req_depth
 
       CpeApp arg -> do
         let (ss1, ss_rest)  -- See Note [lazyId magic] in GHC.Types.Id.Make
@@ -1228,9 +1177,7 @@ cpeApp top_env expr
         rebuild_app' env as (App fun' arg') (fs `appendFloats` floats) ss_rest rt_ticks (req_depth-1)
 
       CpeCast co
-        -> rebuild_app' env as (Cast fun' co') floats ss rt_ticks req_depth
-        where
-           co' = cpSubstCo env co
+        -> rebuild_app' env as (Cast fun' co) floats ss rt_ticks req_depth
       -- See Note [Ticks and mandatory eta expansion]
       CpeTick tickish
         | tickishPlace tickish == PlaceRuntime
@@ -2064,8 +2011,6 @@ data CorePrepEnv
         --      see Note [lazyId magic], Note [Inlining in CorePrep]
         --      and Note [CorePrep inlines trivial CoreExpr not Id] (#12076)
 
-        , cpe_tyco_env :: Maybe CpeTyCoEnv -- See Note [CpeTyCoEnv]
-
         , cpe_rec_ids         :: UnVarSet -- Faster OutIdSet; See Note [Speculative evaluation]
     }
 
@@ -2073,7 +2018,6 @@ mkInitialCorePrepEnv :: CorePrepConfig -> CorePrepEnv
 mkInitialCorePrepEnv cfg = CPE
       { cpe_config        = cfg
       , cpe_env           = emptyVarEnv
-      , cpe_tyco_env      = Nothing
       , cpe_rec_ids       = emptyUnVarSet
       }
 
@@ -2100,117 +2044,6 @@ enterRecGroupRHSs :: CorePrepEnv -> [OutId] -> CorePrepEnv
 enterRecGroupRHSs env grp
   = env { cpe_rec_ids = extendUnVarSetList grp (cpe_rec_ids env) }
 
-------------------------------------------------------------------------------
---           CpeTyCoEnv
--- ---------------------------------------------------------------------------
-
-{- Note [CpeTyCoEnv]
-~~~~~~~~~~~~~~~~~~~~
-The cpe_tyco_env :: Maybe CpeTyCoEnv field carries a substitution
-for type and coercion variables
-
-* We need the coercion substitution to support the elimination of
-  unsafeEqualityProof (see Note [Unsafe coercions])
-
-* We need the type substitution in case one of those unsafe
-  coercions occurs in the kind of tyvar binder (sigh)
-
-We don't need an in-scope set because we don't clone any of these
-binders at all, so no new capture can take place.
-
-The cpe_tyco_env is almost always empty -- it only gets populated
-when we get under an usafeEqualityProof.  Hence the Maybe CpeTyCoEnv,
-which makes everything into a no-op in the common case.
--}
-
-data CpeTyCoEnv = TCE TvSubstEnv CvSubstEnv
-
-emptyTCE :: CpeTyCoEnv
-emptyTCE = TCE emptyTvSubstEnv emptyCvSubstEnv
-
-extend_tce_cv :: CpeTyCoEnv -> CoVar -> Coercion -> CpeTyCoEnv
-extend_tce_cv (TCE tv_env cv_env) cv co
-  = TCE tv_env (extendVarEnv cv_env cv co)
-
-extend_tce_tv :: CpeTyCoEnv -> TyVar -> Type -> CpeTyCoEnv
-extend_tce_tv (TCE tv_env cv_env) tv ty
-  = TCE (extendVarEnv tv_env tv ty) cv_env
-
-lookup_tce_cv :: CpeTyCoEnv -> CoVar -> Coercion
-lookup_tce_cv (TCE _ cv_env) cv
-  = case lookupVarEnv cv_env cv of
-        Just co -> co
-        Nothing -> mkCoVarCo cv
-
-lookup_tce_tv :: CpeTyCoEnv -> TyVar -> Type
-lookup_tce_tv (TCE tv_env _) tv
-  = case lookupVarEnv tv_env tv of
-        Just ty -> ty
-        Nothing -> mkTyVarTy tv
-
-extendCoVarEnv :: CorePrepEnv -> CoVar -> Coercion -> CorePrepEnv
-extendCoVarEnv cpe@(CPE { cpe_tyco_env = mb_tce }) cv co
-  = cpe { cpe_tyco_env = Just (extend_tce_cv tce cv co) }
-  where
-    tce = mb_tce `orElse` emptyTCE
-
-
-cpSubstTy :: CorePrepEnv -> Type -> Type
-cpSubstTy (CPE { cpe_tyco_env = mb_env }) ty
-  = case mb_env of
-      Just env -> runIdentity (subst_ty env ty)
-      Nothing  -> ty
-
-cpSubstCo :: CorePrepEnv -> Coercion -> Coercion
-cpSubstCo (CPE { cpe_tyco_env = mb_env }) co
-  = case mb_env of
-      Just tce -> runIdentity (subst_co tce co)
-      Nothing  -> co
-
-subst_tyco_mapper :: TyCoMapper CpeTyCoEnv Identity
-subst_tyco_mapper = TyCoMapper
-  { tcm_tyvar      = \env tv -> return (lookup_tce_tv env tv)
-  , tcm_covar      = \env cv -> return (lookup_tce_cv env cv)
-  , tcm_hole       = \_ hole -> pprPanic "subst_co_mapper:hole" (ppr hole)
-  , tcm_tycobinder = \env tcv _vis k -> if isTyVar tcv
-                                        then uncurry k (subst_tv_bndr env tcv)
-                                        else uncurry k (subst_cv_bndr env tcv)
-  , tcm_tycon      = \tc -> return tc }
-
-subst_ty :: CpeTyCoEnv -> Type     -> Identity Type
-subst_co :: CpeTyCoEnv -> Coercion -> Identity Coercion
-(subst_ty, _, subst_co, _) = mapTyCoX subst_tyco_mapper
-
-cpSubstTyVarBndr :: CorePrepEnv -> TyVar -> (CorePrepEnv, TyVar)
-cpSubstTyVarBndr env@(CPE { cpe_tyco_env = mb_env }) tv
-  = case mb_env of
-      Nothing  -> (env, tv)
-      Just tce -> (env { cpe_tyco_env = Just tce' }, tv')
-               where
-                  (tce', tv') = subst_tv_bndr tce tv
-
-subst_tv_bndr :: CpeTyCoEnv -> TyVar -> (CpeTyCoEnv, TyVar)
-subst_tv_bndr tce tv
-  = (extend_tce_tv tce tv (mkTyVarTy tv'), tv')
-  where
-    tv'   = mkTyVar (tyVarName tv) kind'
-    kind' = runIdentity $ subst_ty tce $ tyVarKind tv
-
-cpSubstCoVarBndr :: CorePrepEnv -> CoVar -> (CorePrepEnv, CoVar)
-cpSubstCoVarBndr env@(CPE { cpe_tyco_env = mb_env }) cv
-  = case mb_env of
-      Nothing  -> (env, cv)
-      Just tce -> (env { cpe_tyco_env = Just tce' }, cv')
-               where
-                  (tce', cv') = subst_cv_bndr tce cv
-
-subst_cv_bndr :: CpeTyCoEnv -> CoVar -> (CpeTyCoEnv, CoVar)
-subst_cv_bndr tce cv
-  = (extend_tce_cv tce cv (mkCoVarCo cv'), cv')
-  where
-    cv' = mkCoVar (varName cv) ty'
-    ty' = runIdentity (subst_ty tce $ varType cv)
-
 ------------------------------------------------------------------------------
 -- Cloning binders
 -- ---------------------------------------------------------------------------
@@ -2220,12 +2053,8 @@ cpCloneBndrs env bs = mapAccumLM cpCloneBndr env bs
 
 cpCloneBndr  :: CorePrepEnv -> InVar -> UniqSM (CorePrepEnv, OutVar)
 cpCloneBndr env bndr
-  | isTyVar bndr
-  = return (cpSubstTyVarBndr env bndr)
-
-  | isCoVar bndr
-  = return (cpSubstCoVarBndr env bndr)
-
+  | isTyCoVar bndr
+  = return (env, bndr)
   | otherwise
   = do { bndr' <- clone_it bndr
 
@@ -2245,8 +2074,7 @@ cpCloneBndr env bndr
     clone_it bndr
       | isLocalId bndr
       = do { uniq <- getUniqueM
-           ; let ty' = cpSubstTy env (idType bndr)
-           ; return (setVarUnique (setIdType bndr ty') uniq) }
+           ; return (setVarUnique bndr uniq) }
 
       | otherwise   -- Top level things, which we don't want
                     -- to clone, have become GlobalIds by now
diff --git a/compiler/GHC/Iface/Syntax.hs b/compiler/GHC/Iface/Syntax.hs
index fa38aa211302..44dda2f0d805 100644
--- a/compiler/GHC/Iface/Syntax.hs
+++ b/compiler/GHC/Iface/Syntax.hs
@@ -1795,7 +1795,6 @@ freeNamesIfProv :: IfaceUnivCoProv -> NameSet
 freeNamesIfProv (IfacePhantomProv co)    = freeNamesIfCoercion co
 freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co
 freeNamesIfProv (IfacePluginProv _)      = emptyNameSet
-freeNamesIfProv (IfaceCorePrepProv _)    = emptyNameSet
 
 freeNamesIfVarBndr :: VarBndr IfaceBndr vis -> NameSet
 freeNamesIfVarBndr (Bndr bndr _) = freeNamesIfBndr bndr
diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index 1ea0307fc534..1cc626358c58 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -403,7 +403,6 @@ data IfaceUnivCoProv
   = IfacePhantomProv IfaceCoercion
   | IfaceProofIrrelProv IfaceCoercion
   | IfacePluginProv String
-  | IfaceCorePrepProv Bool  -- See defn of CorePrepProv
 
 {- Note [Holes in IfaceCoercion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -625,7 +624,6 @@ substIfaceType env ty
     go_prov (IfacePhantomProv co)    = IfacePhantomProv (go_co co)
     go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
     go_prov co@(IfacePluginProv _)   = co
-    go_prov co@(IfaceCorePrepProv _) = co
 
 substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
 substIfaceAppArgs env args
@@ -1925,8 +1923,6 @@ pprIfaceUnivCoProv (IfaceProofIrrelProv co)
   = text "irrel" <+> pprParendIfaceCoercion co
 pprIfaceUnivCoProv (IfacePluginProv s)
   = text "plugin" <+> doubleQuotes (text s)
-pprIfaceUnivCoProv (IfaceCorePrepProv _)
-  = text "CorePrep"
 
 -------------------
 instance Outputable IfaceTyCon where
@@ -2298,9 +2294,6 @@ instance Binary IfaceUnivCoProv where
   put_ bh (IfacePluginProv a) = do
           putByte bh 3
           put_ bh a
-  put_ bh (IfaceCorePrepProv a) = do
-          putByte bh 4
-          put_ bh a
 
   get bh = do
       tag <- getByte bh
@@ -2311,8 +2304,6 @@ instance Binary IfaceUnivCoProv where
                    return $ IfaceProofIrrelProv a
            3 -> do a <- get bh
                    return $ IfacePluginProv a
-           4 -> do a <- get bh
-                   return (IfaceCorePrepProv a)
            _ -> panic ("get IfaceUnivCoProv " ++ show tag)
 
 
diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index bd4101cf0c2b..bb22a1374eaf 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -1493,7 +1493,6 @@ tcIfaceUnivCoProv :: IfaceUnivCoProv -> IfL UnivCoProvenance
 tcIfaceUnivCoProv (IfacePhantomProv kco)    = PhantomProv <$> tcIfaceCo kco
 tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco
 tcIfaceUnivCoProv (IfacePluginProv str)     = return $ PluginProv str
-tcIfaceUnivCoProv (IfaceCorePrepProv b)     = return $ CorePrepProv b
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/StgToCmm/Expr.hs b/compiler/GHC/StgToCmm/Expr.hs
index b2d44a0d98cd..68afbf758b98 100644
--- a/compiler/GHC/StgToCmm/Expr.hs
+++ b/compiler/GHC/StgToCmm/Expr.hs
@@ -53,7 +53,6 @@ import GHC.Utils.Misc
 import GHC.Data.FastString
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
-import GHC.Utils.Panic.Plain
 
 import Control.Monad ( unless, void )
 import Control.Arrow ( first )
@@ -1028,7 +1027,7 @@ cgIdApp fun_id args = do
                       (text "TagCheck failed on entry in" <+> ppr mod <+> text "- value:" <> ppr fun_id <+> pdoc platform fun))
                       fun
 
-        EnterIt -> assert (null args) $  -- Discarding arguments
+        EnterIt -> assertPpr (null args) (ppr fun_id $$ ppr args) $  -- Discarding arguments
                    emitEnter fun
 
         SlowCall -> do      -- A slow function call via the RTS apply routines
diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
index 6bcba860aaf1..cbb888e2edd5 100644
--- a/compiler/GHC/Tc/TyCl/Utils.hs
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -159,7 +159,6 @@ synonymTyConsOfType ty
      go_prov (PhantomProv co)     = go_co co
      go_prov (ProofIrrelProv co)  = go_co co
      go_prov (PluginProv _)       = emptyNameEnv
-     go_prov (CorePrepProv _)     = emptyNameEnv
 
      go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
               | otherwise             = emptyNameEnv
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 74cc6fcfdcac..b59b11c089da 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1587,7 +1587,6 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co
     go_prov dv (PhantomProv co)    = go_co dv co
     go_prov dv (ProofIrrelProv co) = go_co dv co
     go_prov dv (PluginProv _)      = return dv
-    go_prov dv (CorePrepProv _)    = return dv
 
     go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs
     go_cv dv@(DV { dv_cvs = cvs }) cv
diff --git a/compiler/GHC/Utils/Trace.hs b/compiler/GHC/Utils/Trace.hs
index 112d2f9ba56c..26e48017e62f 100644
--- a/compiler/GHC/Utils/Trace.hs
+++ b/compiler/GHC/Utils/Trace.hs
@@ -8,6 +8,7 @@ module GHC.Utils.Trace
   , pprSTrace
   , pprTraceException
   , warnPprTrace
+  , warnPprTraceM
   , pprTraceUserWarning
   , trace
   )
@@ -84,6 +85,9 @@ warnPprTrace True   s  msg x
                     (text s $$ msg $$ withFrozenCallStack traceCallStackDoc )
                     x
 
+warnPprTraceM :: (Applicative f, HasCallStack) => Bool -> String -> SDoc -> f ()
+warnPprTraceM b s doc = withFrozenCallStack warnPprTrace b s doc (pure ())
+
 -- | For when we want to show the user a non-fatal WARNING so that they can
 -- report a GHC bug, but don't want to panic.
 pprTraceUserWarning :: HasCallStack => SDoc -> a -> a
diff --git a/libraries/base/Unsafe/Coerce.hs b/libraries/base/Unsafe/Coerce.hs
index e1b00ce10d71..33cfcc9bc1a9 100644
--- a/libraries/base/Unsafe/Coerce.hs
+++ b/libraries/base/Unsafe/Coerce.hs
@@ -37,15 +37,16 @@ The programmer thinks that the unsafeCoerce from 't1' to 't2' is safe,
 because it is justified by a runtime test (sameTypeRep t1 t2).
 It used to compile to a cast, with a magical 'UnsafeCo' coercion.
 
-But alas, nothing then stops GHC floating that call to unsafeCoerce
-outwards so we get
+But alas, if `x` is known to be evaluated, nothing then stops GHC floating that
+call to unsafeCoerce outwards so we get
    case (x |> UnsafeCo @t1 @t2) of
      K -> case sameTypeRep t1 t2 of
              False -> blah2
              True  -> ...blah...
 
 and this is utterly wrong, because the unsafeCoerce is being performed
-before the dynamic test. This is exactly the setup in #16893.
+before the dynamic test. This is exactly the setup in #16893 (search for
+"Diagnosis").
 
 The solution is this:
 
@@ -81,13 +82,13 @@ several ways
 
 (U1) unsafeEqualityProof is /never/ inlined.
 
-(U2) In CoreToStg.Prep, we transform
+(U2) In CoreToStg.coreToStgExpr, we transform
        case unsafeEqualityProof of UnsafeRefl g -> blah
       ==>
-       blah[unsafe-co/g]
+       blah
 
-     This eliminates the overhead of evaluating the unsafe
-     equality proof.
+     This eliminates the overhead of evaluating the unsafe equality proof.
+     (It follows that the Case is trivial iff `blah` is.)
 
      Any /other/ occurrence of unsafeEqualityProof is left alone.
      For example you could write
@@ -121,12 +122,25 @@ several ways
         let a = e
             x = K a
         in ...  }
-     Floating the case is OK here, even though it broadens the
-     scope, because we are done with simplification.
-
-(U4) Ditto GHC.Core.Unfold.inlineBoringOk we want to treat
-     the RHS of unsafeCoerce as very small; see
-     Note [Inline unsafeCoerce] in that module.
+     NB: Floating the case is OK here, even though it broadens the scope,
+     because we are done with simplification and won't float out of
+     branching Case alternatives such as in the `sameTypeRep` example above.
+
+     Neglecting this transformation triggered test failures in GHCi debugger
+     test cases such as `print003`, because it could no longer identify things
+     such as `x` above as a value.
+
+(U4) `case unsafeEqualityProof of UnsafeRefl -> rhs` as trivial iff `rhs` is,
+     see `exprIsTrivial`. One reason is that we want to treat the RHS
+     of unsafeCoerce as very small; see Note [Inline unsafeCoerce] in
+     GHC.Core.Unfold.
+     Another reason is
+       f (case unsafeEqualitProof ... of UnsafeRefl co -> x |> co))
+     we do not want to ANF-ise to
+        let arg = case unsafeEqualitProof ... of UnsafeRefl co -> x |> co
+        in f arg
+     because that `let` will turn into a silly indirection `let arg = x in ..`
+     in CoreToStg. Triviality means we can "look through" the Case in CoreToStg.
 
 (U5) The definition of unsafeEqualityProof in Unsafe.Coerce
      looks very strange:
-- 
GitLab