Regression in nightly: type mismatch (4.25.0-nightly-2025-10-10)

Prerequisites

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

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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

I'm getting some strange errors in Nightly.

Steps to Reproduce

#version -- Lean 4.25.0-nightly-2025-10-10

/-- Similar to `List.ofFnM`, but returns a dependent function rather than `List`. -/
def dfun_ofFnM.{u, v}
    {m : Type u → Type v} [Monad m]
    {n : Nat}
    {α : Fin n → Type u}
    (f : (i : Fin n) → m (α i)) :
    m ((i : Fin n) → α i) :=
  sorry

def compute (n : Nat) (v : Vector Nat n) : Except String Bool := do
  let l : List (String × Nat) := sorry
  let hv /- : (i : Fin n) → PLift (v[i] = v[i]) -/ ← dfun_ofFnM fun (i : Fin n) =>
    have : n = l.length := sorry
    let h : v[i] = v[i] := rfl
    .ok (PLift.up h)
  let hv' : ∀ (i : Nat) (hi : i < n), v[i] = v[i] :=
    fun i hi => (hv ⟨i, hi⟩).down -- ERROR
/-
Type mismatch
  (hv ⟨i, hi⟩).down
has type
  ?m.83 ⟨i, hi⟩
but is expected to have type
  v[i] = v[i]
-/
  .ok true

Expected behavior: No error, as in 4.24.0-rc1.

Actual behavior: Error, with a lot of strangeness:

• Uncommenting the type annotation eliminates the error.
• Deleting have : n = l.length := sorry (which is unused) eliminates the error.
• Changing l from a local variable to a parameter eliminates the error.

Also, I'm getting a warning "declaration uses 'sorry'" at a strange location -- it's for the first "v[i]" on the line let h : v[i] = v[i].

Versions

Lean 4.25.0-nightly-2025-10-10

Impact

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

Start by running the self-contained reproducer from the issue against Lean 4.25.0-nightly-2025-10-10 and 4.24.0-rc1, focusing on dfun_ofFnM and compute. Done means the nightly version accepts the example without the type mismatch or misplaced sorry warning, while preserving the reported behavior.