fix: get variable? to handle Type* and Sort* (#8908)

Every time `Type*` and `Sort*` elaborate, they generate fresh universe level variables. This was not being accounted for in the computed vs expected check.

Mathlib/Tactic/Variable.lean

@@ -272,20 +272,28 @@ where
         (binders.zip toOmit).filterMap fun (b, omit) => if omit then none else some b
       if let some expectedBinders := expectedBinders? then
         trace[«variable?»] "checking expected binders"
-        /- We re-elaborate the biders to record expressions that represent the whole resulting
-        local contexts (auto-bound implicits make it so we can't just use the argument to the
-        function for `Term.elabBinders`). -/
-        let ctx1 ← Term.withAutoBoundImplicit <| Term.elabBinders binders' fun _ => do
-          mkForallFVars (← getLCtx).getFVars (.sort .zero)
-        let ctx2 ← Term.withAutoBoundImplicit <| Term.elabBinders expectedBinders fun _ => do
-          mkForallFVars (← getLCtx).getFVars (.sort .zero)
-        trace[«variable?»] "new context: {ctx1}"
-        trace[«variable?»] "expected context: {ctx2}"
-        if ← isDefEq ctx1 ctx2 then
-          return (binders', false)
-        else
-          logWarning "Calculated binders do not match the expected binders given after `=>`."
-          return (binders', true)
+        /- We re-elaborate the binders to create an expression that represents the entire resulting
+        local context (auto-bound implicits mean we can't just the `binders` array). -/
+        let elabAndPackageBinders (binders : TSyntaxArray ``bracketedBinder) :
+            TermElabM AbstractMVarsResult :=
+          withoutModifyingStateWithInfoAndMessages <| Term.withAutoBoundImplicit <|
+            Term.elabBinders binders fun _ => do
+              let e ← mkForallFVars (← getLCtx).getFVars (.sort .zero)
+              let res ← abstractMVars e
+              -- Throw in the level names from the current state since `Type*` produces new
+              -- level names.
+              return {res with paramNames := (← get).levelNames.toArray ++ res.paramNames}
+        let ctx1 ← elabAndPackageBinders binders'
+        let ctx2 ← elabAndPackageBinders expectedBinders
+        trace[«variable?»] "new context: paramNames = {ctx1.paramNames}, {
+          ""}numMVars = {ctx1.numMVars}\n{indentD ctx1.expr}"
+        trace[«variable?»] "expected context: paramNames = {ctx2.paramNames}, {
+          ""}numMVars = {ctx2.numMVars}\n{indentD ctx2.expr}"
+        if ctx1.paramNames == ctx2.paramNames && ctx1.numMVars == ctx2.numMVars then
+          if ← isDefEq ctx1.expr ctx2.expr then
+            return (binders', false)
+        logWarning "Calculated binders do not match the expected binders given after `=>`."
+        return (binders', true)
       else
         return (binders', true)
     extendScope binders'
@@ -297,4 +305,5 @@ where
 /-- Hint for the unused variables linter. Copies the one for `variable`. -/
 @[unused_variables_ignore_fn]
 def ignorevariable? : Lean.Linter.IgnoreFunction := fun _ stack _ =>
-  stack.matches [`null, none, `null, `Mathlib.Command.variable?]
+  stack.matches [`null, none, `null, ``Mathlib.Command.Variable.variable?]
+  || stack.matches [`null, none, `null, `null, ``Mathlib.Command.Variable.variable?]

test/Variable.lean

@@ -235,4 +235,30 @@ variable? [UniqueFactorizationDomain R] =>
   [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] [UniqueFactorizationDomain R]
 end
 
+section
+/-!
+Test that unused variables are not reported for the variable list either before or after `=>`.
+-/
+
+/-- info: Try this: variable? {α : _} => {α : _} -/
+#guard_msgs in
+variable? {α : _}
+
+#guard_msgs in
+variable? {α : _} => {α : _}
+end
+
+section
+/-!
+Test that `Sort*` works. This creates new universe level variables, so we need
+to be sure that the state is reset when testing what comes after the `=>`.
+-/
+
+class foo (β : Nat → Sort*) [CoeFun Nat (fun _ ↦ ∀ a : Nat, β a)] where
+
+#guard_msgs in
+variable? {β : Sort*} [i : foo fun _ ↦ β] =>
+  {β : Sort*} [CoeFun Nat fun _ ↦ (a : Nat) → (fun _ ↦ β) a] [i : foo fun _ ↦ β]
+end
+
 end Tests