Instance parameters depending on `out_params`

Stream: general

[Anne Baanen]

While troubleshooting #11128, I discovered a principle of typeclasses that was kind of surprising to me: if a class takes an instance parameter, and that instance parameter depends on an out_param, sometimes instance search gets blocked:

prelude
import init.core

class semiring (G : Type*) := (one : G)

instance : semiring nat := ⟨1⟩

namespace erroring

class add_monoid_hom_class (F : Type*) (H : out_param Type*) [semiring H] :=
(coe : F → nat → H)
(ext_nat : ∀ (f g : F), coe f 1 = coe g 1 → f = g)

open add_monoid_hom_class

class semiring_hom_class (F : Type*) (H : out_param Type*) [semiring H]
  extends add_monoid_hom_class F H :=
(map_one : ∀ (f : F), coe f 1 = semiring.one)

lemma semiring_hom_class.ext_nat {F : Type*} {H : out_param Type*} [semiring H]
  [semiring_hom_class F H] (f g : F) : f = g :=
add_monoid_hom_class.ext_nat f g $
  (semiring_hom_class.map_one f).trans (semiring_hom_class.map_one g).symm
  -- error: can't synthesize type `H`
  -- no attempt is made to infer `add_monoid_hom_class`

end erroring

The correct solution appears to make everything that depends on an out_param also an out_param:

namespace working

class add_monoid_hom_class (F : Type*) (H : out_param Type*) [out_param $ semiring H] :=
(coe : F → nat → H)
(ext_nat : ∀ (f g : F), coe f 1 = coe g 1 → f = g)

open add_monoid_hom_class

class semiring_hom_class (F : Type*) (H : out_param Type*) [out_param $ semiring H]
  extends add_monoid_hom_class F H :=
(map_one : ∀ (f : F), coe f 1 = semiring.one)

lemma semiring_hom_class.ext_nat {F : Type*} {H : out_param Type*} [semiring H]
  [semiring_hom_class F H] (f g : F) : f = g :=
add_monoid_hom_class.ext_nat f g $
  (semiring_hom_class.map_one f).trans (semiring_hom_class.map_one g).symm

end working

Does the smarter order of elaboration in Lean 4 fix this?

[Gabriel Ebner]

This has nothing to do with the elaboration order.

[Gabriel Ebner]

What happens when you mark a type class argument as out_param is that Lean will preprocess type class queries for that class as follows:
add_monoid_hom_class (A ...) (B...) is rewritten to add_monoid_hom_class (A ...) ?H (i.e., every out_param is replaced by a metavariable).

[Gabriel Ebner]

Note: this only happens for the top-level query. No preprocessing happens during search. If you have instance [add_monoid_hom_class A B] : blah then B is not replaced by a metavariable when the instance is applied.

[Gabriel Ebner]

Looking at your example more closely, marking the instances as out_param as well is actually supposed to be done automatically:

Type class parameters can be annotated with out_param annotations.

Given (C a_1 ... a_n), we replace a_i with a temporary metavariable ?x_i IF

• Case 1
  a_i is an out_param
  OR

• Case 2
  a_i depends on a_j for j < i, and a_j was replaced with a temporary metavariable ?x_j.
  This case is needed to make sure the new C-application is type correct.

[Anne Baanen]

I now have the precise diagnosis: elaborator::synthesize_type_class_instances_step skips instances if elaborator::ready_to_synthesize indicates they have metavariables that are not covered by out_params. However, it doesn't count dependencies of out_params. (Note that preprocess_class is called by the elaborator only after the elaborator decides to call mk_instance, i.e. ready_to_synthesize returns true. So I'd say this is kind of an elaboration order issue.)

[Anne Baanen]

Unfortunately, copying the logic from type_context_old::preprocess_class to elaborator::ready_to_synthesize is not so easy, since preprocess_class uses the metavariables it inserts for out_params to determine the other parameters that have a dependency.

[Anne Baanen]

Alright, I think I have something that works correctly. After the version with more documentation (re-)compiles I'll run the test suite with an assert that the new non-mutating check does the same as the previous one.

[Anne Baanen]

lean#657