[Haskell-cafe] Re: coherence when overlapping?

[Claus Reinke]

> one can force GHC to choose the less specific instance (if one 
> confuses GHC well enough): see the example below.

your second example doesn't really do that, though it may look that way.

>> 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)
..
>> 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

your argument seems to imply that you see FD range parameters as
outputs of the instance inference process (*), so that the first Int 
parameter in the constraint D Int Int is sufficient to select the first 
instance (by ignoring the Int in the second parameter and using 
best-fit overlap resolution), leading to the contradiction Int=Bool.

alas, current FD implementations don't work that way..

Hugs will complain about the overlap being inconsistent with the FD,
for both C and D - does it just look at the instance heads?

GHC will accept D even without overlapping instances enabled, 
but will complain about C, so it seems that it takes the type equality
implied by FDs in instance contexts into account, seeing instances
D Int Bool and D a Int - no overlaps. similarly, when it sees a
constraint D Int Int, only the second instance head will match..

if you comment out the second C instance, and disable overlaps,
the result of test5 will be the same.

> First of all, the inequality constraint is already achievable in
> Haskell now: "TypeEq t1 t2 False" is such a constraint. 

as you noted, that is only used as a constraint, for checks after
instantiation, which is of little help as current Haskell has corners that 
ignore constraints (such as instance selection). specifically, there is a 
difference between the handling of type equality and type inequality: 
the former can be implied by FDs, which are used in instance 
selection, the latter can't and isn't (which is why I'd like to have
inequality constraints that are treated the same way as FD-based
equality constraints, even where constraints are otherwise ignored).

if we want to formalise the interaction of FDs and overlap resolution,
and we want to formalise the latter via inequality guards, then it 
seems that we need to put inequality constraints (negative type 
variable substitutions) on par with equality constraints (positive 
type variable substitutions).

cheers,
claus

(*) or does it seem to me to be that way because that is how I'd
    like FD range parameters to be treated?-)