Implement associated type defaults

Basically, now you can write:

  class Cls a where
    type Typ a
    type Typ a = Just a

And now if an instance does not specify an explicit associated type
instance, one will be generated afresh based on that default. So for
example this instance:

  instance Cls Int where

Will be equivalent to this one:

  instance Cls Int where
    type Typ Int = Just Int

18 files changed, 567 insertions, 355 deletions

diff --git a/compiler/basicTypes/OccName.lhs b/compiler/basicTypes/OccName.lhs
index 3ae9b54085..273a40e7d4 100644
--- a/compiler/basicTypes/OccName.lhs
+++ b/compiler/basicTypes/OccName.lhs
@@ -54,7 +54,7 @@ module OccName (
   	mkClassTyConOcc, mkClassDataConOcc, mkDictOcc, mkIPOcc, 
  	mkSpecOcc, mkForeignExportOcc, mkGenOcc1, mkGenOcc2,
  	mkGenD, mkGenR, mkGenRCo, mkGenC, mkGenS,
-	mkDataTOcc, mkDataCOcc, mkDataConWorkerOcc,
+        mkDataTOcc, mkDataCOcc, mkDataConWorkerOcc,
 	mkSuperDictSelOcc, mkLocalOcc, mkMethodOcc, mkInstTyTcOcc,
 	mkInstTyCoOcc, mkEqPredCoOcc,
         mkVectOcc, mkVectTyConOcc, mkVectDataConOcc, mkVectIsoOcc,
diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index 1d94cf68ee..fb5e223029 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -214,7 +214,7 @@ repTyClD (L loc (TySynonym { tcdLName = tc, tcdTyVars = tvs, tcdTyPats = opt_tys
 repTyClD (L loc (ClassDecl { tcdCtxt = cxt, tcdLName = cls, 
 		             tcdTyVars = tvs, tcdFDs = fds,
 		             tcdSigs = sigs, tcdMeths = meth_binds, 
-                             tcdATs = ats }))
+                             tcdATs = ats, tcdATDefs = [] }))
   = do { cls1 <- lookupLOcc cls 	-- See note [Binders and occurrences] 
        ; dec  <- addTyVarBinds tvs $ \bndrs -> 
            do { cxt1   <- repLContext cxt
diff --git a/compiler/hsSyn/Convert.lhs b/compiler/hsSyn/Convert.lhs
index f84776546a..90cf99d582 100644
--- a/compiler/hsSyn/Convert.lhs
+++ b/compiler/hsSyn/Convert.lhs
@@ -183,7 +183,7 @@ cvtDec (ClassD ctxt cl tvs fds decs)
 	; returnL $ 
             TyClD $ ClassDecl { tcdCtxt = cxt', tcdLName = tc', tcdTyVars = tvs'
 	    	              , tcdFDs = fds', tcdSigs = sigs', tcdMeths = binds'
-			      , tcdATs = ats', tcdDocs = [] }
+			      , tcdATs = ats', tcdATDefs = [], tcdDocs = [] }
                                         -- no docs in TH ^^
 	}
 	
diff --git a/compiler/hsSyn/HsDecls.lhs b/compiler/hsSyn/HsDecls.lhs
index 82f113c096..940e6a73c3 100644
--- a/compiler/hsSyn/HsDecls.lhs
+++ b/compiler/hsSyn/HsDecls.lhs
@@ -499,7 +499,9 @@ data TyClDecl name
 		tcdSigs    :: [LSig name],		-- ^ Methods' signatures
 		tcdMeths   :: LHsBinds name,		-- ^ Default methods
 		tcdATs	   :: [LTyClDecl name],		-- ^ Associated types; ie
-							--   only 'TyFamily' 
+							--   only 'TyFamily'
+                tcdATDefs  :: [LTyClDecl name],         -- ^ Associated type defaults; ie
+                                                        --   only 'TySynonym'
 		tcdDocs    :: [LDocDecl]		-- ^ Haddock docs
     }
   deriving (Data, Typeable)
@@ -646,14 +648,16 @@ instance OutputableBndr name
 	ppr_sigx (Just kind) = dcolon <+> pprKind kind
 
     ppr (ClassDecl {tcdCtxt = context, tcdLName = lclas, tcdTyVars = tyvars, 
-		    tcdFDs  = fds, 
-		    tcdSigs = sigs, tcdMeths = methods, tcdATs = ats})
-      | null sigs && null ats  -- No "where" part
+		    tcdFDs  = fds,
+                    tcdSigs = sigs, tcdMeths = methods,
+                    tcdATs = ats, tcdATDefs = at_defs})
+      | null sigs && isEmptyBag methods && null ats && null at_defs -- No "where" part
       = top_matter
 
       | otherwise	-- Laid out
       = vcat [ top_matter <+> ptext (sLit "where")
 	     , nest 2 $ pprDeclList (map ppr ats ++
+                                     map ppr at_defs ++
 			             pprLHsBindsForUser methods sigs) ]
       where
         top_matter = ptext (sLit "class") 
diff --git a/compiler/iface/BinIface.hs b/compiler/iface/BinIface.hs
index 26b3d9c886..c9c9918cdc 100644
--- a/compiler/iface/BinIface.hs
+++ b/compiler/iface/BinIface.hs
@@ -1456,6 +1456,21 @@ instance Binary IfaceConDecl where
 		a10 <- get bh
 	        return (IfCon a1 a2 a3 a4 a5 a6 a7 a8 a9 a10)
 
+instance Binary IfaceAT where
+    put_ bh (IfaceAT dec defs) = do
+            put_ bh dec
+            put_ bh defs
+    get bh = do dec <- get bh
+                defs <- get bh
+                return (IfaceAT dec defs)
+
+instance Binary IfaceATDefault where
+    put_ bh (IfaceATD tvs pat_tys ty) = do
+        put_ bh tvs
+        put_ bh pat_tys
+        put_ bh ty
+    get bh = liftM3 IfaceATD (get bh) (get bh) (get bh)
+
 instance Binary IfaceClassOp where
    put_ bh (IfaceClassOp n def ty) = do	
 	put_ bh (occNameFS n)
diff --git a/compiler/iface/BuildTyCl.lhs b/compiler/iface/BuildTyCl.lhs
index 7f2ade20cd..98fb19eb82 100644
--- a/compiler/iface/BuildTyCl.lhs
+++ b/compiler/iface/BuildTyCl.lhs
@@ -231,12 +231,12 @@ buildClass :: Bool		-- True <=> do not include unfoldings
 				-- Used when importing a class without -O
 	   -> Name -> [TyVar] -> ThetaType
 	   -> [FunDep TyVar]		   -- Functional dependencies
-	   -> [TyThing]			   -- Associated types
+	   -> [ClassATItem]		   -- Associated types
 	   -> [TcMethInfo]                 -- Method info
 	   -> RecFlag			   -- Info for type constructor
 	   -> TcRnIf m n Class
 
-buildClass no_unf class_name tvs sc_theta fds ats sig_stuff tc_isrec
+buildClass no_unf class_name tvs sc_theta fds at_items sig_stuff tc_isrec
   = do	{ traceIf (text "buildClass")
 	; tycon_name <- newImplicitBinder class_name mkClassTyConOcc
 	; datacon_name <- newImplicitBinder class_name mkClassDataConOcc
@@ -308,10 +308,9 @@ buildClass no_unf class_name tvs sc_theta fds ats sig_stuff tc_isrec
 		-- [If we don't make it a recursive newtype, we'll expand the
 		-- newtype like a synonym, but that will lead to an infinite
 		-- type]
-	      ; atTyCons = [tycon | ATyCon tycon <- ats]
 
 	      ; result = mkClass class_name tvs fds 
-			         sc_theta sc_sel_ids atTyCons
+			         sc_theta sc_sel_ids at_items
 				 op_items tycon
 	      }
 	; traceIf (text "buildClass" <+> ppr tycon) 
diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs
index eb09c2f10f..9e48480766 100644
--- a/compiler/iface/IfaceSyn.lhs
+++ b/compiler/iface/IfaceSyn.lhs
@@ -7,7 +7,8 @@
 module IfaceSyn (
         module IfaceType,
 
-        IfaceDecl(..), IfaceClassOp(..), IfaceConDecl(..), IfaceConDecls(..),
+        IfaceDecl(..), IfaceClassOp(..), IfaceAT(..), IfaceATDefault(..),
+        IfaceConDecl(..), IfaceConDecls(..),
         IfaceExpr(..), IfaceAlt, IfaceNote(..), IfaceLetBndr(..),
         IfaceBinding(..), IfaceConAlt(..),
         IfaceIdInfo(..), IfaceIdDetails(..), IfaceUnfolding(..),
@@ -87,7 +88,7 @@ data IfaceDecl
                  ifName    :: OccName,          -- Name of the class
                  ifTyVars  :: [IfaceTvBndr],    -- Type variables
                  ifFDs     :: [FunDep FastString], -- Functional dependencies
-                 ifATs     :: [IfaceDecl],      -- Associated type families
+                 ifATs     :: [IfaceAT],      -- Associated type families
                  ifSigs    :: [IfaceClassOp],   -- Method signatures
                  ifRec     :: RecFlag           -- Is newtype/datatype associated
                                                 --   with the class recursive?
@@ -102,6 +103,16 @@ data IfaceClassOp = IfaceClassOp OccName DefMethSpec IfaceType
         -- Just False => ordinary polymorphic default method
         -- Just True  => generic default method
 
+data IfaceAT = IfaceAT IfaceDecl [IfaceATDefault]
+        -- Nothing => no default associated type instance
+        -- Just ds => default associated type instance from these templates
+
+data IfaceATDefault = IfaceATD [IfaceTvBndr] [IfaceType] IfaceType
+        -- Each associated type default template is a triple of:
+        --   1. TyVars of the RHS and family arguments (including the class TVs)
+        --   3. The instantiated family arguments
+        --   2. The RHS of the synonym
+
 data IfaceConDecls
   = IfAbstractTyCon Bool        -- c.f TyCon.AbstractTyCon
   | IfOpenDataTyCon             -- Open data family
@@ -383,7 +394,7 @@ ifaceDeclSubBndrs (IfaceClass {ifCtxt = sc_ctxt, ifName = cls_occ,
     --    no wrapper (class dictionaries never have a wrapper)
     [dc_occ, dcww_occ] ++
     -- associated types
-    [ifName at | at <- ats ] ++
+    [ifName at | IfaceAT at _ <- ats ] ++
     -- superclass selectors
     [mkSuperDictSelOcc n cls_occ | n <- [1..n_ctxt]] ++
     -- operation selectors
@@ -466,6 +477,12 @@ pprFamily (Just famInst) = ptext (sLit "FamilyInstance:") <+> ppr famInst
 instance Outputable IfaceClassOp where
    ppr (IfaceClassOp n dm ty) = ppr n <+> ppr dm <+> dcolon <+> ppr ty
 
+instance Outputable IfaceAT where
+   ppr (IfaceAT d defs) = hang (ppr d) 2 (vcat (map ppr defs))
+
+instance Outputable IfaceATDefault where
+   ppr (IfaceATD tvs pat_tys ty) = ppr tvs <+> hsep (map ppr pat_tys) <+> char '=' <+> ppr ty
+
 pprIfaceDeclHead :: IfaceContext -> OccName -> [IfaceTvBndr] -> SDoc
 pprIfaceDeclHead context thing tyvars
   = hsep [pprIfaceContext context, parenSymOcc thing (ppr thing),
@@ -701,7 +718,7 @@ freeNamesIfDecl d@IfaceSyn{} =
 freeNamesIfDecl d@IfaceClass{} =
   freeNamesIfTvBndrs (ifTyVars d) &&&
   freeNamesIfContext (ifCtxt d) &&&
-  freeNamesIfDecls   (ifATs d) &&&
+  fnList freeNamesIfAT     (ifATs d) &&&
   fnList freeNamesIfClsSig (ifSigs d)
 
 freeNamesIfIdDetails :: IfaceIdDetails -> NameSet
@@ -722,8 +739,15 @@ freeNamesIfTcFam Nothing =
 freeNamesIfContext :: IfaceContext -> NameSet
 freeNamesIfContext = fnList freeNamesIfPredType
 
-freeNamesIfDecls :: [IfaceDecl] -> NameSet
-freeNamesIfDecls = fnList freeNamesIfDecl
+freeNamesIfAT :: IfaceAT -> NameSet
+freeNamesIfAT (IfaceAT decl defs)
+  = freeNamesIfDecl decl &&&
+    fnList fn_at_def defs
+  where
+    fn_at_def (IfaceATD tvs pat_tys ty)
+      = freeNamesIfTvBndrs tvs &&&
+        fnList freeNamesIfType pat_tys &&&
+        freeNamesIfType ty
 
 freeNamesIfClsSig :: IfaceClassOp -> NameSet
 freeNamesIfClsSig (IfaceClassOp _n _dm ty) = freeNamesIfType ty
diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs
index b73e00a731..b25d979970 100644
--- a/compiler/iface/MkIface.lhs
+++ b/compiler/iface/MkIface.lhs
@@ -744,7 +744,7 @@ declExtras fix_fn rule_env inst_env decl
                         (map (id_extras . ifConOcc) (visibleIfConDecls cons))
       IfaceClass{ifSigs=sigs, ifATs=ats} -> 
                      IfaceClassExtras (fix_fn n)
-                        (map ifDFun $ (concatMap (lookupOccEnvL inst_env . ifName) ats)
+                        (map ifDFun $ (concatMap at_extras ats)
                                     ++ lookupOccEnvL inst_env n)
 		           -- Include instances of the associated types
 			   -- as well as instances of the class (Trac #5147)
@@ -754,6 +754,7 @@ declExtras fix_fn rule_env inst_env decl
   where
         n = ifName decl
         id_extras occ = (fix_fn occ, lookupOccEnvL rule_env occ)
+        at_extras (IfaceAT decl _) = lookupOccEnvL inst_env (ifName decl)
 
 --
 -- When hashing an instance, we hash only the DFunId, because that
@@ -1330,7 +1331,7 @@ tyThingToIfaceDecl (AClass clas)
 		 ifName	  = getOccName clas,
 		 ifTyVars = toIfaceTvBndrs clas_tyvars,
 		 ifFDs    = map toIfaceFD clas_fds,
-		 ifATs	  = map (tyThingToIfaceDecl . ATyCon) clas_ats,
+		 ifATs	  = map toIfaceAT clas_ats,
 		 ifSigs	  = map toIfaceClassOp op_stuff,
 	  	 ifRec    = boolToRecFlag (isRecursiveTyCon tycon) }
   where
@@ -1338,6 +1339,14 @@ tyThingToIfaceDecl (AClass clas)
       = classExtraBigSig clas
     tycon = classTyCon clas
 
+    toIfaceAT :: ClassATItem -> IfaceAT
+    toIfaceAT (tc, defs)
+      = IfaceAT (tyThingToIfaceDecl (ATyCon tc))
+                (map to_if_at_def defs)
+      where
+        to_if_at_def (ATD tvs pat_tys ty)
+          = IfaceATD (toIfaceTvBndrs tvs) (map toIfaceType pat_tys) (toIfaceType ty)
+
     toIfaceClassOp (sel_id, def_meth)
 	= ASSERT(sel_tyvars == clas_tyvars)
 	  IfaceClassOp (getOccName sel_id) (toDmSpec def_meth) (toIfaceType op_ty)
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index d0ce1b7349..9fbb59bd3e 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -479,7 +479,7 @@ tc_iface_decl _parent ignore_prags
     ; sigs <- mapM tc_sig rdr_sigs
     ; fds  <- mapM tc_fd rdr_fds
     ; cls  <- fixM $ \ cls -> do
-              { ats  <- mapM (tc_iface_decl (AssocFamilyTyCon cls) ignore_prags) rdr_ats
+              { ats  <- mapM (tc_at cls) rdr_ats
               ; buildClass ignore_prags cls_name tyvars ctxt fds ats sigs tc_isrec }
     ; return (AClass cls) }
   where
@@ -491,6 +491,18 @@ tc_iface_decl _parent ignore_prags
 		-- it mentions unless it's necessray to do so
 	  ; return (op_name, dm, op_ty) }
 
+   tc_at cls (IfaceAT tc_decl defs_decls)
+     = do tc <- tc_iface_tc_decl (AssocFamilyTyCon cls) tc_decl
+          defs <- mapM tc_iface_at_def defs_decls
+          return (tc, defs)
+
+   tc_iface_tc_decl parent decl = do
+       ATyCon tc <- tc_iface_decl parent ignore_prags decl
+       return tc
+
+   tc_iface_at_def (IfaceATD tvs pat_tys ty) =
+       bindIfaceTyVars_AT tvs $ \tvs' -> liftM2 (ATD tvs') (mapM tcIfaceType pat_tys) (tcIfaceType ty)
+
    mk_doc op_name op_ty = ptext (sLit "Class op") <+> sep [ppr op_name, ppr op_ty]
 
    tc_fd (tvs1, tvs2) = do { tvs1' <- mapM tcIfaceTyVar tvs1
diff --git a/compiler/parser/RdrHsSyn.lhs b/compiler/parser/RdrHsSyn.lhs
index 468c4d5898..452a946602 100644
--- a/compiler/parser/RdrHsSyn.lhs
+++ b/compiler/parser/RdrHsSyn.lhs
@@ -73,7 +73,7 @@ import Maybes
 import Control.Applicative ((<$>))       
 import Control.Monad
 import Text.ParserCombinators.ReadP as ReadP
-import Data.List        ( nubBy )
+import Data.List        ( nubBy, partition )
 import Data.Char
 
 #include "HsVersions.h"
@@ -179,14 +179,15 @@ mkClassDecl :: SrcSpan
 	    -> P (LTyClDecl RdrName)
 
 mkClassDecl loc (L _ (mcxt, tycl_hdr)) fds where_cls
-  = do { let (binds, sigs, ats, docs) = cvBindsAndSigs (unLoc where_cls)
-       ; let cxt = fromMaybe (noLoc []) mcxt
+  = do { let (binds, sigs, at_stuff, docs) = cvBindsAndSigs (unLoc where_cls)
+             (at_defs, ats) = partition (isTypeDecl . unLoc) at_stuff
+             cxt = fromMaybe (noLoc []) mcxt
        ; (cls, tparams) <- checkTyClHdr tycl_hdr
        ; tyvars <- checkTyVars tycl_hdr tparams      -- Only type vars allowed
        ; checkKindSigs ats
        ; return (L loc (ClassDecl { tcdCtxt = cxt, tcdLName = cls, tcdTyVars = tyvars,
 		             	    tcdFDs = unLoc fds, tcdSigs = sigs, tcdMeths = binds,
-			     	    tcdATs   = ats, tcdDocs  = docs })) }
+			     	    tcdATs   = ats, tcdATDefs = at_defs, tcdDocs  = docs })) }
 
 mkTyData :: SrcSpan
          -> NewOrData
@@ -566,7 +567,7 @@ checkKindSigs = mapM_ check
   where
     check (L l tydecl) 
       | isFamilyDecl tydecl
-        || isSynDecl tydecl  = return ()
+        || isTypeDecl tydecl = return ()
       | otherwise	     = 
 	parseErrorSDoc l (text "Type declaration in a class must be a kind signature or synonym default:" $$ ppr tydecl)
 
diff --git a/compiler/rename/RnSource.lhs b/compiler/rename/RnSource.lhs
index 2f01d7d418..e404e5b718 100644
--- a/compiler/rename/RnSource.lhs
+++ b/compiler/rename/RnSource.lhs
@@ -787,12 +787,13 @@ rnTyClDecl mb_cls tydecl@(TySynonym { tcdTyVars = tyvars, tcdLName = name,
 
 rnTyClDecl _ (ClassDecl {tcdCtxt = context, tcdLName = lcls, 
 		         tcdTyVars = tyvars, tcdFDs = fds, tcdSigs = sigs, 
-		         tcdMeths = mbinds, tcdATs = ats, tcdDocs = docs})
+		         tcdMeths = mbinds, tcdATs = ats, tcdATDefs = at_defs,
+                         tcdDocs = docs})
   = do	{ lcls' <- lookupLocatedTopBndrRn lcls
         ; let cls' = unLoc lcls'
 
 	-- Tyvars scope over superclass context and method signatures
-	; ((tyvars', context', fds', ats', sigs'), stuff_fvs)
+	; ((tyvars', context', fds', ats', at_defs', sigs'), stuff_fvs)
 	    <- bindTyVarsFV tyvars $ \ tyvars' -> do
          	 -- Checks for distinct tyvars
 	     { context' <- rnContext cls_doc context
@@ -800,11 +801,13 @@ rnTyClDecl _ (ClassDecl {tcdCtxt = context, tcdLName = lcls,
              ; let rn_at = rnTyClDecl (Just cls')
              ; (ats', fv_ats) <- mapAndUnzipM (wrapLocFstM rn_at) ats
 	     ; sigs' <- renameSigs Nothing okClsDclSig sigs
+             ; (at_defs', fv_at_defs) <- mapAndUnzipM (wrapLocFstM rn_at) at_defs
 	     ; let fvs = extractHsCtxtTyNames context'	`plusFV`
 	                 hsSigsFVs sigs'                `plusFV`
-                         plusFVs fv_ats
+                         plusFVs fv_ats                 `plusFV`
+                         plusFVs fv_at_defs
 			 -- The fundeps have no free variables
-	     ; return ((tyvars', context', fds', ats', sigs'), fvs) }
+	     ; return ((tyvars', context', fds', ats', at_defs', sigs'), fvs) }
 
 	-- No need to check for duplicate associated type decls
 	-- since that is done by RnNames.extendGlobalRdrEnvRn
@@ -838,7 +841,8 @@ rnTyClDecl _ (ClassDecl {tcdCtxt = context, tcdLName = lcls,
 
 	; return (ClassDecl { tcdCtxt = context', tcdLName = lcls', 
 			      tcdTyVars = tyvars', tcdFDs = fds', tcdSigs = sigs',
-			      tcdMeths = mbinds', tcdATs = ats', tcdDocs = docs'},
+			      tcdMeths = mbinds', tcdATs = ats', tcdATDefs = at_defs',
+                              tcdDocs = docs'},
 	     	  meth_fvs `plusFV` stuff_fvs) }
   where
     cls_doc  = text "In the declaration for class" <+> ppr lcls
diff --git a/compiler/typecheck/TcClassDcl.lhs b/compiler/typecheck/TcClassDcl.lhs
index 1d12c33c8a..6ceb7231e9 100644
--- a/compiler/typecheck/TcClassDcl.lhs
+++ b/compiler/typecheck/TcClassDcl.lhs
@@ -8,7 +8,7 @@ Typechecking class declarations
 \begin{code}
 module TcClassDcl ( tcClassSigs, tcClassDecl2, 
 		    findMethodBind, instantiateMethod, tcInstanceMethodBody,
-		    mkGenericDefMethBind,
+                    mkGenericDefMethBind,
 		    tcAddDeclCtxt, badMethodErr
 		  ) where
 
diff --git a/compiler/typecheck/TcEnv.lhs b/compiler/typecheck/TcEnv.lhs
index 9550232805..3b6b073742 100644
--- a/compiler/typecheck/TcEnv.lhs
+++ b/compiler/typecheck/TcEnv.lhs
@@ -714,8 +714,8 @@ Make a name for the representation tycon of a family instance.  It's an
 newGlobalBinder.
 
 \begin{code}
-newFamInstTyConName :: Name -> [Type] -> SrcSpan -> TcM Name
-newFamInstTyConName tc_name tys loc
+newFamInstTyConName :: Located Name -> [Type] -> TcM Name
+newFamInstTyConName (L loc tc_name) tys
   = do	{ mod   <- getModule
 	; let info_string = occNameString (getOccName tc_name) ++ 
 			    concatMap (occNameString.getDFunTyKey) tys
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index 5049cba8fb..52d2c59751 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -30,13 +30,13 @@ import TcHsType
 import TcUnify
 import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
 import Type
-import Coercion
+import Coercion hiding (substTy)
 import TyCon
 import DataCon
 import Class
 import Var
 import VarEnv
-import VarSet     ( mkVarSet )
+import VarSet     ( mkVarSet, varSetElems )
 import Pair
 import CoreUtils  ( mkPiTypes )
 import CoreUnfold ( mkDFunUnfolding )
@@ -455,15 +455,36 @@ tcLocalInstDecl1 (L loc (InstDecl poly_ty binds uprags ats))
         ; let mini_env = mkVarEnv (classTyVars clas `zip` inst_tys)
 
         -- Next, process any associated types.
-        ; idx_tycons <- tcExtendTyVarEnv tyvars $
+        ; traceTc "tcLocalInstDecl" (ppr poly_ty)
+        ; idx_tycons0 <- tcExtendTyVarEnv tyvars $
                         mapAndRecoverM (tcAssocDecl clas mini_env) ats
 
-        -- Check for misssing associated types
-        ; let class_ats   = map tyConName (classATs clas)
-              defined_ats = mkNameSet $ map (tcdName . unLoc) ats
-              omitted     = filterOut (`elemNameSet` defined_ats) class_ats
+        -- Check for misssing associated types and build them
+        -- from their defaults (if available)
+        ; let defined_ats = mkNameSet $ map (tcdName . unLoc) ats
+              check_at_instance (fam_tc, defs)
+                 -- User supplied instances ==> everything is OK
+                | tyConName fam_tc `elemNameSet` defined_ats = return (Nothing, [])
+                 -- No defaults ==> generate a warning
+                | null defs                                  = return (Just (tyConName fam_tc), [])
+                 -- No user instance, have defaults ==> instatiate them
+                | otherwise = do
+                    defs' <- forM defs $ \(ATD tvs pat_tys rhs) -> do
+                      let mini_env_subst = mkTvSubst (mkInScopeSet (mkVarSet tvs)) mini_env
+                          tvs' = varSetElems (tyVarsOfType rhs')
+                          pat_tys' = substTys mini_env_subst pat_tys
+                          rhs' = substTy mini_env_subst rhs
+                      rep_tc_name <- newFamInstTyConName (noLoc (tyConName fam_tc)) pat_tys'
+                      buildSynTyCon rep_tc_name tvs'
+                                    (SynonymTyCon rhs')
+                                    (mkArrowKinds (map tyVarKind tvs') (typeKind rhs'))
+                                    NoParentTyCon (Just (fam_tc, pat_tys'))
+                    return (Nothing, defs')
+        ; missing_at_stuff <- mapM check_at_instance (classATItems clas)
+        
+        ; let (omitted, idx_tycons1) = unzip missing_at_stuff
         ; warn <- woptM Opt_WarnMissingMethods
-        ; mapM_ (warnTc warn . omittedATWarn) omitted
+        ; mapM_ (warnTc warn . omittedATWarn) (catMaybes omitted)
 
         -- Finally, construct the Core representation of the instance.
         -- (This no longer includes the associated types.)
@@ -475,239 +496,7 @@ tcLocalInstDecl1 (L loc (InstDecl poly_ty binds uprags ats))
               ispec 	= mkLocalInstance dfun overlap_flag
               inst_info = InstInfo { iSpec  = ispec, iBinds = VanillaInst binds uprags False }
 
-        ; return (inst_info, idx_tycons) }
-
-tcAssocDecl :: Class -> VarEnv Type -> LTyClDecl Name -> TcM TyCon
-tcAssocDecl clas mini_env (L loc decl)
-  = setSrcSpan loc      $
-    tcAddDeclCtxt decl  $
-    do { at_tc <- tcFamInstDecl NotTopLevel decl
-       ; let Just (fam_tc, at_tys) = tyConFamInst_maybe at_tc
-  
-       -- Check that the associated type comes from this class
-       ; checkTc (Just clas == tyConAssoc_maybe fam_tc)
-                 (badATErr clas at_tc)
-
-       -- See Note [Checking consistent instantiation]
-       ; zipWithM_ check_arg (tyConTyVars fam_tc) at_tys
-
-       ; return at_tc }
-  where
-    check_arg fam_tc_tv at_ty
-      | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
-      = checkTc (inst_ty `eqType` at_ty) 
-                (wrongATArgErr at_ty inst_ty)
-      | otherwise 
-      = return ()   -- Allow non-type-variable instantiation
-      	       	    -- See Note [Associated type instances]
-\end{code}
-
-Note [Associated type instances]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We allow this:
-  class C a where
-    type T x a
-  instance C Int where
-    type T (S y) Int = y
-    type T Z     Int = Char
-
-Note that 
-  a) The variable 'x' is not bound by the class decl
-  b) 'x' is instantiated to a non-type-variable in the instance
-  c) There are several type instance decls for T in the instance
-
-All this is fine.  Of course, you can't give any *more* instances
-for (T ty Int) elsewhere, becuase it's an *associated* type.
-
-Note [Checking consistent instantiation]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  class C a b where
-    type T a x b
-
-  instance C [p] Int
-    type T [p] y Int = (p,y,y)  -- Induces the family instance TyCon
-    	       	       		--    type TR p y = (p,y,y)
-
-So we 
-  * Form the mini-envt from the class type variables a,b
-    to the instance decl types [p],Int:   [a->[p], b->Int]
-
-  * Look at the tyvars a,x,b of the type family constructor T
-    (it shares tyvars with the class C)
-
-  * Apply the mini-evnt to them, and check that the result is
-    consistent with the instance types [p] y Int
-
-
-%************************************************************************
-%*                                                                      *
-               Type checking family instances
-%*                                                                      *
-%************************************************************************
-
-Family instances are somewhat of a hybrid.  They are processed together with
-class instance heads, but can contain data constructors and hence they share a
-lot of kinding and type checking code with ordinary algebraic data types (and
-GADTs).
-
-\begin{code}
-tcTopFamInstDecl :: LTyClDecl Name -> TcM TyCon
-tcTopFamInstDecl (L loc decl)
-  = setSrcSpan loc      $
-    tcAddDeclCtxt decl  $
-    tcFamInstDecl TopLevel decl
-
-tcFamInstDecl :: TopLevelFlag -> TyClDecl Name -> TcM TyCon
--- TopLevel  => top-level
--- NotTopLevel => in an instance decl
-tcFamInstDecl top_lvl decl
-  = do { -- type family instances require -XTypeFamilies
-         -- and can't (currently) be in an hs-boot file
-       ; let fam_tc_lname = tcdLName decl
-       ; type_families <- xoptM Opt_TypeFamilies
-       ; is_boot <- tcIsHsBoot   -- Are we compiling an hs-boot file?
-       ; checkTc type_families $ badFamInstDecl fam_tc_lname
-       ; checkTc (not is_boot) $ badBootFamInstDeclErr
-
-       -- Look up the family TyCon and check for validity including
-       -- check that toplevel type instances are not for associated types.
-       ; fam_tc <- tcLookupLocatedTyCon fam_tc_lname
-       ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
-       ; when (isTopLevel top_lvl && isTyConAssoc fam_tc)
-              (addErr $ assocInClassErr fam_tc_lname)
-
-         -- Now check the type/data instance itself
-	 -- This is where type and data decls are treated separately
-       ; tc <- tcFamInstDecl1 fam_tc decl
-       ; checkValidTyCon tc     -- Remember to check validity;
-                                -- no recursion to worry about here
-
-       ; return tc }
-
-tcFamInstDecl1 :: TyCon -> TyClDecl Name -> TcM TyCon
-
-  -- "type instance"
-tcFamInstDecl1 fam_tc (decl@TySynonym {tcdLName = L loc tc_name})
-  = kcIdxTyPats fam_tc decl $ \k_tvs k_typats resKind ->
-    do { -- check that the family declaration is for a synonym
-         checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
-
-       ; -- (1) kind check the right-hand side of the type equation
-       ; k_rhs <- kcCheckLHsType (tcdSynRhs decl) (EK resKind EkUnk)
-                  -- ToDo: the ExpKind could be better
-
-         -- we need the exact same number of type parameters as the family
-         -- declaration
-       ; let famArity = tyConArity fam_tc
-       ; checkTc (length k_typats == famArity) $
-                 wrongNumberOfParmsErr famArity
-
-         -- (2) type check type equation
-       ; tcTyVarBndrs k_tvs $ \t_tvs -> do   -- turn kinded into proper tyvars
-       { t_typats <- mapM tcHsKindedType k_typats
-       ; t_rhs    <- tcHsKindedType k_rhs
-
-         -- (3) check the well-formedness of the instance
-       ; checkValidTypeInst t_typats t_rhs
-
-         -- (4) construct representation tycon
-       ; rep_tc_name <- newFamInstTyConName tc_name t_typats loc
-       ; buildSynTyCon rep_tc_name t_tvs
-                       (SynonymTyCon t_rhs)
-                       (typeKind t_rhs)
-                       NoParentTyCon (Just (fam_tc, t_typats))
-       }}
-
-  -- "newtype instance" and "data instance"
-tcFamInstDecl1 fam_tc (decl@TyData { tcdND = new_or_data
-                                   , tcdLName = L loc tc_name
-                                   , tcdCons = cons})
-  = kcIdxTyPats fam_tc decl $ \k_tvs k_typats resKind ->
-    do { -- check that the family declaration is for the right kind
-         checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
-       ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)
-
-       ; -- (1) kind check the data declaration as usual
-       ; k_decl <- kcDataDecl decl k_tvs
-       ; let k_ctxt = tcdCtxt k_decl
-             k_cons = tcdCons k_decl
-
-         -- result kind must be '*' (otherwise, we have too few patterns)
-       ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr (tyConArity fam_tc)
-
-         -- (2) type check indexed data type declaration
-       ; tcTyVarBndrs k_tvs $ \t_tvs -> do   -- turn kinded into proper tyvars
-
-         -- kind check the type indexes and the context
-       { t_typats     <- mapM tcHsKindedType k_typats
-       ; stupid_theta <- tcHsKindedContext k_ctxt
-
-         -- (3) Check that
-         --     (a) left-hand side contains no type family applications
-         --         (vanilla synonyms are fine, though, and we checked for
-         --         foralls earlier)
-       ; mapM_ checkTyFamFreeness t_typats
-
-       ; dataDeclChecks tc_name new_or_data stupid_theta k_cons
-
-         -- (4) construct representation tycon
-       ; rep_tc_name <- newFamInstTyConName tc_name t_typats loc
-       ; let ex_ok = True       -- Existentials ok for type families!
-       ; fixM (\ rep_tycon -> do
-             { let orig_res_ty = mkTyConApp fam_tc t_typats
-             ; data_cons <- tcConDecls ex_ok rep_tycon
-                                       (t_tvs, orig_res_ty) k_cons
-             ; tc_rhs <-
-                 case new_or_data of
-                   DataType -> return (mkDataTyConRhs data_cons)
-                   NewType  -> ASSERT( not (null data_cons) )
-                               mkNewTyConRhs rep_tc_name rep_tycon (head data_cons)
-             ; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive
-                             h98_syntax NoParentTyCon (Just (fam_tc, t_typats))
-                 -- We always assume that indexed types are recursive.  Why?
-                 -- (1) Due to their open nature, we can never be sure that a
-                 -- further instance might not introduce a new recursive
-                 -- dependency.  (2) They are always valid loop breakers as
-                 -- they involve a coercion.
-             })
-       }}
-       where
-         h98_syntax = case cons of      -- All constructors have same shape
-                        L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
-                        _ -> True
-
-tcFamInstDecl1 _ d = pprPanic "tcFamInstDecl1" (ppr d)
-
--- Kind checking of indexed types
--- -
-
--- Kind check type patterns and kind annotate the embedded type variables.
---
--- * Here we check that a type instance matches its kind signature, but we do
---   not check whether there is a pattern for each type index; the latter
---   check is only required for type synonym instances.
-
-kcIdxTyPats :: TyCon
-            -> TyClDecl Name
-            -> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TcM a)
-               -- ^^kinded tvs         ^^kinded ty pats  ^^res kind
-            -> TcM a
-kcIdxTyPats fam_tc decl thing_inside
-  = kcHsTyVars (tcdTyVars decl) $ \tvs ->
-    do { let { (kinds, resKind) = splitKindFunTys (tyConKind fam_tc)
-             ; hs_typats        = fromJust $ tcdTyPats decl }
-
-         -- We may not have more parameters than the kind indicates
-       ; checkTc (length kinds >= length hs_typats) $
-                 tooManyParmsErr (tcdLName decl)
-
-         -- Type functions can have a higher-kinded result
-       ; let resultKind = mkArrowKinds (drop (length hs_typats) kinds) resKind
-       ; typats <- zipWithM kcCheckLHsType hs_typats
-                            [ EK kind (EkArg (ppr fam_tc) n)
-                            | (kind,n) <- kinds `zip` [1..]]
-       ; thing_inside tvs typats resultKind 
-       }
+        ; return (inst_info, idx_tycons0 ++ concat idx_tycons1) }
 \end{code}
 
 
@@ -752,7 +541,7 @@ use.  But, unusually, when compiling instance decls we *copy* the
 INLINE pragma from the default method to the method for that
 particular operation (see Note [INLINE and default methods] below).
 
-So right here in tcInstDecl2 we must re-extend the type envt with
+So right here in tcInstDecls2 we must re-extend the type envt with
 the default method Ids replete with their INLINE pragmas.  Urk.
 
 \begin{code}
@@ -1359,62 +1148,6 @@ instDeclCtxt2 dfun_ty
 inst_decl_ctxt :: SDoc -> SDoc
 inst_decl_ctxt doc = ptext (sLit "In the instance declaration for") <+> quotes doc
 
-wrongATArgErr :: Type -> Type -> SDoc
-wrongATArgErr ty instTy =
-  sep [ ptext (sLit "Type indexes must match class instance head")
-      , ptext (sLit "Found") <+> quotes (ppr ty)
-        <+> ptext (sLit "but expected") <+> quotes (ppr instTy)
-      ]
-
-tooManyParmsErr :: Located Name -> SDoc
-tooManyParmsErr tc_name
-  = ptext (sLit "Family instance has too many parameters:") <+>
-    quotes (ppr tc_name)
-
-tooFewParmsErr :: Arity -> SDoc
-tooFewParmsErr arity
-  = ptext (sLit "Family instance has too few parameters; expected") <+>
-    ppr arity
-
-wrongNumberOfParmsErr :: Arity -> SDoc
-wrongNumberOfParmsErr exp_arity
-  = ptext (sLit "Number of parameters must match family declaration; expected")
-    <+> ppr exp_arity
-
-badBootFamInstDeclErr :: SDoc
-badBootFamInstDeclErr
-  = ptext (sLit "Illegal family instance in hs-boot file")
-
-notFamily :: TyCon -> SDoc
-notFamily tycon
-  = vcat [ ptext (sLit "Illegal family instance for") <+> quotes (ppr tycon)
-         , nest 2 $ parens (ppr tycon <+> ptext (sLit "is not an indexed type family"))]
-
-wrongKindOfFamily :: TyCon -> SDoc
-wrongKindOfFamily family
-  = ptext (sLit "Wrong category of family instance; declaration was for a")
-    <+> kindOfFamily
-  where
-    kindOfFamily | isSynTyCon family = ptext (sLit "type synonym")
-                 | isAlgTyCon family = ptext (sLit "data type")
-                 | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
-
-assocInClassErr :: Located Name -> SDoc
-assocInClassErr name
- = ptext (sLit "Associated type") <+> quotes (ppr name) <+>
-   ptext (sLit "must be inside a class instance")
-
-badFamInstDecl :: Located Name -> SDoc
-badFamInstDecl tc_name
-  = vcat [ ptext (sLit "Illegal family instance for") <+>
-	   quotes (ppr tc_name)
-	 , nest 2 (parens $ ptext (sLit "Use -XTypeFamilies to allow indexed type families")) ]
-
-badATErr :: Class -> TyCon -> SDoc
-badATErr clas at
-  = hsep [ptext (sLit "Class"), quotes (ppr clas), 
-	  ptext (sLit "does not have an associated type"), quotes (ppr at)]
-
 omittedATWarn :: Name -> SDoc
 omittedATWarn at
   = ptext (sLit "No explicit AT declaration for") <+> quotes (ppr at)
diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs
index f5d99b4f1d..62ccade16b 100644
--- a/compiler/typecheck/TcRnDriver.lhs
+++ b/compiler/typecheck/TcRnDriver.lhs
@@ -717,6 +717,16 @@ checkBootDecl (AClass c1)  (AClass c2)
 	  (_, rho_ty2) = splitForAllTys (idType id2)
           op_ty2 = funResultTy rho_ty2
 
+       eqAT (tc1, def_ats1) (tc2, def_ats2)
+         = checkBootTyCon tc1 tc2 &&
+           eqListBy eqATDef def_ats1 def_ats2
+
+       eqATDef (ATD tvs1 ty_pats1 ty1) (ATD tvs2 ty_pats2 ty2)
+         = eqListBy same_kind tvs1 tvs2 &&
+           eqListBy (eqTypeX env) ty_pats1 ty_pats2 &&
+           eqTypeX env ty1 ty2
+         where env = rnBndrs2 env0 tvs1 tvs2
+
        eqFD (as1,bs1) (as2,bs2) = 
          eqListBy (eqTypeX env) (mkTyVarTys as1) (mkTyVarTys as2) &&
          eqListBy (eqTypeX env) (mkTyVarTys bs1) (mkTyVarTys bs2)
@@ -730,7 +740,7 @@ checkBootDecl (AClass c1)  (AClass c2)
         ||   -- Above tests for an "abstract" class
         eqListBy (eqPredX env) sc_theta1 sc_theta2 &&
         eqListBy eqSig op_stuff1 op_stuff2 &&
-        eqListBy checkBootTyCon ats1 ats2)
+        eqListBy eqAT ats1 ats2) 
 
 checkBootDecl (ADataCon dc1) (ADataCon _)
   = pprPanic "checkBootDecl" (ppr dc1)
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index 93d0f5dcbc..7a4ec752cb 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -8,6 +8,7 @@ TcTyClsDecls: Typecheck type and class declarations
 \begin{code}
 module TcTyClsDecls (
 	tcTyAndClassDecls, kcDataDecl, tcConDecls, mkRecSelBinds,
+        tcTopFamInstDecl, tcAssocDecl,
         checkValidTyCon, dataDeclChecks
     ) where
 
@@ -34,7 +35,9 @@ import MkCore		( rEC_SEL_ERROR_ID )
 import IdInfo
 import Var
 import VarSet
+import VarEnv
 import Name
+import NameSet
 import NameEnv
 import Outputable
 import Maybes
@@ -407,8 +410,10 @@ kcFamilyDecl classTvs decl@(TyFamily {tcdKind = kind})
       | otherwise = return ()
     classTyKinds = [hsTyVarNameKind tv | L _ tv <- classTvs]
 
-kcFamilyDecl _ (TySynonym {})              -- type family defaults
-  = panic "TcTyClsDecls.kcFamilyDecl: not implemented yet"
+kcFamilyDecl _ decl@(TySynonym {})
+  = return decl
+   -- We don't have to do anything here for type family defaults:
+   -- tcClassATs will use tcAssocDecl to check them
 kcFamilyDecl _ d = pprPanic "kcFamilyDecl" (ppr d)
 \end{code}
 
@@ -509,7 +514,7 @@ tcTyClDecl1 _parent calc_isrec
 tcTyClDecl1 _parent calc_isrec 
   (ClassDecl {tcdLName = L _ class_name, tcdTyVars = tvs, 
 	      tcdCtxt = ctxt, tcdMeths = meths,
-	      tcdFDs = fundeps, tcdSigs = sigs, tcdATs = ats} )
+	      tcdFDs = fundeps, tcdSigs = sigs, tcdATs = ats, tcdATDefs = at_defs} )
   = ASSERT( isNoParent _parent )
     tcTyVarBndrs tvs		$ \ tvs' -> do 
   { ctxt' <- tcHsKindedContext ctxt
@@ -521,11 +526,15 @@ tcTyClDecl1 _parent calc_isrec
 			-- need to look up its recursiveness
 		    tycon_name = tyConName (classTyCon clas)
 		    tc_isrec = calc_isrec tycon_name
-	    ; atss' <- mapM (addLocM $ tcTyClDecl1 (AssocFamilyTyCon clas) (const Recursive)) ats
-            -- NB: 'ats' only contains "type family" and "data family"
-            --     declarations as well as type family defaults
+            ; traceTc "tcTyClDecl1:before ATs" (ppr class_name)
+
+            ; at_stuff <- tcClassATs clas tvs' ats at_defs
+            -- NB: 'ats' only contains "type family" and "data family" declarations
+            -- and 'at_defs' only contains associated-type defaults
+            ; traceTc "tcTyClDecl1:before build class" (ppr class_name)
+
             ; buildClass False {- Must include unfoldings for selectors -}
-			 class_name tvs' ctxt' fds' (concat atss')
+			 class_name tvs' ctxt' fds' at_stuff
 			 sig_stuff tc_isrec }
 
   ; let gen_dm_ids = [ AnId (mkExportedLocalId gen_dm_name gen_dm_ty)
@@ -552,7 +561,310 @@ tcTyClDecl1 _ _
   = return [ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0)]
 
 tcTyClDecl1 _ _ d = pprPanic "tcTyClDecl1" (ppr d)
+\end{code}
+
+\begin{code}
+tcClassATs :: Class            -- The class
+           -> [TyVar]          -- Class type variables (can't look them up in class b/c its knot-tied)
+           -> [LTyClDecl Name] -- Associated types. All FamTyCon
+           -> [LTyClDecl Name] -- Associated type defaults. All SynTyCon
+           -> TcM [ClassATItem]
+tcClassATs clas clas_tvs ats at_defs = do
+    sequence_ [ failWithTc (badATErr clas n)
+              | n <- map (tcdName . unLoc) at_defs, not (n `elemNameSet` at_names) ]
+              -- Associated type defaults for non associated-types
+    mapM tc_at ats
+  where
+    at_names = mkNameSet (map (tcdName . unLoc) ats)
+    at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv (tcdName (unLoc at_def)) [at_def]) emptyNameEnv at_defs
+
+    tc_at at = do 
+        [ATyCon fam_tc] <- addLocM (tcTyClDecl1 (AssocFamilyTyCon clas) (const Recursive)) at
+        atd <- case lookupNameEnv at_defs_map (tyConName fam_tc) of
+                 Nothing        -> return []
+                 Just def_decls -> mapM (fmap (uncurry3 ATD) . tcDefaultAssocDecl fam_tc clas_tvs) def_decls
+        return (fam_tc, atd)
+\end{code}
+
+Note [Associated type instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We allow this:
+  class C a where
+    type T x a
+  instance C Int where
+    type T (S y) Int = y
+    type T Z     Int = Char
+
+Note that 
+  a) The variable 'x' is not bound by the class decl
+  b) 'x' is instantiated to a non-type-variable in the instance
+  c) There are several type instance decls for T in the instance
+
+All this is fine.  Of course, you can't give any *more* instances
+for (T ty Int) elsewhere, becuase it's an *associated* type.
+
+Note [Checking consistent instantiation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  class C a b where
+    type T a x b
+
+  instance C [p] Int
+    type T [p] y Int = (p,y,y)  -- Induces the family instance TyCon
+                                --    type TR p y = (p,y,y)
+
+So we 
+  * Form the mini-envt from the class type variables a,b
+    to the instance decl types [p],Int:   [a->[p], b->Int]
+
+  * Look at the tyvars a,x,b of the type family constructor T
+    (it shares tyvars with the class C)
+
+  * Apply the mini-evnt to them, and check that the result is
+    consistent with the instance types [p] y Int
+
+
+%************************************************************************
+%*                                                                      *
+               Type checking family instances
+%*                                                                      *
+%************************************************************************
+
+Family instances are somewhat of a hybrid.  They are processed together with
+class instance heads, but can contain data constructors and hence they share a
+lot of kinding and type checking code with ordinary algebraic data types (and
+GADTs).
+
+\begin{code}
+-- Kind checking of indexed types
+-- -
 
+-- Kind check type patterns and kind annotate the embedded type variables.
+--
+-- * Here we check that a type instance matches its kind signature, but we do
+--   not check whether there is a pattern for each type index; the latter
+--   check is only required for type synonym instances.
+
+kcIdxTyPats :: TyCon
+            -> TyClDecl Name
+            -> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TcM a)
+               -- ^^kinded tvs         ^^kinded ty pats  ^^res kind
+            -> TcM a
+kcIdxTyPats fam_tc decl thing_inside
+  = kcHsTyVars (tcdTyVars decl) $ \tvs ->
+    do { let { (kinds, resKind) = splitKindFunTys (tyConKind fam_tc)
+             ; hs_typats        = fromJust $ tcdTyPats decl }
+
+         -- We may not have more parameters than the kind indicates
+       ; checkTc (length kinds >= length hs_typats) $
+                 tooManyParmsErr (tcdLName decl)
+
+         -- Type functions can have a higher-kinded result
+       ; let resultKind = mkArrowKinds (drop (length hs_typats) kinds) resKind
+       ; typats <- zipWithM kcCheckLHsType hs_typats
+                            [ EK kind (EkArg (ppr fam_tc) n)
+                            | (kind,n) <- kinds `zip` [1..]]
+       ; thing_inside tvs typats resultKind 
+       }
+
+
+tcTopFamInstDecl :: LTyClDecl Name -> TcM TyCon
+tcTopFamInstDecl (L loc decl)
+  = setSrcSpan loc      $
+    tcAddDeclCtxt decl  $
+    tcFamInstDecl TopLevel decl
+
+tcFamInstDecl :: TopLevelFlag -> TyClDecl Name -> TcM TyCon
+tcFamInstDecl top_lvl decl
+  = do { -- type family instances require -XTypeFamilies
+         -- and can't (currently) be in an hs-boot file
+       ; let fam_tc_lname = tcdLName decl
+       ; type_families <- xoptM Opt_TypeFamilies
+       ; is_boot <- tcIsHsBoot   -- Are we compiling an hs-boot file?
+       ; checkTc type_families $ badFamInstDecl fam_tc_lname
+       ; checkTc (not is_boot) $ badBootFamInstDeclErr
+
+       -- Look up the family TyCon and check for validity including
+       -- check that toplevel type instances are not for associated types.
+       ; fam_tc <- tcLookupLocatedTyCon fam_tc_lname
+       ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
+       ; when (isTopLevel top_lvl && isTyConAssoc fam_tc)
+              (addErr $ assocInClassErr fam_tc_lname)
+
+         -- Now check the type/data instance itself
+         -- This is where type and data decls are treated separately
+       ; tc <- tcFamInstDecl1 fam_tc decl
+       ; checkValidTyCon tc     -- Remember to check validity;
+                                -- no recursion to worry about here
+
+       ; return tc }
+
+tcFamInstDecl1 :: TyCon -> TyClDecl Name -> TcM TyCon
+
+  -- "type instance"
+tcFamInstDecl1 fam_tc (decl@TySynonym {})
+  = do { -- (1) do the work of verifying the synonym
+       ; (t_tvs, t_typats, t_rhs) <- tcFamSynInstDecl1 fam_tc decl
+
+         -- (2) check the well-formedness of the instance
+       ; checkValidTypeInst t_typats t_rhs
+
+         -- (3) construct representation tycon
+       ; rep_tc_name <- newFamInstTyConName (tcdLName decl) t_typats
+       ; buildSynTyCon rep_tc_name t_tvs
+                       (SynonymTyCon t_rhs)
+                       (typeKind t_rhs)
+                       NoParentTyCon (Just (fam_tc, t_typats))
+       }
+
+  -- "newtype instance" and "data instance"
+tcFamInstDecl1 fam_tc (decl@TyData { tcdND = new_or_data
+                                   , tcdCons = cons})
+  = kcIdxTyPats fam_tc decl $ \k_tvs k_typats resKind ->
+    do { -- check that the family declaration is for the right kind
+         checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
+       ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)
+
+       ; -- (1) kind check the data declaration as usual
+       ; k_decl <- kcDataDecl decl k_tvs
+       ; let k_ctxt = tcdCtxt k_decl
+             k_cons = tcdCons k_decl
+
+         -- result kind must be '*' (otherwise, we have too few patterns)
+       ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr (tyConArity fam_tc)
+
+         -- (2) type check indexed data type declaration
+       ; tcTyVarBndrs k_tvs $ \t_tvs -> do   -- turn kinded into proper tyvars
+
+         -- kind check the type indexes and the context
+       { t_typats     <- mapM tcHsKindedType k_typats
+       ; stupid_theta <- tcHsKindedContext k_ctxt
+
+         -- (3) Check that
+         --     (a) left-hand side contains no type family applications
+         --         (vanilla synonyms are fine, though, and we checked for
+         --         foralls earlier)
+       ; mapM_ checkTyFamFreeness t_typats
+
+       ; dataDeclChecks (tcdName decl) new_or_data stupid_theta k_cons
+
+         -- (4) construct representation tycon
+       ; rep_tc_name <- newFamInstTyConName (tcdLName decl) t_typats
+       ; let ex_ok = True       -- Existentials ok for type families!
+       ; fixM (\ rep_tycon -> do
+             { let orig_res_ty = mkTyConApp fam_tc t_typats
+             ; data_cons <- tcConDecls ex_ok rep_tycon
+                                       (t_tvs, orig_res_ty) k_cons
+             ; tc_rhs <-
+                 case new_or_data of
+                   DataType -> return (mkDataTyConRhs data_cons)
+                   NewType  -> ASSERT( not (null data_cons) )
+                               mkNewTyConRhs rep_tc_name rep_tycon (head data_cons)
+             ; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive
+                             h98_syntax NoParentTyCon (Just (fam_tc, t_typats))
+                 -- We always assume that indexed types are recursive.  Why?
+                 -- (1) Due to their open nature, we can never be sure that a
+                 -- further instance might not introduce a new recursive
+                 -- dependency.  (2) They are always valid loop breakers as
+                 -- they involve a coercion.
+             })
+       }}
+       where
+         h98_syntax = case cons of      -- All constructors have same shape
+                        L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
+                        _ -> True
+
+tcFamInstDecl1 _ d = pprPanic "tcFamInstDecl1" (ppr d)
+
+
+tcFamSynInstDecl1 :: TyCon -> TyClDecl Name -> TcM ([TyVar], [Type], Type)
+tcFamSynInstDecl1 fam_tc (decl@TySynonym {})
+  = kcIdxTyPats fam_tc decl $ \k_tvs k_typats resKind ->
+    do { -- check that the family declaration is for a synonym
+         checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
+
+       ; -- (1) kind check the right-hand side of the type equation
+       ; k_rhs <- kcCheckLHsType (tcdSynRhs decl) (EK resKind EkUnk)
+                  -- ToDo: the ExpKind could be better
+
+         -- we need the exact same number of type parameters as the family
+         -- declaration
+       ; let famArity = tyConArity fam_tc
+       ; checkTc (length k_typats == famArity) $
+                 wrongNumberOfParmsErr famArity
+
+         -- (2) type check type equation
+       ; tcTyVarBndrs k_tvs $ \t_tvs -> do   -- turn kinded into proper tyvars
+       { t_typats <- mapM tcHsKindedType k_typats
+       ; t_rhs    <- tcHsKindedType k_rhs
+
+        -- NB: we don't check well-formedness of the instance here because we call
+        -- this function from within the TcTyClsDecls fixpoint. The callers must do
+        -- the check.
+
+       ; return (t_tvs, t_typats, t_rhs) }}
+tcFamSynInstDecl1 _ decl = pprPanic "tcFamSynInstDecl1" (ppr decl)
+\end{code}
+
+%************************************************************************
+%*                                                                      *
+               Type checking associated family instances
+%*                                                                      *
+%************************************************************************
+
+This stuff used to be in TcInstDcls but has to be in here since we reuse
+this code to type check default associated type instances, and we don't
+want to form a loop by importing stuff from TcInstDcls.
+
+\begin{code}
+tcAssocDecl :: Class           -- ^ Class of associated type
+            -> VarEnv Type     -- ^ Instantiation of class TyVars
+            -> LTyClDecl Name  -- ^ RHS
+            -> TcM TyCon
+tcAssocDecl clas mini_env (L loc decl)
+  = setSrcSpan loc      $
+    tcAddDeclCtxt decl  $
+    do { at_tc <- tcFamInstDecl NotTopLevel decl
+       ; let Just (fam_tc, at_tys) = tyConFamInst_maybe at_tc
+  
+       -- Check that the associated type comes from this class
+       ; checkTc (Just clas == tyConAssoc_maybe fam_tc)
+                 (badATErr clas (tyConName at_tc))
+
+       -- See Note [Checking consistent instantiation]
+       ; zipWithM_ check_arg (tyConTyVars fam_tc) at_tys
+
+       ; return at_tc }
+  where
+    check_arg fam_tc_tv at_ty
+      | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
+      = checkTc (inst_ty `eqType` at_ty) 
+                (wrongATArgErr at_ty inst_ty)
+      | otherwise
+      = return ()   -- Allow non-type-variable instantiation
+                    -- See Note [Associated type instances]
+
+tcDefaultAssocDecl :: TyCon                       -- ^ Family TyCon
+                   -> [TyVar]                     -- ^ TyVars of associated type's class
+                   -> LTyClDecl Name              -- ^ RHS
+                   -> TcM ([TyVar], [Type], Type) -- ^ Type checked RHS and free TyVars
+tcDefaultAssocDecl fam_tc clas_tvs (L loc decl)
+  = setSrcSpan loc      $
+    tcAddDeclCtxt decl  $
+    do { (at_tvs, at_tys, at_rhs) <- tcFamSynInstDecl1 fam_tc decl
+       
+       -- See Note [Checking consistent instantiation]
+       -- We only want to check this on the *class* TyVars,
+       -- not the *family* TyVars (there may be more of these)
+       ; zipWithM_ check_arg clas_tvs at_tys
+
+       ; return (at_tvs, at_tys, at_rhs) }
+  where
+    check_arg fam_tc_tv at_ty
+      = checkTc (mkTyVarTy fam_tc_tv `eqType` at_ty) 
+                (wrongATArgErr at_ty (mkTyVarTy fam_tc_tv))
+\end{code}
+
+\begin{code}
 dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl Name] -> TcM ()
 dataDeclChecks tc_name new_or_data stupid_theta cons
   = do {   -- Check that we don't use GADT syntax in H98 world
@@ -966,13 +1278,16 @@ checkValidClass cls
 	-- Check the class operations
 	; mapM_ (check_op constrained_class_methods) op_stuff
 
+        -- Check the associated type defaults are well-formed
+        ; mapM_ check_at at_stuff
+
   	-- Check that if the class has generic methods, then the
 	-- class has only one parameter.  We can't do generic
 	-- multi-parameter type classes!
 	; checkTc (unary || no_generics) (genericMultiParamErr cls)
 	}
   where
-    (tyvars, fundeps, theta, _, _, op_stuff) = classExtraBigSig cls
+    (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
     unary 	= isSingleton tyvars
     no_generics = null [() | (_, (GenDefMeth _)) <- op_stuff]
 
@@ -1014,6 +1329,9 @@ checkValidClass cls
 		-- in the context of a for-all must mention at least one quantified
 		-- type variable.  What a mess!
 
+    check_at (_fam_tc, defs)
+      = mapM_ (\(ATD _tvs pats rhs) -> checkValidTypeInst pats rhs) defs
+
 checkFamFlag :: Name -> TcM ()
 -- Check that we don't use families without -XTypeFamilies
 -- The parser won't even parse them, but I suppose a GHC API
@@ -1306,6 +1624,11 @@ badDataConTyCon data_con res_ty_tmpl actual_res_ty
 		ptext (sLit "returns type") <+> quotes (ppr actual_res_ty))
        2 (ptext (sLit "instead of an instance of its parent type") <+> quotes (ppr res_ty_tmpl))
 
+badATErr :: Outputable a => a -> Name -> SDoc
+badATErr clas op
+  = hsep [ptext (sLit "Class"), quotes (ppr clas), 
+          ptext (sLit "does not have an associated type"), quotes (ppr op)]
+
 badGadtDecl :: Name -> SDoc
 badGadtDecl tc_name
   = vcat [ ptext (sLit "Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
@@ -1356,4 +1679,55 @@ emptyConDeclsErr :: Name -> SDoc
 emptyConDeclsErr tycon
   = sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"),
 	 nest 2 $ ptext (sLit "(-XEmptyDataDecls permits this)")]
+
+wrongATArgErr :: Type -> Type -> SDoc
+wrongATArgErr ty instTy =
+  sep [ ptext (sLit "Type indexes must match class instance head")
+      , ptext (sLit "Found") <+> quotes (ppr ty)
+        <+> ptext (sLit "but expected") <+> quotes (ppr instTy)
+      ]
+
+tooManyParmsErr :: Located Name -> SDoc
+tooManyParmsErr tc_name
+  = ptext (sLit "Family instance has too many parameters:") <+>
+    quotes (ppr tc_name)
+
+tooFewParmsErr :: Arity -> SDoc
+tooFewParmsErr arity
+  = ptext (sLit "Family instance has too few parameters; expected") <+>
+    ppr arity
+
+wrongNumberOfParmsErr :: Arity -> SDoc
+wrongNumberOfParmsErr exp_arity
+  = ptext (sLit "Number of parameters must match family declaration; expected")
+    <+> ppr exp_arity
+
+badBootFamInstDeclErr :: SDoc
+badBootFamInstDeclErr
+  = ptext (sLit "Illegal family instance in hs-boot file")
+
+notFamily :: TyCon -> SDoc
+notFamily tycon
+  = vcat [ ptext (sLit "Illegal family instance for") <+> quotes (ppr tycon)
+         , nest 2 $ parens (ppr tycon <+> ptext (sLit "is not an indexed type family"))]
+
+wrongKindOfFamily :: TyCon -> SDoc
+wrongKindOfFamily family
+  = ptext (sLit "Wrong category of family instance; declaration was for a")
+    <+> kindOfFamily
+  where
+    kindOfFamily | isSynTyCon family = ptext (sLit "type synonym")
+                 | isAlgTyCon family = ptext (sLit "data type")
+                 | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
+
+assocInClassErr :: Located Name -> SDoc
+assocInClassErr name
+ = ptext (sLit "Associated type") <+> quotes (ppr name) <+>
+   ptext (sLit "must be inside a class instance")
+
+badFamInstDecl :: Located Name -> SDoc
+badFamInstDecl tc_name
+  = vcat [ ptext (sLit "Illegal family instance for") <+>
+           quotes (ppr tc_name)
+         , nest 2 (parens $ ptext (sLit "Use -XTypeFamilies to allow indexed type families")) ]
 \end{code}
diff --git a/compiler/types/Class.lhs b/compiler/types/Class.lhs
index 6489a2fdac..9464e5cd0b 100644
--- a/compiler/types/Class.lhs
+++ b/compiler/types/Class.lhs
@@ -7,14 +7,15 @@ The @Class@ datatype
 
 \begin{code}
 module Class (
-	Class, ClassOpItem, 
-	DefMeth (..),
+	Class,
+        ClassOpItem, DefMeth (..),
+        ClassATItem, ATDefault (..),
 	defMethSpecOfDefMeth,
 
 	FunDep,	pprFundeps, pprFunDep,
 
 	mkClass, classTyVars, classArity, 
-	classKey, className, classATs, classTyCon, classMethods,
+	classKey, className, classATs, classATItems, classTyCon, classMethods,
 	classOpItems, classBigSig, classExtraBigSig, classTvsFds, classSCTheta,
         classAllSelIds, classSCSelId
     ) where
@@ -23,7 +24,7 @@ module Class (
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TyCon	( TyCon )
-import {-# SOURCE #-} TypeRep	( PredType )
+import {-# SOURCE #-} TypeRep	( Type, PredType )
 
 import Var
 import Name
@@ -62,7 +63,7 @@ data Class
 		     			--   superclasses from a 
 					--   dictionary of this class
 	-- Associated types
-        classATs     :: [TyCon],	-- Associated type families
+        classATStuff :: [ClassATItem],	-- Associated type families
 
         -- Class operations (methods, not superclasses)
 	classOpStuff :: [ClassOpItem],	-- Ordered by tag
@@ -76,13 +77,24 @@ type FunDep a = ([a],[a])  --  e.g. class C a b c | a b -> c, a c -> b where...
 			   --  Here fun-deps are [([a,b],[c]), ([a,c],[b])]
 
 type ClassOpItem = (Id, DefMeth)
-	-- Selector function; contains unfolding
+        -- Selector function; contains unfolding
 	-- Default-method info
 
 data DefMeth = NoDefMeth 		-- No default method
 	     | DefMeth Name  		-- A polymorphic default method
 	     | GenDefMeth Name 		-- A generic default method
-             deriving Eq  
+             deriving Eq
+
+type ClassATItem = (TyCon, [ATDefault])
+  -- Default associated types from these templates. If the template list is empty,
+  -- we assume that there is no default -- not that the default is to generate no
+  -- instances (this only makes a difference for warnings).
+
+data ATDefault = ATD [TyVar] [Type] Type
+  -- Each associated type default template is a triple of:
+  --   1. TyVars of the RHS and family arguments (including the class TVs)
+  --   3. The instantiated family arguments
+  --   2. The RHS of the synonym
 
 -- | Convert a `DefMethSpec` to a `DefMeth`, which discards the name field in
 --   the `DefMeth` constructor of the `DefMeth`.
@@ -101,12 +113,12 @@ The @mkClass@ function fills in the indirect superclasses.
 mkClass :: Name -> [TyVar]
 	-> [([TyVar], [TyVar])]
 	-> [PredType] -> [Id]
-	-> [TyCon]
+	-> [ClassATItem]
 	-> [ClassOpItem]
 	-> TyCon
 	-> Class
 
-mkClass name tyvars fds super_classes superdict_sels ats 
+mkClass name tyvars fds super_classes superdict_sels at_stuff
 	op_stuff tycon
   = Class {	classKey     = getUnique name, 
 		className    = name,
@@ -114,7 +126,7 @@ mkClass name tyvars fds super_classes superdict_sels ats
 		classFunDeps = fds,
 		classSCTheta = super_classes,
 		classSCSels  = superdict_sels,
-		classATs     = ats,
+		classATStuff = at_stuff,
 		classOpStuff = op_stuff,
 		classTyCon   = tycon }
 \end{code}
@@ -150,8 +162,14 @@ classMethods (Class {classOpStuff = op_stuff})
   = [op_sel | (op_sel, _) <- op_stuff]
 
 classOpItems :: Class -> [ClassOpItem]
-classOpItems (Class { classOpStuff = op_stuff})
-  = op_stuff
+classOpItems = classOpStuff
+
+classATs :: Class -> [TyCon]
+classATs (Class { classATStuff = at_stuff })
+  = [tc | (tc, _) <- at_stuff]
+
+classATItems :: Class -> [ClassATItem]
+classATItems = classATStuff
 
 classTvsFds :: Class -> ([TyVar], [FunDep TyVar])
 classTvsFds c
@@ -162,10 +180,10 @@ classBigSig (Class {classTyVars = tyvars, classSCTheta = sc_theta,
 	 	    classSCSels = sc_sels, classOpStuff = op_stuff})
   = (tyvars, sc_theta, sc_sels, op_stuff)
 
-classExtraBigSig :: Class -> ([TyVar], [FunDep TyVar], [PredType], [Id], [TyCon], [ClassOpItem])
+classExtraBigSig :: Class -> ([TyVar], [FunDep TyVar], [PredType], [Id], [ClassATItem], [ClassOpItem])
 classExtraBigSig (Class {classTyVars = tyvars, classFunDeps = fundeps,
 			 classSCTheta = sc_theta, classSCSels = sc_sels,
-			 classATs = ats, classOpStuff = op_stuff})
+			 classATStuff = ats, classOpStuff = op_stuff})
   = (tyvars, fundeps, sc_theta, sc_sels, ats, op_stuff)
 \end{code}
 
diff --git a/compiler/utils/Util.lhs b/compiler/utils/Util.lhs
index c5f1c0c2ed..ef36e8a9e3 100644
--- a/compiler/utils/Util.lhs
+++ b/compiler/utils/Util.lhs
@@ -32,6 +32,7 @@ module Util (
 
         -- * Tuples
         fstOf3, sndOf3, thirdOf3,
+        uncurry3,
 
         -- * List operations controlled by another list
         takeList, dropList, splitAtList, split,
@@ -44,7 +45,7 @@ module Util (
         sortLe, sortWith, minWith, on,
 
         -- * Comparisons
-        isEqual, eqListBy,
+        isEqual, eqListBy, eqMaybeBy,
         thenCmp, cmpList,
         removeSpaces,
         
@@ -208,6 +209,9 @@ thirdOf3 :: (a,b,c) -> c
 fstOf3      (a,_,_) =  a
 sndOf3      (_,b,_) =  b
 thirdOf3    (_,_,c) =  c
+
+uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
+uncurry3 f (a, b, c) = f a b c
 \end{code}
 
 %************************************************************************
@@ -677,6 +681,11 @@ eqListBy _  []     []     = True
 eqListBy eq (x:xs) (y:ys) = eq x y && eqListBy eq xs ys
 eqListBy _  _      _      = False
 
+eqMaybeBy :: (a ->a->Bool) -> Maybe a -> Maybe a -> Bool
+eqMaybeBy _  Nothing  Nothing  = True
+eqMaybeBy eq (Just x) (Just y) = eq x y
+eqMaybeBy _  _        _        = False
+
 cmpList :: (a -> a -> Ordering) -> [a] -> [a] -> Ordering
     -- `cmpList' uses a user-specified comparer