Possible bug with autoImplicit

Stream: lean4

[Luke West]

Hi all, I think I may have found a bug in Lean 4. The MRE is below, using the most recent version of Lean 4. I discovered it while trying to eliminate unnecessary Mathlib imports in my project. When the import providing IsAssociative was eliminated, line 1 did NOT produce an error, because of auto bound implicit arguments. However, the final line errors with the message (kernel) declaration has free variables 'isAtom'. Interestingly, disabling autoImplicit after the variable declaration, but before the declaration of isAtom, will prevent the error, even though neither op nor assc are used in isAtom. Replacing the custom notation with (@Test α) will also prevent the error, as will importing Mathlib.Init.Algebra.Classes or deleting the declaration of assc.

variable {α : Type} {op : α → α → α} {assc : IsAssociative α op}

inductive Test : Type
| atom : α → Test

set_option quotPrecheck false
local notation:max "T" => (@Test α)

-- set_option autoImplicit false

def isAtom (a : T) : Prop := True

[Mac Malone]

I suspect that the problem is that @Test is being hygienically transformed into an unused identifier which is being auto-implicited.

[Luke West]

Huh, I don't really know what that means - why would that transformation happen? And if @Test is the issue, why does commenting out assc fix it? Thanks for taking a look, btw

[Luke West]

Also, do you know what's the usual best procedure for bug reports on Lean 4? I was thinking I'd post here first to make sure it really is a bug, but maybe I should skip right to making a Github issue

[Andrés Goens]

it usually is good to post here (people are more likely to see it here, and the devs are currently overwhelmed and will probably not get to the issue for a while)

[Andrés Goens]

in this case I would probably post it on github now that no one seems to know exactly what's up

[Andrés Goens]

I suspect it's because auto implicit is too greedy to use that variable T. It sounds like it's more an issue with the parser, as your notation should be delaborated before autoimplicit kicks in? Maybe @Sebastian Ullrich can shed some light on this?

[Sebastian Ullrich]

Some very weird interaction between section variables, auto implicits, and quotation preresolution for sure. The three riders of the bugpocalypse.

[Sebastian Ullrich]

Note that after removing assc, the dubious quotPrecheck false isn't necessary anymore