Superclass Cycle via Associated Type

[Simon Peyton-Jones]

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