Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs

[Leo White <lpw25@cam.ac.uk>]

[Sorry if this is a repeat post]

> But it seems to me that this contradicts the definition of injectivity.
> Namely, if we follow your definition, and have 'a bivar = 'b bivar, then
> clearly bivar is not injective.

I think Gabriel meant that 'a bivar = 'b bivar were equal in the
subtyiping relationship, rather than in the unification
relationship. (Perhaps we should use a different symbol for subtyping
equality).

> So there are two solutions: either we do not allow a bi-variant type
> to be injective (breaking our simple statement that concrete types
> are injective in all their parameters), or we consider bi-variance +
> injectivity is some intermediary state, where we can use both directions
> of subtyping, but not strong (unification) equality.

I don't see how this implies the need for the strengthening you
describe. As I see it:

  type 'a t = T

creates a type that is bi-variant in its parameter, so all occurences of
'a in:

  type 'a u = 'a t -> 'a t

are in bi-variant positions, so u should also be bi-variant.

> The practical reason is to make easier to define indices.
> If we keep the bi-variance in an invariant context, then the following
> type definition is refused:
>
> 	type 'a t = T;;
> 	type _ g = G : 'a -> 'a t g;;
>
> In 4.00, this definition is refused because 'a in 'a t g is bi-variant, but 'a appears
> in a covariant position.

I don't see why this could not be allowed without the restriction you
propose. I thought that this was rejected in 4.00 because 4.00 used
bi-variance as an (unsafe) approximation of non-injective. Since we now
track injectivity separately from variance g be accepted (with 'a covariant).