Eliminate unsafeEqualityProof in CorePrepwip/T19700

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

11 files changed, 30 insertions, 3 deletions

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 66ba8ee8ab..72c96c962a 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -594,6 +594,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 3438f372fc..a5da50bd1d 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 e0f153287f..f60b60b02b 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 aa5423d0f6..1e6f2d08ef 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -1540,12 +1540,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
@@ -1857,6 +1860,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
 
 {- *********************************************************************
 *                                                                      *
@@ -1913,6 +1917,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 d25135af06..570096fd42 100644
--- a/compiler/GHC/Core/TyCo/Tidy.hs
+++ b/compiler/GHC/Core/TyCo/Tidy.hs
@@ -261,6 +261,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 93b41c1c3b..49a10c5a39 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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~