feat(tactic/lint): Three new linters, update illegal_constants (#1947)

* add three new linters

* fix failing declarations

* restrict and rename illegal_constants linter

* update doc

* update ge_or_gt test

* update mk_nolint

* fix error

* Update scripts/mk_nolint.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* Update src/meta/expr.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* clarify unfolds_to_class

* fix names since name is no longer protected

also change one declaration back to instance, since it did not cause a linter failure

* fix errors, move notes to docstrings

* add comments to docstring

* update mk_all.sh

* fix linter errors

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

docs/commands.md

@@ -108,9 +108,13 @@ The following linters are run by default:
 1. `unused_arguments` checks for unused arguments in declarations.
 2. `def_lemma` checks whether a declaration is incorrectly marked as a def/lemma.
 3. `dup_namespce` checks whether a namespace is duplicated in the name of a declaration.
-4. `illegal_constant` checks whether ≥/> is used in the declaration.
+4. `ge_or_gt` checks whether ≥/> is used in the declaration.
 5. `instance_priority` checks that instances that always apply have priority below default.
 6. `doc_blame` checks for missing doc strings on definitions and constants.
+7.  `has_inhabited_instance` checks whether every type has an associated `inhabited` instance.
+8.  `impossible_instance` checks for instances that can never fire.
+9.  `incorrect_type_class_argument` checks for arguments in [square brackets] that are not classes.
+10. `dangerous_instance` checks for instances that generate type-class problems with metavariables.
 
 Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
 This is not run by default.

scripts/mk_all.sh

@@ -39,5 +39,6 @@ cat <<EOT >> lint_mathlib.lean
 
 open nat -- need to do something before running a command
 
-#lint_mathlib- only unused_arguments dup_namespace doc_blame illegal_constants def_lemma instance_priority
+#lint_mathlib- only unused_arguments dup_namespace doc_blame ge_or_gt def_lemma instance_priority
+  impossible_instance incorrect_type_class_argument dangerous_instance
 EOT

scripts/mk_nolint.lean

@@ -25,7 +25,8 @@ open io io.fs
 /-- Defines the list of linters that will be considered. -/
 meta def active_linters :=
 [`linter.unused_arguments, `linter.dup_namespace, `linter.doc_blame,
- `linter.illegal_constants, `linter.def_lemma, `linter.instance_priority]
+ `linter.ge_or_gt, `linter.def_lemma, `linter.instance_priority, --`linter.has_inhabited_instance,
+ `linter.impossible_instance, `linter.incorrect_type_class_argument, `linter.dangerous_instance]
 
 /-- Runs when called with `lean --run` -/
 meta def main : io unit :=

src/algebra/lie_algebra.lean

@@ -255,7 +255,9 @@ structure lie_subalgebra extends submodule R L :=
 instance lie_subalgebra_coe_submodule : has_coe (lie_subalgebra R L) (submodule R L) :=
 ⟨lie_subalgebra.to_submodule⟩
 
-instance lie_subalgebra_lie_algebra [L' : lie_subalgebra R L] : lie_algebra R L' := {
+/-- A Lie subalgebra forms a new Lie algebra.
+This cannot be an instance, since being a Lie subalgebra is (currently) not a class. -/
+def lie_subalgebra_lie_algebra (L' : lie_subalgebra R L) : lie_algebra R L' := {
   bracket  := λ x y, ⟨⁅x.val, y.val⁆, L'.lie_mem x.property y.property⟩,
   lie_add  := by { intros, apply set_coe.ext, apply lie_add, },
   add_lie  := by { intros, apply set_coe.ext, apply add_lie, },

src/category/monad/writer.lean

@@ -148,8 +148,15 @@ export monad_writer_adapter (adapt_writer)
 section
 variables {ω ω' : Type u} {m m' : Type u → Type v}
 
-@[priority 100] -- see Note [lower instance priority]
-instance monad_writer_adapter_trans {n n' : Type u → Type v} [monad_functor m m' n n'] [monad_writer_adapter ω ω' m m'] : monad_writer_adapter ω ω' n n' :=
+/-- Transitivity.
+
+This instance generates the type-class problem bundled_hom ?m (which is why this is marked as
+`[nolint]`). Currently that is not a problem, as there are almost no instances of `bundled_hom`.
+
+see Note [lower instance priority] -/
+@[nolint, priority 100]
+instance monad_writer_adapter_trans {n n' : Type u → Type v} [monad_functor m m' n n']
+  [monad_writer_adapter ω ω' m m'] : monad_writer_adapter ω ω' n n' :=
 ⟨λ α f, monad_map (λ α, (adapt_writer f : m α → m' α))⟩
 
 instance [monad m] : monad_writer_adapter ω ω' (writer_t ω m) (writer_t ω' m) :=

src/category_theory/adjunction/limits.lean

@@ -44,8 +44,7 @@ def functoriality_is_left_adjoint :
     counit := functoriality_counit adj K } }
 
 /-- A left adjoint preserves colimits. -/
-@[priority 100] -- see Note [lower instance priority]
-instance left_adjoint_preserves_colimits : preserves_colimits F :=
+def left_adjoint_preserves_colimits : preserves_colimits F :=
 { preserves_colimits_of_shape := λ J 𝒥,
   { preserves_colimit := λ F,
     by exactI
@@ -57,7 +56,7 @@ omit adj
 
 @[priority 100] -- see Note [lower instance priority]
 instance is_equivalence_preserves_colimits (E : C ⥤ D) [is_equivalence E] : preserves_colimits E :=
-adjunction.left_adjoint_preserves_colimits E.adjunction
+left_adjoint_preserves_colimits E.adjunction
 
 -- verify the preserve_colimits instance works as expected:
 example (E : C ⥤ D) [is_equivalence E]
@@ -100,8 +99,7 @@ def functoriality_is_right_adjoint :
     counit := functoriality_counit' adj K } }
 
 /-- A right adjoint preserves limits. -/
-@[priority 100] -- see Note [lower instance priority]
-instance right_adjoint_preserves_limits : preserves_limits G :=
+def right_adjoint_preserves_limits : preserves_limits G :=
 { preserves_limits_of_shape := λ J 𝒥,
   { preserves_limit := λ K,
     by exactI
@@ -113,7 +111,7 @@ omit adj
 
 @[priority 100] -- see Note [lower instance priority]
 instance is_equivalence_preserves_limits (E : D ⥤ C) [is_equivalence E] : preserves_limits E :=
-adjunction.right_adjoint_preserves_limits E.inv.adjunction
+right_adjoint_preserves_limits E.inv.adjunction
 
 -- verify the preserve_limits instance works as expected:
 example (E : D ⥤ C) [is_equivalence E]

src/category_theory/concrete_category/bundled_hom.lean

@@ -44,8 +44,11 @@ namespace bundled_hom
 variable [𝒞 : bundled_hom hom]
 include 𝒞
 
-/-- Every `@bundled_hom c _` defines a category with objects in `bundled c`. -/
-instance : category (bundled c) :=
+/-- Every `@bundled_hom c _` defines a category with objects in `bundled c`.
+
+This instance generates the type-class problem bundled_hom ?m (which is why this is marked as
+`[nolint]`). Currently that is not a problem, as there are almost no instances of `bundled_hom`. -/
+@[nolint] instance category : category (bundled c) :=
 by refine
 { hom := λ X Y, @hom X.1 Y.1 X.str Y.str,
   id := λ X, @bundled_hom.id c hom 𝒞 X X.str,
@@ -56,8 +59,11 @@ by refine
 intros; apply 𝒞.hom_ext;
   simp only [𝒞.id_to_fun, 𝒞.comp_to_fun, function.left_id, function.right_id]
 
-/-- A category given by `bundled_hom` is a concrete category. -/
-instance concrete_category : concrete_category (bundled c) :=
+/-- A category given by `bundled_hom` is a concrete category.
+
+This instance generates the type-class problem bundled_hom ?m (which is why this is marked as
+`[nolint]`). Currently that is not a problem, as there are almost no instances of `bundled_hom`. -/
+@[nolint] instance : concrete_category (bundled c) :=
 { forget := { obj := λ X, X,
               map := λ X Y f, 𝒞.to_fun X.str Y.str f,
               map_id' := λ X, 𝒞.id_to_fun X.str,

src/data/list/defs.lean

@@ -13,6 +13,11 @@ open function nat
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 
+/-- Returns whether a list is []. Returns a boolean even if `l = []` is not decidable. -/
+def is_nil {α} : list α → bool
+| [] := tt
+| _  := ff
+
 instance [decidable_eq α] : has_sdiff (list α) :=
 ⟨ list.diff ⟩
 
@@ -172,6 +177,16 @@ map_with_index_core f 0 as
      indexes_of a [a, b, a, a] = [0, 2, 3] -/
 def indexes_of [decidable_eq α] (a : α) : list α → list nat := find_indexes (eq a)
 
+/-- Auxilliary definition for `indexes_values`. -/
+def indexes_values_aux {α} (f : α → bool) : list α → ℕ → list (ℕ × α)
+| []      n := []
+| (x::xs) n := let ns := indexes_values_aux xs (n+1) in if f x then (n, x)::ns else ns
+
+/-- Returns `(l.find_indexes f).zip l`, i.e. pairs of `(n, x)` such that `f x = tt` and
+  `l.nth = some x`, in increasing order of first arguments. -/
+def indexes_values {α} (l : list α) (f : α → bool) : list (ℕ × α) :=
+indexes_values_aux f l 0
+
 /-- `countp p l` is the number of elements of `l` that satisfy `p`. -/
 def countp (p : α → Prop) [decidable_pred p] : list α → nat
 | []      := 0

src/meta/expr.lean

@@ -377,22 +377,31 @@ iterating through the expression. In one performance test `pi_binders` was more
 quicker than `mk_local_pis` (when applied to the type of all imported declarations 100x)."
 
 /-- Get the codomain/target of a pi-type.
-  This definition doesn't instantiate bound variables, and therefore produces a term that is open.-/
-meta def pi_codomain : expr → expr -- see note [open expressions]
+  This definition doesn't instantiate bound variables, and therefore produces a term that is open.
+  See note [open expressions]. -/
+meta def pi_codomain : expr → expr
 | (pi n bi d b) := pi_codomain b
 | e             := e
 
-/-- Auxilliary defintion for `pi_binders`. -/
--- see note [open expressions]
+/-- Get the body/value of a lambda-expression.
+  This definition doesn't instantiate bound variables, and therefore produces a term that is open.
+  See note [open expressions]. -/
+meta def lambda_body : expr → expr
+| (lam n bi d b) := lambda_body b
+| e             := e
+
+/-- Auxilliary defintion for `pi_binders`.
+  See note [open expressions]. -/
 meta def pi_binders_aux : list binder → expr → list binder × expr
 | es (pi n bi d b) := pi_binders_aux (⟨n, bi, d⟩::es) b
 | es e             := (es, e)
 
 /-- Get the binders and codomain of a pi-type.
   This definition doesn't instantiate bound variables, and therefore produces a term that is open.
   The.tactic `get_pi_binders` in `tactic.core` does the same, but also instantiates the
-  free variables -/
-meta def pi_binders (e : expr) : list binder × expr := -- see note [open expressions]
+  free variables.
+  See note [open expressions]. -/
+meta def pi_binders (e : expr) : list binder × expr :=
 let (es, e) := pi_binders_aux [] e in (es.reverse, e)
 
 /-- Auxilliary defintion for `get_app_fn_args`. -/
@@ -439,6 +448,15 @@ meta def is_default_local : expr → bool
 | (expr.local_const _ _ binder_info.default _) := tt
 | _ := ff
 
+/-- `has_local_constant e l` checks whether local constant `l` occurs in expression `e` -/
+meta def has_local_constant (e l : expr) : bool :=
+e.has_local_in $ mk_name_set.insert l.local_uniq_name
+
+/-- Turns a local constant into a binder -/
+meta def to_binder : expr → binder
+| (local_const _ nm bi t) := ⟨nm, bi, t⟩
+| _                       := default binder
+
 end expr
 
 /-! ### Declarations about `environment` -/

src/order/filter/filter_product.lean

@@ -189,15 +189,19 @@ instance [comm_ring β] : comm_ring β* :=
 { ..filter_product.ring,
   ..filter_product.comm_semigroup }
 
-instance [zero_ne_one_class β] (NT : φ ≠ ⊥) : zero_ne_one_class β* :=
+/-- If `φ ≠ ⊥` then `0 ≠ 1` in the ultraproduct.
+This cannot be an instance, since it depends on `φ ≠ ⊥`. -/
+protected def zero_ne_one_class [zero_ne_one_class β] (NT : φ ≠ ⊥) : zero_ne_one_class β* :=
 { zero_ne_one := λ c, have c' : _ := quotient.exact' c, by
   { change _ ∈ _ at c',
     simp only [set.set_of_false, zero_ne_one, empty_in_sets_eq_bot] at c',
     exact NT c' },
   ..filter_product.has_zero,
   ..filter_product.has_one }
 
-instance [division_ring β] (U : is_ultrafilter φ) : division_ring β* :=
+/-- If `φ` is an ultrafilter then the ultraproduct is a division ring.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected def division_ring [division_ring β] (U : is_ultrafilter φ) : division_ring β* :=
 { mul_inv_cancel := λ x, quotient.induction_on' x $ λ a hx, quotient.sound' $
     have hx1 : _ := (not_imp_not.mpr quotient.eq'.mpr) hx,
     have hx2 : _ := (ultrafilter_iff_compl_mem_iff_not_mem.mp U _).mpr hx1,
@@ -214,11 +218,16 @@ instance [division_ring β] (U : is_ultrafilter φ) : division_ring β* :=
   ..filter_product.has_inv,
   ..filter_product.zero_ne_one_class U.1 }
 
-instance [field β] (U : is_ultrafilter φ) : field β* :=
+/-- If `φ` is an ultrafilter then the ultraproduct is a field.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected def field [field β] (U : is_ultrafilter φ) : field β* :=
 { ..filter_product.comm_ring,
   ..filter_product.division_ring U }
 
-noncomputable instance [discrete_field β] (U : is_ultrafilter φ) : discrete_field β* :=
+/-- If `φ` is an ultrafilter then the ultraproduct is a discrete field.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected noncomputable def discrete_field [discrete_field β] (U : is_ultrafilter φ) :
+  discrete_field β* :=
 { inv_zero := quotient.sound' $ by show _ ∈ _;
     simp only [inv_zero, eq_self_iff_true, (set.univ_def).symm, univ_sets],
   has_decidable_eq := by apply_instance,
@@ -239,7 +248,9 @@ instance [partial_order β] : partial_order β* :=
     show _ ∈ _, by rw hI; exact inter_sets _ hab hba
   ..filter_product.preorder }
 
-instance [linear_order β] (U : is_ultrafilter φ) : linear_order β* :=
+/-- If `φ` is an ultrafilter then the ultraproduct is a linear order.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected def linear_order [linear_order β] (U : is_ultrafilter φ) : linear_order β* :=
 { le_total := λ x y, quotient.induction_on₂' x y $ λ a b,
     have hS : _ ⊆ {i | b i ≤ a i} := λ i, le_of_not_le,
     or.cases_on (mem_or_compl_mem_of_ultrafilter U {i | a i ≤ b i})
@@ -363,15 +374,19 @@ by rw lt_def U; exact of_rel₂ U.1
 lemma lift_id : lift id = (id : β* → β*) :=
 funext $ λ x, quotient.induction_on' x $ by apply λ a, quotient.sound (setoid.refl _)
 
-instance [ordered_comm_group β] (U : is_ultrafilter φ) : ordered_comm_group β* :=
+/-- If `φ` is an ultrafilter then the ultraproduct is an ordered commutative group.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected def ordered_comm_group [ordered_comm_group β] (U : is_ultrafilter φ) : ordered_comm_group β* :=
 { add_le_add_left := λ x y hxy z, by revert hxy; exact quotient.induction_on₃' x y z
     (λ a b c hab, by filter_upwards [hab] λ i hi, by simpa),
   add_lt_add_left := λ x y hxy z, by revert hxy; exact quotient.induction_on₃' x y z
     (λ a b c hab, by rw lt_def U at hab ⊢;
     filter_upwards [hab] λ i hi, add_lt_add_left hi (c i)),
   ..filter_product.partial_order, ..filter_product.add_comm_group }
 
-instance [ordered_ring β] (U : is_ultrafilter φ) : ordered_ring β* :=
+/-- If `φ` is an ultrafilter then the ultraproduct is an ordered ring.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected def ordered_ring [ordered_ring β] (U : is_ultrafilter φ) : ordered_ring β* :=
 { mul_nonneg := λ x y, quotient.induction_on₂' x y $
     λ a b ha hb, by filter_upwards [ha, hb] λ i, by simp only [set.mem_set_of_eq];
     exact mul_nonneg,
@@ -380,36 +395,55 @@ instance [ordered_ring β] (U : is_ultrafilter φ) : ordered_ring β* :=
   ..filter_product.ring, ..filter_product.ordered_comm_group U,
   ..filter_product.zero_ne_one_class U.1 }
 
-instance [linear_ordered_ring β] (U : is_ultrafilter φ) : linear_ordered_ring β* :=
+/-- If `φ` is an ultrafilter then the ultraproduct is a linear ordered ring.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected def linear_ordered_ring [linear_ordered_ring β] (U : is_ultrafilter φ) :
+  linear_ordered_ring β* :=
 { zero_lt_one := by rw lt_def U; show (∀* i, (0 : β) < 1); simp [zero_lt_one],
   ..filter_product.ordered_ring U, ..filter_product.linear_order U }
 
-instance [linear_ordered_field β] (U : is_ultrafilter φ) : linear_ordered_field β* :=
+/-- If `φ` is an ultrafilter then the ultraproduct is a linear ordered field.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected def linear_ordered_field [linear_ordered_field β] (U : is_ultrafilter φ) :
+  linear_ordered_field β* :=
 { ..filter_product.linear_ordered_ring U, ..filter_product.field U }
 
-instance [linear_ordered_comm_ring β] (U : is_ultrafilter φ) : linear_ordered_comm_ring β* :=
+/-- If `φ` is an ultrafilter then the ultraproduct is a linear ordered commutative ring.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected def linear_ordered_comm_ring [linear_ordered_comm_ring β] (U : is_ultrafilter φ) :
+  linear_ordered_comm_ring β* :=
 { ..filter_product.linear_ordered_ring U, ..filter_product.comm_monoid }
 
-noncomputable instance [decidable_linear_order β] (U : is_ultrafilter φ) :
+/-- If `φ` is an ultrafilter then the ultraproduct is a decidable linear order.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected noncomputable def decidable_linear_order [decidable_linear_order β] (U : is_ultrafilter φ) :
   decidable_linear_order β* :=
 { decidable_le := by apply_instance,
   ..filter_product.linear_order U }
 
-noncomputable instance [decidable_linear_ordered_comm_group β] (U : is_ultrafilter φ) :
+/-- If `φ` is an ultrafilter then the ultraproduct is a decidable linear ordered commutative group.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected noncomputable def decidable_linear_ordered_comm_group
+  [decidable_linear_ordered_comm_group β] (U : is_ultrafilter φ) :
   decidable_linear_ordered_comm_group β* :=
 { ..filter_product.ordered_comm_group U, ..filter_product.decidable_linear_order U }
 
-noncomputable instance [decidable_linear_ordered_comm_ring β] (U : is_ultrafilter φ) :
+/-- If `φ` is an ultrafilter then the ultraproduct is a decidable linear ordered commutative ring.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected noncomputable def decidable_linear_ordered_comm_ring
+  [decidable_linear_ordered_comm_ring β] (U : is_ultrafilter φ) :
   decidable_linear_ordered_comm_ring β* :=
 { ..filter_product.linear_ordered_comm_ring U,
   ..filter_product.decidable_linear_ordered_comm_group U }
 
-noncomputable instance [discrete_linear_ordered_field β] (U : is_ultrafilter φ) :
-  discrete_linear_ordered_field β* :=
+/-- If `φ` is an ultrafilter then the ultraproduct is a discrete linear ordered field.
+This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
+protected noncomputable def discrete_linear_ordered_field [discrete_linear_ordered_field β]
+  (U : is_ultrafilter φ) : discrete_linear_ordered_field β* :=
 { ..filter_product.linear_ordered_field U, ..filter_product.decidable_linear_ordered_comm_ring U,
   ..filter_product.discrete_field U }
 
-instance [ordered_cancel_comm_monoid β] : ordered_cancel_comm_monoid β* :=
+instance ordered_cancel_comm_monoid [ordered_cancel_comm_monoid β] : ordered_cancel_comm_monoid β* :=
 { add_le_add_left := λ x y hxy z, by revert hxy; exact quotient.induction_on₃' x y z
     (λ a b c hab, by filter_upwards [hab] λ i hi, by simpa),
   le_of_add_le_add_left := λ x y z, quotient.induction_on₃' x y z $ λ x y z h,

src/order/fixed_points.lean

@@ -170,7 +170,9 @@ Sup_le $ λ x hxA, (HA hxA) ▸ (hf $ le_Sup hxA)
 theorem f_le_Inf_of_fixed_points (A : set α) (HA : A ⊆ fixed_points f) : f (Inf A) ≤ Inf A :=
 le_Inf $ λ x hxA, (HA hxA) ▸ (hf $ Inf_le hxA)
 
-instance : complete_lattice (fixed_points f) :=
+/-- The fixed points of `f` form a complete lattice.
+This cannot be an instance, since it depends on the monotonicity of `f`. -/
+protected def complete_lattice : complete_lattice (fixed_points f) :=
 { le           := λx y, x.1 ≤ y.1,
   le_refl      := λ x, le_refl x,
   le_trans     := λ x y z, le_trans,

src/order/pilex.lean

@@ -65,8 +65,10 @@ have lt_not_symm : ∀ {x y : pilex ι β}, ¬ (x < y ∧ y < x),
         (λ hyx, lt_irrefl (x i) (by simpa [hyx] using hi.2))⟩, by tauto⟩,
   ..pilex.has_lt }
 
-instance [linear_order ι] (wf : well_founded ((<) : ι → ι → Prop)) [∀ a, linear_order (β a)] :
-  linear_order (pilex ι β) :=
+/-- `pilex` is a linear order if the original order is well-founded.
+This cannot be an instance, since it depends on the well-foundedness of `<`. -/
+protected def pilex.linear_order [linear_order ι] (wf : well_founded ((<) : ι → ι → Prop))
+  [∀ a, linear_order (β a)] : linear_order (pilex ι β) :=
 { le_total := λ x y, by classical; exact
     or_iff_not_imp_left.2 (λ hxy, begin
       have := not_or_distrib.1 hxy,