fixed the approach to erasure proof to have the from / to targets, still need to update the erasure code in core

15 files changed, 54 insertions, 29 deletions

diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs
index a8012c1df7..3da30de6ad 100644
--- a/compiler/backpack/RnModIface.hs
+++ b/compiler/backpack/RnModIface.hs
@@ -702,7 +702,8 @@ rnIfaceCo (IfaceSubCo c) = IfaceSubCo <$> rnIfaceCo c
 rnIfaceCo (IfaceAxiomRuleCo ax cos)
     = IfaceAxiomRuleCo ax <$> mapM rnIfaceCo cos
 rnIfaceCo (IfaceKindCo c) = IfaceKindCo <$> rnIfaceCo c
-rnIfaceCo (IfaceErased) = return IfaceErased
+rnIfaceCo (IfaceErased role lty rty)
+    = IfaceErased role <$>  rnIfaceType lty <*> rnIfaceType rty
 
 rnIfaceTyCon :: Rename IfaceTyCon
 rnIfaceTyCon (IfaceTyCon n info)
diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs
index 6e675ada8b..daeeaf4b66 100644
--- a/compiler/coreSyn/CoreFVs.hs
+++ b/compiler/coreSyn/CoreFVs.hs
@@ -372,7 +372,7 @@ orphNamesOfMCo MRefl    = emptyNameSet
 orphNamesOfMCo (MCo co) = orphNamesOfCo co
 
 orphNamesOfCo :: Coercion -> NameSet
-orphNamesOfCo (ErasedCoercion)      = emptyNameSet
+orphNamesOfCo (ErasedCoercion _r lty rty )      = orphNamesOfType lty `unionNameSet` rty
 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/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 10dc129444..167bf1a7b8 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -301,8 +301,8 @@ coreDumpFlag CoreDesugarOpt           = Just Opt_D_dump_ds
 coreDumpFlag CoreTidy                 = Just Opt_D_dump_simpl
 coreDumpFlag CorePrep                 = Just Opt_D_dump_prep
 coreDumpFlag CoreOccurAnal            = Just Opt_D_dump_occur_anal
-coreDumpFlag CoreEraseCoercionEvidence =
-    panic "imposible to lint core with erased coercions,rebuild libraries with core linting enabled"
+coreDumpFlag CoreEraseCoercionEvidence =  --- improve this with flags
+    panic "bad idea to lint with erased coercions,rebuild libraries with core linting enabled"
 
 coreDumpFlag CoreDoPrintCore          = Nothing
 coreDumpFlag (CoreDoRuleCheck {})     = Nothing
@@ -1689,7 +1689,11 @@ lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, Linted
 
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
-lintCoercion ErasedCoercion = panic "core linting requires core lint on your dependencies"
+lintCoercion (ErasedCoercion role lty rty)
+  = do { kl <- lintType lty ;
+         kr <- lintType rty
+         return (kl,kr,lty,rty,role)
+       }
 lintCoercion (Refl ty)
   = do { k <- lintType ty
        ; return (k, k, ty, ty, Nominal) }
diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs
index 61a824ebbf..7603eeea30 100644
--- a/compiler/coreSyn/CoreUtils.hs
+++ b/compiler/coreSyn/CoreUtils.hs
@@ -114,14 +114,12 @@ 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)
@@ -179,7 +177,6 @@ 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)
@@ -262,7 +259,6 @@ 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/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 1bdba6e892..02050868aa 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -1578,7 +1578,8 @@ freeNamesIfMCoercion IfaceMRefl    = emptyNameSet
 freeNamesIfMCoercion (IfaceMCo co) = freeNamesIfCoercion co
 
 freeNamesIfCoercion :: IfaceCoercion -> NameSet
-freeNamesIfCoercion IfaceErased = emptyNameSet
+freeNamesIfCoercion (IfaceErased _role ltyp rtyp)
+  = freeNamesIfType ltyp && freeNamesIfType rtyp
 freeNamesIfCoercion (IfaceReflCo t) = freeNamesIfType t
 freeNamesIfCoercion (IfaceGReflCo _ t mco)
   = freeNamesIfType t &&& freeNamesIfMCoercion mco
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 45ed09431b..a92cdf4d4a 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -348,7 +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
+  | IfaceErased       Role IFaceType IfaceType --- coercions are erased
 
 data IfaceUnivCoProv
   = IfaceUnsafeCoerceProv
@@ -523,7 +523,7 @@ substIfaceType env ty
     go_co (IfaceKindCo co)           = IfaceKindCo (go_co co)
     go_co (IfaceSubCo co)            = IfaceSubCo (go_co co)
     go_co (IfaceAxiomRuleCo n cos)   = IfaceAxiomRuleCo n (go_cos cos)
-    go_co (IfaceErased) = IfaceErased
+    go_co (IfaceErased role lty rty) = IfaceErased role (go_co lty rty)
     go_cos = map go_co
 
     go_prov IfaceUnsafeCoerceProv    = IfaceUnsafeCoerceProv
@@ -1596,7 +1596,10 @@ ppr_co ctxt_prec (IfaceSubCo co)
   = ppr_special_co ctxt_prec (text "Sub") [co]
 ppr_co ctxt_prec (IfaceKindCo co)
   = ppr_special_co ctxt_prec (text "Kind") [co]
-ppr_co ctxt_prec (IfaceErased) = text "ErasedCoercion"
+ppr_co ctxt_prec (IfaceErased role lty rtyp)
+  = maybeParen ctxt_prec appPrec $
+    text "ErasedCoercion" <+> ppr role <+>
+    pprParendIfaceType lty <+> pprParendIfaceType rty
 ppr_special_co :: PprPrec -> SDoc -> [IfaceCoercion] -> SDoc
 ppr_special_co ctxt_prec doc cos
   = maybeParen ctxt_prec appPrec
@@ -1890,8 +1893,11 @@ instance Binary IfaceCoercion where
           putByte bh 17
           put_ bh a
           put_ bh b
-  put_ bh (IfaceErased) = do
+  put_ bh (IfaceErased r lty rty) = do
           putByte bh 18
+          putByte bh r
+          putByte bh lty
+          putByte bh rty
   put_ _ (IfaceFreeCoVar cv)
        = pprPanic "Can't serialise IfaceFreeCoVar" (ppr cv)
   put_ _  (IfaceHoleCo cv)
@@ -1955,7 +1961,10 @@ instance Binary IfaceCoercion where
                    b <- get bh
                    return $ IfaceAxiomRuleCo a b
            18 -> do
-                  return $ IfaceErased
+                  role <- get bh
+                  lty  <- get bh
+                  rty  <- get bh
+                  return $ IfaceErased r lty rty
            _ -> panic ("get IfaceCoercion " ++ show tag)
 
 instance Binary IfaceUnivCoProv where
@@ -2031,7 +2040,7 @@ instance NFData IfaceCoercion where
     IfaceSubCo f1 -> rnf f1
     IfaceFreeCoVar f1 -> f1 `seq` ()
     IfaceHoleCo f1 -> f1 `seq` ()
-    IfaceErased -> ()
+    IfaceErased rl lty rty-> rnf r `seq`  rn lty `seq` rnf rty
 
 instance NFData IfaceUnivCoProv where
   rnf x = seq x ()
diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs
index 17800b877d..62b091c0af 100644
--- a/compiler/iface/ToIface.hs
+++ b/compiler/iface/ToIface.hs
@@ -265,7 +265,7 @@ toIfaceCoercionX fr co
     go_mco MRefl     = IfaceMRefl
     go_mco (MCo co)  = IfaceMCo $ go co
 
-    go (ErasedCoercion)     = IfaceErased
+    go (ErasedCoercion r lty rty)     = IfaceErased r lty rty
     go (Refl ty)            = IfaceReflCo (toIfaceTypeX fr ty)
     go (GRefl r ty mco)     = IfaceGReflCo r (toIfaceTypeX fr ty) (go_mco mco)
     go (CoVarCo cv)
diff --git a/compiler/simplCore/CoreEraseCoercionProofs.hs b/compiler/simplCore/CoreEraseCoercionProofs.hs
index 508666e160..bbc4d3b183 100644
--- a/compiler/simplCore/CoreEraseCoercionProofs.hs
+++ b/compiler/simplCore/CoreEraseCoercionProofs.hs
@@ -35,7 +35,8 @@ coreExprEraseProof (Lam   v e) =  Lam v $ coreExprEraseProof e
 coreExprEraseProof (Let   binder bod) = Let (eraseBinders binder) (coreExprEraseProof bod)
 coreExprEraseProof (Case  scrut v ty alts  )=
     Case (coreExprEraseProof scrut) v ty (map eraseAltPfs alts)
-coreExprEraseProof (Cast  e _) = Cast (coreExprEraseProof e) ErasedCoercion
+coreExprEraseProof (Cast  e co ) = Cast (coreExprEraseProof e) (ErasedCoercion role lty rty )
+  where
 coreExprEraseProof (Tick  tick e)= Tick tick (coreExprEraseProof e)
 coreExprEraseProof (Type  t) = Type t
 coreExprEraseProof (Coercion _)= Coercion ErasedCoercion
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 0ac553c0ea..4cf5db3e04 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -1356,6 +1356,10 @@ collect_cand_qtvs_co :: VarSet -- bound variables
                      -> TcM CandidatesQTvs
 collect_cand_qtvs_co bound = go_co
   where
+
+    go_co dv (ErasedCoercion _role lty rty ) = do
+                                    dv1 <-collect_cand_qtvs True bound dv lty
+                                    collect_cand_qtvs True bound dv1 rty
     go_co dv (Refl ty)             = collect_cand_qtvs True bound dv ty
     go_co dv (GRefl _ ty mco)      = do dv1 <- collect_cand_qtvs True bound dv ty
                                         go_mco dv1 mco
diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index 04dbed0776..a09140d862 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -117,7 +117,7 @@ synonymTyConsOfType ty
      go_mco MRefl    = emptyNameEnv
      go_mco (MCo co) = go_co co
 
-     go_co (ErasedCoercion) = emptyNameEnv
+     go_co (ErasedCoercion r lty rty ) = go lty `plusNameEnv` go rty
      go_co (Refl ty)              = go ty
      go_co (GRefl _ ty mco)       = go ty `plusNameEnv` go_mco mco
      go_co (TyConAppCo _ tc cs)   = go_tc tc `plusNameEnv` go_co_s cs
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 4b0e228e02..45445c55f0 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -1435,7 +1435,8 @@ promoteCoercion co = case co of
 
     SubCo g
       -> promoteCoercion g
-    ErasedCoercion -> ErasedCoercion
+
+    ErasedCoercion r lty rty -> ErasedCoercion r ty1 ty2
   where
     Pair ty1 ty2 = coercionKind co
     ki1 = typeKind ty1
@@ -2123,7 +2124,7 @@ seqMCo MRefl    = ()
 seqMCo (MCo co) = seqCo co
 
 seqCo :: Coercion -> ()
-seqCo (ErasedCoercion) = ()
+seqCo (ErasedCoercion r lt rt) = r `seq` seqType lt `seq` seqType rt
 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
@@ -2189,7 +2190,7 @@ coercionLKind :: Coercion -> Type
 coercionLKind co
   = go co
   where
-    go (ErasedCoercion)   = panic "erased coercions have no type, dont lint em"
+    go (ErasedCoercion _role ltyp _rtyp)   = ltype
     go (Refl ty)                = ty
     go (GRefl _ ty _)           = ty
     go (TyConAppCo _ tc cos)    = mkTyConApp tc (map go cos)
@@ -2244,8 +2245,7 @@ go_nth d ty
 coercionRKind :: Coercion -> Type
 coercionRKind co
   = go co
-  where
-    go (ErasedCoercion)= panic  "no kind for erased coercions "
+    go (ErasedCoercion _role _ltyp rtype)   = k
     go (Refl ty)                = ty
     go (GRefl _ ty MRefl)       = ty
     go (GRefl _ ty (MCo co1))   = mkCastTy ty co1
@@ -2351,6 +2351,7 @@ change reduces /total/ compile time by a factor of more than ten.
 coercionRole :: Coercion -> Role
 coercionRole = go
   where
+    go (ErasedCoercion r _ _) = r
     go (Refl _) = Nominal
     go (GRefl r _ _) = r
     go (TyConAppCo r _ _) = r
@@ -2369,7 +2370,7 @@ coercionRole = go
     go (KindCo {}) = Nominal
     go (SubCo _) = Representational
     go (AxiomRuleCo ax _) = coaxrRole ax
-    go (ErasedCoercion) = panic "coercionRole is not defined for ErasedCoercion"
+    go (ErasedCoercion r _ _) = r
 
 {-
 Note [Nested InstCos]
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 3e31457766..ca83a297fc 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -191,7 +191,7 @@ opt_co4_wrap env sym rep r co
     pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
     result
 -}
-opt_co4 _lc _sym _rp _role ErasedCoercion = ErasedCoercion
+opt_co4 _lc _sym _rp _role e@(ErasedCoercion) = e
 opt_co4 env _   rep r (Refl ty)
   = ASSERT2( r == Nominal, text "Expected role:" <+> ppr r    $$
                            text "Found role:" <+> ppr Nominal $$
diff --git a/compiler/types/TyCoFVs.hs b/compiler/types/TyCoFVs.hs
index d9453defd2..442b37c5fd 100644
--- a/compiler/types/TyCoFVs.hs
+++ b/compiler/types/TyCoFVs.hs
@@ -207,8 +207,10 @@ tyCoVarsOfCos cos = ty_co_vars_of_cos cos emptyVarSet emptyVarSet
 
 
 ty_co_vars_of_co :: Coercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
+ty_co_vars_of_co (ErasedCoercion _r lty rty) is acc =  ty_co_vars_of_type rty is $
+                                                       ty_co_vars_of_type lty is acc
 ty_co_vars_of_co (Refl ty)            is acc = ty_co_vars_of_type ty is acc
-ty_co_vars_of_co (GRefl _ ty mco)     is acc = ty_co_vars_of_type ty is $
+ty_co_vars_of_co (GRefl _ ty mco)     is acc = ty_co_vars_of_type ty is acc $
                                                ty_co_vars_of_mco mco is acc
 ty_co_vars_of_co (TyConAppCo _ _ cos) is acc = ty_co_vars_of_cos cos is acc
 ty_co_vars_of_co (AppCo co arg)       is acc = ty_co_vars_of_co co is $
@@ -341,6 +343,7 @@ exactTyCoVarsOfType ty
     goMCo MRefl    = emptyVarSet
     goMCo (MCo co) = goCo co
 
+    goCo (ErasedCoercion _ lty rty ) = go lty `unionVarSet` go rty
     goCo (Refl ty)            = go ty
     goCo (GRefl _ ty mco)     = go ty `unionVarSet` goMCo mco
     goCo (TyConAppCo _ _ args)= goCos args
@@ -437,7 +440,8 @@ tyCoVarsOfCosSet cos = tyCoVarsOfCos $ nonDetEltsUFM cos
 tyCoFVsOfCo :: Coercion -> FV
 -- Extracts type and coercion variables from a coercion
 -- See Note [Free variables of types]
-tyCoFVsOfCo (ErasedCoercion) _ _ _ = emptyFV
+tyCoFVsOfCo (ErasedCoercion _ lty rty) fv_cand in_scope acc
+  = (tyCoFVsOfType lty `unionFV` tyCoFVsOfType rty) fv_cand in_scope acc
 tyCoFVsOfCo (Refl ty) fv_cand in_scope acc
   = tyCoFVsOfType ty fv_cand in_scope acc
 tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc
@@ -527,6 +531,7 @@ almostDevoidCoVarOfCo cv co =
   almost_devoid_co_var_of_co co cv
 
 almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
+almost_devoid_co_var_of_co (ErasedCoercion _ _ _)  _ =  True
 almost_devoid_co_var_of_co (Refl {}) _ = True   -- covar is allowed in Refl and
 almost_devoid_co_var_of_co (GRefl {}) _ = True  -- GRefl, so we don't look into
                                                 -- the coercions
@@ -730,6 +735,8 @@ noFreeVarsOfTypes = all noFreeVarsOfType
 -- | Returns True if this coercion has no free variables. Should be the same as
 -- isEmptyVarSet . tyCoVarsOfCo, but faster in the non-forall case.
 noFreeVarsOfCo :: Coercion -> Bool
+noFreeVarsOfCo (ErasedCoercion r lty rty)=  noFreeVarsOfType lty &&
+                                            noFreeVarsOfType rty
 noFreeVarsOfCo (Refl ty)              = noFreeVarsOfType ty
 noFreeVarsOfCo (GRefl _ ty co)        = noFreeVarsOfType ty && noFreeVarsOfMCo co
 noFreeVarsOfCo (TyConAppCo _ _ args)  = all noFreeVarsOfCo args
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 926b066260..d5c7b647ea 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -1674,7 +1674,7 @@ coercionSize (ForAllCo _ h co)   = 1 + coercionSize co + coercionSize h
 coercionSize (FunCo _ co1 co2)   = 1 + coercionSize co1 + coercionSize co2
 coercionSize (CoVarCo _)         = 1
 coercionSize (HoleCo _)          = 1
-coercionSize ErasedCoercion      = 1
+coercionSize (ErasedCoercion _ lty rty  )=   1 + typeSize lty + typeSize rty
 coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args)
 coercionSize (UnivCo p _ t1 t2)  = 1 + provSize p + typeSize t1 + typeSize t2
 coercionSize (SymCo co)          = 1 + coercionSize co
diff --git a/compiler/types/TyCoSubst.hs b/compiler/types/TyCoSubst.hs
index db7563914f..8d37d1c24f 100644
--- a/compiler/types/TyCoSubst.hs
+++ b/compiler/types/TyCoSubst.hs
@@ -791,6 +791,7 @@ subst_co subst co
     go_mco (MCo co) = MCo (go co)
 
     go :: Coercion -> Coercion
+    go (ErasedCoercion r lty rty ) = ErasedCoercion  r $! (go_ty lty) $! (go_ty rty)
     go (Refl ty)             = mkNomReflCo $! (go_ty ty)
     go (GRefl r ty mco)      = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco)
     go (TyConAppCo r tc args)= let args' = map go args