Fundep/Existential Types in 5.03

[Ashley Yakeley]

At 2002-04-08 04:14, Simon Peyton-Jones wrote:

>I don't know how to make existentials "know" about functional
>dependencies.

Existentials are not the only things that don't "know" about functional 
dependencies. This for instance does not compile:

  class C a b | a -> b

  g :: (C a b,C a b') => b -> b'
  g x = x

I submit that it should, even if it's bad style to write the type of 'g' 
like that.

This may seem a pointless case, given that one can easily rewrite the 
type to tell GHC what it can't figure out for itself (that b and b' are 
the same), but I suspect that it's the same principle as the existential 
datatype case below, where there doesn't appear to be a workaround.

>  In the type system that GHC implements, your
>example fails, and I don't see any meaningful way to make it
>succeed.  But maybe someone else does.

Does anyone even know of a workaround? Given this, find an implementation 
of 'f' that retrieves the contents of its 'D' argument:

  class C a b | a -> b

  data D a = forall b. (C a b) => MkD b

  f :: (C a b) => D a -> b
  -- f (MkD b) = b    won't compile

It's very annoying if it can't be done.

-- 
Ashley Yakeley, Seattle WA