GHC, functional dependency, rank-2 type

[Simon Peyton-Jones]

That is indeed bizarre.  I'll look into it.

Simon

| -----Original Message-----
| From: haskell-bounces at haskell.org [mailto:haskell-bounces at haskell.org]
On Behalf Of
| oleg at pobox.com
| Sent: 13 January 2004 05:51
| To: haskell at haskell.org
| Subject: GHC, functional dependency, rank-2 type
| 
| 
| 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
| 
| <interactive>:1:
|     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
| 
| _______________________________________________
| Haskell mailing list
| Haskell at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell