[Haskell-cafe] Re: coherence when overlapping?

[oleg at pobox.com]

It seems that the subject is a bit more complex, and one can force GHC
to choose the less specific instance (if one confuses GHC well
enough): see the example below.

First of all, the inequality constraint is already achievable in
Haskell now: "TypeEq t1 t2 False" is such a constraint. One can
write polymorphic functions that distinguish if the argument a list
(any list of something) or not, etc. One can write stronger invariants
like records where labels are guaranteed to be unique.

There are two problems: first there are several notions of type
inequality, all of which are useful in different
circumstances. 
	http://www.haskell.org/pipermail/haskell-prime/2006-March/000936.html

Second, how inequality interacts with functional dependencies -- and
in general, with the type improvement. And here, many interesting
things emerge. For example, the following code


> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
>
> module Foo1 where
>
> class C a b | a -> b where
>     f :: a -> b
>
> instance C Int Bool where
>     f x = True
>
> instance TypeCast Int b => C a b where
>     f x = typeCast (100::Int)
>
> 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
>
> class D a b | a -> b where
>     g :: a -> b
>
> instance D Bool Bool where
>     g x = not x
>
> instance TypeCast a b => D a b where
>     g x = typeCast x
>
> test1 = f (42::Int) -- ==> True
> test2 = f 'a'       -- ==> 100
>
> test3 = g (1::Int)  -- ==> 1
> test4 = g True      -- ==> False
>
> bar x = g (f x) `asTypeOf` x

We see that test1 through test4 behave as expected. We can even define
the function 'bar'. It's inferred type is

	*Foo1> :t bar
	bar :: (C a b, D b a) => a -> a

The question becomes: is this a function? Can it be applied to
anything at all? If we apply it to Int (thus instantiating the type a to
Int), the type b is instantiated to Bool, and so (following the
functional dependency for class D), the type a should be Bool (and it
is already an Int). OTH, if we apply bar to anything but Int, then
the type b should be Int, and so should the type a. Liar's paradox.
And indeed, bar cannot be applied to anything because the constraints
are contradictory.

What is more interesting is the slight variation of that example:

> class C a b | a -> b where
>     f :: a -> b
>
> instance C Int Int where
>     f x = 10+x
>
> instance TypeCast a b => C a b where
>     f x = typeCast x
>
> class D a b | a -> b where
>     g :: a -> b
>
> instance D Int Bool where
>     g x = True
>
> instance TypeCast Int b => D a b where
>     g x = typeCast (10::Int)
>
> test1 = f (42::Int)
> test2 = f 'a'
>
> test3 = g (1::Int)
> test4 = g True
>
> bar x = g (f x) `asTypeOf` x
>
> test5 = bar (1::Int)

	*Foo> :t bar
	bar :: (C a b, D b a) => a -> a

If bar is applied to an Int, then the type b should be an Int, so the
first instance of D ought to have been chosen, which gives the
contradiction a = Bool. And yet it works (GHC 6.4.1). Test5 is
accepted and even works 
	*Foo> test5
	10