[Haskell-cafe] Re: technique to allow innocuous ambiguity in instance declarations?

[oleg at pobox.com]

Nicolas Frisby posed a problem about controlling the order of
instance selection rules (or, the application of type improvement rules)

Given the following code

> newtype IdL a = IdL a
> newtype IdR a = IdR a
>
> class C f g where nest :: f a -> g a
>
> instance C IdL IdR where nest (IdL x) = IdR x
>
> newtype TransR f a = TransR (f a)
> newtype TransL f a = TransL (f a)
>
> instance C f g => C (TransL f) g where -- Instance1
>     nest (TransL x) = nest x
>
> instance C f g => C f (TransR g) where -- Instance2
>     nest x = TransR (nest x)

we can quite happily write

> test1 :: TransL IdL a -> IdR a
> test1 = nest

and ditto

> test2 :: IdL a -> TransR IdR a
> test2 = nest

but we can't write

> testx :: TransL IdL a -> TransR IdR a
> testx = nest

because the typechecker doesn't know which instance to choose: either
to attempt to improve constraints  as
       C (TransL IdL) (TransR IdR) --> C IdL (TransR IdR) -->
		C IdL IdR
(choosing the Instance1 first)
or
       C (TransL IdL) (TransR IdR) --> C (TransL IdL) IdR -->
		C IdL IdR
choosing Instance2 first.

One can see that the end result is just the same. But the typechecker
doesn't actually know that instances commute, so it reports the
ambiguity and quits. But suppose we do know that these particular
instances commute. How to impart this knowledge to the typechecker?
Or, simply, how to tell the typechecker to remove the ambiguity by
choosing Instance1 first?

It turns out, there is a simple way. It relies again on this quite
useful contraption, TypeCast. The idea is to introduce the most
general instance C f g. The typechecker will choose it if nothing more
specific applies. And then we examine f and g to see what we've got
and how to proceed from that. At that point, it's us who decides what
to improve first. The idea is similar to the one described in

      http://pobox.com/~oleg/ftp/Haskell/types.html#is-function-type

The complete code follows. Now testx typechecks.


> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
>
> module N where
>
> newtype IdL a = IdL a
> newtype IdR a = IdR a
>
> class C f g where nest :: f a -> g a
>
> instance C IdL IdR where nest (IdL x) = IdR x
>
> newtype TransR f a = TransR (f a)
> newtype TransL f a = TransL (f a)
>
> instance (IsTransL f b, C' b f g) => C f g where
>     nest = nest' (undefined::b)
>
> class C' b f g where nest' :: b -> f a -> g a
>
> instance C f g => C' HTrue (TransL f) g where
>     nest' _ (TransL x) = nest x
>
> instance C f g => C' HFalse f (TransR g) where
>     nest' _ x = TransR (nest x)
>
> {- From the first attempt
> instance C f g => C (TransL f) g where
>     nest (TransL x) = nest x
>
> instance C f g => C f (TransR g) where
>     nest x = TransR (nest x)
> -}
>
> test1 :: TransL IdL a -> IdR a
> test1 = nest
>
> test2 :: IdL a -> TransR IdR a
> test2 = nest
>
>
> testx :: TransL IdL a -> TransR IdR a
> testx = nest
>
> data HTrue
> data HFalse
>
> class IsTransL (a :: * -> * ) b | a -> b
> instance TypeCast f HTrue => IsTransL (TransL y) f
> instance TypeCast f HFalse => IsTransL a f
>
>
> -- Our silver bullet
>
> 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