current state of play

4 files changed, 10 insertions, 5 deletions

diff --git a/compiler/simplCore/CoreEraseCoercionProofs.hs b/compiler/simplCore/CoreEraseCoercionProofs.hs
index 1b053ec6ff..68cf85797c 100644
--- a/compiler/simplCore/CoreEraseCoercionProofs.hs
+++ b/compiler/simplCore/CoreEraseCoercionProofs.hs
@@ -42,8 +42,7 @@ coreExprEraseProof (Cast  e co ) =    Cast (coreExprEraseProof e) (forcedEraseCo
 coreExprEraseProof (Tick  tick e)= Tick tick (coreExprEraseProof e)
 coreExprEraseProof (Type  t) = Type t
 coreExprEraseProof (Coercion co )=  Coercion $! forcedEraseCoercion co
-  where
-    (Pair lty rty,role) = coercionKindRole co
+
 eraseAltPfs :: CoreAlt -> CoreAlt
 eraseAltPfs (con, vars, body) = (con,vars,coreExprEraseProof body)
 
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 7371036eec..0cd374641c 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -1292,11 +1292,13 @@ mkCoherenceRightCo r ty co co2
   | otherwise = co2 `mkTransCo` GRefl r ty (MCo co)
 
 -- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.
-mkKindCo :: Coercion -> Coercion
+mkKindCo :: HasCallStack =>Coercion -> Coercion
 mkKindCo co | Just (ty, _) <- isReflCo_maybe co = Refl (typeKind ty)
 mkKindCo (GRefl _ _ (MCo co)) = co
 mkKindCo (UnivCo (PhantomProv h) _ _ _)    = h
 mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
+mkKindCo (UnivCo ErasedProv _ t1 t2 )
+  = mkUnivCo ErasedProv Nominal  (typeKind t1) (typeKind t2)
 mkKindCo co
   | Pair ty1 ty2 <- coercionKind co
        -- generally, calling coercionKind during coercion creation is a bad idea,
@@ -1309,10 +1311,11 @@ mkKindCo co
   | otherwise
   = KindCo co
 
-mkSubCo :: Coercion -> Coercion
+mkSubCo :: HasCallStack =>Coercion -> Coercion
 -- Input coercion is Nominal, result is Representational
 -- see also Note [Role twiddling functions]
 mkSubCo (Refl ty) = GRefl Representational ty MRefl
+mkSubCo (UnivCo ErasedProv Nominal t1 t2) =mkUnivCo ErasedProv Representational t1 t2
 mkSubCo (GRefl Nominal ty co) = GRefl Representational ty co
 mkSubCo (TyConAppCo Nominal tc cos)
   = TyConAppCo Representational tc (applyRoles tc cos)
@@ -1519,6 +1522,7 @@ promoteCoercion co = case co of
     UnivCo (PhantomProv kco) _ _ _    -> kco
     UnivCo (ProofIrrelProv kco) _ _ _ -> kco
     UnivCo (PluginProv _) _ _ _       -> mkKindCo co
+    UnivCo ErasedProv _r t1 t2         -> mkUnivCo ErasedProv Nominal (typeKind t1) (typeKind t2)
 
     SymCo g
       -> mkSymCo (promoteCoercion g)
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index d43a7e27e3..5d9ccae46f 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -1491,6 +1491,7 @@ instance Outputable UnivCoProvenance where
   ppr (PhantomProv _)    = text "(phantom)"
   ppr (ProofIrrelProv _) = text "(proof irrel.)"
   ppr (PluginProv str)   = parens (text "plugin" <+> brackets (text str))
+  ppr (ErasedProv)       = text "Erased proof"
 
 -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
 data CoercionHole
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 2b9a3bcc53..bd6001f42f 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -651,7 +651,7 @@ mapCoercion :: Monad m
             => TyCoMapper env m -> env -> Coercion -> m Coercion
 mapCoercion mapper@(TyCoMapper { tcm_covar = covar
                                , tcm_hole = cohole
-                               , tcm_tyvar = tyvar
+                               -- , tcm_tyvar = tyvar
                                , tcm_tycobinder = tycobinder
                                , tcm_tycon = tycon })
             env co
@@ -696,6 +696,7 @@ mapCoercion mapper@(TyCoMapper { tcm_covar = covar
     go_prov (PhantomProv co)    = PhantomProv <$> go co
     go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
     go_prov p@(PluginProv _)    = return p
+    go_prov ErasedProv          = return ErasedProv
 
 {-
 ************************************************************************