Entirely re-jig the handling of default type-family instances (fixes Trac #9063)
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 15 Jul 2014 06:43:55 +0000 (07:43 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 15 Jul 2014 06:43:55 +0000 (07:43 +0100)
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.

38 files changed:
compiler/deSugar/DsMeta.hs
compiler/hsSyn/Convert.lhs
compiler/hsSyn/HsDecls.lhs
compiler/iface/IfaceSyn.lhs
compiler/iface/MkIface.lhs
compiler/iface/TcIface.lhs
compiler/parser/RdrHsSyn.lhs
compiler/rename/RnSource.lhs
compiler/typecheck/TcDeriv.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcRnDriver.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/typecheck/TcValidity.lhs
compiler/types/Class.lhs
docs/users_guide/glasgow_exts.xml
testsuite/tests/indexed-types/should_fail/Overlap4.stderr
testsuite/tests/indexed-types/should_fail/Overlap5.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail1a.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr
testsuite/tests/parser/should_fail/T8506.stderr
testsuite/tests/parser/should_fail/readFail025.stderr
testsuite/tests/polykinds/Makefile
testsuite/tests/polykinds/T7939a.stderr
testsuite/tests/polykinds/T9063.hs [new file with mode: 0644]
testsuite/tests/polykinds/T9263.hs [new file with mode: 0644]
testsuite/tests/polykinds/T9263a.hs [new file with mode: 0644]
testsuite/tests/polykinds/T9263b.hs [new file with mode: 0644]
testsuite/tests/polykinds/T9264.hs [new file with mode: 0644]
testsuite/tests/polykinds/all.T
testsuite/tests/typecheck/should_compile/T5481.stderr
testsuite/tests/typecheck/should_compile/tc253.hs
testsuite/tests/typecheck/should_fail/AssocTyDef02.stderr
testsuite/tests/typecheck/should_fail/AssocTyDef03.stderr
testsuite/tests/typecheck/should_fail/AssocTyDef04.stderr
testsuite/tests/typecheck/should_fail/AssocTyDef05.stderr
testsuite/tests/typecheck/should_fail/AssocTyDef06.stderr
utils/haddock

index 435f5c7..adfc0f6 100644 (file)
@@ -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 $ \ _ ->
index 122be81..e22af3b 100644 (file)
@@ -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]
index d35a7e5..845c052 100644 (file)
@@ -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
index 7b202ac..935b8ed 100644 (file)
@@ -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
index b4d36ae..460c607 100644 (file)
@@ -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)
index 14eb723..68f9e8f 100644 (file)
@@ -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
index af351b7..93a98d0 100644 (file)
@@ -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 "= ...")
 
index dae9d81..9bc0e44 100644 (file)
@@ -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',
index aa15a63..d18c21c 100644 (file)
@@ -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
index ed682df..c3ba825 100644 (file)
@@ -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
 
index 0836c32..281db25 100644 (file)
@@ -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) &&
index 8723d8b..f09bef8 100644 (file)
@@ -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
index c7ba56c..b5e6d64 100644 (file)
@@ -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) $
index 29df065..9863b8d 100644 (file)
@@ -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
index f1d7b94..42e04fc 100644 (file)
@@ -6024,28 +6024,39 @@ instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
   data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
   ...
 
-instance (Eq (Elem [e])) => Collects ([e]) where
+instance Eq (Elem [e]) => Collects [e] where
   type Elem [e] = e
   ...
 </programlisting>
-        The most important point about associated family instances is that the
-        type indexes corresponding to class parameters must be identical to
-        the type given in the instance head; here this is the first argument
-        of <literal>GMap</literal>, namely <literal>Either a b</literal>,
-        which coincides with the only class parameter.
-      </para>
-      <para>
-       Instances for an associated family can only appear as part of
-       instance declarations of the class in which the family was declared -
-       just as with the equations of the methods of a class.  Also in
-       correspondence to how methods are handled, declarations of associated
-       types can be omitted in class instances.  If an associated family
-       instance is omitted, the corresponding instance type is not inhabited;
+Note the following points:
+<itemizedlist>
+<listitem><para>
+        The type indexes corresponding to class parameters must have precisely the same shape
+        the type given in the instance head.  To have the same "shape" means that
+        the two types are identical modulo renaming of type variables. For example:
+<programlisting>
+instance Eq (Elem [e]) => Collects [e] where
+  -- Choose one of the following alternatives:
+  type Elem [e] = e       -- OK
+  type Elem [x] = x       -- OK
+  type Elem x   = x       -- BAD; shape of 'x' is different to '[e]'
+  type Elem [Maybe x] = x -- BAD: shape of '[Maybe x]' is different to '[e]'
+</programlisting>
+</para></listitem>
+<listitem><para>
+       An instances for an associated family can only appear as part of
+       an instance declarations of the class in which the family was declared,
+       just as with the equations of the methods of a class.
+</para></listitem>
+<listitem><para>
+     The instance for an associated type can be omitted in class instances.  In that case,
+     unless there is a default instance (see <xref linkend="assoc-decl-defs"/>), 
+     the corresponding instance type is not inhabited;
        i.e., only diverging expressions, such
        as <literal>undefined</literal>, can assume the type.
-      </para>
-      <para>
-        Although it is unusual, there can be <emphasis>multiple</emphasis>
+</para></listitem>
+<listitem><para>
+        Although it is unusual, there (currently) can be <emphasis>multiple</emphasis>
         instances for an associated family in a single instance declaration.
         For example, this is legitimate:
 <programlisting>
@@ -6059,8 +6070,10 @@ instance GMapKey Flob where
         Since you cannot give any <emphasis>subsequent</emphasis> instances for
         <literal>(GMap Flob ...)</literal>, this facility is most useful when
         the free indexed parameter is of a kind with a finite number of alternatives
-        (unlike <literal>*</literal>).
-      </para>
+        (unlike <literal>*</literal>).  WARNING: this facility may be withdrawn in the future.
+</para></listitem>
+</itemizedlist>
+</para>
     </sect3>
 
     <sect3 id="assoc-decl-defs">
@@ -6078,22 +6091,50 @@ class IsBoolMap v where
 instance IsBoolMap [(Int, Bool)] where
   lookupKey = lookup
 </programlisting>
-The <literal>instance</literal> keyword is optional.
-      </para>
+In an <literal>instance</literal> declaration for the class, if no explicit
+<literal>type instance</literal> declaration is given for the associated type, the default declaration
+is used instead, just as with default class methods.
+</para>
 <para>
-There can also be multiple defaults for a single type, as long as they do not
-overlap:
+Note the following points:
+<itemizedlist>
+<listitem><para>
+  The <literal>instance</literal> keyword is optional.
+</para></listitem>
+<listitem><para>
+   There can be at most one default declaration for an associated type synonym.
+</para></listitem>
+<listitem><para>
+  A default declaration is not permitted for an associated
+  <emphasis>data</emphasis> type.
+</para></listitem>
+<listitem><para>
+   The default declaration must mention only type <emphasis>variables</emphasis> on the left hand side,
+   and the right hand side must mention only type varaibels bound on the left hand side.
+   However, unlike the associated type family declaration itself,
+   the type variables of the default instance are independent of those of the parent class.
+</para></listitem>
+</itemizedlist>
+Here are some examples:
 <programlisting>
-class C a where
-  type F a b
-  type F a Int  = Bool
-  type F a Bool = Int
+  class C a where
+    type F1 a :: *
+    type instance F1 a = [a]     -- OK
+    type instance F1 a = a->a    -- BAD; only one default instance is allowed
+
+    type F2 b a                  -- OK; note the family has more type
+                                 --     variables than the class
+    type instance F2 c d = c->d  -- OK; you don't have to use 'a' in the type instance
+
+    type F3 a
+    type F3 [b] = b              -- BAD; only type variables allowed on the LHS
+
+    type F4 a
+    type F4 b = a                -- BAD; 'a' is not in scope  in the RHS
 </programlisting>
+</para>
 
-A default declaration is not permitted for an associated
-<emphasis>data</emphasis> type.
-      </para>
-    </sect3>
+</sect3>
 
     <sect3 id="scoping-class-params">
       <title>Scoping of class parameters</title>
index d64036c..d162233 100644 (file)
@@ -1,5 +1,4 @@
 
 Overlap4.hs:7:3:
     Number of parameters must match family declaration; expected 2
-    In the equations for closed type family ‘F’
     In the type family declaration for ‘F’
index 3adf2f3..a889145 100644 (file)
@@ -1,5 +1,6 @@
 
 Overlap5.hs:8:3:
-    Mismatched type names in closed type family declaration.
-    First name was F; this one is G
-    In the family declaration for ‘F’
+    Mismatched type name in type family instance.
+      Expected: F
+        Actual: G
+    In the type family declaration for ‘F’
index 8318927..f57af39 100644 (file)
@@ -1,4 +1,4 @@
 
 SimpleFail1a.hs:4:1:
-    Couldn't match kind ‘* -> *’ against ‘*’
+    Number of parameters must match family declaration; expected 2
     In the data instance declaration for ‘T1’
index e1059a4..3ecd31a 100644 (file)
@@ -1,4 +1,4 @@
 
 SimpleFail1b.hs:4:1:
-    Number of parameters must match family declaration; expected no more than 2
+    Number of parameters must match family declaration; expected 2
     In the data instance declaration for ‘T1’
index 91a3eb2..8c4c743 100644 (file)
@@ -1,6 +1,6 @@
 
-SimpleFail4.hs:8:8:
-    Type indexes must match class instance head
-    Found ‘Int’ but expected ‘a
-    In the type synonym instance default declaration for ‘S2’
-    In the class declaration for ‘C2’
+SimpleFail4.hs:8:11:
+    Unexpected type ‘Int’
+    In the default declaration for ‘S2
+    A default declaration should have form
+      default S2 a = ...
index b0e9fde..d7de4fe 100644 (file)
@@ -3,4 +3,4 @@ T8506.hs:3:16:
     Unexpected type ‘Int’
     In the class declaration for ‘Shapable’
     A class declaration should have form
-      class Shapable a b c where ...
+      class Shapable a where ...
index da220cd..5641642 100644 (file)
@@ -3,4 +3,4 @@ readFail025.hs:5:8:
     Unexpected type ‘String’
     In the data declaration for ‘T’
     A data declaration should have form
-      data T a b c = ...
+      data T a = ...
index aa8b482..8636bb9 100644 (file)
@@ -38,3 +38,9 @@ T8449:
        $(RM) -f T8449.hi T8449.o T8449a.hi T8449a.o
        '$(TEST_HC)' $(TEST_HC_OPTS) -c T8449a.hs
        '$(TEST_HC)' $(TEST_HC_OPTS) -c T8449.hs
+
+T9263:
+       $(RM) -f T9263.hi T9263.o T9263a.hi T9263a.o T9263b.hi T9263b.o
+       '$(TEST_HC)' $(TEST_HC_OPTS) -c T9263b.hs
+       '$(TEST_HC)' $(TEST_HC_OPTS) -c T9263a.hs
+       '$(TEST_HC)' $(TEST_HC_OPTS) -c T9263.hs
index 09b818a..22388dd 100644 (file)
@@ -4,4 +4,4 @@ T7939a.hs:7:5:
     The first argument of ‘F’ should have kind ‘*’,
       but ‘Maybe’ has kind ‘* -> *’
     In the type ‘Maybe’
-    In the family declaration for ‘F’
+    In the type family declaration for ‘F’
diff --git a/testsuite/tests/polykinds/T9063.hs b/testsuite/tests/polykinds/T9063.hs
new file mode 100644 (file)
index 0000000..007f475
--- /dev/null
@@ -0,0 +1,16 @@
+{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators,
+             UndecidableInstances #-}
+
+module T9063 where
+
+import Data.Type.Equality
+import Data.Proxy
+
+class kproxy ~ 'KProxy => PEq (kproxy :: KProxy a) where
+  type (:==) (x :: a) (y :: a) :: Bool
+  type x :== y = x == y
+
+instance PEq ('KProxy :: KProxy Bool)
+
+foo :: Proxy (True :== True) -> Proxy (True == True)
+foo = id
diff --git a/testsuite/tests/polykinds/T9263.hs b/testsuite/tests/polykinds/T9263.hs
new file mode 100644 (file)
index 0000000..e913e1f
--- /dev/null
@@ -0,0 +1,2 @@
+module T9263 where
+  import T9263a
diff --git a/testsuite/tests/polykinds/T9263a.hs b/testsuite/tests/polykinds/T9263a.hs
new file mode 100644 (file)
index 0000000..1cecaba
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies #-}
+module T9263a where
+
+import T9263b
+import Data.Proxy
+
+data Void
+
+instance PEq ('KProxy :: KProxy Void)
diff --git a/testsuite/tests/polykinds/T9263b.hs b/testsuite/tests/polykinds/T9263b.hs
new file mode 100644 (file)
index 0000000..d267eac
--- /dev/null
@@ -0,0 +1,8 @@
+{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}
+module T9263b where
+
+import Data.Proxy
+
+class kproxy ~ 'KProxy => PEq (kproxy :: KProxy a) where
+   type F (x :: a) :: Bool
+   type F (x :: a) = False
diff --git a/testsuite/tests/polykinds/T9264.hs b/testsuite/tests/polykinds/T9264.hs
new file mode 100644 (file)
index 0000000..df75599
--- /dev/null
@@ -0,0 +1,6 @@
+{-# LANGUAGE PolyKinds, TypeFamilies, ScopedTypeVariables #-}
+module T9264 where
+
+class C (a :: k) where
+   type F (a :: k)
+   type F (a :: k) = Int
index f642acd..22a159d 100644 (file)
@@ -103,3 +103,6 @@ test('T8985', normal, compile, [''])
 test('T9106', normal, compile_fail, [''])
 test('T9144', normal, compile_fail, [''])
 test('T9222', normal, compile, [''])
+test('T9264', normal, compile, [''])
+test('T9263', normal, run_command, ['$MAKE -s --no-print-directory T9263'])
+test('T9063', normal, compile, [''])
index df5d23b..719c4ce 100644 (file)
@@ -1,8 +1,4 @@
 
-T5481.hs:6:5:
-    The RHS of an associated type declaration mentions type variable ‘b’
-      All such variables must be bound on the LHS
+T5481.hs:6:16: Not in scope: type variable ‘b’
 
-T5481.hs:8:5:
-    The RHS of an associated type declaration mentions type variable ‘a’
-      All such variables must be bound on the LHS
+T5481.hs:8:16: Not in scope: type variable ‘a’
index 4771b82..3ce439e 100644 (file)
@@ -4,8 +4,11 @@ module ShouldCompile where
 class Cls a where
     type Fam a b :: *
     -- Multiple defaults!
-    type Fam a Bool = Maybe a
-    type Fam a Int = (String, a)
+    type Fam a x = FamHelper a x
+
+type family FamHelper a x
+type instance FamHelper a Bool = Maybe a
+type instance FamHelper a Int  = (String, a)
 
 instance Cls Int where
     -- Gets type family from default
index 9b3ac0e..b310a79 100644 (file)
@@ -1,6 +1,6 @@
 
-AssocTyDef02.hs:6:10:
-    Type indexes must match class instance head
-    Found ‘[b]’ but expected ‘a
-    In the type synonym instance default declaration for ‘Typ’
-    In the class declaration for ‘Cls’
+AssocTyDef02.hs:6:14:
+    Unexpected type ‘[b]’
+    In the default declaration for ‘Typ
+    A default declaration should have form
+      default Typ a = ...
index e62a2af..c0950bc 100644 (file)
@@ -1,5 +1,5 @@
-
-AssocTyDef03.hs:6:5:
-    Wrong category of family instance; declaration was for a data type
-    In the type instance declaration for ‘Typ’
-    In the class declaration for ‘Cls’
+\r
+AssocTyDef03.hs:6:5:\r
+    Wrong category of family instance; declaration was for a data type\r
+    In the default type instance declaration for ‘Typ’\r
+    In the class declaration for ‘Cls’\r
index 550d098..4fbaaef 100644 (file)
@@ -1,7 +1,7 @@
-
-AssocTyDef04.hs:6:18:
-    Expecting one more argument to ‘Maybe’
-    Expected kind ‘*’, but ‘Maybe’ has kind ‘* -> *’
-    In the type ‘Maybe’
-    In the type instance declaration for ‘Typ’
-    In the class declaration for ‘Cls’
+\r
+AssocTyDef04.hs:6:18:\r
+    Expecting one more argument to ‘Maybe’\r
+    Expected kind ‘*’, but ‘Maybe’ has kind ‘* -> *’\r
+    In the type ‘Maybe’\r
+    In the default type instance declaration for ‘Typ’\r
+    In the class declaration for ‘Cls’\r
index 8f5b5a5..660d081 100644 (file)
@@ -1,5 +1,5 @@
-
-AssocTyDef05.hs:6:10:
-    Number of parameters must match family declaration; expected 1
-    In the type synonym instance default declaration for ‘Typ’
-    In the class declaration for ‘Cls’
+\r
+AssocTyDef05.hs:6:5:\r
+    Number of parameters must match family declaration; expected 1\r
+    In the default type instance declaration for ‘Typ’\r
+    In the class declaration for ‘Cls’\r
index 29db541..665ad22 100644 (file)
@@ -1,5 +1,6 @@
-
-AssocTyDef06.hs:6:10:
-    Number of parameters must match family declaration; expected no more than 1
-    In the type instance declaration for ‘Typ’
-    In the class declaration for ‘Cls’
+\r
+AssocTyDef06.hs:6:16:\r
+    Unexpected type ‘Int’\r
+    In the default declaration for ‘Typ’\r
+    A default declaration should have form\r
+      default Typ a b = ...\r
index 8d20ca8..cb96b4f 160000 (submodule)
@@ -1 +1 @@
-Subproject commit 8d20ca8d5a9bee73252ff2035ec45f9c03d0820c
+Subproject commit cb96b4f1ed0462b4a394b9fda6612c3bea9886bd