I talked to Dimitrios. Fundamentally we think we should be able to handle recursive superclasses, albeit we have a bit more work to do on the type inference engine first. The situation we think we can handle ok is stuff like Edward wants (I've removed all the methods): class LeftModule Whole m => Additive m class Additive m => Abelian m class (Semiring r, Additive m) => LeftModule r m class Multiplicative m where (*) :: m -> m -> m class LeftModule Natural m => Monoidal m class (Abelian m, Multiplicative m, LeftModule m m) => Semiring m class (LeftModule Integer m, Monoidal m) => Group m class Multiplicative m => Unital m class (Monoidal r, Unital r, Semiring r) => Rig class (Rig r, Group r) => Ring r The superclasses are recursive but a) They constrain only type variables b) The variables in the superclass context are all mentioned in the head. In class Q => C a b c fv(Q) is subset of {a,b,c} Question to all: is that enough? ======= The main difficulty with going further ============== Here's an extreme case class A [a] => A a where op :: a -> Int f :: A a => a -> Int f x = [[[[[x]]]]] + 1 The RHS of f needs A [[[[[a]]]]] The type sig provides (A a), and hence (A [a]), and hence (A [[a]]) and so on. BUT it's hard for the solver to spot all the now-infinite number of things that are provided by the type signature. Gabor's example is less drastic class Immutable (Frozen a) => Mutable a where type Frozen a class Mutable (Thawed a) => Immutable a where type Thawed a but not much less drastic. (Mutable a) in a signature has a potentially infinite number of superclasses Immutable (Frozen a) Mutable (Thawed (Frozen a)) ...etc... It's not obvious how to deal with this. However Gabor's example can perhaps be rendered with a MPTC: class (Frozen t ~ f, Thawed f ~ t) => Mutable f t where type Frozen a type Thawed a unsafeFreeze :: t -> Frozen t unsafeThaw :: f -> Thawed f And you can do *that* today. Simon