Remove IsCoercion

5 files changed, 40 insertions, 60 deletions

diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index c6335a95c6..f328ce9014 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -967,6 +967,7 @@ ds_tc_coercion subst tc_co
     go (TcCastCo co1 co2)       = mkCoCast (go co1) (go co2)
     go (TcCoVarCo v)            = ds_ev_id subst v
     go (TcAxiomRuleCo co ts cs) = AxiomRuleCo co (map (Coercion.substTy subst) ts) (map go cs)
+    go (TcCoercion co)          = co
 
     ds_co_binds :: TcEvBinds -> CvSubst
     ds_co_binds (EvBinds bs)      = foldl ds_scc subst (sccEvBinds bs)
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index 071159d7e5..b3e7525856 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -35,6 +35,7 @@ import Name
 import Control.Monad
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Control.Arrow ( first, second )
 
 #include "HsVersions.h"
 
@@ -217,7 +218,8 @@ tcLookupFamInst fam_envs tycon tys
 -- Checks for a newtype, and for being saturated
 -- Just like Coercion.instNewTyCon_maybe, but returns a TcCoercion
 tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion)
-tcInstNewTyCon_maybe = gInstNewTyCon_maybe
+tcInstNewTyCon_maybe tc tys = fmap (second TcCoercion) $
+                              instNewTyCon_maybe tc tys
 
 -- | Like 'tcLookupDataFamInst_maybe', but returns the arguments back if
 -- there is no data family to unwrap.
@@ -226,12 +228,12 @@ tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
 tcLookupDataFamInst fam_inst_envs tc tc_args
   | Just (rep_tc, rep_args, co)
       <- tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
-  = (rep_tc, rep_args, co)
+  = (rep_tc, rep_args, TcCoercion co)
   | otherwise
   = (tc, tc_args, mkTcRepReflCo (mkTyConApp tc tc_args))
 
 tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType]
-                          -> Maybe (TyCon, [TcType], TcCoercion)
+                          -> Maybe (TyCon, [TcType], Coercion)
 -- ^ Converts a data family type (eg F [a]) to its representation type (eg FList a)
 -- and returns a coercion between the two: co :: F [a] ~R FList a
 tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
@@ -241,7 +243,7 @@ tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
                  , fim_tys      = rep_args } <- match
   , let co_tc  = famInstAxiom rep_fam
         rep_tc = dataFamInstRepTyCon rep_fam
-        co     = mkTcUnbranchedAxInstCo Representational co_tc rep_args
+        co     = mkUnbranchedAxInstCo Representational co_tc rep_args
   = Just (rep_tc, rep_args, co)
 
   | otherwise
@@ -263,7 +265,7 @@ tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs
                               -> Maybe (TcCoercion, Type)
 tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
 -- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe
-  = topNormaliseTypeX_maybe stepper ty
+  = fmap (first TcCoercion) $ topNormaliseTypeX_maybe stepper ty
   where
     stepper
       = unwrap_newtype
@@ -271,7 +273,7 @@ tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
         \ rec_nts tc tys ->
         case tcLookupDataFamInst_maybe faminsts tc tys of
           Just (tc', tys', co) ->
-            modifyStepResultCo (co `mkTcTransCo`)
+            modifyStepResultCo (co `mkTransCo`)
                                (unwrap_newtype rec_nts tc' tys')
           Nothing -> NS_Done
 
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 8183e87b18..60ac88994e 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -147,12 +147,9 @@ data TcCoercion
   | TcSubCo TcCoercion
   | TcCastCo TcCoercion TcCoercion     -- co1 |> co2
   | TcLetCo TcEvBinds TcCoercion
+  | TcCoercion Coercion            -- embed a Core Coercion
   deriving (Data.Data, Data.Typeable)
 
-instance IsCoercion TcCoercion where
-  gMkTransCo  = mkTcTransCo
-  gMkAxInstCo = mkTcAxInstCo
-
 isEqVar :: Var -> Bool
 -- Is lifted coercion variable (only!)
 isEqVar v = case tyConAppTyCon_maybe (varType v) of
@@ -382,6 +379,7 @@ tcCoercionKind co = go co
        case coaxrProves ax ts (map tcCoercionKind cs) of
          Just res -> res
          Nothing -> panic "tcCoercionKind: malformed TcAxiomRuleCo"
+    go (TcCoercion co)        = coercionKind co
 
 eqVarRole :: EqVar -> Role
 eqVarRole cv = getEqPredRole (varType cv)
@@ -413,6 +411,7 @@ tcCoercionRole = go
     go (TcAxiomRuleCo c _ _)  = coaxrRole c
     go (TcCastCo c _)         = go c
     go (TcLetCo _ c)          = go c
+    go (TcCoercion co)        = coercionRole co
 
 
 coVarsOfTcCo :: TcCoercion -> VarSet
@@ -438,7 +437,10 @@ coVarsOfTcCo tc_co
     go (TcLetCo {}) = emptyVarSet    -- Harumph. This does legitimately happen in the call
                                      -- to evVarsOfTerm in the DEBUG check of setEvBind
     go (TcAxiomRuleCo _ _ cos)   = mapUnionVarSet go cos
-
+    go (TcCoercion co)           = -- the use of coVarsOfTcCo in dsTcCoercion will
+                                   -- fail if there are any proper, unlifted covars
+                                   ASSERT( isEmptyVarSet (coVarsOfCo co) )
+                                   emptyVarSet
 
     -- We expect only coercion bindings, so use evTermCoercion
     go_bind :: EvBind -> VarSet
@@ -487,6 +489,7 @@ ppr_co p (TcLRCo lr co)       = pprPrefixApp p (ppr lr) [pprParendTcCo co]
 ppr_co p (TcSubCo co)         = pprPrefixApp p (ptext (sLit "Sub")) [pprParendTcCo co]
 ppr_co p (TcAxiomRuleCo co ts ps) = maybeParen p TopPrec
                                   $ ppr_tc_axiom_rule_co co ts ps
+ppr_co p (TcCoercion co)      = pprPrefixApp p (text "Core co:") [ppr co]
 
 ppr_tc_axiom_rule_co :: CoAxiomRule -> [TcType] -> [TcCoercion] -> SDoc
 ppr_tc_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index be17cd3e79..4b7b930668 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -38,6 +38,7 @@ import TypeRep     -- We can see the representation of types
 import TcType
 import TcMType ( defaultKindVarToStar, zonkQuantifiedTyVar, writeMetaTyVar )
 import TcEvidence
+import Coercion ( coVarsOfCo )
 import TysPrim
 import TysWiredIn
 import Type
@@ -1480,3 +1481,5 @@ zonkTcCoToCo env co
                                      ; cs' <- mapM go cs
                                      ; return (TcAxiomRuleCo co ts' cs')
                                      }
+    go c@(TcCoercion _co)     = ASSERT( isEmptyVarSet (coVarsOfCo _co) )
+                                return c   -- these can't contain TcTyVars
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 5b557d489a..71a003df3e 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -30,7 +30,7 @@ module Coercion (
         mkAxiomRuleCo,
 
         -- ** Decomposition
-        gInstNewTyCon_maybe, instNewTyCon_maybe,
+        instNewTyCon_maybe,
 
         NormaliseStepper, NormaliseStepResult(..), composeSteppers,
         modifyStepResultCo, unwrapNewTypeStepper,
@@ -77,9 +77,6 @@ module Coercion (
 
         -- * Other
         applyCo,
-
-        -- * Generalised coercions
-        IsCoercion(..), gMkUnbranchedAxInstCo
        ) where
 
 #include "HsVersions.h"
@@ -1216,22 +1213,18 @@ mkCoCast c g
 
 -- | If @co :: T ts ~ rep_ty@ then:
 --
--- > gInstNewTyCon_maybe T ts = Just (rep_ty, co)
+-- > instNewTyCon_maybe T ts = Just (rep_ty, co)
 --
 -- Checks for a newtype, and for being saturated
-gInstNewTyCon_maybe :: IsCoercion co => TyCon -> [Type] -> Maybe (Type, co)
-gInstNewTyCon_maybe tc tys
+instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
+instNewTyCon_maybe tc tys
   | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc  -- Check for newtype
   , tvs `leLength` tys                                    -- Check saturated enough
   = Just ( applyTysX tvs ty tys
-         , gMkUnbranchedAxInstCo Representational co_tc tys)
+         , mkUnbranchedAxInstCo Representational co_tc tys)
   | otherwise
   = Nothing
 
--- | Type-restricted form of 'gInstNewTyCon_maybe'.
-instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
-instNewTyCon_maybe = gInstNewTyCon_maybe
-
 {-
 ************************************************************************
 *                                                                      *
@@ -1242,28 +1235,28 @@ instNewTyCon_maybe = gInstNewTyCon_maybe
 
 -- | A function to check if we can reduce a type by one step. Used
 -- with 'topNormaliseTypeX_maybe'.
-type NormaliseStepper co = RecTcChecker
-                        -> TyCon     -- tc
-                        -> [Type]    -- tys
-                        -> NormaliseStepResult co
+type NormaliseStepper = RecTcChecker
+                     -> TyCon     -- tc
+                     -> [Type]    -- tys
+                     -> NormaliseStepResult
 
 -- | The result of stepping in a normalisation function.
 -- See 'topNormaliseTypeX_maybe'.
-data NormaliseStepResult co
+data NormaliseStepResult
   = NS_Done   -- ^ nothing more to do
   | NS_Abort  -- ^ utter failure. The outer function should fail too.
-  | NS_Step RecTcChecker Type co  -- ^ we stepped, yielding new bits;
-                                  -- ^ co :: old type ~ new type
+  | NS_Step RecTcChecker Type Coercion  -- ^ we stepped, yielding new bits;
+                                        -- ^ co :: old type ~ new type
 
-modifyStepResultCo :: (co -> co)
-                   -> NormaliseStepResult co -> NormaliseStepResult co
+modifyStepResultCo :: (Coercion -> Coercion)
+                   -> NormaliseStepResult -> NormaliseStepResult
 modifyStepResultCo f (NS_Step rec_nts ty co) = NS_Step rec_nts ty (f co)
 modifyStepResultCo _ result                  = result
 
 -- | Try one stepper and then try the next, if the first doesn't make
 -- progress.
-composeSteppers :: NormaliseStepper co -> NormaliseStepper co
-                -> NormaliseStepper co
+composeSteppers :: NormaliseStepper -> NormaliseStepper
+                -> NormaliseStepper
 composeSteppers step1 step2 rec_nts tc tys
   = case step1 rec_nts tc tys of
       success@(NS_Step {}) -> success
@@ -1272,9 +1265,9 @@ composeSteppers step1 step2 rec_nts tc tys
 
 -- | A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
 -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
-unwrapNewTypeStepper :: IsCoercion co => NormaliseStepper co
+unwrapNewTypeStepper :: NormaliseStepper
 unwrapNewTypeStepper rec_nts tc tys
-  | Just (ty', co) <- gInstNewTyCon_maybe tc tys
+  | Just (ty', co) <- instNewTyCon_maybe tc tys
   = case checkRecTc rec_nts tc of
       Just rec_nts' -> NS_Step rec_nts' ty' co
       Nothing       -> NS_Abort
@@ -1287,8 +1280,7 @@ unwrapNewTypeStepper rec_nts tc tys
 -- this function returns. The roles of the coercions produced by the
 -- 'NormaliseStepper' must all be the same, which is the role returned from
 -- the call to 'topNormaliseTypeX_maybe'.
-topNormaliseTypeX_maybe :: IsCoercion co
-                        => NormaliseStepper co -> Type -> Maybe (co, Type)
+topNormaliseTypeX_maybe :: NormaliseStepper -> Type -> Maybe (Coercion, Type)
 topNormaliseTypeX_maybe stepper
   = go initRecTc Nothing
   where
@@ -1308,7 +1300,7 @@ topNormaliseTypeX_maybe stepper
                  | otherwise         = Nothing
 
     Nothing    `trans` co2 = Just co2
-    (Just co1) `trans` co2 = Just (co1 `gMkTransCo` co2)
+    (Just co1) `trans` co2 = Just (co1 `mkTransCo` co2)
 
 topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
@@ -1984,26 +1976,5 @@ Note [Kind coercions]
 Kind coercions are only of the form: Refl kind. They are only used to
 instantiate kind polymorphic type constructors in TyConAppCo. Remember
 that kind instantiation only happens with TyConApp, not AppTy.
-
-%************************************************************************
-%*                                                                      *
-                   Generalised coercions
-%*                                                                      *
-%************************************************************************
 -}
 
--- | Classifies a coercion type. The two canonical inhabitants are
--- 'Coercion' and 'TcCoercion'. This is useful in order to parameterise
--- several functions. Note that there are many missing features; they
--- can be added as necessary.
-class Outputable co => IsCoercion co where
-  gMkTransCo  :: co -> co -> co
-  gMkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> co
-
-instance IsCoercion Coercion where
-  gMkTransCo  = mkTransCo
-  gMkAxInstCo = mkAxInstCo
-
-gMkUnbranchedAxInstCo :: IsCoercion co
-                      => Role -> CoAxiom Unbranched -> [Type] -> co
-gMkUnbranchedAxInstCo r ax = gMkAxInstCo r ax 0