type _ expr =
     | Int : int -> int expr
     | Add : (int -> int -> int) expr
     | App : ('a -> 'b) expr * 'a expr -> 'b expr

let rec eval : type a. a expr -> a = function
  | Int n -> n
  | Add -> (+)
  | App (f, x) -> eval f (eval x)

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

let cast : type a b. (a, b) eq -> a -> b =
  function Refl -> fun x -> x

let cast_fst : type a b. (a * b, int * bool) eq -> a -> int =
  function Refl -> fun x -> x

type zero = Zero
type 'a succ = Succ of 'a
type (_,_) vec =
    Nil : (_, zero) vec
  | Cons : 'a * ('a,'n) vec -> ('a, 'n succ) vec

let rec map : type a b n. (a -> b) -> (a,n) vec -> (b,n) vec =
  fun f -> function
    | Nil -> Nil
    | Cons (a, l) -> Cons (f a, map f l)

let head : type a n. (a,n succ) vec -> a =
  function Cons (a, _) -> a

let cast_len : type a b n1 n2. ((a, n1) vec, (b, n2) vec) eq -> n1 -> n2 =
  function Refl -> fun x -> x

let succ_inj : type n1 n2. (n1 succ, n2 succ) eq -> (n1, n2) eq =
  fun Refl -> Refl

(* Extra examples *)

type _ ty =
    Tbool : bool ty
  | Tint : int ty
  | Tpair : 'a ty * 'b ty -> ('a * 'b) ty
  | Tarrow : 'a ty * 'b ty -> ('a -> 'b) ty

type dyn = Dyn : 'a ty * 'a -> dyn

let rec sum (Dyn (a, x)) : int =
  match a with
  | Tbool -> if x then 1 else 0
  | Tint -> x
  | Tpair (t1, t2) -> sum (Dyn (t1, fst x)) + sum (Dyn (t2, snd x))
  | Tarrow (t1, t2) -> 0

type _ hlist =
  | HNil : zero hlist
  | HCons : 'a * 'b hlist -> ('a * 'b) hlist