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