[Haskell-cafe] Functional dependencies and type inference
Thomas Jäger
thjaeger at gmail.com
Mon Aug 22 21:01:51 EDT 2005
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?
More information about the Haskell-Cafe
mailing list