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