6.3. Instance Synthesis🔗

Instance synthesis is a recursive search procedure that either finds an instance for a given type class or fails. In other words, given a type that is registered as a type class, instance synthesis attempts constructs a term with said type. It respects reducibility: semi-reducible or irreducible definitions are not unfolded, so instances for a definition are not automatically treated as instances for its unfolding unless it is reducible. There may be multiple possible instances for a given class; in this case, declared priorities and order of declaration are used as tiebreakers, in that order, with more recent instances taking precedence over earlier ones with the same priority.

This search procedure is efficient in the presence of diamonds and does not loop indefinitely when there are cycles. Diamonds occur when there is more than one route to a given goal, and cycles are situations when two instances each could be solved if the other were solved. Diamonds occur regularly in practice when encoding mathematical concepts using type classes, and Lean's coercion feature naturally leads to cycles, e.g. between finite sets and finite multisets.

Instance synthesis can be tested using the Lean.Parser.Command.synth : command#synth command.

syntax

The Lean.Parser.Command.synth : command#synth command attempts to synthesize an instance for the provided class. If it succeeds, then the resulting term is output.

command ::= ...
    | #synth term

Additionally, inferInstance and inferInstanceAs can be used to synthesize an instance in a position where the instance itself is needed.

def

inferInstance.{u} {α : Sort u} [i : α] : α

inferInstance synthesizes a value of any target type by typeclass inference. This function has the same type signature as the identity function, but the square brackets on the [i : α] argument means that it will attempt to construct this argument by typeclass inference. (This will fail if α is not a class.) Example:

#check (inferInstance : Inhabited Nat) -- Inhabited Nat

def foo : Inhabited (Nat × Nat) :=
  inferInstance

example : foo.default = (default, default) :=
  rfl

def

inferInstanceAs.{u} (α : Sort u) [i : α] : α

inferInstanceAs α synthesizes a value of any target type by typeclass inference. This is just like inferInstance except that α is given explicitly instead of being inferred from the target type. It is especially useful when the target type is some α' which is definitionally equal to α, but the instance we are looking for is only registered for α (because typeclass search does not unfold most definitions, but definitional equality does.) Example:

#check inferInstanceAs (Inhabited Nat) -- Inhabited Nat

6.3.1. Instance Search Summary

Generally speaking, instance synthesis is a recursive search procedure that may, in general, backtrack arbitrarily. Synthesis may succeed with an instance term, fail if no such term can be found, or get stuck if there is insufficient information. A detailed description of the instance synthesis algorithm is available in Selsam, Ullrich, and de Moura (2020)Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura, 2020. “Tabled typeclass resolution”. arXiv:2001.04301. An instance search problem is given by a type class applied to concrete arguments; these argument values may or may not be known. Instance search attempts every locally-bound variable whose type is a class, as well as each registered instance, in order of priority and definition. When candidate instances themselves have instance-implicit parameters, they impose further synthesis tasks.

A problem is only attempted when all of the input parameters to the type class are known. When a problem cannot yet be attempted, then that branch is stuck; progress in other subproblems may result in the problem becoming solvable. Output or semi-output parameters may be either known or unknown at the start of instance search. Output parameters are ignored when checking whether an instance matches the problem, while semi-output parameters are considered.

Every candidate solution for a given problem is saved in a table; this prevents infinite regress in case of cycles as well as exponential search overheads in the presence of diamonds (that is, multiple paths by which the same goal can be achieved). A branch of the search fails when any of the following occur:

All potential instances have been attempted, and the search space is exhausted.
The instance size limit specified by the option synthInstance.maxSize is reached.
The synthesized value of an output parameter does not match the specified value in the search problem. Failed branches are not retried.

If search would otherwise fail or get stuck, the search process attempts to use matching default instances in order of priority. For default instances, the input parameters do not need to be fully known, and may be instantiated by the instances parameter values. Default instances may take instance-implicit parameters, which induce further recursive search.

Successful branches in which the problem is fully known (that is, in which there are no unsolved metavariables) are pruned, and further potentially-successful instances are not attempted, because no later instance could cause the previously-succeeding branch to fail.

6.3.2. Instance Search Problems

Instance search occurs during the elaboration of (potentially nullary) function applications. Some of the implicit parameters' values are forced by others; for instance, an implicit type parameter may be solved using the type of a later value argument that is explicitly provided. Implicit parameters may also be solved using information from the expected type at that point in the program. The search for instance implicit arguments may make use of the implicit argument values that have been found, and may additionally solve others.

Instance synthesis begins with the type of the instance-implicit parameter. This type must be the application of a type class to zero or more arguments; these argument values may be known or unknown when search begins. If an argument to a class is unknown, the search process will not instantiate it unless the corresponding parameter is marked as an output parameter, explicitly making it an output of the instance synthesis routine.

Search may succeed, fail, or get stuck; a stuck search may occur when an unknown argument value becoming known might enable progress to be made. Stuck searches may be re-invoked when the elaborator has discovered one of the previously-unknown implicit arguments. If this does not occur, stuck searches become failures.

6.3.3. Candidate Instances

Instance synthesis uses both local and global instances in its search. Local instances are those available in the local context; they may be either parameters to a function or locally defined with let. Local instances do not need to be indicated specially; any local variable whose type is a type class is a candidate for instance synthesis. Global instances are those available in the global environment; every global instance is a defined name with the instance attribute applied.Lean.Parser.Command.declaration : commandinstance declarations automatically apply the instance attribute.

Local Instances

In this example, addPairs contains a locally-defined instance of Add NatPair:

structure NatPair where
  x : Nat
  y : Nat

def addPairs (p1 p2 : NatPair) : NatPair :=
  let _ : Add NatPair :=
    ⟨fun ⟨x1, y1⟩ ⟨x2, y2⟩ => ⟨x1 + x2, y1 + y2⟩⟩
  p1 + p2

The local instance is used for the addition, having been found by instance synthesis.

Local Instances Have Priority

Here, addPairs contains a locally-defined instance of Add NatPair, even though there is a global instance:

structure NatPair where
  x : Nat
  y : Nat

instance : Add NatPair where
  add
    | ⟨x1, y1⟩, ⟨x2, y2⟩ => ⟨x1 + x2, y1 + y2⟩

def addPairs (p1 p2 : NatPair) : NatPair :=
  let _ : Add NatPair :=
    ⟨fun _ _ => ⟨0, 0⟩⟩
  p1 + p2

The local instance is selected instead of the global one:

{ x := 0, y := 0 }#eval addPairs ⟨1, 2⟩ ⟨5, 2⟩

{ x := 0, y := 0 }

6.3.4. Instance Parameters and Synthesis🔗

The search process for instances is largely governed by class parameters. Type classes take a certain number of parameters, and instances are tried during the search when their choice of parameters is compatible with those in the class type for which the instance is being synthesized.

Instances themselves may also take parameters, but the role of instances' parameters in instance synthesis is very different. Instances' parameters represent either variables that may be instantiated by instance synthesis or further synthesis work to be done before the instance can be used. In particular, parameters to instances may be explicit, implicit, or instance-implicit. If they are instance implicit, then they induce further recursive instance searching, while explicit or implicit parameters must be solved by unification.

Implicit and Explicit Parameters to Instances

While instances typically take parameters either implicitly or instance-implicitly, explicit parameters may be filled out as if they were implicit during instance synthesis. In this example, aNonemptySumInstance is found by synthesis, applied explicitly to Nat, which is needed to make it type-correct.

instance aNonemptySumInstance (α : Type) {β : Type} [inst : Nonempty α] : Nonempty (α ⊕ β) :=
  let ⟨x⟩ := inst
  ⟨.inl x⟩

set_option pp.explicit true in
@aNonemptySumInstance Nat Empty (@instNonemptyOfInhabited Nat instInhabitedNat)#synth Nonempty (Nat ⊕ Empty)

In the output, both the explicit argument Nat and the implicit argument Empty were found by unification with the search goal, while the Nonempty Nat instance was found via recursive instance synthesis.

@aNonemptySumInstance Nat Empty (@instNonemptyOfInhabited Nat instInhabitedNat)

6.3.5. Output Parameters🔗

By default, the parameters of a type class are considered to be inputs to the search process. If the parameters are not known, then the search process gets stuck, because choosing an instance would require the parameters to have values that match those in the instance, which cannot be determined on the basis of incomplete information. In most cases, guessing instances would make instance synthesis unpredictable.

In some cases, however, the choice of one parameter should cause an automatic choice of another. For example, the overloaded membership predicate type class Membership treats the type of elements of a data structure as an output, so that the type of element can be determined by the type of data structure at a use site, instead of requiring that there be sufficient type annotations to determine both types prior to starting instance synthesis. An element of a List Nat can be concluded to be a Nat simply on the basis of its membership in the list.

Type class parameters can be declared as outputs by wrapping their types in the outParam gadget. When a class parameter is an output parameter, instance synthesis will not require that it be known; in fact, any existing value is ignored completely. The first instance that matches the input parameters is selected, and that instance's assignment of the output parameter becomes its value. If there was a pre-existing value, then it is compared with the assignment after synthesis is complete, and it is an error if they do not match.

def

outParam.{u} (α : Sort u) : Sort u

Gadget for marking output parameters in type classes.

For example, the Membership class is defined as:

class Membership (α : outParam (Type u)) (γ : Type v)

This means that whenever a typeclass goal of the form Membership ?α ?γ comes up, Lean will wait to solve it until ?γ is known, but then it will run typeclass inference, and take the first solution it finds, for any value of ?α, which thereby determines what ?α should be.

This expresses that in a term like a ∈ s, s might be a Set α or List α or some other type with a membership operation, and in each case the "member" type α is determined by looking at the container type.

Output Parameters and Stuck Search

This serialization framework provides a way to convert values to some underlying storage type:

class Serialize (input output : Type) where
  ser : input → output
export Serialize (ser)

instance : Serialize Nat String where
  ser n := toString n

instance [Serialize α γ] [Serialize β γ] [Append γ] :
    Serialize (α × β) γ where
  ser
    | (x, y) => ser x ++ ser y

In this example, the output type is unknown.

example := typeclass instance problem is stuck, it is often due to metavariables
  Serialize (Nat × Nat) ?m.16ser (2, 3)

Instance synthesis can't select the Serialize Nat String instance, and thus the Append String instance, because that would require instantiating the output type as String, so the search gets stuck:

typeclass instance problem is stuck, it is often due to metavariables
  Serialize (Nat × Nat) ?m.16

One way to fix the problem is to supply an expected type:

example : String := ser (2, 3)

The other is to make the output type into an output parameter:

class Serialize (input : Type) (output : outParam Type) where
  ser : input → output
export Serialize (ser)

instance : Serialize Nat String where
  ser n := toString n

instance [Serialize α γ] [Serialize β γ] [Append γ] :
    Serialize (α × β) γ where
  ser
    | (x, y) => ser x ++ ser y

Now, instance synthesis is free to select the Serialize Nat String instance, which solves the unknown implicit output parameter of ser:

example := ser (2, 3)

Output Parameters with Pre-Existing Values

The class OneSmaller represents a way to transform non-maximal elements of a type into elements of a type that has one fewer elements. There are two separate instances that can match an input type Option Bool, with different outputs:

class OneSmaller (α : Type) (β : outParam Type) where
  biggest : α
  shrink : (x : α) → x ≠ biggest → β

instance : OneSmaller (Option α) α where
  biggest := none
  shrink
    | some x, _ => x

instance : OneSmaller (Option Bool) (Option Unit) where
  biggest := some true
  shrink
    | none, _ => none
    | some false, _ => some ()

instance : OneSmaller Bool Unit where
  biggest := true
  shrink
    | false, _ => ()

Because instance synthesis selects the most recently defined instance, the following code is an error:

#check failed to synthesize
  OneSmaller (Option Bool) Bool
Additional diagnostic information may be available using the `set_option diagnostics true` command.OneSmaller.shrink (β := Bool) (some false) sorry

failed to synthesize
  OneSmaller (Option Bool) Bool
Additional diagnostic information may be available using the `set_option diagnostics true` command.

The OneSmaller (Option Bool) (Option Unit) instance was selected during instance synthesis, without regard to the supplied value of β.

Semi-output parameters are like output parameters in that they are not required to be known prior to synthesis commencing; unlike output parameters, their values are taken into account when selecting instances.

def

semiOutParam.{u} (α : Sort u) : Sort u

Gadget for marking semi output parameters in type classes.

Semi-output parameters influence the order in which arguments to type class instances are processed. Lean determines an order where all non-(semi-)output parameters to the instance argument have to be figured out before attempting to synthesize an argument (that is, they do not contain assignable metavariables created during TC synthesis). This rules out instances such as [Mul β] : Add α (because β could be anything). Marking a parameter as semi-output is a promise that instances of the type class will always fill in a value for that parameter.

For example, the Coe class is defined as:

class Coe (α : semiOutParam (Sort u)) (β : Sort v)

This means that all Coe instances should provide a concrete value for α (i.e., not an assignable metavariable). An instance like Coe Nat Int or Coe α (Option α) is fine, but Coe α Nat is not since it does not provide a value for α.

Semi-output parameters impose a requirement on instances: each instance of a class with semi-output parameters should determine the values of its semi-output parameters.

Semi-Output Parameters with Pre-Existing Values

The class OneSmaller represents a way to transform non-maximal elements of a type into elements of a type that one fewer elements. It has two separate instances that can match an input type Option Bool, with different outputs:

class OneSmaller (α : Type) (β : semiOutParam Type) where
  biggest : α
  shrink : (x : α) → x ≠ biggest → β

instance : OneSmaller (Option α) α where
  biggest := none
  shrink
    | some x, _ => x

instance : OneSmaller (Option Bool) (Option Unit) where
  biggest := some true
  shrink
    | none, _ => none
    | some false, _ => some ()

instance : OneSmaller Bool Unit where
  biggest := true
  shrink
    | false, _ => ()

Because instance synthesis takes semi-output parameters into account when selecting instances, the OneSmaller (Option Bool) (Option Unit) instance is passed over due to the supplied value for β:

OneSmaller.shrink (some false) ⋯ : Bool#check OneSmaller.shrink (β := Bool) (some false) sorry

OneSmaller.shrink (some false) ⋯ : Bool

6.3.6. Default Instances🔗

When instance synthesis would otherwise fail, having not selected an instance, the default instances specified using the default_instance attribute are attempted in order of priority. When priorities are equal, more recently-defined default instances are chosen before earlier ones. The first default instance that causes the search to succeed is chosen.

Default instances may induce further recursive instance search if the default instances themselves have instance-implicit parameters. If the recursive search fails, the search process backtracks and the next default instance is tried.

6.3.7. “Morally Canonical” Instances

During instance synthesis, if a goal is fully known (that is, contains no metavariables) and search succeeds, no further instances will be attempted for that same goal. In other words, when search succeeds for a goal in a way that can't be refuted by a subsequent increase in information, the goal will not be attempted again, even if there are other instances that could potentially have been used. This optimization can prevent a failure in a later branch of an instance synthesis search from causing spurious backtracking that replaces a fast solution from an earlier branch with a slow exploration of a large state space.

The optimization relies on the assumption that instances are morally canonical. Even if there is more than one potential implementation of a given type class's overloaded operations, or more than one way to synthesize an instance due to diamonds, any discovered instance should be considered as good as any other. In other words, there's no need to consider all potential instances so long as one of them has been guaranteed to work. The optimization may be disabled with the backwards-compatibility option backward.synthInstance.canonInstances, which may be removed in a future version of Lean.

Code that uses instance-implicit parameters should be prepared to consider all instances as equivalent. In other words, it should be robust in the face of differences in synthesized instances. When the code relies on instances in fact being equivalent, it should either explicitly manipulate instances (e.g. via local definitions, by saving them in structure fields, or having a structure inherit from the appropriate class) or it should make this dependency explicit in the type, so that different choices of instance lead to incompatible types.

6.3.8. Options

option

backward.synthInstance.canonInstances

Default value: true

use optimization that relies on 'morally canonical' instances during type class resolution

option

synthInstance.maxHeartbeats

Default value: 20000

maximum amount of heartbeats per typeclass resolution problem. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit

option

synthInstance.maxSize

Default value: 128

maximum number of instances used to construct a solution in the type class instance synthesis procedure