GHC, functional dependency, rank2 type
Simon PeytonJones
simonpj at microsoft.com
Tue Jan 13 11:17:03 EST 2004
That is indeed bizarre. I'll look into it.
Simon
 Original Message
 From: haskellbounces at haskell.org [mailto:haskellbounces 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, rank2 type


 There appears to be a problem with GHC's handling of multiparameter
 constraints with functional dependencies in the context of rank2
 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
 welltyped. 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 multiparameter,
 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
 welltyped 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 fglasgowexts fallowundecidableinstances #}

 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
More information about the Haskell
mailing list