Entirely re-jig the handling of default type-family instances (fixes Trac #9063)

In looking at Trac #9063 I decided to re-design the default
instances for associated type synonyms.  Previously it was all
jolly complicated, to support generality that no one wanted, and
was arguably undesirable.

Specifically

* The default instance for an associated type can have only
  type variables on the LHS.  (Not type patterns.)

* There can be at most one default instances declaration for
  each associated type.

To achieve this I had to do a surprisingly large amount of refactoring
of HsSyn, specifically to parameterise HsDecls.TyFamEqn over the type
of the LHS patterns.

That change in HsDecls has a (trivial) knock-on effect in Haddock, so
this commit does a submodule update too.

The net result is good though.  The code is simpler; the language
specification is simpler.  Happy days.

Trac #9263 and #9264 are thereby fixed as well.

14 files changed, 461 insertions, 315 deletions

diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index 435f5c73a2..adfc0f688f 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -396,10 +396,10 @@ repTyFamInstD decl@(TyFamInstDecl { tfid_eqn = eqn })
        ; repTySynInst tc eqn1 }
 
 repTyFamEqn :: LTyFamInstEqn Name -> DsM (Core TH.TySynEqnQ)
-repTyFamEqn (L loc (TyFamInstEqn { tfie_pats = HsWB { hswb_cts = tys
-                                                    , hswb_kvs = kv_names
-                                                    , hswb_tvs = tv_names }
-                                 , tfie_rhs = rhs }))
+repTyFamEqn (L loc (TyFamEqn { tfe_pats = HsWB { hswb_cts = tys
+                                               , hswb_kvs = kv_names
+                                               , hswb_tvs = tv_names }
+                                 , tfe_rhs = rhs }))
   = do { let hs_tvs = HsQTvs { hsq_kvs = kv_names
                              , hsq_tvs = userHsTyVarBndrs loc tv_names }   -- Yuk
        ; addTyClTyVarBinds hs_tvs $ \ _ ->
diff --git a/compiler/hsSyn/Convert.lhs b/compiler/hsSyn/Convert.lhs
index 122be81972..e22af3b947 100644
--- a/compiler/hsSyn/Convert.lhs
+++ b/compiler/hsSyn/Convert.lhs
@@ -201,13 +201,20 @@ cvtDec (ClassD ctxt cl tvs fds decs)
         ; unless (null adts')
             (failWith $ (ptext (sLit "Default data instance declarations are not allowed:"))
                    $$ (Outputable.ppr adts'))
+        ; at_defs <- mapM cvt_at_def ats'
         ; returnL $ TyClD $
           ClassDecl { tcdCtxt = cxt', tcdLName = tc', tcdTyVars = tvs'
                     , tcdFDs = fds', tcdSigs = sigs', tcdMeths = binds'
-                    , tcdATs = fams', tcdATDefs = ats', tcdDocs = []
+                    , tcdATs = fams', tcdATDefs = at_defs, tcdDocs = []
                     , tcdFVs = placeHolderNames }
                               -- no docs in TH ^^
         }
+  where
+    cvt_at_def :: LTyFamInstDecl RdrName -> CvtM (LTyFamDefltEqn RdrName)
+    -- Very similar to what happens in RdrHsSyn.mkClassDecl
+    cvt_at_def decl = case RdrHsSyn.mkATDefault decl of
+                        Right def     -> return def
+                        Left (_, msg) -> failWith msg
 
 cvtDec (InstanceD ctxt ty decs)
   = do  { let doc = ptext (sLit "an instance declaration")
@@ -280,9 +287,9 @@ cvtTySynEqn :: Located RdrName -> TySynEqn -> CvtM (LTyFamInstEqn RdrName)
 cvtTySynEqn tc (TySynEqn lhs rhs)
   = do  { lhs' <- mapM cvtType lhs
         ; rhs' <- cvtType rhs
-        ; returnL $ TyFamInstEqn { tfie_tycon = tc
-                                 , tfie_pats = mkHsWithBndrs lhs'
-                                 , tfie_rhs = rhs' } }
+        ; returnL $ TyFamEqn { tfe_tycon = tc
+                             , tfe_pats = mkHsWithBndrs lhs'
+                             , tfe_rhs = rhs' } }
 
 ----------------
 cvt_ci_decs :: MsgDoc -> [TH.Dec]
diff --git a/compiler/hsSyn/HsDecls.lhs b/compiler/hsSyn/HsDecls.lhs
index d35a7e5c5e..845c05296c 100644
--- a/compiler/hsSyn/HsDecls.lhs
+++ b/compiler/hsSyn/HsDecls.lhs
@@ -29,7 +29,7 @@ module HsDecls (
   InstDecl(..), LInstDecl, NewOrData(..), FamilyInfo(..),
   TyFamInstDecl(..), LTyFamInstDecl, instDeclDataFamInsts,
   DataFamInstDecl(..), LDataFamInstDecl, pprDataFamInstFlavour,
-  TyFamInstEqn(..), LTyFamInstEqn,
+  TyFamEqn(..), TyFamInstEqn, LTyFamInstEqn, TyFamDefltEqn, LTyFamDefltEqn,
   LClsInstDecl, ClsInstDecl(..),
 
   -- ** Standalone deriving declarations
@@ -472,7 +472,7 @@ data TyClDecl name
                 tcdSigs    :: [LSig name],              -- ^ Methods' signatures
                 tcdMeths   :: LHsBinds name,            -- ^ Default methods
                 tcdATs     :: [LFamilyDecl name],       -- ^ Associated types; ie
-                tcdATDefs  :: [LTyFamInstDecl name],    -- ^ Associated type defaults
+                tcdATDefs  :: [LTyFamDefltEqn name],    -- ^ Associated type defaults
                 tcdDocs    :: [LDocDecl],               -- ^ Haddock docs
                 tcdFVs     :: NameSet
     }
@@ -573,7 +573,7 @@ tyFamInstDeclName = unLoc . tyFamInstDeclLName
 tyFamInstDeclLName :: OutputableBndr name
                    => TyFamInstDecl name -> Located name
 tyFamInstDeclLName (TyFamInstDecl { tfid_eqn =
-                     (L _ (TyFamInstEqn { tfie_tycon = ln })) })
+                     (L _ (TyFamEqn { tfe_tycon = ln })) })
   = ln
 
 tyClDeclLName :: TyClDecl name -> Located name
@@ -632,7 +632,7 @@ instance OutputableBndr name
       | otherwise       -- Laid out
       = vcat [ top_matter <+> ptext (sLit "where")
              , nest 2 $ pprDeclList (map ppr ats ++
-                                     map ppr at_defs ++
+                                     map ppr_fam_deflt_eqn at_defs ++
                                      pprLHsBindsForUser methods sigs) ]
       where
         top_matter = ptext (sLit "class") 
@@ -657,7 +657,7 @@ instance (OutputableBndr name) => Outputable (FamilyDecl name) where
             ClosedTypeFamily eqns -> ( ptext (sLit "where")
                                      , if null eqns
                                        then ptext (sLit "..")
-                                       else vcat $ map ppr eqns )
+                                       else vcat $ map ppr_fam_inst_eqn eqns )
             _                     -> (empty, empty)
 
 pprFlavour :: FamilyInfo name -> SDoc
@@ -678,7 +678,7 @@ pp_vanilla_decl_head thing tyvars context
 
 pp_fam_inst_lhs :: OutputableBndr name
    => Located name
-   -> HsWithBndrs [LHsType name]
+   -> HsTyPats name
    -> HsContext name
    -> SDoc
 pp_fam_inst_lhs thing (HsWB { hswb_cts = typats }) context -- explicit type patterns
@@ -686,12 +686,13 @@ pp_fam_inst_lhs thing (HsWB { hswb_cts = typats }) context -- explicit type patt
           , hsep (map (pprParendHsType.unLoc) typats)]
 
 pprTyClDeclFlavour :: TyClDecl a -> SDoc
-pprTyClDeclFlavour (ClassDecl {})  = ptext (sLit "class")
-pprTyClDeclFlavour (FamDecl {})    = ptext (sLit "family")
-pprTyClDeclFlavour (SynDecl {})    = ptext (sLit "type")
-pprTyClDeclFlavour (DataDecl { tcdDataDefn = (HsDataDefn { dd_ND = nd }) })
-  = ppr nd
+pprTyClDeclFlavour (ClassDecl {})   = ptext (sLit "class")
+pprTyClDeclFlavour (SynDecl {})     = ptext (sLit "type")
 pprTyClDeclFlavour (ForeignType {}) = ptext (sLit "foreign type")
+pprTyClDeclFlavour (FamDecl { tcdFam = FamilyDecl { fdInfo = info }})
+  = pprFlavour info
+pprTyClDeclFlavour (DataDecl { tcdDataDefn = HsDataDefn { dd_ND = nd } })
+  = ppr nd
 \end{code}
 
 %************************************************************************
@@ -893,25 +894,49 @@ pprConDecl decl@(ConDecl { con_details = InfixCon ty1 ty2, con_res = ResTyGADT {
 %*                                                                      *
 %************************************************************************
 
+Note [Type family instance declarations in HsSyn]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The data type TyFamEqn represents one equation of a type family instance.
+It is parameterised over its tfe_pats field:
+
+ * An ordinary type family instance declaration looks like this in source Haskell
+      type instance T [a] Int = a -> a
+   (or something similar for a closed family)
+   It is represented by a TyFamInstEqn, with *type* in the tfe_pats field.
+
+ * On the other hand, the *default instance* of an associated type looksl like
+   this in source Haskell
+      class C a where
+        type T a b
+        type T a b = a -> b   -- The default instance
+   It is represented by a TyFamDefltEqn, with *type variables8 in the tfe_pats field.
+
 \begin{code}
 ----------------- Type synonym family instances -------------
+type LTyFamInstEqn  name = Located (TyFamInstEqn  name)
+type LTyFamDefltEqn name = Located (TyFamDefltEqn name)
 
-type LTyFamInstEqn name = Located (TyFamInstEqn name)
-
--- | One equation in a type family instance declaration
-data TyFamInstEqn name   
-  = TyFamInstEqn
-       { tfie_tycon :: Located name
-       , tfie_pats  :: HsWithBndrs [LHsType name]
+type HsTyPats name = HsWithBndrs [LHsType name]
             -- ^ Type patterns (with kind and type bndrs)
             -- See Note [Family instance declaration binders]
-       , tfie_rhs   :: LHsType name }         
+
+type TyFamInstEqn  name = TyFamEqn name (HsTyPats name)
+type TyFamDefltEqn name = TyFamEqn name (LHsTyVarBndrs name)
+  -- See Note [Type family instance declarations in HsSyn]
+
+-- | One equation in a type family instance declaration
+-- See Note [Type family instance declarations in HsSyn]
+data TyFamEqn name pats
+  = TyFamEqn
+       { tfe_tycon :: Located name
+       , tfe_pats  :: pats
+       , tfe_rhs   :: LHsType name }
   deriving( Typeable, Data )
 
 type LTyFamInstDecl name = Located (TyFamInstDecl name)
-data TyFamInstDecl name 
+data TyFamInstDecl name
   = TyFamInstDecl
-       { tfid_eqn  :: LTyFamInstEqn name 
+       { tfid_eqn  :: LTyFamInstEqn name
        , tfid_fvs  :: NameSet }
   deriving( Typeable, Data )
 
@@ -921,11 +946,9 @@ type LDataFamInstDecl name = Located (DataFamInstDecl name)
 data DataFamInstDecl name
   = DataFamInstDecl
        { dfid_tycon :: Located name
-       , dfid_pats  :: HsWithBndrs [LHsType name]   -- lhs
-            -- ^ Type patterns (with kind and type bndrs)
-            -- See Note [Family instance declaration binders]
-       , dfid_defn  :: HsDataDefn  name             -- rhs
-       , dfid_fvs   :: NameSet }                    -- free vars for dependency analysis
+       , dfid_pats  :: HsTyPats name      -- LHS
+       , dfid_defn  :: HsDataDefn  name   -- RHS
+       , dfid_fvs   :: NameSet }          -- Rree vars for dependency analysis
   deriving( Typeable, Data )
 
 
@@ -937,10 +960,10 @@ data ClsInstDecl name
       { cid_poly_ty :: LHsType name    -- Context => Class Instance-type
                                        -- Using a polytype means that the renamer conveniently
                                        -- figures out the quantified type variables for us.
-      , cid_binds :: LHsBinds name
-      , cid_sigs  :: [LSig name]                -- User-supplied pragmatic info
-      , cid_tyfam_insts :: [LTyFamInstDecl name]  -- type family instances
-      , cid_datafam_insts :: [LDataFamInstDecl name] -- data family instances
+      , cid_binds         :: LHsBinds name           -- Class methods
+      , cid_sigs          :: [LSig name]             -- User-supplied pragmatic info
+      , cid_tyfam_insts   :: [LTyFamInstDecl name]   -- Type family instances
+      , cid_datafam_insts :: [LDataFamInstDecl name] -- Data family instances
       , cid_overlap_mode :: Maybe OverlapMode
       }
   deriving (Data, Typeable)
@@ -984,17 +1007,23 @@ instance (OutputableBndr name) => Outputable (TyFamInstDecl name) where
 
 pprTyFamInstDecl :: OutputableBndr name => TopLevelFlag -> TyFamInstDecl name -> SDoc
 pprTyFamInstDecl top_lvl (TyFamInstDecl { tfid_eqn = eqn })
-   = ptext (sLit "type") <+> ppr_instance_keyword top_lvl <+> (ppr eqn)
+   = ptext (sLit "type") <+> ppr_instance_keyword top_lvl <+> ppr_fam_inst_eqn eqn
 
 ppr_instance_keyword :: TopLevelFlag -> SDoc
 ppr_instance_keyword TopLevel    = ptext (sLit "instance")
 ppr_instance_keyword NotTopLevel = empty
 
-instance (OutputableBndr name) => Outputable (TyFamInstEqn name) where
-  ppr (TyFamInstEqn { tfie_tycon = tycon
-                    , tfie_pats  = pats
-                    , tfie_rhs   = rhs })
-    = (pp_fam_inst_lhs tycon pats []) <+> equals <+> (ppr rhs)
+ppr_fam_inst_eqn :: OutputableBndr name => LTyFamInstEqn name -> SDoc
+ppr_fam_inst_eqn (L _ (TyFamEqn { tfe_tycon = tycon
+                                , tfe_pats  = pats
+                                , tfe_rhs   = rhs }))
+    = pp_fam_inst_lhs tycon pats [] <+> equals <+> ppr rhs
+
+ppr_fam_deflt_eqn :: OutputableBndr name => LTyFamDefltEqn name -> SDoc
+ppr_fam_deflt_eqn (L _ (TyFamEqn { tfe_tycon = tycon
+                                 , tfe_pats  = tvs
+                                 , tfe_rhs   = rhs }))
+    = pp_vanilla_decl_head tycon tvs [] <+> equals <+> ppr rhs
 
 instance (OutputableBndr name) => Outputable (DataFamInstDecl name) where
   ppr = pprDataFamInstDecl TopLevel
diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs
index 7b202acf7d..935b8eda93 100644
--- a/compiler/iface/IfaceSyn.lhs
+++ b/compiler/iface/IfaceSyn.lhs
@@ -168,9 +168,10 @@ data IfaceClassOp = IfaceClassOp IfaceTopBndr DefMethSpec IfaceType
         -- Just False => ordinary polymorphic default method
         -- Just True  => generic default method
 
-data IfaceAT = IfaceAT
-                  IfaceDecl        -- The associated type declaration
-                  [IfaceAxBranch]  -- Default associated type instances, if any
+data IfaceAT = IfaceAT  -- See Class.ClassATItem
+                  IfaceDecl          -- The associated type declaration
+                  (Maybe IfaceType)  -- Default associated type instance, if any
+
 
 -- This is just like CoAxBranch
 data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars  :: [IfaceTvBndr]
@@ -839,12 +840,12 @@ instance Outputable IfaceAT where
    ppr = pprIfaceAT showAll
 
 pprIfaceAT :: ShowSub -> IfaceAT -> SDoc
-pprIfaceAT ss (IfaceAT d defs)
+pprIfaceAT ss (IfaceAT d mb_def)
   = vcat [ pprIfaceDecl ss d
-         , ppUnless (null defs) $ nest 2 $
-           ptext (sLit "Defaults:") <+> vcat (map (pprAxBranch pp_tc) defs) ]
-  where
-    pp_tc = ppr (ifName d)
+         , case mb_def of
+              Nothing  -> empty
+              Just rhs -> nest 2 $
+                          ptext (sLit "Default:") <+> ppr rhs ]
 
 instance Outputable IfaceTyConParent where
   ppr p = pprIfaceTyConParent p
@@ -1174,9 +1175,11 @@ freeNamesIfContext :: IfaceContext -> NameSet
 freeNamesIfContext = fnList freeNamesIfType
 
 freeNamesIfAT :: IfaceAT -> NameSet
-freeNamesIfAT (IfaceAT decl defs)
+freeNamesIfAT (IfaceAT decl mb_def)
   = freeNamesIfDecl decl &&&
-    fnList freeNamesIfAxBranch defs
+    case mb_def of
+      Nothing  -> emptyNameSet
+      Just rhs -> freeNamesIfType rhs
 
 freeNamesIfClsSig :: IfaceClassOp -> NameSet
 freeNamesIfClsSig (IfaceClassOp _n _dm ty) = freeNamesIfType ty
diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs
index b4d36aed91..460c6076ba 100644
--- a/compiler/iface/MkIface.lhs
+++ b/compiler/iface/MkIface.lhs
@@ -1476,7 +1476,7 @@ checkList (check:checks) = do recompile <- check
 \begin{code}
 tyThingToIfaceDecl :: TyThing -> IfaceDecl
 tyThingToIfaceDecl (AnId id)      = idToIfaceDecl id
-tyThingToIfaceDecl (ATyCon tycon) = tyConToIfaceDecl emptyTidyEnv tycon
+tyThingToIfaceDecl (ATyCon tycon) = snd (tyConToIfaceDecl emptyTidyEnv tycon)
 tyThingToIfaceDecl (ACoAxiom ax)  = coAxiomToIfaceDecl ax
 tyThingToIfaceDecl (AConLike cl)  = case cl of
     RealDataCon dc -> dataConToIfaceDecl dc -- for ppr purposes only
@@ -1568,48 +1568,52 @@ coAxBranchToIfaceBranch' tc (CoAxBranch { cab_tvs = tvs, cab_lhs = lhs
     -- See Note [CoAxBranch type variables] in CoAxiom
 
 -----------------
-tyConToIfaceDecl :: TidyEnv -> TyCon -> IfaceDecl
+tyConToIfaceDecl :: TidyEnv -> TyCon -> (TidyEnv, IfaceDecl)
 -- We *do* tidy TyCons, because they are not (and cannot
 -- conveniently be) built in tidy form
+-- The returned TidyEnv is the one after tidying the tyConTyVars
 tyConToIfaceDecl env tycon
   | Just clas <- tyConClass_maybe tycon
   = classToIfaceDecl env clas
 
   | Just syn_rhs <- synTyConRhs_maybe tycon
-  = IfaceSyn {  ifName    = getOccName tycon,
-                ifTyVars  = if_tc_tyvars,
-                ifRoles   = tyConRoles tycon,
-                ifSynRhs  = to_ifsyn_rhs syn_rhs,
-                ifSynKind = tidyToIfaceType tc_env1 (synTyConResKind tycon) }
+  = ( tc_env1
+    , IfaceSyn {  ifName    = getOccName tycon,
+                  ifTyVars  = if_tc_tyvars,
+                  ifRoles   = tyConRoles tycon,
+                  ifSynRhs  = to_ifsyn_rhs syn_rhs,
+                  ifSynKind = tidyToIfaceType tc_env1 (synTyConResKind tycon) })
 
   | isAlgTyCon tycon
-  = IfaceData { ifName    = getOccName tycon,
-                ifCType   = tyConCType tycon,
-                ifTyVars  = if_tc_tyvars,
-                ifRoles   = tyConRoles tycon,
-                ifCtxt    = tidyToIfaceContext tc_env1 (tyConStupidTheta tycon),
-                ifCons    = ifaceConDecls (algTyConRhs tycon),
-                ifRec     = boolToRecFlag (isRecursiveTyCon tycon),
-                ifGadtSyntax = isGadtSyntaxTyCon tycon,
-                ifPromotable = isJust (promotableTyCon_maybe tycon),
-                ifParent  = parent }
+  = ( tc_env1
+    , IfaceData { ifName    = getOccName tycon,
+                  ifCType   = tyConCType tycon,
+                  ifTyVars  = if_tc_tyvars,
+                  ifRoles   = tyConRoles tycon,
+                  ifCtxt    = tidyToIfaceContext tc_env1 (tyConStupidTheta tycon),
+                  ifCons    = ifaceConDecls (algTyConRhs tycon),
+                  ifRec     = boolToRecFlag (isRecursiveTyCon tycon),
+                  ifGadtSyntax = isGadtSyntaxTyCon tycon,
+                  ifPromotable = isJust (promotableTyCon_maybe tycon),
+                  ifParent  = parent })
 
   | isForeignTyCon tycon
-  = IfaceForeign { ifName    = getOccName tycon,
-                   ifExtName = tyConExtName tycon }
+  = (env, IfaceForeign { ifName    = getOccName tycon,
+                         ifExtName = tyConExtName tycon })
 
-  | otherwise
+  | otherwise  -- FunTyCon, PrimTyCon, promoted TyCon/DataCon
   -- For pretty printing purposes only.
-  = IfaceData { ifName       = getOccName tycon,
-                ifCType      = Nothing,
-                ifTyVars     = funAndPrimTyVars,
-                ifRoles      = tyConRoles tycon,
-                ifCtxt       = [],
-                ifCons       = IfDataTyCon [],
-                ifRec        = boolToRecFlag False,
-                ifGadtSyntax = False,
-                ifPromotable = False,
-                ifParent     = IfNoParent }
+  = ( env
+    , IfaceData { ifName       = getOccName tycon,
+                  ifCType      = Nothing,
+                  ifTyVars     = funAndPrimTyVars,
+                  ifRoles      = tyConRoles tycon,
+                  ifCtxt       = [],
+                  ifCons       = IfDataTyCon [],
+                  ifRec        = boolToRecFlag False,
+                  ifGadtSyntax = False,
+                  ifPromotable = False,
+                  ifParent     = IfNoParent })
   where
     (tc_env1, tc_tyvars) = tidyTyClTyVarBndrs env (tyConTyVars tycon)
     if_tc_tyvars = toIfaceTvBndrs tc_tyvars
@@ -1680,17 +1684,18 @@ toIfaceBang env (HsUnpack (Just co)) = IfUnpackCo (toIfaceCoercion (tidyCo env c
 toIfaceBang _   HsStrict             = IfStrict
 toIfaceBang _   (HsUserBang {})      = panic "toIfaceBang"
 
-classToIfaceDecl :: TidyEnv -> Class -> IfaceDecl
+classToIfaceDecl :: TidyEnv -> Class -> (TidyEnv, IfaceDecl)
 classToIfaceDecl env clas
-  = IfaceClass { ifCtxt   = tidyToIfaceContext env1 sc_theta,
-                 ifName   = getOccName (classTyCon clas),
-                 ifTyVars = toIfaceTvBndrs clas_tyvars',
-                 ifRoles  = tyConRoles (classTyCon clas),
-                 ifFDs    = map toIfaceFD clas_fds,
-                 ifATs    = map toIfaceAT clas_ats,
-                 ifSigs   = map toIfaceClassOp op_stuff,
-                 ifMinDef = fmap getFS (classMinimalDef clas),
-                 ifRec    = boolToRecFlag (isRecursiveTyCon tycon) }
+  = ( env1
+    , IfaceClass { ifCtxt   = tidyToIfaceContext env1 sc_theta,
+                   ifName   = getOccName (classTyCon clas),
+                   ifTyVars = toIfaceTvBndrs clas_tyvars',
+                   ifRoles  = tyConRoles (classTyCon clas),
+                   ifFDs    = map toIfaceFD clas_fds,
+                   ifATs    = map toIfaceAT clas_ats,
+                   ifSigs   = map toIfaceClassOp op_stuff,
+                   ifMinDef = fmap getFS (classMinimalDef clas),
+                   ifRec    = boolToRecFlag (isRecursiveTyCon tycon) })
   where
     (clas_tyvars, clas_fds, sc_theta, _, clas_ats, op_stuff)
       = classExtraBigSig clas
@@ -1699,8 +1704,10 @@ classToIfaceDecl env clas
     (env1, clas_tyvars') = tidyTyVarBndrs env clas_tyvars
 
     toIfaceAT :: ClassATItem -> IfaceAT
-    toIfaceAT (tc, defs)
-      = IfaceAT (tyConToIfaceDecl env1 tc) (map (coAxBranchToIfaceBranch' tc) defs)
+    toIfaceAT (ATI tc def)
+      = IfaceAT if_decl (fmap (tidyToIfaceType env2) def)
+      where
+        (env2, if_decl) = tyConToIfaceDecl env1 tc
 
     toIfaceClassOp (sel_id, def_meth)
         = ASSERT(sel_tyvars == clas_tyvars)
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 14eb723a86..68f9e8fd65 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -544,13 +544,18 @@ tc_iface_decl _parent ignore_prags
                 -- it mentions unless it's necessary to do so
           ; return (op_name, dm, op_ty) }
 
-   tc_at cls (IfaceAT tc_decl defs_decls)
+   tc_at cls (IfaceAT tc_decl if_def)
      = do ATyCon tc <- tc_iface_decl (AssocFamilyTyCon cls) ignore_prags tc_decl
-          defs <- forkM (mk_at_doc tc) (tc_ax_branches defs_decls)
+          mb_def <- case if_def of
+                      Nothing  -> return Nothing
+                      Just def -> forkM (mk_at_doc tc)                 $
+                                  extendIfaceTyVarEnv (tyConTyVars tc) $
+                                  do { tc_def <- tcIfaceType def
+                                     ; return (Just tc_def) }
                   -- Must be done lazily in case the RHS of the defaults mention
                   -- the type constructor being defined here
                   -- e.g.   type AT a; type AT b = AT [b]   Trac #8002
-          return (tc, defs)
+          return (ATI tc mb_def)
 
    mk_sc_doc pred = ptext (sLit "Superclass") <+> ppr pred
    mk_at_doc tc = ptext (sLit "Associated type") <+> ppr tc
diff --git a/compiler/parser/RdrHsSyn.lhs b/compiler/parser/RdrHsSyn.lhs
index af351b7f31..93a98d068e 100644
--- a/compiler/parser/RdrHsSyn.lhs
+++ b/compiler/parser/RdrHsSyn.lhs
@@ -34,6 +34,7 @@ module RdrHsSyn (
         mkGadtDecl,          -- [Located RdrName] -> LHsType RdrName -> ConDecl RdrName
         mkSimpleConDecl,
         mkDeprecatedGadtRecordDecl,
+        mkATDefault,
 
         -- Bunch of functions in the parser monad for
         -- checking and constructing values
@@ -73,7 +74,7 @@ import TysWiredIn       ( unitTyCon, unitDataCon )
 import ForeignCall
 import OccName          ( srcDataName, varName, isDataOcc, isTcOcc,
                           occNameString )
-import PrelNames        ( forall_tv_RDR )
+import PrelNames        ( forall_tv_RDR, allNameStrings )
 import DynFlags
 import SrcLoc
 import OrdList          ( OrdList, fromOL )
@@ -124,16 +125,31 @@ mkClassDecl :: SrcSpan
             -> P (LTyClDecl RdrName)
 
 mkClassDecl loc (L _ (mcxt, tycl_hdr)) fds where_cls
-  = do { let (binds, sigs, ats, at_defs, _, docs) = cvBindsAndSigs (unLoc where_cls)
+  = do { let (binds, sigs, ats, at_insts, _, docs) = cvBindsAndSigs (unLoc where_cls)
              cxt = fromMaybe (noLoc []) mcxt
        ; (cls, tparams) <- checkTyClHdr tycl_hdr
-       ; tyvars <- checkTyVars (ptext (sLit "class")) whereDots
-                               cls tparams      -- Only type vars allowed
+       ; tyvars <- checkTyVarsP (ptext (sLit "class")) whereDots cls tparams
+       ; at_defs <- mapM (eitherToP . mkATDefault) at_insts
        ; return (L loc (ClassDecl { tcdCtxt = cxt, tcdLName = cls, tcdTyVars = tyvars,
                                     tcdFDs = unLoc fds, tcdSigs = sigs, tcdMeths = binds,
                                     tcdATs = ats, tcdATDefs = at_defs, tcdDocs  = docs,
                                     tcdFVs = placeHolderNames })) }
 
+mkATDefault :: LTyFamInstDecl RdrName
+            -> Either (SrcSpan, SDoc) (LTyFamDefltEqn RdrName)
+-- Take a type-family instance declaration and turn it into
+-- a type-family default equation for a class declaration
+-- We parse things as the former and use this function to convert to the latter
+-- 
+-- We use the Either monad because this also called 
+-- from Convert.hs
+mkATDefault (L loc (TyFamInstDecl { tfid_eqn = L _ e }))
+      | TyFamEqn { tfe_tycon = tc, tfe_pats = pats, tfe_rhs = rhs } <- e
+      = do { tvs <- checkTyVars (ptext (sLit "default")) equalsDots tc (hswb_cts pats)
+           ; return (L loc (TyFamEqn { tfe_tycon = tc
+                                     , tfe_pats = tvs
+                                     , tfe_rhs = rhs })) }
+
 mkTyData :: SrcSpan
          -> NewOrData
          -> Maybe CType
@@ -144,7 +160,7 @@ mkTyData :: SrcSpan
          -> P (LTyClDecl RdrName)
 mkTyData loc new_or_data cType (L _ (mcxt, tycl_hdr)) ksig data_cons maybe_deriv
   = do { (tc, tparams) <- checkTyClHdr tycl_hdr
-       ; tyvars <- checkTyVars (ppr new_or_data) equalsDots tc tparams
+       ; tyvars <- checkTyVarsP (ppr new_or_data) equalsDots tc tparams
        ; defn <- mkDataDefn new_or_data cType mcxt ksig data_cons maybe_deriv
        ; return (L loc (DataDecl { tcdLName = tc, tcdTyVars = tyvars,
                                    tcdDataDefn = defn,
@@ -172,7 +188,7 @@ mkTySynonym :: SrcSpan
             -> P (LTyClDecl RdrName)
 mkTySynonym loc lhs rhs
   = do { (tc, tparams) <- checkTyClHdr lhs
-       ; tyvars <- checkTyVars (ptext (sLit "type")) equalsDots tc tparams
+       ; tyvars <- checkTyVarsP (ptext (sLit "type")) equalsDots tc tparams
        ; return (L loc (SynDecl { tcdLName = tc, tcdTyVars = tyvars
                                 , tcdRhs = rhs, tcdFVs = placeHolderNames })) }
 
@@ -181,9 +197,9 @@ mkTyFamInstEqn :: LHsType RdrName
                -> P (TyFamInstEqn RdrName)
 mkTyFamInstEqn lhs rhs
   = do { (tc, tparams) <- checkTyClHdr lhs
-       ; return (TyFamInstEqn { tfie_tycon = tc
-                              , tfie_pats  = mkHsWithBndrs tparams
-                              , tfie_rhs   = rhs }) }
+       ; return (TyFamEqn { tfe_tycon = tc
+                          , tfe_pats  = mkHsWithBndrs tparams
+                          , tfe_rhs   = rhs }) }
 
 mkDataFamInst :: SrcSpan
          -> NewOrData
@@ -214,7 +230,7 @@ mkFamDecl :: SrcSpan
           -> P (LTyClDecl RdrName)
 mkFamDecl loc info lhs ksig
   = do { (tc, tparams) <- checkTyClHdr lhs
-       ; tyvars <- checkTyVars (ppr info) equals_or_where tc tparams
+       ; tyvars <- checkTyVarsP (ppr info) equals_or_where tc tparams
        ; return (L loc (FamDecl (FamilyDecl { fdInfo = info, fdLName = tc
                                             , fdTyVars = tyvars, fdKindSig = ksig }))) }
   where
@@ -502,26 +518,42 @@ we can bring x,y into scope.  So:
    * For RecCon we do not
 
 \begin{code}
-checkTyVars :: SDoc -> SDoc -> Located RdrName -> [LHsType RdrName] -> P (LHsTyVarBndrs RdrName)
+checkTyVarsP :: SDoc -> SDoc -> Located RdrName -> [LHsType RdrName] -> P (LHsTyVarBndrs RdrName)
+-- Same as checkTyVars, but in the P monad
+checkTyVarsP pp_what equals_or_where tc tparms 
+  = eitherToP $ checkTyVars pp_what equals_or_where tc tparms 
+
+eitherToP :: Either (SrcSpan, SDoc) a -> P a
+-- Adapts the Either monad to the P monad
+eitherToP (Left (loc, doc)) = parseErrorSDoc loc doc
+eitherToP (Right thing)     = return thing
+checkTyVars :: SDoc -> SDoc -> Located RdrName -> [LHsType RdrName] 
+            -> Either (SrcSpan, SDoc) (LHsTyVarBndrs RdrName)
 -- Check whether the given list of type parameters are all type variables
--- (possibly with a kind signature).
-checkTyVars pp_what equals_or_where tc tparms = do { tvs <- mapM chk tparms
-                                 ; return (mkHsQTvs tvs) }
+-- (possibly with a kind signature)
+-- We use the Either monad because it's also called (via mkATDefault) from
+-- Convert.hs
+checkTyVars pp_what equals_or_where tc tparms 
+  = do { tvs <- mapM chk tparms
+       ; return (mkHsQTvs tvs) }
   where
+        
         -- Check that the name space is correct!
     chk (L l (HsKindSig (L _ (HsTyVar tv)) k))
         | isRdrTyVar tv    = return (L l (KindedTyVar tv k))
     chk (L l (HsTyVar tv))
         | isRdrTyVar tv    = return (L l (UserTyVar tv))
-    chk t@(L l _)
-        = parseErrorSDoc l $
-          vcat [ ptext (sLit "Unexpected type") <+> quotes (ppr t)
-               , ptext (sLit "In the") <+> pp_what <+> ptext (sLit "declaration for") <+> quotes (ppr tc)
-               , vcat[ (ptext (sLit "A") <+> pp_what <+> ptext (sLit "declaration should have form"))
-                     , nest 2 (pp_what <+> ppr tc <+> ptext (sLit "a b c")
-                               <+> equals_or_where) ] ]
+    chk t@(L loc _)
+        = Left (loc, 
+                vcat [ ptext (sLit "Unexpected type") <+> quotes (ppr t)
+                     , ptext (sLit "In the") <+> pp_what <+> ptext (sLit "declaration for") <+> quotes (ppr tc)
+                     , vcat[ (ptext (sLit "A") <+> pp_what <+> ptext (sLit "declaration should have form"))
+                     , nest 2 (pp_what <+> ppr tc 
+                                       <+> hsep (map text (takeList tparms allNameStrings))
+                                       <+> equals_or_where) ] ])
 
 whereDots, equalsDots :: SDoc
+-- Second argument to checkTyVars
 whereDots  = ptext (sLit "where ...")
 equalsDots = ptext (sLit "= ...")
 
diff --git a/compiler/rename/RnSource.lhs b/compiler/rename/RnSource.lhs
index dae9d81d5a..9bc0e44780 100644
--- a/compiler/rename/RnSource.lhs
+++ b/compiler/rename/RnSource.lhs
@@ -465,7 +465,7 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds
        ; traceRn (text "rnSrcInstDecl"  <+> ppr inst_ty' $$ ppr inst_tyvars $$ ppr ktv_names)
        ; ((ats', adts', other_sigs'), more_fvs) 
              <- extendTyVarEnvFVRn ktv_names $
-                do { (ats', at_fvs) <- rnATInstDecls rnTyFamInstDecl cls inst_tyvars ats
+                do { (ats',  at_fvs)  <- rnATInstDecls rnTyFamInstDecl cls inst_tyvars ats
                    ; (adts', adt_fvs) <- rnATInstDecls rnDataFamInstDecl cls inst_tyvars adts
                    ; (other_sigs', sig_fvs) <- renameSigs (InstDeclCtxt cls) other_sigs
                    ; return ( (ats', adts', other_sigs')
@@ -564,14 +564,29 @@ rnTyFamInstDecl mb_cls (TyFamInstDecl { tfid_eqn = L loc eqn })
 rnTyFamInstEqn :: Maybe (Name, [Name])
                -> TyFamInstEqn RdrName
                -> RnM (TyFamInstEqn Name, FreeVars)
-rnTyFamInstEqn mb_cls (TyFamInstEqn { tfie_tycon = tycon
-                                    , tfie_pats  = HsWB { hswb_cts = pats }
-                                    , tfie_rhs   = rhs })
+rnTyFamInstEqn mb_cls (TyFamEqn { tfe_tycon = tycon
+                                , tfe_pats  = HsWB { hswb_cts = pats }
+                                , tfe_rhs   = rhs })
   = do { (tycon', pats', rhs', fvs) <-
            rnFamInstDecl (TySynCtx tycon) mb_cls tycon pats rhs rnTySyn
-       ; return (TyFamInstEqn { tfie_tycon = tycon'
-                              , tfie_pats  = pats'
-                              , tfie_rhs   = rhs' }, fvs) }
+       ; return (TyFamEqn { tfe_tycon = tycon'
+                          , tfe_pats  = pats'
+                          , tfe_rhs   = rhs' }, fvs) }
+
+rnTyFamDefltEqn :: Name
+                -> TyFamDefltEqn RdrName
+                -> RnM (TyFamDefltEqn Name, FreeVars)
+rnTyFamDefltEqn cls (TyFamEqn { tfe_tycon = tycon
+                              , tfe_pats  = tyvars
+                              , tfe_rhs   = rhs })
+  = bindHsTyVars ctx (Just cls) [] tyvars $ \ tyvars' ->
+    do { tycon'      <- lookupFamInstName (Just cls) tycon
+       ; (rhs', fvs) <- rnLHsType ctx rhs
+       ; return (TyFamEqn { tfe_tycon = tycon'
+                          , tfe_pats  = tyvars'
+                          , tfe_rhs   = rhs' }, fvs) }
+  where
+    ctx = TyFamilyCtx tycon
 
 rnDataFamInstDecl :: Maybe (Name, [Name])
                   -> DataFamInstDecl RdrName
@@ -590,7 +605,7 @@ rnDataFamInstDecl mb_cls (DataFamInstDecl { dfid_tycon = tycon
 Renaming of the associated types in instances.
 
 \begin{code}
--- rename associated type family decl in class
+-- Rename associated type family decl in class
 rnATDecls :: Name      -- Class
           -> [LFamilyDecl RdrName] 
           -> RnM ([LFamilyDecl Name], FreeVars)
@@ -941,7 +956,7 @@ rnTyClDecl (SynDecl { tcdLName = tycon, tcdTyVars = tyvars, tcdRhs = rhs })
                                     do { (rhs', fvs) <- rnTySyn doc rhs
                                        ; return ((tyvars', rhs'), fvs) }
        ; return (SynDecl { tcdLName = tycon', tcdTyVars = tyvars'
-                        , tcdRhs = rhs', tcdFVs = fvs }, fvs) }
+                         , tcdRhs = rhs', tcdFVs = fvs }, fvs) }
 
 -- "data", "newtype" declarations
 -- both top level and (for an associated type) in an instance decl
@@ -966,20 +981,20 @@ rnTyClDecl (ClassDecl {tcdCtxt = context, tcdLName = lcls,
                         -- kind signatures on the tyvars
 
         -- Tyvars scope over superclass context and method signatures
-        ; ((tyvars', context', fds', ats', at_defs', sigs'), stuff_fvs)
+        ; ((tyvars', context', fds', ats', sigs'), stuff_fvs)
             <- bindHsTyVars cls_doc Nothing kvs tyvars $ \ tyvars' -> do
                   -- Checks for distinct tyvars
              { (context', cxt_fvs) <- rnContext cls_doc context
              ; fds'  <- rnFds fds
                          -- The fundeps have no free variables
              ; (ats',     fv_ats)     <- rnATDecls cls' ats
-             ; (at_defs', fv_at_defs) <- rnATInstDecls rnTyFamInstDecl cls' tyvars' at_defs
              ; (sigs', sig_fvs) <- renameSigs (ClsDeclCtxt cls') sigs
              ; let fvs = cxt_fvs     `plusFV`
                          sig_fvs     `plusFV`
-                         fv_ats      `plusFV`
-                         fv_at_defs
-             ; return ((tyvars', context', fds', ats', at_defs', sigs'), fvs) }
+                         fv_ats
+             ; return ((tyvars', context', fds', ats', sigs'), fvs) }
+
+        ; (at_defs', fv_at_defs) <- rnList (rnTyFamDefltEqn cls') at_defs
 
         -- No need to check for duplicate associated type decls
         -- since that is done by RnNames.extendGlobalRdrEnvRn
@@ -1011,7 +1026,7 @@ rnTyClDecl (ClassDecl {tcdCtxt = context, tcdLName = lcls,
   -- Haddock docs
         ; docs' <- mapM (wrapLocM rnDocDecl) docs
 
-        ; let all_fvs = meth_fvs `plusFV` stuff_fvs
+        ; let all_fvs = meth_fvs `plusFV` stuff_fvs `plusFV` fv_at_defs
         ; return (ClassDecl { tcdCtxt = context', tcdLName = lcls',
                               tcdTyVars = tyvars', tcdFDs = fds', tcdSigs = sigs',
                               tcdMeths = mbinds', tcdATs = ats', tcdATDefs = at_defs',
diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs
index aa15a63a2a..d18c21c9de 100644
--- a/compiler/typecheck/TcDeriv.lhs
+++ b/compiler/typecheck/TcDeriv.lhs
@@ -20,7 +20,7 @@ import FamInst
 import TcErrors( reportAllUnsolved )
 import TcValidity( validDerivPred )
 import TcEnv
-import TcTyClsDecls( tcFamTyPats, tcAddDataFamInstCtxt )
+import TcTyClsDecls( tcFamTyPats, famTyConShape, tcAddDataFamInstCtxt )
 import TcClassDcl( tcAddDeclCtxt )      -- Small helper
 import TcGenDeriv                       -- Deriv stuff
 import TcGenGenerics
@@ -601,7 +601,7 @@ 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 tc_name (tyConKind fam_tc) pats (\_ -> return ()) $
+       ; tcFamTyPats (famTyConShape fam_tc) pats (\_ -> return ()) $
          \ tvs' pats' _ ->
            concatMapM (deriveTyData True tvs' fam_tc pats') preds }
         -- Tiresomely we must figure out the "lhs", which is awkward for type families
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index ed682df1b4..c3ba825cd5 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -38,7 +38,7 @@ import TcDeriv
 import TcEnv
 import TcHsType
 import TcUnify
-import Coercion   ( pprCoAxiom, pprCoAxBranch )
+import Coercion   ( pprCoAxiom )
 import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
 import Type
 import TcEvidence
@@ -70,6 +70,7 @@ import BooleanFormula ( isUnsatisfied, pprBooleanFormulaNice )
 
 import Control.Monad
 import Maybes     ( isNothing, isJust, whenIsJust )
+import Data.List  ( mapAccumL )
 \end{code}
 
 Typechecking instance declarations is done in two passes. The first
@@ -528,40 +529,11 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
 
         -- Check for missing associated types and build them
         -- from their defaults (if available)
-        ; let defined_ats = mkNameSet $ map (tyFamInstDeclName . unLoc) ats
-              defined_adts = mkNameSet $ map (unLoc . dfid_tycon . unLoc) adts
-
-              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
-                   || tyConName fam_tc `elemNameSet` defined_adts
-                = return []
-
-                 -- No defaults ==> generate a warning
-                | null defs
-                = do { warnMissingMethodOrAT "associated type" (tyConName fam_tc)
-                     ; return [] }
-
-                 -- No user instance, have defaults ==> instatiate them
-                 -- Example:   class C a where { type F a b :: *; type F a b = () }
-                 --            instance C [x]
-                 -- Then we want to generate the decl:   type F [x] b = ()
-                | otherwise 
-                = forM defs $ \br@(CoAxBranch { cab_lhs = pat_tys, cab_rhs = rhs }) ->
-                  do { let pat_tys' = substTys mini_subst pat_tys
-                           rhs'     = substTy  mini_subst rhs
-                           tv_set'  = tyVarsOfTypes pat_tys'
-                           tvs'     = varSetElemsKvsFirst tv_set'
-                     ; rep_tc_name <- newFamInstTyConName (noLoc (tyConName fam_tc)) pat_tys'
-                     ; let axiom = mkSingleCoAxiom rep_tc_name tvs' fam_tc pat_tys' rhs'
-                     ; traceTc "mk_deflt_at_instance" (vcat [ ppr (tyvars, theta, clas, inst_tys)
-                                                            , pprCoAxBranch fam_tc br
-                                                            , pprCoAxiom axiom ])
-                     ; ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' ) 
-                       newFamInst SynFamilyInst axiom }
-
-        ; tyfam_insts1 <- mapM mk_deflt_at_instances (classATItems clas)
+        ; let defined_ats = mkNameSet (map (tyFamInstDeclName . unLoc) ats)
+                            `unionNameSets` 
+                            mkNameSet (map (unLoc . dfid_tycon . unLoc) adts)
+        ; tyfam_insts1 <- mapM (tcATDefault mini_subst defined_ats) 
+                               (classATItems clas)
         
         -- Finally, construct the Core representation of the instance.
         -- (This no longer includes the associated types.)
@@ -585,6 +557,48 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
 
         ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts) }
 
+
+tcATDefault :: TvSubst -> NameSet -> ClassATItem -> TcM [FamInst]
+-- ^ Construct default instances for any associated types that
+-- aren't given a user definition
+-- Returns [] or singleton
+tcATDefault inst_subst defined_ats (ATI fam_tc defs)
+  -- User supplied instances ==> everything is OK
+  | tyConName fam_tc `elemNameSet` defined_ats
+  = return []
+
+  -- No user instance, have defaults ==> instatiate them
+   -- Example:   class C a where { type F a b :: *; type F a b = () }
+   --            instance C [x]
+   -- Then we want to generate the decl:   type F [x] b = ()
+  | Just rhs_ty <- defs
+  = do { let (subst', pat_tys') = mapAccumL subst_tv inst_subst
+                                            (tyConTyVars fam_tc)
+             rhs'     = substTy subst' rhs_ty
+             tv_set'  = tyVarsOfTypes pat_tys'
+             tvs'     = varSetElemsKvsFirst tv_set'
+       ; rep_tc_name <- newFamInstTyConName (noLoc (tyConName fam_tc)) pat_tys'
+       ; let axiom = mkSingleCoAxiom rep_tc_name tvs' fam_tc pat_tys' rhs'
+       ; traceTc "mk_deflt_at_instance" (vcat [ ppr fam_tc, ppr rhs_ty
+                                              , pprCoAxiom axiom ])
+       ; fam_inst <- ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' ) 
+                     newFamInst SynFamilyInst axiom
+       ; return [fam_inst] }
+
+   -- No defaults ==> generate a warning
+  | otherwise  -- defs = Nothing
+  = do { warnMissingMethodOrAT "associated type" (tyConName fam_tc)
+       ; return [] }
+  where
+    subst_tv subst tc_tv 
+      | Just ty <- lookupVarEnv (getTvSubstEnv subst) tc_tv
+      = (subst, ty)
+      | otherwise
+      = (extendTvSubst subst tc_tv ty', ty')
+      where
+        ty' = mkTyVarTy (updateTyVarKind (substTy subst) tc_tv)
+                           
+
 --------------
 tcAssocTyDecl :: Class                   -- Class of associated type
               -> VarEnv Type             -- Instantiation of class TyVars
@@ -633,7 +647,7 @@ tcTyFamInstDecl :: Maybe (Class, VarEnv Type) -- the class & mini_env if applica
 tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
   = setSrcSpan loc           $
     tcAddTyFamInstCtxt decl  $
-    do { let fam_lname = tfie_tycon (unLoc eqn)
+    do { let fam_lname = tfe_tycon (unLoc eqn)
        ; fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_lname
 
          -- (0) Check it's an open type family
@@ -642,14 +656,13 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
        ; checkTc (isOpenSynFamilyTyCon fam_tc) (notOpenFamily fam_tc)
 
          -- (1) do the work of verifying the synonym group
-       ; co_ax_branch <- tcSynFamInstDecl fam_tc decl
+       ; co_ax_branch <- tcTyFamInstEqn (famTyConShape fam_tc) eqn
 
          -- (2) check for validity
        ; checkValidTyFamInst mb_clsinfo fam_tc co_ax_branch
 
          -- (3) construct coercion axiom
-       ; rep_tc_name <- newFamInstAxiomName loc
-                                            (tyFamInstDeclName decl)
+       ; rep_tc_name <- newFamInstAxiomName loc (unLoc fam_lname)
                                             [co_ax_branch]
        ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
        ; newFamInst SynFamilyInst axiom }
@@ -672,7 +685,7 @@ tcDataFamInstDecl mb_clsinfo
        ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)
 
          -- Kind check type patterns
-       ; tcFamTyPats (unLoc fam_tc_name) (tyConKind fam_tc) pats
+       ; tcFamTyPats (famTyConShape fam_tc) pats
                      (kcDataDefn defn) $ 
            \tvs' pats' res_kind -> do
 
diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs
index 0836c327fb..281db25620 100644
--- a/compiler/typecheck/TcRnDriver.lhs
+++ b/compiler/typecheck/TcRnDriver.lhs
@@ -696,17 +696,14 @@ checkBootTyCon tc1 tc2
           (_, rho_ty2) = splitForAllTys (idType id2)
           op_ty2 = funResultTy rho_ty2
 
-       eqAT (tc1, def_ats1) (tc2, def_ats2)
+       eqAT (ATI tc1 def_ats1) (ATI tc2 def_ats2)
          = checkBootTyCon tc1 tc2 &&
-           eqListBy eqATDef def_ats1 def_ats2
+           eqATDef def_ats1 def_ats2
 
        -- Ignore the location of the defaults
-       eqATDef (CoAxBranch { cab_tvs = tvs1, cab_lhs =  ty_pats1, cab_rhs = ty1 })
-               (CoAxBranch { cab_tvs = tvs2, cab_lhs =  ty_pats2, cab_rhs = ty2 })
-         | Just env <- eqTyVarBndrs emptyRnEnv2 tvs1 tvs2
-         = eqListBy (eqTypeX env) ty_pats1 ty_pats2 &&
-           eqTypeX env ty1 ty2
-         | otherwise = False
+       eqATDef Nothing    Nothing    = True
+       eqATDef (Just ty1) (Just ty2) = eqTypeX env ty1 ty2
+       eqATDef _ _ = False           
 
        eqFD (as1,bs1) (as2,bs2) =
          eqListBy (eqTypeX env) (mkTyVarTys as1) (mkTyVarTys as2) &&
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index 8723d8bbee..f09bef8081 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -14,7 +14,7 @@ module TcTyClsDecls (
         -- Functions used by TcInstDcls to check
         -- data/type family instance declarations
         kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
-        tcSynFamInstDecl, tcFamTyPats,
+        tcFamTyPats, tcTyFamInstEqn, famTyConShape,
         tcAddTyFamInstCtxt, tcAddDataFamInstCtxt,
         wrongKindOfFamily, dataConCtxt, badDataConTyCon
     ) where
@@ -502,10 +502,12 @@ kcTyClDecl (ForeignType {}) = return ()
 
 -- closed type families look at their equations, but other families don't
 -- do anything here
-kcTyClDecl (FamDecl (FamilyDecl { fdLName = L _ fam_tc_name
-                                , fdInfo = ClosedTypeFamily eqns }))
-  = do { k <- kcLookupKind fam_tc_name
-       ; mapM_ (kcTyFamInstEqn fam_tc_name k) eqns }
+kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
+                                , fdTyVars = hs_tvs
+                                , fdInfo   = ClosedTypeFamily eqns }))
+  = do { tc_kind <- kcLookupKind fam_tc_name
+       ; let fam_tc_shape = ( fam_tc_name, length (hsQTvBndrs hs_tvs), tc_kind)
+       ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns }
 kcTyClDecl (FamDecl {})    = return ()
 
 -------------------
@@ -699,14 +701,11 @@ tcFamDecl1 parent
 
        ; 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
+         -- Process the equations, creating CoAxBranches
+       ; tc_kind <- kcLookupKind tc_name
+       ; let fam_tc_shape = (tc_name, length (hsQTvBndrs tvs), tc_kind) 
+     
+       ; branches <- mapM (tcTyFamInstEqn fam_tc_shape) eqns
 
          -- we need the tycon that we will be creating, but it's in scope.
          -- just look it up.
@@ -836,76 +835,90 @@ Note that:
   - We can get default definitions only for type families, not data families
 
 \begin{code}
-tcClassATs :: Name             -- The class name (not knot-tied)
-           -> TyConParent      -- The class parent of this associated type
-           -> [LFamilyDecl Name] -- Associated types.
-           -> [LTyFamInstDecl Name] -- Associated type defaults.
+tcClassATs :: Name                  -- The class name (not knot-tied)
+           -> TyConParent           -- The class parent of this associated type
+           -> [LFamilyDecl Name]    -- Associated types.
+           -> [LTyFamDefltEqn Name] -- Associated type defaults.
            -> TcM [ClassATItem]
 tcClassATs class_name parent ats at_defs
   = do {  -- Complain about associated type defaults for non associated-types
          sequence_ [ failWithTc (badATErr class_name n)
-                   | n <- map (tyFamInstDeclName . unLoc) at_defs
+                   | n <- map at_def_tycon at_defs
                    , not (n `elemNameSet` at_names) ]
        ; mapM tc_at ats }
   where
-    at_names = mkNameSet (map (unLoc . fdLName . unLoc) ats)
+    at_def_tycon :: LTyFamDefltEqn Name -> Name
+    at_def_tycon (L _ eqn) = unLoc (tfe_tycon eqn)
+
+    at_fam_name :: LFamilyDecl Name -> Name
+    at_fam_name (L _ decl) = unLoc (fdLName decl)
+
+    at_names = mkNameSet (map at_fam_name ats)
 
-    at_defs_map :: NameEnv [LTyFamInstDecl Name]
+    at_defs_map :: NameEnv [LTyFamDefltEqn Name]
     -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
     at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
-                                          (tyFamInstDeclName (unLoc at_def)) [at_def])
+                                          (at_def_tycon at_def) [at_def])
                         emptyNameEnv 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 <- mapM (tcDefaultAssocDecl fam_tc) at_defs
-                  ; return (fam_tc, atd) }
+                  ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at)
+                                  `orElse` []
+                  ; atd <- tcDefaultAssocDecl fam_tc at_defs
+                  ; return (ATI fam_tc atd) }
 
 -------------------------
-tcDefaultAssocDecl :: TyCon                -- ^ Family TyCon
-                   -> LTyFamInstDecl Name  -- ^ RHS
-                   -> TcM CoAxBranch       -- ^ Type checked RHS and free TyVars
-tcDefaultAssocDecl fam_tc (L loc decl)
+tcDefaultAssocDecl :: TyCon                  -- ^ Family TyCon
+                   -> [LTyFamDefltEqn Name]  -- ^ Defaults
+                   -> TcM (Maybe Type)       -- ^ Type checked RHS
+tcDefaultAssocDecl _ []
+  = return Nothing  -- No default declaration
+
+tcDefaultAssocDecl _ (d1:_:_)
+  = failWithTc (ptext (sLit "More than one default declaration for") 
+                <+> ppr (tfe_tycon (unLoc d1)))
+
+tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
+                                           , tfe_pats = hs_tvs
+                                           , tfe_rhs = rhs })]
   = setSrcSpan loc $
-    tcAddTyFamInstCtxt decl $
-    do { traceTc "tcDefaultAssocDecl" (ppr decl)
-       ; tcSynFamInstDecl fam_tc decl }
+    tcAddFamInstCtxt (ptext (sLit "default type instance")) tc_name $
+    tcTyClTyVars tc_name hs_tvs $ \ tvs rhs_kind ->
+    do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
+       ; checkTc (isSynFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
+       ; let (fam_name, fam_pat_arity, _) = famTyConShape fam_tc
+       ; ASSERT( fam_name == tc_name )
+         checkTc (length (hsQTvBndrs hs_tvs) == fam_pat_arity)
+                 (wrongNumberOfParmsErr fam_pat_arity)
+       ; rhs_ty <- tcCheckLHsType rhs rhs_kind
+       ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
+       ; let fam_tc_tvs = tyConTyVars fam_tc
+             subst = zipTopTvSubst tvs (mkTyVarTys fam_tc_tvs)
+       ; return ( ASSERT( equalLength fam_tc_tvs tvs )
+                  Just (substTy subst rhs_ty) ) }
     -- We check for well-formedness and validity later, in checkValidClass
 
 -------------------------
-tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM CoAxBranch
--- Placed here because type family instances appear as
--- default decls in class declarations
-tcSynFamInstDecl fam_tc (TyFamInstDecl { tfid_eqn = eqn })
-  = do { checkTc (isSynFamilyTyCon 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 ()
-tcSynFamInstNames (L _ first) names
-  = do { let badNames = filter ((/= first) . unLoc) names
-       ; mapM_ (failLocated (wrongNamesInInstGroup first)) badNames }
-  where
-    failLocated :: (Name -> SDoc) -> Located Name -> TcM ()
-    failLocated msg_fun (L loc name)
-      = setSrcSpan loc $
-        failWithTc (msg_fun name)
-
-kcTyFamInstEqn :: Name -> Kind -> LTyFamInstEqn Name -> TcM ()
-kcTyFamInstEqn fam_tc_name kind
-    (L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
+kcTyFamInstEqn :: FamTyConShape -> LTyFamInstEqn Name -> TcM ()
+kcTyFamInstEqn fam_tc_shape
+    (L loc (TyFamEqn { tfe_pats = pats, tfe_rhs = hs_ty }))
   = setSrcSpan loc $
     discardResult $
-    tc_fam_ty_pats fam_tc_name kind pats (discardResult . (tcCheckLHsType hs_ty))
-
-tcTyFamInstEqn :: Name -> Kind -> LTyFamInstEqn Name -> TcM CoAxBranch
-tcTyFamInstEqn fam_tc_name kind
-    (L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
+    tc_fam_ty_pats fam_tc_shape pats (discardResult . (tcCheckLHsType hs_ty))
+
+tcTyFamInstEqn :: FamTyConShape -> LTyFamInstEqn Name -> TcM CoAxBranch
+-- Needs to be here, not in TcInstDcls, because closed families
+-- (typechecked here) have TyFamInstEqns
+tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_)
+    (L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
+                     , tfe_pats = pats
+                     , tfe_rhs = hs_ty }))
   = setSrcSpan loc $
-    tcFamTyPats fam_tc_name kind pats (discardResult . (tcCheckLHsType hs_ty)) $
+    tcFamTyPats fam_tc_shape pats (discardResult . (tcCheckLHsType hs_ty)) $
        \tvs' pats' res_kind ->
-    do { rhs_ty <- tcCheckLHsType hs_ty res_kind
+    do { checkTc (fam_tc_name == eqn_tc_name) 
+                 (wrongTyFamName fam_tc_name eqn_tc_name)
+       ; rhs_ty <- tcCheckLHsType hs_ty res_kind
        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
        ; traceTc "tcTyFamInstEqn" (ppr fam_tc_name <+> ppr tvs')
           -- don't print out the pats here, as they might be zonked inside the knot
@@ -947,6 +960,19 @@ type families.
 tcFamTyPats type checks the patterns, zonks, and then calls thing_inside
 to generate a desugaring. It is used during type-checking (not kind-checking).
 
+Note [Type-checking type patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When typechecking the patterns of a family instance declaration, we can't
+rely on using the family TyCon, because this is sometimes called
+from within a type-checking knot. (Specifically for closed type families.)
+The type FamTyConShape gives just enough information to do the job.
+
+The "arity" field of FamTyConShape is the *visible* arity of the family
+type constructor, i.e. what the users sees and writes, not including kind
+arguments.
+
+See also Note [tc_fam_ty_pats vs tcFamTyPats]
+
 Note [Failing early in kcDataDefn]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We need to use checkNoErrs when calling kcConDecl. This is because kcConDecl
@@ -961,15 +987,18 @@ two bad things could happen:
 
 \begin{code}
 -----------------
--- 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.
--- See Note [tc_fam_ty_pats vs tcFamTyPats]
-tc_fam_ty_pats :: Name -- of the family TyCon
-               -> Kind -- of the family TyCon
+type FamTyConShape = (Name, Arity, Kind) -- See Note [Type-checking type patterns]
+
+famTyConShape :: TyCon -> FamTyConShape
+famTyConShape fam_tc
+  = ( tyConName fam_tc
+    , length (filterOut isKindVar (tyConTyVars fam_tc))
+    , tyConKind fam_tc )
+
+tc_fam_ty_pats :: FamTyConShape
                -> HsWithBndrs [LHsType Name] -- Patterns
-               -> (TcKind -> TcM ())       -- Kind checker for RHS
-                                           -- result is ignored
+               -> (TcKind -> TcM ())         -- Kind checker for RHS
+                                             -- result is ignored
                -> TcM ([Kind], [Type], Kind)
 -- Check the type patterns of a type or data family instance
 --     type instance F <pat1> <pat2> = <type>
@@ -982,7 +1011,7 @@ tc_fam_ty_pats :: Name -- of the family TyCon
 -- In that case, the type variable 'a' will *already be in scope*
 -- (and, if C is poly-kinded, so will its kind parameter).
 
-tc_fam_ty_pats fam_tc_name kind
+tc_fam_ty_pats (name, arity, kind)
                (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars })
                kind_checker
   = do { let (fam_kvs, fam_body) = splitForAllTys kind
@@ -994,9 +1023,8 @@ tc_fam_ty_pats fam_tc_name kind
          -- 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
+       ; checkTc (length arg_pats == arity) $
+         wrongNumberOfParmsErr arity
 
          -- Instantiate with meta kind vars
        ; fam_arg_kinds <- mapM (const newMetaKindVar) fam_kvs
@@ -1011,22 +1039,21 @@ tc_fam_ty_pats fam_tc_name kind
          -- See Note [Quantifying over family patterns]
        ; typats <- tcHsTyVarBndrs hs_tvs $ \ _ ->
                    do { kind_checker res_kind
-                      ; tcHsArgTys (quotes (ppr fam_tc_name)) arg_pats arg_kinds }
+                      ; tcHsArgTys (quotes (ppr name)) arg_pats arg_kinds }
 
        ; return (fam_arg_kinds, typats, res_kind) }
 
 -- See Note [tc_fam_ty_pats vs tcFamTyPats]
-tcFamTyPats :: Name -- of the family ToCon
-            -> Kind -- of the family TyCon
+tcFamTyPats :: FamTyConShape
             -> HsWithBndrs [LHsType Name] -- patterns
             -> (TcKind -> TcM ())         -- kind-checker for RHS
             -> ([TKVar]              -- Kind and type variables
                 -> [TcType]          -- Kind and type arguments
                 -> Kind -> TcM a)
             -> TcM a
-tcFamTyPats fam_tc_name kind pats kind_checker thing_inside
+tcFamTyPats fam_shape@(name,_,_) pats kind_checker thing_inside
   = do { (fam_arg_kinds, typats, res_kind)
-            <- tc_fam_ty_pats fam_tc_name kind pats kind_checker
+            <- tc_fam_ty_pats fam_shape pats kind_checker
        ; let all_args = fam_arg_kinds ++ typats
 
             -- Find free variables (after zonking) and turn
@@ -1040,7 +1067,7 @@ tcFamTyPats fam_tc_name kind pats kind_checker thing_inside
        ; all_args'    <- zonkTcTypeToTypes ze all_args
        ; res_kind'    <- zonkTcTypeToType  ze res_kind
 
-       ; traceTc "tcFamTyPats" (ppr fam_tc_name)
+       ; traceTc "tcFamTyPats" (ppr name)
             -- don't print out too much, as we might be in the knot
        ; tcExtendTyVarEnv qtkvs' $
          thing_inside qtkvs' all_args' res_kind' }
@@ -1484,16 +1511,19 @@ checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
 checkValidDataCon dflags existential_ok tc con
   = setSrcSpan (srcLocSpan (getSrcLoc con))     $
     addErrCtxt (dataConCtxt con)                $
-    do  { traceTc "checkValidDataCon" (ppr con $$ ppr tc)
-
-          -- Check that the return type of the data constructor
+    do  { -- Check that the return type of the data constructor
           -- matches the type constructor; eg reject this:
           --   data T a where { MkT :: Bogus a }
           -- c.f. Note [Check role annotations in a second pass]
           --  and Note [Checking GADT return types]
-        ; let tc_tvs = tyConTyVars tc
+          let tc_tvs = tyConTyVars tc
               res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
               orig_res_ty = dataConOrigResTy con
+        ; traceTc "checkValidDataCon" (vcat
+              [ ppr con, ppr tc, ppr tc_tvs
+              , ppr res_ty_tmpl <+> dcolon <+> ppr (typeKind res_ty_tmpl)
+              , ppr orig_res_ty <+> dcolon <+> ppr (typeKind orig_res_ty)])
+
         ; checkTc (isJust (tcMatchTy (mkVarSet tc_tvs)
                                      res_ty_tmpl
                                      orig_res_ty))
@@ -1645,15 +1675,10 @@ checkValidClass cls
                 -- in the context of a for-all must mention at least one quantified
                 -- type variable.  What a mess!
 
-    check_at_defs (fam_tc, defs)
+    check_at_defs (ATI fam_tc _)
       = do { traceTc "check-at" (ppr fam_tc $$ ppr (tyConTyVars fam_tc) $$ ppr tyvars)
            ; checkTc (any (`elem` tyvars) (tyConTyVars fam_tc)) 
-                     (noClassTyVarErr cls (ptext (sLit "associated type") <+> quotes (ppr fam_tc)))
-                     
-           ; tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $
-             mapM_ (checkValidTyFamInst mb_clsinfo fam_tc) defs }
-
-    mb_clsinfo = Just (cls, mkVarEnv [ (tv, mkTyVarTy tv) | tv <- tyvars ])
+                     (noClassTyVarErr cls (ptext (sLit "associated type") <+> quotes (ppr fam_tc))) }
 
 checkFamFlag :: Name -> TcM ()
 -- Check that we don't use families without -XTypeFamilies
@@ -2010,13 +2035,6 @@ gotten by appying the eq_spec to the univ_tvs of the data con.
 %************************************************************************
 
 \begin{code}
-tcAddDefaultAssocDeclCtxt :: Name -> TcM a -> TcM a
-tcAddDefaultAssocDeclCtxt name thing_inside
-  = addErrCtxt ctxt thing_inside
-  where
-     ctxt = hsep [ptext (sLit "In the type synonym instance default declaration for"),
-                  quotes (ppr name)]
-
 tcAddTyFamInstCtxt :: TyFamInstDecl Name -> TcM a -> TcM a
 tcAddTyFamInstCtxt decl
   = tcAddFamInstCtxt (ptext (sLit "type instance")) (tyFamInstDeclName decl)
@@ -2157,16 +2175,16 @@ 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")
+wrongNumberOfParmsErr :: Arity -> SDoc
+wrongNumberOfParmsErr max_args
+  = ptext (sLit "Number of parameters must match family declaration; expected")
     <+> ppr max_args
 
-wrongNamesInInstGroup :: Name -> Name -> SDoc
-wrongNamesInInstGroup first cur
-  = ptext (sLit "Mismatched type names in closed type family declaration.") $$
-    ptext (sLit "First name was") <+>
-    (ppr first) <> (ptext (sLit "; this one is")) <+> (ppr cur)
+wrongTyFamName :: Name -> Name -> SDoc
+wrongTyFamName fam_tc_name eqn_tc_name
+  = hang (ptext (sLit "Mismatched type name in type family instance."))
+       2 (vcat [ ptext (sLit "Expected:") <+> ppr fam_tc_name
+               , ptext (sLit "  Actual:") <+> ppr eqn_tc_name ])
 
 inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
 inaccessibleCoAxBranch tc fi
diff --git a/compiler/typecheck/TcValidity.lhs b/compiler/typecheck/TcValidity.lhs
index c7ba56c426..b5e6d64522 100644
--- a/compiler/typecheck/TcValidity.lhs
+++ b/compiler/typecheck/TcValidity.lhs
@@ -46,7 +46,6 @@ import ListSetOps
 import SrcLoc
 import Outputable
 import FastString
-import BasicTypes ( Arity )
 
 import Control.Monad
 import Data.Maybe
@@ -1165,26 +1164,18 @@ checkValidFamPats :: TyCon -> [TyVar] -> [Type] -> TcM ()
 --         type instance F (T a) = a
 -- c) Have the right number of patterns
 checkValidFamPats fam_tc tvs 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
+  = ASSERT( length ty_pats == tyConArity fam_tc )
+      -- 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)
+      -- But this is checked at the time the axiom is created
+    do { 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.
---
 checkTyFamFreeness :: Type -> TcM ()
 checkTyFamFreeness ty
   = checkTc (isTyFamFree ty) $
diff --git a/compiler/types/Class.lhs b/compiler/types/Class.lhs
index 29df06572b..9863b8d98f 100644
--- a/compiler/types/Class.lhs
+++ b/compiler/types/Class.lhs
@@ -17,7 +17,7 @@ The @Class@ datatype
 module Class (
 	Class,
         ClassOpItem, DefMeth (..),
-        ClassATItem,
+        ClassATItem(..),
         ClassMinimalDef,
 	defMethSpecOfDefMeth,
 
@@ -32,8 +32,7 @@ module Class (
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TyCon	( TyCon, tyConName, tyConUnique )
-import {-# SOURCE #-} TypeRep	( PredType )
-import CoAxiom
+import {-# SOURCE #-} TypeRep	( Type, PredType )
 import Var
 import Name
 import BasicTypes
@@ -100,10 +99,10 @@ data DefMeth = NoDefMeth 		-- No default method
 	     | GenDefMeth Name 		-- A generic default method
              deriving Eq
 
-type ClassATItem = (TyCon,           -- See Note [Associated type tyvar names]
-                    [CoAxBranch])    -- Default associated types from these templates 
-  -- We can have more than one default per type; see
-  -- Note [Associated type defaults] in TcTyClsDecls
+data ClassATItem
+  = ATI TyCon         -- See Note [Associated type tyvar names]
+        (Maybe Type)  -- Default associated type (if any) from this template
+                      -- Note [Associated type defaults]
 
 type ClassMinimalDef = BooleanFormula Name -- Required methods
 
@@ -115,9 +114,39 @@ defMethSpecOfDefMeth meth
 	NoDefMeth	-> NoDM
 	DefMeth _	-> VanillaDM
 	GenDefMeth _	-> GenericDM
-
 \end{code}
 
+Note [Associated type defaults]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The following is an example of associated type defaults:
+   class C a where
+     data D a r
+
+     type F x a b :: *
+     type F p q r = (p,q)->r    -- Default
+
+Note that
+
+ * The TyCons for the associated types *share type variables* with the
+   class, so that we can tell which argument positions should be
+   instantiated in an instance decl.  (The first for 'D', the second
+   for 'F'.)
+
+ * We can have default definitions only for *type* families,
+   not data families
+
+ * In the default decl, the "patterns" should all be type variables,
+   but (in the source language) they don't need to be the same as in
+   the 'type' decl signature or the class.  It's more like a
+   free-standing 'type instance' declaration.
+
+ * HOWEVER, in the internal ClassATItem we rename the RHS to match the
+   tyConTyVars of the family TyCon.  So in the example above we'd get
+   a ClassATItem of
+        ATI F ((x,a) -> b)
+   So the tyConTyVars of the family TyCon bind the free vars of
+   the default Type rhs
+
 The @mkClass@ function fills in the indirect superclasses.
 
 \begin{code}
@@ -198,7 +227,7 @@ classOpItems = classOpStuff
 
 classATs :: Class -> [TyCon]
 classATs (Class { classATStuff = at_stuff })
-  = [tc | (tc, _) <- at_stuff]
+  = [tc | ATI tc _ <- at_stuff]
 
 classATItems :: Class -> [ClassATItem]
 classATItems = classATStuff