inference with functional dependencies
Inferring equality between types when there are functional dependencies seems to be less powerful than I expected. Here's a simple example: class Eq b => C a b | a -> b data T a = forall b . C a b => T b data U a = forall b . C a b => U b compare :: T a -> U a -> Bool compare (T x) (U y) = x == y I expected the compiler (GHC) would be able to deduce that the b type in the representation of T a and U a must be the same, since both stand in a C a b relationship, and a functionally determines b in that relationship. Instead I get the message: Inferred type is less polymorphic than expected Quantified type variable `b1' is unified with `b' When checking a pattern that binds x :: b y :: b1 In an equation for function `Test.compare': Test.compare (T x) (U y) = x == y Is this expected behavior? Is there a way for me to provide the necessary hints so that code like this could be accepted? Thanks, Avi Pfeffer -- Avi Pfeffer avi@eecs.harvard.edu www.eecs.harvard.edu/~avi Maxwell Dworkin 251 Division of Engineering and Applied Sciences Tel: (617) 496-1876 Harvard University Fax: (617) 496-1066
On 2001-08-13T18:08:08-0400, Avi Pfeffer wrote:
Inferring equality between types when there are functional dependencies seems to be less powerful than I expected. Here's a simple example:
class Eq b => C a b | a -> b
data T a = forall b . C a b => T b data U a = forall b . C a b => U b
compare :: T a -> U a -> Bool compare (T x) (U y) = x == y
Hrm, is it possible for you to define instead data T a b = C a b => T a b data U a b = C a b => U a b and propagate the dependency inference of "a -> b" upward in your program? Or even simply say data T a b = T a b data U a b = U a b and put the C constraint further higher up in your program? Just a thought... -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig I saw my inner child once, on a milk carton.
participants (2)
-
Avi Pfeffer -
Ken Shan