Overlapping instances in existentials

[oleg@pobox.com]

Ed Komp replied to Simon Peyton-Jones:
> 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.

Indeed, the open world assumption makes it rather difficult to define
a constraint that two type variables must denote different types. I
wish it were possible to easily write
	forall a b. (NotEq a b) => ...

Functional dependencies can be used to achieve a similar effect -- but
sometimes that are not applicable. I wish there were a way to assert
to the compiler that there will be no more instances of a specific
class. The compiler can record this assumption in the object
file. When the compiler builds the final executable and finds an
unexpected instance, the compiler can tell the user that he lied.

 > | class SubType a b where
 > |   inj :: a -> b
 > |   prj :: b -> Maybe a
 > |
 > | instance SubType a (Either a x) where
 > |   inj       =3D Left
 > |   prj       =3D either Just (const Nothing)
 > |
 > | instance (SubType a b) =3D> SubType a (Either x b) where
 > |     inj       =3D Right . inj
 > |     prj       =3D either (const Nothing) prj
 > |
 > | 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


I'm quite dubious that test can be typed at all (see below). Even if
the problem with overlapping instances could be solved. I seem to
remember being on this road before. I'd be great to get GHC to run the
typechecker at run time, to choose the right instance. Alas.

In the example above, the constraint on Foo only guarantees (SubType x
BaseType). When we create MkFoo True, for example, the compiler knows
the type the value being encapsulated, chooses the right instance
(that is, the dictionary), and places the dictionary and the value
into the MkFoo envelope. The function test executes "inj x" whose
return type is different from the BaseType. that is, 'inj' implicitly
has the constraint (SubType x Value). However, MkFoo x only guarantees
(SubType x BaseType). This is not a technicality. Let us disambiguate
the instances and remove all overlapping:

> class SubType a b where
>    inj :: a -> b
>    prj :: b -> Maybe a

> instance SubType Bool (Either Bool x) where
>    inj       = Left
>    prj       = either Just (const Nothing)

> instance SubType Integer (Either Integer x) where
>    inj       = Left
>    prj       = either Just (const Nothing)

> instance (SubType Bool b) => SubType Bool (Either Integer b) where
>      inj       = Right . inj
>      prj       = either (const Nothing) prj

> instance (SubType Bool b) => SubType Bool (Either Double b) where
>      inj       = Right . inj
>      prj       = either (const Nothing) prj

> instance (SubType Integer b) => SubType Integer (Either Double b) where
>      inj       = Right . inj
>      prj       = either (const Nothing) prj

> 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

> test1 :: Foo -> BaseType
> test1 (MkFoo x) = inj x

This code types and even runs:

*> test1 $ MkFoo True
*> Right (Left True)

Indeed, when the compiler sees MkFoo True, it chooses the right instance
of the class (SubType x BaseType), and packs the corresponding
dictionary into MkFoo. When we run test1 $ MkFoo True, the compiler
extracts the dictionary from MkFoo, extracts the field inj from that
dictionary, and runs the corresponding procedure. At this time (at run
time), the compiler does not and cannot choose instances.

If we uncomment the procedure test above, we predictably get the
error:

/tmp/k2.hs:32:
    Could not deduce (SubType x Value)
        from the context (SubType x BaseType)
    Probable fix:
        Add (SubType x Value)
        to the existential context of a data constructor
        Or add an instance declaration for (SubType x Value)
    arising from use of `inj' at /tmp/k2.hs:32
    In the definition of `test': inj x

As we saw above, we cannot widen the constraint at the run time. The
function test wants to use a different function inj -- not the one
associated with (SubType Bool BaseType) -- the chosen instance -- but
a different one, associated with an instance (SubType Bool
Value). However, we cannot chose the instance at that time because the
compiler does not know the exact type of the value in the existential
envelope. To do as you wish, the compiler would have had to compile the
typechhecer into the target executable code. Not that it would be a bad
idea.