feat(tactic/lint): add universe linter (#8685)

* The linter checks that there are no bad `max u v` occurrences in declarations (bad means that neither `u` nor `v` occur by themselves). See documentation for more details.
* `meta/expr` now imports `meta/rb_map` (but this doesn't give any new transitive imports, so it barely matters). I also removed a transitive import from `meta/rb_map`.



Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>

Author: fpvandoorn

src/meta/expr.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek, Robert Y. Lewis, Floris van Doorn
 -/
 import data.string.defs
-import data.option.defs
+import meta.rb_map
 import tactic.derive_inhabited
 /-!
 # Additional operations on expr and related types
@@ -247,6 +247,17 @@ meta def fold_mvar {α} : level → (name → α → α) → α → α
 | (max a b) f := fold_mvar a f ∘ fold_mvar b f
 | (imax a b) f := fold_mvar a f ∘ fold_mvar b f
 
+/--
+`l.params` is the set of parameters occuring in `l`.
+For example if `l = max 1 (max (u+1) (max v w))` then `l.params = {u, v, w}`.
+-/
+protected meta def params (u : level) : name_set :=
+u.fold mk_name_set $ λ v l,
+  match v with
+  | (param nm) := l.insert nm
+  | _ := l
+  end
+
 end level
 
 /-! ### Declarations about `binder` -/
@@ -882,6 +893,21 @@ protected meta def apply_replacement_fun (f : name → name) (test : expr → bo
   | _ := none
   end
 
+open native
+/--
+  `univ_params_grouped e` computes for each `level` `u` of `e` the parameters that occur in `u`,
+  and returns the corresponding set of lists of parameters.
+  In pseudo-mathematical form, this returns `{ { p : parameter | p ∈ u } | (u : level) ∈ e }`
+  We use `list name` instead of `name_set`, since `name_set` does not have an order.
+-/
+meta def univ_params_grouped (e : expr) : rb_set (list name) :=
+e.fold mk_rb_set $ λ e n l,
+  match e with
+  | e@(sort u) := l.insert u.params.to_list
+  | e@(const nm us) := l.union $ rb_set.of_list $ us.map $ λ u : level, u.params.to_list
+  | _ := l
+  end
+
 end expr
 
 /-! ### Declarations about `environment` -/

src/meta/rb_map.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
 -/
-import data.option.defs
 import data.list.defs
 
 /-!

src/model_theory/basic.lean

@@ -43,6 +43,7 @@ namespace first_order
 
 /-- A first-order language consists of a type of functions of every natural-number arity and a
   type of relations of every natural-number arity. -/
+@[nolint check_univs] -- false positive
 structure language :=
 (functions : ℕ → Type u) (relations : ℕ → Type v)
 

src/tactic/lint/default.lean

@@ -50,6 +50,7 @@ The following linters are run by default:
 18. `has_coe_to_fun` checks that every type that coerces to a function has a direct
     `has_coe_to_fun` instance.
 19. `check_type` checks that the statement of a declaration is well-typed.
+20. `check_univs` checks that that there are no bad `max u v` universe levels.
 
 Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
 This is not run by default.

src/tactic/lint/misc.lean

@@ -16,6 +16,7 @@ This file defines several small linters:
   - `doc_blame_thm` checks that every theorem has a documentation string (not enabled by default).
   - `def_lemma` checks that a declaration is a lemma iff its type is a proposition.
   - `check_type` checks that the statement of a declaration is well-typed.
+  - `check_univs` checks that that there are no bad `max u v` universe levels.
 -/
 
 open tactic expr
@@ -212,8 +213,6 @@ meta def linter.doc_blame_thm : linter :=
   errors_found := "THEOREMS ARE MISSING DOCUMENTATION STRINGS:",
   is_fast := ff }
 
-
-
 /-!
 ## Linter for correct usage of `lemma`/`def`
 -/
@@ -249,6 +248,10 @@ has been used. -/
 
 attribute [nolint def_lemma] classical.dec classical.dec_pred classical.dec_rel classical.dec_eq
 
+/-!
+## Linter that checks whether declarations are well-typed
+-/
+
 /-- Checks whether the statement of a declaration is well-typed. -/
 meta def check_type (d : declaration) : tactic (option string) :=
 (type_check d.type >> return none) <|> return "The statement doesn't type-check"
@@ -266,3 +269,53 @@ Some definitions in the statement are marked `@[irreducible]`, which means that
 "or `@[semireducible]`. This can especially cause problems with type class inference or " ++
 "`@[simps]`.",
   is_fast := tt }
+
+/-!
+## Linter for universe parameters
+-/
+
+open native
+
+/--
+  The good parameters are the parameters that occur somewhere in the `rb_set` as a singleton or
+  (recursively) with only other good parameters.
+  All other parameters in the `rb_set` are bad.
+-/
+meta def bad_params : rb_set (list name) → list name | l :=
+let good_levels : name_set :=
+  l.fold mk_name_set $ λ us prev, if us.length = 1 then prev.insert us.head else prev in
+if good_levels.empty then
+l.fold [] list.union
+else bad_params $ rb_set.of_list $ l.to_list.map $ λ us, us.filter $ λ nm, !good_levels.contains nm
+
+/--
+Checks whether all universe levels `u` in `d` are "good".
+This means that `u` either occurs in a `level` of `d` by itself, or (recursively)
+with only other good levels.
+When this fails, usually this means that there is a level `max u v`, where neither `u` nor `v`
+occur by themselves in a level. It is ok if *one* of `u` or `v` never occurs alone. For example,
+`(α : Type u) (β : Type (max u v))` is a occasionally useful method of saying that `β` lives in
+a higher universe level than `α`.
+-/
+meta def check_univs (d : declaration) : tactic (option string) := do
+  let l := d.type.univ_params_grouped.union d.value.univ_params_grouped,
+  let bad := bad_params l,
+  if bad.empty then return none else return $ some $ "universes " ++ to_string bad ++
+  " only occur together."
+
+/-- A linter for checking that there are no bad `max u v` universe levels. -/
+@[linter]
+meta def linter.check_univs : linter :=
+{ test := check_univs,
+  auto_decls := tt,
+  no_errors_found :=
+    "All declaratations have good universe levels.",
+  errors_found := "THE STATEMENTS OF THE FOLLOWING DECLARATIONS HAVE BAD UNIVERSE LEVELS. " ++
+"This usually means that there is a `max u v` in the declaration where neither `u` nor `v` " ++
+"occur by themselves. Solution: Find the type (or type bundled with data) that has this " ++
+"universe argument and provide the universe level explicitly. If this happens in an implicit " ++
+"argument of the declaration, a better solution is to move this argument to a `variables` " ++
+"command (where the universe level can be kept implicit).
+Note: if the linter flags an automatically generated declaration `xyz._proof_i`, it means that
+the universe problem is with `xyz` itself (even if the linter doesn't flag `xyz`)",
+  is_fast := tt }

src/topology/category/Profinite/projective.lean

@@ -25,11 +25,12 @@ Let `X` be a profinite set.
 
 noncomputable theory
 
+universe variables u v w
 open category_theory function
 
 namespace Profinite
 
-instance projective_ultrafilter (X : Type*) :
+instance projective_ultrafilter (X : Type u) :
   projective (of $ ultrafilter X) :=
 { factors := λ Y Z f g hg,
   begin
@@ -46,14 +47,14 @@ instance projective_ultrafilter (X : Type*) :
   end }
 
 /-- For any profinite `X`, the natural map `ultrafilter X → X` is a projective presentation. -/
-def projective_presentation (X : Profinite) : projective_presentation X :=
+def projective_presentation (X : Profinite.{u}) : projective_presentation X :=
 { P := of $ ultrafilter X,
   f := ⟨_, continuous_ultrafilter_extend id⟩,
   projective := Profinite.projective_ultrafilter X,
   epi := concrete_category.epi_of_surjective _ $
     λ x, ⟨(pure x : ultrafilter X), congr_fun (ultrafilter_extend_extends (𝟙 X)) x⟩ }
 
-instance : enough_projectives Profinite :=
+instance : enough_projectives Profinite.{u} :=
 { presentation := λ X, ⟨projective_presentation X⟩ }
 
 end Profinite