Problems with scoped type variables and existential data constructors

[Dylan Thurston]

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