Problems with scoped type variables and existential data constructors

[Simon Peyton-Jones]

| | /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)
|=20
| The trouble is that=20
| 	Exist :: forall a, t.  Silly a t =3D> Exist t
|=20
| Now this is an ambigous type,


Sorry, I was wrong about this.  The type should be

	data Exist a =3D forall t. Silly a t =3D> Exist t

	Exist :: forall a, t. Silly a t =3D> t -> Exist a

So it's not ambiguous; but my other comment was right.  In your example:

| > applyId (Exist x) =3D Exist (Id x)

the LHS pattern discharges the constraint (Silly a1 t), but the RHS
introduces the
constraint (Silly a2 t), and there's no connection between t1 and t2.
Why should there be?  You could give a type signature

	applyId :: Exist a -> Exist a

and that would force them to be the same

S

Simon