I've been getting some slightly strange behaviour from ghc 5.00.2 using existential data constructors, and I wonder if it's correct. The first is that I can't seem to use scoped type variables when matching against an existential data constructor. That is,
data Exist = forall a. Exist a
bottom (Exist (_ :: t)) = Exist (undefined :: t)
gives me the error Inferred type is less polymorphic than expected Quantified type variable `a' is unified with `t' When checking a pattern that binds In an equation for function `bottom': bottom (Exist (_ :: t)) = Exist (undefined :: t) I can work around this, as follows:
bottom' (Exist x) = case x of {(_::t) -> Exist (undefined :: t)}
but it is annoying. The second case may have to do with context reduction. Consider
class Silly a b
data Exist a = forall t. Silly a t => Exist t
data Id x = Id x instance (Silly a b) => Silly a (Id b)
applyId (Exist x) = Exist (Id x)
This gives me /tmp/t.hs:8: Could not deduce `Silly a1 t' from the context (Silly a t) Probable fix: Add `Silly a1 t' to the the existential context of a data constructor arising from use of `Exist' at /tmp/t.hs:8 in the definition of function `applyId': Exist (Id x) although the instance declaration does guarantee the program is type correct. I can fix this by adding a functional dependency:
class Silly a b | b -> a
but this is again annoying. Am I expecting too much from the type checker? Thanks, Dylan Thurston