leanprover
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:
- [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
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
lfrom 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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.
This seems to be related to the fact that #10319 adds a new get-elem tactic that relies on omega. I modified the example, forcing the usage of omega in the v[i] expressions:
-- Latest Mathlib
/--
info: Lean 4.24.0-rc1
Target: x86_64-unknown-linux-gnu
-/
#guard_msgs in
#version
/-- 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]'(by omega) = v[i]'(by omega) := 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]Lean 4
-/
.ok true
This example, using omega, even fails on Latest Mathlib (see version above) and Mathlib stable (4.23). I don't understand why omega is causing problems here, but I see as much: The proof term hidden in v[i] that is generated by omega for some reason uses this : n = l.length. Without this, omega finds a different proof not relying on this. This reliance on this seems to be somehow problematic.
In fact, get_elem_tactic using omega isn't new, as can be seen in Init.Tactics -- but it seems that you previously had luck that the tactic succeeded with simp +arith; done before trying omega. On the new nightly, this is no longer true because I added a new extension to get_elem_tactic that is tried before simp +arith. (Not sure what do do about this bug yet!)
Update: Another interesting observation: Using let instead of have eliminates the error, too.
Hi @datokrat, thank you for investigating, indeed if I change let h : v[i] = v[i] := rfl to let h : v[i]'(by simp) = v[i]'(by simp) := rfl it works in Nightly.
Do you think I should make this change in my code, or is there hope that the next release won't have this issue?
It's not clear to me whether there anything here that can be fixed -- the error message was definitely unhelpful for me, and the fragility with the error appearing and disappearing with seemingly unrelated changes (including your let/have observation) seems bizarre to me, but I'm not sure if that's something that can/should be fixed or just an unfortunate consequence of the complexity of the type checker.
I agree that the error message is not helpful, @tom93. Regarding whether or how this will be fixed, I can't say yet. I would suggest that you change have : n = l.length into let : n = l.length. This workaround seems less weird.
Here's a further minimized example:
-- Mathlib stable
/--
info: Lean 4.23.0
Target: x86_64-unknown-linux-gnu
-/
#guard_msgs in
#version
def f {α : Type} (f : α) : Unit := sorry
def t1 : Nat := 0
def t2 (_ : True) : Nat := 0
-- works
example : Unit :=
f (have : True := trivial; PLift.up (rfl : t1 = 0))
-- fails
example : Unit :=
f (let : True := trivial; PLift.up (rfl : t2 this = 0))
-- fails
example : Unit :=
f (have : True := trivial; PLift.up (rfl : t2 this = 0))
I believe that in the last example, Lean infers that the α parameter is PLift.up (t2 this = 0), i.e. it tries to write something like f (α := PLift.up (t2 this = 0)) (have : True := sorry; PLift.up (rfl : t2 this = 0)). Note that the α parameter depends on this, but this is only available inside the have expression of the explicit parameter! If you use let instead of have, Lean seems to be smart enough to unfold this to trivial, but it doesn't seem to do this for variables declared using have.
I think I also stumbled upon a similar problem before, but I was never able to minimize it as nicely, so thanks for this bug report! But at this point, I need to defer to others in the team that know more about the elaboration of let and have than I do.
/cc @kmill - you might be interested in this let/have difference (I didn't take a look further than Paul)
