"failed to generate equational theorem" when matching on not only recursive call

[nomeata]

This could be a duplicate of #3219 or #2962. Still reporting it separately, so when a fix is applied each example can be checked and closed separately, and nothing falls through the cracks.

Here is a minimized version of the issue that's currently biting me:

inductive Expr where
  | const (i : BitVec 32)
  | op (op : Unit) (e1 : Expr)

-- fails:

def optimize : Expr → Expr
  | .const i => .const i
  | .op bop e1 =>
    match bop, optimize e1 with
    | _, .const _ => .op bop (.const 0)
    | _, _ => .const 0

#check optimize.eq_1

-- works:

def optimize2 : Expr → Expr
  | .const i => .const i
  | .op bop e1 =>
    match optimize2 e1 with
    | .const _ => .op bop (.const 0)
    | _ => .const 0

#check optimize2.eq_1

-- also works:

def optimize3 : Expr → Expr
  | .const i => .const i
  | .op bop e1 =>
    match bop, e1 with
    | _, .const _ => .op bop (optimize3 e1)
    | _, _ => .const 0

#check optimize3.eq_1

Note it seems crucial to have a match that matches on both the recursive call, and some other parameter.

Switching to well-founded recursion does not help.

Versions

"4.13.0-rc3"

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.