Overlapping instances in existentials

[Dylan Thurston]

--gBBFr7Ir9EOA20Yy
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable

On Thu, Jun 19, 2003 at 11:08:35AM -0500, Ed Komp wrote:
>  > | type BaseType =3D Either Integer ( Either Bool () )
>  > |
>  > | type Value =3D (Either Double BaseType)
>  > |
>  > | data Foo =3D  forall x. (SubType x BaseType)  =3D> MkFoo x
>  > |
>  > | test :: Foo -> Value
>  > | test (MkFoo x) =3D inj x
>=20
>=20
> 'x' is the variable I am concerned about.
> Since it is an argument to MkFoo,
> we know that (SubType x BaseType)
> and we also know that:
>=20
> NOT  (SubType Double BaseType), so 'x' cannot be instantiated as Double.

I'm missing something.  Why do we know NOT (SubType Double BaseType)?
Nothing in the code above prevents you from having such an instance,
does it?

Peace,
	Dylan

--gBBFr7Ir9EOA20Yy
Content-Type: application/pgp-signature
Content-Disposition: inline

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.2.2 (GNU/Linux)

iD8DBQE+8vWOVeybfhaa3tcRApkJAJ9ZdxnZYLTB3rOcMefbd417YVxRqgCcCHBc
d9szvZjwLjWgTbb1iybmj3w=
=P8Gi
-----END PGP SIGNATURE-----

--gBBFr7Ir9EOA20Yy--