(kernel) declaration has free variables error when using auto implicits, variables, and quotation pre-resolution

[westluke]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

I discovered this issue while trying to eliminate unnecessary Mathlib imports in my project. The MRE is shown below. 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 to make isAssociative actually defined, 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

I also posted about this bug on the Zulip channel here.

Steps to Reproduce

1. In a fresh project, replace the contents of Main.lean with the MRE code.
2. Run lake build, or just start the Lean 4 VS Code extension.

Expected behavior: The file compiles cleanly, no errors visible in VS Code

Actual behavior: isAtom gets a red underline with the error (kernel) declaration has free variables 'isAtom'.

Reproduces how often: 100%

Versions

Lean (version 4.0.0-nightly-2023-05-18, commit df49512, Release)
OS: Pop!_OS 22.04 LTS

[Kha]

Line 1 now produces an error