Eliminate unsafeEqualityProof in CorePrep

The main idea here is to avoid treating
  * case e of {}
  * case unsafeEqualityProof of UnsafeRefl co -> blah
specially in CoreToStg.  Instead, nail them in CorePrep,
by converting

   case e of {}
     ==>   e |> unsafe-co

   case unsafeEqualityProof of UnsafeRefl cv -> blah
     ==> blah[unsafe-co/cv]

in GHC.Core.Prep.  Now expressions that we want to treat as trivial
really are trivial.  We can get rid of cpExprIsTrivial.

And we fix #19700.

A downside is that, at least under unsafeEqualityProof, we substitute
in types and coercions, which is more work. But a big advantage is
that it's all very simple and principled: CorePrep really gets rid of
the unsafeCoerce stuff, as it does empty case, runRW#, lazyId etc.

I've updated the overview in GHC.Core.Prep, and added
  Note [Unsafe coercions] in GHC.Core.Prep
  Note [Implementing unsafeCoerce] in base:Unsafe.Coerce

We get 3% fewer bytes allocated when compiling perf/compiler/T5631,
which uses a lot of unsafeCoerces.  (It's a happy-generated parser.)

Metric Decrease:
    T5631

(cherry picked from commit 6c7fff0b6f9514d6572cbe6bbfa4aafc259caebe)

23 files changed, 525 insertions, 223 deletions

diff --git a/compiler/GHC/Core.hs b/compiler/GHC/Core.hs
index 2c30b6f3d4..7f30fc5f00 100644
--- a/compiler/GHC/Core.hs
+++ b/compiler/GHC/Core.hs
@@ -259,7 +259,7 @@ data Expr b
   | Let   (Bind b) (Expr b)
   | Case  (Expr b) b Type [Alt b]   -- See Note [Case expression invariants]
                                     -- and Note [Why does Case have a 'Type' field?]
-  | Cast  (Expr b) Coercion
+  | Cast  (Expr b) CoercionR        -- The Coercion has Representational role
   | Tick  CoreTickish (Expr b)
   | Type  Type
   | Coercion Coercion
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 21e7202b96..4fcd366dfe 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -1352,6 +1352,7 @@ 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
 
@@ -1458,6 +1459,7 @@ 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)
@@ -2281,6 +2283,7 @@ 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 4783ac6fe1..14f8d2c71c 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -576,6 +576,7 @@ 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 cef3dc3cbe..67ad9b0384 100644
--- a/compiler/GHC/Core/FVs.hs
+++ b/compiler/GHC/Core/FVs.hs
@@ -404,6 +404,7 @@ 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
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index a3ea0bb1d3..e57b6d159d 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -2116,7 +2116,8 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
             ; checkWarnL (not lev_poly2)
                          (report "right-hand type is levity-polymorphic")
             ; when (not (lev_poly1 || lev_poly2)) $
-              do { checkWarnL (reps1 `equalLength` reps2)
+              do { checkWarnL (reps1 `equalLength` reps2 ||
+                               is_core_prep_prov prov)
                               (report "between values with different # of reps")
                  ; zipWithM_ validateCoercion reps1 reps2 }}
        where
@@ -2128,6 +2129,13 @@ 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
+     is_core_prep_prov CorePrepProv = True
+     is_core_prep_prov _            = False
+
      validateCoercion :: PrimRep -> PrimRep -> LintM ()
      validateCoercion rep1 rep2
        = do { platform <- targetPlatform <$> getDynFlags
@@ -2158,6 +2166,7 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
             ; return (ProofIrrelProv kco') }
 
      lint_prov _ _ prov@(PluginProv _) = return prov
+     lint_prov _ _ prov@CorePrepProv   = return prov
 
      check_kinds kco k1 k2
        = do { let Pair k1' k2' = coercionKind kco
diff --git a/compiler/GHC/Core/Subst.hs b/compiler/GHC/Core/Subst.hs
index 520bfd5d16..22cd6d5ca1 100644
--- a/compiler/GHC/Core/Subst.hs
+++ b/compiler/GHC/Core/Subst.hs
@@ -579,7 +579,7 @@ cloneTyVarBndr (Subst in_scope id_env tv_env cv_env) tv uniq
         (TCvSubst in_scope' tv_env' cv_env', tv')
            -> (Subst in_scope' id_env tv_env' cv_env', tv')
 
-substCoVarBndr :: Subst -> TyVar -> (Subst, TyVar)
+substCoVarBndr :: Subst -> CoVar -> (Subst, CoVar)
 substCoVarBndr (Subst in_scope id_env tv_env cv_env) cv
   = case Coercion.substCoVarBndr (TCvSubst in_scope tv_env cv_env) cv of
         (TCvSubst in_scope' tv_env' cv_env', cv')
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index 73ff22c85b..31c13676e5 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -650,6 +650,7 @@ 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
@@ -720,6 +721,7 @@ almost_devoid_co_var_of_prov (PhantomProv 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_type :: Type -> CoVar -> Bool
 almost_devoid_co_var_of_type (TyVarTy _) _ = True
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 636dc87405..079bb77c14 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -1541,12 +1541,15 @@ 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.Pprep
+
   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
@@ -1858,6 +1861,7 @@ 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
 
 {- *********************************************************************
 *                                                                      *
@@ -1914,6 +1918,7 @@ 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 39695bbc06..74fa6d1dfe 100644
--- a/compiler/GHC/Core/TyCo/Subst.hs
+++ b/compiler/GHC/Core/TyCo/Subst.hs
@@ -852,6 +852,7 @@ 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 20b7788cbc..c722b41e67 100644
--- a/compiler/GHC/Core/TyCo/Tidy.hs
+++ b/compiler/GHC/Core/TyCo/Tidy.hs
@@ -250,6 +250,7 @@ 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 5ed621d404..11070644f9 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -581,6 +581,7 @@ 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
@@ -914,6 +915,7 @@ 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
 
 
 {-
@@ -3107,6 +3109,7 @@ 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
 
 
 {-
@@ -3161,6 +3164,7 @@ 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
 
diff --git a/compiler/GHC/Core/Unfold.hs b/compiler/GHC/Core/Unfold.hs
index 8fdbc1b891..1af27fc045 100644
--- a/compiler/GHC/Core/Unfold.hs
+++ b/compiler/GHC/Core/Unfold.hs
@@ -278,7 +278,7 @@ 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 (U4a) in Note [Implementing unsafeCoerce].
+unsafeCoerce.  This is (U4) in Note [Implementing unsafeCoerce].
 
 Note [Computing the size of an expression]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs
index a4587d58ee..61f995a5c8 100644
--- a/compiler/GHC/CoreToIface.hs
+++ b/compiler/GHC/CoreToIface.hs
@@ -313,6 +313,8 @@ 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        = pprPanic "toIfaceCoercionX" empty
+         -- CorePrepProv only happens after the iface file is generated
 
 toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
 toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
diff --git a/compiler/GHC/CoreToStg.hs b/compiler/GHC/CoreToStg.hs
index d8a6dd0e95..45b94c2413 100644
--- a/compiler/GHC/CoreToStg.hs
+++ b/compiler/GHC/CoreToStg.hs
@@ -54,7 +54,6 @@ import GHC.Types.IPE
 import GHC.Types.Demand    ( isUsedOnceDmd )
 import GHC.Builtin.PrimOps ( PrimCall(..) )
 import GHC.Types.SrcLoc    ( mkGeneralSrcSpan )
-import GHC.Builtin.Names   ( unsafeEqualityProofName )
 
 import Control.Monad (ap)
 import Data.Maybe (fromMaybe)
@@ -269,12 +268,13 @@ coreTopBindsToStg
 coreTopBindsToStg _      _        env ccs []
   = (env, ccs, [])
 coreTopBindsToStg dflags this_mod env ccs (b:bs)
+  | NonRec _ rhs <- b, isTyCoArg rhs
+  = coreTopBindsToStg dflags this_mod env1 ccs1 bs
+  | otherwise
   = (env2, ccs2, b':bs')
   where
-        (env1, ccs1, b' ) =
-          coreTopBindToStg dflags this_mod env ccs b
-        (env2, ccs2, bs') =
-          coreTopBindsToStg dflags this_mod env1 ccs1 bs
+    (env1, ccs1, b' ) = coreTopBindToStg dflags this_mod env ccs b
+    (env2, ccs2, bs') = coreTopBindsToStg dflags this_mod env1 ccs1 bs
 
 coreTopBindToStg
         :: DynFlags
@@ -426,6 +426,7 @@ coreToStgExpr (Cast expr _)
 
 -- Cases require a little more real work.
 
+{-
 coreToStgExpr (Case scrut _ _ [])
   = coreToStgExpr scrut
     -- See Note [Empty case alternatives] in GHC.Core If the case
@@ -437,25 +438,20 @@ coreToStgExpr (Case scrut _ _ [])
     -- code generator, and put a return point anyway that calls a
     -- runtime system error function.
 
-
-coreToStgExpr e0@(Case scrut bndr _ alts) = do
-    alts2 <- extendVarEnvCts [(bndr, LambdaBound)] (mapM vars_alt alts)
-    scrut2 <- coreToStgExpr scrut
-    let stg = StgCase scrut2 bndr (mkStgAltType bndr alts) alts2
+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
+  = coreToStgExpr rhs
     -- See (U2) in Note [Implementing unsafeCoerce] in base:Unsafe.Coerce
-    case scrut2 of
-      StgApp id [] | idName id == unsafeEqualityProofName
-                   , isDeadBinder bndr ->
-        -- We can only discard the case if the case-binder is dead
-        -- It usually is, but see #18227
-        case alts2 of
-          [(_, [_co], rhs)] ->
-            return rhs
-          _ ->
-            pprPanic "coreToStgExpr" $
-              text "Unexpected unsafe equality case expression:" $$ ppr e0 $$
-              text "STG:" $$ pprStgExpr panicStgPprOpts stg
-      _ -> return stg
+-}
+
+-- The normal case for case-expressions
+coreToStgExpr (Case scrut bndr _ alts)
+  = do { scrut2 <- coreToStgExpr scrut
+       ; alts2 <- extendVarEnvCts [(bndr, LambdaBound)] (mapM vars_alt alts)
+       ; return (StgCase scrut2 bndr (mkStgAltType bndr alts) alts2) }
   where
     vars_alt :: CoreAlt -> CtsM (AltCon, [Var], StgExpr)
     vars_alt (Alt con binders rhs)
@@ -645,25 +641,24 @@ coreToStgLet
          -> CoreExpr     -- body
          -> CtsM StgExpr -- new let
 
-coreToStgLet bind body = do
-    (bind2, body2)
-       <- do
+coreToStgLet bind body
+  | NonRec _ rhs <- bind, isTyCoArg rhs
+  = coreToStgExpr body
 
-          ( bind2, env_ext)
-                <- vars_bind bind
+  | otherwise
+  = do { (bind2, env_ext) <- vars_bind bind
 
           -- Do the body
-          extendVarEnvCts env_ext $ do
-             body2 <- coreToStgExpr body
-
-             return (bind2, body2)
+         ; body2 <- extendVarEnvCts env_ext $
+                    coreToStgExpr body
 
         -- Compute the new let-expression
-    let
-        new_let | isJoinBind bind = StgLetNoEscape noExtFieldSilent bind2 body2
-                | otherwise       = StgLet noExtFieldSilent bind2 body2
+        ; let new_let | isJoinBind bind
+                      = StgLetNoEscape noExtFieldSilent bind2 body2
+                      | otherwise
+                      = StgLet noExtFieldSilent bind2 body2
 
-    return new_let
+        ; return new_let }
   where
     mk_binding binder rhs
         = (binder, LetBound NestedLet (manifestArity rhs))
diff --git a/compiler/GHC/CoreToStg/Prep.hs b/compiler/GHC/CoreToStg/Prep.hs
index af94cb92d7..c4394eae4c 100644
--- a/compiler/GHC/CoreToStg/Prep.hs
+++ b/compiler/GHC/CoreToStg/Prep.hs
@@ -49,6 +49,7 @@ 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
@@ -77,8 +78,10 @@ import GHC.Types.TyThing
 import GHC.Types.CostCentre ( CostCentre, ccFromThisModule )
 import GHC.Types.Unique.Supply
 
+import GHC.Data.Pair
 import Data.Bits
 import Data.List        ( unfoldr )
+import Data.Functor.Identity
 import Control.Monad
 import qualified Data.Set as S
 
@@ -144,10 +147,58 @@ The goal of this pass is to prepare for code generation.
     profiling mode. We have to do this here beucase we won't have unfoldings
     after this pass (see `zapUnfolding` and Note [Drop unfoldings and rules].
 
+13. Eliminate case clutter in favour of unsafe coercions.
+    See Note [Unsafe coercions]
+
+14. Eliminate some magic Ids, specifically
+     runRW# (\s. e)  ==>  e[readWorldId/s]
+             lazy e  ==>  e
+         noinline e  ==>  e
+     ToDo:  keepAlive# ...
+    This is done in cpeApp
+
 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:
+
+* 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.
+
+* 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 requiresuse ot 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 tranformations, 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).
 
 Note [CorePrep invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -403,7 +454,7 @@ cpeBind top_lvl env (NonRec bndr rhs)
                                    dmd is_unlifted
                                    env bndr1 rhs
        -- See Note [Inlining in CorePrep]
-       ; let triv_rhs = cpExprIsTrivial rhs1
+       ; let triv_rhs = exprIsTrivial rhs1
              env2    | triv_rhs  = extendCorePrepEnvExpr env1 bndr rhs1
                      | otherwise = env1
              floats1 | triv_rhs, isInternalName (idName bndr)
@@ -585,8 +636,10 @@ cpeRhsE :: CorePrepEnv -> CoreExpr -> UniqSM (Floats, CpeRhs)
 -- For example
 --      f (g x)   ===>   ([v = g x], f v)
 
-cpeRhsE _env expr@(Type {})      = return (emptyFloats, expr)
-cpeRhsE _env expr@(Coercion {})  = return (emptyFloats, expr)
+cpeRhsE env (Type ty)
+  = return (emptyFloats, Type (cpSubstTy env ty))
+cpeRhsE env (Coercion co)
+  = return (emptyFloats, Coercion (cpSubstCo env co))
 cpeRhsE env expr@(Lit (LitNumber nt i))
    = case cpe_convertNumLit env nt i of
       Nothing -> return (emptyFloats, expr)
@@ -619,7 +672,7 @@ cpeRhsE env (Tick tickish expr)
 
 cpeRhsE env (Cast expr co)
    = do { (floats, expr') <- cpeRhsE env expr
-        ; return (floats, Cast expr' co) }
+        ; return (floats, Cast expr' (cpSubstCo env co)) }
 
 cpeRhsE env expr@(Lam {})
    = do { let (bndrs,body) = collectBinders expr
@@ -627,19 +680,30 @@ cpeRhsE env expr@(Lam {})
         ; body' <- cpeBodyNF env' body
         ; return (emptyFloats, mkLams bndrs' body') }
 
-cpeRhsE env (Case scrut bndr ty alts)
+-- Eliminate empty case
+-- See Note [Unsafe coercions]
+cpeRhsE env (Case scrut _ ty [])
+  = do { (floats, scrut') <- cpeRhsE env scrut
+       ; let ty' = cpSubstTy env ty
+             co' = mkUnsafeCo Representational (exprType scrut') ty'
+       ; 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
-  , [Alt con bs rhs] <- alts
-  = do { (floats1, scrut') <- cpeBody env scrut
-       ; (env1, bndr')     <- cpCloneBndr env bndr
-       ; (env2, bs')       <- cpCloneBndrs env1 bs
-       ; (floats2, rhs')   <- cpeBody env2 rhs
-       ; let case_float = FloatCase scrut' bndr' con bs' True
-             floats'    = (floats1 `addFloat` case_float)
-                          `appendFloats` floats2
-       ; return (floats', rhs') }
+  , 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 = mkUnsafeCo Nominal (cpSubstTy env ty1) (cpSubstTy env ty2)
+        env'   = extendCoVarEnv env co_var the_co
+  = cpeRhsE env' rhs
 
-  | otherwise
+cpeRhsE env (Case scrut bndr ty alts)
   = do { (floats, scrut') <- cpeBody env scrut
        ; (env', bndr2) <- cpCloneBndr env bndr
        ; let alts'
@@ -715,9 +779,9 @@ rhsToBody expr@(Lam {})
   | all isTyVar bndrs           -- Type lambdas are ok
   = return (emptyFloats, expr)
   | otherwise                   -- Some value lambdas
-  = do { fn <- newVar (exprType expr)
-       ; let rhs   = cpeEtaExpand (exprArity expr) expr
-             float = FloatLet (NonRec fn rhs)
+  = do { let rhs = cpeEtaExpand (exprArity expr) expr
+       ; fn <- newVar (exprType rhs)
+       ; let float = FloatLet (NonRec fn rhs)
        ; return (unitFloat float, Var fn) }
   where
     (bndrs,body) = collectBinders expr
@@ -808,7 +872,7 @@ cpeApp top_env expr
           : CpeApp s0
           : CpeApp k
           : rest <- args
-        = do { y <- newVar result_ty
+        = do { y  <- newVar (cpSubstTy env result_ty)
              ; s2 <- newVar realWorldStatePrimTy
              ; -- beta reduce if possible
              ; (floats, k') <- case k of
@@ -846,7 +910,7 @@ cpeApp top_env expr
            -- Apps it is under are type applications only (c.f.
            -- exprIsTrivial).  But note that we need the type of the
            -- expression, not the id.
-           ; (app, floats) <- rebuild_app args e2 (exprType e2) emptyFloats stricts
+           ; (app, floats) <- rebuild_app env args e2 emptyFloats stricts
            ; mb_saturate hd app floats depth }
         where
           stricts = case idStrictness v of
@@ -866,13 +930,11 @@ cpeApp top_env expr
 
         -- N-variable fun, better let-bind it
     cpe_app env fun args depth
-      = do { (fun_floats, fun') <- cpeArg env evalDmd fun ty
+      = do { (fun_floats, fun') <- cpeArg env evalDmd fun
                           -- The evalDmd says that it's sure to be evaluated,
                           -- so we'll end up case-binding it
-           ; (app, floats) <- rebuild_app args fun' ty fun_floats []
+           ; (app, floats) <- rebuild_app env args fun' fun_floats []
            ; mb_saturate Nothing app floats depth }
-        where
-          ty = exprType fun
 
     -- Saturate if necessary
     mb_saturate head app floats depth =
@@ -887,38 +949,45 @@ cpeApp top_env expr
     -- all of which are used to possibly saturate this application if it
     -- has a constructor or primop at the head.
     rebuild_app
-        :: [ArgInfo]                  -- The arguments (inner to outer)
+        :: CorePrepEnv
+        -> [ArgInfo]                  -- The arguments (inner to outer)
         -> CpeApp
-        -> Type
         -> Floats
         -> [Demand]
         -> UniqSM (CpeApp, Floats)
-    rebuild_app [] app _ floats ss = do
-      MASSERT(null ss) -- make sure we used all the strictness info
-      return (app, floats)
-    rebuild_app (a : as) fun' fun_ty floats ss = case a of
-      CpeApp arg@(Type arg_ty) ->
-        rebuild_app as (App fun' arg) (piResultTy fun_ty arg_ty) floats ss
-      CpeApp arg@(Coercion {}) ->
-        rebuild_app as (App fun' arg) (funResultTy fun_ty) floats ss
+    rebuild_app _ [] app floats ss
+      = ASSERT(null ss) -- make sure we used all the strictness info
+        return (app, floats)
+
+    rebuild_app env (a : as) fun' floats ss = case a of
+
+      CpeApp (Type arg_ty)
+        -> rebuild_app env as (App fun' (Type arg_ty')) floats ss
+        where
+          arg_ty' = cpSubstTy env arg_ty
+
+      CpeApp (Coercion co)
+        -> rebuild_app env as (App fun' (Coercion co')) floats ss
+        where
+            co' = cpSubstCo env co
+
       CpeApp arg -> do
         let (ss1, ss_rest)  -- See Note [lazyId magic] in GHC.Types.Id.Make
                = case (ss, isLazyExpr arg) of
                    (_   : ss_rest, True)  -> (topDmd, ss_rest)
                    (ss1 : ss_rest, False) -> (ss1,    ss_rest)
                    ([],            _)     -> (topDmd, [])
-            (_, arg_ty, res_ty) =
-              case splitFunTy_maybe fun_ty of
-                Just as -> as
-                Nothing -> pprPanic "cpeBody" (ppr fun_ty $$ ppr expr)
-        (fs, arg') <- cpeArg top_env ss1 arg arg_ty
-        rebuild_app as (App fun' arg') res_ty (fs `appendFloats` floats) ss_rest
-      CpeCast co ->
-        let ty2 = coercionRKind co
-        in rebuild_app as (Cast fun' co) ty2 floats ss
-      CpeTick tickish ->
+        (fs, arg') <- cpeArg top_env ss1 arg
+        rebuild_app env as (App fun' arg') (fs `appendFloats` floats) ss_rest
+
+      CpeCast co
+        -> rebuild_app env as (Cast fun' co') floats ss
+        where
+           co' = cpSubstCo env co
+
+      CpeTick tickish
         -- See [Floating Ticks in CorePrep]
-        rebuild_app as fun' fun_ty (addFloat floats (FloatTick tickish)) ss
+        -> rebuild_app env as fun' (addFloat floats (FloatTick tickish)) ss
 
 isLazyExpr :: CoreExpr -> Bool
 -- See Note [lazyId magic] in GHC.Types.Id.Make
@@ -1143,30 +1212,24 @@ However, until then we simply add a special case excluding literals from the
 floating done by cpeArg.
 -}
 
+mkUnsafeCo :: Role -> Type -> Type -> Coercion
+mkUnsafeCo role ty1 ty2 = mkUnivCo CorePrepProv role ty1 ty2
+
 -- | Is an argument okay to CPE?
 okCpeArg :: CoreExpr -> Bool
 -- Don't float literals. See Note [ANF-ising literal string arguments].
 okCpeArg (Lit _) = False
 -- Do not eta expand a trivial argument
-okCpeArg expr    = not (cpExprIsTrivial expr)
-
-cpExprIsTrivial :: CoreExpr -> Bool
-cpExprIsTrivial e
-  | Tick t e <- e
-  , not (tickishIsCode t)
-  = cpExprIsTrivial e
-  | Case scrut _ _ alts <- e
-  , isUnsafeEqualityProof scrut
-  , [Alt _ _ rhs] <- alts
-  = cpExprIsTrivial rhs
-  | otherwise
-  = exprIsTrivial e
+okCpeArg expr    = not (exprIsTrivial expr)
 
 -- This is where we arrange that a non-trivial argument is let-bound
 cpeArg :: CorePrepEnv -> Demand
-       -> CoreArg -> Type -> UniqSM (Floats, CpeArg)
-cpeArg env dmd arg arg_ty
+       -> CoreArg -> UniqSM (Floats, CpeArg)
+cpeArg env dmd arg
   = do { (floats1, arg1) <- cpeRhsE env arg     -- arg1 can be a lambda
+       ; let arg_ty      = exprType arg1
+             is_unlifted = isUnliftedType arg_ty
+             want_float  = wantFloatNested NonRecursive dmd is_unlifted
        ; (floats2, arg2) <- if want_float floats1 arg1
                             then return (floats1, arg1)
                             else dontFloat floats1 arg1
@@ -1180,9 +1243,6 @@ cpeArg env dmd arg arg_ty
                  ; return (addFloat floats2 arg_float, varToCoreExpr v) }
          else return (floats2, arg2)
        }
-  where
-    is_unlifted = isUnliftedType arg_ty
-    want_float  = wantFloatNested NonRecursive dmd is_unlifted
 
 {-
 Note [Floating unlifted arguments]
@@ -1345,7 +1405,7 @@ Note [Speculative evaluation]
 Since call-by-value is much cheaper than call-by-need, we case-bind arguments
 that are either
 
-  1. Strictly evaluated anyway, according to the StrictSig of the callee, or
+  1. Strictly evaluated anyway, according to the DmdSig of the callee, or
   2. ok-for-spec, according to 'exprOkForSpeculation'
 
 While (1) is a no-brainer and always beneficial, (2) is a bit
@@ -1622,104 +1682,20 @@ 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_convertNumLit   :: LitNumType -> Integer -> Maybe CoreExpr
         -- ^ Convert some numeric literals (Integer, Natural) into their
         -- final Core form
     }
 
--- | Create a function that converts Bignum literals into their final CoreExpr
-mkConvertNumLiteral
-   :: HscEnv
-   -> IO (LitNumType -> Integer -> Maybe CoreExpr)
-mkConvertNumLiteral hsc_env = do
-   let
-      dflags   = hsc_dflags hsc_env
-      platform = targetPlatform dflags
-      home_unit = hsc_home_unit hsc_env
-      guardBignum act
-         | isHomeUnitInstanceOf home_unit primUnitId
-         = return $ panic "Bignum literals are not supported in ghc-prim"
-         | isHomeUnitInstanceOf home_unit bignumUnitId
-         = return $ panic "Bignum literals are not supported in ghc-bignum"
-         | otherwise = act
-
-      lookupBignumId n      = guardBignum (tyThingId <$> lookupGlobal hsc_env n)
-
-   -- The lookup is done here but the failure (panic) is reported lazily when we
-   -- try to access the `bigNatFromWordList` function.
-   --
-   -- If we ever get built-in ByteArray# literals, we could avoid the lookup by
-   -- directly using the Integer/Natural wired-in constructors for big numbers.
-
-   bignatFromWordListId <- lookupBignumId bignatFromWordListName
-
-   let
-      convertNumLit nt i = case nt of
-         LitNumInteger -> Just (convertInteger i)
-         LitNumNatural -> Just (convertNatural i)
-         _             -> Nothing
-
-      convertInteger i
-         | platformInIntRange platform i -- fit in a Int#
-         = mkConApp integerISDataCon [Lit (mkLitInt platform i)]
-
-         | otherwise -- build a BigNat and embed into IN or IP
-         = let con = if i > 0 then integerIPDataCon else integerINDataCon
-           in mkBigNum con (convertBignatPrim (abs i))
-
-      convertNatural i
-         | platformInWordRange platform i -- fit in a Word#
-         = mkConApp naturalNSDataCon [Lit (mkLitWord platform i)]
-
-         | otherwise --build a BigNat and embed into NB
-         = mkBigNum naturalNBDataCon (convertBignatPrim i)
-
-      -- we can't simply generate:
-      --
-      --    NB (bigNatFromWordList# [W# 10, W# 20])
-      --
-      -- using `mkConApp` because it isn't in ANF form. Instead we generate:
-      --
-      --    case bigNatFromWordList# [W# 10, W# 20] of ba { DEFAULT -> NB ba }
-      --
-      -- via `mkCoreApps`
-
-      mkBigNum con ba = mkCoreApps (Var (dataConWorkId con)) [ba]
-
-      convertBignatPrim i =
-         let
-            target    = targetPlatform dflags
-
-            -- ByteArray# literals aren't supported (yet). Were they supported,
-            -- we would use them directly. We would need to handle
-            -- wordSize/endianness conversion between host and target
-            -- wordSize  = platformWordSize platform
-            -- byteOrder = platformByteOrder platform
-
-            -- For now we build a list of Words and we produce
-            -- `bigNatFromWordList# list_of_words`
-
-            words = mkListExpr wordTy (reverse (unfoldr f i))
-               where
-                  f 0 = Nothing
-                  f x = let low  = x .&. mask
-                            high = x `shiftR` bits
-                        in Just (mkConApp wordDataCon [Lit (mkLitWord platform low)], high)
-                  bits = platformWordSizeInBits target
-                  mask = 2 ^ bits - 1
-
-         in mkApps (Var bignatFromWordListId) [words]
-
-
-   return convertNumLit
-
-
 mkInitialCorePrepEnv :: HscEnv -> IO CorePrepEnv
 mkInitialCorePrepEnv hsc_env = do
    convertNumLit <- mkConvertNumLiteral hsc_env
    return $ CPE
-      { cpe_dynFlags = hsc_dflags hsc_env
-      , cpe_env = emptyVarEnv
+      { cpe_dynFlags      = hsc_dflags hsc_env
+      , cpe_env           = emptyVarEnv
+      , cpe_tyco_env      = Nothing
       , cpe_convertNumLit = convertNumLit
       }
 
@@ -1743,6 +1719,117 @@ lookupCorePrepEnv cpe id
         Just exp -> exp
 
 ------------------------------------------------------------------------------
+--           CpeTyCoEnv
+-- ---------------------------------------------------------------------------
+
+{- Note [CpeTyCoEnv]
+~~~~~~~~~~~~~~~~~~~~
+The cpe_tyco_env :: Maybe CpeTyCoEnv field carries a substitution
+for type and coercion varibles
+
+* 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 -> if isTyVar tcv
+                                      then return (subst_tv_bndr env tcv)
+                                      else return (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
 -- ---------------------------------------------------------------------------
 
@@ -1751,8 +1838,11 @@ cpCloneBndrs env bs = mapAccumLM cpCloneBndr env bs
 
 cpCloneBndr  :: CorePrepEnv -> InVar -> UniqSM (CorePrepEnv, OutVar)
 cpCloneBndr env bndr
-  | not (isId bndr)
-  = return (env, bndr)
+  | isTyVar bndr
+  = return (cpSubstTyVarBndr env bndr)
+
+  | isCoVar bndr
+  = return (cpSubstCoVarBndr env bndr)
 
   | otherwise
   = do { bndr' <- clone_it bndr
@@ -1769,11 +1859,13 @@ cpCloneBndr env bndr
        ; return (extendCorePrepEnv env bndr bndr'', bndr'') }
   where
     clone_it bndr
-      | isLocalId bndr, not (isCoVar bndr)
-      = do { uniq <- getUniqueM; return (setVarUnique bndr uniq) }
+      | isLocalId bndr
+      = do { uniq <- getUniqueM
+           ; let ty' = cpSubstTy env (idType bndr)
+           ; return (setVarUnique (setIdType bndr ty') uniq) }
+
       | otherwise   -- Top level things, which we don't want
                     -- to clone, have become GlobalIds by now
-                    -- And we don't clone tyvars, or coercion variables
       = return bndr
 
 {- Note [Drop unfoldings and rules]
@@ -1906,3 +1998,95 @@ collectCostCentres mod_name
     -- Unfoldings may have cost centres that in the original definion are
     -- optimized away, see #5889.
     get_unf = maybeUnfoldingTemplate . realIdUnfolding
+
+
+------------------------------------------------------------------------------
+-- Numeric literals
+-- ---------------------------------------------------------------------------
+
+-- | Create a function that converts Bignum literals into their final CoreExpr
+mkConvertNumLiteral
+   :: HscEnv
+   -> IO (LitNumType -> Integer -> Maybe CoreExpr)
+mkConvertNumLiteral hsc_env = do
+   let
+      dflags   = hsc_dflags hsc_env
+      platform = targetPlatform dflags
+      home_unit = hsc_home_unit hsc_env
+      guardBignum act
+         | isHomeUnitInstanceOf home_unit primUnitId
+         = return $ panic "Bignum literals are not supported in ghc-prim"
+         | isHomeUnitInstanceOf home_unit bignumUnitId
+         = return $ panic "Bignum literals are not supported in ghc-bignum"
+         | otherwise = act
+
+      lookupBignumId n      = guardBignum (tyThingId <$> lookupGlobal hsc_env n)
+
+   -- The lookup is done here but the failure (panic) is reported lazily when we
+   -- try to access the `bigNatFromWordList` function.
+   --
+   -- If we ever get built-in ByteArray# literals, we could avoid the lookup by
+   -- directly using the Integer/Natural wired-in constructors for big numbers.
+
+   bignatFromWordListId <- lookupBignumId bignatFromWordListName
+
+   let
+      convertNumLit nt i = case nt of
+         LitNumInteger -> Just (convertInteger i)
+         LitNumNatural -> Just (convertNatural i)
+         _             -> Nothing
+
+      convertInteger i
+         | platformInIntRange platform i -- fit in a Int#
+         = mkConApp integerISDataCon [Lit (mkLitInt platform i)]
+
+         | otherwise -- build a BigNat and embed into IN or IP
+         = let con = if i > 0 then integerIPDataCon else integerINDataCon
+           in mkBigNum con (convertBignatPrim (abs i))
+
+      convertNatural i
+         | platformInWordRange platform i -- fit in a Word#
+         = mkConApp naturalNSDataCon [Lit (mkLitWord platform i)]
+
+         | otherwise --build a BigNat and embed into NB
+         = mkBigNum naturalNBDataCon (convertBignatPrim i)
+
+      -- we can't simply generate:
+      --
+      --    NB (bigNatFromWordList# [W# 10, W# 20])
+      --
+      -- using `mkConApp` because it isn't in ANF form. Instead we generate:
+      --
+      --    case bigNatFromWordList# [W# 10, W# 20] of ba { DEFAULT -> NB ba }
+      --
+      -- via `mkCoreApps`
+
+      mkBigNum con ba = mkCoreApps (Var (dataConWorkId con)) [ba]
+
+      convertBignatPrim i =
+         let
+            target    = targetPlatform dflags
+
+            -- ByteArray# literals aren't supported (yet). Were they supported,
+            -- we would use them directly. We would need to handle
+            -- wordSize/endianness conversion between host and target
+            -- wordSize  = platformWordSize platform
+            -- byteOrder = platformByteOrder platform
+
+            -- For now we build a list of Words and we produce
+            -- `bigNatFromWordList# list_of_words`
+
+            words = mkListExpr wordTy (reverse (unfoldr f i))
+               where
+                  f 0 = Nothing
+                  f x = let low  = x .&. mask
+                            high = x `shiftR` bits
+                        in Just (mkConApp wordDataCon [Lit (mkLitWord platform low)], high)
+                  bits = platformWordSizeInBits target
+                  mask = 2 ^ bits - 1
+
+         in mkApps (Var bignatFromWordListId) [words]
+
+
+   return convertNumLit
+
diff --git a/compiler/GHC/StgToByteCode.hs b/compiler/GHC/StgToByteCode.hs
index 4d9dc0b4e1..68efa16fe5 100644
--- a/compiler/GHC/StgToByteCode.hs
+++ b/compiler/GHC/StgToByteCode.hs
@@ -466,7 +466,7 @@ schemeR :: [Id]                 -- Free vars of the RHS, ordered as they
 schemeR fvs (nm, rhs)
    = schemeR_wrk fvs nm rhs (collect rhs)
 
--- If an expression is a lambda (after apply bcView), return the
+-- If an expression is a lambda, return the
 -- list of arguments to the lambda (in R-to-L order) and the
 -- underlying expression
 
diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
index 6c8daa0d56..7c56b12324 100644
--- a/compiler/GHC/Tc/TyCl/Utils.hs
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -153,6 +153,7 @@ 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 b6f5065997..c241c717ae 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1531,6 +1531,7 @@ collect_cand_qtvs_co orig_ty 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/Types/Id/Make.hs b/compiler/GHC/Types/Id/Make.hs
index 2fe11c66a7..633accada8 100644
--- a/compiler/GHC/Types/Id/Make.hs
+++ b/compiler/GHC/Types/Id/Make.hs
@@ -764,7 +764,7 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
     tycon        = dataConTyCon data_con       -- The representation TyCon (not family)
     wrap_ty      = dataConWrapperType data_con
     ev_tys       = eqSpecPreds eq_spec ++ theta
-    all_arg_tys  = (map unrestricted ev_tys) ++ orig_arg_tys
+    all_arg_tys  = map unrestricted ev_tys ++ orig_arg_tys
     ev_ibangs    = map (const HsLazy) ev_tys
     orig_bangs   = dataConSrcBangs data_con
 
diff --git a/libraries/base/Unsafe/Coerce.hs b/libraries/base/Unsafe/Coerce.hs
index 07d1f2da9f..5ebc9c637e 100644
--- a/libraries/base/Unsafe/Coerce.hs
+++ b/libraries/base/Unsafe/Coerce.hs
@@ -90,10 +90,10 @@ several ways
 
 (U1) unsafeEqualityProof is /never/ inlined.
 
-(U2) In CoreToStg.coreToStg, we transform
-       case unsafeEqualityProof of UnsafeRefl -> blah
+(U2) In CoreToStg.Prep, we transform
+       case unsafeEqualityProof of UnsafeRefl g -> blah
       ==>
-       blah
+       blah[unsafe-co/g]
 
      This eliminates the overhead of evaluating the unsafe
      equality proof.
@@ -127,18 +127,15 @@ several ways
      and produce a thunk even after discarding the unsafeEqualityProof.
      So instead we float out the case to give
         case unsafeEqualityProof ... of { UnsafeRefl ->
-        let a = K e
+        let a = e
             x = K a
-        in ...
-     Flaoting the case is OK here, even though it broardens the
+        in ...  }
+     Floating the case is OK here, even though it broadens the
      scope, because we are done with simplification.
 
-(U4) GHC.CoreToStg.Prep.cpeExprIsTrivial anticipates the
-     upcoming discard of unsafeEqualityProof.
-
-(U4a) Ditto GHC.Core.Unfold.inlineBoringOk we want to treat
-      the RHS of unsafeCoerce as very small; see
-      Note [Inline unsafeCoerce] in that module.
+(U4) Ditto GHC.Core.Unfold.inlineBoringOk we want to treat
+     the RHS of unsafeCoerce as very small; see
+     Note [Inline unsafeCoerce] in that module.
 
 (U5) The definition of unsafeEqualityProof in Unsafe.Coerce
      looks very strange:
@@ -212,17 +209,6 @@ There are yet more wrinkles
       the kind-/homogeneous/ unsafeEqualityProof twice.
 
       See Note [Wiring in unsafeCoerce#] in Desugar.
-
-(U11) We must also be careful to discard unsafeEqualityProof in the
-      bytecode generator; see ByteCodeGen.bcView.  Here we don't really
-      care about fast execution, but (annoyingly) we /do/ care about the
-      GHCi debugger, and GHCi itself uses unsafeCoerce.
-
-      Moreover, in GHC.Tc.Module.tcGhciStmts we use unsafeCoerce#, rather
-      than the more kosher unsafeCoerce, because (with -O0) the latter
-      may not be inlined.
-
-      Sigh
 -}
 
 -- | This type is treated magically within GHC. Any pattern match of the
diff --git a/testsuite/tests/core-to-stg/Makefile b/testsuite/tests/core-to-stg/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/core-to-stg/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/core-to-stg/T19700.hs b/testsuite/tests/core-to-stg/T19700.hs
new file mode 100644
index 0000000000..25f0ab5629
--- /dev/null
+++ b/testsuite/tests/core-to-stg/T19700.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UnboxedTuples #-}
+module T19700 where
+
+import GHC.Exts (Int(..), Int#, SmallArray#, SmallMutableArray#, State#,
+                 indexSmallArray#, newSmallArray#, sizeofSmallArray#, unsafeFreezeSmallArray#, writeSmallArray#)
+import GHC.ST (ST(..), runST)
+import Prelude hiding (length)
+
+-- | /O(n)/ Transform this map by applying a function to every value.
+mapWithKey :: (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
+mapWithKey f = go
+  where
+    go Empty                 = Empty
+    go (Leaf h (L k v))      = leaf h k (f k v)
+    go (BitmapIndexed b ary) = BitmapIndexed b $ map' go ary
+    go (Full ary)            = Full $ map' go ary
+    go (Collision h ary)     =
+        Collision h $ map' (\ (L k v) -> let !v' = f k v in L k v') ary
+{-# INLINE mapWithKey #-}
+
+leaf :: Hash -> k -> v -> HashMap k v
+leaf h k = \ !v -> Leaf h (L k v)
+{-# INLINE leaf #-}
+
+data Leaf k v = L !k !v
+
+data HashMap k v
+    = Empty
+    | BitmapIndexed !Bitmap !(Array (HashMap k v))
+    | Leaf !Hash !(Leaf k v)
+    | Full !(Array (HashMap k v))
+    | Collision !Hash !(Array (Leaf k v))
+
+type Hash   = Word
+type Bitmap = Word
+
+data Array a = Array {
+      unArray :: !(SmallArray# a)
+    }
+
+data MArray s a = MArray {
+      unMArray :: !(SmallMutableArray# s a)
+    }
+
+indexM :: Array a -> Int -> ST s a
+indexM ary _i@(I# i#) =
+        case indexSmallArray# (unArray ary) i# of (# b #) -> return b
+{-# INLINE indexM #-}
+
+length :: Array a -> Int
+length ary = I# (sizeofSmallArray# (unArray ary))
+{-# INLINE length #-}
+
+map' :: (a -> b) -> Array a -> Array b
+map' f = \ ary ->
+    let !n = length ary
+    in run $ do
+        mary <- new_ n
+        go ary mary 0 n
+  where
+    go ary mary i n
+        | i >= n    = return mary
+        | otherwise = do
+             x <- indexM ary i
+             write mary i $! f x
+             go ary mary (i+1) n
+{-# INLINE map' #-}
+
+new :: Int -> a -> ST s (MArray s a)
+new (I# n#) !b =
+    ST $ \s ->
+        case newSmallArray# n# b s of
+            (# s', ary #) -> (# s', MArray ary #)
+{-# INLINE new #-}
+
+new_ :: Int -> ST s (MArray s a)
+new_ n = new n undefinedElem
+
+run :: (forall s . ST s (MArray s e)) -> Array e
+run act = runST $ act >>= unsafeFreeze
+{-# INLINE run #-}
+
+undefinedElem :: a
+undefinedElem = error "Data.Strict.HashMap.Autogen.Internal.Array: Undefined element"
+{-# NOINLINE undefinedElem #-}
+
+unsafeFreeze :: MArray s a -> ST s (Array a)
+unsafeFreeze mary
+    = ST $ \s -> case unsafeFreezeSmallArray# (unMArray mary) s of
+                   (# s', ary #) -> (# s', Array ary #)
+{-# INLINE unsafeFreeze #-}
+
+write :: MArray s a -> Int -> a -> ST s ()
+write ary _i@(I# i#) !b = ST $ \ s ->
+        case writeSmallArray# (unMArray ary) i# b s of
+            s' -> (# s' , () #)
+{-# INLINE write #-}
diff --git a/testsuite/tests/core-to-stg/all.T b/testsuite/tests/core-to-stg/all.T
new file mode 100644
index 0000000000..baab982cb4
--- /dev/null
+++ b/testsuite/tests/core-to-stg/all.T
@@ -0,0 +1,3 @@
+# Tests for CorePrep and CoreToStg
+
+test('T19700', normal, compile, ['-O'])