Comment author: @garrigue

Interesting. In the case of an abstract type, we add an equation and are done.
The question is whether it is safe to do the same for private abbreviations, i.e. add an equation and forget the original private definition. Intuitively this seems correct, but I need to think a bit more about it.
(A safer way might be to call mcomp on the definitions before adding the abbreviation).

Comment author: @gasche

From the soundness point of view I think there is no problem: it is always sound to forget a type definition, so from type t = private int keep only the abstract type type t, and then to add t = int by using the equation. This way to add equations can always be used as a fall-back when we don't know how to push the equation into the definition.

Comment author: kantian

I tend to be agree with gasche, and we can encode his argumentation with functor.

module M : sig 
  type t = private int
  val eq : (t, int) eq
end = struct
  type t = int
  let eq = Refl
end

module Forget
(T : sig type t end)
(M : sig
  type t = private T.t
  val eq : (t, T.t) eq
end) : sig
  type t
  val eq1 : (t, T.t) eq
  val eq2 : (t, M.t) eq
end = struct
  type t = M.t
  let eq1 = M.eq
  let eq2 = Refl
end

let module N = Forget (struct type t = int end) (M) in
let i = match N.eq1 with Refl -> (1 : N.t) in
match N.eq2 with Refl -> (i : M.t);;
- : M.t = 1

Comment author: @garrigue

My problem is not soundness, but principality:
What do we do when both sides are private abbreviations?
Should we also refine other nominal types (with the same problem)?
It might be ok, but requires a proper argument.
Actually, subtyping seems problematic: when we equate two private abbreviations, choice of the one we keep is going to be relevant.

Comment author: kantian

I'm not sure I understand your questions, since principality problematic is not clear to me.

By the way, currently one can rely on elemantary theory of equality to perform the desired cast. This works in all situations (abstract type, private abbreviations for both types...)

module Eq = struct
  type (_,_) t = Refl : ('a,'a) t
  let sym : type a b. (a,b) t -> (b,a) t = fun Refl -> Refl
  let trans : type a b c. (a,b) t -> (b,c) t -> (a,c) t =
    fun Refl Refl -> Refl
  let cast : type a b. (a,b) t -> a -> b = fun Refl x -> x
end

type ('a,'b) eq = ('a,'b) Eq.t = Refl : ('a,'a) eq

module M : sig
  type t = private int
  val eq : (t, int) eq
end = struct
  type t = int
  let eq = Refl
end

module N : sig
  type t = private M.t
  val eq : (t, M.t) eq
end = struct
  type t = M.t
  let eq = Refl
end

let m1 = Eq.(cast @@ sym M.eq) 1;;
val m1 : M.t = 1

let n1 = Eq.(cast @@ sym N.eq) m1;;
val n1 : N.t = 1

let n1bis = Eq.(cast @@ sym @@ trans N.eq M.eq) 1;;
val n1bis : N.t = 1

I have just a question: what did you mean by this in your first reply?

(A safer way might be to call mcomp on the definitions before adding the abbreviation).

Comment author: @garrigue

Then here is an example of the problem

type (_,_) eq = Refl : ('a, 'a) eq

module M : sig type t = private int  val eq : (t, int) eq end =
  struct type t = int  let eq = Refl end

module N : sig type t = private M.t  val eq : (t, int) eq end =
  struct type t = M.t  let eq = M.eq end

module P : sig type t = private N.t  val eq : (t, M.t) eq end =
  struct type t = N.t  let eq = N.eq end

let f1 (i : P.t) = match P.eq with Refl -> (i :> int);;
let f2 (i : P.t) = match P.eq with Refl -> (i :> N.t);;

There are two option for the match here: either replace P.t = private N.t by P.t = M.t
or replace M.t = private int by M.t = P.t.
In the first case, f1 succeeds but f2 fails, and in the second case f2 succeeds but f1 fails.
The second case is actually even more problematic, as it results in a definitional loop:

 M.t = P.t = private N.t and N.t = private M.t ...

But this doesn't mean that the first option is the correct one: f2 already types currently
by doing nothing, so that the first option is even incomparable with doing nothing.

Comment author: kantian

Ok, I think that I better understand the problem.

Your second case is interresting, it can currently be encoded in OCaml an it leads the type checker in an infinite loop. ;-)

Here is the first option:

module Opt1 = struct
  module rec M' : sig type t = private int end = M
  and N' : sig type t = private M'.t end = N
  and P' : sig type t val eq : (t, M'.t) eq end = P
end

(* f1 succeeds *)
let open Opt1 in
fun x -> match P'.eq with Refl -> (x : P'.t :> int);;
- : Opt1.P'.t -> int = <fun>

(* f2 fails *)
let open Opt1 in
fun x -> match P'.eq with Refl -> (x : P'.t :> N'.t);;
Error: Type P'.t is not a subtype of N'.t

Here your second option:

module Opt2 = struct
  module rec M' : sig type t end = M
  and N' : sig type t = private M'.t end = N
  and P' : sig type t = private N'.t val eq : (t, M'.t) eq end = P
end

(* f2 succeeds *)
let open Opt2 in
fun x -> match P'.eq with Refl -> (x : P'.t :> N'.t);;
- : Opt2.P'.t -> Opt2.N'.t = <fun>

(* with f1 the type checker loops infinitely and never returns 
   I had to kill utop *)
let open Opt2 in
fun x -> match P'.eq with Refl -> (x : P'.t :> int);;
Fatal error: exception UTop_main.Term(-11)

There is even a more agressive solution : forget both private abbreviations, but in this case none of your functions type check.

Now, I'm not really sure there is a safe solution regarding subtyping and principality problematic. Currently, the most safe way could be to rely on general principles of type equality as I did in my previous reply.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

Extra comment: I was too fast in dismissing soundness as a problem here.
When this bug was reported, the way exhaustiveness was handled meant that losing an equation could make a pattern untypable, and break soundness. This is now fixed, but of course the principality problem is still there.

I'm currently working on adding equations for nominal types (#9042), but I think I will have to stick to abstract types, or be very restrictive on the compatibility of the two definitions.

By the way, I don't think this is a bug. An incompleteness, yes, but the specification only says that we add equations to abstract types.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.