gsg

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

module EqTag : sig
  type 'a t
  val create : unit -> 'a t
  val equal : 'a t -> 'b t -> ('a, 'b) equality option
end = struct
  type 'a tag = ..;;
  type 'a polymorphic_equality = {
    eq : 'b . ('a tag -> 'b tag -> ('a, 'b) equality option);

gsg

module type ToStr = sig
  type t
  val to_string : t -> string
end

module Str (T:ToStr) = struct
  let stringify t = T.to_string t
end

let to_string (type t) (module M : ToStr with type t = t) (x : t) =

gsg

open Printf

module rec Nil : sig
  type +'a t = 'a
  val app : ('a t, 'a) Type.app
end = struct
  type 'a t = 'a
  let app = Type.Nil
end

gsg

open Printf

module Type = struct
  type _ t =
    | Unit : unit t
    | Bool : bool t
    | Int : int t
    | Sum : 's sum -> 's t

gsg

open Printf

module type T = sig type t end

module type ARGLIST = sig type 'a t end

module Nil = struct type 'a t = 'a end

module Arg (T : T) (Rest : ARGLIST) = struct

gsg

module Type = struct
  type _ t =
    | Bool : bool t
    | Int : int t
    | Float : float t
    | Tuple : (_, 't) agg -> 't t
    | Record : (_, 'r) agg * string array * string -> 'r t
    | Fun : 'a t * 'b t -> ('a -> 'b) t
    | Sum : 's sum -> 's t

gsg

(* Compiles *)
module rec One : sig
  val a : int -> int
end = struct
  let a x = x + (One.a x)
end

(* Compiles *)
module rec Two : sig
  val a : int -> int

gsg

type (_, _) arr =
  | Const : 'a -> (_, 'a) arr
  | Comp  : ('a, 'b) arr * ('b, 'c) arr -> ('a, 'c) arr

let rec eval : type a b . a -> (a, b) arr -> b =
  fun x arr ->
    match arr with
    | Const a -> a
    | Comp (u, v) -> eval (eval x u) v

gsg

module RRef : RREF = struct
  type snap = SNil : snap | SCons : 'a * 'a ref * snap -> snap

  type reflist = RNil : reflist | RCons : 'a ref * reflist -> reflist

  let cell_list = ref RNil

  let rref x =
    let r = ref x in
    cell_list := RCons (r, !cell_list);

gsg

type _ expr =
  | Num : int -> int expr
  | Add : int expr * int expr -> int expr
  | Lt  : int expr * int expr -> bool expr

let rec eval (type a) (expr : a expr) : a =
  match expr with
  | Num n -> n
  | Add (a, b) -> eval a + eval b
  | Lt (a, b) -> eval a < eval b