Editing GHC/Type families (section)

== Detailed definition of type synonym families ==

Type 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 type synonyms).  The former is the more general variant, as it lacks the requirement for the type-indices 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.

=== Family declarations ===

Indexed type families are introduced by a signature, such as 
<haskell>
type family Elem c :: *
</haskell>
The special <hask>family</hask> distinguishes family from standard type declarations.  The result kind annotation is optional and, as usual, defaults to <hask>*</hask> if omitted.  An example is
<haskell>
type family Elem c
</haskell>
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 w.r.t. 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:
<haskell>
type family F a b :: * -> *   -- F's arity is 2, 
                              -- although its overall kind is * -> * -> * -> *
</haskell>
Given this declaration the following are examples of well-formed and malformed types:
<haskell>
F Char [Int]       -- OK!  Kind: * -> *
F Char [Int] Bool  -- OK!  Kind: *
F IO Bool          -- WRONG: kind mismatch in the first argument
F Bool             -- WRONG: unsaturated application
</haskell>

A top-level type family can be declared as open or closed. (Associated type
families are always open.) A closed type family has all of its equations
defined in one place and cannot be extended, whereas an open family can have
instances spread across modules. The advantage of a closed family is that
its equations are tried in order, similar to a term-level function definition:
<haskell>
type family G a where
  G Int = Bool
  G a   = Char
</haskell>
With this definition, the type <hask>G Int</hask> becomes <hask>Bool</hask>
and, say, <hask>G Double</hask> becomes <hask>Char</hask>. See also [https://gitlab.haskell.org/ghc/ghc/-/wikis/new-axioms here] for more information about closed type families.

==== Associated family declarations ====

When a type family is declared as part of a type class, we drop the <hask>family</hask> special.  The <hask>Elem</hask> declaration takes the following form
<haskell>
class Collects ce where
  type Elem ce :: *
  ...
</haskell>
Exactly as in the case of an associated data declaration, '''the named type parameters must be a permutation of a subset of the class parameters'''.  Examples
<haskell>
class C a b c where { type T c a :: * }   -- OK
class D a where { type T a x :: * }       -- No: x is not a class parameter
class D a where { type T a :: * -> * }    -- OK
</haskell>

=== Type instance declarations ===

Instance declarations of open type families are very similar to standard type synonym declarations.  The only two differences are that the keyword <hask>type</hask> is followed by <hask>instance</hask> 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 <hask>[e]</hask> instance for <hask>Elem</hask> is
<haskell>
type instance Elem [e] = e
</haskell>

A type family instance declaration must satisfy the following rules:
* An appropriate family declaration is in scope - just like class instances require the class declaration to be visible.  
* The instance declaration conforms to the kind determined by its family declaration
* The number of type parameters in an instance declaration matches the number of type parameters in the family declaration.
* 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.

Here are some examples of admissible and illegal type instances and closed families:
<haskell>
type family F a :: *
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 F2 a where                           -- OK!
  F2 (Maybe Int)  = Int
  F2 (Maybe Bool) = Bool
  F2 (Maybe a)    = String

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

==== Closed family simplification ====

Included in ghc starting 7.8.1.

When dealing with closed families, simplifying the type is harder than just finding a left-hand side that matches and replacing that with a right-hand side. GHC will select an equation to use in a given type family application (the "target") if and only if the following 2 conditions hold:

# There is a substitution from the variables in the equation's LHS that makes the left-hand side of the branch coincide with the target.
# For each previous equation in the family: either the LHS of that equation is ''apart'' from the type family application, '''or''' the equation is ''compatible'' with the chosen equation.

Now, we define ''apart'' and ''compatible'':
# Two types are ''apart'' when one cannot simplify to the other, even after arbitrary type-family simplifications
# Two equations are ''compatible'' if, either, their LHSs are apart or their LHSs unify and their RHSs are the same under the substitution induced by the unification.

Some examples are in order:
<haskell>
type family F a where
  F Int  = Bool
  F Bool = Char
  F a    = Bool

type family And (a :: Bool) (b :: Bool) :: Bool where
  And False c     = False
  And True  d     = d
  And e     False = False
  And f     True  = f
  And g     g     = g
</haskell>

In <hask>F</hask>, all pairs of equations are compatible except the second and third. The first two are compatible because their LHSs are apart. The first and third are compatible because the unifying substitution leads the RHSs to be the same. But, the second and third are not compatible because neither of these conditions holds. As a result, GHC will not use the third equation to simplify a target unless that target is apart from <hask>Bool</hask>.

In <hask>And</hask>, ''every'' pair of equations is compatible, meaning GHC never has to make the extra apartness check during simplification.

Why do all of this? It's a matter of type safety. Consider this example:

<haskell>
type family J a b where
  J a a = Int
  J a b = Bool
</haskell>

Say GHC selected the second branch just because the first doesn't apply at the moment, because two type variables are distinct. The problem is that those variables might later be instantiated at the same value, and then the first branch would have applied. You can convince this sort of inconsistency to produce <hask>unsafeCoerce</hask>.

It gets worse. GHC has no internal notion of inequality, so it can't use previous, failed term-level GADT pattern matches to refine its type assumptions. For example:

<haskell>
data G :: * -> * where
 GInt  :: G Int
 GBool :: G Bool

type family Foo (a :: *) :: * where
 Foo Int = Char
 Foo a   = Double

bar :: G a -> Foo a
bar GInt  = 'x'
bar _     = 3.14
</haskell>

The last line will fail to typecheck, because GHC doesn't know that the type variable <hask>a</hask> can't be <hask>Int</hask> here, even though it's obvious. The only general way to fix this is to have inequality evidence introduced into GHC, and that's a big deal and we don't know if we have the motivation for such a change yet.

==== Associated type instances ====

When an associated family instance is declared within a type class instance, we drop the <hask>instance</hask> keyword in the family instance.  So, the <hask>[e]</hask> instance for <hask>Elem</hask> becomes:
<haskell>
instance (Eq (Elem [e])) => Collects ([e]) where
  type Elem [e] = e
  ...
</haskell>
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 <hask>[e]</hask>, which coincides with the only class parameter.

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; i.e., only diverging expressions, such as <hask>undefined</hask>, can assume the type.

==== Overlap ====

The instance declarations of an open type family used in a single program must be compatible, in the form defined above. This 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. 

Here are two examples to illustrate the condition under which overlap is permitted.
<haskell>
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]
</haskell>

==== Decidability ====

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 [http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html Type Checking with Open Type Functions]).  Instance declarations have the general form
<haskell>
type instance F t1 .. tn = t
</haskell>
where we require that for every type family application <hask>(G s1 .. sm)</hask> in <hask>t</hask>, 
# <hask>s1 .. sm</hask> do not contain any type family constructors,
# the total number of symbols (data type constructors and type variables) in <hask>s1 .. sm</hask> is strictly smaller than in <hask>t1 .. tn</hask>, and
# for every type variable <hask>a</hask>, <hask>a</hask> occurs in <hask>s1 .. sm</hask> at most as often as in <hask>t1 .. tn</hask>.
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 <hask>a ~ [F a]</hask>, 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 <tt>-XUndecidableInstances</tt> is passed to the compiler, the above restrictions are not enforced and it is on the programmer to ensure termination of the normalisation of type families during type inference.

=== Equality constraints ===

Type context can include equality constraints of the form <hask>t1 ~ t2</hask>, which denote that the types <hask>t1</hask> and <hask>t2</hask> need to be the same.  In the presence of type families, whether two types are equal cannot generally be decided locally.  Hence, the contexts of function signatures may include equality constraints, as in the following example:
<haskell>
sumCollects :: (Collects c1, Collects c2, Elem c1 ~ Elem c2) => c1 -> c2 -> c2
</haskell>
where we require that the element type of <hask>c1</hask> and <hask>c2</hask> are the same.  In general, the types <hask>t1</hask> and <hask>t2</hask> of an equality constraint may be arbitrary monotypes; i.e., they may not contain any quantifiers, independent of whether higher-rank types are otherwise enabled.

Equality constraints can also appear in class and instance contexts.  The former enable a simple translation of programs using functional dependencies into programs using family synonyms instead.  The general idea is to rewrite a class declaration of the form
<haskell>
class C a b | a -> b
</haskell>
to
<haskell>
class (F a ~ b) => C a b where
  type F a
</haskell>
That is, we represent every functional dependency (FD) <hask>a1 .. an -> b</hask> by an FD type family <hask>F a1 .. an</hask> and a superclass context equality <hask>F a1 .. an ~ b</hask>, essentially giving a name to the functional dependency.  In class instances, we define the type instances of FD families in accordance with the class head.  Method signatures are not affected by that process.