Dear Oleg,

Is this very different from exposing the GADT equality directly in the
module interface?

module A : sig
  type t (* abstract *)
  val reveals_abstraction : (int, t) eq (* or maybe not *)
  val x : t
end

let Refl = A.reveals_abstraction in A.x + 1

On Fri, Feb 26, 2021 at 5:24 PM Oleg <oleg@okmij.org> wrote:

>
> I wonder if the following behavior involving extensible GADTs is
> intentional. It could be useful -- on the other hand, it breaks the type
> abstraction, smuggling out the type equality that was present in the
> implementation of a module but should not be visible to the clients of
> the module. The example is fully above the board, using no magic. It
> runs on OCaml 4.11.1.
>
> Come to think of it, the example is not surprising: if we can reify
> the type equality as a value, we can certainly smuggle it out. Still
> it leaves an uneasy feeling.
>
> Incidentally, I came across the example when pondering Garrigue and
> Henry's paper submitted to the OCaml 2013 workshop.
> https://ocaml.org/meetings/ocaml/2013/proposals/runtime-types.pdf
>
> The paper mentions that runtime type representations may allow breaking
> type abstractions (p2, near the end of the first column).
> Their paper describes a compiler extension. The present example works
> in OCaml as it is, and doesn't depend on any OCaml internals.
>
> First is the preliminaries. Sorry it is a bit long. It is included to
> make the example self-contained.
>
>   (* Type representation library
>     A minimal version of
>     http://okmij.org/ftp/ML/trep.ml
>   *)
>
>   type _ trep = ..
>
>   type (_,_) eq = Refl : ('a,'a) eq
>
>   (* The initial registry, for common data types *)
>   type _ trep +=
>     | Int    : int trep
>
>   type teq_t = {teq: 'a 'b. 'a trep -> 'b trep -> ('a,'b) eq option}
>
>   let teqref : teq_t ref = ref {teq = fun x y -> None} (* default case *)
>
>   (* extensible function *)
>   let teq : type a b. a trep -> b trep -> (a,b) eq option = fun x y ->
>     (!teqref).teq x y
>
>   (* Registering an extension of teq *)
>   let teq_extend : teq_t -> unit = fun {teq = ext} ->
>     let {teq=teq_old} = !teqref in
>     teqref := {teq = fun x y -> match ext x y with None -> teq_old x y | r
> -> r}
>
>   (* Registering the initial extension *)
>   let () =
>     let teq_init : type a b. a trep -> b trep -> (a,b) eq option = fun x y
> ->
>       match (x,y) with
>       | (Int,Int)       -> Some Refl
>       | _  -> None
>     in teq_extend {teq = teq_init}
>
>
> Now, the main problematic example
>
>   module A : sig
>     type t             (* Here, t is abstract *)
>     type _ trep += AT : t trep
>     val x : t
>    end = struct
>     type t = int        (* Here, t is concrete int *)
>     type _ trep += AT : t trep
>     let x = 1
>
>     let () =
>      let teq : type a b. a trep -> b trep -> (a,b) eq option = fun x y ->
>        match (x,y) with
>        | (AT,AT) -> Some Refl
>        | (AT,Int) -> Some Refl      (* Since t = int, it type checks *)
>        | (Int,AT) -> Some Refl
>        | _ -> None
>     in teq_extend {teq=teq}
>   end
>
>
> And here is the problematic behavior:
>
>   # let _ = A.x + 1
>
>   Line 1, characters 8-11:
>   1 | let _ = A.x + 1
>               ^^^
>   Error: This expression has type A.t but an expression was expected of
> type
>            int
>
> That is the expected behavior: to the user of the module A, the type
> A.t is abstract. The users cannot/should not know how it is actually
> implemented.
>
> But we can still find it out
>
>   # let _ = match teq A.AT Int with | Some Refl -> A.x + 1 | _ -> assert
> false
>   - : int = 2
>
> and bring in the equality that t is an int, and get A.x + 1 to type
> check after all.
>
>
>