Recursive definition fails

Stream: lean4

[Raghuram]

Why does the first definition of trans below fail, but the second succeed?

inductive TransClosure (r : α → α → Prop) : α → α → Prop
| extends : r a b → TransClosure r a b
| trans_left : r a b → TransClosure r b c → TransClosure r a c

def trans' {a b c} : TransClosure r a b → TransClosure r b c → TransClosure r a c
| .extends h₁       => .trans_left h₁
| .trans_left h₁ h₂ => .trans_left h₁ ∘ trans' h₂

def trans {a b c} : TransClosure r a b → TransClosure r b c → TransClosure r a c := by
  intro h₁; induction h₁
  case «extends» h₁       => exact .trans_left h₁
  case trans_left h₁ _ hᵢ => exact .trans_left h₁ ∘ hᵢ

(#eval Lean.versionString: 4.0.0-nightly-2022-09-29, in case this is a bug.)

[Leonardo de Moura]

Created an issue for it: https://github.com/leanprover/lean4/issues/1672

[Daniel Fabian]

feel free to track the progress on github for more in-depth discussions.