Problems with scoped type variables and existential data constructors

[Simon Peyton-Jones]

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