datatype list (a:t@ype) =
  | nil (a)
  | cons (a) of (a, list a)

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

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

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

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 lend = list_length(d)
  val () = printf("length d: %d\n", @(lend))

in
  ()
end