Linters about type classes #
This file defines several linters checking the correct usage of type classes and the appropriate definition of instances:
instance_priorityensures that blanket instances have low priority.
has_inhabited_instanceschecks that every type has an
impossible_instancechecks that there are no instances which can never apply.
incorrect_type_class_argumentchecks that only type classes are used in instance-implicit arguments.
dangerous_instancechecks for instances that generate subproblems with metavariables.
fails_quicklychecks that type class resolution finishes quickly.
class_structurechecks that every
classis a structure, i.e.
@[class] defis forbidden.
has_coe_variablechecks that there is no instance of type
has_coe α t.
[inhabited α]arguments could be generalized to
decidable_classicalchecks propositions for
[decidable_... p]hypotheses that are not used in the statement, and could thus be removed by using
classicalin the proof.
linter.has_coe_to_funchecks whether necessary
has_coe_to_funinstances are declared.
linter.check_reducibilitychecks whether non-instances with a class as type are reducible.
Pretty prints a list of arguments of a declaration. Assumes
l is a list of argument positions
and binders (or any other element that can be pretty printed).
l can be obtained e.g. by applying
list.indexes_values to a list obtained by
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
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
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
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
mulfield, 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
foothat have a
foo._maindeclaration. 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.