Linters about type classes #

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

instance_priority ensures that blanket instances have low priority.
has_nonempty_instances checks that every type has a nonempty instance, an inhabited instance, or a unique instance.
impossible_instance checks that there are no instances which can never apply.
incorrect_type_class_argument checks that only type classes are used in instance-implicit arguments.
dangerous_instance checks for instances that generate subproblems with metavariables.
fails_quickly checks that type class resolution finishes quickly.
class_structure checks that every class is a structure, i.e. @[class] def is forbidden.
has_coe_variable checks that there is no instance of type has_coe α t.
inhabited_nonempty checks whether [inhabited α] arguments could be generalized to [nonempty α].
decidable_classical checks propositions for [decidable_... p] hypotheses that are not used in the statement, and could thus be removed by using classical in the proof.
linter.has_coe_to_fun checks whether necessary has_coe_to_fun instances are declared.
linter.check_reducibility checks whether non-instances with a class as type are reducible.

source

meta def print_arguments {α : Type u_1} [has_to_tactic_format α] (l : list (ℕ × α)) :

tactic string

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 get_pi_binders.

source

def library_note.implicit instance arguments :

unit

There are places where typeclass arguments are specified with implicit {} brackets instead of the usual [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type of one of the other arguments. When they can be inferred from these other arguments, it is faster to use this method than to use type class inference.

For example, when writing lemmas about (f : α →+* β), it is faster to specify the fact that α and β are semirings as {rα : semiring α} {rβ : semiring β} rather than the usual [semiring α] [semiring β].

source

def library_note.lower instance priority :

unit

Certain instances always apply during type-class resolution. For example, the instance add_comm_group.to_add_group {α} [add_comm_group α] : add_group α applies to all type-class resolution problems of the form add_group _, and type-class inference will then do an exhaustive search to find a commutative group. These instances take a long time to fail. Other instances will only apply if the goal has a certain shape. For example int.add_group : add_group ℤ or add_group.prod {α β} [add_group α] [add_group β] : add_group (α × β). Usually these instances will fail quickly, and when they apply, they are almost always the desired instance. For this reason, we want the instances of the second type (that only apply in specific cases) to always have higher priority than the instances of the first type (that always apply). See also #1561.

Therefore, if we create an instance that always applies, we set the priority of these instances to 100 (or something similar, which is below the default value of 1000).

source

meta def linter.instance_priority :

linter

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

source

meta def linter.has_nonempty_instance :

linter

A linter for missing nonempty instances.

source

meta def linter.impossible_instance :

linter

A linter object for impossible_instance.

source

meta def linter.incorrect_type_class_argument :

linter

A linter object for incorrect_type_class_argument.

source

meta def linter.dangerous_instance :

linter

A linter object for dangerous_instance.

source

meta def find_nondep_aux :

list expr → expr_set → tactic expr_set

Auxilliary definition for find_nondep

source

meta def find_nondep :

tactic (list expr)

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

source

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

tactic (option string)

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).

source

meta def linter.fails_quickly :

linter

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

source

meta def linter.class_structure :

linter

A linter object for class_structure.

source

meta def linter.has_coe_variable :

linter

A linter object for has_coe_variable.

source

meta def linter.inhabited_nonempty :

linter

A linter object for inhabited_nonempty.

source

meta def linter.decidable_classical :

linter

A linter object for decidable_classical.

source

meta def linter.fintype_finite_fun (d : declaration) :

tactic (option string)

Checks whether a declaration is Prop-valued and takes a fintype _ hypothesis that is unused elsewhere in the type. In this case, that hypothesis can be replaced with casesI nonempty_fintype _ in the proof.

source

meta def linter.fintype_finite :

linter

A linter object for fintype vs finite.

source

meta def linter.has_coe_to_fun :

linter

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

source

meta def check_reducible_non_instances (d : declaration) :

tactic (option string)

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.

source

meta def linter.check_reducibility :

linter

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