Get rid of EvCoercible

and use EvCoercion to describe the evidence for Coercible instances.

6 files changed, 48 insertions, 114 deletions

diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index 85b1cc6e4d..54744bc342 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -49,11 +49,10 @@ import TcEvidence
 import TcType
 import Type
 import Coercion hiding (substCo)
-import TysWiredIn ( eqBoxDataCon, coercibleTyCon, coercibleDataCon, tupleCon )
+import TysWiredIn ( eqBoxDataCon, coercibleDataCon, tupleCon )
 import Id
 import Class
 import DataCon	( dataConWorkId )
-import FamInstEnv ( instNewTyConTF_maybe )
 import Name
 import MkId	( seqId )
 import Var
@@ -786,48 +785,6 @@ dsEvTerm (EvLit l) =
     EvNum n -> mkIntegerExpr n
     EvStr s -> mkStringExprFS s
 
--- Note [Coercible Instances]
-dsEvTerm (EvCoercible (EvCoercibleRefl ty)) = do
-  return $ mkEqBox $ mkReflCo Representational ty
-
-dsEvTerm (EvCoercible (EvCoercibleTyCon tyCon evs)) = do
-  ntEvs <- mapM (mapEvCoercibleArgM dsEvTerm) evs
-  wrapInEqRCases ntEvs $ \cos -> do
-    return $ mkEqBox $
-      mkTyConAppCo Representational tyCon cos
-
-dsEvTerm (EvCoercible (EvCoercibleNewType lor tyCon tys v)) = do
-  ntEv <- dsEvTerm v
-  famenv <- dsGetFamInstEnvs
-  let Just (_, ntCo) = instNewTyConTF_maybe famenv tyCon tys
-  wrapInEqRCase ntEv $ \co -> do
-          return $ mkEqBox $ connect lor co ntCo
-  where connect CLeft co2 co1 = mkTransCo co1 co2
-        connect CRight co2 co1 = mkTransCo co2 (mkSymCo co1)
-
-wrapInEqRCase :: CoreExpr -> (Coercion -> DsM CoreExpr) -> DsM CoreExpr
-wrapInEqRCase e mkBody = do
-  cov <- newSysLocalDs (mkCoercionType Representational ty1 ty2)
-  body' <- mkBody (mkCoVarCo cov)
-  return $
-        ASSERT(tc == coercibleTyCon)
-        mkWildCase
-                e
-                (exprType e)
-                (exprType body')
-                [(DataAlt coercibleDataCon, [cov], body')]
-  where
-  Just (tc, [_k, ty1, ty2]) = splitTyConApp_maybe (exprType e)
-
-wrapInEqRCases :: [EvCoercibleArg CoreExpr] -> ([Coercion] -> DsM CoreExpr) -> DsM CoreExpr
-wrapInEqRCases (EvCoercibleArgN t:es) mkBody =
-  wrapInEqRCases es (\cos -> mkBody (mkReflCo Nominal t:cos))
-wrapInEqRCases (EvCoercibleArgR e:es) mkBody = wrapInEqRCase e $ \co ->
-  wrapInEqRCases es (\cos -> mkBody (co:cos))
-wrapInEqRCases (EvCoercibleArgP t1 t2:es) mkBody =
-  wrapInEqRCases es (\cos -> mkBody (mkUnivCo Phantom t1 t2:cos))
-wrapInEqRCases [] mkBody = mkBody []
-
 ---------------------------------------
 dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
 -- This is the crucial function that moves 
diff --git a/compiler/prelude/TysWiredIn.lhs-boot b/compiler/prelude/TysWiredIn.lhs-boot
index b6dab8a21b..305d82e2b5 100644
--- a/compiler/prelude/TysWiredIn.lhs-boot
+++ b/compiler/prelude/TysWiredIn.lhs-boot
@@ -5,7 +5,7 @@ import {-# SOURCE #-} TyCon      (TyCon)
 import {-# SOURCE #-} TypeRep    (Type)
 
 
-eqTyCon :: TyCon
+eqTyCon, coercibleTyCon :: TyCon
 typeNatKind, typeSymbolKind :: Type
 mkBoxedTupleTy :: [Type] -> Type
 \end{code}
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index ea0c3b59d7..a0df74b75a 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -16,7 +16,6 @@ module TcEvidence (
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, 
   EvTerm(..), mkEvCast, evVarsOfTerm, 
   EvLit(..), evTermCoercion,
-  EvCoercible(..), EvCoercibleArg(..), mapEvCoercibleArgM,
 
   -- TcCoercion
   TcCoercion(..), LeftOrRight(..), pickLR,
@@ -26,13 +25,15 @@ module TcEvidence (
   mkTcAxiomRuleCo,
   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, 
   isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
-  tcCoercionRole, eqVarRole
+  tcCoercionRole, eqVarRole,
+  coercionToTcCoercion
 
   ) where
 #include "HsVersions.h"
 
 import Var
 import Coercion( LeftOrRight(..), pickLR, nthRole )
+import qualified Coercion as C
 import PprCore ()   -- Instance OutputableBndr TyVar
 import TypeRep  -- Knows type representation
 import TcType
@@ -427,6 +428,23 @@ ppr_forall_co p ty
     split1 tvs ty                 = (reverse tvs, ty)
 \end{code}
 
+Conversion from Coercion to TcCoercion
+(at the moment, this is only needed to convert the result of
+instNewTyConTF_maybe, so all unused cases are panics for now).
+
+\begin{code}
+coercionToTcCoercion :: C.Coercion -> TcCoercion
+coercionToTcCoercion = go
+  where
+    go (C.Refl r t)                = TcRefl r t
+    go (C.TransCo c1 c2)           = TcTransCo (go c1) (go c2)
+    go (C.AxiomInstCo coa ind cos) = TcAxiomInstCo coa ind (map go cos)
+    go (C.SubCo c)                 = TcSubCo (go c)
+    go (C.AppCo c1 c2)             = TcAppCo (go c1) (go c2)
+    go co                          = pprPanic "coercionToTcCoercion" (ppr co)
+\end{code}
+
+
 %************************************************************************
 %*                                                                      *
                   HsWrapper
@@ -584,9 +602,6 @@ data EvTerm
   | EvLit EvLit       -- Dictionary for KnownNat and KnownLit classes.
                       -- Note [KnownNat & KnownSymbol and EvLit]
 
-  | EvCoercible EvCoercible      -- Dictionary for "Coercible a b"
-                                 -- Note [Coercible Instances] in TcInteract
-
   deriving( Data.Data, Data.Typeable)
 
 
@@ -594,23 +609,6 @@ data EvLit
   = EvNum Integer
   | EvStr FastString
     deriving( Data.Data, Data.Typeable)
-
-data EvCoercible
-  = EvCoercibleRefl Type
-  | EvCoercibleTyCon TyCon [EvCoercibleArg EvTerm]
-  | EvCoercibleNewType LeftOrRight TyCon [Type] EvTerm
-    deriving( Data.Data, Data.Typeable)
-
-data EvCoercibleArg a
-  = EvCoercibleArgN Type
-  | EvCoercibleArgR a
-  | EvCoercibleArgP Type Type
-    deriving( Data.Data, Data.Typeable)
-
-mapEvCoercibleArgM :: Monad m => (a -> m b) -> EvCoercibleArg a -> m (EvCoercibleArg b)
-mapEvCoercibleArgM _ (EvCoercibleArgN t)     = return (EvCoercibleArgN t)
-mapEvCoercibleArgM f (EvCoercibleArgR v)     = do { v' <- f v; return (EvCoercibleArgR v') }
-mapEvCoercibleArgM _ (EvCoercibleArgP t1 t2) = return (EvCoercibleArgP t1 t2)
 \end{code}
 
 Note [Coercion evidence terms]
@@ -741,12 +739,6 @@ evVarsOfTerm (EvCast tm co)       = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo c
 evVarsOfTerm (EvTupleMk evs)      = evVarsOfTerms evs
 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
 evVarsOfTerm (EvLit _)            = emptyVarSet
-evVarsOfTerm (EvCoercible evnt)   = evVarsOfEvCoercible evnt
-
-evVarsOfEvCoercible :: EvCoercible -> VarSet
-evVarsOfEvCoercible (EvCoercibleRefl _)          = emptyVarSet
-evVarsOfEvCoercible (EvCoercibleTyCon _ evs)     = evVarsOfTerms [v | EvCoercibleArgR v <- evs ]
-evVarsOfEvCoercible (EvCoercibleNewType _ _ _ v) = evVarsOfTerm v
 
 evVarsOfTerms :: [EvTerm] -> VarSet
 evVarsOfTerms = foldr (unionVarSet . evVarsOfTerm) emptyVarSet 
@@ -809,23 +801,11 @@ instance Outputable EvTerm where
   ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
   ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
   ppr (EvLit l)          = ppr l
-  ppr (EvCoercible co)   = ptext (sLit "Coercible") <+> ppr co
   ppr (EvDelayedError ty msg) =     ptext (sLit "error") 
                                 <+> sep [ char '@' <> ppr ty, ppr msg ]
 
 instance Outputable EvLit where
   ppr (EvNum n) = integer n
   ppr (EvStr s) = text (show s)
-
-instance Outputable EvCoercible where
-  ppr (EvCoercibleRefl ty) = ppr ty
-  ppr (EvCoercibleTyCon tyCon evs) = ppr tyCon <+> hsep (map ppr evs)
-  ppr (EvCoercibleNewType CLeft tyCon tys v) = ppr (tyCon `mkTyConApp` tys) <+> char ';' <+> ppr v
-  ppr (EvCoercibleNewType CRight tyCon tys v) =ppr v <+> char ';' <+> ppr (tyCon `mkTyConApp` tys)
-
-instance Outputable a => Outputable (EvCoercibleArg a) where
-  ppr (EvCoercibleArgN t)     = ptext (sLit "N:") <+> ppr t
-  ppr (EvCoercibleArgR v)     = ptext (sLit "R:") <+> ppr v
-  ppr (EvCoercibleArgP t1 t2) = ptext (sLit "P:") <+> parens (ppr (t1,t2))
 \end{code}
 
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 1470e931c0..7d973a44bb 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -1181,9 +1181,6 @@ zonkEvTerm env (EvTupleSel tm n)  = do { tm' <- zonkEvTerm env tm
 zonkEvTerm env (EvTupleMk tms)    = do { tms' <- mapM (zonkEvTerm env) tms
                                        ; return (EvTupleMk tms') }
 zonkEvTerm _   (EvLit l)          = return (EvLit l)
-zonkEvTerm env (EvCoercible evnt) = do { evnt' <- zonkEvCoercible env evnt
-                                       ; return (EvCoercible evnt')
-                                       }
 zonkEvTerm env (EvSuperClass d n) = do { d' <- zonkEvTerm env d
                                        ; return (EvSuperClass d' n) }
 zonkEvTerm env (EvDFunApp df tys tms)
@@ -1194,16 +1191,6 @@ zonkEvTerm env (EvDelayedError ty msg)
   = do { ty' <- zonkTcTypeToType env ty
        ; return (EvDelayedError ty' msg) }
 
-
-zonkEvCoercible :: ZonkEnv -> EvCoercible -> TcM EvCoercible
-zonkEvCoercible _   (EvCoercibleRefl ty) = return (EvCoercibleRefl ty)
-zonkEvCoercible env (EvCoercibleTyCon tyCon evs) = do
-        evs' <- mapM (mapEvCoercibleArgM (zonkEvTerm env)) evs
-        return (EvCoercibleTyCon tyCon evs')
-zonkEvCoercible env (EvCoercibleNewType l tyCon tys v) = do
-        v' <- zonkEvTerm env v
-        return (EvCoercibleNewType l tyCon tys v')
-
 zonkTcEvBinds :: ZonkEnv -> TcEvBinds -> TcM (ZonkEnv, TcEvBinds)
 zonkTcEvBinds env (TcEvBinds var) = do { (env', bs') <- zonkEvBindsVar env var
                                        ; return (env', EvBinds bs') }
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 854c27edb7..099339765d 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -1957,8 +1957,7 @@ getCoercibleInst safeMode famenv rdr_env loc ty1 ty2
                           )
                    Representational -> do
                         ct_ev <- requestCoercible loc ta1 ta2
-                        local_var <- mkSysLocalM (fsLit "coev") $
-                                coercibleClass `mkClassPred` [typeKind ta1, ta1, ta2]
+                        local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred ta1 ta2
                         return
                           ( freshGoal ct_ev
                           , Just (EvBind local_var (getEvTerm ct_ev))
@@ -1970,27 +1969,31 @@ getCoercibleInst safeMode famenv rdr_env loc ty1 ty2
                           , Nothing
                           , TcPhantomCo ta1 ta2)
        let (arg_new, arg_binds, arg_cos) = unzip3 arg_stuff
-       let binds = EvBinds (listToBag (catMaybes arg_binds))
-       let tcCo = TcLetCo binds (mkTcTyConAppCo Representational tc1 arg_cos)
-
-       return $ GenInst (catMaybes arg_new)
-              $ EvCoercion tcCo
+           binds = EvBinds (listToBag (catMaybes arg_binds))
+           tcCo = TcLetCo binds (mkTcTyConAppCo Representational tc1 arg_cos)
+       return $ GenInst (catMaybes arg_new) (EvCoercion tcCo)
 
   | Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
-    Just (concTy, _) <- instNewTyConTF_maybe famenv tc tyArgs,
+    Just (concTy, ntCo) <- instNewTyConTF_maybe famenv tc tyArgs,
     dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
   = do markDataConsAsUsed rdr_env tc
        ct_ev <- requestCoercible loc concTy ty2
-       return $ GenInst (freshGoals [ct_ev])
-              $ EvCoercible (EvCoercibleNewType CLeft tc tyArgs (getEvTerm ct_ev))
+       local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred concTy ty2
+       let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev)))
+           tcCo = TcLetCo binds $
+                          coercionToTcCoercion ntCo `mkTcTransCo` mkTcCoVarCo local_var
+       return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo)
 
   | Just (tc,tyArgs) <- splitTyConApp_maybe ty2,
-    Just (concTy, _) <- instNewTyConTF_maybe famenv tc tyArgs,
+    Just (concTy, ntCo) <- instNewTyConTF_maybe famenv tc tyArgs,
     dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
   = do markDataConsAsUsed rdr_env tc
        ct_ev <- requestCoercible loc ty1 concTy
-       return $ GenInst (freshGoals [ct_ev])
-              $ EvCoercible (EvCoercibleNewType CRight tc tyArgs (getEvTerm ct_ev))
+       local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred ty1 concTy
+       let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev)))
+           tcCo = TcLetCo binds $
+                          mkTcCoVarCo local_var `mkTcTransCo` mkTcSymCo (coercionToTcCoercion ntCo)
+       return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo)
 
   | otherwise
   = return NoInstance
@@ -2020,7 +2023,7 @@ markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
 requestCoercible :: CtLoc -> TcType -> TcType -> TcS MaybeNew
 requestCoercible loc ty1 ty2 =
     ASSERT2( typeKind ty1 `tcEqKind` typeKind ty2, ppr ty1 <+> ppr ty2)
-    newWantedEvVarNonrec loc' (coercibleClass `mkClassPred` [typeKind ty1, ty1, ty2])
+    newWantedEvVarNonrec loc' (mkCoerciblePred ty1 ty2)
   where loc' = bumpCtLocDepth CountConstraints loc
 
 \end{code}
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index d45cd8c6ef..0abe463f18 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -48,7 +48,7 @@ module Type (
         -- Pred types
         mkFamilyTyConApp,
         isDictLikeTy,
-        mkEqPred, mkPrimEqPred, mkReprPrimEqPred,
+        mkEqPred, mkCoerciblePred, mkPrimEqPred, mkReprPrimEqPred,
         mkClassPred,
         noParenPred, isClassPred, isEqPred,
         isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
@@ -160,7 +160,7 @@ import NameEnv
 import Class
 import TyCon
 import TysPrim
-import {-# SOURCE #-} TysWiredIn ( eqTyCon, typeNatKind, typeSymbolKind )
+import {-# SOURCE #-} TysWiredIn ( eqTyCon, coercibleTyCon, typeNatKind, typeSymbolKind )
 import PrelNames ( eqTyConKey, coercibleTyConKey,
                    ipClassNameKey, openTypeKindTyConKey,
                    constraintKindTyConKey, liftedTypeKindTyConKey )
@@ -899,6 +899,13 @@ mkEqPred ty1 ty2
   where
     k = typeKind ty1
 
+mkCoerciblePred :: Type -> Type -> PredType
+mkCoerciblePred ty1 ty2
+  = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 $$ ppr k $$ ppr (typeKind ty2) )
+    TyConApp coercibleTyCon [k, ty1, ty2]
+  where
+    k = typeKind ty1
+
 mkPrimEqPred :: Type -> Type -> Type
 mkPrimEqPred ty1  ty2
   = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 )