mathlib documentation

tactic.lint.type_classes

Linters about type classes #

This file defines several linters checking the correct usage of type classes and the appropriate definition of instances:

A linter object for checking instance priorities of instances that always apply. This is in the default linter set.

A linter for missing inhabited instances.

A linter object for impossible_instance.

A linter object for incorrect_type_class_argument.

A linter object for dangerous_instance.

Auxilliary definition for find_nondep

meta def find_nondep  :

Finds all hypotheses that don't occur in the target or other hypotheses.

meta def fails_quickly (max_steps : ) (d : declaration) :

Tests whether type-class inference search will end quickly on certain unsolvable type-class problems. This is to detect loops or very slow searches, which are problematic (recall that normal type-class search often creates unsolvable subproblems, which have to fail quickly for type-class inference to perform well. We create these type-class problems by taking an instance, and removing the last hypothesis that doesn't appear in the goal (or a later hypothesis). Note: this argument is necessarily an instance-implicit argument if it passes the linter.incorrect_type_class_argument. 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 (usually a maximum depth in the search).

A linter object for fails_quickly. We currently set the number of steps in the type-class search pretty high. Some instances take quite some time to fail, and we seem to run against the caching issue in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/odd.20repeated.20type.20class.20search

A linter object for class_structure.

A linter object for has_coe_variable.

A linter object for inhabited_nonempty.

A linter object for decidable_classical.

Linter that checks whether has_coe_to_fun instances comply with Note [function coercion].

Checks whether an instance contains a semireducible non-instance with a class as type in its value. We add some restrictions to get not too many false positives:

  • We only consider classes with an add or mul field, since those classes are most likely to occur as a field to another class, and be an extension of another class.
  • We only consider instances of type-valued classes and non-instances that are definitions.
  • We currently ignore declarations foo that have a foo._main declaration. We could look inside, or at the generated equation lemmas, but it's unlikely that there are many problematic instances defined using the equation compiler.

A linter that checks whether an instance contains a semireducible non-instance.