I'm sorry to open an old wound. I've just had an insight for a clarification. On Nov 26, 2003 Ken Shan wrote:
Consider the following code, which uses type classes with functional dependencies:
{-# OPTIONS -fglasgow-exts #-} module Foo where class R a b | a -> b where r :: a -> b
-- 1 rr :: (R a b1, R a b2) => a -> (b1, b2) rr a = (r a, r a)
-- 2 data RAB a = RAB (forall b. (R a b) => (a, b)) mkRAB :: (R a b) => a -> b -> RAB a mkRAB a b = RAB (a, b)
Neither 1 nor 2 passes the type-checker (GHC 6.0.1). The error messages are similar: Inferred type is less polymorphic than expected Quantified type variable `b2' is unified with another quantified type variable When trying to generalise the type inferred for `rr' Signature type: forall a b1 b2. (R a b1, R a b2) => a -> (b1, b2) Type to generalise: a -> (b1, b1)
In both cases, the compiler is failing to make use of functional dependencies information that it has at its disposal. Specifically, it seems to me that, if two type variables b1 and b2 have been unified due to functional dependencies, making two constraints in the context identical, then the inner constraint ("inner" with respect to the scope of quantified type variables) should be ignored.
Regarding the function rr, I'm afraid I'm compelled to side with the typechecker. It appears that the typechecker does make use of the functional dependencies to reject the code because the user has specified too general a signature. Exactly the _same_ error occurs in the following code ab:: a -> Maybe a ab = Just rrr:: a -> (Maybe a, Maybe a1) rrr a = (ab a, ab a) Inferred type is less polymorphic than expected Quantified type variable `a1' is unified with another quantified type variable `a' When trying to generalise the type inferred for `rrr' Signature type: forall a a1. a -> (Maybe a, Maybe a1) Type to generalise: a1 -> (Maybe a1, Maybe a1) When checking the type signature for `rrr' When generalising the type(s) for `rrr' Error messages are identical. Because ab is a function rather than a method, there trivially is a functional dependency between the function's argument and its result. Furthermore, exactly the same error occurs in rrrr:: a -> b rrrr x = x Inferred type is less polymorphic than expected Quantified type variable `b' is unified with another quantified type variable `a' When trying to generalise the type inferred for `rrrr' Signature type: forall a b. a -> b Type to generalise: b -> b When checking the type signature for `rrrr' When generalising the type(s) for `rrrr' Regarding the original function rr, the best solution seems to be to let the compiler figure out its type. It seems in these circumstances the most general type exists -- and thus the compiler can figure it out. Now, regarding function mkRAB. It seems there is a simple solution: data RAB a = RAB (forall b. (R a b) => (a, b)) mkRAB a = RAB (a, r a) Indeed, the class R a b promised that there is a function 'r' such that given a value of type 'a' can produce a value of type 'b'. So, we can make use of such a function. One can object: in a value of a type RAB (forall b. (R a b) => (a, b)), the types of two components of a pair `(a, b)' must be related by the relation R a b. The values can in principle be arbitrary. What if one wishes to create a value RAB (x,z) such that the value z has the type of (r x) but is not equal to (r x)? Well, there is an underhanded way to help that. class R a b | a -> b where r :: a -> b r1 :: a -> Integer -> b that is, we define an additional method that takes an integer and somehow makes the value of a type 'b'. We may imagine an Array(s) of all possible values of type 'b' (specialized for those types 'b' for which there are instances of the class R) and the method r1 merely uses its second argument to select from that array. In any case, Goedel showed that quite many pleasant and unpleasant things can be encoded in integers. The first argument of r1 is merely a window dressing to make the typechecker happy. Thus we can define mkRAB' a b = RAB (a, r1 a b) To make the code more concrete, we introduce two instances instance R Int Char where {r = toEnum; r1 _ = toEnum . fromInteger} instance R Float (Maybe Float) where r = Just r1 _ 1 = Nothing r1 _ n = Just (fromRational $ toRational (n-1) / (2^(128+1))) In the second instances, we take advantage of the existence of an injection from IEEE floating-point numbers to integers. We can try evaluating "mkRAB 65", "mkRAB' 65 66", "mkRAB' (1.0::Float) 0", etc. -- and everything works. Building RAB values is not enough -- we should be able to use them. For example, we should be able to define the following function useRAB :: (Eq b, R a b) => RAB a -> b -> Bool useRAB (RAB (a, b1)) b2 = b1 == b2 As Ken Shan pointed out on Nov 27, 2003, it doesn't type. But the following does: useRAB (RAB x) b2 = (snd x) == b2 If we ask the typechecker to give us the type of useRAB, it says: *Foo> :t useRAB useRAB :: forall b a. (R a b, Eq b) => RAB a -> b -> Bool which is _precisely_ as we wished. It all seems to work: *Foo> useRAB (mkRAB (65::Int)) 'a' False *Foo> useRAB (mkRAB (65::Int)) 'A' True *Foo> useRAB (mkRAB (65::Int)) 'B' False *Foo> useRAB (mkRAB' (65::Int) 66) 'B' True *Foo> useRAB (mkRAB (1.0::Float)) (Just (1.0::Float)) True *Foo> useRAB (mkRAB' (1.0::Float) 1) Nothing True Am I missing something in the original problem?