List.append recall

Stream: mathlib4

[Martin Dvořák]

What makes the following code fail please?

import Mathlib

recall List.append {α : Type _} : List α → List α → List α
  | []  , s => s
  | a::l, s => a :: List.append l s

[Markus Himmel]

I don't think recall understands that when you're building the new definition to be checked against the existing one, the List.append in the body is a recursive call.