[Haskellcafe] Functional dependencies and type inference
Simon PeytonJones
simonpj at microsoft.com
Thu Aug 11 06:39:32 EDT 2005
Einar
Good question. This is a more subtle form of the same problem as I
described in my last message. In fact, it's what Martin Sulzmann calls
"the critical example". Here is a boiled down version, much simpler to
understand.
module Proxy where
class Dep a b  a > b
instance Dep Char Bool
foo :: forall a. a > (forall b. Dep a b => a > b) > Int
foo x f = error "urk"
bar :: (Char > Bool) > Int
bar g = foo 'c' g
You would think this should be legal, since bar is just an instantation
of foo, with a=Char and b=Bool. But GHC rejects it. Why?
GHC looks at the call to foo (in bar's RHS), and instantiates it with
a=Char. That tells it that the second argument should have type
(forall b. Dep Char b => Char > b)
But it doesn't! It has type (Char > Bool). And to GHC these are not
the same types.
You may say that they *should* be the same types. The crispest way I
know to explain why it arguably should be rejected is to try translating
the program into System F (which is what GHC actually does). Then the
RHS of bar looks like
bar (g::Char>Bool) = foo {Char} 'c' (...???...)
The {Char} is the type argument to foo. But what can we pass for
(...???...)?. We must pass a polymorphic function, with type
forall b. Dep Char b > Char > b
But all we have is g::Char>Bool. And System F has no way to connect
the two.
Well, that's the problem anyway. I can think of three "solutions":
 Reject such programs (GHC's current solution)
 Abandon compilation via System F
 Extend System F
I'm working on the third of these, with Martin, Manuel, and Stephanie.
Simon
 Original Message
 From: haskellcafebounces at haskell.org
[mailto:haskellcafebounces at haskell.org] On Behalf Of
 Einar Karttunen
 Sent: 15 July 2005 13:48
 To: haskellcafe at haskell.org
 Subject: [Haskellcafe] Functional dependencies and type inference

 Hello

 I am having problems with GHC infering functional dependencies related
 types in a too conservative fashion.

 > class Imp2 a b  a > b
 > instance Imp2 (Foo a) (Wrap a)
 >
 >
 > newtype Wrap a = Wrap { unWrap :: a }
 > data Foo a = Foo
 > data Proxy (cxt :: * > *)
 >
 > foo :: Imp2 (ctx c) d => Proxy ctx > (forall a b. (Imp2 (ctx a) b)
=> a > b) > c > d
 > foo p f x = f x

 The type of "foo (undefined :: Proxy Foo)" is inferred as
 "forall c. (forall a b. (Imp2 (Foo a) b) => a > b) > c > Wrap c"
 which shows the outmost functional dependence is working fine. ctx
 is carried to the inner Imp2.

 However "foo (undefined :: Proxy Foo) Wrap" will fail complaining that

 Couldn't match the rigid variable `b' against `Wrap a'
 `b' is bound by the polymorphic type `forall a b. (Imp2 (ctx a)
b) => a > b'
 at <interactive>:1:032
 Expected type: a > b
 Inferred type: a > Wrap a
 In the second argument of `foo', namely `Wrap'

 My guess is that GHC cannot see that the functional dependency
 guarantees that there are no instances which make the inferred
 type invalid. Any solutions to this problem?


  Einar Karttunen
More information about the HaskellCafe
mailing list