# Problems with scoped type variables and existential data constructors

**Simon Peyton-Jones
**
simonpj@microsoft.com

*Tue, 21 Aug 2001 07:05:59 -0700*

The first is a bug, thank you very much. Fixed in the upcoming release.
The second is not a bug: see inline comments below.
Simon
|* -----Original Message-----
*|* From: Dylan Thurston [mailto:dpt@math.harvard.edu]=20
*|* Sent: 21 August 2001 06:17
*|* To: glasgow-haskell-users@haskell.org
*|* Subject: Problems with scoped type variables and existential=20
*|* data constructors
*|*=20
*|*=20
*|* I've been getting some slightly strange behaviour from ghc=20
*|* 5.00.2 using existential data constructors, and I wonder if=20
*|* it's correct.
*|*=20
*|* The first is that I can't seem to use scoped type variables=20
*|* when matching against an existential data constructor. That is,
*|*=20
*|* > data Exist =3D forall a. Exist a
*|* >=20
*|* > bottom (Exist (_ :: t)) =3D Exist (undefined :: t)
*|*=20
*|* gives me the error
*|*=20
*|* 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)) =3D Exist (undefined :: t)
*|*=20
*|* I can work around this, as follows:
*|*=20
*|* > bottom' (Exist x) =3D case x of {(_::t) -> Exist (undefined :: t)}
*|*=20
*|* but it is annoying.
*|*=20
*|*=20
*|* The second case may have to do with context reduction. Consider
*|*=20
*|* > class Silly a b
*|* >=20
*|* > data Exist a =3D forall t. Silly a t =3D> Exist t
*|* >=20
*|* > data Id x =3D Id x
*|* > instance (Silly a b) =3D> Silly a (Id b)
*|* >=20
*|* > applyId (Exist x) =3D Exist (Id x)
*|*=20
*|* This gives me
*|*=20
*|* /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)
*
The trouble is that=20
Exist :: forall a, t. Silly a t =3D> Exist t
Now this is an ambigous type, (which GHC doesn't current report,
something
I will fix), unless there's a functional dependency from t->a.
So the two calls to Exist in the LHS and RHS have different 'a's, and
that's
why you can't discharge one with theother.
Simon