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

[David RENAULT <renault@labri.fr>]

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