Use reduceTyFamApp_maybe in TcInteract.matchFamwip/rae-new-coercible

3 files changed, 10 insertions, 33 deletions

diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index a0433f954f..16d4bfcb67 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -38,7 +38,7 @@ import TypeRep     -- We can see the representation of types
 import TcType
 import TcMType ( defaultKindVarToStar, zonkQuantifiedTyVar, writeMetaTyVar )
 import TcEvidence
-import Coercion ( coVarsOfCo )
+import Coercion
 import TysPrim
 import TysWiredIn
 import Type
@@ -1426,14 +1426,14 @@ zonkCoToCo env co
     go (Refl r ty)               = mkReflCo r <$> zonkTcTypeToType env ty
     go (TyConAppCo r tc args)    = mkTyConAppCo r tc <$> mapM go args
     go (AppCo co arg)            = mkAppCo <$> go co <*> go arg
-    go (AxiomInstCo ax ind args) = mkAxiomInstCo ax ind <$> mapM go args
+    go (AxiomInstCo ax ind args) = AxiomInstCo ax ind <$> mapM go args
     go (UnivCo r ty1 ty2)        = mkUnivCo r <$> zonkTcTypeToType env ty1
                                               <*> zonkTcTypeToType env ty2
     go (SymCo co)                = mkSymCo <$> go co
     go (TransCo co1 co2)         = mkTransCo <$> go co1 <*> go co2
     go (NthCo n co)              = mkNthCo n <$> go co
     go (LRCo lr co)              = mkLRCo lr <$> go co
-    go (InstCo co arg)           = mkInstCo <$> go co <*> zonkCoArgToCoArg env arg
+    go (InstCo co arg)           = mkInstCo <$> go co <*> zonkTcTypeToType env arg
     go (SubCo co)                = mkSubCo <$> go co
     go (AxiomRuleCo ax ts cs)    = AxiomRuleCo ax <$> mapM (zonkTcTypeToType env) ts
                                                   <*> mapM go cs
@@ -1507,4 +1507,5 @@ zonkTcCoToCo env co
                                      ; cs' <- mapM go cs
                                      ; return (TcAxiomRuleCo co ts' cs')
                                      }
-    go (TcCoercion co)        = do { co' <- zonkCoToCo co; return (TcCoercion co') }
+    go (TcCoercion co)        = do { co' <- zonkCoToCo env co
+                                   ; return (TcCoercion co') }
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 0e37bc1f72..a0dda96f84 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -106,7 +106,6 @@ import Kind
 import TcType
 import DynFlags
 import Type
-import CoAxiom(sfMatchFam)
 
 import TcEvidence
 import Class
@@ -132,11 +131,11 @@ import UniqFM
 import Maybes ( orElse, firstJusts )
 
 import TrieMap
+import Control.Arrow ( first )
 import Control.Monad( ap, when, unless, MonadPlus(..) )
 import MonadUtils
 import Data.IORef
 import Data.List ( partition, foldl' )
-import Pair
 
 #ifdef DEBUG
 import Digraph
@@ -1742,33 +1741,9 @@ instDFunConstraints loc = mapM (newWantedEvVar loc)
 matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
 matchFam tycon args
-  | isOpenTypeFamilyTyCon tycon
   = do { fam_envs <- getFamInstEnvs
-       ; let mb_match = tcLookupFamInst fam_envs tycon args
-       ; traceTcS "lookupFamInst" $
-                  vcat [ ppr tycon <+> ppr args
-                       , pprTvBndrs (varSetElems (tyVarsOfTypes args))
-                       , ppr mb_match ]
-       ; case mb_match of
-           Nothing -> return Nothing
-           Just (FamInstMatch { fim_instance = famInst
-                              , fim_tys      = inst_tys })
-             -> let co = mkTcUnbranchedAxInstCo Nominal (famInstAxiom famInst) inst_tys
-                    ty = pSnd $ tcCoercionKind co
-                in return $ Just (co, ty) }
-
-  | Just ax <- isClosedSynFamilyTyCon_maybe tycon
-  , Just (ind, inst_tys) <- chooseBranch ax args
-  = let co = mkTcAxInstCo Nominal ax ind inst_tys
-        ty = pSnd (tcCoercionKind co)
-    in return $ Just (co, ty)
-
-  | Just ops <- isBuiltInSynFamTyCon_maybe tycon =
-    return $ do (r,ts,ty) <- sfMatchFam ops args
-                return (mkTcAxiomRuleCo r ts [], ty)
-
-  | otherwise
-  = return Nothing
+       ; return $ fmap (first TcCoercion) $
+         reduceTyFamApp_maybe fam_envs Nominal tycon args }
 
 {-
 Note [Residual implications]
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index 25787264ac..0b5bf2b521 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -20,11 +20,12 @@ module FamInstEnv (
 
         FamInstMatch(..),
         lookupFamInstEnv, lookupFamInstEnvConflicts,
-        chooseBranch, isDominatedBy,
+        isDominatedBy,
 
         -- Normalisation
         topNormaliseType, topNormaliseType_maybe,
         normaliseType, normaliseTcApp,
+        reduceTyFamApp_maybe,
 
         -- Flattening
         flattenTys