diff --git a/compiler/GHC/Core.hs b/compiler/GHC/Core.hs
index 0aa89011ca50a88b23664250a6a2be0da6fac787..f856b51332937849223b9297dba967ae93a0c5e7 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 9000e7a399e94578b5db79732563769f503be94c..5f842bb66d49836a173f02cfdc4cb42a9dbeb5b0 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 44a381259801ac697dd8c2142eb384523fb71544..3ffbcecda4de78a2b6b54447779bbc9b0fa5fdf6 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 225bc05960297712d8e09adf1198a937e632277b..2c268e878a2a0ba6f0d6d7254face64742b8afc6 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 e889564715e3931c53fe1c13b6141d64d89a71c7..e0a816e24f1d840f9220ecbcf5a4ef92f9a65cf9 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 185da7df526ecb15002a0143c4b05b14509134c4..93e9bf073ef73cd6c2d8d29e17d612b7df79b222 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 c56d86d6ceff9cf459bdd3292583eddd0da90d01..1dd4881355f92fbbbf187cf454d593386931f2ee 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 3dd1759a347a529061c3cd713cc55f86f700666b..14bf82e170f9cea05afcd769f827abcccbb64451 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 af86de998f5bd70068f2337f301e1ab7044443cb..f85ca8f90f0a56a77b9dc012768d215577ba07f6 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 0d41fd5660896891d36a1fbdf9b2ebdf59be65de..72faaaa5d2dff8f45b55cdaa4fbb84c8176e8b00 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 e5e091a30af9a0297196ec2361260996acaee748..0dabaa5e2fd36593283ba13f45d27ffd8fbcd6bc 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 cd2e195904435039b221b3cd2ba4fa9e0e59caf4..9c1b403948587bf2b73441a38b8e7281ecf7908f 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 ec75efa7d3f13615e0a72b8fb3b60ca9cc063606..aee2ea557547bbcf2f42b4e6fd018781a34efa54 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 1a4a23362360caa54ad1be6ae0a96ba3543fb039..a166292bd0f5bfaaceab4864e093e27ead8410f6 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 2a231741281c8611a37a22ac62e99351bef9d234..70be311e8187c9ead16ac74df0456f7559440e31 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 fee9a8ac37ef16f097b4fda5bcf254ce36f97c56..2d62d46987981b2fad788f45d1a32c0f489a1e6d 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 6b310095f0ffa697b0ac1503b4164c74a5d08622..6d1d3afe2380d3a8fea067c8e1a4bc7bfa7156cf 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 fa38aa211302931c4f836f12f2f99bc3f1391222..44dda2f0d805418a714dc43d47b8ab0d539dff79 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 1ea0307fc5346ec90db2218412e65e2766ea90ed..1cc626358c58795a1fae841eb6e29357c673db0c 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 bd4101cf0c2babbc334bc1ff70cca8ccc8555a44..bb22a1374eaf3ee2cf6159356a41affd2ca9fa81 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 b2d44a0d98cdce4921b63ce299d15fd8800a0389..68afbf758b989433177f2830f9bcf768604df783 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 6bcba860aaf145873fdc3e822d709544dd47ef07..cbb888e2edd58c18cb82a82583506f42c542f0f8 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 74cc6fcfdcac8b2dd569d327846a59fe793c6980..b59b11c089da71202cc9772671e0d2a4e1b2faca 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 112d2f9ba56cd770f671cf065fff22dc33c7fb96..26e48017e62fcc055aea65d7c9e659d0fe51fce5 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 e1b00ce10d7175630356d565f7278d3a438d1fa5..33cfcc9bc1a9912c926c19c2542c9568d461d38a 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: