fixing gaps in supporting coercion erasure

6 files changed, 16 insertions, 5 deletions

diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs
index fef3915c51..6e675ada8b 100644
--- a/compiler/coreSyn/CoreFVs.hs
+++ b/compiler/coreSyn/CoreFVs.hs
@@ -372,6 +372,7 @@ orphNamesOfMCo MRefl    = emptyNameSet
 orphNamesOfMCo (MCo co) = orphNamesOfCo co
 
 orphNamesOfCo :: Coercion -> NameSet
+orphNamesOfCo (ErasedCoercion)      = emptyNameSet
 orphNamesOfCo (Refl ty)             = orphNamesOfType ty
 orphNamesOfCo (GRefl _ ty mco)      = orphNamesOfType ty `unionNameSet` orphNamesOfMCo mco
 orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos
diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs
index 50fdcd9c7b..8ca94493e2 100644
--- a/compiler/coreSyn/CoreUtils.hs
+++ b/compiler/coreSyn/CoreUtils.hs
@@ -114,12 +114,14 @@ exprType :: CoreExpr -> Type
 -- really be said to have a type
 exprType (Var var)           = idType var
 exprType (Lit lit)           = literalType lit
+exprType (Coercion ErasedCoercion) = panic "exprType of ErasedCoercion"
 exprType (Coercion co)       = coercionType co
 exprType (Let bind body)
   | NonRec tv rhs <- bind    -- See Note [Type bindings]
   , Type ty <- rhs           = substTyWithUnchecked [tv] [ty] (exprType body)
   | otherwise                = exprType body
 exprType (Case _ _ ty _)     = ty
+exprType (Cast e ErasedCoercion)= exprType e -- this is representationally true
 exprType (Cast _ co)         = pSnd (coercionKind co)
 exprType (Tick _ e)          = exprType e
 exprType (Lam binder expr)   = mkLamType binder (exprType expr)
@@ -177,6 +179,7 @@ isExprLevPoly = go
    go_app (Lam _ e)       = go_app e
    go_app (Let _ e)       = go_app e
    go_app (Case _ _ ty _) = resultIsLevPoly ty
+   go_app (Cast e ErasedCoercion) = go_app e
    go_app (Cast _ co)     = resultIsLevPoly (coercionRKind co)
    go_app (Tick _ e)      = go_app e
    go_app e@(Type {})     = pprPanic "isExprLevPoly app ty" (ppr e)
@@ -259,6 +262,7 @@ applyTypeToArgs e op_ty args
 -- | Wrap the given expression in the coercion safely, dropping
 -- identity coercions and coalescing nested coercions
 mkCast :: CoreExpr -> CoercionR -> CoreExpr
+mkCast e ErasedCoercion = e
 mkCast e co
   | ASSERT2( coercionRole co == Representational
            , text "coercion" <+> ppr co <+> ptext (sLit "passed to mkCast")
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index d649be701b..e517a4f0a0 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -348,6 +348,7 @@ data IfaceCoercion
   | IfaceSubCo        IfaceCoercion
   | IfaceFreeCoVar    CoVar    -- See Note [Free tyvars in IfaceType]
   | IfaceHoleCo       CoVar    -- ^ See Note [Holes in IfaceCoercion]
+  | IfaceErased  --- coercions are erased
 
 data IfaceUnivCoProv
   = IfaceUnsafeCoerceProv
diff --git a/compiler/simplCore/CoreEraseCoercionProofs.hs b/compiler/simplCore/CoreEraseCoercionProofs.hs
index ca59949d4d..9fee14b29f 100644
--- a/compiler/simplCore/CoreEraseCoercionProofs.hs
+++ b/compiler/simplCore/CoreEraseCoercionProofs.hs
@@ -15,7 +15,7 @@ Top-level interface function, @eraseCoercionProgram@.
 
 eraseCoercionProgram :: ModGuts -> CoreM ModGuts
 eraseCoercionProgram pgm@(ModGuts { mg_binds = binds })
-  = do { dflags <- getDynFlags
+  = do { dflags <- getDynFlags ;
          return (pgm { mg_binds = map (coreProgramEraseCoercionProofs dflags) binds })
         }
 
@@ -28,8 +28,8 @@ coreProgramEraseCoercionProofs dflags topLevelBindings =
       else topLevelBindings
 
 coreExprEraseProof :: Expr b -> Expr b
-coreExprEraseProof e@(Var   Id) = e
-coreExprEraseProof e@(Lit   Literal) = e
+coreExprEraseProof e@(Var   _) = e
+coreExprEraseProof e@(Lit   _) = e
 coreExprEraseProof (App   f  e)  = App (coreExprEraseProof f) (coreExprEraseProof)
 coreExprEraseProof (Lam   v e) =  Lam v $ coreExprEraseProof e
 coreExprEraseProof (Let   binders bod) = Let (eraseBinders binder) (coreExprEraseProof bod)
diff --git a/compiler/simplCore/CoreMonad.hs b/compiler/simplCore/CoreMonad.hs
index 742ae39bf5..edf6044c26 100644
--- a/compiler/simplCore/CoreMonad.hs
+++ b/compiler/simplCore/CoreMonad.hs
@@ -145,6 +145,7 @@ instance Outputable CoreToDo where
   ppr CoreOccurAnal            = text "Occurrence analysis"
   ppr CoreDoPrintCore          = text "Print core"
   ppr (CoreDoRuleCheck {})     = text "Rule check"
+  ppr (CoreEraseCoercionEvidence) = text "Erase Coercion Proofs"
   ppr CoreDoNothing            = text "CoreDoNothing"
   ppr (CoreDoPasses passes)    = text "CoreDoPasses" <+> ppr passes
 
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index b338bfbf9e..cace39cd43 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -110,7 +110,7 @@ module Coercion (
 
         -- * Other
         promoteCoercion, buildCoercion,
-
+        ErasedCoercion,
         simplifyArgsWorker
        ) where
 
@@ -1435,7 +1435,7 @@ promoteCoercion co = case co of
 
     SubCo g
       -> promoteCoercion g
-
+    ErasedCoercion -> ErasedCoercion
   where
     Pair ty1 ty2 = coercionKind co
     ki1 = typeKind ty1
@@ -2123,6 +2123,7 @@ seqMCo MRefl    = ()
 seqMCo (MCo co) = seqCo co
 
 seqCo :: Coercion -> ()
+seqCo (ErasedCoercion) = ()
 seqCo (Refl ty)                 = seqType ty
 seqCo (GRefl r ty mco)          = r `seq` seqType ty `seq` seqMCo mco
 seqCo (TyConAppCo r tc cos)     = r `seq` tc `seq` seqCos cos
@@ -2188,6 +2189,7 @@ coercionLKind :: Coercion -> Type
 coercionLKind co
   = go co
   where
+    go (ErasedCoercion)   = panic "erased coercions have no type, dont lint em"
     go (Refl ty)                = ty
     go (GRefl _ ty _)           = ty
     go (TyConAppCo _ tc cos)    = mkTyConApp tc (map go cos)
@@ -2243,6 +2245,7 @@ coercionRKind :: Coercion -> Type
 coercionRKind co
   = go co
   where
+    go (ErasedCoercion)= panic  "no kind for erased coercions "
     go (Refl ty)                = ty
     go (GRefl _ ty MRefl)       = ty
     go (GRefl _ ty (MCo co1))   = mkCastTy ty co1
@@ -2366,6 +2369,7 @@ coercionRole = go
     go (KindCo {}) = Nominal
     go (SubCo _) = Representational
     go (AxiomRuleCo ax _) = coaxrRole ax
+    go (ErasedCoercion) = panic "coercionRole is not defined for ErasedCoercion"
 
 {-
 Note [Nested InstCos]