[Haskell-cafe] More mystery with existentials and fundeps

[Matthew Sackman]

Hi,

> {-# OPTIONS_GHC -fglasgow-exts #-}
>
> class F a b | b -> a where
>
> data G :: * -> * where
>           GC :: (F a b) => a -> G b
>
> foo :: (F a b) => G b -> a
> foo g = case g of
>           (GC a) -> a

I may be being dumb, but I think this should work. Any value of G
using the GC constructor will be able to define a from G b given F a b
due to the functional dependency.

In the above 'case' statement version I get:
    Couldn't match expected type `a' (a rigid variable)
           against inferred type `a1' (a rigid variable)
      `a' is bound by the type signature for `foo' at Test.lhs:10:11
      `a1' is bound by the pattern for `GC' at Test.lhs:12:12-15
    In the expression: a
    In a case alternative: (GC a) -> a
    In the expression: case g of (GC a) -> a

> foo2 :: (F a b) => G b -> a
> foo2 g = let (GC a) = g in a

And this 'let' statement version explodes with:
    My brain just exploded.
    I can't handle pattern bindings for existentially-quantified constructors.
    In the binding group for
        (GC a)
    In a pattern binding: (GC a) = g
    In the expression: let (GC a) = g in a
    In the definition of `foo2': foo2 g = let (GC a) = g in a

So is this a missing feature of GHC or am I (more likely) utterly
mistaken about what should be possible here?

Many thanks,

Matthew