That is indeed bizarre. I'll look into it. Simon | -----Original Message----- | From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of | oleg@pobox.com | Sent: 13 January 2004 05:51 | To: haskell@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@haskell.org | http://www.haskell.org/mailman/listinfo/haskell