by? generates sorryAX instead of reporting proof

[mars0i]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

(by? ...) should report the type of the proof generated, but is generating sorryAX instead.

Context

From https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Basic.20confusion.20about.20type.20inference.20in.20exercise/near/473474460

I'm a beginner. In the Zulip thread, @kmill explained how to use rewrite to prove an equality needed for the tail-recursive vector reverse I was trying to define. I wanted to understand what the (by ...) expression was doing, and he suggested using (by? ...) to see by's return type.

(My example probably isn't as minimal as possible, but I don't understand the problem well enough to know how to simplify the example without just randomly changing things. This is the best I can do at this point. Also, this could very well be the same as an existing issue--I can see some that might be the same, for all I know--but I can't tell.)

Steps to Reproduce

inductive Vect (a : Type u) : Nat -> Type u where
   | nil : Vect a 0
   | cons : a -> Vect a n -> Vect a (n + 1)
deriving Repr

def Vect.cast {m n : Nat} (h : m = n) (v : Vect α m) : Vect α n :=
  h ▸ v  

def Vect.revHelper (xs : Vect a n) (acc : Vect a m) : Vect a (m + n) :=
  match xs with
  | .nil => acc
  | .cons y ys => 
     (revHelper ys (.cons y acc)).cast (by? rw [Nat.succ_add]; rfl)

Lean underlines by?, and reports:

lean-nightly.lean:13:40
Tactic state
1 goal
a : Type ?u.1396
n m : Nat
xs : Vect a n
acc : Vect a m
n✝ : Nat
y : a
ys : Vect a n✝
⊢ ?m.1648 = m + (n✝ + 1)
Suggestions

Try this: sorryAx (?_ = m + (n✝ + 1)) true

Messages (2)
lean-nightly.lean:13:40

Try this: sorryAx (?m.1648 = m + (n✝ + 1)) true

lean-nightly.lean:13:48

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?n.succ + ?m
a : Type ?u.1396
n m : Nat
xs : Vect a n
acc : Vect a m
n✝ : Nat
y : a
ys : Vect a n✝
⊢ ?m.1648 = m + (n✝ + 1)

Expected behavior: [Clear and concise description of what you expect to happen]

@kmill said in this Zulip thread that the (by? ...) expression should cause display of the type of the return value of the application of the tactics in the expression. (I haven't figured out how to get more than minimal documentation on by? yet.)

Note that if by? is replaced by by, Vect.revHelper typechecks, and if I assign the result of the by expression to a variable using have or let, I can see the equality proof:

def Vect.revHelper' (xs : Vect a n) (acc : Vect a m) : Vect a (m + n) :=
  match xs with
  | .nil => acc
  | .cons y ys => 
     have prf := (by rw [Nat.succ_add]; rfl)
     (revHelper' ys (.cons y acc)).cast prf

Putting the cursor on the last line shows the type of prf:

prf : m + 1 + n✝ = m + (n✝ + 1)

Actual behavior: [Clear and concise description of what actually happens]

The Infoview window reports with sorryAX, and shows only the rhs of the equality type returned by the tactics. In addition, there's an error on the first tactic, even though it worked fine with by.

Versions

Lean (version 4.13.0-rc3, x86_64-apple-darwin22.6.0, commit 01d414ac36dc, Release)

MacOS 14.7

Additional Information

Nothing.

Impact

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