[Haskell-cafe] Functional dependencies and type inference

[Thomas Jäger]

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?