+In a class declaration, all of the class type variables must be reachable (in the sense
+mentioned in <xref linkend="type-restrictions"/>)
+from the free variables of each method type.
+For example:
+
+<programlisting>
+ class Coll s a where
+ empty :: s
+ insert :: s -> a -> s
+</programlisting>
+
+is not OK, because the type of <literal>empty</literal> doesn't mention
+<literal>a</literal>. Functional dependencies can make the type variable
+reachable:
+<programlisting>
+ class Coll s a | s -> a where
+ empty :: s
+ insert :: s -> a -> s
+</programlisting>
+
+Alternatively <literal>Coll</literal> might be rewritten
+
+<programlisting>
+ class Coll s a where
+ empty :: s a
+ insert :: s a -> a -> s a
+</programlisting>
+
+
+which makes the connection between the type of a collection of
+<literal>a</literal>'s (namely <literal>(s a)</literal>) and the element type <literal>a</literal>.
+Occasionally this really doesn't work, in which case you can split the
+class like this:
+
+
+<programlisting>
+ class CollE s where
+ empty :: s
+
+ class CollE s => Coll s a where
+ insert :: s -> a -> s
+</programlisting>
+</para>
+</sect3>
+
+
+<sect3>
+<title>Background on functional dependencies</title>
+
+<para>The following description of the motivation and use of functional dependencies is taken
+from the Hugs user manual, reproduced here (with minor changes) by kind
+permission of Mark Jones.
+</para>
+<para>
+Consider the following class, intended as part of a
+library for collection types:
+<programlisting>
+ class Collects e ce where
+ empty :: ce
+ insert :: e -> ce -> ce
+ member :: e -> ce -> Bool
+</programlisting>
+The type variable e used here represents the element type, while ce is the type
+of the container itself. Within this framework, we might want to define
+instances of this class for lists or characteristic functions (both of which
+can be used to represent collections of any equality type), bit sets (which can
+be used to represent collections of characters), or hash tables (which can be
+used to represent any collection whose elements have a hash function). Omitting
+standard implementation details, this would lead to the following declarations:
+<programlisting>
+ instance Eq e => Collects e [e] where ...
+ instance Eq e => Collects e (e -> Bool) where ...
+ instance Collects Char BitSet where ...
+ instance (Hashable e, Collects a ce)
+ => Collects e (Array Int ce) where ...
+</programlisting>
+All this looks quite promising; we have a class and a range of interesting
+implementations. Unfortunately, there are some serious problems with the class
+declaration. First, the empty function has an ambiguous type:
+<programlisting>
+ empty :: Collects e ce => ce
+</programlisting>
+By "ambiguous" we mean that there is a type variable e that appears on the left
+of the <literal>=></literal> symbol, but not on the right. The problem with
+this is that, according to the theoretical foundations of Haskell overloading,
+we cannot guarantee a well-defined semantics for any term with an ambiguous
+type.
+</para>
+<para>
+We can sidestep this specific problem by removing the empty member from the
+class declaration. However, although the remaining members, insert and member,
+do not have ambiguous types, we still run into problems when we try to use
+them. For example, consider the following two functions:
+<programlisting>
+ f x y = insert x . insert y
+ g = f True 'a'
+</programlisting>
+for which GHC infers the following types:
+<programlisting>
+ f :: (Collects a c, Collects b c) => a -> b -> c -> c
+ g :: (Collects Bool c, Collects Char c) => c -> c
+</programlisting>
+Notice that the type for f allows the two parameters x and y to be assigned
+different types, even though it attempts to insert each of the two values, one
+after the other, into the same collection. If we're trying to model collections
+that contain only one type of value, then this is clearly an inaccurate
+type. Worse still, the definition for g is accepted, without causing a type
+error. As a result, the error in this code will not be flagged at the point
+where it appears. Instead, it will show up only when we try to use g, which
+might even be in a different module.
+</para>
+
+<sect4><title>An attempt to use constructor classes</title>
+
+<para>
+Faced with the problems described above, some Haskell programmers might be
+tempted to use something like the following version of the class declaration:
+<programlisting>
+ class Collects e c where
+ empty :: c e
+ insert :: e -> c e -> c e
+ member :: e -> c e -> Bool
+</programlisting>
+The key difference here is that we abstract over the type constructor c that is
+used to form the collection type c e, and not over that collection type itself,
+represented by ce in the original class declaration. This avoids the immediate
+problems that we mentioned above: empty has type <literal>Collects e c => c
+e</literal>, which is not ambiguous.
+</para>
+<para>
+The function f from the previous section has a more accurate type:
+<programlisting>
+ f :: (Collects e c) => e -> e -> c e -> c e
+</programlisting>
+The function g from the previous section is now rejected with a type error as
+we would hope because the type of f does not allow the two arguments to have
+different types.
+This, then, is an example of a multiple parameter class that does actually work
+quite well in practice, without ambiguity problems.
+There is, however, a catch. This version of the Collects class is nowhere near
+as general as the original class seemed to be: only one of the four instances
+for <literal>Collects</literal>
+given above can be used with this version of Collects because only one of
+them---the instance for lists---has a collection type that can be written in
+the form c e, for some type constructor c, and element type e.
+</para>
+</sect4>
+
+<sect4><title>Adding functional dependencies</title>
+
+<para>
+To get a more useful version of the Collects class, Hugs provides a mechanism
+that allows programmers to specify dependencies between the parameters of a
+multiple parameter class (For readers with an interest in theoretical
+foundations and previous work: The use of dependency information can be seen
+both as a generalization of the proposal for `parametric type classes' that was
+put forward by Chen, Hudak, and Odersky, or as a special case of Mark Jones's
+later framework for "improvement" of qualified types. The
+underlying ideas are also discussed in a more theoretical and abstract setting
+in a manuscript [implparam], where they are identified as one point in a
+general design space for systems of implicit parameterization.).
+
+To start with an abstract example, consider a declaration such as:
+<programlisting>
+ class C a b where ...
+</programlisting>
+which tells us simply that C can be thought of as a binary relation on types
+(or type constructors, depending on the kinds of a and b). Extra clauses can be
+included in the definition of classes to add information about dependencies
+between parameters, as in the following examples:
+<programlisting>
+ class D a b | a -> b where ...
+ class E a b | a -> b, b -> a where ...
+</programlisting>
+The notation <literal>a -> b</literal> used here between the | and where
+symbols --- not to be
+confused with a function type --- indicates that the a parameter uniquely
+determines the b parameter, and might be read as "a determines b." Thus D is
+not just a relation, but actually a (partial) function. Similarly, from the two
+dependencies that are included in the definition of E, we can see that E
+represents a (partial) one-one mapping between types.
+</para>
+<para>
+More generally, dependencies take the form <literal>x1 ... xn -> y1 ... ym</literal>,
+where x1, ..., xn, and y1, ..., yn are type variables with n>0 and
+m>=0, meaning that the y parameters are uniquely determined by the x
+parameters. Spaces can be used as separators if more than one variable appears
+on any single side of a dependency, as in <literal>t -> a b</literal>. Note that a class may be
+annotated with multiple dependencies using commas as separators, as in the
+definition of E above. Some dependencies that we can write in this notation are
+redundant, and will be rejected because they don't serve any useful
+purpose, and may instead indicate an error in the program. Examples of
+dependencies like this include <literal>a -> a </literal>,
+<literal>a -> a a </literal>,
+<literal>a -> </literal>, etc. There can also be
+some redundancy if multiple dependencies are given, as in
+<literal>a->b</literal>,
+ <literal>b->c </literal>, <literal>a->c </literal>, and
+in which some subset implies the remaining dependencies. Examples like this are
+not treated as errors. Note that dependencies appear only in class
+declarations, and not in any other part of the language. In particular, the
+syntax for instance declarations, class constraints, and types is completely
+unchanged.
+</para>
+<para>
+By including dependencies in a class declaration, we provide a mechanism for
+the programmer to specify each multiple parameter class more precisely. The
+compiler, on the other hand, is responsible for ensuring that the set of
+instances that are in scope at any given point in the program is consistent
+with any declared dependencies. For example, the following pair of instance
+declarations cannot appear together in the same scope because they violate the
+dependency for D, even though either one on its own would be acceptable:
+<programlisting>
+ instance D Bool Int where ...
+ instance D Bool Char where ...
+</programlisting>
+Note also that the following declaration is not allowed, even by itself:
+<programlisting>
+ instance D [a] b where ...
+</programlisting>
+The problem here is that this instance would allow one particular choice of [a]
+to be associated with more than one choice for b, which contradicts the
+dependency specified in the definition of D. More generally, this means that,
+in any instance of the form:
+<programlisting>
+ instance D t s where ...
+</programlisting>
+for some particular types t and s, the only variables that can appear in s are
+the ones that appear in t, and hence, if the type t is known, then s will be
+uniquely determined.
+</para>
+<para>
+The benefit of including dependency information is that it allows us to define
+more general multiple parameter classes, without ambiguity problems, and with
+the benefit of more accurate types. To illustrate this, we return to the
+collection class example, and annotate the original definition of <literal>Collects</literal>
+with a simple dependency:
+<programlisting>
+ class Collects e ce | ce -> e where
+ empty :: ce
+ insert :: e -> ce -> ce
+ member :: e -> ce -> Bool
+</programlisting>
+The dependency <literal>ce -> e</literal> here specifies that the type e of elements is uniquely
+determined by the type of the collection ce. Note that both parameters of
+Collects are of kind *; there are no constructor classes here. Note too that
+all of the instances of Collects that we gave earlier can be used
+together with this new definition.
+</para>
+<para>
+What about the ambiguity problems that we encountered with the original
+definition? The empty function still has type Collects e ce => ce, but it is no
+longer necessary to regard that as an ambiguous type: Although the variable e
+does not appear on the right of the => symbol, the dependency for class
+Collects tells us that it is uniquely determined by ce, which does appear on
+the right of the => symbol. Hence the context in which empty is used can still
+give enough information to determine types for both ce and e, without
+ambiguity. More generally, we need only regard a type as ambiguous if it
+contains a variable on the left of the => that is not uniquely determined
+(either directly or indirectly) by the variables on the right.
+</para>
+<para>
+Dependencies also help to produce more accurate types for user defined
+functions, and hence to provide earlier detection of errors, and less cluttered
+types for programmers to work with. Recall the previous definition for a
+function f:
+<programlisting>
+ f x y = insert x y = insert x . insert y
+</programlisting>
+for which we originally obtained a type:
+<programlisting>
+ f :: (Collects a c, Collects b c) => a -> b -> c -> c
+</programlisting>
+Given the dependency information that we have for Collects, however, we can
+deduce that a and b must be equal because they both appear as the second
+parameter in a Collects constraint with the same first parameter c. Hence we
+can infer a shorter and more accurate type for f:
+<programlisting>
+ f :: (Collects a c) => a -> a -> c -> c
+</programlisting>
+In a similar way, the earlier definition of g will now be flagged as a type error.
+</para>
+<para>
+Although we have given only a few examples here, it should be clear that the
+addition of dependency information can help to make multiple parameter classes
+more useful in practice, avoiding ambiguity problems, and allowing more general
+sets of instance declarations.
+</para>
+</sect4>
+</sect3>
+</sect2>
+
+<sect2 id="instance-decls">
+<title>Instance declarations</title>
+
+<para>An instance declaration has the form
+<screen>
+ instance ( <replaceable>assertion</replaceable><subscript>1</subscript>, ..., <replaceable>assertion</replaceable><subscript>n</subscript>) => <replaceable>class</replaceable> <replaceable>type</replaceable><subscript>1</subscript> ... <replaceable>type</replaceable><subscript>m</subscript> where ...
+</screen>
+The part before the "<literal>=></literal>" is the
+<emphasis>context</emphasis>, while the part after the
+"<literal>=></literal>" is the <emphasis>head</emphasis> of the instance declaration.
+</para>
+
+<sect3 id="flexible-instance-head">
+<title>Relaxed rules for the instance head</title>
+
+<para>
+In Haskell 98 the head of an instance declaration
+must be of the form <literal>C (T a1 ... an)</literal>, where
+<literal>C</literal> is the class, <literal>T</literal> is a data type constructor,
+and the <literal>a1 ... an</literal> are distinct type variables.
+GHC relaxes these rules in two ways.
+<itemizedlist>
+<listitem>
+<para>
+The <option>-XFlexibleInstances</option> flag allows the head of the instance
+declaration to mention arbitrary nested types.
+For example, this becomes a legal instance declaration
+<programlisting>
+ instance C (Maybe Int) where ...
+</programlisting>
+See also the <link linkend="instance-overlap">rules on overlap</link>.
+</para></listitem>
+<listitem><para>
+With the <option>-XTypeSynonymInstances</option> flag, instance heads may use type
+synonyms. As always, using a type synonym is just shorthand for
+writing the RHS of the type synonym definition. For example:
+
+
+<programlisting>
+ type Point = (Int,Int)
+ instance C Point where ...
+ instance C [Point] where ...
+</programlisting>
+
+
+is legal. However, if you added
+
+
+<programlisting>
+ instance C (Int,Int) where ...
+</programlisting>
+
+
+as well, then the compiler will complain about the overlapping
+(actually, identical) instance declarations. As always, type synonyms
+must be fully applied. You cannot, for example, write:
+
+<programlisting>
+ type P a = [[a]]
+ instance Monad P where ...
+</programlisting>
+
+</para></listitem>
+</itemizedlist>
+</para>
+</sect3>
+
+<sect3 id="instance-rules">
+<title>Relaxed rules for instance contexts</title>
+
+<para>In Haskell 98, the assertions in the context of the instance declaration
+must be of the form <literal>C a</literal> where <literal>a</literal>
+is a type variable that occurs in the head.
+</para>
+
+<para>
+The <option>-XFlexibleContexts</option> flag relaxes this rule, as well
+as the corresponding rule for type signatures (see <xref linkend="flexible-contexts"/>).
+With this flag the context of the instance declaration can each consist of arbitrary
+(well-kinded) assertions <literal>(C t1 ... tn)</literal> subject only to the
+following rules:
+<orderedlist>
+<listitem><para>
+The Paterson Conditions: for each assertion in the context
+<orderedlist>
+<listitem><para>No type variable has more occurrences in the assertion than in the head</para></listitem>
+<listitem><para>The assertion has fewer constructors and variables (taken together
+ and counting repetitions) than the head</para></listitem>
+</orderedlist>
+</para></listitem>
+
+<listitem><para>The Coverage Condition. For each functional dependency,
+<replaceable>tvs</replaceable><subscript>left</subscript> <literal>-></literal>
+<replaceable>tvs</replaceable><subscript>right</subscript>, of the class,
+every type variable in
+S(<replaceable>tvs</replaceable><subscript>right</subscript>) must appear in
+S(<replaceable>tvs</replaceable><subscript>left</subscript>), where S is the
+substitution mapping each type variable in the class declaration to the
+corresponding type in the instance declaration.
+</para></listitem>
+</orderedlist>
+These restrictions ensure that context reduction terminates: each reduction
+step makes the problem smaller by at least one
+constructor. Both the Paterson Conditions and the Coverage Condition are lifted
+if you give the <option>-XUndecidableInstances</option>
+flag (<xref linkend="undecidable-instances"/>).
+You can find lots of background material about the reason for these
+restrictions in the paper <ulink
+url="http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/">
+Understanding functional dependencies via Constraint Handling Rules</ulink>.
+</para>
+<para>
+For example, these are OK:
+<programlisting>
+ instance C Int [a] -- Multiple parameters
+ instance Eq (S [a]) -- Structured type in head
+
+ -- Repeated type variable in head
+ instance C4 a a => C4 [a] [a]
+ instance Stateful (ST s) (MutVar s)
+
+ -- Head can consist of type variables only
+ instance C a
+ instance (Eq a, Show b) => C2 a b
+
+ -- Non-type variables in context
+ instance Show (s a) => Show (Sized s a)
+ instance C2 Int a => C3 Bool [a]
+ instance C2 Int a => C3 [a] b
+</programlisting>
+But these are not:
+<programlisting>
+ -- Context assertion no smaller than head
+ instance C a => C a where ...
+ -- (C b b) has more more occurrences of b than the head
+ instance C b b => Foo [b] where ...
+</programlisting>
+</para>
+
+<para>
+The same restrictions apply to instances generated by
+<literal>deriving</literal> clauses. Thus the following is accepted:
+<programlisting>
+ data MinHeap h a = H a (h a)
+ deriving (Show)
+</programlisting>
+because the derived instance
+<programlisting>
+ instance (Show a, Show (h a)) => Show (MinHeap h a)
+</programlisting>
+conforms to the above rules.
+</para>
+
+<para>
+A useful idiom permitted by the above rules is as follows.
+If one allows overlapping instance declarations then it's quite
+convenient to have a "default instance" declaration that applies if
+something more specific does not:
+<programlisting>
+ instance C a where
+ op = ... -- Default
+</programlisting>
+</para>
+</sect3>
+
+<sect3 id="undecidable-instances">
+<title>Undecidable instances</title>
+
+<para>
+Sometimes even the rules of <xref linkend="instance-rules"/> are too onerous.
+For example, sometimes you might want to use the following to get the
+effect of a "class synonym":
+<programlisting>
+ class (C1 a, C2 a, C3 a) => C a where { }
+
+ instance (C1 a, C2 a, C3 a) => C a where { }
+</programlisting>
+This allows you to write shorter signatures:
+<programlisting>
+ f :: C a => ...
+</programlisting>
+instead of
+<programlisting>
+ f :: (C1 a, C2 a, C3 a) => ...
+</programlisting>
+The restrictions on functional dependencies (<xref
+linkend="functional-dependencies"/>) are particularly troublesome.
+It is tempting to introduce type variables in the context that do not appear in
+the head, something that is excluded by the normal rules. For example:
+<programlisting>
+ class HasConverter a b | a -> b where
+ convert :: a -> b
+
+ data Foo a = MkFoo a
+
+ instance (HasConverter a b,Show b) => Show (Foo a) where
+ show (MkFoo value) = show (convert value)
+</programlisting>
+This is dangerous territory, however. Here, for example, is a program that would make the
+typechecker loop:
+<programlisting>
+ class D a
+ class F a b | a->b
+ instance F [a] [[a]]
+ instance (D c, F a c) => D [a] -- 'c' is not mentioned in the head
+</programlisting>
+Similarly, it can be tempting to lift the coverage condition:
+<programlisting>
+ class Mul a b c | a b -> c where
+ (.*.) :: a -> b -> c
+
+ instance Mul Int Int Int where (.*.) = (*)
+ instance Mul Int Float Float where x .*. y = fromIntegral x * y
+ instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
+</programlisting>
+The third instance declaration does not obey the coverage condition;
+and indeed the (somewhat strange) definition:
+<programlisting>
+ f = \ b x y -> if b then x .*. [y] else y
+</programlisting>
+makes instance inference go into a loop, because it requires the constraint
+<literal>(Mul a [b] b)</literal>.
+</para>
+<para>
+Nevertheless, GHC allows you to experiment with more liberal rules. If you use
+the experimental flag <option>-XUndecidableInstances</option>
+<indexterm><primary>-XUndecidableInstances</primary></indexterm>,
+both the Paterson Conditions and the Coverage Condition
+(described in <xref linkend="instance-rules"/>) are lifted. Termination is ensured by having a
+fixed-depth recursion stack. If you exceed the stack depth you get a
+sort of backtrace, and the opportunity to increase the stack depth
+with <option>-fcontext-stack=</option><emphasis>N</emphasis>.
+</para>
+
+</sect3>
+
+
+<sect3 id="instance-overlap">
+<title>Overlapping instances</title>
+<para>
+In general, <emphasis>GHC requires that that it be unambiguous which instance
+declaration
+should be used to resolve a type-class constraint</emphasis>. This behaviour
+can be modified by two flags: <option>-XOverlappingInstances</option>
+<indexterm><primary>-XOverlappingInstances
+</primary></indexterm>
+and <option>-XIncoherentInstances</option>
+<indexterm><primary>-XIncoherentInstances
+</primary></indexterm>, as this section discusses. Both these
+flags are dynamic flags, and can be set on a per-module basis, using
+an <literal>OPTIONS_GHC</literal> pragma if desired (<xref linkend="source-file-options"/>).</para>
+<para>
+When GHC tries to resolve, say, the constraint <literal>C Int Bool</literal>,
+it tries to match every instance declaration against the
+constraint,
+by instantiating the head of the instance declaration. For example, consider
+these declarations:
+<programlisting>
+ instance context1 => C Int a where ... -- (A)
+ instance context2 => C a Bool where ... -- (B)
+ instance context3 => C Int [a] where ... -- (C)
+ instance context4 => C Int [Int] where ... -- (D)
+</programlisting>
+The instances (A) and (B) match the constraint <literal>C Int Bool</literal>,
+but (C) and (D) do not. When matching, GHC takes
+no account of the context of the instance declaration
+(<literal>context1</literal> etc).
+GHC's default behaviour is that <emphasis>exactly one instance must match the
+constraint it is trying to resolve</emphasis>.
+It is fine for there to be a <emphasis>potential</emphasis> of overlap (by
+including both declarations (A) and (B), say); an error is only reported if a
+particular constraint matches more than one.
+</para>
+
+<para>
+The <option>-XOverlappingInstances</option> flag instructs GHC to allow
+more than one instance to match, provided there is a most specific one. For
+example, the constraint <literal>C Int [Int]</literal> matches instances (A),
+(C) and (D), but the last is more specific, and hence is chosen. If there is no
+most-specific match, the program is rejected.
+</para>
+<para>
+However, GHC is conservative about committing to an overlapping instance. For example:
+<programlisting>
+ f :: [b] -> [b]
+ f x = ...
+</programlisting>
+Suppose that from the RHS of <literal>f</literal> we get the constraint
+<literal>C Int [b]</literal>. But
+GHC does not commit to instance (C), because in a particular
+call of <literal>f</literal>, <literal>b</literal> might be instantiate
+to <literal>Int</literal>, in which case instance (D) would be more specific still.
+So GHC rejects the program.
+(If you add the flag <option>-XIncoherentInstances</option>,
+GHC will instead pick (C), without complaining about
+the problem of subsequent instantiations.)
+</para>
+<para>
+Notice that we gave a type signature to <literal>f</literal>, so GHC had to
+<emphasis>check</emphasis> that <literal>f</literal> has the specified type.
+Suppose instead we do not give a type signature, asking GHC to <emphasis>infer</emphasis>
+it instead. In this case, GHC will refrain from
+simplifying the constraint <literal>C Int [b]</literal> (for the same reason
+as before) but, rather than rejecting the program, it will infer the type
+<programlisting>
+ f :: C Int [b] => [b] -> [b]
+</programlisting>
+That postpones the question of which instance to pick to the
+call site for <literal>f</literal>
+by which time more is known about the type <literal>b</literal>.
+You can write this type signature yourself if you use the
+<link linkend="flexible-contexts"><option>-XFlexibleContexts</option></link>
+flag.
+</para>
+<para>
+Exactly the same situation can arise in instance declarations themselves. Suppose we have
+<programlisting>
+ class Foo a where
+ f :: a -> a
+ instance Foo [b] where
+ f x = ...
+</programlisting>
+and, as before, the constraint <literal>C Int [b]</literal> arises from <literal>f</literal>'s
+right hand side. GHC will reject the instance, complaining as before that it does not know how to resolve
+the constraint <literal>C Int [b]</literal>, because it matches more than one instance
+declaration. The solution is to postpone the choice by adding the constraint to the context
+of the instance declaration, thus:
+<programlisting>
+ instance C Int [b] => Foo [b] where
+ f x = ...
+</programlisting>
+(You need <link linkend="instance-rules"><option>-XFlexibleInstances</option></link> to do this.)
+</para>
+<para>
+The willingness to be overlapped or incoherent is a property of
+the <emphasis>instance declaration</emphasis> itself, controlled by the
+presence or otherwise of the <option>-XOverlappingInstances</option>
+and <option>-XIncoherentInstances</option> flags when that module is
+being defined. Neither flag is required in a module that imports and uses the
+instance declaration. Specifically, during the lookup process: