escaped_existential.ml

module N : sig
  type +'a t = private int
  val create : int -> 'a t
end= struct
  type +'a t = int
  let create n = n
end

type nil = private Nil_type

type (_,_) elt =
  | Elt_fine: 'nat N.t ->
    ('l,'nat * 'l) elt
  | Elt: 'nat N.t -> ('l,'nat -> 'l) elt

type _ t =
  | Nil : nil t
  | Cons : ('x, 'fx) elt * 'x t -> 'fx t

(* Does not detect the escaped existential type *)
(* check_wrong: ('a -> $'b -> nil, 'elt) m -> 'a N.t -> $'b N.t -> unit *)
let check_wrong:  ('a -> 'b -> nil) t
  -> 'a N.t -> 'b N.t -> unit = fun sh i j ->
  let Cons(Elt dim, _) = sh in
  ()

(* Does detect the escaped existential type *)
let check_detected:  ('a * 'b * nil) t
  -> 'a N.t -> 'b N.t -> unit = fun sh i j ->
  let Cons(Elt_fine dim, _) = sh in
  ()