Revise implementation of overlapping type family instances.

This commit changes the syntax and story around overlapping type
family instances. Before, we had "unbranched" instances and
"branched" instances. Now, we have closed type families and
open ones.

The behavior of open families is completely unchanged. In particular,
coincident overlap of open type family instances still works, despite
emails to the contrary.

A closed type family is declared like this:
> type family F a where
>   F Int = Bool
>   F a   = Char
The equations are tried in order, from top to bottom, subject to
certain constraints, as described in the user manual. It is not
allowed to declare an instance of a closed family.

15 files changed, 299 insertions, 239 deletions

diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs
index 44a0cefac5..3f220b1339 100644
--- a/compiler/typecheck/FamInst.lhs
+++ b/compiler/typecheck/FamInst.lhs
@@ -35,6 +35,7 @@ import Maybes
 import TcMType
 import TcType
 import Name
+import VarSet -- RAE
 import Control.Monad
 import Data.Map (Map)
 import qualified Data.Map as Map
@@ -53,34 +54,27 @@ import qualified Data.Map as Map
 -- creates the fresh variables and applies the necessary substitution
 -- It is defined here to avoid a dependency from FamInstEnv on the monad
 -- code.
-newFamInst :: FamFlavor -> Bool -> CoAxiom br -> TcRnIf gbl lcl(FamInst br)
+
+newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst
 -- Freshen the type variables of the FamInst branches
 -- Called from the vectoriser monad too, hence the rather general type
-newFamInst flavor is_branched axiom@(CoAxiom { co_ax_tc       = fam_tc
-                                             , co_ax_branches = ax_branches })
-  = do { fam_branches <- go ax_branches
-       ; return (FamInst { fi_fam      = tyConName fam_tc
+newFamInst flavor axiom@(CoAxiom { co_ax_branches = FirstBranch branch
+                                 , co_ax_tc = fam_tc })
+  = do { (subst, tvs') <- tcInstSkolTyVarsLoc loc tvs
+       ; return (FamInst { fi_fam      = fam_tc_name
                          , fi_flavor   = flavor
-                         , fi_branches = fam_branches
-                         , fi_branched = is_branched
+                         , fi_tcs      = roughMatchTcs lhs
+                         , fi_tvs      = tvs'
+                         , fi_tys      = substTys subst lhs
+                         , fi_rhs      = substTy  subst rhs
                          , fi_axiom    = axiom }) }
   where
-    go :: BranchList CoAxBranch br -> TcRnIf gbl lcl (BranchList FamInstBranch br)
-    go (FirstBranch br) = do { br' <- go_branch br
-                             ; return (FirstBranch br') }
-    go (NextBranch br brs) = do { br' <- go_branch br
-                                ; brs' <- go brs
-                                ;return (NextBranch br' brs') }
-    go_branch :: CoAxBranch -> TcRnIf gbl lcl FamInstBranch 
-    go_branch (CoAxBranch { cab_tvs = tvs1
-                          , cab_lhs = lhs
-                          , cab_loc = loc
-                          , cab_rhs = rhs })
-       = do { (subst, tvs2) <- tcInstSkolTyVarsLoc loc tvs1
-            ; return (FamInstBranch { fib_tvs   = tvs2
-                                    , fib_lhs   = substTys subst lhs
-                                    , fib_rhs   = substTy  subst rhs
-                                    , fib_tcs   = roughMatchTcs lhs }) }
+    fam_tc_name = tyConName fam_tc
+    CoAxBranch { cab_loc = loc
+               , cab_tvs = tvs
+               , cab_lhs = lhs
+               , cab_rhs = rhs } = branch
+
 \end{code}
 
 
@@ -218,14 +212,14 @@ which implies that :R42T was declared as 'data instance T [a]'.
 \begin{code}
 tcLookupFamInst :: TyCon -> [Type] -> TcM (Maybe FamInstMatch)
 tcLookupFamInst tycon tys
-  | not (isFamilyTyCon tycon)
+  | not (isOpenFamilyTyCon tycon)
   = return Nothing
   | otherwise
   = do { instEnv <- tcGetFamInstEnvs
        ; let mb_match = lookupFamInstEnv instEnv tycon tys 
---       ; traceTc "lookupFamInst" ((ppr tycon <+> ppr tys) $$ 
---                                  pprTvBndrs (varSetElems (tyVarsOfTypes tys)) $$ 
---                                  ppr mb_match $$ ppr instEnv)
+       ; traceTc "lookupFamInst" ((ppr tycon <+> ppr tys) $$ 
+                                  pprTvBndrs (varSetElems (tyVarsOfTypes tys)) $$ 
+                                  ppr mb_match $$ ppr instEnv)
        ; case mb_match of
 	   [] -> return Nothing
 	   (match:_) 
@@ -242,7 +236,7 @@ tcLookupFamInst tycon tys
 
 \begin{code}
 -- Add new locally-defined family instances
-tcExtendLocalFamInstEnv :: [FamInst br] -> TcM a -> TcM a
+tcExtendLocalFamInstEnv :: [FamInst] -> TcM a -> TcM a
 tcExtendLocalFamInstEnv fam_insts thing_inside
  = do { env <- getGblEnv
       ; (inst_env', fam_insts') <- foldlM addLocalFamInst  
@@ -257,7 +251,7 @@ tcExtendLocalFamInstEnv fam_insts thing_inside
 -- and then add it to the home inst env
 -- This must be lazy in the fam_inst arguments, see Note [Lazy axiom match]
 -- in FamInstEnv.lhs
-addLocalFamInst :: (FamInstEnv,[FamInst Branched]) -> FamInst br -> TcM (FamInstEnv, [FamInst Branched])
+addLocalFamInst :: (FamInstEnv,[FamInst]) -> FamInst -> TcM (FamInstEnv, [FamInst])
 addLocalFamInst (home_fie, my_fis) fam_inst
         -- home_fie includes home package and this module
         -- my_fies is just the ones from this module
@@ -276,13 +270,12 @@ addLocalFamInst (home_fie, my_fis) fam_inst
            -- overlaps correctly
        ; eps <- getEps
        ; let inst_envs  = (eps_fam_inst_env eps, home_fie')
-             fam_inst'  = toBranchedFamInst fam_inst
-             home_fie'' = extendFamInstEnv home_fie fam_inst'
+             home_fie'' = extendFamInstEnv home_fie fam_inst
 
            -- Check for conflicting instance decls
-       ; no_conflict <- checkForConflicts inst_envs fam_inst'
+       ; no_conflict <- checkForConflicts inst_envs fam_inst
        ; if no_conflict then
-            return (home_fie'', fam_inst' : my_fis')
+            return (home_fie'', fam_inst : my_fis')
          else 
             return (home_fie,   my_fis) }
 
@@ -298,39 +291,35 @@ Check whether a single family instance conflicts with those in two instance
 environments (one for the EPS and one for the HPT).
 
 \begin{code}
-checkForConflicts :: FamInstEnvs -> FamInst Branched -> TcM Bool
-checkForConflicts inst_envs fam_inst@(FamInst { fi_branches = branches
-                                              , fi_branched = branched })
-  = do { let conflicts = brListMap (lookupFamInstEnvConflicts inst_envs branched fam_tc) branches
-             no_conflicts = all null conflicts
-       ; traceTc "checkForConflicts" (ppr conflicts $$ ppr fam_inst $$ ppr inst_envs)
-       ; unless no_conflicts $
-	   zipWithM_ (conflictInstErr fam_inst) (brListIndices branches) conflicts
+checkForConflicts :: FamInstEnvs -> FamInst -> TcM Bool
+checkForConflicts inst_envs fam_inst
+  = do { let conflicts = lookupFamInstEnvConflicts inst_envs fam_inst
+             no_conflicts = null conflicts
+       ; traceTc "checkForConflicts" (ppr (map fim_instance conflicts) $$
+                                      ppr fam_inst $$ ppr inst_envs)
+       ; unless no_conflicts $ conflictInstErr fam_inst conflicts
        ; return no_conflicts }
-    where fam_tc = famInstTyCon fam_inst
 
-conflictInstErr :: FamInst Branched -> BranchIndex -> [FamInstMatch] -> TcRn ()
-conflictInstErr fam_inst branch conflictingMatch
-  | (FamInstMatch { fim_instance = confInst
-                  , fim_index = confIndex }) : _ <- conflictingMatch
+conflictInstErr :: FamInst -> [FamInstMatch] -> TcRn ()
+conflictInstErr fam_inst conflictingMatch
+  | (FamInstMatch { fim_instance = confInst }) : _ <- conflictingMatch
   = addFamInstsErr (ptext (sLit "Conflicting family instance declarations:"))
-                   [(fam_inst, branch),
-                    (confInst, confIndex) ]
-  | otherwise -- no conflict on this branch; see Trac #7560
-  = return ()
+                   [fam_inst, confInst]
+  | otherwise 
+  = panic "conflictInstErr"
 
-addFamInstsErr :: SDoc -> [(FamInst Branched, Int)] -> TcRn ()
+addFamInstsErr :: SDoc -> [FamInst] -> TcRn ()
 addFamInstsErr herald insts
   = ASSERT( not (null insts) )
     setSrcSpan srcSpan $ addErr $
     hang herald
-       2 (vcat [ pprCoAxBranchHdr (famInstAxiom fi) index 
-               | (fi,index) <- sorted ])
+       2 (vcat [ pprCoAxBranchHdr (famInstAxiom fi) 0
+               | fi <- sorted ])
  where
-   getSpan   = getSrcLoc . famInstAxiom . fst
+   getSpan   = getSrcLoc . famInstAxiom
    sorted    = sortWith getSpan insts
-   (fi1,ix1) = head sorted
-   srcSpan   = coAxBranchSpan (coAxiomNthBranch (famInstAxiom fi1) ix1)
+   fi1       = head sorted
+   srcSpan   = coAxBranchSpan (coAxiomSingleBranch (famInstAxiom fi1))
    -- The sortWith just arranges that instances are dislayed in order
    -- of source location, which reduced wobbling in error messages,
    -- and is better for users
diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs
index ac2d81072a..21e2bbb5b9 100644
--- a/compiler/typecheck/TcDeriv.lhs
+++ b/compiler/typecheck/TcDeriv.lhs
@@ -46,7 +46,6 @@ import RdrName
 import Name
 import NameSet
 import TyCon
-import CoAxiom
 import TcType
 import Var
 import VarSet
@@ -355,7 +354,7 @@ tcDeriving tycl_decls inst_decls deriv_decls
   where
     ddump_deriving :: Bag (InstInfo Name) -> HsValBinds Name
                    -> Bag TyCon                 -- ^ Empty data constructors
-                   -> Bag (FamInst Unbranched)  -- ^ Rep type family instances
+                   -> Bag (FamInst)             -- ^ Rep type family instances
                    -> SDoc
     ddump_deriving inst_infos extra_binds repMetaTys repFamInsts
       =    hang (ptext (sLit "Derived instances:"))
@@ -370,12 +369,11 @@ tcDeriving tycl_decls inst_decls deriv_decls
     hangP s x = text "" $$ hang (ptext (sLit s)) 2 x
 
 -- Prints the representable type family instance
-pprRepTy :: FamInst Unbranched -> SDoc
-pprRepTy fi@(FamInst { fi_branches = FirstBranch (FamInstBranch { fib_lhs = lhs
-                                                                , fib_rhs = rhs }) })
+pprRepTy :: FamInst -> SDoc
+pprRepTy fi@(FamInst { fi_tys = lhs })
   = ptext (sLit "type") <+> ppr (mkTyConApp (famInstTyCon fi) lhs) <+>
-      equals <+> ppr rhs 
-
+      equals <+> ppr rhs
+  where rhs = famInstRHS fi
 
 -- As of 24 April 2012, this only shares MetaTyCons between derivations of
 -- Generic and Generic1; thus the types and logic are quite simple.
@@ -552,8 +550,9 @@ deriveFamInst decl@(DataFamInstDecl { dfid_tycon = L _ tc_name, dfid_pats = pats
                                     , dfid_defn = HsDataDefn { dd_derivs = Just preds } })
   = tcAddDataFamInstCtxt decl $
     do { fam_tc <- tcLookupTyCon tc_name
-       ; tcFamTyPats fam_tc pats (\_ -> return ()) $ \ tvs' pats' _ ->
-         mapM (deriveTyData tvs' fam_tc pats') preds }
+       ; tcFamTyPats tc_name (tyConKind fam_tc) pats (\_ -> return ()) $
+         \ tvs' pats' _ ->
+           mapM (deriveTyData tvs' fam_tc pats') preds }
         -- Tiresomely we must figure out the "lhs", which is awkward for type families
         -- E.g.   data T a b = .. deriving( Eq )
         --          Here, the lhs is (T a b)
@@ -744,10 +743,8 @@ mkEqnHelp orig tvs cls cls_tys tc_app mtheta
                 Nothing -> bale_out (ptext (sLit "No family instance for")
                                      <+> quotes (pprTypeApp tycon tys))
                 Just (FamInstMatch { fim_instance = famInst
-                                   , fim_index    = index
                                    , fim_tys      = tys })
-                  -> ASSERT( index == 0 )
-                     let tycon' = dataFamInstRepTyCon famInst
+                  -> let tycon' = dataFamInstRepTyCon famInst
                      in return (tycon', tys) }
 \end{code}
 
diff --git a/compiler/typecheck/TcEnv.lhs b/compiler/typecheck/TcEnv.lhs
index 528c06cbd5..058e84a22e 100644
--- a/compiler/typecheck/TcEnv.lhs
+++ b/compiler/typecheck/TcEnv.lhs
@@ -734,8 +734,9 @@ newGlobalBinder.
 newFamInstTyConName :: Located Name -> [Type] -> TcM Name
 newFamInstTyConName (L loc name) tys = mk_fam_inst_name id loc name [tys]
 
-newFamInstAxiomName :: SrcSpan -> Name -> [[Type]] -> TcM Name
-newFamInstAxiomName = mk_fam_inst_name mkInstTyCoOcc
+newFamInstAxiomName :: SrcSpan -> Name -> [CoAxBranch] -> TcM Name
+newFamInstAxiomName loc name branches
+  = mk_fam_inst_name mkInstTyCoOcc loc name (map coAxBranchLHS branches)
 
 mk_fam_inst_name :: (OccName -> OccName) -> SrcSpan -> Name -> [[Type]] -> TcM Name
 mk_fam_inst_name adaptOcc loc tc_name tyss
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index f58c466566..8615293a17 100644
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -1238,9 +1238,8 @@ tcTagToEnum loc fun_name arg res_ty
            ; case mb_fam of
                Nothing -> failWithTc (tagToEnumError ty doc3)
                Just (FamInstMatch { fim_instance = rep_fam
-                                  , fim_index    = index
                                   , fim_tys      = rep_args })
-                   -> return ( mkTcSymCo (mkTcAxInstCo co_tc index rep_args)
+                   -> return ( mkTcSymCo (mkTcUnbranchedAxInstCo co_tc rep_args)
                              , rep_tc, rep_args )
                  where
                    co_tc  = famInstAxiom rep_fam
diff --git a/compiler/typecheck/TcGenDeriv.lhs b/compiler/typecheck/TcGenDeriv.lhs
index 564756269e..77bda8274b 100644
--- a/compiler/typecheck/TcGenDeriv.lhs
+++ b/compiler/typecheck/TcGenDeriv.lhs
@@ -51,7 +51,6 @@ import PrelNames hiding (error_RDR)
 import PrimOp
 import SrcLoc
 import TyCon
-import CoAxiom
 import TcType
 import TysPrim
 import TysWiredIn
@@ -87,7 +86,7 @@ data DerivStuff     -- Please add this auxiliary stuff
 
   -- Generics
   | DerivTyCon TyCon                   -- New data types
-  | DerivFamInst (FamInst Unbranched)  -- New type family instances
+  | DerivFamInst (FamInst)             -- New type family instances
 
   -- New top-level auxiliary bindings
   | DerivHsBind (LHsBind RdrName, LSig RdrName) -- Also used for SYB
@@ -1916,7 +1915,7 @@ type SeparateBagsDerivStuff = -- AuxBinds and SYB bindings
                               ( Bag (LHsBind RdrName, LSig RdrName)
                                 -- Extra bindings (used by Generic only)
                               , Bag TyCon   -- Extra top-level datatypes
-                              , Bag (FamInst Unbranched) -- Extra family instances
+                              , Bag (FamInst)           -- Extra family instances
                               , Bag (InstInfo RdrName)) -- Extra instances
 
 genAuxBinds :: SrcSpan -> BagDerivStuff -> SeparateBagsDerivStuff
diff --git a/compiler/typecheck/TcGenGenerics.lhs b/compiler/typecheck/TcGenGenerics.lhs
index cd233751ff..f4765e9425 100644
--- a/compiler/typecheck/TcGenGenerics.lhs
+++ b/compiler/typecheck/TcGenGenerics.lhs
@@ -27,9 +27,7 @@ import TcType
 import TcGenDeriv
 import DataCon
 import TyCon
-import CoAxiom
-import Coercion         ( mkSingleCoAxiom )
-import FamInstEnv       ( FamInst, FamFlavor(..) )
+import FamInstEnv       ( FamInst, FamFlavor(..), mkSingleCoAxiom )
 import FamInst
 import Module           ( Module, moduleName, moduleNameString )
 import IfaceEnv         ( newGlobalBinder )
@@ -72,7 +70,7 @@ For the generic representation we need to generate:
 
 \begin{code}
 gen_Generic_binds :: GenericKind -> TyCon -> MetaTyCons -> Module
-                 -> TcM (LHsBinds RdrName, FamInst Unbranched)
+                 -> TcM (LHsBinds RdrName, FamInst)
 gen_Generic_binds gk tc metaTyCons mod = do
   repTyInsts <- tc_mkRepFamInsts gk tc metaTyCons mod
   return (mkBindsRep gk tc, repTyInsts)
@@ -404,7 +402,7 @@ tc_mkRepFamInsts :: GenericKind     -- Gen0 or Gen1
                -> TyCon           -- The type to generate representation for
                -> MetaTyCons      -- Metadata datatypes to refer to
                -> Module          -- Used as the location of the new RepTy
-               -> TcM (FamInst Unbranched) -- Generated representation0 coercion
+               -> TcM (FamInst)   -- Generated representation0 coercion
 tc_mkRepFamInsts gk tycon metaDts mod = 
        -- Consider the example input tycon `D`, where data D a b = D_ a
        -- Also consider `R:DInt`, where { data family D x y :: * -> *
@@ -445,7 +443,7 @@ tc_mkRepFamInsts gk tycon metaDts mod =
                         (nameSrcSpan (tyConName tycon))
 
      ; let axiom = mkSingleCoAxiom rep_name tyvars fam_tc appT repTy
-     ; newFamInst SynFamilyInst False axiom  }
+     ; newFamInst SynFamilyInst axiom  }
 
 --------------------------------------------------------------------------------
 -- Type representation
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index d810b0a2f8..c7d65a6b57 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -18,7 +18,7 @@ module TcHsType (
 	UserTypeCtxt(..), 
 
                 -- Type checking type and class decls
-	kcTyClTyVars, tcTyClTyVars,
+	kcLookupKind, kcTyClTyVars, tcTyClTyVars,
         tcHsConArgType, tcDataKindSig, 
         tcClassSigType, 
 
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index 753bc327be..2156bba9db 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -31,7 +31,6 @@ import TcRnMonad
 import TcValidity
 import TcMType
 import TcType
-import Coercion( mkSingleCoAxiom, mkBranchedCoAxiom, pprCoAxBranch )
 import BuildTyCl
 import Inst
 import InstEnv
@@ -455,7 +454,7 @@ addClsInsts :: [InstInfo Name] -> TcM a -> TcM a
 addClsInsts infos thing_inside
   = tcExtendLocalInstEnv (map iSpec infos) thing_inside
 
-addFamInsts :: [FamInst Branched] -> TcM a -> TcM a
+addFamInsts :: [FamInst] -> TcM a -> TcM a
 -- Extend (a) the family instance envt
 --        (b) the type envt with stuff from data type decls
 addFamInsts fam_insts thing_inside
@@ -465,7 +464,7 @@ addFamInsts fam_insts thing_inside
        ; tcg_env <- tcAddImplicits things
        ; setGblEnv tcg_env thing_inside }
   where
-    axioms = map famInstAxiom fam_insts
+    axioms = map (toBranchedAxiom . famInstAxiom) fam_insts
     tycons = famInstsRepTyCons fam_insts
     things = map ATyCon tycons ++ map ACoAxiom axioms 
 \end{code}
@@ -489,7 +488,7 @@ the brutal solution will do.
 
 \begin{code}
 tcLocalInstDecl :: LInstDecl Name
-                -> TcM ([InstInfo Name], [FamInst Branched])
+                -> TcM ([InstInfo Name], [FamInst])
         -- A source-file instance declaration
         -- Type-check all the stuff before the "where"
         --
@@ -500,13 +499,13 @@ tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl }))
 
 tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl }))
   = do { fam_inst <- tcDataFamInstDecl Nothing (L loc decl)
-       ; return ([], [toBranchedFamInst fam_inst]) }
+       ; return ([], [fam_inst]) }
 
 tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
   = do { (insts, fam_insts) <- tcClsInstDecl (L loc decl)
-       ; return (insts, map toBranchedFamInst fam_insts) }
+       ; return (insts, fam_insts) }
 
-tcClsInstDecl :: LClsInstDecl Name -> TcM ([InstInfo Name], [FamInst Unbranched])
+tcClsInstDecl :: LClsInstDecl Name -> TcM ([InstInfo Name], [FamInst])
 tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
                                   , cid_sigs = uprags, cid_tyfam_insts = ats
                                   , cid_datafam_insts = adts }))
@@ -533,7 +532,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
         ; let defined_ats = mkNameSet $ map (tyFamInstDeclName . unLoc) ats
               defined_adts = mkNameSet $ map (unLoc . dfid_tycon . unLoc) adts
 
-              mk_deflt_at_instances :: ClassATItem -> TcM [FamInst Unbranched]
+              mk_deflt_at_instances :: ClassATItem -> TcM [FamInst]
               mk_deflt_at_instances (fam_tc, defs)
                  -- User supplied instances ==> everything is OK
                 | tyConName fam_tc `elemNameSet` defined_ats
@@ -558,7 +557,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
                      ; rep_tc_name <- newFamInstTyConName (noLoc (tyConName fam_tc)) pat_tys'
                      ; let axiom = mkSingleCoAxiom rep_tc_name tvs' fam_tc pat_tys' rhs'
                      ; ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' ) 
-                       newFamInst SynFamilyInst False {- group -} axiom }
+                       newFamInst SynFamilyInst axiom }
 
         ; tyfam_insts1 <- mapM mk_deflt_at_instances (classATItems clas)
         
@@ -581,10 +580,10 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
 tcAssocTyDecl :: Class                   -- Class of associated type
               -> VarEnv Type             -- Instantiation of class TyVars
               -> LTyFamInstDecl Name     
-              -> TcM (FamInst Unbranched)
+              -> TcM (FamInst)
 tcAssocTyDecl clas mini_env ldecl
   = do { fam_inst <- tcTyFamInstDecl (Just (clas, mini_env)) ldecl
-       ; return $ toUnbranchedFamInst fam_inst }
+       ; return fam_inst }
 \end{code}
 
 %************************************************************************
@@ -620,14 +619,12 @@ tcFamInstDeclCombined mb_clsinfo fam_tc_lname
        ; return fam_tc }
 
 tcTyFamInstDecl :: Maybe (Class, VarEnv Type) -- the class & mini_env if applicable
-                -> LTyFamInstDecl Name -> TcM (FamInst Branched)
+                -> LTyFamInstDecl Name -> TcM FamInst
   -- "type instance"
-tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_group = group
-                                                      , tfid_eqns = eqns }))
+tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
   = setSrcSpan loc           $
     tcAddTyFamInstCtxt decl  $
-    do { let (eqn1:_) = eqns
-             fam_lname = tfie_tycon (unLoc eqn1)
+    do { let fam_lname = tfie_tycon (unLoc eqn)
        ; fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_lname
 
          -- (0) Check it's an open type family
@@ -637,36 +634,20 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_group = group
                  (notOpenFamily fam_tc)
 
          -- (1) do the work of verifying the synonym group
-       ; co_ax_branches <- tcSynFamInstDecl fam_tc decl
+       ; co_ax_branch <- tcSynFamInstDecl fam_tc decl
 
-         -- (2) check for validity and inaccessibility
-       ; foldlM_ (check_valid_branch fam_tc) [] co_ax_branches
+         -- (2) check for validity
+       ; checkValidTyFamInst mb_clsinfo fam_tc co_ax_branch
 
          -- (3) construct coercion axiom
        ; rep_tc_name <- newFamInstAxiomName loc
                                             (tyFamInstDeclName decl)
-                                            (map cab_lhs co_ax_branches)
-       ; let axiom = mkBranchedCoAxiom rep_tc_name fam_tc co_ax_branches
-       ; newFamInst SynFamilyInst group axiom }
-    where 
-      check_valid_branch :: TyCon
-                         -> [CoAxBranch]     -- previous
-                         -> CoAxBranch       -- current
-                         -> TcM [CoAxBranch] -- current : previous
-      check_valid_branch fam_tc prev_branches cur_branch
-        = do { -- Check the well-formedness of the instance
-               checkValidTyFamInst mb_clsinfo fam_tc cur_branch
-
-               -- Check whether the branch is dominated by earlier
-               -- ones and hence is inaccessible
-             ; when (cur_branch `isDominatedBy` prev_branches) $
-               setSrcSpan (coAxBranchSpan cur_branch) $
-               addErrTc $ inaccessibleCoAxBranch fam_tc cur_branch
-
-             ; return $ cur_branch : prev_branches }
+                                            [co_ax_branch]
+       ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
+       ; newFamInst SynFamilyInst axiom }
 
 tcDataFamInstDecl :: Maybe (Class, VarEnv Type)
-                  -> LDataFamInstDecl Name -> TcM (FamInst Unbranched)
+                  -> LDataFamInstDecl Name -> TcM FamInst
   -- "newtype instance" and "data instance"
 tcDataFamInstDecl mb_clsinfo 
     (L loc decl@(DataFamInstDecl
@@ -683,7 +664,7 @@ tcDataFamInstDecl mb_clsinfo
        ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)
 
          -- Kind check type patterns
-       ; tcFamTyPats fam_tc pats (kcDataDefn defn) $ 
+       ; tcFamTyPats (unLoc fam_tc_name) (tyConKind fam_tc) pats (kcDataDefn defn) $ 
            \tvs' pats' res_kind -> do
 
        { -- Check that left-hand side contains no type family applications
@@ -725,7 +706,7 @@ tcDataFamInstDecl mb_clsinfo
                  -- further instance might not introduce a new recursive
                  -- dependency.  (2) They are always valid loop breakers as
                  -- they involve a coercion.
-              ; fam_inst <- newFamInst (DataFamilyInst rep_tc) False axiom
+              ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
               ; return (rep_tc, fam_inst) }
 
          -- Remember to check validity; no recursion to worry about here
@@ -765,6 +746,8 @@ Solution: eta-reduce both axioms, thus:
 Now
    d' = d |> Monad (sym (ax2 ; ax1))
 
+This eta reduction happens both for data instances and newtype instances.
+
 See Note [Newtype eta] in TyCon.
 
 
@@ -1576,11 +1559,6 @@ badFamInstDecl tc_name
            quotes (ppr tc_name)
          , nest 2 (parens $ ptext (sLit "Use -XTypeFamilies to allow indexed type families")) ]
 
-inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
-inaccessibleCoAxBranch tc fi
-  = ptext (sLit "Inaccessible family instance equation:") $$
-      (pprCoAxBranch tc fi)
-
 notOpenFamily :: TyCon -> SDoc
 notOpenFamily tc
   = ptext (sLit "Illegal instance for closed family") <+> quotes (ppr tc)
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 42238a8769..27cf52e85e 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -20,7 +20,6 @@ import VarSet
 import Type
 import Unify
 import FamInstEnv
-import Coercion( mkAxInstRHS )
 
 import Var
 import TcType
@@ -1431,17 +1430,13 @@ doTopReactFunEq _ct fl fun_tc args xi loc
     do { match_res <- matchFam fun_tc args   -- See Note [MATCHING-SYNONYMS]
        ; case match_res of {
            Nothing -> return NoTopInt ;
-           Just (FamInstMatch { fim_instance = famInst
-                              , fim_index    = index
-                              , fim_tys      = rep_tys }) -> 
+           Just (co, ty) ->
 
     -- Found a top-level instance
     do {    -- Add it to the solved goals
          unless (isDerived fl) (addSolvedFunEq fam_ty fl xi)
 
-       ; let coe_ax = famInstAxiom famInst 
-       ; succeed_with "Fun/Top" (mkTcAxInstCo coe_ax index rep_tys)
-                      (mkAxInstRHS coe_ax index rep_tys) } } } } }
+       ; succeed_with "Fun/Top" co ty } } } } }
   where
     fam_ty = mkTyConApp fun_tc args
 
@@ -1709,17 +1704,17 @@ matchClassInst _ clas [ k, ty ] _
     case unwrapNewTyCon_maybe (classTyCon clas) of
       Just (_,dictRep, axDict)
         | Just tcSing <- tyConAppTyCon_maybe dictRep ->
-           do mbInst <- matchFam tcSing [k,ty]
+           do mbInst <- matchOpenFam tcSing [k,ty]
               case mbInst of
                 Just FamInstMatch
                   { fim_instance = FamInst { fi_axiom  = axDataFam
                                            , fi_flavor = DataFamilyInst tcon
                                            }
-                  , fim_index = ix, fim_tys = tys
+                  , fim_tys = tys
                   } | Just (_,_,axSing) <- unwrapNewTyCon_maybe tcon ->
 
                   do let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo axSing tys
-                         co2 = mkTcSymCo $ mkTcAxInstCo axDataFam ix tys
+                         co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDataFam tys
                          co3 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDict [k,ty]
                      return $ GenInst [] $ EvCast (EvLit evLit) $
                         mkTcTransCo co1 $ mkTcTransCo co2 co3
diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs
index 08590203a3..56cdf60afc 100644
--- a/compiler/typecheck/TcRnDriver.lhs
+++ b/compiler/typecheck/TcRnDriver.lhs
@@ -460,6 +460,7 @@ tcRnSrcDecls boot_iface decls
                                    tcg_fords    = fords' } } ;
 
         setGlobalTypeEnv tcg_env' final_type_env
+       
    } }
 
 tc_rn_src_decls :: ModDetails
@@ -487,7 +488,7 @@ tc_rn_src_decls boot_details ds
         case group_tail of {
            Nothing -> do { tcg_env <- checkMain ;       -- Check for `main'
                            traceTc "returning from tc_rn_src_decls: " $
-                             ppr $ nameEnvElts $ tcg_type_env tcg_env ; -- RAE
+                             ppr $ nameEnvElts $ tcg_type_env tcg_env ;
                            return (tcg_env, tcl_env)
                       } ;
 
@@ -769,8 +770,9 @@ checkBootTyCon tc1 tc2
   , Just syn_rhs2 <- synTyConRhs_maybe tc2
   , Just env <- eqTyVarBndrs emptyRnEnv2 (tyConTyVars tc1) (tyConTyVars tc2)
   = ASSERT(tc1 == tc2)
-    let eqSynRhs (SynFamilyTyCon o1 i1) (SynFamilyTyCon o2 i2)
-            = o1==o2 && i1==i2
+    let eqSynRhs OpenSynFamilyTyCon OpenSynFamilyTyCon = True
+        eqSynRhs (ClosedSynFamilyTyCon ax1) (ClosedSynFamilyTyCon ax2)
+            = ax1 == ax2
         eqSynRhs (SynonymTyCon t1) (SynonymTyCon t2)
             = eqTypeX env t1 t2
         eqSynRhs _ _ = False
@@ -956,7 +958,6 @@ tcTopSrcDecls boot_details
                                  -- tcg_dus: see Note [Newtype constructor usage in foreign declarations]
 
         addUsedRdrNames fo_rdr_names ;
-        traceTc "Tc8: type_env: " (ppr $ nameEnvElts $ tcg_type_env tcg_env') ; -- RAE
         return (tcg_env', tcl_env)
     }}}}}}
   where
@@ -1654,13 +1655,8 @@ tcRnDeclsi hsc_env ictxt local_decls =
                              tcg_vects     = vects',
                              tcg_fords     = fords' }
 
-    tcg_env'' <- setGlobalTypeEnv tcg_env' final_type_env
-
-    traceTc "returning from tcRnDeclsi: " $ ppr $ nameEnvElts $ tcg_type_env tcg_env'' -- RAE
-
-    return tcg_env''
-
-
+    setGlobalTypeEnv tcg_env' final_type_env
+    
 #endif /* GHCi */
 \end{code}
 
@@ -1738,7 +1734,7 @@ tcRnLookupName' name = do
 
 tcRnGetInfo :: HscEnv
             -> Name
-            -> IO (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst Branched]))
+            -> IO (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst]))
 
 -- Used to implement :info in GHCi
 --
@@ -1763,13 +1759,13 @@ tcRnGetInfo hsc_env name
     (cls_insts, fam_insts) <- lookupInsts thing
     return (thing, fixity, cls_insts, fam_insts)
 
-lookupInsts :: TyThing -> TcM ([ClsInst],[FamInst Branched])
+lookupInsts :: TyThing -> TcM ([ClsInst],[FamInst])
 lookupInsts (ATyCon tc)
   | Just cls <- tyConClass_maybe tc
   = do  { inst_envs <- tcGetInstEnvs
         ; return (classInstances inst_envs cls, []) }
 
-  | isFamilyTyCon tc || isTyConAssoc tc
+  | isOpenFamilyTyCon tc || isTyConAssoc tc
   = do  { inst_envs <- tcGetFamInstEnvs
         ; return ([], familyInstances inst_envs tc) }
 
@@ -1901,7 +1897,7 @@ ppr_types insts type_env
         -- that the type checker has invented.  Top-level user-defined things
         -- have External names.
 
-ppr_tycons :: [FamInst br] -> TypeEnv -> SDoc
+ppr_tycons :: [FamInst] -> TypeEnv -> SDoc
 ppr_tycons fam_insts type_env
   = vcat [ text "TYPE CONSTRUCTORS"
          ,   nest 2 (ppr_tydecls tycons)
@@ -1919,7 +1915,7 @@ ppr_insts :: [ClsInst] -> SDoc
 ppr_insts []     = empty
 ppr_insts ispecs = text "INSTANCES" $$ nest 2 (pprInstances ispecs)
 
-ppr_fam_insts :: [FamInst br] -> SDoc
+ppr_fam_insts :: [FamInst] -> SDoc
 ppr_fam_insts []        = empty
 ppr_fam_insts fam_insts =
   text "FAMILY INSTANCES" $$ nest 2 (pprFamInsts fam_insts)
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index b53c40d358..43b4f36aa2 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -298,7 +298,7 @@ data TcGblEnv
         tcg_anns      :: [Annotation],      -- ...Annotations
         tcg_tcs       :: [TyCon],           -- ...TyCons and Classes
         tcg_insts     :: [ClsInst],         -- ...Instances
-        tcg_fam_insts :: [FamInst Branched],-- ...Family instances
+        tcg_fam_insts :: [FamInst],         -- ...Family instances
         tcg_rules     :: [LRuleDecl Id],    -- ...Rules
         tcg_fords     :: [LForeignDecl Id], -- ...Foreign import & exports
         tcg_vects     :: [LVectDecl Id],    -- ...Vectorisation declarations
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 930444a1ba..9a7049fcca 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -86,7 +86,7 @@ module TcSMonad (
 
     getDefaultInfo, getDynFlags,
 
-    matchClass, matchFam, MatchInstResult (..), 
+    matchClass, matchFam, matchOpenFam, MatchInstResult (..), 
     checkWellStagedDFun, 
     pprEq                                    -- Smaller utils, re-exported from TcM
                                              -- TODO (DV): these are only really used in the 
@@ -132,6 +132,7 @@ import TcRnTypes
 import Unique 
 import UniqFM
 import Maybes ( orElse, catMaybes, firstJust )
+import Pair ( pSnd )
 
 import Control.Monad( unless, when, zipWithM )
 import Data.IORef
@@ -1674,8 +1675,30 @@ matchClass clas tys
 	}
         }
 
-matchFam :: TyCon -> [Type] -> TcS (Maybe FamInstMatch)
-matchFam tycon args = wrapTcS $ tcLookupFamInst tycon args
+matchOpenFam :: TyCon -> [Type] -> TcS (Maybe FamInstMatch)
+matchOpenFam tycon args = wrapTcS $ tcLookupFamInst tycon args
+
+matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
+matchFam tycon args
+  | isOpenSynFamilyTyCon tycon
+  = do { maybe_match <- matchOpenFam tycon args
+       ; case maybe_match of
+           Nothing -> return Nothing
+           Just (FamInstMatch { fim_instance = famInst
+                              , fim_tys      = inst_tys })
+             -> let co = mkTcUnbranchedAxInstCo (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 ax ind inst_tys
+        ty = pSnd (tcCoercionKind co)
+    in return $ Just (co, ty)
+
+  | otherwise
+  = return Nothing
+       
 \end{code}
 
 \begin{code}
diff --git a/compiler/typecheck/TcSplice.lhs b/compiler/typecheck/TcSplice.lhs
index 2561bd967c..59b06d4a8e 100644
--- a/compiler/typecheck/TcSplice.lhs
+++ b/compiler/typecheck/TcSplice.lhs
@@ -1027,7 +1027,7 @@ reifyInstances th_nm th_tys
                -> do { inst_envs <- tcGetInstEnvs
                      ; let (matches, unifies, _) = lookupInstEnv inst_envs cls tys
                      ; mapM reifyClassInstance (map fst matches ++ unifies) }
-               | isFamilyTyCon tc
+               | isOpenFamilyTyCon tc
                -> do { inst_envs <- tcGetFamInstEnvs
                      ; let matches = lookupFamInstEnv inst_envs tc tys
                      ; mapM (reifyFamilyInstance . fim_instance) matches }
@@ -1169,7 +1169,6 @@ reifyThing (AGlobal (AnId id))
     }
 
 reifyThing (AGlobal (ATyCon tc))   = reifyTyCon tc
-reifyThing (AGlobal (ACoAxiom ax)) = reifyAxiom ax
 reifyThing (AGlobal (ADataCon dc))
   = do  { let name = dataConName dc
         ; ty <- reifyType (idType (dataConWrapId dc))
@@ -1192,12 +1191,7 @@ reifyThing (ATyVar tv tv1)
 
 reifyThing thing = pprPanic "reifyThing" (pprTcTyThingCategory thing)
 
-------------------------------
-reifyAxiom :: CoAxiom br -> TcM TH.Info
-reifyAxiom (CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
-  = do { eqns <- sequence $ brListMap reifyAxBranch branches
-       ; return (TH.TyConI (TH.TySynInstD (reifyName tc) eqns)) }
-
+-------------------------------------------
 reifyAxBranch :: CoAxBranch -> TcM TH.TySynEqn
 reifyAxBranch (CoAxBranch { cab_lhs = args, cab_rhs = rhs })
   = do { args' <- mapM reifyType args
@@ -1216,18 +1210,24 @@ reifyTyCon tc
   = return (TH.PrimTyConI (reifyName tc) (tyConArity tc) (isUnLiftedTyCon tc))
 
   | isFamilyTyCon tc
-  = do { let flavour = reifyFamFlavour tc
-             tvs     = tyConTyVars tc
+  = do { let tvs     = tyConTyVars tc
              kind    = tyConKind tc
        ; kind' <- if isLiftedTypeKind kind then return Nothing
                   else fmap Just (reifyKind kind)
 
-       ; fam_envs <- tcGetFamInstEnvs
-       ; instances <- mapM reifyFamilyInstance (familyInstances fam_envs tc)
        ; tvs' <- reifyTyVars tvs
-       ; return (TH.FamilyI
-                    (TH.FamilyD flavour (reifyName tc) tvs' kind')
-                    instances) }
+       ; flav' <- reifyFamFlavour tc
+       ; case flav' of
+         { Left flav ->  -- open type/data family
+             do { fam_envs <- tcGetFamInstEnvs
+                ; instances <- mapM reifyFamilyInstance (familyInstances fam_envs tc)
+                ; return (TH.FamilyI
+                            (TH.FamilyD flav (reifyName tc) tvs' kind')
+                            instances) }
+         ; Right eqns -> -- closed type family
+             return (TH.FamilyI
+                      (TH.ClosedTypeFamilyD (reifyName tc) tvs' kind' eqns)
+                      []) } }
 
   | Just (tvs, rhs) <- synTyConDefn_maybe tc  -- Vanilla type synonym
   = do { rhs' <- reifyType rhs
@@ -1308,31 +1308,26 @@ reifyClassInstance i
      n_silent = dfunNSilent dfun
 
 ------------------------------
-reifyFamilyInstance :: FamInst br -> TcM TH.Dec
-reifyFamilyInstance fi@(FamInst { fi_flavor = flavor
-                                , fi_branches = branches
-                                , fi_fam = fam })
+reifyFamilyInstance :: FamInst -> TcM TH.Dec
+reifyFamilyInstance (FamInst { fi_flavor = flavor 
+                             , fi_fam = fam
+                             , fi_tys = lhs
+                             , fi_rhs = rhs })
   = case flavor of
       SynFamilyInst ->
-        do { th_eqns <- sequence $ brListMap reifyFamInstBranch branches
-           ; return (TH.TySynInstD (reifyName fam) th_eqns) }
+        do { th_lhs <- reifyTypes lhs
+           ; th_rhs <- reifyType  rhs
+           ; return (TH.TySynInstD (reifyName fam) (TH.TySynEqn th_lhs th_rhs)) }
 
       DataFamilyInst rep_tc ->
         do { let tvs = tyConTyVars rep_tc
                  fam' = reifyName fam
-                 lhs = famInstBranchLHS $ famInstSingleBranch (toUnbranchedFamInst fi)
            ; cons <- mapM (reifyDataCon (mkTyVarTys tvs)) (tyConDataCons rep_tc)
            ; th_tys <- reifyTypes lhs
            ; return (if isNewTyCon rep_tc
                      then TH.NewtypeInstD [] fam' th_tys (head cons) []
                      else TH.DataInstD    [] fam' th_tys cons        []) }
 
-reifyFamInstBranch :: FamInstBranch -> TcM TH.TySynEqn
-reifyFamInstBranch (FamInstBranch { fib_lhs = lhs, fib_rhs = rhs })
-  = do { th_lhs <- reifyTypes lhs
-       ; th_rhs <- reifyType rhs
-       ; return (TH.TySynEqn th_lhs th_rhs) }
-
 ------------------------------
 reifyType :: TypeRep.Type -> TcM TH.Type
 -- Monadic only because of failure
@@ -1394,11 +1389,17 @@ reifyCxt   = mapM reifyPred
 reifyFunDep :: ([TyVar], [TyVar]) -> TH.FunDep
 reifyFunDep (xs, ys) = TH.FunDep (map reifyName xs) (map reifyName ys)
 
-reifyFamFlavour :: TyCon -> TH.FamFlavour
-reifyFamFlavour tc | isSynFamilyTyCon tc = TH.TypeFam
-                   | isFamilyTyCon    tc = TH.DataFam
-                   | otherwise
-                   = panic "TcSplice.reifyFamFlavour: not a type family"
+reifyFamFlavour :: TyCon -> TcM (Either TH.FamFlavour [TH.TySynEqn])
+reifyFamFlavour tc
+  | isOpenSynFamilyTyCon tc = return $ Left TH.TypeFam
+  | isDataFamilyTyCon    tc = return $ Left TH.DataFam
+
+  | Just ax <- isClosedSynFamilyTyCon_maybe tc
+  = do { eqns <- brListMapM reifyAxBranch $ coAxiomBranches ax
+       ; return $ Right eqns }
+                   
+  | otherwise
+  = panic "TcSplice.reifyFamFlavour: not a type family"
 
 reifyTyVars :: [TyVar] -> TcM [TH.TyVarBndr]
 reifyTyVars = mapM reifyTyVar . filter isTypeVar
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index 41cbeae349..044086d937 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -37,11 +37,12 @@ import TcMType
 import TcType
 import TysWiredIn( unitTy )
 import FamInst
-import Coercion( mkCoAxBranch )
+import FamInstEnv( isDominatedBy, mkCoAxBranch, mkBranchedCoAxiom )
+import Coercion( pprCoAxBranch )
 import Type
 import Kind
 import Class
-import CoAxiom( CoAxBranch(..) )
+import CoAxiom
 import TyCon
 import DataCon
 import Id
@@ -648,16 +649,53 @@ tcTyClDecl1 _ _
 \begin{code}
 tcFamDecl1 :: TyConParent -> FamilyDecl Name -> TcM [TyThing]
 tcFamDecl1 parent
-            (FamilyDecl {fdFlavour = TypeFamily, fdLName = L _ tc_name, fdTyVars = tvs})
+            (FamilyDecl {fdInfo = OpenTypeFamily, fdLName = L _ tc_name, fdTyVars = tvs})
   = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
-  { traceTc "type family:" (ppr tc_name)
+  { traceTc "open type family:" (ppr tc_name)
   ; checkFamFlag tc_name
-  ; let syn_rhs = SynFamilyTyCon { synf_open = True, synf_injective = False }
-  ; tycon <- buildSynTyCon tc_name tvs' syn_rhs kind parent
+  ; tycon <- buildSynTyCon tc_name tvs' OpenSynFamilyTyCon kind parent
   ; return [ATyCon tycon] }
 
 tcFamDecl1 parent
-           (FamilyDecl {fdFlavour = DataFamily, fdLName = L _ tc_name, fdTyVars = tvs})
+            (FamilyDecl { fdInfo = ClosedTypeFamily eqns
+                        , fdLName = lname@(L _ tc_name), fdTyVars = tvs })
+-- Closed type families are a little tricky, because they contain the definition
+-- of both the type family and the equations for a CoAxiom.
+  = do { traceTc "closed type family:" (ppr tc_name)
+         -- the variables in the header have no scope:
+       ; (tvs', kind) <- tcTyClTyVars tc_name tvs $ \ tvs' kind ->
+                         return (tvs', kind)
+
+       ; checkFamFlag tc_name -- make sure we have -XTypeFamilies
+
+         -- check to make sure all the names used in the equations are
+         -- consistent
+       ; let names = map (tfie_tycon . unLoc) eqns
+       ; tcSynFamInstNames lname names
+
+         -- process the equations, creating CoAxBranches
+       ; tycon_kind <- kcLookupKind tc_name
+       ; branches <- mapM (tcTyFamInstEqn tc_name tycon_kind) eqns
+
+         -- we need the tycon that we will be creating, but it's in scope.
+         -- just look it up.
+       ; fam_tc <- tcLookupLocatedTyCon lname
+
+         -- create a CoAxiom, with the correct src location
+       ; loc <- getSrcSpanM
+       ; co_ax_name <- newFamInstAxiomName loc tc_name branches
+       ; let co_ax = mkBranchedCoAxiom co_ax_name fam_tc branches
+
+         -- now, finally, build the TyCon
+       ; let syn_rhs = ClosedSynFamilyTyCon co_ax
+       ; tycon <- buildSynTyCon tc_name tvs' syn_rhs kind parent
+
+       ; return [ATyCon tycon, ACoAxiom co_ax] }
+-- We check for instance validity later, when doing validity checking for
+-- the tycon
+
+tcFamDecl1 parent
+           (FamilyDecl {fdInfo = DataFamily, fdLName = L _ tc_name, fdTyVars = tvs})
   = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
   { traceTc "data family:" (ppr tc_name)
   ; checkFamFlag tc_name
@@ -770,13 +808,13 @@ tcClassATs class_name parent ats at_defs
     tc_at at = do { [ATyCon fam_tc] <- addLocM (tcFamDecl1 parent) at
                   ; let at_defs = lookupNameEnv at_defs_map (unLoc $ fdLName $ unLoc at)
                                         `orElse` []
-                  ; atd <- concatMapM (tcDefaultAssocDecl fam_tc) at_defs
+                  ; atd <- mapM (tcDefaultAssocDecl fam_tc) at_defs
                   ; return (fam_tc, atd) }
 
 -------------------------
 tcDefaultAssocDecl :: TyCon                -- ^ Family TyCon
                    -> LTyFamInstDecl Name  -- ^ RHS
-                   -> TcM [CoAxBranch]     -- ^ Type checked RHS and free TyVars
+                   -> TcM CoAxBranch       -- ^ Type checked RHS and free TyVars
 tcDefaultAssocDecl fam_tc (L loc decl)
   = setSrcSpan loc $
     tcAddTyFamInstCtxt decl $
@@ -785,17 +823,12 @@ tcDefaultAssocDecl fam_tc (L loc decl)
     -- We check for well-formedness and validity later, in checkValidClass
 
 -------------------------
-tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM [CoAxBranch]
+tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM CoAxBranch
 -- Placed here because type family instances appear as
 -- default decls in class declarations
-tcSynFamInstDecl fam_tc (TyFamInstDecl { tfid_eqns = eqns })
-  -- we know the first equation matches the fam_tc because of the lookup logic
-  -- now, just check that all other names match the first
-  = do { let names = map (tfie_tycon . unLoc) eqns
-             first = head names
-       ; tcSynFamInstNames first names
-       ; checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
-       ; mapM (tcTyFamInstEqn fam_tc) eqns }
+tcSynFamInstDecl fam_tc (TyFamInstDecl { tfid_eqn = eqn })
+  = do { checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
+       ; tcTyFamInstEqn (tyConName fam_tc) (tyConKind fam_tc) eqn }
 
 -- Checks to make sure that all the names in an instance group are the same
 tcSynFamInstNames :: Located Name -> [Located Name] -> TcM ()
@@ -808,15 +841,15 @@ tcSynFamInstNames (L _ first) names
       = setSrcSpan loc $
         failWithTc (msg_fun name)
 
-tcTyFamInstEqn :: TyCon -> LTyFamInstEqn Name -> TcM CoAxBranch
-tcTyFamInstEqn fam_tc
+tcTyFamInstEqn :: Name -> Kind -> LTyFamInstEqn Name -> TcM CoAxBranch
+tcTyFamInstEqn fam_tc_name kind
     (L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
   = setSrcSpan loc $
-    tcFamTyPats fam_tc pats (discardResult . (tcCheckLHsType hs_ty)) $
+    tcFamTyPats fam_tc_name kind pats (discardResult . (tcCheckLHsType hs_ty)) $
        \tvs' pats' res_kind ->
     do { rhs_ty <- tcCheckLHsType hs_ty res_kind
        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
-       ; traceTc "tcSynFamInstEqn" (ppr fam_tc <+> (ppr tvs' $$ ppr pats' $$ ppr rhs_ty))
+       ; traceTc "tcSynFamInstEqn" (ppr fam_tc_name <+> (ppr tvs' $$ ppr pats' $$ ppr rhs_ty))
        ; return (mkCoAxBranch tvs' pats' rhs_ty loc) }
 
 kcDataDefn :: HsDataDefn Name -> TcKind -> TcM ()
@@ -846,7 +879,11 @@ kcResultKind (Just k) res_k
 --   check is only required for type synonym instances.
 
 -----------------
-tcFamTyPats :: TyCon
+-- Note that we can't use the family TyCon, because this is sometimes called
+-- from within a type-checking knot. So, we ask our callers to do a little more
+-- work.
+tcFamTyPats :: Name -- of the family TyCon
+            -> Kind -- of the family TyCon
             -> HsWithBndrs [LHsType Name] -- Patterns
             -> (TcKind -> TcM ())       -- Kind checker for RHS
                                         -- result is ignored
@@ -863,23 +900,27 @@ tcFamTyPats :: TyCon
 -- In that case, the type variable 'a' will *already be in scope*
 -- (and, if C is poly-kinded, so will its kind parameter).
 
-tcFamTyPats fam_tc (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars })
+tcFamTyPats fam_tc_name kind
+            (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars })
             kind_checker thing_inside
-  = do { -- A family instance must have exactly the same number of type
-         -- parameters as the family declaration.  You can't write
-         --     type family F a :: * -> *
-         --     type instance F Int y = y
-         -- because then the type (F Int) would be like (\y.y)
-       ; let (fam_kvs, fam_body) = splitForAllTys (tyConKind fam_tc)
-             fam_arity = tyConArity fam_tc - length fam_kvs
-       ; checkTc (length arg_pats == fam_arity) $
-                 wrongNumberOfParmsErr fam_arity
+  = do { let (fam_kvs, fam_body) = splitForAllTys kind
+
+         -- We wish to check that the pattern has the right number of arguments
+         -- in checkValidFamPats (in TcValidity), so we can do the check *after*
+         -- we're done with the knot. But, the splitKindFunTysN below will panic
+         -- if there are *too many* patterns. So, we do a preliminary check here.
+         -- Note that we don't have enough information at hand to do a full check,
+         -- as that requires the full declared arity of the family, which isn't
+         -- nearby.
+       ; let max_args = length (fst $ splitKindFunTys fam_body)
+       ; checkTc (length arg_pats <= max_args) $
+           wrongNumberOfParmsErrTooMany max_args
 
          -- Instantiate with meta kind vars
        ; fam_arg_kinds <- mapM (const newMetaKindVar) fam_kvs
        ; loc <- getSrcSpanM
        ; let (arg_kinds, res_kind)
-                 = splitKindFunTysN fam_arity $
+                 = splitKindFunTysN (length arg_pats) $
                    substKiWith fam_kvs fam_arg_kinds fam_body
              hs_tvs = HsQTvs { hsq_kvs = kvars
                              , hsq_tvs = userHsTyVarBndrs loc tvars }
@@ -888,7 +929,7 @@ tcFamTyPats fam_tc (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tva
          -- See Note [Quantifying over family patterns]
        ; typats <- tcHsTyVarBndrs hs_tvs $ \ _ ->
                    do { kind_checker res_kind
-                      ; tcHsArgTys (quotes (ppr fam_tc)) arg_pats arg_kinds }
+                      ; tcHsArgTys (quotes (ppr fam_tc_name)) arg_pats arg_kinds }
        ; let all_args = fam_arg_kinds ++ typats
 
             -- Find free variables (after zonking) and turn
@@ -1214,7 +1255,7 @@ checkValidTyCl decl
            _ -> return () }
 
 checkValidFamDecl :: FamilyDecl Name -> TcM ()
-checkValidFamDecl (FamilyDecl { fdLName = lname, fdFlavour = flav })
+checkValidFamDecl (FamilyDecl { fdLName = lname, fdInfo = flav })
   = checkValidDecl (hsep [ptext (sLit "In the"), ppr flav,
                           ptext (sLit "declaration for"), quotes (ppr lname)])
                    lname
@@ -1241,8 +1282,9 @@ checkValidTyCon tc
 
   | Just syn_rhs <- synTyConRhs_maybe tc
   = case syn_rhs of
-      SynFamilyTyCon {} -> return ()
-      SynonymTyCon ty   -> checkValidType syn_ctxt ty
+      ClosedSynFamilyTyCon ax -> checkValidClosedCoAxiom ax
+      OpenSynFamilyTyCon  -> return ()
+      SynonymTyCon ty     -> checkValidType syn_ctxt ty
 
   | otherwise
   = do { -- Check the context on the data decl
@@ -1306,6 +1348,23 @@ checkValidTyCon tc
                 fty2 = dataConFieldType con2 label
     check_fields [] = panic "checkValidTyCon/check_fields []"
 
+checkValidClosedCoAxiom :: CoAxiom Branched -> TcM ()
+checkValidClosedCoAxiom (CoAxiom { co_ax_branches = branches, co_ax_tc = tc })
+ = tcAddClosedTypeFamilyDeclCtxt tc $
+   do { brListFoldlM_ check_accessibility [] branches
+      ; void $ brListMapM (checkValidTyFamInst Nothing tc) branches }
+   where
+     check_accessibility :: [CoAxBranch]       -- prev branches (in reverse order)
+                         -> CoAxBranch         -- cur branch
+                         -> TcM [CoAxBranch]   -- cur : prev
+               -- Check whether the branch is dominated by earlier
+               -- ones and hence is inaccessible
+     check_accessibility prev_branches cur_branch
+       = do { when (cur_branch `isDominatedBy` prev_branches) $
+              setSrcSpan (coAxBranchSpan cur_branch) $
+              addErrTc $ inaccessibleCoAxBranch tc cur_branch
+            ; return (cur_branch : prev_branches) }
+
 checkFieldCompat :: Name -> DataCon -> DataCon -> TyVarSet
                  -> Type -> Type -> Type -> Type -> TcM ()
 checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2
@@ -1705,10 +1764,7 @@ tcAddDefaultAssocDeclCtxt name thing_inside
 
 tcAddTyFamInstCtxt :: TyFamInstDecl Name -> TcM a -> TcM a
 tcAddTyFamInstCtxt decl
-  | [_] <- tfid_eqns decl
   = tcAddFamInstCtxt (ptext (sLit "type instance")) (tyFamInstDeclName decl)
-  | otherwise
-  = tcAddFamInstCtxt (ptext (sLit "type instance group")) (tyFamInstDeclName decl)
 
 tcAddDataFamInstCtxt :: DataFamInstDecl Name -> TcM a -> TcM a
 tcAddDataFamInstCtxt decl
@@ -1723,6 +1779,13 @@ tcAddFamInstCtxt flavour tycon thing_inside
                   <+> ptext (sLit "declaration for"),
                   quotes (ppr tycon)]
 
+tcAddClosedTypeFamilyDeclCtxt :: TyCon -> TcM a -> TcM a
+tcAddClosedTypeFamilyDeclCtxt tc
+  = addErrCtxt ctxt
+  where
+    ctxt = ptext (sLit "In the equations for closed type family") <+>
+           quotes (ppr tc)
+
 resultTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
 resultTypeMisMatch field_name con1 con2
   = vcat [sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2,
@@ -1830,11 +1893,6 @@ emptyConDeclsErr tycon
   = sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"),
          nest 2 $ ptext (sLit "(-XEmptyDataDecls permits this)")]
 
-wrongNumberOfParmsErr :: Arity -> SDoc
-wrongNumberOfParmsErr exp_arity
-  = ptext (sLit "Number of parameters must match family declaration; expected")
-    <+> ppr exp_arity
-
 wrongKindOfFamily :: TyCon -> SDoc
 wrongKindOfFamily family
   = ptext (sLit "Wrong category of family instance; declaration was for a")
@@ -1844,10 +1902,20 @@ wrongKindOfFamily family
                  | isAlgTyCon family = ptext (sLit "data type")
                  | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
 
+wrongNumberOfParmsErrTooMany :: Arity -> SDoc
+wrongNumberOfParmsErrTooMany max_args
+  = ptext (sLit "Number of parameters must match family declaration; expected no more than")
+    <+> ppr max_args
+
 wrongNamesInInstGroup :: Name -> Name -> SDoc
 wrongNamesInInstGroup first cur
-  = ptext (sLit "Mismatched family names in instance group.") $$
+  = ptext (sLit "Mismatched type names in closed type family declaration.") $$
     ptext (sLit "First name was") <+>
     (ppr first) <> (ptext (sLit "; this one is")) <+> (ppr cur)
 
+inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
+inaccessibleCoAxBranch tc fi
+  = ptext (sLit "Inaccessible family instance equation:") $$
+      (pprCoAxBranch tc fi)
+
 \end{code}
diff --git a/compiler/typecheck/TcValidity.lhs b/compiler/typecheck/TcValidity.lhs
index 54377192f4..968d8695cc 100644
--- a/compiler/typecheck/TcValidity.lhs
+++ b/compiler/typecheck/TcValidity.lhs
@@ -45,6 +45,7 @@ import ListSetOps
 import SrcLoc
 import Outputable
 import FastString
+import BasicTypes ( Arity )
 
 import Control.Monad
 import Data.List        ( (\\) )
@@ -1135,10 +1136,25 @@ checkValidFamPats :: TyCon -> [TyVar] -> [Type] -> TcM ()
 --    e.g. we disallow (Trac #7536)
 --         type T a = Int
 --         type instance F (T a) = a
+-- c) Have the right number of patterns
 checkValidFamPats fam_tc tvs ty_pats
-  = do { mapM_ checkTyFamFreeness ty_pats
+  = do { -- A family instance must have exactly the same number of type
+         -- parameters as the family declaration.  You can't write
+         --     type family F a :: * -> *
+         --     type instance F Int y = y
+         -- because then the type (F Int) would be like (\y.y)
+         checkTc (length ty_pats == fam_arity) $
+           wrongNumberOfParmsErr (fam_arity - length fam_kvs) -- report only types
+       ; mapM_ checkTyFamFreeness ty_pats
        ; let unbound_tvs = filterOut (`elemVarSet` exactTyVarsOfTypes ty_pats) tvs
        ; checkTc (null unbound_tvs) (famPatErr fam_tc unbound_tvs ty_pats) }
+  where fam_arity    = tyConArity fam_tc
+        (fam_kvs, _) = splitForAllTys (tyConKind fam_tc)
+
+wrongNumberOfParmsErr :: Arity -> SDoc
+wrongNumberOfParmsErr exp_arity
+  = ptext (sLit "Number of parameters must match family declaration; expected")
+    <+> ppr exp_arity
 
 -- Ensure that no type family instances occur in a type.
 --