Super-monster patch implementing the new typechecker -- at last

[ghc-hetmet.git] / compiler / types / FamInstEnv.lhs

diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index d1a3445..4cf33fc 100644 (file)
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -10,22 +10,20 @@ module FamInstEnv (
        pprFamInst, pprFamInstHdr, pprFamInsts, 
        famInstHead, mkLocalFamInst, mkImportedFamInst,
 
        pprFamInst, pprFamInstHdr, pprFamInsts, 
        famInstHead, mkLocalFamInst, mkImportedFamInst,
 

-       FamInstEnvs, FamInstEnv, emptyFamInstEnv, 
+       FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, 

        extendFamInstEnv, extendFamInstEnvList, 
        famInstEnvElts, familyInstances,
 
        extendFamInstEnv, extendFamInstEnvList, 
        famInstEnvElts, familyInstances,
 

-       lookupFamInstEnv, lookupFamInstEnvUnify,
+       lookupFamInstEnv, lookupFamInstEnvConflicts,

        
        -- Normalisation
        
        -- Normalisation

-       toplevelNormaliseFamInst
+       topNormaliseType

     ) where
 
 #include "HsVersions.h"
 
 import InstEnv
 import Unify
     ) where
 
 #include "HsVersions.h"
 
 import InstEnv
 import Unify

-import TcGadt
-import TcType

 import Type
 import TypeRep
 import TyCon
 import Type
 import TypeRep
 import TyCon

@@ -33,14 +31,11 @@ import Coercion
 import VarSet
 import Var
 import Name
 import VarSet
 import Var
 import Name

-import OccName
-import SrcLoc

 import UniqFM
 import Outputable
 import Maybes
 import Util
 import UniqFM
 import Outputable
 import Maybes
 import Util

-
-import Maybe
+import FastString

 \end{code}
 
 
 \end{code}
 
 

@@ -75,6 +70,7 @@ data FamInst
 famInstTyCon :: FamInst -> TyCon
 famInstTyCon = fi_tycon
 
 famInstTyCon :: FamInst -> TyCon
 famInstTyCon = fi_tycon
 

+famInstTyVars :: FamInst -> TyVarSet

 famInstTyVars = fi_tvs
 \end{code}
 
 famInstTyVars = fi_tvs
 \end{code}
 

@@ -89,17 +85,18 @@ instance Outputable FamInst where
 pprFamInst :: FamInst -> SDoc
 pprFamInst famInst
   = hang (pprFamInstHdr famInst)
 pprFamInst :: FamInst -> SDoc
 pprFamInst famInst
   = hang (pprFamInstHdr famInst)

-       2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcSpan famInst)))
+       2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))

 
 pprFamInstHdr :: FamInst -> SDoc
 pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
   = pprTyConSort <+> pprHead
   where
 
 pprFamInstHdr :: FamInst -> SDoc
 pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
   = pprTyConSort <+> pprHead
   where

-    pprHead = pprTypeApp (parenSymOcc (getOccName fam) (ppr fam)) tys
-    pprTyConSort | isDataTyCon tycon = ptext SLIT("data instance")
-                | isNewTyCon  tycon = ptext SLIT("newtype instance")
-                | isSynTyCon  tycon = ptext SLIT("type instance")
-                | otherwise         = panic "FamInstEnv.pprFamInstHdr"
+    pprHead = pprTypeApp fam tys
+    pprTyConSort | isDataTyCon     tycon = ptext (sLit "data instance")
+                | isNewTyCon      tycon = ptext (sLit "newtype instance")
+                | isSynTyCon      tycon = ptext (sLit "type instance")
+                | isAbstractTyCon tycon = ptext (sLit "data instance")
+                | otherwise             = panic "FamInstEnv.pprFamInstHdr"

 
 pprFamInsts :: [FamInst] -> SDoc
 pprFamInsts finsts = vcat (map pprFamInst finsts)
 
 pprFamInsts :: [FamInst] -> SDoc
 pprFamInsts finsts = vcat (map pprFamInst finsts)

@@ -168,6 +165,9 @@ data FamilyInstEnv
 --  * The fs_tvs are distinct in each FamInst
 --     of a range value of the map (so we can safely unify them)
 
 --  * The fs_tvs are distinct in each FamInst
 --     of a range value of the map (so we can safely unify them)
 

+emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
+emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
+

 emptyFamInstEnv :: FamInstEnv
 emptyFamInstEnv = emptyUFM
 
 emptyFamInstEnv :: FamInstEnv
 emptyFamInstEnv = emptyUFM
 

@@ -196,7 +196,7 @@ extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *

-\subsection{Looking up a family instance}
+               Looking up a family instance

 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 

@@ -219,48 +219,68 @@ we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
 
 \begin{code}
 type FamInstMatch = (FamInst, [Type])           -- Matching type instance
 
 \begin{code}
 type FamInstMatch = (FamInst, [Type])           -- Matching type instance

-
-lookupFamInstEnv :: FamInstEnvs
-                -> TyCon -> [Type]             -- What we are looking for
-                -> [FamInstMatch]              -- Successful matches
-lookupFamInstEnv (pkg_ie, home_ie) fam tys
-  = home_matches ++ pkg_matches
+  -- See Note [Over-saturated matches]
+
+lookupFamInstEnv
+    :: FamInstEnvs
+    -> TyCon -> [Type]         -- What we are looking for
+    -> [FamInstMatch]          -- Successful matches
+
+lookupFamInstEnv
+   = lookup_fam_inst_env match True
+   where
+     match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
+
+lookupFamInstEnvConflicts
+    :: FamInstEnvs
+    -> FamInst         -- Putative new instance
+    -> [TyVar]         -- Unique tyvars, matching arity of FamInst
+    -> [FamInstMatch]  -- Conflicting matches
+-- E.g. when we are about to add
+--    f : type instance F [a] = a->a
+-- we do (lookupFamInstConflicts f [b])
+-- to find conflicting matches
+-- The skolem tyvars are needed because we don't have a 
+-- unique supply to hand
+
+lookupFamInstEnvConflicts envs fam_inst skol_tvs
+  = lookup_fam_inst_env my_unify False envs fam tys'

   where
   where

-    rough_tcs    = roughMatchTcs tys
-    all_tvs      = all isNothing rough_tcs
-    home_matches = lookup home_ie 
-    pkg_matches  = lookup pkg_ie  
-
-    --------------
-    lookup env = case lookupUFM env fam of
-                  Nothing -> []        -- No instances for this class
-                  Just (FamIE insts has_tv_insts)
-                      -- Short cut for common case:
-                      --   The thing we are looking up is of form (C a
-                      --   b c), and the FamIE has no instances of
-                      --   that form, so don't bother to search 
-                    | all_tvs && not has_tv_insts -> []
-                    | otherwise                   -> find insts
-
-    --------------
-    find [] = []
-    find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, 
-                         fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
-       -- Fast check for no match, uses the "rough match" fields
-      | instanceCantMatch rough_tcs mb_tcs
-      = find rest
-
-        -- Proper check
-      | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
-      = (item, substTyVars subst (tyConTyVars tycon)) : find rest
-
-        -- No match => try next
-      | otherwise
-      = find rest
+    inst_tycon = famInstTyCon fam_inst
+    (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
+                           (tyConFamInst_maybe inst_tycon)
+    skol_tys = mkTyVarTys skol_tvs
+    tys'     = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
+        -- In example above,   fam tys' = F [b]   
+
+    my_unify old_fam_inst tpl_tvs tpl_tys match_tys
+       = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
+                 (ppr fam <+> ppr tys) $$
+                 (ppr tpl_tvs <+> ppr tpl_tys) )
+               -- Unification will break badly if the variables overlap
+               -- They shouldn't because we allocate separate uniques for them
+         case tcUnifyTys instanceBindFun tpl_tys match_tys of
+             Just subst | conflicting old_fam_inst subst -> Just subst
+             _other                                      -> Nothing
+
+      -- - In the case of data family instances, any overlap is fundamentally a
+      --   conflict (as these instances imply injective type mappings).
+      -- - In the case of type family instances, overlap is admitted as long as
+      --   the right-hand sides of the overlapping rules coincide under the
+      --   overlap substitution.  We require that they are syntactically equal;
+      --   anything else would be difficult to test for at this stage.
+    conflicting old_fam_inst subst 
+      | isAlgTyCon fam = True
+      | otherwise      = not (old_rhs `tcEqType` new_rhs)
+      where
+        old_tycon = famInstTyCon old_fam_inst
+        old_tvs   = tyConTyVars old_tycon
+        old_rhs   = mkTyConApp old_tycon  (substTyVars subst old_tvs)
+        new_rhs   = mkTyConApp inst_tycon (substTyVars subst skol_tvs)

 \end{code}
 
 While @lookupFamInstEnv@ uses a one-way match, the next function
 \end{code}
 
 While @lookupFamInstEnv@ uses a one-way match, the next function

-@lookupFamInstEnvUnify@ uses two-way matching (ie, unification).  This is
+@lookupFamInstEnvConflicts@ uses two-way matching (ie, unification).  This is

 needed to check for overlapping instances.
 
 For class instances, these two variants of lookup are combined into one
 needed to check for overlapping instances.
 
 For class instances, these two variants of lookup are combined into one

@@ -270,16 +290,45 @@ Moreover, matching is the wildly more frequently used operation in the case of
 indexed synonyms and we don't want to slow that down by needless unification.
 
 \begin{code}
 indexed synonyms and we don't want to slow that down by needless unification.
 
 \begin{code}

-lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
-                     -> [(FamInstMatch)]
-lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
-  = home_matches ++ pkg_matches
+------------------------------------------------------------
+-- Might be a one-way match or a unifier
+type MatchFun =  FamInst               -- The FamInst template
+             -> TyVarSet -> [Type]     --   fi_tvs, fi_tys of that FamInst
+             -> [Type]                 -- Target to match against
+             -> Maybe TvSubst
+
+type OneSidedMatch = Bool     -- Are optimisations that are only valid for
+                              -- one sided matches allowed?
+
+lookup_fam_inst_env          -- The worker, local to this module
+    :: MatchFun
+    -> OneSidedMatch
+    -> FamInstEnvs
+    -> TyCon -> [Type]         -- What we are looking for
+    -> [FamInstMatch]          -- Successful matches
+lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
+  | not (isFamilyTyCon fam) 
+  = []
+  | otherwise
+  = ASSERT( n_tys >= arity )   -- Family type applications must be saturated
+    home_matches ++ pkg_matches

   where
   where

-    rough_tcs    = roughMatchTcs tys
-    all_tvs      = all isNothing rough_tcs

     home_matches = lookup home_ie 
     pkg_matches  = lookup pkg_ie  
 
     home_matches = lookup home_ie 
     pkg_matches  = lookup pkg_ie  
 

+    -- See Note [Over-saturated matches]
+    arity = tyConArity fam
+    n_tys = length tys
+    extra_tys = drop arity tys
+    (match_tys, add_extra_tys) 
+       | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
+       | otherwise     = (tys,            \res_tys -> res_tys)
+                -- The second case is the common one, hence functional representation
+
+    --------------
+    rough_tcs = roughMatchTcs match_tys
+    all_tvs   = all isNothing rough_tcs && one_sided
+

     --------------
     lookup env = case lookupUFM env fam of
                   Nothing -> []        -- No instances for this class
     --------------
     lookup env = case lookupUFM env fam of
                   Nothing -> []        -- No instances for this class

@@ -299,117 +348,149 @@ lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
       | instanceCantMatch rough_tcs mb_tcs
       = find rest
 
       | instanceCantMatch rough_tcs mb_tcs
       = find rest
 

-      | otherwise
-      = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
-                (ppr fam <+> ppr tys <+> ppr all_tvs) $$
-                (ppr tycon <+> ppr tpl_tvs <+> ppr tpl_tys)
-               )
-               -- Unification will break badly if the variables overlap
-               -- They shouldn't because we allocate separate uniques for them
-        case tcUnifyTys bind_fn tpl_tys tys of
-           Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon)
-                          in
-                          (item, rep_tys) : find rest
-           Nothing    -> find rest
+        -- Proper check
+      | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
+      = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest

 
 

--- See explanation at @InstEnv.bind_fn@.
---
-bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
-          | otherwise                             = BindMe
+        -- No match => try next
+      | otherwise
+      = find rest

 \end{code}
 
 \end{code}
 

---------------------------------------
--- Normalisation 
+Note [Over-saturated matches]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's ok to look up an over-saturated type constructor.  E.g.
+     type family F a :: * -> *
+     type instance F (a,b) = Either (a->b)
+
+The type instance gives rise to a newtype TyCon (at a higher kind
+which you can't do in Haskell!):
+     newtype FPair a b = FP (Either (a->b))
+
+Then looking up (F (Int,Bool) Char) will return a FamInstMatch 
+     (FPair, [Int,Bool,Char])
+
+The "extra" type argument [Char] just stays on the end.
+
+
+
+
+%************************************************************************
+%*                                                                     *
+               Looking up a family instance
+%*                                                                     *
+%************************************************************************

 
 \begin{code}
 
 \begin{code}

-       -- get rid of TOPLEVEL type functions by rewriting them 
-       -- i.e. treating their equations as a TRS
-toplevelNormaliseFamInst :: FamInstEnvs ->
-                           Type ->
-                           (CoercionI,Type)
-toplevelNormaliseFamInst env ty
-       | Just ty' <- tcView ty = normaliseFamInst env ty'
-toplevelNormaliseFamInst env ty@(TyConApp tyCon tys)
-       | isOpenTyCon tyCon
-       = normaliseFamInst env ty
-toplevelNormaliseFamInst env ty
-       = (IdCo,ty)
+topNormaliseType :: FamInstEnvs
+                -> Type
+                -> Maybe (Coercion, Type)
+
+-- Get rid of *outermost* (or toplevel) 
+--     * type functions 
+--     * newtypes
+-- using appropriate coercions.
+-- By "outer" we mean that toplevelNormaliseType guarantees to return
+-- a type that does not have a reducible redex (F ty1 .. tyn) as its
+-- outermost form.  It *can* return something like (Maybe (F ty)), where
+-- (F ty) is a redex.
+
+-- Its a bit like Type.repType, but handles type families too
+
+topNormaliseType env ty
+  = go [] ty
+  where
+    go :: [TyCon] -> Type -> Maybe (Coercion, Type)
+    go rec_nts ty | Just ty' <- coreView ty    -- Expand synonyms
+       = go rec_nts ty'        
+
+    go rec_nts (TyConApp tc tys)               -- Expand newtypes
+       | Just co_con <- newTyConCo_maybe tc    -- See Note [Expanding newtypes]
+       = if tc `elem` rec_nts                  --  in Type.lhs
+         then Nothing
+         else let nt_co = mkTyConApp co_con tys
+              in add_co nt_co rec_nts' nt_rhs
+       where
+         nt_rhs = newTyConInstRhs tc tys
+         rec_nts' | isRecursiveTyCon tc = tc:rec_nts
+                  | otherwise           = rec_nts
+
+    go rec_nts (TyConApp tc tys)               -- Expand open tycons
+       | isFamilyTyCon tc
+       , (ACo co, ty) <- normaliseTcApp env tc tys
+       =       -- The ACo says "something happened"
+               -- Note that normaliseType fully normalises, but it has do to so
+               -- to be sure that 
+          add_co co rec_nts ty
+
+    go _ _ = Nothing
+
+    add_co co rec_nts ty 
+       = case go rec_nts ty of
+               Nothing         -> Just (co, ty)
+               Just (co', ty') -> Just (mkTransCoercion co co', ty')

         
 
         
 

-       -- get rid of ALL type functions by rewriting them 
-       -- i.e. treating their equations as a TRS
-normaliseFamInst :: FamInstEnvs ->     -- environment with family instances
-                   Type ->             -- old type
-                   (CoercionI,Type)    -- (coercion,new type)
-normaliseFamInst env ty 
-       | Just ty' <- tcView ty = normaliseFamInst env ty' 
-normaliseFamInst env ty@(TyConApp tyCon tys) =
-       let (cois,ntys) = mapAndUnzip (normaliseFamInst env) tys
-           tycon_coi   = mkTyConAppCoI tyCon ntys cois
-           maybe_ty_co = lookupFamInst env tyCon ntys
-        in case maybe_ty_co of
-               -- a matching family instance exists
-               Just (ty',co) ->
-                       let first_coi      = mkTransCoI tycon_coi (ACo co)
-                           (rest_coi,nty) = normaliseFamInst env ty'
-                           fix_coi        = mkTransCoI first_coi rest_coi
-                       in (fix_coi,nty)
-               -- no matching family instance exists
+---------------
+normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
+normaliseTcApp env tc tys
+  = let        -- First normalise the arg types so that they'll match 
+       -- when we lookup in in the instance envt
+       (cois, ntys) = mapAndUnzip (normaliseType env) tys
+       tycon_coi    = mkTyConAppCoI tc cois
+    in         -- Now try the top-level redex
+    case lookupFamInstEnv env tc ntys of
+               -- A matching family instance exists
+       [(fam_inst, tys)] -> (fix_coi, nty)
+           where
+               rep_tc         = famInstTyCon fam_inst
+               co_tycon       = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
+               co             = mkTyConApp co_tycon tys
+               first_coi      = mkTransCoI tycon_coi (ACo co)
+               (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys)
+               fix_coi        = mkTransCoI first_coi rest_coi
+
+               -- No unique matching family instance exists;

                -- we do not do anything
                -- we do not do anything

-               Nothing -> 
-                       (tycon_coi,TyConApp tyCon ntys)
-normaliseFamInst env ty@(AppTy ty1 ty2)        =
-       let (coi1,nty1) = normaliseFamInst env ty1
-           (coi2,nty2) = normaliseFamInst env ty2
-       in  (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
-normaliseFamInst env ty@(FunTy ty1 ty2)        =
-       let (coi1,nty1) = normaliseFamInst env ty1
-           (coi2,nty2) = normaliseFamInst env ty2
-       in  (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
-normaliseFamInst env ty@(ForAllTy tyvar ty1)   =
-       let (coi,nty1) = normaliseFamInst env ty1
-       in  (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
-normaliseFamInst env ty@(NoteTy note ty1)      =
-       let (coi,nty1) = normaliseFamInst env ty1
-       in  (mkNoteTyCoI note coi,NoteTy note nty1)
-normaliseFamInst env ty@(TyVarTy _) =
-       (IdCo,ty)
-normaliseFamInst env (PredTy predty) =
-       normaliseFamInstPred env predty 
-
-normaliseFamInstPred :: FamInstEnvs -> PredType -> (CoercionI,Type)
-normaliseFamInstPred env (ClassP cls tys) =
-       let (cois,tys') = mapAndUnzip (normaliseFamInst env) tys
-       in  (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
-normaliseFamInstPred env (IParam ipn ty) =
-       let (coi,ty') = normaliseFamInst env ty
+       _ -> (tycon_coi, TyConApp tc ntys)
+---------------
+normaliseType :: FamInstEnvs           -- environment with family instances
+             -> Type                   -- old type
+             -> (CoercionI, Type)      -- (coercion,new type), where
+                                       -- co :: old-type ~ new_type
+-- Normalise the input type, by eliminating *all* type-function redexes
+-- Returns with IdCo if nothing happens
+
+normaliseType env ty 
+  | Just ty' <- coreView ty = normaliseType env ty' 
+normaliseType env (TyConApp tc tys)
+  = normaliseTcApp env tc tys
+normaliseType env (AppTy ty1 ty2)
+  = let (coi1,nty1) = normaliseType env ty1
+        (coi2,nty2) = normaliseType env ty2
+    in  (mkAppTyCoI coi1 coi2, AppTy nty1 nty2)
+normaliseType env (FunTy ty1 ty2)
+  = let (coi1,nty1) = normaliseType env ty1
+        (coi2,nty2) = normaliseType env ty2
+    in  (mkFunTyCoI coi1 coi2, FunTy nty1 nty2)
+normaliseType env (ForAllTy tyvar ty1)
+  = let (coi,nty1) = normaliseType env ty1
+    in  (mkForAllTyCoI tyvar coi, ForAllTy tyvar nty1)
+normaliseType _   ty@(TyVarTy _)
+  = (IdCo ty,ty)
+normaliseType env (PredTy predty)
+  = normalisePred env predty
+
+---------------
+normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
+normalisePred env (ClassP cls tys)
+  =    let (cois,tys') = mapAndUnzip (normaliseType env) tys
+       in  (mkClassPPredCoI cls cois, PredTy $ ClassP cls tys')
+normalisePred env (IParam ipn ty)
+  =    let (coi,ty') = normaliseType env ty

        in  (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
        in  (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')

-normaliseFamInstPred env (EqPred ty1 ty2) =
-       let (coi1,ty1') = normaliseFamInst env ty1
-            (coi2,ty2') = normaliseFamInst env ty2
-       in  (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')
- 
-lookupFamInst :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Type,Coercion)
-
--- (lookupFamInst F tys) looks for a top-level instance
---     co : forall a. F tys' = G a
---   (The rhs is always of form G a; see Note [The FamInst structure]
---     in FamInst.)
--- where we can instantiate 'a' with t to make tys'[t/a] = tys
--- Hence   (co t) : F tys ~ G t
--- Then we return (Just (G t, co t))
-
-lookupFamInst env tycon tys 
-  | not (isOpenTyCon tycon)            -- Dead code; fix.
-  = Nothing
-  | otherwise
-  = case lookupFamInstEnv env tycon tys of
-          [(subst, fam_inst)] -> 
-            Just (mkTyConApp rep_tc substituted_vars, mkTyConApp coercion_tycon substituted_vars)
-               where   -- NB: invariant of lookupFamInstEnv is that (tyConTyVars rep_tc)
-                       --     is in the domain of the substitution
-                 rep_tc           = famInstTyCon fam_inst
-                 coercion_tycon   = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
-                 substituted_vars = substTyVars subst (tyConTyVars rep_tc)
-          other -> Nothing
+normalisePred env (EqPred ty1 ty2)
+  =    let (coi1,ty1') = normaliseType env ty1
+            (coi2,ty2') = normaliseType env ty2
+       in  (mkEqPredCoI coi1 coi2, PredTy $ EqPred ty1' ty2')

 \end{code}
 \end{code}