Superclass Cycle via Associated Type

[Nicolas Frisby]

(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