+<para>
+ <emphasis>Multi-parameter type classes are permitted</emphasis>. For example:
+
+
+<programlisting>
+ class Collection c a where
+ union :: c a -> c a -> c a
+ ...etc.
+</programlisting>
+
+
+
+</para>
+</listitem>
+<listitem>
+
+<para>
+ <emphasis>The class hierarchy must be acyclic</emphasis>. However, the definition
+of "acyclic" involves only the superclass relationships. For example,
+this is OK:
+
+
+<programlisting>
+ class C a where {
+ op :: D b => a -> b -> b
+ }
+
+ class C a => D a where { ... }
+</programlisting>
+
+
+Here, <literal>C</literal> is a superclass of <literal>D</literal>, but it's OK for a
+class operation <literal>op</literal> of <literal>C</literal> to mention <literal>D</literal>. (It
+would not be OK for <literal>D</literal> to be a superclass of <literal>C</literal>.)
+
+</para>
+</listitem>
+<listitem>
+
+<para>
+ <emphasis>There are no restrictions on the context in a class declaration
+(which introduces superclasses), except that the class hierarchy must
+be acyclic</emphasis>. So these class declarations are OK:
+
+
+<programlisting>
+ class Functor (m k) => FiniteMap m k where
+ ...
+
+ class (Monad m, Monad (t m)) => Transform t m where
+ lift :: m a -> (t m) a
+</programlisting>
+
+
+</para>
+</listitem>
+<listitem>
+
+<para>
+ <emphasis>In the signature of a class operation, every constraint
+must mention at least one type variable that is not a class type
+variable</emphasis>.
+
+Thus:
+
+
+<programlisting>
+ class Collection c a where
+ mapC :: Collection c b => (a->b) -> c a -> c b
+</programlisting>
+
+
+is OK because the constraint <literal>(Collection a b)</literal> mentions
+<literal>b</literal>, even though it also mentions the class variable
+<literal>a</literal>. On the other hand:
+
+
+<programlisting>
+ class C a where
+ op :: Eq a => (a,b) -> (a,b)
+</programlisting>
+
+
+is not OK because the constraint <literal>(Eq a)</literal> mentions on the class
+type variable <literal>a</literal>, but not <literal>b</literal>. However, any such
+example is easily fixed by moving the offending context up to the
+superclass context:
+
+
+<programlisting>
+ class Eq a => C a where
+ op ::(a,b) -> (a,b)
+</programlisting>
+
+
+A yet more relaxed rule would allow the context of a class-op signature
+to mention only class type variables. However, that conflicts with
+Rule 1(b) for types above.
+
+</para>
+</listitem>
+<listitem>
+
+<para>
+ <emphasis>The type of each class operation must mention <emphasis>all</emphasis> of
+the class type variables</emphasis>. 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>. This rule is a consequence of Rule 1(a), above, for
+types, and has the same motivation.
+
+Sometimes, offending class declarations exhibit misunderstandings. For
+example, <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>
+</listitem>
+
+</OrderedList>
+
+</para>
+
+</sect3>
+
+<sect3 id="instance-decls">
+<title>Instance declarations</title>
+
+<para>
+
+<OrderedList>
+<listitem>
+
+<para>
+ <emphasis>Instance declarations may not overlap</emphasis>. The two instance
+declarations
+
+
+<programlisting>
+ instance context1 => C type1 where ...
+ instance context2 => C type2 where ...
+</programlisting>
+
+
+"overlap" if <literal>type1</literal> and <literal>type2</literal> unify
+
+However, if you give the command line option
+<option>-fallow-overlapping-instances</option><indexterm><primary>-fallow-overlapping-instances
+option</primary></indexterm> then overlapping instance declarations are permitted.
+However, GHC arranges never to commit to using an instance declaration
+if another instance declaration also applies, either now or later.
+
+<itemizedlist>
+<listitem>
+
+<para>
+ EITHER <literal>type1</literal> and <literal>type2</literal> do not unify
+</para>
+</listitem>
+<listitem>
+
+<para>
+ OR <literal>type2</literal> is a substitution instance of <literal>type1</literal>
+(but not identical to <literal>type1</literal>), or vice versa.
+</para>
+</listitem>
+</itemizedlist>
+Notice that these rules
+<itemizedlist>
+<listitem>
+
+<para>
+ make it clear which instance decl to use
+(pick the most specific one that matches)
+
+</para>
+</listitem>
+<listitem>
+
+<para>
+ do not mention the contexts <literal>context1</literal>, <literal>context2</literal>
+Reason: you can pick which instance decl
+"matches" based on the type.
+</para>
+</listitem>
+
+</itemizedlist>
+However the rules are over-conservative. Two instance declarations can overlap,
+but it can still be clear in particular situations which to use. For example:
+<programlisting>
+ instance C (Int,a) where ...
+ instance C (a,Bool) where ...
+</programlisting>
+These are rejected by GHC's rules, but it is clear what to do when trying
+to solve the constraint <literal>C (Int,Int)</literal> because the second instance
+cannot apply. Yell if this restriction bites you.
+</para>
+<para>
+GHC is also conservative about committing to an overlapping instance. For example:
+<programlisting>
+ class C a where { op :: a -> a }
+ instance C [Int] where ...
+ instance C a => C [a] where ...
+
+ f :: C b => [b] -> [b]
+ f x = op x
+</programlisting>
+From the RHS of f we get the constraint <literal>C [b]</literal>. But
+GHC does not commit to the second instance declaration, because in a paricular
+call of f, b might be instantiate to Int, so the first instance declaration
+would be appropriate. So GHC rejects the program. If you add <option>-fallow-incoherent-instances</option>
+GHC will instead silently pick the second instance, without complaining about
+the problem of subsequent instantiations.
+</para>
+<para>
+Regrettably, GHC doesn't guarantee to detect overlapping instance
+declarations if they appear in different modules. GHC can "see" the
+instance declarations in the transitive closure of all the modules
+imported by the one being compiled, so it can "see" all instance decls
+when it is compiling <literal>Main</literal>. However, it currently chooses not
+to look at ones that can't possibly be of use in the module currently
+being compiled, in the interests of efficiency. (Perhaps we should
+change that decision, at least for <literal>Main</literal>.)
+
+</para>
+</listitem>
+<listitem>
+
+<para>
+ <emphasis>There are no restrictions on the type in an instance
+<emphasis>head</emphasis>, except that at least one must not be a type variable</emphasis>.
+The instance "head" is the bit after the "=>" in an instance decl. For
+example, these are OK:
+
+
+<programlisting>
+ instance C Int a where ...
+
+ instance D (Int, Int) where ...
+
+ instance E [[a]] where ...
+</programlisting>
+
+
+Note that instance heads <emphasis>may</emphasis> contain repeated type variables.
+For example, this is OK:
+
+
+<programlisting>
+ instance Stateful (ST s) (MutVar s) where ...
+</programlisting>
+
+
+The "at least one not a type variable" restriction is to ensure that
+context reduction terminates: each reduction step removes one type
+constructor. For example, the following would make the type checker
+loop if it wasn't excluded:
+
+
+<programlisting>
+ instance C a => C a where ...
+</programlisting>
+
+
+There are two situations in which the rule is a bit of a pain. First,
+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>
+
+
+Second, 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>
+
+
+I'm on the lookout for a simple rule that preserves decidability while
+allowing these idioms. The experimental flag
+<option>-fallow-undecidable-instances</option><indexterm><primary>-fallow-undecidable-instances
+option</primary></indexterm> lifts this restriction, allowing all the types in an
+instance head to be type variables.
+
+</para>
+</listitem>
+<listitem>
+
+<para>
+ <emphasis>Unlike Haskell 1.4, instance heads may use type
+synonyms</emphasis>. 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>
+
+
+This design decision is independent of all the others, and easily
+reversed, but it makes sense to me.
+
+</para>