Superclass equalities

[Chris Kuklewicz]

On 22/06/2011 17:57, Simon Peyton-Jones wrote:
> I have long advertised a plan to allow so-called superclass equalities.  I've
> just pushed patches to implement them. So now you can write
> 
> class (F a ~ b) => C a b where  { ... }

That is fantastic.  I have a question about this feature as compared to the two
methods used to define the TypeCast superclass equality constraint in HList.

Can (~) replace all uses of TypeCast?  If not, then can (~) help define TypeCast
in a better way?  The two existing ways are a bit fragile.

I will put the TypeCast definitions below so readers of this question need not
go digging.  I just refreshed my understanding of TypeCast by re-reading
appendix D of the extended technical report for HList at [1,2].

The class TypeCast should only have instances when x and y are unified:

> class TypeCast x y | x -> y, y -> x where typeCast :: x -> y

The first definition for TypeCast is simply

> instance TypeCast x x where typeCast = id

But this was fragile since the class and instance have to be kept apart and the
instance has be imported carefully.  Quoting [2]:

> To keep the compiler from applying the type simplification rule too early, we
> should prevent the early inference of the rule from the instance of TypeCast
> in the first place. For example, we may keep the compiler from seeing the
> instance TypeCast x x until the very end. That is, we place that instance in
> a separate module and import it at a higher level in the module hierarchy
> than all clients of the class TypeCast.

The second definition of TypeCast can be included normally but is quite curious
looking:

> class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
> class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
> class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
> instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
> instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
> instance TypeCast'' () a a where typeCast'' _ x  = x

The HList authors follow this definition in [2] with:

> While this code works in GHC and is logically sound, we have to admit that
> we turned the drawbacks of the type-checker to our advantage. This leaves a
> sour after-taste. We would have preferred to rely on a sound semantic theory
> of overloading rather than on playing games with the type-checker. Hopefully,
> the results of the foundational work by Sulzmann and others [32, 23] will
> eventually be implemented in all Haskell compilers.

[1] Page: http://homepages.cwi.nl/~ralf/HList/
[2] Pdf: http://homepages.cwi.nl/~ralf/HList/paper.pdf