Overlapping Instances + Existentials = Incoherent Instances

[Dan Doel]

On Wednesday 03 February 2010 11:34:27 am Stefan Holdermans wrote:
> I don't think it's the same thing. The whole point of the existential
> is that at the creation site of any value of type Ex the type of the
> value being packaged is hidden. At the use site, therefore, the only
> suitable instance is the one for C a. In particular, there is no way
> for the baz to tell whether an Int is wrapped in the existential.
> 
> However, if we pack a dictionary along, as in
> 
>    data Ex = forall a. C a => Ex a
> 
> then, you'll find that baz will pick the dictionary supplied with the
> existential package rather than the one from the general instance.

This is (I think) exactly the behavior that IncoherentInstances enables, 
though, except for universal quantification. If our function has the type:

  forall a. a -> String

then the only instance that can be picked for the parameter is the C a 
instance, because the function knows nothing about a; a is hidden from the 
function's perspective, rather from a global perspective, but the function is 
the one picking the instance to use, since it isn't given one. If instead we 
pass the dictionary explicitly:

  forall a. C a => a -> String

the function uses that dictionary. In fact, if existentials were first class, 
we could directly write some isomorphic types that show the analogy:

  forall a. a -> String        ~= (exists a. a) -> String
  forall a. C a => a -> String ~= (exists a. C a => a) -> String

The bottom two naturally work, because we're passing the dictionary. On the 
top, the existential version works, but the universal version doesn't, unless 
we enable an extra extension.

As a final data point, one can encode existential types via their universal 
eliminators:

  type Ex' = forall r. (forall a. a -> r) -> r

  hide :: forall a. a -> Ex'
  hide x k = k x

  open :: (forall a. a -> r) -> Ex' -> r
  open f ex = ex f

Now we can try to write the unconstrained function:

  quux :: a -> String
  quux x = open foo (hide x)

But, this gives an error telling us that we need IncoherentInstances.

-- Dan