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
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 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
because many instances only apply in that special case, and we do want to catch those loops.