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?-)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
