vector ocaml dependent vector

vector.ml

type zero = unit * unit
type 'a minus1 = 'snd constraint 'a = unit * 'snd
type 'a plus1 = unit * 'a

type _ lst =
    | [] : zero lst
    | ( :: ) : int * 'b lst -> ('b lst) plus1 lst

let cons n lst = n :: lst

let hd = function
    | h :: _ -> h

let tl = function
    | _ :: t -> t

let l0 = []
let l1 = 1 :: l0
let l2 = 2 :: l1

let l1' = tl l2
let l0' = tl l1
let _ = tl l0' (* error *)