test: lint against variable whose type has universe metavariables

[robin-carlier]

In the past, universe metavariables in binders in the variable command have caused performance issues.
They are also at risk of getting involuntarily unified later on.

This PR adds a linter (currently emitting a lot of warnings throughout the library) against variable (foo : Foo) (or variable (foo : Foo) in where the type Foo contains universe MVars.

---

I mostly wanted an excuse to learn a bit more about linters.

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[github-actions]

PR summary e81210da0f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 8239 files with changed transitive imports taking up over 359433 characters: this is too many to display!
You can run this locally from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

---

Declarations diff (regex)

+ Foo
+ containsId
+ pruneUpdate
+ typelessBinder?
+ universeMVarInVariable

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit e81210da0f
Reference commit 9d302fc708

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[robin-carlier]

Currently, the linter breaks on things like

variable {α : Type*} [PartialOrder α] [SuccOrder α]
  (succ : ∀ a, ¬IsMax a → motive (succ a))

because the Command.runTermElabM runs after the elaboration of the variable command, so that at the linter step, succ is elaborated as the variable defined here, and is not well-typed anymore. There is probably a way to avoid this by being a bit hacky (e.g., counting how many things the currently-linted variable command adds to the scope, then dropping them from the scope before running runTermElabM). The other possibility is to decide that such variable commands should be fixed, e.g.

variable [PartialOrder α] [SuccOrder α]
  (succ : ∀ a, ¬IsMax a → motive (Order.succ a))

and leave the linter as is.

In #42591 an LLM got Mathlib lint-free with this linter and that speeds the library by 317G instructions/ .22%, which is nice, but also not as dramatic as what #32842 did, it’s also not clear how costly this linter is if active globally (and it’s also assuming the LLM-generated diff did not secretely monomorphize some declarations).