data forall a. List (a) where {
  Nil  : List (a)
  Cons : a -> List (a) -> List (a)
};

length : forall c. List (c) -> Int;
length = \list. case list of {
  Nil                 => 0;
  Cons x xs           => 1 + length xs;
  Cons x (Cons y Nil) => 2;
};