[Caml-list] Breaking type abstraction of modules

[Oleg <oleg@okmij.org>]

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.