Overlapping instances in existentials

[Dean Herington]

Dylan Thurston wrote:

> On Thu, Jun 19, 2003 at 11:08:35AM -0500, Ed Komp wrote:
> >  > | type BaseType = Either Integer ( Either Bool () )
> >  > |
> >  > | type Value = (Either Double BaseType)
> >  > |
> >  > | data Foo =  forall x. (SubType x BaseType)  => MkFoo x
> >  > |
> >  > | test :: Foo -> Value
> >  > | test (MkFoo x) = inj x
> >
> >
> > '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:
> >
> > 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?

Put another way, only with a "closed world" assumption could the compiler
"know" that NOT  (SubType Double BaseType).  GHC deliberately eschews such an
assumption, so that adding new instances doesn't change the semantics of a
program.

Dean