7.8. Multi-parameter type classes

This section documents GHC's implementation of multi-parameter type classes. There's lots of background in the paper Type classes: exploring the design space (Simon Peyton Jones, Mark Jones, Erik Meijer).

I'd like to thank people who reported shorcomings in the GHC 3.02 implementation. Our default decisions were all conservative ones, and the experience of these heroic pioneers has given useful concrete examples to support several generalisations. (These appear below as design choices not implemented in 3.02.)

I've discussed these notes with Mark Jones, and I believe that Hugs will migrate towards the same design choices as I outline here. Thanks to him, and to many others who have offered very useful feedback.

7.8.1. Types

There are the following restrictions on the form of a qualified type:

  forall tv1..tvn (c1, ...,cn) => type

(Here, I write the "foralls" explicitly, although the Haskell source language omits them; in Haskell 1.4, all the free type variables of an explicit source-language type signature are universally quantified, except for the class type variables in a class declaration. However, in GHC, you can give the foralls if you want. See Section 7.11).

  1. Each universally quantified type variable tvi must be mentioned (i.e. appear free) in type. The reason for this is that a value with a type that does not obey this restriction could not be used without introducing ambiguity. Here, for example, is an illegal type:
      forall a. Eq a => Int
    When a value with this type was used, the constraint Eq tv would be introduced where tv is a fresh type variable, and (in the dictionary-translation implementation) the value would be applied to a dictionary for Eq tv. The difficulty is that we can never know which instance of Eq to use because we never get any more information about tv.

  2. Every constraint ci must mention at least one of the universally quantified type variables tvi. For example, this type is OK because C a b mentions the universally quantified type variable b:
      forall a. C a b => burble
    The next type is illegal because the constraint Eq b does not mention a:
      forall a. Eq b => burble
    The reason for this restriction is milder than the other one. The excluded types are never useful or necessary (because the offending context doesn't need to be witnessed at this point; it can be floated out). Furthermore, floating them out increases sharing. Lastly, excluding them is a conservative choice; it leaves a patch of territory free in case we need it later.

These restrictions apply to all types, whether declared in a type signature or inferred.

Unlike Haskell 1.4, constraints in types do not have to be of the form (class type-variables). Thus, these type signatures are perfectly OK

  f :: Eq (m a) => [m a] -> [m a]
  g :: Eq [a] => ...

This choice recovers principal types, a property that Haskell 1.4 does not have.

7.8.2. Class declarations

  1. Multi-parameter type classes are permitted. For example:
      class Collection c a where
        union :: c a -> c a -> c a
        ...etc.

  2. The class hierarchy must be acyclic. However, the definition of "acyclic" involves only the superclass relationships. For example, this is OK:
      class C a where {
        op :: D b => a -> b -> b
      }
    
      class C a => D a where { ... }
    Here, C is a superclass of D, but it's OK for a class operation op of C to mention D. (It would not be OK for D to be a superclass of C.)

  3. There are no restrictions on the context in a class declaration (which introduces superclasses), except that the class hierarchy must be acyclic. So these class declarations are OK:
      class Functor (m k) => FiniteMap m k where
        ...
    
      class (Monad m, Monad (t m)) => Transform t m where
        lift :: m a -> (t m) a

  4. In the signature of a class operation, every constraint must mention at least one type variable that is not a class type variable. Thus:
      class Collection c a where
        mapC :: Collection c b => (a->b) -> c a -> c b
    is OK because the constraint (Collection a b) mentions b, even though it also mentions the class variable a. On the other hand:
      class C a where
        op :: Eq a => (a,b) -> (a,b)
    is not OK because the constraint (Eq a) mentions on the class type variable a, but not b. However, any such example is easily fixed by moving the offending context up to the superclass context:
      class Eq a => C a where
        op ::(a,b) -> (a,b)
    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.

  5. The type of each class operation must mention all of the class type variables. For example:
      class Coll s a where
        empty  :: s
        insert :: s -> a -> s
    is not OK, because the type of empty doesn't mention a. 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, Coll might be rewritten
      class Coll s a where
        empty  :: s a
        insert :: s a -> a -> s a
    which makes the connection between the type of a collection of a's (namely (s a)) and the element type a. Occasionally this really doesn't work, in which case you can split the class like this:
      class CollE s where
        empty  :: s
    
      class CollE s => Coll s a where
        insert :: s -> a -> s

7.8.3. Instance declarations

  1. Instance declarations may not overlap. The two instance declarations
      instance context1 => C type1 where ...
      instance context2 => C type2 where ...
    "overlap" if type1 and type2 unify However, if you give the command line option -fallow-overlapping-instances then two overlapping instance declarations are permitted iff

    • EITHER type1 and type2 do not unify

    • OR type2 is a substitution instance of type1 (but not identical to type1)

    • OR vice versa

    Notice that these rules

    • make it clear which instance decl to use (pick the most specific one that matches)

    • do not mention the contexts context1, context2 Reason: you can pick which instance decl "matches" based on the type.

    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 Main. 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 Main.)

  2. There are no restrictions on the type in an instance head, except that at least one must not be a type variable. The instance "head" is the bit after the "=>" in an instance decl. For example, these are OK:
      instance C Int a where ...
    
      instance D (Int, Int) where ...
    
      instance E [[a]] where ...
    Note that instance heads may contain repeated type variables. For example, this is OK:
      instance Stateful (ST s) (MutVar s) where ...
    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:
      instance C a => C a where ...
    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:
      instance C a where
        op = ... -- Default
    Second, sometimes you might want to use the following to get the effect of a "class synonym":
      class (C1 a, C2 a, C3 a) => C a where { }
    
      instance (C1 a, C2 a, C3 a) => C a where { }
    This allows you to write shorter signatures:
      f :: C a => ...
    instead of
      f :: (C1 a, C2 a, C3 a) => ...
    I'm on the lookout for a simple rule that preserves decidability while allowing these idioms. The experimental flag -fallow-undecidable-instances lifts this restriction, allowing all the types in an instance head to be type variables.

  3. Unlike Haskell 1.4, 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:
      type Point = (Int,Int)
      instance C Point   where ...
      instance C [Point] where ...
    is legal. However, if you added
      instance C (Int,Int) where ...
    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:
      type P a = [[a]]
      instance Monad P where ...
    This design decision is independent of all the others, and easily reversed, but it makes sense to me.

  4. The types in an instance-declaration context must all be type variables. Thus
    instance C a b => Eq (a,b) where ...
    is OK, but
    instance C Int b => Foo b where ...
    is not OK. Again, the intent here is to make sure that context reduction terminates. Voluminous correspondence on the Haskell mailing list has convinced me that it's worth experimenting with a more liberal rule. If you use the flag -fallow-undecidable-instances can use arbitrary types in an instance context. 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 -fcontext-stackN.