Functional dependencies interfere with generalization

[Ken Shan]

Hello,

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 `b1'
    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)
    When checking the type signature for `rr'
    When generalising the type(s) for `rr'

    Inferred type is less polymorphic than expected
        Quantified type variable `b' escapes
        It is mentioned in the environment:
          b :: b (bound at Foo.hs:17)
    In the first argument of `RAB', namely `(a, b)'
    In the definition of `mkRAB': mkRAB a b = RAB (a, b)

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.

Is there a technical reason why the type checker should reject the code
above?  Would it be possible to at least automatically define a function
like

    equal :: forall f a b1 b1. (R a b1, R a b2) => f b1 -> f b2

for every functional dependency, with which I would be able to persuade
the type checker to generalize (Baars and Swierstra, ICFP 2002)?  I
suppose I can use unsafeCoerce to manually define such a function... is
that a bad idea for some reason I don't see?

Thank you,
	Ken

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
Tax the rich!
new journal Physical Biology: http://physbio.iop.org/
What if All Chemists Went on Strike? (science fiction):
http://www.iupac.org/publications/ci/2003/2506/iw3_letters.html
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://haskell.org/pipermail/haskell/attachments/20031126/958d8c2f/attachment.bin