type zero = unit and 'a succ = unit * 'a

type (_,_) vec =
  | Vnil  : (_,zero) vec
  | Vcons : 'a * ('a, 'n) vec -> ('a, 'n succ) vec

type _ index =
  | I0 : 'n succ index
  | IS : 'n index -> 'n succ index

type _ is_succ = IsSucc : _ succ is_succ

let index_is_succ : type n. n index -> n is_succ =
  function I0 -> IsSucc | IS _ -> IsSucc

let rec remove : type a n. (a,n succ) vec -> n succ index -> (a,n) vec =
  fun lst j ->
  match j, lst with
  | I0,   Vcons (_, l) -> l
  | IS j, Vcons (a, l) ->
      let IsSucc = index_is_succ j in Vcons (a, remove l j)
;;        

type (_,_) table =
  | Tnil : (_,unit) table
  | Tcons : ('a,'m) vec * ('a, 'sz) table -> ('a, 'm * 'sz) table
;;

type (_, _) lt =
  | Lt0 : (zero, _ * _) lt
  | LtS : ('m, 'sz) lt -> ('m succ, 'n * 'sz) lt

type (_,_,_,_) decr_nth =
  | Nth0 : (zero, 'n succ * 'sz, 'n succ, 'n * 'sz) decr_nth
  | NthS : ('i, 'sz, 'n, 'sza) decr_nth ->
           ('i succ, 'm * 'sz, 'n, 'm * 'sza) decr_nth

let rec decr_lt : type i sz n sz'. (i,sz,n,sz') decr_nth -> (i,sz) lt =
  function
    | Nth0 -> Lt0
    | NthS d -> LtS (decr_lt d)

let rec remove_tbl : type a sz i sz' n.
        (a,sz) table -> (i, sz, n, sz') decr_nth -> n index -> (a,sz') table =
  fun tbl i j ->
    match i, tbl with
    | Nth0, Tcons (v, t) -> Tcons (remove v j, t)
    | NthS d, Tcons (v, t) -> Tcons (v, remove_tbl t d j)
;;


let mkc x v = Vcons (x, v)
let mk1 x = mkc x Vnil
let mk2 x y = mkc x (mk1 y)
let mk3 x y z = mkc x (mk2 y z)
let mk4 x y z t = mkc x (mk3 y z t)

let tbl =
  Tcons (mk3 "X" "Y" "Z",
         Tcons (mk2 "U" "V", Tcons (mk4 "A" "B" "C" "D", Tnil)))

let tst1 = remove_tbl tbl Nth0 I0
let tst2 = remove_tbl tbl Nth0 (IS I0)
let tst3 = remove_tbl tbl Nth0 (IS (IS I0))
let tst4 = remove_tbl tbl (NthS Nth0) I0
let tst5 = remove_tbl tbl (NthS (NthS Nth0)) (IS I0)