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_inhabited_instances checks that every type has an inhabited 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
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.

source

meta def print_arguments {α : Type u_1} [has_to_tactic_format α] :

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

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_inhabited_instance :

linter

A linter for missing inhabited 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 apply_to_fresh_variables :

expr → tactic expr

Applies expression e to local constants, but lifts all the arguments that are Sort-valued to Type-valued sorts.

source

meta def fails_quickly :

ℕ → declaration → tactic (option string)

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.

source

meta def linter.fails_quickly :

linter

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

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.