+data family GMap k :: * -> *
+</programlisting>
+ The special <literal>family</literal> distinguishes family from standard
+ data declarations. The result kind annotation is optional and, as
+ usual, defaults to <literal>*</literal> if omitted. An example is
+<programlisting>
+data family Array e
+</programlisting>
+ Named arguments can also be given explicit kind signatures if needed.
+ Just as with
+ [http://www.haskell.org/ghc/docs/latest/html/users_guide/gadt.html GADT
+ declarations] named arguments are entirely optional, so that we can
+ declare <literal>Array</literal> alternatively with
+<programlisting>
+data family Array :: * -> *
+</programlisting>
+ </para>
+
+ <sect4 id="assoc-data-family-decl">
+ <title>Associated data family declarations</title>
+ <para>
+ When a data family is declared as part of a type class, we drop
+ the <literal>family</literal> special. The <literal>GMap</literal>
+ declaration takes the following form
+<programlisting>
+class GMapKey k where
+ data GMap k :: * -> *
+ ...
+</programlisting>
+ In contrast to toplevel declarations, named arguments must be used for
+ all type parameters that are to be used as type-indexes. Moreover,
+ the argument names must be class parameters. Each class parameter may
+ only be used at most once per associated type, but some may be omitted
+ and they may be in an order other than in the class head. Hence, the
+ following contrived example is admissible:
+<programlisting>
+ class C a b c where
+ data T c a :: *
+</programlisting>
+ </para>
+ </sect4>
+ </sect3>
+
+ <sect3 id="data-instance-declarations">
+ <title>Data instance declarations</title>
+
+ <para>
+ Instance declarations of data and newtype families are very similar to
+ standard data and newtype declarations. The only two differences are
+ that the keyword <literal>data</literal> or <literal>newtype</literal>
+ is followed by <literal>instance</literal> and that some or all of the
+ type arguments can be non-variable types, but may not contain forall
+ types or type synonym families. However, data families are generally
+ allowed in type parameters, and type synonyms are allowed as long as
+ they are fully applied and expand to a type that is itself admissible -
+ exactly as this is required for occurrences of type synonyms in class
+ instance parameters. For example, the <literal>Either</literal>
+ instance for <literal>GMap</literal> is
+<programlisting>
+data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
+</programlisting>
+ In this example, the declaration has only one variant. In general, it
+ can be any number.
+ </para>
+ <para>
+ Data and newtype instance declarations are only permitted when an
+ appropriate family declaration is in scope - just as a class instance declaratoin
+ requires the class declaration to be visible. Moreover, each instance
+ declaration has to conform to the kind determined by its family
+ declaration. This implies that the number of parameters of an instance
+ declaration matches the arity determined by the kind of the family.
+ </para>
+ <para>
+ A data family instance declaration can use the full exprssiveness of
+ ordinary <literal>data</literal> or <literal>newtype</literal> declarations:
+ <itemizedlist>
+ <listitem><para> Although, a data family is <emphasis>introduced</emphasis> with
+ the keyword "<literal>data</literal>", a data family <emphasis>instance</emphasis> can
+ use either <literal>data</literal> or <literal>newtype</literal>. For example:
+<programlisting>
+data family T a
+data instance T Int = T1 Int | T2 Bool
+newtype instance T Char = TC Bool
+</programlisting>
+ </para></listitem>
+ <listitem><para> A <literal>data instance</literal> can use GADT syntax for the data constructors,
+ and indeed can define a GADT. For example:
+<programlisting>
+data family G a b
+data instance G [a] b where
+ G1 :: c -> G [Int] b
+ G2 :: G [a] Bool
+</programlisting>
+ </para></listitem>
+ <listitem><para> You can use a <literal>deriving</literal> clause on a
+ <literal>data instance</literal> or <literal>newtype instance</literal>
+ declaration.
+ </para></listitem>
+ </itemizedlist>
+ </para>
+
+ <para>
+ Even if type families are defined as toplevel declarations, functions
+ that perform different computations for different family instances may still
+ need to be defined as methods of type classes. In particular, the
+ following is not possible:
+<programlisting>
+data family T a
+data instance T Int = A
+data instance T Char = B
+foo :: T a -> Int
+foo A = 1 -- WRONG: These two equations together...
+foo B = 2 -- ...will produce a type error.
+</programlisting>
+Instead, you would have to write <literal>foo</literal> as a class operation, thus:
+<programlisting>
+class C a where
+ foo :: T a -> Int
+instance Foo Int where
+ foo A = 1
+instance Foo Char where
+ foo B = 2
+</programlisting>
+ (Given the functionality provided by GADTs (Generalised Algebraic Data
+ Types), it might seem as if a definition, such as the above, should be
+ feasible. However, type families are - in contrast to GADTs - are
+ <emphasis>open;</emphasis> i.e., new instances can always be added,
+ possibly in other
+ modules. Supporting pattern matching across different data instances
+ would require a form of extensible case construct.)
+ </para>
+
+ <sect4 id="assoc-data-inst">
+ <title>Associated data instances</title>
+ <para>
+ When an associated data family instance is declared within a type
+ class instance, we drop the <literal>instance</literal> keyword in the
+ family instance. So, the <literal>Either</literal> instance
+ for <literal>GMap</literal> becomes:
+<programlisting>
+instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
+ data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
+ ...
+</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. Any parameters to the
+ family constructor that do not correspond to class parameters, need to
+ be variables in every instance; here this is the
+ variable <literal>v</literal>.
+ </para>
+ <para>
+ Instances for an associated family can only appear as part of
+ instances 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;
+ i.e., only diverging expressions, such
+ as <literal>undefined</literal>, can assume the type.
+ </para>
+ </sect4>
+
+ <sect4 id="scoping-class-params">
+ <title>Scoping of class parameters</title>
+ <para>
+ In the case of multi-parameter type classes, the visibility of class
+ parameters in the right-hand side of associated family instances
+ depends <emphasis>solely</emphasis> on the parameters of the data
+ family. As an example, consider the simple class declaration
+<programlisting>
+class C a b where
+ data T a
+</programlisting>
+ Only one of the two class parameters is a parameter to the data
+ family. Hence, the following instance declaration is invalid:
+<programlisting>
+instance C [c] d where
+ data T [c] = MkT (c, d) -- WRONG!! 'd' is not in scope
+</programlisting>
+ Here, the right-hand side of the data instance mentions the type
+ variable <literal>d</literal> that does not occur in its left-hand
+ side. We cannot admit such data instances as they would compromise
+ type safety.
+ </para>
+ </sect4>
+
+ <sect4 id="family-class-inst">
+ <title>Type class instances of family instances</title>
+ <para>
+ Type class instances of instances of data families can be defined as
+ usual, and in particular data instance declarations can
+ have <literal>deriving</literal> clauses. For example, we can write
+<programlisting>
+data GMap () v = GMapUnit (Maybe v)
+ deriving Show
+</programlisting>
+ which implicitly defines an instance of the form
+<programlisting>
+instance Show v => Show (GMap () v) where ...