GHC, functional dependency, rank-2 type

oleg at oleg at
Mon Jan 12 21:50:42 EST 2004

There appears to be a problem with GHC's handling of multi-parameter
constraints with functional dependencies in the context of rank-2
types. The problem is not present in Hugs.

Let us first consider a simple example:

> module Test where
> class Foo a
> class Bar a
> data Obj = Obj
> instance Bar Obj
> instance (Bar a) => Foo a
> foo:: (Foo a) => a -> String
> foo _ = "works"
> runFoo:: (forall a. (Foo a) => a -> w) -> w
> runFoo f = f Obj

Here, the type of foo indicates

> Test> :t foo
> foo :: Foo a => a -> String

that foo can be applied to the value of any type so long as it is in
class Foo. The type of runFoo says that runFoo takes a function that
can process the value of every type of class Foo. The function foo
seems to be such a function. Therefore, "runFoo foo" should be
well-typed. And it is, and it works, both in Hugs (version November
2002) and in GHC 6.0.1 (which is the current version for FreeBSD).

However, if we make the classes Foo and Bar seemingly multi-parameter,
the trouble begins:

> class Foo a b | a->b
> class Bar a b | a->b
> data Obj = Obj
> instance Bar Obj Obj
> instance (Bar a b) => Foo a b
> foo:: (Foo a b) => a -> String
> foo _ = "works"
> runFoo:: (forall a b. (Foo a b) => a -> w) -> w
> runFoo f = f Obj

In Hugs:

> Test> :t foo   
> foo :: Foo a b => a -> String
> Test> runFoo foo
> "works"

As before, the function foo promises to handle the value of any type a
so long as "Foo a b" is satisfied (for any b -- although there can be
only one such b, due to the functional dependency). The function
runFoo takes any function that can handle the value of any type "a"
subject to the "Foo a b" constraint. So, "runFoo foo" should be
well-typed and should work. And it is, in Hugs.

GHC 6.01 is a different matter, unfortunately. An attempt to load the
above code in GHC succeeds, with flags:
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

Furthermore, the types of foo and runFoo seem to be in perfect match.

> *Test> :t foo
> foo :: forall a b. (Foo a b) => a -> String
> *Test> :t runFoo
> runFoo :: forall w. (forall a b. (Foo a b) => a -> w) -> w

And yet,

*Test> runFoo foo

    Could not deduce (Bar a b) from the context (Foo a b)
      arising from use of `foo' at <interactive>:1
    Probable fix:
        Add (Bar a b) to the expected type of an expression
    In the first argument of `runFoo', namely `foo'
    In the definition of `it': it = runFoo foo

Why all of the sudden does GHC need the constraint Bar a b? The
function foo didn't ask for that... However, if we define foo and
runFoo as follows:

> foo:: (Foo a b) => a -> b -> String
> foo _ _ = "works"
> runFoo:: (forall a b. (Foo a b) => a -> b -> w) -> w
> runFoo f = f Obj Obj

then both GHC and Hugs are happy: "runFoo foo" says that it works in both.

What's more bizarre, even the following works:

> runFoo:: (forall a b. (Foo a b) => a -> b -> w) -> w
> runFoo f = f Obj undefined

More information about the Haskell mailing list