feat(lint): add two new linters (#2089)

* feat(lint): add two new linters

checks whether type-class inference searches end relatively quickly
checks that there are no instances has_coe a t with variable a

* remove `is_fast` from `has_coe_variable`

* add link to note

* typo in priority

* fix error, implement comments

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

docs/commands.md

@@ -115,10 +115,12 @@ The following linters are run by default:
 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.
-11. `inhabited_nonempty` checks for `inhabited` instance arguments that should be changed to `nonempty`.
-12. `simp_nf` checks that the left-hand side of simp lemmas is in simp-normal form.
-13. `simp_var_head` checks that there are no variables as head symbol of left-hand sides of simp lemmas.
-14. `simp_comm` checks that no commutativity lemmas (such as `add_comm`) are marked simp.
+11. `fails_quickly` tests that type-class inference ends (relatively) quickly when applied to variables.
+12. `has_coe_variable` tests that there are no instances of type `has_coe α t` for a variable `α`.
+13. `inhabited_nonempty` checks for `inhabited` instance arguments that should be changed to `nonempty`.
+14. `simp_nf` checks that the left-hand side of simp lemmas is in simp-normal form.
+15. `simp_var_head` checks that there are no variables as head symbol of left-hand sides of simp lemmas.
+16. `simp_comm` checks that no commutativity lemmas (such as `add_comm`) are marked simp.
 
 Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
 This is not run by default.

src/tactic/core.lean

@@ -6,6 +6,8 @@ Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek
 import data.dlist.basic category.basic meta.expr meta.rb_map data.bool tactic.library_note
   tactic.derive_inhabited
 
+universe variable u
+
 namespace expr
 open tactic
 
@@ -41,7 +43,7 @@ args.mfoldr (λarg i:expr, do
   inner
 
 /-- `traverse f e` applies the monadic function `f` to the direct descendants of `e`. -/
-meta def {u} traverse {m : Type → Type u} [applicative m]
+meta def traverse {m : Type → Type u} [applicative m]
   {elab elab' : bool} (f : expr elab → m (expr elab')) :
   expr elab → m (expr elab')
  | (var v)  := pure $ var v
@@ -1332,6 +1334,23 @@ open interactive interactive.types
 local postfix `?`:9001 := optional
 local postfix *:9001 := many .
 "
+/-- Applies tactic `t`. If it succeeds, revert the state, and return the value. If it fails,
+  returns the error message. -/
+meta def retrieve_or_report_error {α : Type u} (t : tactic α) : tactic (α ⊕ string) :=
+λ s, match t s with
+| (interaction_monad.result.success a s') := result.success (sum.inl a) s
+| (interaction_monad.result.exception msg' _ s') :=
+  result.success (sum.inr (msg'.iget ()).to_string) s
+end
+
+/-- This tactic succeeds if `t` succeeds or fails with message `msg` such that `p msg` is `tt`.
+-/
+meta def succeeds_or_fails_with_msg {α : Type} (t : tactic α) (p : string → bool) : tactic unit :=
+do x ← retrieve_or_report_error t,
+match x with
+| (sum.inl _) := skip
+| (sum.inr msg) := if p msg then skip else fail msg
+end
 
 /-- `trace_error msg t` executes the tactic `t`. If `t` fails, traces `msg` and the failure message
 of `t`. -/
@@ -1346,7 +1365,7 @@ meta def trace_error (msg : string) (t : tactic α) : tactic α
 This combinator is for testing purposes. It succeeds if `t` fails with message `msg`,
 and fails otherwise.
 -/
-meta def {u} success_if_fail_with_msg {α : Type u} (t : tactic α) (msg : string) : tactic unit :=
+meta def success_if_fail_with_msg {α : Type u} (t : tactic α) (msg : string) : tactic unit :=
 λ s, match t s with
 | (interaction_monad.result.exception msg' _ s') :=
   let expected_msg := (msg'.iget ()).to_string in

src/tactic/lint.lean

@@ -24,10 +24,12 @@ The following linters are run by default:
 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.
-11. `inhabited_nonempty` checks for `inhabited` instance arguments that should be changed to `nonempty`.
-12. `simp_nf` checks that the left-hand side of simp lemmas is in simp-normal form.
-13. `simp_var_head` checks that there are no variables as head symbol of left-hand sides of simp lemmas.
-14. `simp_comm` checks that no commutativity lemmas (such as `add_comm`) are marked simp.
+11. `fails_quickly` tests that type-class inference ends (relatively) quickly when applied to variables.
+12. `has_coe_variable` tests that there are no instances of type `has_coe α t` for a variable `α`.
+13. `inhabited_nonempty` checks for `inhabited` instance arguments that should be changed to `nonempty`.
+14. `simp_nf` checks that the left-hand side of simp lemmas is in simp-normal form.
+15. `simp_var_head` checks that there are no variables as head symbol of left-hand sides of simp lemmas.
+16. `simp_comm` checks that no commutativity lemmas (such as `add_comm`) are marked simp.
 
 Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
 This is not run by default.
@@ -407,7 +409,7 @@ meta def incorrect_type_class_argument (d : declaration) : tactic (option string
   _ :: _ ← return bad_arguments | return none,
   (λ s, some $ "These are not classes. " ++ s) <$> print_arguments bad_arguments
 
-/-- A linter object for `impossible_instance`. -/
+/-- A linter object for `incorrect_type_class_argument`. -/
 @[linter, priority 1420] meta def linter.incorrect_type_class_argument : linter :=
 { test := incorrect_type_class_argument,
   no_errors_found := "All declarations have correct type-class arguments",
@@ -433,6 +435,59 @@ meta def dangerous_instance (d : declaration) : tactic (option string) := do
   no_errors_found := "No dangerous instances",
   errors_found := "DANGEROUS INSTANCES FOUND.\nThese instances are recursive, and create a new type-class problem which will have metavariables. Currently this linter does not check whether the metavariables only occur in arguments marked with `out_param`, in which case this linter gives a false positive." }
 
+/-- Applies expression `e` to local constants, but lifts all the arguments that are `Sort`-valued to
+  `Type`-valued sorts. -/
+meta def apply_to_fresh_variables (e : expr) : tactic expr := do
+t ← infer_type e,
+(xs, b) ← mk_local_pis t,
+xs.mmap' $ λ x, try $ do {
+  u ← mk_meta_univ,
+  tx ← infer_type x,
+  ttx ← infer_type tx,
+  unify ttx (expr.sort u.succ) },
+return $ e.app_of_list xs
+
+/-- Tests whether type-class inference search for a class will end quickly when applied to
+  variables. This tactic succeeds if `mk_instance` succeeds quickly or fails quickly with the error
+  message that it cannot find an instance. It fails if the tactic takes too long, or if any other
+  error message is raised.
+  We make sure that we apply the tactic to variables living in `Type u` instead of `Sort u`,
+  because many instances only apply in that special case, and we do want to catch those loops. -/
+meta def fails_quickly (max_steps : ℕ) (d : declaration) : tactic (option string) := do
+  e ← mk_const d.to_name,
+  tt ← is_class e | return none,
+  e' ← apply_to_fresh_variables e,
+  sum.inr msg ← retrieve_or_report_error $ tactic.try_for max_steps $
+    succeeds_or_fails_with_msg (mk_instance e')
+      $ λ s, "tactic.mk_instance failed to generate instance for".is_prefix_of s | return none,
+  return $ some $
+    if msg = "try_for tactic failed, timeout" then "type-class inference timed out" else msg
+
+/-- A linter object for `fails_quickly`. If we want to increase the maximum number of steps
+  type-class inference is allowed to take, we can increase the number `3000` in the definition.
+  As of 5 Mar 2020 the longest trace (for `is_add_hom`) takes 2900-3000 "heartbeats". -/
+@[linter, priority 1408] meta def linter.fails_quickly : linter :=
+{ test := fails_quickly 3000,
+  no_errors_found := "No time-class searches timed out",
+  errors_found := "TYPE CLASS SEARCHES TIMED OUT.
+For the following classes, there is an instance that causes a loop, or an excessively long search.",
+  is_fast := ff }
+
+/-- Tests whether there is no instance of type `has_coe α t` where `α` is a variable.
+See note [use has_coe_t]. -/
+meta def has_coe_variable (d : declaration) : tactic (option string) := do
+  tt ← is_instance d.to_name | return none,
+  `(has_coe %%a _) ← return d.type.pi_codomain | return none,
+  tt ← return a.is_var | return none,
+  return $ some $ "illegal instance"
+
+/-- A linter object for `has_coe_variable`. -/
+@[linter, priority 1405] meta def linter.has_coe_variable : linter :=
+{ test := has_coe_variable,
+  no_errors_found := "No invalid `has_coe` instances",
+  errors_found := "INVALID `has_coe` INSTANCES.
+Make the following declarations instances of the class `has_coe_t` instead of `has_coe`." }
+
 /-- Checks whether a declaration is prop-valued and takes an `inhabited _` argument that is unused
     elsewhere in the type. In this case, that argument can be replaced with `nonempty _`. -/
 meta def inhabited_nonempty (d : declaration) : tactic (option string) :=

test/lint.lean

@@ -64,13 +64,6 @@ run_cmd do
   (_, s) ← lint tt tt [`linter.dummy_linter] tt,
   guard $ "/- found something: -/\n#print foo.foo /- gotcha! -/".is_suffix_of s.to_string
 
-instance impossible_instance_test {α β : Type} [add_group α] : has_add α := infer_instance
-
-run_cmd do
-  d ← get_decl `impossible_instance_test,
-  x ← impossible_instance d,
-  guard $ x = some "Impossible to infer argument 2: {β : Type}"
-
 def incorrect_type_class_argument_test {α : Type} (x : α) [x = x] [decidable_eq α] [group α] :
   unit := ()
 
@@ -79,10 +72,53 @@ run_cmd do
   x ← incorrect_type_class_argument d,
   guard $ x = some "These are not classes. argument 3: [_inst_1 : x = x]"
 
-instance dangerous_instance_test {α β γ : Type} [ring α] [add_comm_group β] [has_coe α β]
-  [has_inv γ] : has_add β := infer_instance
+section
+def impossible_instance_test {α β : Type} [add_group α] : has_add α := infer_instance
+local attribute [instance] impossible_instance_test
+run_cmd do
+  d ← get_decl `impossible_instance_test,
+  x ← impossible_instance d,
+  guard $ x = some "Impossible to infer argument 2: {β : Type}"
 
+def dangerous_instance_test {α β γ : Type} [ring α] [add_comm_group β] [has_coe α β]
+  [has_inv γ] : has_add β := infer_instance
+local attribute [instance] dangerous_instance_test
 run_cmd do
   d ← get_decl `dangerous_instance_test,
   x ← dangerous_instance d,
   guard $ x = some "The following arguments become metavariables. argument 1: {α : Type}, argument 3: {γ : Type}"
+end
+
+section
+def foo_has_mul {α} [has_mul α] : has_mul α := infer_instance
+local attribute [instance, priority 1] foo_has_mul
+run_cmd do
+  d ← get_decl `has_mul,
+  some s ← fails_quickly 500 d,
+  guard $ s = "type-class inference timed out"
+local attribute [instance, priority 10000] foo_has_mul
+run_cmd do
+  d ← get_decl `has_mul,
+  some s ← fails_quickly 3000 d,
+  guard $ "maximum class-instance resolution depth has been reached".is_prefix_of s
+end
+
+section
+def foo_instance {α} (R : setoid α) : has_coe α (quotient R) := ⟨quotient.mk⟩
+local attribute [instance, priority 1] foo_instance
+run_cmd do
+  d ← get_decl `foo_instance,
+  some "illegal instance" ← has_coe_variable d,
+  d ← get_decl `has_coe_to_fun,
+  some s ← fails_quickly 3000 d,
+  guard $ "maximum class-instance resolution depth has been reached".is_prefix_of s
+end
+
+/- test of `apply_to_fresh_variables` -/
+run_cmd do
+  e ← mk_const `id,
+  e2 ← apply_to_fresh_variables e,
+  type_check e2,
+  `(@id %%α %%a) ← instantiate_mvars e2,
+  expr.sort (level.succ $ level.mvar u) ← infer_type α,
+  skip