datatype list (a:t@ype, int) =
  | nil (a, 0)
  | {n:nat} cons (a, n+1) of (a, list (a, n))

fun{a:t@ype} list_length {n:nat} (xs: list (a, n)): int n = 
  case+ xs of
  | nil () => 0
  | cons (_, xs) => 1 + list_length(xs)

fun{a:t@ype} list_append {n1,n2:nat} (xs: list (a, n1), ys: list (a, n2)): list (a, n1+n2) =
  case+ xs of
  | nil () => ys
  | cons (x, xs) => cons(x, list_append(xs, ys))

fun{a,b:t@ype} list_zip {n:nat} (xs: list (a, n), ys: list (b, n)): list ('(a,b), n) =
  case+ (xs, ys) of
  | (nil (), nil ()) => nil ()
  | (cons (x, xs), cons (y, ys)) => cons('(x,y), list_zip(xs, ys))

implement main() = let
  val a = cons(1, cons(2, cons(3, cons(4, nil))))
  val b = cons(5, cons(6, cons(7, cons(8, nil))))
  val lena = list_length(a)
  val lenb = list_length(b)
  val () = printf("length a: %d\n", @(lena))
  val () = printf("length b: %d\n", @(lenb))
  val c = list_append(a, b)
  val lenc = list_length(c)
  val () = printf("length c: %d\n", @(lenc))
//  val d = list_zip(a, c) // <== different lengths!
  val d = list_zip(a, b) // <== different lengths!
  val lend = list_length(d)
  val () = printf("length d: %d\n", @(lend))

in
  ()
end