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

[Alain Frisch <alain@frisch.fr>]

On 04/28/2013 02:02 AM, Jacques Garrigue wrote:
> The fix is simple enough: we should track injectivity, and assume that abstract
> types are not injective by default.
> However, this also means that the first type I defined above (using Hashtbl.t)
> will be refused.
>
> How many of you are using GADTs in this way, and how dependent are you on
> abstract types ?

FWIW, it turns out that we have very recently introduced such a case 
(and I realized it while synchronizing our version of OCaml with the trunk).

We used to have a functor with this signature:

module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
     sig
       module type S = sig
         type s
         type t
         val t: t ttype
         val eq: (s, t T.t) TypEq.t
       end
       val check: 'a ttype -> (module S with type s = 'a) option
     end

ttype is our type representing type structures at runtime.  The functors 
returns a function that checks if a given runtime type represents an 
instance of an unary abstract type constructor passed in argument to the 
functor (the functors check that this is indeed an abstract type).   In 
case of success, the function returns the ttype of the type constructor 
argument.  The existential is encoded with a first-class module and the 
type-equality is encoded in the classical way (('a, 'b) TypEq.t 
witnesses the equality of 'a and 'b:  type (_, _) t = Eq: ('a, 'a) t).

A GADT was recently introduced to replace this with a more direct 
representation:

module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
     sig
       type _ is_t = Is: 'a ttype -> 'a T.t is_t
       val check: 'a ttype -> 'a is_t option
     end

The problem is that this doesn't work any more (because T.t is not 
injective).

For now, I think I'll use:


module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) :
     sig
       type _ is_t = Is: 'b ttype * ('a, 'b T.t) TypEq.t -> 'a is_t
       val is_t: 'a ttype -> 'a is_t option
     end


which is accepted and roughly equivalent (by opening the equality 
witness, one can retrieve the static equality 'a == 'b T.t).


Alain