Persist CorePrepProv into IfaceUnivCoProvwip/T19768

CorePrepProv is only created in CorePrep, so I thought it wouldn't be
needed in IfaceUnivCoProv.  But actually IfaceSyn is used during
pretty-printing, and we can certainly pretty-print things after
CorePrep as #19768 showed.

So the simplest thing is to represent CorePrepProv in IfaceSyn.

To improve what Lint can do I also added a boolean to CorePrepProv, to
record whether it is homogeneously kinded or not. It is introduced in
two distinct ways (see Note [Unsafe coercions] in GHC.CoreToStg.Prep),
one of which may be hetero-kinded (e.g. Int ~ Int#) beause it is
casting a divergent expression; but the other is not.  The boolean
keeps track.

16 files changed, 84 insertions, 63 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 4fcd366dfe..b364091958 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -1352,7 +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
+                     CorePrepProv _   -> True
       = Just $ UnivCo prov Nominal co1 co2
     setNominalRole_maybe_helper _ = Nothing
 
@@ -1456,10 +1456,10 @@ promoteCoercion co = case co of
     AxiomInstCo {} -> mkKindCo co
     AxiomRuleCo {} -> mkKindCo co
 
-    UnivCo (PhantomProv kco) _ _ _    -> kco
+    UnivCo (PhantomProv kco)    _ _ _ -> kco
     UnivCo (ProofIrrelProv kco) _ _ _ -> kco
-    UnivCo (PluginProv _) _ _ _       -> mkKindCo co
-    UnivCo CorePrepProv _ _ _         -> mkKindCo co
+    UnivCo (PluginProv _)       _ _ _ -> mkKindCo co
+    UnivCo (CorePrepProv _)     _ _ _ -> mkKindCo co
 
     SymCo g
       -> mkSymCo (promoteCoercion g)
@@ -2283,7 +2283,7 @@ seqProv :: UnivCoProvenance -> ()
 seqProv (PhantomProv co)    = seqCo co
 seqProv (ProofIrrelProv co) = seqCo co
 seqProv (PluginProv _)      = ()
-seqProv CorePrepProv        = ()
+seqProv (CorePrepProv _)    = ()
 
 seqCos :: [Coercion] -> ()
 seqCos []       = ()
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 72c96c962a..62b83bd8c1 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -594,7 +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
+      CorePrepProv _     -> prov
 
 -------------
 opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
diff --git a/compiler/GHC/Core/FVs.hs b/compiler/GHC/Core/FVs.hs
index 67ad9b0384..1fbf119172 100644
--- a/compiler/GHC/Core/FVs.hs
+++ b/compiler/GHC/Core/FVs.hs
@@ -404,7 +404,7 @@ orphNamesOfProv :: UnivCoProvenance -> NameSet
 orphNamesOfProv (PhantomProv co)    = orphNamesOfCo co
 orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co
 orphNamesOfProv (PluginProv _)      = emptyNameSet
-orphNamesOfProv CorePrepProv        = 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 74b6ca7e9a..b3ed2ce8eb 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -2108,13 +2108,15 @@ 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 (not lev_poly1)
                          (report "left-hand type is levity-polymorphic")
             ; checkWarnL (not lev_poly2)
                          (report "right-hand type is levity-polymorphic")
             ; when (not (lev_poly1 || lev_poly2)) $
-              do { checkWarnL (reps1 `equalLength` reps2 ||
-                               is_core_prep_prov prov)
+              do { checkWarnL (reps1 `equalLength` reps2)
                               (report "between values with different # of reps")
                  ; zipWithM_ validateCoercion reps1 reps2 }}
        where
@@ -2130,8 +2132,8 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
      --  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
+     allow_ill_kinded_univ_co (CorePrepProv homo_kind) = not homo_kind
+     allow_ill_kinded_univ_co _                        = False
 
      validateCoercion :: PrimRep -> PrimRep -> LintM ()
      validateCoercion rep1 rep2
@@ -2162,8 +2164,8 @@ 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
+     lint_prov _ _ prov@(CorePrepProv _) = return prov
 
      check_kinds kco k1 k2
        = do { let Pair k1' k2' = coercionKind kco
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index 31c13676e5..0cc06e0fa6 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -650,7 +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
+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,8 +720,8 @@ 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_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 1e6f2d08ef..eec0d91f0c 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -1540,7 +1540,9 @@ 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
+  | 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
 
@@ -1548,7 +1550,7 @@ 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)"
+  ppr (CorePrepProv _)   = text "(CorePrep)"
 
 -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
 data CoercionHole
@@ -1860,7 +1862,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
+    go_prov _   (CorePrepProv _)    = mempty
 
 {- *********************************************************************
 *                                                                      *
@@ -1917,7 +1919,7 @@ provSize :: UnivCoProvenance -> Int
 provSize (PhantomProv co)    = 1 + coercionSize co
 provSize (ProofIrrelProv co) = 1 + coercionSize co
 provSize (PluginProv _)      = 1
-provSize CorePrepProv        = 1
+provSize (CorePrepProv _)    = 1
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs
index 74fa6d1dfe..e9c9b85a23 100644
--- a/compiler/GHC/Core/TyCo/Subst.hs
+++ b/compiler/GHC/Core/TyCo/Subst.hs
@@ -852,7 +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
+    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 570096fd42..96cbed6ade 100644
--- a/compiler/GHC/Core/TyCo/Tidy.hs
+++ b/compiler/GHC/Core/TyCo/Tidy.hs
@@ -261,7 +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
+    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 0b82442412..1f2872e056 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -581,7 +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
+    go_prov _     p@(CorePrepProv _)  = p
 
       -- the "False" and "const" are to accommodate the type of
       -- substForAllCoBndrUsing, which is general enough to
@@ -915,7 +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
+    go_prov _   p@(CorePrepProv _)  = return p
 
 
 {-
@@ -3140,7 +3140,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
+    go_prov _   p@(CorePrepProv _)  = return p
 
 
 {-
@@ -3195,7 +3195,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
+     go_prov (CorePrepProv _)    = emptyUniqSet
         -- this last case can happen from the tyConsOfType used from
         -- checkTauTvUpdate
 
diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs
index 3add18ff02..b9980a0edf 100644
--- a/compiler/GHC/CoreToIface.hs
+++ b/compiler/GHC/CoreToIface.hs
@@ -313,8 +313,7 @@ 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
+    go_prov (CorePrepProv b)    = IfaceCorePrepProv b
 
 toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
 toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
diff --git a/compiler/GHC/CoreToStg/Prep.hs b/compiler/GHC/CoreToStg/Prep.hs
index c4169b5029..48817f0439 100644
--- a/compiler/GHC/CoreToStg/Prep.hs
+++ b/compiler/GHC/CoreToStg/Prep.hs
@@ -164,32 +164,32 @@ Note [Unsafe coercions]
 ~~~~~~~~~~~~~~~~~~~~~~~
 CorePrep does these two transformations:
 
-* Convert empty case to cast with an unsafe coercion
+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.
-
-* 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.
+   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 tranformations, so the reasons
@@ -197,7 +197,10 @@ 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).
+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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -683,8 +686,14 @@ cpeRhsE env expr@(Lam {})
 -- 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'
+       ; 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
@@ -698,7 +707,8 @@ cpeRhsE env (Case scrut bndr _ alts)
                       -- 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)
+        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
 
@@ -1211,9 +1221,6 @@ 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].
diff --git a/compiler/GHC/Iface/Syntax.hs b/compiler/GHC/Iface/Syntax.hs
index dfc39fb244..fe1fa6a58f 100644
--- a/compiler/GHC/Iface/Syntax.hs
+++ b/compiler/GHC/Iface/Syntax.hs
@@ -1690,6 +1690,7 @@ 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 b90676f062..034198bd9a 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -396,6 +396,7 @@ data IfaceUnivCoProv
   = IfacePhantomProv IfaceCoercion
   | IfaceProofIrrelProv IfaceCoercion
   | IfacePluginProv String
+  | IfaceCorePrepProv Bool  -- See defn of CorePrepProv
 
 {- Note [Holes in IfaceCoercion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -595,7 +596,8 @@ substIfaceType env ty
 
     go_prov (IfacePhantomProv co)    = IfacePhantomProv (go_co co)
     go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
-    go_prov (IfacePluginProv str)    = IfacePluginProv str
+    go_prov co@(IfacePluginProv _)   = co
+    go_prov co@(IfaceCorePrepProv _) = co
 
 substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
 substIfaceAppArgs env args
@@ -1744,6 +1746,8 @@ pprIfaceUnivCoProv (IfaceProofIrrelProv co)
   = text "irrel" <+> pprParendIfaceCoercion co
 pprIfaceUnivCoProv (IfacePluginProv s)
   = text "plugin" <+> doubleQuotes (text s)
+pprIfaceUnivCoProv (IfaceCorePrepProv _)
+  = text "CorePrep"
 
 -------------------
 instance Outputable IfaceTyCon where
@@ -2101,6 +2105,9 @@ 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
@@ -2111,6 +2118,8 @@ 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 b3644633af..a17679c89a 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -1418,6 +1418,7 @@ 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/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
index 7c56b12324..efaf909ef8 100644
--- a/compiler/GHC/Tc/TyCl/Utils.hs
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -153,7 +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_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 3819feb223..8070b4d513 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1534,7 +1534,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_prov dv (CorePrepProv _)    = return dv
 
     go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs
     go_cv dv@(DV { dv_cvs = cvs }) cv