Look through type synonyms when deciding if something is a type literal.
[ghc.git] / compiler / types / FamInstEnv.lhs
index b1ab2f6..0efd3ca 100644 (file)
@@ -5,28 +5,32 @@
 FamInstEnv: Type checked family instance declarations
 
 \begin{code}
-{-# OPTIONS -fno-warn-tabs #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and
--- detab the module (please do the detabbing in a separate patch). See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
--- for details
-
 module FamInstEnv (
-       FamInst(..), FamFlavor(..), famInstAxiom, famInstTyVars,
-        famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon, 
-        famInstLHS,
-       pprFamInst, pprFamInstHdr, pprFamInsts, 
-       mkSynFamInst, mkDataFamInst, mkImportedFamInst,
-
-       FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, 
-       extendFamInstEnv, overwriteFamInstEnv, extendFamInstEnvList, 
-       famInstEnvElts, familyInstances,
-
-       lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvConflicts',
-       
-       -- Normalisation
-       topNormaliseType, normaliseType, normaliseTcApp
+        Branched, Unbranched,
+
+        FamInst(..), FamFlavor(..), FamInstBranch(..), 
+
+        famInstAxiom, famInstBranchRoughMatch,
+        famInstsRepTyCons, famInstNthBranch, famInstSingleBranch,
+        famInstBranchLHS, famInstBranches, 
+        toBranchedFamInst, toUnbranchedFamInst,
+        famInstTyCon, famInstRepTyCon_maybe, dataFamInstRepTyCon, 
+        pprFamInst, pprFamInsts, 
+        pprFamFlavor, 
+        mkImportedFamInst, 
+
+        FamInstEnv, FamInstEnvs,
+        emptyFamInstEnvs, emptyFamInstEnv, famInstEnvElts, familyInstances,
+        extendFamInstEnvList, extendFamInstEnv, deleteFromFamInstEnv,
+        identicalFamInst,
+
+        FamInstMatch(..),
+        lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvConflicts',
+        
+        isDominatedBy,
+
+        -- Normalisation
+        topNormaliseType, normaliseType, normaliseTcApp
     ) where
 
 #include "HsVersions.h"
@@ -34,11 +38,14 @@ module FamInstEnv (
 import InstEnv
 import Unify
 import Type
+import Coercion hiding ( substTy )
 import TypeRep
 import TyCon
-import Coercion
+import CoAxiom
 import VarSet
+import VarEnv
 import Name
+import NameSet
 import UniqFM
 import Outputable
 import Maybes
@@ -48,9 +55,9 @@ import FastString
 
 
 %************************************************************************
-%*                                                                     *
-\subsection{Type checked family instance heads}
-%*                                                                     *
+%*                                                                      *
+           Type checked family instance heads
+%*                                                                      *
 %************************************************************************
 
 Note [FamInsts and CoAxioms]
@@ -61,38 +68,77 @@ Note [FamInsts and CoAxioms]
 * A CoAxiom is a System-FC thing: it can relate any two types
 
 * A FamInst is a Haskell source-language thing, corresponding
-  to a type/data family instance declaration.  
+  to a type/data family instance declaration.
     - The FamInst contains a CoAxiom, which is the evidence
       for the instance
 
-    - The LHS of the CoAxiom is always of form F ty1 .. tyn
-      where F is a type family
+    - The LHSs of the CoAxiom branches are always of form
+      F ty1 .. tyn where F is a type family
+
+* A FamInstBranch corresponds to a CoAxBranch -- it represents
+  one alternative in a family instance group. We could theoretically
+  not have FamInstBranches and just use the CoAxBranches within
+  the CoAxiom stored in the FamInst, but for one problem: we want to
+  cache the "rough match" top-level tycon names for quick matching.
+  This data is not stored in a CoAxBranch, so we use FamInstBranches
+  instead.
 
+Note [fi_group field]
+~~~~~~~~~~~~~~~~~~~~~
+A FamInst stores whether or not it was declared with "type instance where"
+for two reasons: 
+  1. for accurate pretty-printing; and 
+  2. because confluent overlap is disallowed between branches 
+     declared in groups. 
+Note that this "group-ness" is properly associated with the FamInst,
+which thinks about overlap, and not in the CoAxiom, which blindly
+assumes that it is part of a consistent axiom set.
+
+A "group" with fi_group=True can have just one element, however.
+
+Note [Why we need fib_rhs]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+It may at first seem unnecessary to store the right-hand side of an equation
+in a FamInstBranch. After all, FamInstBranches are used only for matching a
+family application; the underlying CoAxiom is used to perform the actual
+simplification.
+
+However, we do need to know the rhs field during conflict checking to support
+confluent overlap. When two unbranched instances have overlapping left-hand
+sides, we check if the right-hand sides are coincident in the region of overlap.
+This check requires fib_rhs. See lookupFamInstEnvConflicts.
 
 \begin{code}
-data FamInst  -- See Note [FamInsts and CoAxioms]
-  = FamInst { fi_axiom  :: CoAxiom      -- The new coercion axiom introduced
-                                        -- by this family instance
-            , fi_flavor :: FamFlavor
-
-            -- Everything below here is a redundant, 
-            -- cached version of the two things above
-            , fi_fam   :: Name         -- Family name
-               -- INVARIANT: fi_fam = name of fi_fam_tc
-
-               -- Used for "rough matching"; same idea as for class instances
-                -- See Note [Rough-match field] in InstEnv
-           , fi_tcs   :: [Maybe Name]  -- Top of type args
-               -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
-
-               -- Used for "proper matching"; ditto
-           , fi_tvs    :: TyVarSet     -- Template tyvars for full match
-            , fi_fam_tc :: TyCon        -- Family tycon
-           , fi_tys    :: [Type]       --   and its arg types
-               -- INVARIANT: fi_tvs = coAxiomTyVars fi_axiom
-               --            (fi_fam_tc, fi_tys) = coAxiomSplitLHS fi_axiom
+data FamInst br -- See Note [FamInsts and CoAxioms], Note [Branched axioms] in CoAxiom
+  = FamInst { fi_axiom    :: CoAxiom br      -- The new coercion axiom introduced
+                                             -- by this family instance
+            , fi_flavor   :: FamFlavor
+            , fi_group    :: Bool            -- True <=> declared with "type instance where"
+                                             -- See Note [fi_group field]
+
+            -- Everything below here is a redundant,
+            -- cached version of the two things above,
+            -- except that the TyVars are freshened in the FamInstBranches
+            , fi_branches :: BranchList FamInstBranch br
+                                             -- Haskell-source-language view of 
+                                             -- a CoAxBranch
+            , fi_fam      :: Name            -- Family name
+                -- INVARIANT: fi_fam = name of fi_axiom.co_ax_tc
             }
 
+data FamInstBranch
+  = FamInstBranch
+    { fib_tvs    :: [TyVar]      -- Bound type variables
+                                 -- Like ClsInsts, these variables are always
+                                 -- fresh. See Note [Template tyvars are fresh]
+                                 -- in InstEnv
+    , fib_lhs    :: [Type]       -- type patterns
+    , fib_rhs    :: Type         -- RHS of family instance
+                                 -- See Note [Why we need fib_rhs]
+    , fib_tcs    :: [Maybe Name] -- used for "rough matching" during typechecking
+                                 -- see Note [Rough-match field] in InstEnv
+    }
+
 data FamFlavor 
   = SynFamilyInst         -- A synonym family
   | DataFamilyInst TyCon  -- A data family, with its representation TyCon
@@ -101,161 +147,171 @@ data FamFlavor
 
 \begin{code}
 -- Obtain the axiom of a family instance
-famInstAxiom :: FamInst -> CoAxiom
+famInstAxiom :: FamInst br -> CoAxiom br
 famInstAxiom = fi_axiom
 
-famInstLHS :: FamInst -> (TyCon, [Type])
-famInstLHS (FamInst { fi_fam_tc = tc, fi_tys = tys }) = (tc, tys)
+famInstTyCon :: FamInst br -> TyCon
+famInstTyCon = co_ax_tc . fi_axiom
+
+famInstNthBranch :: FamInst br -> Int -> FamInstBranch
+famInstNthBranch (FamInst { fi_branches = branches }) index
+  = ASSERT( 0 <= index && index < (length $ fromBranchList branches) )
+    brListNth branches index 
+
+famInstSingleBranch :: FamInst Unbranched -> FamInstBranch
+famInstSingleBranch (FamInst { fi_branches = FirstBranch branch }) = branch
+
+toBranchedFamInst :: FamInst br -> FamInst Branched
+toBranchedFamInst (FamInst ax flav grp branches fam)
+  = FamInst (toBranchedAxiom ax) flav grp (toBranchedList branches) fam
+
+toUnbranchedFamInst :: FamInst br -> FamInst Unbranched
+toUnbranchedFamInst (FamInst ax flav grp branches fam)
+  = FamInst (toUnbranchedAxiom ax) flav grp (toUnbranchedList branches) fam
+
+famInstBranches :: FamInst br -> BranchList FamInstBranch br
+famInstBranches = fi_branches
+
+famInstBranchLHS :: FamInstBranch -> [Type]
+famInstBranchLHS = fib_lhs
+
+famInstBranchRoughMatch :: FamInstBranch -> [Maybe Name]
+famInstBranchRoughMatch = fib_tcs
 
 -- Return the representation TyCons introduced by data family instances, if any
-famInstsRepTyCons :: [FamInst] -> [TyCon]
+famInstsRepTyCons :: [FamInst br] -> [TyCon]
 famInstsRepTyCons fis = [tc | FamInst { fi_flavor = DataFamilyInst tc } <- fis]
 
 -- Extracts the TyCon for this *data* (or newtype) instance
-famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
-famInstRepTyCon_maybe fi 
+famInstRepTyCon_maybe :: FamInst br -> Maybe TyCon
+famInstRepTyCon_maybe fi
   = case fi_flavor fi of
        DataFamilyInst tycon -> Just tycon
        SynFamilyInst        -> Nothing
 
-dataFamInstRepTyCon :: FamInst -> TyCon
-dataFamInstRepTyCon fi 
+dataFamInstRepTyCon :: FamInst br -> TyCon
+dataFamInstRepTyCon fi
   = case fi_flavor fi of
        DataFamilyInst tycon -> tycon
        SynFamilyInst        -> pprPanic "dataFamInstRepTyCon" (ppr fi)
-
-famInstTyVars :: FamInst -> TyVarSet
-famInstTyVars = fi_tvs
 \end{code}
 
+%************************************************************************
+%*                                                                      *
+        Pretty printing
+%*                                                                      *
+%************************************************************************
+
 \begin{code}
-instance NamedThing FamInst where
+instance NamedThing (FamInst br) where
    getName = coAxiomName . fi_axiom
 
-instance Outputable FamInst where
+instance Outputable (FamInst br) where
    ppr = pprFamInst
 
 -- Prints the FamInst as a family instance declaration
-pprFamInst :: FamInst -> SDoc
-pprFamInst famInst
-  = hang (pprFamInstHdr famInst)
-       2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> ppr ax)
-               , ifPprDebug (ptext (sLit "RHS:") <+> ppr (coAxiomRHS ax))
-               , ptext (sLit "--") <+> pprDefinedAt (getName famInst)])
-  where
-    ax = fi_axiom famInst
-
-pprFamInstHdr :: FamInst -> SDoc
-pprFamInstHdr (FamInst {fi_axiom = axiom, fi_flavor = flavor})
-  = pprTyConSort <+> pp_instance <+> pprHead
+pprFamInst :: FamInst br -> SDoc
+pprFamInst (FamInst { fi_branches = brs, fi_flavor = SynFamilyInst
+                    , fi_group = True, fi_axiom = axiom })
+  = hang (ptext (sLit "type instance where"))
+       2 (vcat [pprCoAxBranchHdr axiom i | i <- brListIndices brs])
+
+pprFamInst fi@(FamInst { fi_flavor = flavor
+                       , fi_group = False, fi_axiom = ax })
+  = pprFamFlavor flavor <+> pp_instance
+    <+> pprCoAxBranchHdr ax 0
   where
-    (fam_tc, tys) = coAxiomSplitLHS axiom 
-    
     -- For *associated* types, say "type T Int = blah" 
     -- For *top level* type instances, say "type instance T Int = blah"
     pp_instance 
-      | isTyConAssoc fam_tc = empty
-      | otherwise           = ptext (sLit "instance")
-
-    pprHead = pprTypeApp fam_tc tys
-    pprTyConSort = case flavor of
-                     SynFamilyInst        -> ptext (sLit "type")
-                     DataFamilyInst tycon
-                       | isDataTyCon     tycon -> ptext (sLit "data")
-                       | isNewTyCon      tycon -> ptext (sLit "newtype")
-                       | isAbstractTyCon tycon -> ptext (sLit "data")
-                       | otherwise             -> ptext (sLit "WEIRD") <+> ppr tycon
-
-pprFamInsts :: [FamInst] -> SDoc
+      | isTyConAssoc (famInstTyCon fi) = empty
+      | otherwise                      = ptext (sLit "instance")
+
+pprFamInst _ = panic "pprFamInst"
+
+pprFamFlavor :: FamFlavor -> SDoc
+pprFamFlavor flavor
+  = case flavor of
+      SynFamilyInst        -> ptext (sLit "type")
+      DataFamilyInst tycon
+        | isDataTyCon     tycon -> ptext (sLit "data")
+        | isNewTyCon      tycon -> ptext (sLit "newtype")
+        | isAbstractTyCon tycon -> ptext (sLit "data")
+        | otherwise             -> ptext (sLit "WEIRD") <+> ppr tycon
+
+pprFamInsts :: [FamInst br] -> SDoc
 pprFamInsts finsts = vcat (map pprFamInst finsts)
+\end{code}
 
--- | Create a coercion identifying a @type@ family instance.
--- It has the form @Co tvs :: F ts ~ R@, where @Co@ is 
--- the coercion constructor built here, @F@ the family tycon and @R@ the
--- right-hand side of the type family instance.
-mkSynFamInst :: Name       -- ^ Unique name for the coercion tycon
-             -> [TyVar]    -- ^ Type parameters of the coercion (@tvs@)
-             -> TyCon      -- ^ Family tycon (@F@)
-             -> [Type]     -- ^ Type instance (@ts@)
-             -> Type       -- ^ Representation tycon (@R@)
-             -> FamInst
-mkSynFamInst name tvs fam_tc inst_tys rep_ty
-  = FamInst { fi_fam    = tyConName fam_tc,
-              fi_fam_tc = fam_tc,
-              fi_tcs    = roughMatchTcs inst_tys,
-              fi_tvs    = mkVarSet tvs,
-              fi_tys    = inst_tys,
-              fi_flavor = SynFamilyInst,
-              fi_axiom  = axiom }
-  where
-    axiom = CoAxiom { co_ax_unique   = nameUnique name
-                    , co_ax_name     = name
-                    , co_ax_implicit = False
-                    , co_ax_tvs      = tvs
-                    , co_ax_lhs      = mkTyConApp fam_tc inst_tys 
-                    , co_ax_rhs      = rep_ty }
-
--- | Create a coercion identifying a @data@ or @newtype@ representation type
--- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@,
--- where @Co@ is the coercion constructor built here, @F@ the family tycon
--- and @R@ the (derived) representation tycon.
-mkDataFamInst :: Name         -- ^ Unique name for the coercion tycon
-              -> [TyVar]      -- ^ Type parameters of the coercion (@tvs@)
-              -> TyCon        -- ^ Family tycon (@F@)
-              -> [Type]       -- ^ Type instance (@ts@)
-              -> TyCon        -- ^ Representation tycon (@R@)
-              -> FamInst
-mkDataFamInst name tvs fam_tc inst_tys rep_tc
-  = FamInst { fi_fam    = tyConName fam_tc,
-              fi_fam_tc = fam_tc,
-              fi_tcs    = roughMatchTcs inst_tys,
-              fi_tvs    = mkVarSet tvs,
-              fi_tys    = inst_tys,
-              fi_flavor = DataFamilyInst rep_tc,
-              fi_axiom  = axiom }
-  where
-    axiom = CoAxiom { co_ax_unique   = nameUnique name
-                    , co_ax_name     = name
-                    , co_ax_implicit = False
-                    , co_ax_tvs      = tvs
-                    , co_ax_lhs      = mkTyConApp fam_tc inst_tys 
-                    , co_ax_rhs      = mkTyConApp rep_tc (mkTyVarTys tvs) }
+Note [Lazy axiom match]
+~~~~~~~~~~~~~~~~~~~~~~~
+It is Vitally Important that mkImportedFamInst is *lazy* in its axiom
+parameter. The axiom is loaded lazily, via a forkM, in TcIface. Sometime
+later, mkImportedFamInst is called using that axiom. However, the axiom
+may itself depend on entities which are not yet loaded as of the time
+of the mkImportedFamInst. Thus, if mkImportedFamInst eagerly looks at the
+axiom, a dependency loop spontaneously appears and GHC hangs. The solution
+is simply for mkImportedFamInst never, ever to look inside of the axiom
+until everything else is good and ready to do so. We can assume that this
+readiness has been achieved when some other code pulls on the axiom in the
+FamInst. Thus, we pattern match on the axiom lazily (in the where clause,
+not in the parameter list) and we assert the consistency of names there
+also.
+
+\begin{code}
 
 -- Make a family instance representation from the information found in an
 -- interface file.  In particular, we get the rough match info from the iface
 -- (instead of computing it here).
 mkImportedFamInst :: Name               -- Name of the family
-                  -> [Maybe Name]       -- Rough match info
-                  -> CoAxiom            -- Axiom introduced
-                  -> FamInst            -- Resulting family instance
-mkImportedFamInst fam mb_tcs axiom
+                  -> Bool               -- is this a group?
+                  -> [[Maybe Name]]     -- Rough match info, per branch
+                  -> CoAxiom Branched   -- Axiom introduced
+                  -> FamInst Branched   -- Resulting family instance
+mkImportedFamInst fam group roughs axiom
   = FamInst {
-      fi_fam    = fam,
-      fi_fam_tc = fam_tc,
-      fi_tcs    = mb_tcs,
-      fi_tvs    = mkVarSet . coAxiomTyVars $ axiom,
-      fi_tys    = tys,
-      fi_axiom  = axiom,
-      fi_flavor = flavor }
-  where 
-     (fam_tc, tys) = coAxiomSplitLHS axiom
+      fi_fam      = fam,
+      fi_axiom    = axiom,
+      fi_flavor   = flavor,
+      fi_group    = group,
+      fi_branches = branches }
+  where
+     -- Lazy match (See note [Lazy axiom match])
+     CoAxiom { co_ax_branches = axBranches }
+       = ASSERT( fam == tyConName (coAxiomTyCon axiom) )
+         axiom
+
+     branches = toBranchList $ map mk_imp_fam_inst_branch $ 
+                (roughs `zipLazy` fromBranchList axBranches)
+                -- Lazy zip (See note [Lazy axiom match])
+
+     mk_imp_fam_inst_branch (mb_tcs, ~(CoAxBranch { cab_tvs = tvs
+                                                  , cab_lhs = lhs
+                                                  , cab_rhs = rhs }))
+                -- Lazy match (See note [Lazy axiom match])
+       = FamInstBranch { fib_tvs    = tvs
+                       , fib_lhs    = lhs
+                       , fib_rhs    = rhs
+                       , fib_tcs    = mb_tcs }
 
          -- Derive the flavor for an imported FamInst rather disgustingly
          -- Maybe we should store it in the IfaceFamInst?
-     flavor = case splitTyConApp_maybe (coAxiomRHS axiom) of
-                Just (tc, _)
-                  | Just ax' <- tyConFamilyCoercion_maybe tc
-                  , ax' == axiom
-                  -> DataFamilyInst tc
-                _ -> SynFamilyInst
+     flavor
+       | FirstBranch (CoAxBranch { cab_rhs = rhs }) <- axBranches
+       , Just (tc, _) <- splitTyConApp_maybe rhs
+       , Just ax' <- tyConFamilyCoercion_maybe tc
+       , (toBranchedAxiom ax') == axiom
+       = DataFamilyInst tc
+
+       | otherwise
+       = SynFamilyInst
 \end{code}
 
 
-
 %************************************************************************
-%*                                                                     *
-               FamInstEnv
-%*                                                                     *
+%*                                                                      *
+                FamInstEnv
+%*                                                                      *
 %************************************************************************
 
 Note [FamInstEnv]
@@ -274,28 +330,25 @@ Neverthless it is still useful to have data families in the FamInstEnv:
  - For finding the representation type...see FamInstEnv.topNormaliseType
    and its call site in Simplify
 
- - In standalone deriving instance Eq (T [Int]) we need to find the 
+ - In standalone deriving instance Eq (T [Int]) we need to find the
    representation type for T [Int]
 
 \begin{code}
-type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
+type FamInstEnv = UniqFM FamilyInstEnv  -- Maps a family to its instances
      -- See Note [FamInstEnv]
 
 type FamInstEnvs = (FamInstEnv, FamInstEnv)
      -- External package inst-env, Home-package inst-env
 
-data FamilyInstEnv
-  = FamIE [FamInst]    -- The instances for a particular family, in any order
-         Bool          -- True <=> there is an instance of form T a b c
-                       --      If *not* then the common case of looking up
-                       --      (T a b c) can fail immediately
+newtype FamilyInstEnv
+  = FamIE [FamInst Branched] -- The instances for a particular family, in any order
 
 instance Outputable FamilyInstEnv where
-  ppr (FamIE fs b) = ptext (sLit "FamIE") <+> ppr b <+> vcat (map ppr fs)
+  ppr (FamIE fs) = ptext (sLit "FamIE") <+> vcat (map ppr fs)
 
 -- INVARIANTS:
 --  * The fs_tvs are distinct in each FamInst
---     of a range value of the map (so we can safely unify them)
+--      of a range value of the map (so we can safely unify them)
 
 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
@@ -303,69 +356,61 @@ emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
 emptyFamInstEnv :: FamInstEnv
 emptyFamInstEnv = emptyUFM
 
-famInstEnvElts :: FamInstEnv -> [FamInst]
-famInstEnvElts fi = [elt | FamIE elts <- eltsUFM fi, elt <- elts]
+famInstEnvElts :: FamInstEnv -> [FamInst Branched]
+famInstEnvElts fi = [elt | FamIE elts <- eltsUFM fi, elt <- elts]
 
-familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
+familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst Branched]
 familyInstances (pkg_fie, home_fie) fam
   = get home_fie ++ get pkg_fie
   where
     get env = case lookupUFM env fam of
-               Just (FamIE insts _) -> insts
-               Nothing              -> []
+                Just (FamIE insts) -> insts
+                Nothing            -> []
 
-extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
+extendFamInstEnvList :: FamInstEnv -> [FamInst br] -> FamInstEnv
 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
 
-extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
-extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
-  = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
+extendFamInstEnv :: FamInstEnv -> FamInst br -> FamInstEnv
+extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm})
+  = addToUFM_C add inst_env cls_nm (FamIE [ins_item_br])
   where
-    add (FamIE items tyvar) _ = FamIE (ins_item:items)
-                                     (ins_tyvar || tyvar)
-    ins_tyvar = not (any isJust mb_tcs)
-
-overwriteFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
-overwriteFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
-  = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
-  where
-    add (FamIE items tyvar) _ = FamIE (replaceFInst items)
-                                     (ins_tyvar || tyvar)
-    ins_tyvar = not (any isJust mb_tcs)
-    match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
-    
-    inst_axiom = famInstAxiom ins_item
-    (fam, tys) = coAxiomSplitLHS inst_axiom
-    arity = tyConArity fam
-    n_tys = length tys
-    match_tys 
-        | arity > n_tys = take arity tys
-        | otherwise     = tys
-    rough_tcs = roughMatchTcs match_tys
-    
-    replaceFInst [] = [ins_item]
-    replaceFInst (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, 
-                                  fi_tys = tpl_tys }) : rest)
-       -- Fast check for no match, uses the "rough match" fields
-      | instanceCantMatch rough_tcs mb_tcs
-      = item : replaceFInst rest
-
-        -- Proper check
-      | Just _ <- match item tpl_tvs tpl_tys match_tys
-      = ins_item : rest
-
-        -- No match => try next
-      | otherwise
-      = item : replaceFInst rest
-
-
-
+    ins_item_br = toBranchedFamInst ins_item
+    add (FamIE items) _ = FamIE (ins_item_br:items)
+
+deleteFromFamInstEnv :: FamInstEnv -> FamInst br -> FamInstEnv
+deleteFromFamInstEnv inst_env fam_inst@(FamInst {fi_fam = fam_nm})
+ = adjustUFM adjust inst_env fam_nm
+ where
+   adjust :: FamilyInstEnv -> FamilyInstEnv
+   adjust (FamIE items) = FamIE (filterOut (identicalFamInst fam_inst) items)
+
+identicalFamInst :: FamInst br1 -> FamInst br2 -> Bool
+-- Same LHS, *and* the instance is defined in the same module
+-- Used for overriding in GHCi
+identicalFamInst (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 })
+  =  nameModule (coAxiomName ax1) == nameModule (coAxiomName ax2)
+     && coAxiomTyCon ax1 == coAxiomTyCon ax2
+     && brListLength brs1 == brListLength brs2
+     && and (brListZipWith identical_ax_branch brs1 brs2)
+  where brs1 = coAxiomBranches ax1
+        brs2 = coAxiomBranches ax2
+        identical_ax_branch br1 br2
+          = length tvs1 == length tvs2
+            && length lhs1 == length lhs2
+            && and (zipWith (eqTypeX rn_env) lhs1 lhs2)
+          where
+            tvs1 = coAxBranchTyVars br1
+            tvs2 = coAxBranchTyVars br2
+            lhs1 = coAxBranchLHS br1
+            lhs2 = coAxBranchLHS br2
+            rn_env = rnBndrs2 (mkRnEnv2 emptyInScopeSet) tvs1 tvs2
+                       
 \end{code}
 
 %************************************************************************
-%*                                                                     *
-               Looking up a family instance
-%*                                                                     *
+%*                                                                      *
+                Looking up a family instance
+%*                                                                      *
 %************************************************************************
 
 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
@@ -385,174 +430,307 @@ desugared to
 
 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
 
+Note [Instance checking within groups]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Consider the following:
+
+type instance where
+  F Int = Bool
+  F a   = Int
+
+g :: Show a => a -> F a
+g x = length (show x)
+
+Should that type-check? No. We need to allow for the possibility
+that 'a' might be Int and therefore 'F a' should be Bool. We can
+simplify 'F a' to Int only when we can be sure that 'a' is not Int.
+
+To achieve this, after finding a possible match within an instance group, we
+have to go back to all previous FamInstBranchess and check that, under the
+substitution induced by the match, other matches are not possible. This is
+similar to what happens with class instance selection, when we need to
+guarantee that there is only a match and no unifiers. The exact algorithm is
+different here because the the potentially-overlapping group is closed.
+
+ALTERNATE APPROACH: As we are processing the branches, we could check if an
+instance unifies but does not match. If this happens, there is no possible
+match and we can fail right away. This might be more efficient.
+
+Note [Early failure optimisation for instance groups]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As we're searching through the instances for a match, it is
+possible that we find an branch within an instance that matches, but
+a previous branch still unifies. In this case, we can abort the
+search, because any other instance that matches will necessarily
+overlap with the instance group we're currently searching. Because
+overlap among instance groups is disallowed, we know that that
+no such other instance exists.
+
+Note [Confluence checking within groups]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC allows type family instances to have overlapping patterns as long as the
+right-hand sides are coincident in the region of overlap. Can we extend this
+notion of confluent overlap to branched instances? Not in any obvious way.
+
+Consider this:
+
+type instance where
+  F Int = Int
+  F a = a
+
+Without confluence checking (in other words, as implemented), we cannot now
+simplify an application of (F b) -- b might unify with Int later on, so this
+application is stuck. However, it would seem easy to just check that, in the
+region of overlap, (i.e. b |-> Int), the right-hand sides coincide, so we're
+OK. The problem happens when we are simplifying an application (F (G a)),
+where (G a) is stuck. What, now, is the region of overlap? We can't soundly
+simplify (F (G a)) without knowing that the right-hand sides are confluent
+in the region of overlap, but we also can't in any obvious way identify the
+region of overlap. We don't want to do analysis on the instances of G, because
+that is not sound in a world with open type families. (If G were known to be
+closed, there might be a way forward here.) To find the region of overlap,
+it is conceivable that we might convert (G a) to some fresh type variable and
+then unify, but we must be careful to convert every (G a) to the same fresh
+type variable. And then, what if there is an (H a) lying around? It all seems
+rather subtle, error-prone, confusing, and probably won't help anyone. So,
+we're not doing it.
+
+So, why is this not a problem with non-branched confluent overlap? Because
+we don't need to verify that an application is apart from anything. The
+non-branched confluent overlap check happens when we add the instance to the
+environment -- we're unifying among patterns, which cannot contain type family
+appplications. So, we're safe there and can continue supporting that feature.
+
 \begin{code}
-type FamInstMatch = (FamInst, [Type])           -- Matching type instance
-  -- See Note [Over-saturated matches]
+-- when matching a type family application, we get a FamInst,
+-- a 0-based index of the branch that matched, and the list of types
+-- the axiom should be applied to
+data FamInstMatch = FamInstMatch { fim_instance :: FamInst Branched
+                                 , fim_index    :: BranchIndex
+                                 , fim_tys      :: [Type]
+                                 }
+
+instance Outputable FamInstMatch where
+  ppr (FamInstMatch { fim_instance = inst
+                    , fim_index    = ind
+                    , fim_tys      = tys })
+    = ptext (sLit "match with") <+> parens (ppr inst)
+        <> brackets (ppr ind) <+> ppr tys
 
 lookupFamInstEnv
     :: FamInstEnvs
-    -> TyCon -> [Type]         -- What we are looking for
-    -> [FamInstMatch]          -- Successful matches
+    -> TyCon -> [Type]          -- What we are looking for
+    -> [FamInstMatch]           -- Successful matches
 -- Precondition: the tycon is saturated (or over-saturated)
 
 lookupFamInstEnv
-   = lookup_fam_inst_env match True
-   where
-     match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
+  = lookup_fam_inst_env match True
+  where
+    match :: MatchFun
+    match seen (FamInstBranch { fib_tvs = tpl_tvs
+                              , fib_lhs = tpl_tys })
+          _ match_tys 
+      = ASSERT( tyVarsOfTypes match_tys `disjointVarSet` tpl_tv_set )
+                -- Unification will break badly if the variables overlap
+                -- They shouldn't because we allocate separate uniques for them
+        case tcMatchTys tpl_tv_set tpl_tys match_tys of
+          -- success
+          Just subst
+            | checkConflict seen match_tys
+            -> (Nothing, StopSearching) -- we found an incoherence, so stop searching
+            -- see Note [Early failure optimisation for instance groups]
+
+            | otherwise
+            -> (Just subst, KeepSearching)
+
+          -- failure; instance not relevant
+          Nothing -> (Nothing, KeepSearching) 
+      where
+        tpl_tv_set = mkVarSet tpl_tvs
+
+    -- see Note [Instance checking within groups]
+    checkConflict :: [FamInstBranch] -- the previous branches in the instance that matched
+                  -> [Type]          -- the types in the tyfam application we are matching
+                  -> Bool            -- is there a conflict?
+    checkConflict [] _ = False
+    checkConflict ((FamInstBranch { fib_lhs = tpl_tys }) : rest) match_tys
+          -- see Note [Confluence checking within groups]
+      | SurelyApart <- tcApartTys instanceBindFun tpl_tys match_tys
+      = checkConflict rest match_tys
+      | otherwise
+      = True
 
 lookupFamInstEnvConflicts
     :: FamInstEnvs
-    -> FamInst         -- Putative new instance
-    -> [TyVar]         -- Unique tyvars, matching arity of FamInst
-    -> [FamInstMatch]  -- Conflicting matches
+    -> Bool             -- True <=> we are checking part of a group with other branches
+    -> TyCon            -- The TyCon of the family
+    -> FamInstBranch    -- the putative new instance branch
+    -> [FamInstMatch]   -- Conflicting branches
 -- 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
 --
 -- Precondition: the tycon is saturated (or over-saturated)
 
-lookupFamInstEnvConflicts envs fam_inst skol_tvs
-  = lookup_fam_inst_env my_unify False envs fam tys1
+lookupFamInstEnvConflicts envs grp tc
+                          (FamInstBranch { fib_lhs = tys, fib_rhs = rhs })
+  = lookup_fam_inst_env my_unify False envs tc tys
   where
-    inst_axiom = famInstAxiom fam_inst
-    (fam, tys) = famInstLHS fam_inst
-    skol_tys   = mkTyVarTys skol_tvs
-    tys1       = substTys (zipTopTvSubst (coAxiomTyVars inst_axiom) skol_tys) tys
-        -- In example above,   fam tys' = F [b]   
-
-    my_unify old_fam_inst tpl_tvs tpl_tys match_tys
-       = ASSERT2( tyVarsOfTypes tys1 `disjointVarSet` tpl_tvs,
-                 (ppr fam <+> ppr tys1) $$
-                 (ppr tpl_tvs <+> ppr tpl_tys) )
-               -- Unification will break badly if the variables overlap
-               -- They shouldn't because we allocate separate uniques for them
+    my_unify :: MatchFun
+    my_unify _ (FamInstBranch { fib_tvs = tpl_tvs, fib_lhs = tpl_tys
+                              , fib_rhs = tpl_rhs }) old_grp match_tys
+       = ASSERT( tyVarsOfTypes tys `disjointVarSet` mkVarSet tpl_tvs )
+                -- 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
-
-      -- Note [Family instance overlap conflicts]
-    conflicting old_fam_inst subst 
-      | isAlgTyCon fam = True
-      | otherwise      = not (old_rhs `eqType` new_rhs)
-      where
-        old_axiom = famInstAxiom old_fam_inst
-        old_tvs   = coAxiomTyVars old_axiom
-        old_rhs   = mkAxInstRHS old_axiom  (substTyVars subst old_tvs)
-        new_rhs   = mkAxInstRHS inst_axiom (substTyVars subst skol_tvs)
+              Just subst
+                |  isDataFamilyTyCon tc
+                || grp
+                || old_grp
+                || rhs_conflict tpl_rhs rhs subst
+                -> (Just subst, KeepSearching)
+                | otherwise -- confluent overlap
+                -> (Nothing, KeepSearching)
+              -- irrelevant instance
+              Nothing -> (Nothing, KeepSearching)
+
+    -- checks whether two RHSs are distinct, under a unifying substitution
+    -- Note [Family instance overlap conflicts]
+    rhs_conflict :: Type -> Type -> TvSubst -> Bool
+    rhs_conflict rhs1 rhs2 subst 
+      = not (rhs1' `eqType` rhs2')
+        where
+          rhs1' = substTy subst rhs1
+          rhs2' = substTy subst rhs2
 
 -- This variant is called when we want to check if the conflict is only in the
 -- home environment (see FamInst.addLocalFamInst)
-lookupFamInstEnvConflicts' :: FamInstEnv -> FamInst -> [TyVar] -> [FamInstMatch]
-lookupFamInstEnvConflicts' env fam_inst skol_tvs
-  = lookupFamInstEnvConflicts (emptyFamInstEnv, env) fam_inst skol_tvs
+lookupFamInstEnvConflicts' :: FamInstEnv -> Bool -> TyCon 
+                           -> FamInstBranch -> [FamInstMatch]
+lookupFamInstEnvConflicts' env
+  = lookupFamInstEnvConflicts (emptyFamInstEnv, env)
 \end{code}
 
+Note [lookup_fam_inst_env' implementation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+To reduce code duplication, both lookups during simplification and conflict
+checking are routed through lookup_fam_inst_env', which looks for a
+matching/unifying branch compared to some target. In the simplification
+case, the search is for a match for a target application; in the conflict-
+checking case, the search is for a unifier for a putative new instance branch.
+
+The two uses are differentiated by different MatchFuns, which look at a given
+branch to see if it is relevant and whether the search should continue. The
+the branch is relevant (i.e. matches or unifies), Just subst is
+returned; if the instance is not relevant, Nothing is returned. The MatchFun
+also indicates what the search algorithm should do next: it could
+KeepSearching or StopSearching.
+
+When to StopSearching? See Note [Early failure optimisation for instance groups]
+
+For class instances, these two variants of lookup are combined into one
+function (cf, @InstEnv@).  We don't do that for family instances as the
+results of matching and unification are used in two different contexts.
+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.
+
 Note [Family instance overlap conflicts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 - 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.  eg
+  the neither instance declares an instance group and the right-hand
+  sides of the overlapping rules coincide under the overlap substitution.
+  For example:
        type instance F a Int = a
        type instance F Int b = b
-  These two overlap on (F Int Int) but then both RHSs are Int, 
+  These two overlap on (F Int Int) but then both RHSs are Int,
   so all is well. We require that they are syntactically equal;
   anything else would be difficult to test for at this stage.
 
-
-While @lookupFamInstEnv@ uses a one-way match, the next function
-@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
-function (cf, @InstEnv@).  We don't do that for family instances as the
-results of matching and unification are used in two different contexts.
-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}
 ------------------------------------------------------------
+data ContSearch = KeepSearching
+                | StopSearching
+
 -- 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 MatchFun =  [FamInstBranch]     -- the previous branches in the instance
+              -> FamInstBranch       -- the individual branch to check
+              -> Bool                -- is this branch a part of a group?
+              -> [Type]              -- the types to match against
+              -> (Maybe TvSubst, ContSearch)
 
 type OneSidedMatch = Bool     -- Are optimisations that are only valid for
                               -- one sided matches allowed?
 
-lookup_fam_inst_env'         -- The worker, local to this module
+lookup_fam_inst_env'          -- The worker, local to this module
     :: MatchFun
     -> OneSidedMatch
     -> FamInstEnv
-    -> TyCon -> [Type]         -- What we are looking for
-    -> [FamInstMatch]          -- Successful matches
-lookup_fam_inst_env' match_fun one_sided ie fam tys
-  | not (isFamilyTyCon fam) 
-  = []
-  | otherwise
-  = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys )     -- Family type applications must be saturated
-    lookup ie
+    -> TyCon -> [Type]        -- What we are looking for
+    -> [FamInstMatch]
+lookup_fam_inst_env' match_fun _one_sided ie fam tys
+  | isFamilyTyCon fam
+  , Just (FamIE insts) <- lookupUFM ie fam
+  = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys ) 
+    if arity < n_tys then    -- Family type applications must be saturated
+                             -- See Note [Over-saturated matches]
+        map wrap_extra_tys (find match_fun (take arity tys) insts)
+    else
+        find match_fun tys insts    -- The common case
+
+  | otherwise = []
   where
-    -- 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
-
-    --------------
+    wrap_extra_tys fim@(FamInstMatch { fim_tys = match_tys })
+      = fim { fim_tys = match_tys ++ extra_tys }
+
+
+find :: MatchFun -> [Type] -> [FamInst Branched] -> [FamInstMatch]
+find _         _         [] = []
+find match_fun match_tys (inst@(FamInst { fi_branches = branches, fi_group = is_group }) : rest)
+  = case findBranch [] (fromBranchList branches) 0 of
+      (Just match, StopSearching) -> [match]
+      (Just match, KeepSearching) -> match : find match_fun match_tys rest
+      (Nothing,    StopSearching) -> []
+      (Nothing,    KeepSearching) -> find match_fun match_tys rest
+  where
     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
-                  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_axiom = axiom }) : rest)
-       -- Fast check for no match, uses the "rough match" fields
-      | instanceCantMatch rough_tcs mb_tcs
-      = find rest
 
-        -- Proper check
-      | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
-      = (item, add_extra_tys $ substTyVars subst (coAxiomTyVars axiom)) : find rest
-
-        -- No match => try next
+    findBranch :: [FamInstBranch]  -- the branches that have already been checked
+               -> [FamInstBranch]  -- still looking through these
+               -> BranchIndex      -- index of teh first of the "still looking" list
+               -> (Maybe FamInstMatch, ContSearch)
+    findBranch _ [] _ = (Nothing, KeepSearching)
+    findBranch seen (branch@(FamInstBranch { fib_tvs = tvs, fib_tcs = mb_tcs }) : rest) ind
+      | instanceCantMatch rough_tcs mb_tcs
+      = findBranch seen rest (ind+1) -- branch won't unify later; no need to add to 'seen'
       | otherwise
-      = find rest
--- Precondition: the tycon is saturated (or over-saturated)
-
-lookup_fam_inst_env          -- The worker, local to this module
+      = case match_fun seen branch is_group match_tys of
+          (Nothing, KeepSearching) -> findBranch (branch : seen) rest (ind+1)
+          (Nothing, StopSearching) -> (Nothing, StopSearching)
+          (Just subst, cont)       -> (Just match, cont)
+              where 
+                match = FamInstMatch { fim_instance = inst
+                                     , fim_index    = ind
+                                     , fim_tys      = substTyVars subst tvs }
+
+lookup_fam_inst_env           -- The worker, local to this module
     :: MatchFun
     -> OneSidedMatch
     -> FamInstEnvs
-    -> TyCon -> [Type]         -- What we are looking for
-    -> [FamInstMatch]          -- Successful matches
+    -> TyCon -> [Type]          -- What we are looking for
+    -> [FamInstMatch]           -- What was found
 
 -- Precondition: the tycon is saturated (or over-saturated)
-
 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys = 
     lookup_fam_inst_env' match_fun one_sided home_ie fam tys ++
     lookup_fam_inst_env' match_fun one_sided pkg_ie  fam tys
-
 \end{code}
 
 Note [Over-saturated matches]
@@ -565,28 +743,46 @@ 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 
+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.
 
+\begin{code}
 
+-- checks if one LHS is dominated by a list of other branches
+-- in other words, if an application would match the first LHS, it is guaranteed
+-- to match at least one of the others. The RHSs are ignored.
+-- This algorithm is conservative:
+--   True -> the LHS is definitely covered by the others
+--   False -> no information
+-- It is currently (Oct 2012) used only for generating errors for
+-- inaccessible branches. If these errors go unreported, no harm done.
+-- This is defined here to avoid a dependency from CoAxiom to Unify
+isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
+isDominatedBy branch branches
+  = or $ map match branches
+    where
+      lhs = coAxBranchLHS branch
+      match (CoAxBranch { cab_tvs = tvs, cab_lhs = tys })
+        = isJust $ tcMatchTys (mkVarSet tvs) tys lhs
+\end{code}
 
 
 %************************************************************************
-%*                                                                     *
-               Looking up a family instance
-%*                                                                     *
+%*                                                                      *
+                Looking up a family instance
+%*                                                                      *
 %************************************************************************
 
 \begin{code}
 topNormaliseType :: FamInstEnvs
-                -> Type
-                -> Maybe (Coercion, Type)
+                 -> Type
+                 -> Maybe (Coercion, Type)
 
--- Get rid of *outermost* (or toplevel) 
---     * type functions 
---     * newtypes
+-- 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
@@ -596,76 +792,74 @@ topNormaliseType :: FamInstEnvs
 -- Its a bit like Type.repType, but handles type families too
 
 topNormaliseType env ty
-  = go [] ty
+  = go emptyNameSet 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)
-        | isNewTyCon tc                -- Expand newtypes
-       = if tc `elem` rec_nts  -- See Note [Expanding newtypes] in Type.lhs
-         then Nothing
-          else let nt_co = mkAxInstCo (newTyConCo tc) tys
-               in add_co nt_co rec_nts' nt_rhs
-
-       | isFamilyTyCon tc              -- Expand open tycons
-       , (co, ty) <- normaliseTcApp env tc tys
-               -- Note that normaliseType fully normalises 'tys', 
-               -- It has do to so to be sure that nested calls like
-               --    F (G Int)
-               -- are correctly top-normalised
+    go :: NameSet -> Type -> Maybe (Coercion, Type)
+    go rec_nts ty 
+        | Just ty' <- coreView ty     -- Expand synonyms
+        = go rec_nts ty'
+
+        | Just (rec_nts', nt_co, nt_rhs) <- topNormaliseNewTypeX rec_nts ty
+        = add_co nt_co rec_nts' nt_rhs
+
+    go rec_nts (TyConApp tc tys) 
+        | isFamilyTyCon tc              -- Expand open tycons
+        , (co, ty) <- normaliseTcApp env tc tys
+                -- Note that normaliseType fully normalises 'tys',
+                -- wrt type functions but *not* newtypes
+                -- It has do to so to be sure that nested calls like
+                --    F (G Int)
+                -- are correctly top-normalised
         , not (isReflCo co)
         = add_co co rec_nts ty
-        where
-          nt_rhs = newTyConInstRhs tc tys
-          rec_nts' | isRecursiveTyCon tc = tc:rec_nts
-                   | otherwise           = rec_nts
 
     go _ _ = Nothing
 
-    add_co co rec_nts ty 
-       = case go rec_nts ty of
-               Nothing         -> Just (co, ty)
-               Just (co', ty') -> Just (mkTransCo co co', ty')
-        
+    add_co co rec_nts ty
+        = case go rec_nts ty of
+                Nothing         -> Just (co, ty)
+                Just (co', ty') -> Just (mkTransCo co co', ty')
+
 
 ---------------
 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type)
 normaliseTcApp env tc tys
   | isFamilyTyCon tc
-  , tyConArity tc <= length tys           -- Unsaturated data families are possible
-  , [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys 
+  , tyConArity tc <= length tys    -- Unsaturated data families are possible
+  , [FamInstMatch { fim_instance = fam_inst
+                  , fim_index    = fam_ind
+                  , fim_tys      = inst_tys }] <- lookupFamInstEnv env tc ntys 
   = let    -- A matching family instance exists
         ax              = famInstAxiom fam_inst
-        co              = mkAxInstCo  ax inst_tys
-        rhs             = mkAxInstRHS ax inst_tys
-       first_coi       = mkTransCo tycon_coi co
-       (rest_coi,nty)  = normaliseType env rhs
-       fix_coi         = mkTransCo first_coi rest_coi
+        co              = mkAxInstCo  ax fam_ind inst_tys
+        rhs             = mkAxInstRHS ax fam_ind inst_tys
+        first_coi       = mkTransCo tycon_coi co
+        (rest_coi,nty)  = normaliseType env rhs
+        fix_coi         = mkTransCo first_coi rest_coi
     in 
     (fix_coi, nty)
 
   | otherwise   -- No unique matching family instance exists;
-               -- we do not do anything
+                -- we do not do anything (including for newtypes)
   = (tycon_coi, TyConApp tc ntys)
 
   where
-       -- Normalise the arg types so that they'll match 
-       -- when we lookup in in the instance envt
+        -- 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    = mkTyConAppCo tc cois
 
 ---------------
-normaliseType :: FamInstEnvs           -- environment with family instances
-             -> Type                   -- old type
-             -> (Coercion, Type)       -- (coercion,new type), where
-                                       -- co :: old-type ~ new_type
+normaliseType :: FamInstEnvs            -- environment with family instances
+              -> Type                   -- old type
+              -> (Coercion, Type)       -- (coercion,new type), where
+                                        -- co :: old-type ~ new_type
 -- Normalise the input type, by eliminating *all* type-function redexes
 -- Returns with Refl if nothing happens
+-- Does nothing to newtypes
 
-normaliseType env ty 
-  | Just ty' <- coreView ty = normaliseType env ty' 
+normaliseType env ty
+  | Just ty' <- coreView ty = normaliseType env ty'
 normaliseType env (TyConApp tc tys)
   = normaliseTcApp env tc tys
 normaliseType _env ty@(LitTy {}) = (Refl ty, ty)