Re: [Caml-list] GADTs : a type variable cannot be deduced

[Gabriel Scherer <gabriel.scherer@gmail.com>]

The equality we're talking about the following: two types are equal if
they are exactly exchangeable from the type-checking point of view.

From this point of view, (int t) and (bool t) may be equal or
different depending on how (t) is defined.

Consider:
  type 'a u = int
in this case (int u) and (bool u) are equal (to int), but consider an
algebraic datatype (sum or record)
  type 'a t = Foo of bool
in this case (int t) and (bool t) are considered distinct by the type-checker,
even if 'a does not actually appear in the definition of the algebraic
datatype. To wit:

  # type 'a t = Foo of bool;;
  type 'a t = Foo of bool
  # let (x : int t) = Foo true;;
  val x : int t = Foo true
  # let (y : bool t) = Foo false;;
  val y : bool t = Foo false
  # [x; y];;
  Error: This expression has type bool t but an expression
         was expected of type int t
         Type bool is not compatible with type int

So "new" types like variants or records are always injective in all
their parameters, but type synonyms may not be.

(Note: the notion of "equality" we're talking about is distinct from,
and stricter than, the symmetric closure of OCaml's subtyping
relation: here we have (int t ≤ bool t) and conversely)

Now if you have

module Foo : sig
  type 'a t
end = struct
 ...
end

You cannot know (without looking at the implementation) if the
abstract declaration of ('a t) here is more like the (type 'a u = int)
example, or the (type 'a t = Foo of bool) example. So OCaml must
conservatively assume that ('a t) may fail to be injective.

Then consider the definition

  type _ nat = Succ : 'a nat -> ('a succ nat)

OCaml will accept this definition if it can prove that, for any type
foo, if (Succ blah : foo succ nat) holds for any OCaml type (foo),
then (blah : foo) also holds. (Because this implication will then be
used to type-check code that pattern-matches on this type.) This
implication is only true if ('a succ) is injective. Hence, the
definition is rejected when ('a succ) is defined as ('a u) above, or
abstract.

On Tue, Oct 29, 2013 at 3:17 PM, David RENAULT <renault@labri.fr> wrote:
> Gabriel Scherer wrote:
>> The problem is with the assumed injectivity of the abstract type 'a
>> succ. You should write:
>>
>>   type 'a succ = Succ
>>
>> then everything works out.
>>
>> Injectivity was assumed to hold for types *defined* to be abstract, but
>> does not hold for types *declared* as abstract (That may have been
>> defined concretely as just "int" in their implementation). For
>> consistency, defined-abstract type are no more assumed to be injective,
>> so you should always use a constructor for that (using a constructor
>> makes your type nominal/generative/fresh, which enforces injectivity).
>>
>> Remark: I'll let you work out while it would be problematic to consider
>> a ('a succ succ nat)-matching branch as dead when matching over a ('a
>> succ nat) value, under the definition (type 'a succ = int).
>
> OK, thank you for your answer, I have taken some time to dive into the
> question of injectivity of types, and I believe that there is something
> I am missing. With your help, the following code compiles :
>
> ====================================================================
> type 'a succ = Succ
> type _ nat = NS : 'a nat -> ('a succ) nat
> ====================================================================
>
> If we leave the type abstract, then the type function NS may not be
> injective. But if we give a concrete implementation with a constructor,
> it works out. To me, the concrete implementation is not injective (it
> maps everything on "Succ nat"), but you proclaim that it becomes
> automatically injective. Why does mapping everything onto a new type
> enforce injectivity ?
>
>                 RENAULT David
>