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