# Problems with scoped type variables and existential data constructors

**Dylan Thurston
**
dpt@math.harvard.edu

*Tue, 21 Aug 2001 01:17:13 -0400*

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