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@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?