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@gmail.com] | Sent: 23 August 2005 02:02 | To: Simon Peyton-Jones | Cc: Einar Karttunen; haskell-cafe@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 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?