Type class problem

Brandon Michael Moore brandon@its.caltech.edu
Thu, 14 Aug 2003 16:43:57 -0700 (PDT)


To try some of the examples from paper "Recursion Schemes from Comonads",
I wanted to define instances of Show and Observable for types defined as
the fixed point of a functor.

I defined type recursion and naturals as

>newtype Mu f = In {unIn :: f (Mu f)}
>data N f = S f | Z
>type Nat = Mu N

An application of Mu should be showable if the functor maps showable types
to showable types, so the most natural way to define the instance seemed
to be

instance (Show a => Show (f a)) => Show (Mu f) where
  show (In x) = show x

Of course that constraint didn't work, so I made a class PShow with a
method that witnessed the constraint

>class PShow f where
>  pshow :: (Show a) => f a -> String

Now I could define a generic show instance for Mu, and got a Show instance
for Nat by defing a PShow instance for N

>instance (PShow f) => Show (Mu f) where
>  show (In x) = pshow x

>instance PShow N where
>  pshow Z = "Z"
>  pshow (S k) = "S "+show K

show (In (S (In (S (In Z))))) -> "S S Z"

This works fine, but you need to be able to use the method of P<Class> in
the definition of <Class> (Mu f). I couldn't figure out how to do the same
thing with Observable (the use of the class methods is a few layers away
from the public interface).

I tried to define a set of mutaully recursive definitions

instance (Observable (f (Mu f))) => Observable (Mu f) where
  observer (In x) = send "In" (return In << x)
instance (Observable a) => Observable (N a) where
  observer Z = send "Z" (return Z)
  observer (S x) = send "S" (return S << x)

unfortunately, the class constraint solver doesn't doesn't like this. I
get an error message like

Constraint Stack Overflow:
  Observable (N (Mu N))
  Observable (Mu N)
  Observable (N (Mu N))
  Observable (Mu N)
  ...

I expected that that constraint solver would realize it could construct a
dictionary transformer with a type like Observer Nat -> Observer Nat and
take the fixed point to get an instance for Nat. I haven't looked at the
implementation, but it seems like it would be easy to add the constraint
we are trying to derive to the list of assumptions when trying to
construct all the anteceedents of an instance declaration.

Can anyone tell me how to
1) get around this
2) modify GHC to handle this :)

Brandon