gsg

type (_, _) t =
  | Default : ('a, 'a) t
  | Given : ('a, 'b) t

let test : type a b . (a, b) t -> (a -> b) -> a -> b =
  fun m f arg ->
    match m with
    | Default -> f arg
    | Given -> f arg

gsg

let min a =
  let index = 0 in
  let elt = a.(0) in
  let rec loop index elt =
    if index >= Array.length a then elt
    else if a.(index) < elt then
      let elt = a.(index) in
      ... in
  if Array.length a = 1 then a.(0)
  else loop index elt

gsg

let min_elt array =
  let rec loop index elt =
    if index >= Array.length array then ...
    else ... in
  if Array.length array = 0 then ...
  else loop 1 array.(0)

gsg

let test arg =
  let rec id x = x
  and g (y : int) = id y
  and h (y : float) = id y in
  g, h

let test2 arg =
  let rec id x = x in
  let g (y : int) = id y in
  let h (y : float) = id y in

gsg

(* Sigh, GADTs are allergic to uninhabited types with params  *)
type nullary = { nullary : 'a . 'a }
type 'a unary = { unary : 'a . 'a }
type ('a, 'b) binary = { binary : 'a . 'a }

type symbol = string

module Env = Map.Make (struct
    type t = symbol

gsg

type _ expr = Int : int -> int expr | Float : float -> float expr

type any_expr = Any : 'a expr -> any_expr

type _ ty = TyInt : int ty | TyFloat : float ty

let rec eval : type a . a expr -> a = function
  | Int i -> i
  | Float f -> f

gsg

type _ expr = Int : int -> int expr | Float : float -> float expr

type any_expr = Any : 'a expr -> any_expr

type _ ty = TyInt : int ty | TyFloat : float ty

let rec eval : type a . a expr -> a = function
  | Int i -> i
  | Float f -> f

gsg

type binop = Add | Sub | Mul | Div
type cmpop = Lt | Gt | LtEq | GtEq | Eq | NotEq

type 'a arith = AInt : int arith | AFloat : float arith
type 'a comparable =
  | CBool : bool comparable
  | Arith : 'a arith -> 'a comparable

type 'a expr =
  | Bool : bool -> bool expr

gsg

type literal
type param

type _ t =
  | QueryString : string -> literal t
  | IntParam : string -> param t
  | StringParam : string -> param t

type query =
  | Nil : query

gsg

open Printf

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 = ..;;