6.4.9. Type families¶

TypeFamilies¶

Implies:	`MonoLocalBinds`, `KindSignatures`, `ExplicitNamespaces`
Implied by:	`TypeFamilyDependencies`
Since:	6.8.1

Allow use and definition of indexed type and data families.

Indexed type families form an extension to facilitate type-level programming. Type families are a generalisation of associated data types [AssocDataTypes2005] and associated type synonyms [AssocTypeSyn2005] Type families themselves are described in Schrijvers 2008 [TypeFamilies2008]. Type families essentially provide type-indexed data types and named functions on types, which are useful for generic programming and highly parameterised library interfaces as well as interfaces with enhanced static information, much like dependent types. They might also be regarded as an alternative to functional dependencies, but provide a more functional style of type-level programming than the relational style of functional dependencies.

Indexed type families, or type families for short, are type constructors that represent sets of types. Set members are denoted by supplying the type family constructor with type parameters, which are called type indices. The difference between vanilla parametrised type constructors and family constructors is much like between parametrically polymorphic functions and (ad-hoc polymorphic) methods of type classes. Parametric polymorphic functions behave the same at all type instances, whereas class methods can change their behaviour in dependence on the class type parameters. Similarly, vanilla type constructors imply the same data representation for all type instances, but family constructors can have varying representation types for varying type indices.

Indexed type families come in three flavours: data families, open type synonym families, and closed type synonym families. They are the indexed family variants of algebraic data types and type synonyms, respectively. The instances of data families can be data types and newtypes.

Type families are enabled by the language extension TypeFamilies. Additional information on the use of type families in GHC is available on the Haskell wiki page on type families.

[AssocDataTypes2005]

“Associated Types with Class”, M. Chakravarty, G. Keller, S. Peyton Jones, and S. Marlow. In Proceedings of “The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL‘05)”, pages 1-13, ACM Press, 2005.

[AssocTypeSyn2005]

“Type Associated Type Synonyms”. M. Chakravarty, G. Keller, and S. Peyton Jones. In Proceedings of “The Tenth ACM SIGPLAN International Conference on Functional Programming”, ACM Press, pages 241-253, 2005.

[TypeFamilies2008]

“Type Checking with Open Type Functions”, T. Schrijvers, S. Peyton-Jones, M. Chakravarty, and M. Sulzmann, in Proceedings of “ICFP 2008: The 13th ACM SIGPLAN International Conference on Functional Programming”, ACM Press, pages 51-62, 2008.

6.4.9.1. Data families¶

Data families appear in two flavours: (1) they can be defined on the toplevel or (2) they can appear inside type classes (in which case they are known as associated types). The former is the more general variant, as it lacks the requirement for the type-indexes to coincide with the class parameters. However, the latter can lead to more clearly structured code and compiler warnings if some type instances were - possibly accidentally - omitted. In the following, we always discuss the general toplevel form first and then cover the additional constraints placed on associated types.

6.4.9.1.1. Data family declarations¶

Indexed data families are introduced by a signature, such as

data family GMap k :: Type -> Type

The special family distinguishes family from standard data declarations. The result kind annotation is optional and, as usual, defaults to Type if omitted. An example is

data family Array e

Named arguments can also be given explicit kind signatures if needed. Just as with GADT declarations named arguments are entirely optional, so that we can declare Array alternatively with

data family Array :: Type -> Type

Unlike with ordinary data definitions, the result kind of a data family does not need to be Type. It can alternatively be:

Of the form TYPE r for some r (see Representation polymorphism). For example:

data family DF1 :: TYPE IntRep
data family DF2 (r :: RuntimeRep)  :: TYPE r
data family DF3 :: Type -> TYPE WordRep

A bare kind variable (with PolyKinds enabled). For example:

data family DF4 :: k
data family DF5 (a :: k) :: k
data family DF6 :: (k -> Type) -> k

Data instances’ kinds must end in Type, however. This restriction is slightly relaxed when the UnliftedNewtypes extension is enabled, as it permits a newtype instance’s kind to end in TYPE r for some r.

6.4.9.1.2. Data instance declarations¶

Instance declarations of data and newtype families are very similar to standard data and newtype declarations. The only two differences are that the keyword data or newtype is followed by instance 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 Either instance for GMap is

data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)

In this example, the declaration has only one variant. In general, it can be any number.

When ExplicitForAll is enabled, type and kind variables used on the left hand side can be explicitly bound. For example:

data instance forall a (b :: Proxy a). F (Proxy b) = FProxy Bool

When an explicit forall is present, all type and kind variables mentioned which are not already in scope must be bound by the forall:

data instance forall   (a :: k). F a = FOtherwise  -- rejected: k not in scope
data instance forall k (a :: k). F a = FOtherwise  -- accepted

When the flag -Wunused-type-patterns is enabled, type variables that are mentioned in the patterns on the left hand side, but not used on the right hand side are reported. Variables that occur multiple times on the left hand side are also considered used. To suppress the warnings, unused variables should be either replaced or prefixed with underscores. Type variables starting with an underscore (_x) are otherwise treated as ordinary type variables.

This resembles the wildcards that can be used in Partial Type Signatures. However, there are some differences. No error messages reporting the inferred types are generated, nor does the extension PartialTypeSignatures have any effect.

A type or kind variable explicitly bound using ExplicitForAll but not used on the left hand side will generate an error, not a warning.

Data and newtype instance declarations are only permitted when an appropriate family declaration is in scope - just as a class instance declaration 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.

A data family instance declaration can use the full expressiveness of ordinary data or newtype declarations:

Although, a data family is introduced with the keyword “data”, a data family instance can use either data or newtype. For example:
```
data family T a
data    instance T Int  = T1 Int | T2 Bool
newtype instance T Char = TC Bool
```

A data instance can use GADT syntax for the data constructors, and indeed can define a GADT. For example:

data family G a b
data instance G [a] b where
   G1 :: c -> G [Int] b
   G2 :: G [a] Bool

You can use a deriving clause on a data instance or newtype instance declaration.

Even if data 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:

data family T a
data instance T Int  = A
data instance T Char = B
foo :: T a -> Int
foo A = 1
foo B = 2

Instead, you would have to write foo as a class operation, thus:

class Foo a where
  foo :: T a -> Int
instance Foo Int where
  foo A = 1
instance Foo Char where
  foo B = 2

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 - in contrast to GADTs - are open; 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.

6.4.9.1.3. Overlap of data instances¶

The instance declarations of a data family used in a single program may not overlap at all, independent of whether they are associated or not. In contrast to type class instances, this is not only a matter of consistency, but one of type safety.

6.4.9.2. Synonym families¶

Type families appear in three flavours: (1) they can be defined as open families on the toplevel, (2) they can be defined as closed families on the toplevel, or (3) they can appear inside type classes (in which case they are known as associated type synonyms). Toplevel families are more general, as they lack the requirement for the type-indexes to coincide with the class parameters. However, associated type synonyms can lead to more clearly structured code and compiler warnings if some type instances were - possibly accidentally - omitted. In the following, we always discuss the general toplevel forms first and then cover the additional constraints placed on associated types. Note that closed associated type synonyms do not exist.

6.4.9.2.1. Type family declarations¶

Open indexed type families are introduced by a signature, such as

type family Elem c :: Type

The special family distinguishes family from standard type declarations. The result kind annotation is optional and, as usual, defaults to Type if omitted. An example is

type family Elem c

Parameters can also be given explicit kind signatures if needed. We call the number of parameters in a type family declaration, the family’s arity, and all applications of a type family must be fully saturated with respect to that arity. This requirement is unlike ordinary type synonyms and it implies that the kind of a type family is not sufficient to determine a family’s arity, and hence in general, also insufficient to determine whether a type family application is well formed. As an example, consider the following declaration:

type family F a b :: Type -> Type
  -- F's arity is 2,
  -- although its overall kind is Type -> Type -> Type -> Type

Given this declaration the following are examples of well-formed and malformed types:

F Char [Int]       -- OK!  Kind: Type -> Type
F Char [Int] Bool  -- OK!  Kind: Type
F IO Bool          -- WRONG: kind mismatch in the first argument
F Bool             -- WRONG: unsaturated application

The result kind annotation is optional and defaults to Type (like argument kinds) if omitted. Polykinded type families can be declared using a parameter in the kind annotation:

type family F a :: k

In this case the kind parameter k is actually an implicit parameter of the type family.

At definition site, the arity determines what inputs can be matched on:

data PT (a :: Type)

type family F1 :: k -> Type
type instance F1 = PT
  -- OK, 'k' can be matched on.

type family F0 :: forall k. k -> Type
type instance F0 = PT
  -- Error:
  --   • Expected kind ‘forall k. k -> Type’,
  --       but ‘PT’ has kind ‘Type -> Type’
  --   • In the type ‘PT’
  --     In the type instance declaration for ‘F0’

Both F1 and F0 have kind forall k. k -> Type, but their arity differs.

At use sites, the arity determines if the definition can be used in a higher-rank scenario:

type HRK (f :: forall k. k -> Type) = (f Int, f Maybe, f True)

type H1 = HRK F0  -- OK
type H2 = HRK F1
  -- Error:
  --   • Expected kind ‘forall k. k -> Type’,
  --       but ‘F1’ has kind ‘k0 -> Type’
  --   • In the first argument of ‘HRK’, namely ‘F1’
  --     In the type ‘HRK F1’
  --     In the type declaration for ‘H2’

This is a consequence of the requirement that all applications of a type family must be fully saturated with respect to their arity.

6.4.9.2.2. Type instance declarations¶

Instance declarations of type families are very similar to standard type synonym declarations. The only two differences are that the keyword type is followed by instance 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, and type synonyms are allowed as long as they are fully applied and expand to a type that is admissible - these are the exact same requirements as for data instances. For example, the [e] instance for Elem is

type instance Elem [e] = e

Type arguments can be replaced with underscores (_) if the names of the arguments don’t matter. This is the same as writing type variables with unique names. Unused type arguments can be replaced or prefixed with underscores to avoid warnings when the -Wunused-type-patterns flag is enabled. The same rules apply as for Data instance declarations.

Also in the same way as Data instance declarations, when ExplicitForAll is enabled, type and kind variables can be explicitly bound in a type instance declaration.

Type family instance declarations are only legitimate when an appropriate family declaration is in scope - just like class instances require the class declaration to be visible. Moreover, each instance declaration has to conform to the kind determined by its family declaration, and the number of type parameters in an instance declaration must match the number of type parameters in the family declaration. Finally, the right-hand side of a type instance must be a monotype (i.e., it may not include foralls) and after the expansion of all saturated vanilla type synonyms, no synonyms, except family synonyms may remain.

6.4.9.2.3. Closed type families¶

A type family can also be declared with a where clause, defining the full set of equations for that family. For example:

type family F a where
  F Int  = Double
  F Bool = Char
  F a    = String

A closed type family’s equations are tried in order, from top to bottom, when simplifying a type family application. In this example, we declare an instance for F such that F Int simplifies to Double, F Bool simplifies to Char, and for any other type a that is known not to be Int or Bool, F a simplifies to String. Note that GHC must be sure that a cannot unify with Int or Bool in that last case; if a programmer specifies just F a in their code, GHC will not be able to simplify the type. After all, a might later be instantiated with Int.

A closed type family’s equations have the same restrictions and extensions as the equations for open type family instances. For instance, when ExplicitForAll is enabled, type or kind variables used on the left hand side of an equation can be explicitly bound, such as in:

type family R a where
  forall t a. R (t a) = [a]
  forall a.   R a     = a

A closed type family may be declared with no equations. Such closed type families are opaque type-level definitions that will never reduce, are not necessarily injective (unlike empty data types), and cannot be given any instances. This is different from omitting the equations of a closed type family in a hs-boot file, which uses the syntax where .., as in that case there may or may not be equations given in the hs file.

6.4.9.2.4. Type family examples¶

Here are some examples of admissible and illegal type instances:

type family F a :: Type
type instance F [Int]   = Int   -- OK!
type instance F String  = Char  -- OK!
type instance F (F a)   = a     -- WRONG: type parameter mentions a type family
type instance
  F (forall a. (a, b))  = b     -- WRONG: a forall type appears in a type parameter
type instance
  F Float = forall a.a          -- WRONG: right-hand side may not be a forall type
type family H a where          -- OK!
  H Int  = Int
  H Bool = Bool
  H a    = String
type instance H Char = Char    -- WRONG: cannot have instances of closed family
type family K a where          -- OK!

type family G a b :: Type -> Type
type instance G Int            = (,)     -- WRONG: must be two type parameters
type instance G Int Char Float = Double  -- WRONG: must be two type parameters

6.4.9.2.5. Compatibility and apartness of type family equations¶

There must be some restrictions on the equations of type families, lest we define an ambiguous rewrite system. So, equations of open type families are restricted to be compatible. Two type patterns are compatible if

all corresponding types and implicit kinds in the patterns are apart, or
the two patterns unify producing a substitution, and the right-hand sides are equal under that substitution.

Two types are considered apart if, for all possible substitutions, the types cannot reduce to a common reduct.

The first clause of “compatible” is the more straightforward one. It says that the patterns of two distinct type family instances cannot overlap. For example, the following is disallowed:

type instance F Int = Bool
type instance F Int = Char

The second clause is a little more interesting. It says that two overlapping type family instances are allowed if the right-hand sides coincide in the region of overlap. Some examples help here:

type instance F (a, Int) = [a]
type instance F (Int, b) = [b]   -- overlap permitted

type instance G (a, Int)  = [a]
type instance G (Char, a) = [a]  -- ILLEGAL overlap, as [Char] /= [Int]

Note that this compatibility condition is independent of whether the type family is associated or not, and it is not only a matter of consistency, but one of type safety.

For a polykinded type family, the kinds are checked for apartness just like types. For example, the following is accepted:

type family J a :: k
type instance J Int = Bool
type instance J Int = Maybe

These instances are compatible because they differ in their implicit kind parameter; the first uses Type while the second uses Type -> Type.

The definition for “compatible” uses a notion of “apart”, whose definition in turn relies on type family reduction. This condition of “apartness”, as stated, is impossible to check, so we use this conservative approximation: two types are considered to be apart when the two types cannot be unified, even by a potentially infinite unifier. Allowing the unifier to be infinite disallows the following pair of instances:

type instance H x   x = Int
type instance H [x] x = Bool

The type patterns in this pair equal if x is replaced by an infinite nesting of lists. Rejecting instances such as these is necessary for type soundness.

Compatibility also affects closed type families. When simplifying an application of a closed type family, GHC will select an equation only when it is sure that no incompatible previous equation will ever apply. Here are some examples:

type family F a where
  F Int = Bool
  F a   = Char

type family G a where
  G Int = Int
  G a   = a

In the definition for F, the two equations are incompatible – their patterns are not apart, and yet their right-hand sides do not coincide. Thus, before GHC selects the second equation, it must be sure that the first can never apply. So, the type F a does not simplify; only a type such as F Double will simplify to Char. In G, on the other hand, the two equations are compatible. Thus, GHC can ignore the first equation when looking at the second. So, G a will simplify to a.

Incompatibilities between closed type family equations can be displayed in :info when -fprint-axiom-incomps is enabled.

However see Type, class and other declarations for the overlap rules in GHCi.

6.4.9.2.6. Decidability of type synonym instances¶

In order to guarantee that type inference in the presence of type families is decidable, we need to place a number of additional restrictions on the formation of type instance declarations (c.f., Definition 5 (Relaxed Conditions) of “Type Checking with Open Type Functions”). Instance declarations have the general form

type instance F t1 .. tn = t

where we require that for every type family application (G s1 .. sm) in t,

s1 .. sm do not contain any type family constructors,
the total number of symbols (data type constructors and type variables) in s1 .. sm is strictly smaller than in t1 .. tn, and
for every type variable a, a occurs in s1 .. sm at most as often as in t1 .. tn.

These restrictions are easily verified and ensure termination of type inference. However, they are not sufficient to guarantee completeness of type inference in the presence of, so called, ‘’loopy equalities’‘, such as a ~ [F a], where a recursive occurrence of a type variable is underneath a family application and data constructor application - see the above mentioned paper for details.

If the option UndecidableInstances is passed to the compiler (see Instance termination rules), the above restrictions are not enforced and it is on the programmer to ensure termination of the normalisation of type families during type inference.

6.4.9.2.7. Reducing type family applications¶

-ffamily-application-cache¶: The flag -ffamily-application-cache (on by default) instructs GHC to use a cache when reducing type family applications. In most cases, this will speed up compilation. The use of this flag will not affect runtime behaviour.

When GHC encounters a type family application (like F Int a) in a program, it must often reduce it in order to complete type checking. Here is a simple example:

type family F a where
  F Int            = Bool
  F (Maybe Double) = Char

g :: F Int -> Bool
g = not

Despite the fact that g’s type mentions F Int, GHC must recognize that g’s argument really has type Bool. This is done by reducing F Int to become Bool. Sometimes, there is not enough information to reduce a type family application; we say such an application is stuck. Continuing this example, an occurrence of F (Maybe a) (for some type variable a) would be stuck, as no equation applies.

During type checking, GHC uses heuristics to determine which type family application to reduce next; there is no predictable ordering among different type family applications. The non-determinism rarely matters in practice. In most programs, type family reduction terminates, and so these choices are immaterial. However, if a type family application does not terminate, it is possible that type-checking may unpredictably diverge. (GHC will always take the same path for a given source program, but small changes in that source program may induce GHC to take a different path. Compiling a given, unchanged source program is still deterministic.)

In order to speed up type family reduction, GHC normally uses a cache, remembering what type family applications it has previously reduced. This feature can be disabled with -fno-family-application-cache.

6.4.9.3. Wildcards on the LHS of data and type family instances¶

When the name of a type argument of a data or type instance declaration doesn’t matter, it can be replaced with an underscore (_). This is the same as writing a type variable with a unique name.

data family F a b :: Type
data instance F Int _ = Int
-- Equivalent to  data instance F Int b = Int

type family T a :: Type
type instance T (a,_) = a
-- Equivalent to  type instance T (a,b) = a

This use of underscore for wildcard in a type pattern is exactly like pattern matching in the term language, but is rather different to the use of a underscore in a partial type signature (see Type Wildcards).

A type variable beginning with an underscore is not treated specially in a type or data instance declaration. For example:

data instance F Bool _a = _a -> Int
-- Equivalent to  data instance F Bool a = a -> Int

Contrast this with the special treatment of named wildcards in type signatures (Named Wildcards).

6.4.9.4. Associated data and type families¶

A data or type synonym family can be declared as part of a type class, thus:

class GMapKey k where
  data GMap k :: Type -> Type
  ...

class Collects ce where
  type Elem ce :: Type
  ...

When doing so, we (optionally) may drop the “family” keyword.

The type parameters must all be type variables, of course, and some (but not necessarily all) of then can be the 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:

class C a b c where
  type T c a x :: Type

Here c and a are class parameters, but the type is also indexed on a third parameter x.

6.4.9.4.1. Associated instances¶

When an associated data or type synonym family instance is declared within a type class instance, we (optionally) may drop the instance keyword in the family instance:

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
  type Elem [e] = e
  ...

The data or type family instance for an associated type must follow the rule that the type indexes corresponding to class parameters must be precisely the same as types given in the instance head. For example:

class Collects ce where
  type Elem ce :: Type

instance Eq (Elem [e]) => Collects [e] where
  -- Choose one of the following alternatives:
  type Elem [e] = e       -- OK
  type Elem [x] = x       -- BAD; '[x]' is different to '[e]' from head
  type Elem x   = x       -- BAD; 'x' is different to '[e]'
  type Elem [Maybe x] = x -- BAD: '[Maybe x]' is different to '[e]'

Note the following points:

An instance 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.

The type variables on the right hand side of the type family equation must, as usual, be explicitly bound by the left hand side. This restriction is relaxed for kind variables, however, as the right hand side is allowed to mention kind variables that are implicitly bound. For example, these are legitimate:

data family Nat :: k -> k -> Type
-- k is implicitly bound by an invisible kind pattern
newtype instance Nat :: (k -> Type) -> (k -> Type) -> Type where
  Nat :: (forall xx. f xx -> g xx) -> Nat f g

class Funct f where
  type Codomain f :: Type
instance Funct ('KProxy :: KProxy o) where
  -- o is implicitly bound by the kind signature
  -- of the LHS type pattern ('KProxy)
  type Codomain 'KProxy = NatTr (Proxy :: o -> Type)

The instance for an associated type can be omitted in class instances. In that case, unless there is a default instance (see Associated type synonym defaults), the corresponding instance type is not inhabited; i.e., only diverging expressions, such as undefined, can assume the type.
Although it is unusual, there (currently) can be multiple instances for an associated family in a single instance declaration. For example, this is legitimate:
```
instance GMapKey Flob where
  data GMap Flob [v] = G1 v
  data GMap Flob Int = G2 Int
  ...
```
Here we give two data instance declarations, one in which the last parameter is [v], and one for which it is Int. Since you cannot give any subsequent instances for (GMap Flob ...), this facility is most useful when the free indexed parameter is of a kind with a finite number of alternatives (unlike Type).
When ExplicitForAll is enabled, type and kind variables can be explicitly bound in associated data or type family instances in the same way (and with the same restrictions) as Data instance declarations or Type instance declarations. For example, adapting the above, the following is accepted:
```
instance Eq (Elem [e]) => Collects [e] where
  type forall e. Elem [e] = e
```

6.4.9.4.2. Associated type synonym defaults¶

It is possible for the class defining the associated type to specify a default for associated type instances. So for example, this is OK:

class IsBoolMap v where
  type Key v
  type instance Key v = Int

  lookupKey :: Key v -> v -> Maybe Bool

instance IsBoolMap [(Int, Bool)] where
  lookupKey = lookup

In an instance declaration for the class, if no explicit type instance declaration is given for the associated type, the default declaration is used instead, just as with default class methods.

Note the following points:

The instance keyword is optional.
There can be at most one default declaration for an associated type synonym.
A default declaration is not permitted for an associated data type.
The default declaration must mention only type variables on the left hand side, and type variables may not be repeated on the left-hand side. The right hand side must mention only type variables that are explicitly bound on the left hand side. This restriction is relaxed for kind variables, however, as the right hand side is allowed to mention kind variables that are implicitly bound on the left hand side.

Like with Associated instances, it is possible to explicitly bind type and kind variables in default declarations with a forall by using the ExplicitForAll language extension.
Unlike the associated type family declaration itself, the type variables of the default instance are independent of those of the parent class.

Here are some examples:

class C (a :: Type) where
  type F1 a :: Type
  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, and the argument to F3 is
                               --      instantiated to [b], which is not
                               --      a bare type variable

  type F4 x y
  type F4 x x = x              -- BAD; the type variable x is repeated on
                               --      the LHS

  type F5 a
  type F5 b = a                -- BAD; 'a' is not in scope  in the RHS

  type F6 a :: [k]
  type F6 a = ('[] :: [x])     -- OK; the kind variable x is implicitly
                               --     bound by an invisible kind pattern
                               --     on the LHS

  type F7 a
  type F7 a =
    Proxy ('[] :: [x])         -- BAD; the kind variable x is not bound,
                               --      even by an invisible kind pattern

  type F8 (x :: a) :: [a]
  type F8 x = ('[] :: [a])     -- OK; the kind variable a is implicitly
                               --     bound by the kind signature of the
                               --     LHS type pattern

  type F9 (a :: k)
  type F9 a = Maybe a          -- BAD; the kind variable k is
                               --      instantiated to Type, which is not
                               --      a bare kind variable

  type F10 (a :: j) (b :: k)
  type F10 (a :: z) (b :: z)
    = Proxy a                  -- BAD; the kind variable z is repeated,
                               --      as both j and k are instantiated to z

  type F11 a b
  type forall a b. F11 a b = a -- OK; LHS type variables can be
                               --     explicitly bound with 'forall'

  type F12 (a :: k)
  type F12 @k a = Proxy a      -- OK; visible kind application syntax is
                               --     permitted in default declarations

6.4.9.4.3. Scoping of class parameters¶

The visibility of class parameters in the right-hand side of associated family instances depends solely on the parameters of the family. As an example, consider the simple class declaration

class C a b where
  data T a

Only one of the two class parameters is a parameter to the data family. Hence, the following instance declaration is invalid:

instance C [c] d where
  data T [c] = MkT (c, d)    -- WRONG!!  'd' is not in scope

Here, the right-hand side of the data instance mentions the type variable d that does not occur in its left-hand side. We cannot admit such data instances as they would compromise type safety.

Bear in mind that it is also possible for the right-hand side of an associated family instance to contain kind parameters (by using the PolyKinds extension). For instance, this class and instance are perfectly admissible:

class C k where
  type T :: k

instance C (Maybe a) where
  type T = (Nothing :: Maybe a)

Here, although the right-hand side (Nothing :: Maybe a) mentions a kind variable a which does not occur on the left-hand side, this is acceptable, because a is implicitly bound by T’s kind pattern.

A kind variable can also be bound implicitly in a LHS type pattern, as in this example:

class C a where
  type T (x :: a) :: [a]

instance C (Maybe a) where
  type T x = ('[] :: [Maybe a])

In ('[] :: [Maybe a]), the kind variable a is implicitly bound by the kind signature of the LHS type pattern x.

6.4.9.4.4. Instance contexts and associated type and data instances¶

Associated type and data instance declarations do not inherit any context specified on the enclosing instance. For type instance declarations, it is unclear what the context would mean. For data instance declarations, it is unlikely a user would want the context repeated for every data constructor. The only place where the context might likely be useful is in a deriving clause of an associated data instance. However, even here, the role of the outer instance context is murky. So, for clarity, we just stick to the rule above: the enclosing instance context is ignored. If you need to use a non-trivial context on a derived instance, use a standalone deriving clause (at the top level).

6.4.9.5. Import and export¶

The rules for export lists (Haskell Report Section 5.2) need adjustment for type families:

The form T(..), where T is a data family, names the family T and all the in-scope constructors (whether in scope qualified or unqualified) that are data instances of T.
The form T(.., ci, .., fj, ..), where T is a data family, names T and the specified constructors ci and fields fj as usual. The constructors and field names must belong to some data instance of T, but are not required to belong to the same instance.
The form C(..), where C is a class, names the class C and all its methods and associated types.
The form C(.., mi, .., type Tj, ..), where C is a class, names the class C, and the specified methods mi and associated types Tj. The types need a keyword “type” to distinguish them from data constructors.
Whenever there is no export list and a data instance is defined, the corresponding data family type constructor is exported along with the new data constructors, regardless of whether the data family is defined locally or in another module.

6.4.9.5.1. Examples¶

Recall our running GMapKey class example:

class GMapKey k where
  data GMap k :: Type -> Type
  insert :: GMap k v -> k -> v -> GMap k v
  lookup :: GMap k v -> k -> Maybe v
  empty  :: GMap k v

instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
  data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
  ...method declarations...

Here are some export lists and their meaning:

```
module GMap( GMapKey )
```
Exports just the class name.
```
module GMap( GMapKey(..) )
```
Exports the class, the associated type GMap and the member functions empty, lookup, and insert. The data constructors of GMap (in this case GMapEither) are not exported.

module GMap( GMapKey( type GMap, empty, lookup, insert ) )

Same as the previous item. Note the “type” keyword.

```
module GMap( GMapKey(..), GMap(..) )
```
Same as previous item, but also exports all the data constructors for GMap, namely GMapEither.

module GMap ( GMapKey( empty, lookup, insert), GMap(..) )

Same as previous item.

module GMap ( GMapKey, empty, lookup, insert, GMap(..) )

Same as previous item.

Two things to watch out for:

You cannot write GMapKey(type GMap(..)) — i.e., sub-component specifications cannot be nested. To specify GMap’s data constructors, you have to list it separately.
Consider this example:
```
module X where
  data family D

module Y where
  import X
  data instance D Int = D1 | D2
```
Module Y exports all the entities defined in Y, namely the data constructors D1 and D2, and implicitly the data family D, even though it’s defined in X. This means you can write import Y( D(D1,D2) ) without giving an explicit export list like this:
```
     module Y( D(..) ) where ...
or   module Y( module Y, D ) where ...
```

6.4.9.5.2. Instances¶

Family instances are implicitly exported, just like class instances. However, this applies only to the heads of instances, not to the data constructors an instance defines.

6.4.9.6. Type families and instance declarations¶

Type families require us to extend the rules for the form of instance heads, which are given in Relaxed rules for the instance head. Specifically:

Data type families may appear in an instance head
Type synonym families may not appear (at all) in an instance head

The reason for the latter restriction is that there is no way to check for instance matching. Consider

type family F a
type instance F Bool = Int

class C a

instance C Int
instance C (F a)

Now a constraint (C (F Bool)) would match both instances. The situation is especially bad because the type instance for F Bool might be in another module, or even in a module that is not yet written.

However, type class instances of instances of data families can be defined much like any other data type. For example, we can say

data instance T Int = T1 Int | T2 Bool
instance Eq (T Int) where
  (T1 i) == (T1 j) = i==j
  (T2 i) == (T2 j) = i==j
  _      == _      = False

Note that class instances are always for particular instances of a data family and never for an entire family as a whole. This is for essentially the same reasons that we cannot define a toplevel function that performs pattern matching on the data constructors of different instances of a single type family. It would require a form of extensible case construct.

Data instance declarations can also have deriving clauses. For example, we can write

data GMap () v = GMapUnit (Maybe v)
               deriving Show

which implicitly defines an instance of the form

instance Show v => Show (GMap () v) where ...

6.4.9.7. Injective type families¶

TypeFamilyDependencies¶

Implies:	`TypeFamilies`
Since:	8.0.1

Allow functional dependency annotations on type families. This allows one to define injective type families.

Starting with GHC 8.0 type families can be annotated with injectivity information. This information is then used by GHC during type checking to resolve type ambiguities in situations where a type variable appears only under type family applications. Consider this contrived example:

type family Id a
type instance Id Int = Int
type instance Id Bool = Bool

id :: Id t -> Id t
id x = x

Here the definition of id will be rejected because type variable t appears only under type family applications and is thus ambiguous. But this code will be accepted if we tell GHC that Id is injective, which means it will be possible to infer t at call sites from the type of the argument:

type family Id a = r | r -> a

Injective type families are enabled with -XTypeFamilyDependencies language extension. This extension implies -XTypeFamilies.

For full details on injective type families refer to Haskell Symposium 2015 paper Injective type families for Haskell.

6.4.9.7.1. Syntax of injectivity annotation¶

The injectivity annotation is added after the type family head and consists of two parts:

a type variable that names the result of a type family. Syntax: = tyvar or = (tyvar :: kind). The type variable must be fresh.
an injectivity annotation of the form | A -> B, where A is the result type variable (see previous bullet) and B is a list of argument type and kind variables in which type family is injective. It is possible to omit some variables if the type family is not injective in them.

Examples:

type family Id a = result | result -> a where
type family F a b c = d | d -> a c b
type family G (a :: k) b c = foo | foo -> k b where

For open and closed type families it is OK to name the result but skip the injectivity annotation. This is not the case for associated type synonyms, where the named result without injectivity annotation will be interpreted as associated type synonym default.

6.4.9.7.2. Verifying the injectivity annotation against type family equations¶

Once the user declares type family to be injective GHC must verify that this declaration is correct, i.e., that type family equations don’t violate the injectivity annotation. A general idea is that if at least one equation (bullets (1), (2) and (3) below) or a pair of equations (bullets (4) and (5) below) violates the injectivity annotation then a type family is not injective in a way the user claims and an error is reported. In the bullets below RHS refers to the right-hand side of the type family equation being checked for injectivity. LHS refers to the arguments of that type family equation. Below are the rules followed when checking injectivity of a type family:

If a RHS of a type family equation is a type family application GHC reports that the type family is not injective.
If a RHS of a type family equation is a bare type variable we require that all LHS variables (including implicit kind variables) are also bare. In other words, this has to be a sole equation of that type family and it has to cover all possible patterns. If the patterns are not covering GHC reports that the type family is not injective.
If a LHS type variable that is declared as injective is not mentioned on injective position in the RHS GHC reports that the type family is not injective. Injective position means either argument to a type constructor or injective argument to a type family. Type inference can potentially loop when looking under injective type families in the RHS, so this requires UndecidableInstances; GHC suggests enabling the flag when it is necessary.
Open type families Open type families are typechecked incrementally. This means that when a module is imported type family instances contained in that module are checked against instances present in already imported modules.

A pair of an open type family equations is checked by attempting to unify their RHSs. If the RHSs don’t unify this pair does not violate injectivity annotation. If unification succeeds with a substitution then LHSs of unified equations must be identical under that substitution. If they are not identical then GHC reports that the type family is not injective.
In a closed type family all equations are ordered and in one place. Equations are also checked pair-wise but this time an equation has to be paired with all the preceding equations. Of course a single-equation closed type family is trivially injective (unless (1), (2) or (3) above holds).

When checking a pair of closed type family equations GHC tried to unify their RHSs. If they don’t unify this pair of equations does not violate injectivity annotation. If the RHSs can be unified under some substitution (possibly empty) then either the LHSs unify under the same substitution or the LHS of the latter equation is subsumed by earlier equations. If neither condition is met GHC reports that a type family is not injective.

Note that for the purpose of injectivity check in bullets (4) and (5) GHC uses a special variant of unification algorithm that treats type family applications as possibly unifying with anything.