Local notation leads to hidden sorry

Stream: general

[Niels Voss]

In the following code

set_option autoImplicit false

variable (n : Nat)

local notation "m" => n

variable (a₁ : Fin n)
def test₁ : Fin m := a₁
#print axioms test₁ -- does not depend on any axioms

variable (a₂ : Fin m)
def test₂ : Fin m := a₂
#print axioms test₂ -- depends on axioms [sorryAx]

The only difference between test₁ and test₂ is that test₂ uses a variable declared with local notation, yet test₂ depends on sorryAx. Am I using local notation incorrectly?

In tactic mode, it shows a₂ : Fin (sorryAx Nat true).

[Kyle Miller]

It looks like it's this issue

[Niels Voss]

I have a longer example where it leads to an infinite loop in the typechecker. Would that be caused by the same bug?

[Niels Voss]

import Mathlib

set_option autoImplicit false
set_option maxHeartbeats 0

open scoped BigOperators

variable {n : ℕ} {m : ℕ} (v : Fin m → EuclideanSpace ℝ (Fin n))

noncomputable def g : ℕ := Fintype.card ((Finset.univ.toList.argmax (‖∑ i in ·, v i‖)).toFinset)
local notation "h" => g v

variable (a₁ : Fin (g v))
def test₁ : Fin h := a₁ -- Works fine

variable (a₂ : Fin h)
def test₂ : Fin h := a₂ -- Infinite loop