(Sorry I'm so late to this dialogue.) In http://www.haskell.org/pipermail/glasgow-haskell-users/2011-July/020593.html, SPJ asks

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?

I just recently came upon my own desire for this capability, but I'm pretty sure my reply to SPJ's question is "No." I'd like to extend Sat's modeling capabilities to also cover superclass constraints.

type family Super a class Sat (Super a) => Sat a where dict :: a

This seems to necessitate recursive dictionaries — I'm not familiar enough with the dictionary-implementation details to understand how much of an understatement that might be. All I can say is that my own intuitions about those things don't yet deem this technique infeasible. Let's take a reification of Ord as an example.

data EmptyD a = EmptyD type instance Super (EmptyD a) = EmptyD a instance Sat (EmptyD a) where dict = EmptyD

data EqD a where EqD :: Eq a => EqD a type instance Super (EqD a) = EmptyD a instance Eq a => Sat (EqD a) where dict = EqD

data OrdD a where OrdD :: Ord a => OrdD a type instance Super (OrdD a) = EqD a instance Ord a => Sat (OrdD a) where dict = OrdD

Now GHC can derive Sat (EqD a) from Sat (OrdD a). I'd bet this could be cleaned via Constraint Kinds [1] — if not totally subsumed by them:

type family Super a :: Constraint class Super a => Sat a where dict :: a

data OrdD a where OrdD :: Ord a => OrdD a type instance Super (OrdD a) = Ord a instance Ord a => Sat (OrdD a) where dict = OrdD

With these definitions, there'd be an isomorphism between Sat (OrdD a) and Ord a. I don't know how difficult it would be for GHC to wield that isomorphism. At this point, though, perhaps Constraint Kinds simply deprecate Sat? [1] does, after all, define "one reified dictionary to rule them all". ----- [1] - http://blog.omega-prime.co.uk/?p=127