[Haskell-cafe] Functional dependencies and type inference

[Simon Peyton-Jones]

Thomas

Strange and interesting example!  If I had a pound for every time functional dependencies had messed up my brain, I'd be a rich man.   Apart from anything else, your example is another case of the "critical example"
	http://www.haskell.org/pipermail/haskell-cafe/2005-August/010974.html
as you mention.   It's also jolly strange that GHC infers the (un-writable) type
	bar :: (forall r. (Dep Int r) => Int -> r) -> Bar -> Char
but you can write neither that type nor
	bar :: (Int -> Bool) -> Bar -> Char
so in fact GHC won't type the bogus type-cast.  Nevertheless, those are artefacts of GHC's not-yet-right implementation of fundeps.  

I think the real problem here is that the "newtype-deriving" mechanism isn't conservative enough.  Given
	class C a where { op :: ty }
	newtype T = MkT S
the idea is that if S is an instance of a class C, then T can be, witnessed by the same functions.

That amounts to saying that 
	ty[S/a] is interchangeable with ty[T/a]
and that isn't really true when fundeps get in on the act.

I can't say I really understand it fully, but that's as far as I can take it today. 

Question: what restrictions on the newtype-deriving mechanism would make it sound?  

Simon

| -----Original Message-----
| From: Thomas Jäger [mailto:thjaeger at gmail.com]
| Sent: 23 August 2005 02:02
| To: Simon Peyton-Jones
| Cc: Einar Karttunen; haskell-cafe at haskell.org
| Subject: Re: [Haskell-cafe] Functional dependencies and type inference
| 
| Simon,
| 
| I believe there may be some nasty interactions with generalized
| newtype-deriving, since we can construct two Leibniz-equal types which
| are mapped to different types using fundeps:
| 
|   class Foo a where
|     foo :: forall f. f Int -> f a
| 
|   instance Foo Int where
|     foo = id
| 
|   newtype Bar = Bar Int deriving Foo
| 
|   -- 'Equality' of Int and Bar
|   eq :: forall f. f Int -> f Bar
|   eq = foo
| 
|   class Dep a b | a -> b
| 
|   instance Dep Int Bool
|   instance Dep Bar Char
| 
|   newtype Baz a = Baz { runBaz :: forall r. Dep a r => a -> r }
| 
|   conv :: (forall f. f a -> f b) ->
|     (forall r. Dep a r => a -> r) -> (forall r. Dep b r => b -> r)
|   conv f g = runBaz $ f (Baz g)
| 
|   bar = conv eq
| 
| Here, after type erasure, 'bar' is the identity function . Ghc infers
| 
|   bar :: (forall r. (Dep Int r) => Int -> r) -> Bar -> Char
| 
| This is not valid as an explicit type signature, but presumably the
| proposal implies that we could type bar as
| 
|   bar :: (Int -> Bool) -> Bar -> Char
| 
| instead. Now
| 
|   \x -> bar' (const x) (Bar 0) :: Bool -> Char
| 
| would become an unsafe coercion function from Bool to Char.
| 
| 
| Thomas
| 
| On 8/11/05, Simon Peyton-Jones <simonpj at microsoft.com> wrote:
| > 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?