Overlapping instances in existentials

[Ed Komp]

Simon,

Thanks for the extended response to my question about
overlapping instances.
Before my original posting, I had read a posting that included
the example with Show that you included in your response.

I believed (and still do) that my specific case is a bit different.

> | To determine (SubType y Value) which is just:
> |               (SubType y (Either Double BaseType))
> | 
> | it seems to me that GHC should (has to?) use
> |    instance (SubType a b) => SubType a (Either x b)
> | 
> | I do not see how the other alternative is applicable:
> |       instance SubType a (Either a x)
> 
> Well, the "target" (Subtype y (Either Double BaseType))
> can match against *both* of these instances.
> 
> It can match
>     instance (SubType a b) => SubType a (Either x b)
> 
> by taking a=y, x=Double, b=BaseType
> 
> *If y were instantiated to Double* it could match the second instance
> declaration too.  Now, you say, y is an existential type variable, so it
> can't be instantiated to Double --- but that's tricky to pin down.
> 

Within the GHC compiler
 > can't be instantiated to Double --- but that's tricky to pin down.

this may be tricky to pin down.
But, there is specific information in my example to exclude Double:
I had carefully constructed the type definitions to avoid
ambiguity.

  > | 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.

Am I correct when I say that:
this specific case is not ambiguous,
but the compiler does not recognize the constraint on 'x'
which dis-ambiguates this case.
OR
is this _really_ ambiguous.

I am not suggesting a change in the compiler to recognize
such specific cases (though I would not object :-);
but I want to be sure I understand what I have written.

thanks
Ed Komp