Why does this result in a conflict?
class Foo a b | b -> a where
foo :: a -> b -> Bool
instance Eq a => Foo a a where
foo = (==)
instance Eq a => Foo a (a -> a) where
foo x f = f x == x
Note that the code will compile if I remove the functional dependecy.
I was under the impression that functional dependencies should only disallow stuff like the following, when in fact, it compiles!
class Foo a b | b -> a where
foo :: a -> b -> Bool
instance Eq a => Foo a a where
foo = (==)
instance Eq a => Foo Bool a where
foo _ x = x == x
Same b
parameter, yet different a
parameters. Shouldn't b -> a
disallow this, as this means a
is uniquely determined by b
?
Have you tried actually using the second version? I'm guessing that while the instances compile, you'll start getting ambiguity and overlap errors when you call foo
.
The biggest stumbling block here is that fundeps don't interact with type variables the way you might expect them to--instance selection doesn't really look for solutions, it just blindly matches by attempting unification. Specifically, when you write Foo a a
, the a
is completely arbitrary, and can thus unify with a type like b -> b
. When the second parameter has the form b -> b
, it therefore matches both instances, but the fundeps say that in one case the first parameter should be b -> b
, but in the other that it should be b
. Hence the conflict.
Since this apparently surprises people, here's what happens if you try to use the second version:
bar = foo () ()
results in:
Couldn't match type `Bool' with `()'
When using functional dependencies to combine
Foo Bool a,
...because the fundep says, via the second instance, that any type as the second parameter uniquely determines Bool
as the first. So the first parameter must be Bool
.
bar = foo True ()
results in:
Couldn't match type `()' with `Bool'
When using functional dependencies to combine
Foo a a,
...because the fundep says, via the first instance, that any type as the second parameter uniquely determines the same type for the first. So the first parameter must be ()
.
bar = foo () True
results in errors due to both instances, since this time they agree that the first parameter should be Bool
.
bar = foo True True
results in:
Overlapping instances for Foo Bool Bool
arising from a use of `foo'
...because both instances are satisfied, and therefore overlap.
Pretty fun, huh?