Infinite loop with recursive list

[Stevendeo]

Alt-ergo seems to enter an infinite loop on the following example:

type 'a t = Cons of {elt : 'a; tail : 'a t} | Nil

function length (list : 'a t) : int =
  match list with
  | Nil -> 0
  | Cons(_, l') -> length(l') + 1
end

logic l : int t

goal g: length(l) <= 4