[Haskell-cafe] Functional dependencies and type inference

[Simon Peyton-Jones]

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: haskell-cafe-bounces at haskell.org
[mailto:haskell-cafe-bounces at haskell.org] On Behalf Of
| Einar Karttunen
| Sent: 15 July 2005 13:48
| To: haskell-cafe at haskell.org
| Subject: [Haskell-cafe] 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:0-32
|       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