Special sauce in List.get?

Stream: lean4

[Heather Macbeth]

I'm puzzled by the following example, which came up while I was trying to minimize another question. I made a function List.bar which as far as I can tell has the same signature as List.get. But an error I get when using List.get is not there for List.bar.

I don't know if the presence of the calc is fundamental here, but when I try to change it to e.g. show, the error goes away. So ping @Gabriel Ebner who's been working on calc lately.

def List.bar (l : List α) (n : Fin l.length) : α := sorry

#check List.bar -- {α : Type u_1} → (l : List α) → Fin (List.length l) → α
#check List.get -- {α : Type u} → (as : List α) → Fin (List.length as) → α

example {w : List Nat} {i2 i1 : Nat} (hi : i1 = i2) (h1 : i2 < w.length) :
    w.bar ⟨i2, h1⟩ ≤ w.bar ⟨i1, Nat.lt_of_le_of_lt (Nat.le_of_eq hi) h1⟩ := by
  calc
    w.bar ⟨i2, h1⟩ ≤ w.bar ⟨i1, _⟩ :=
    by
      subst hi
      apply Nat.le_refl

example {w : List Nat} {i2 i1 : Nat} (hi : i1 = i2) (h1 : i2 < w.length) :
   w.get ⟨i2, h1⟩ ≤ w.get ⟨i1, Nat.lt_of_le_of_lt (Nat.le_of_eq hi) h1⟩ := by
  calc
    w.get ⟨i2, h1⟩ ≤ w.get ⟨i1, _⟩ :=
    by
      subst hi
      apply Nat.le_refl -- "tactic 'apply' failed"

[Kevin Buzzard]

Works for me on...erm...branch port/RingTheory.Subring.Basic

[Heather Macbeth]

@Kevin Buzzard thanks -- you mean you can reproduce it or you can't reproduce it?

[Kevin Buzzard]

Sorry! with version 4.0.0-nightly-2023-01-29, commit 38a0d1e3733e, Release the apply works fine, no error.

[Heather Macbeth]

I see. I'm on nightly-2023-02-03, and there have been recent changes to calc which this nightly brings in.

[Heather Macbeth]

(This was encountered while I was doing the bump PR !4#1999)

[Gabriel Ebner]

lean4#2095