Mini-RFC: Weak instance arguments

Stream: lean4

[Kyle Miller]

Lemmas meant for rewriting often have instance arguments that can be picked up from either the LHS or the RHS by unification, and the set of such instances can depending on whether the rewriting is in the forwards or backwards direction. For example, in the following lemma the BEq instance can be picked up from the LHS.

theorem List.erase_cons {α : Type _} [BEq α] (xs : List α) (x a : α) :
    List.erase (x :: xs) a = if x == a then xs else x :: List.erase xs a := by
  rw [List.erase]; split <;> simp [*]

Right now, the semantics of [...] arguments are to always do typeclass instance synthesis, even if the instance was picked up via unification (and if it does, it makes sure that unified instance is defeq to the synthesized instance).

The way to get instance arguments be picked up by unification is to use {...} arguments instead. However, this can entail writing two versions of each rewrite lemma, depending on whether they're meant to be applied in the forward or backward direction.

There were some experiments we did in mathlib during the port earlier this year, and we found that eagerly synthesizing instance arguments could be very expensive, to the point that some examples deep in the algebraic hierarchy would time out. Switching some key lemmas to use {...} arguments instead would make things go through instantly (both rewrites and apply/refine proofs).

[Kyle Miller]

Idea: What if there were a [{...}] binder type that is like {...}, but if it has not been unified with anything, it invokes typeclass instance synthesis?

If this is workable, it would let us write rewrite lemmas that can be applied both in the forward and backward direction while picking up instances through unification, without needing to write two versions of such lemmas. This would also let us more easily work with overlapping Decidable and Fintype instances, which we tend to run into in mathlib, but which in practice are harmless because they are Subsingleton types.

[Kyle Miller]

This [{...}] binder type would be similar (or the same as?) the way [...] arguments elaborated in the Lean 3 community edition. The mathlib library is designed with this elaboration strategy in mind.

[Kyle Miller]

Alternative idea: rw and simp could know how to analyze rewrite lemmas and change [...] binders to {...} binders if they can be solved by unification. This would be less invasive of a change to the core language, but on the other hand this wouldn't let the feature activate in term proofs.

[Kyle Miller]

(More ideas are welcome. These [{...}] binders are just something that crossed my mind today as a way to preserve the current meaning of [...], which is good because it ensures instances are canonical, while letting us selectively weaken that guarantee for performance and applicability reasons.)

[Eric Wieser]

Kyle Miller said:

Right now, the semantics of [...] arguments are to always do typeclass instance synthesis, even if the instance was picked up via unification (and if it does, it makes sure that unified instance is defeq to the synthesized instance).

Is there a good reason for these semantics? What would break if we took your proposed semantics for [{...}], but just applied them to [...]?

[Eric Wieser]

Which is to say; I'm not convinced that[...] is actually meaningfully protecting against non-canonical instances

[Eric Wieser]

Is the danger that you pick up instances with Eq.mpr terms in?

[Kyle Miller]

I think ensuring instances are canonical is a good reason, but you're asking "is resynthesizing instances necessary for this purpose", right?

I'm not sure myself what are practical examples of incorrect instances that can pop up. I guess one example might be if you rewrite Multiplicative X = X. Or perhaps there is some rewrite lemma that introduces a noncanonical instance into a term, and you don't want simp (or other automation) to run wild with it.

[Eric Wieser]

I think my claim is two-fold:

• It's quite rare to get a non-canonical instance in the first place, and almost always when it happens, it was deliberate.
• Canonicity is subjective, and in the presence of instance diamonds (like docs3#pi.has_smul'') resynthesizing presumably won't save you anyway?

[Eric Rodriguez]

I will agree that this resynthesisation behaviour is odd, and possibly not wanted. Is it a small change to remove this from Lean4 core, and try to see whether as a further bonus it would significantly speedup mathlib4 to remove it?

[Kyle Miller]

The resynthesization behavior is intentional and wanted by the core developers.

To turn it off, it might take some work to make sure typeclass synthesis is well-behaved. It eagerly synthesizes instances and only defers them if it can't make progress. In the [{...}] proposal, the synthesis would not be eager, and it would only kick in if it doesn't end up finding an instance through unification.

Switching to that globally would be a big change in elaboration, and it doesn't seem like a good default to me.

[Kyle Miller]

Eric Wieser said:

Canonicity is subjective

I think the assumption is that every way of synthesizing a particular instance is supposed to be defeq to one another, and that defeq equivalence class is "the" canonical instance. I know some diamonds are particularly stubborn though.

Of course, we break this rule with Fintype and Decidable in mathlib... and I'd hate to have to resolve these diamonds since we generally don't care which instance was found for these so long as there is one.

[Eric Rodriguez]

Kyle Miller said:

The resynthesization behavior is intentional and wanted by the core developers.

To turn it off, it might take some work to make sure typeclass synthesis is well-behaved. It eagerly synthesizes instances and only defers them if it can't make progress. In the [{...}] proposal, the synthesis would not be eager, and it would only kick in if it doesn't end up finding an instance through unification.

Switching to that globally would be a big change in elaboration, and it doesn't seem like a good default to me.

I understand that it is intentional, sorry. I meant to say that with the context of Mathlib, it may require a big redesign to make it work properly, and I feel like the advantages of the system are probably poorly-understood compared to our current instance design.

[Kyle Miller]

I know Lean 3 community edition had changes related to typeclass instance synthesis, which we made use of in mathlib, but I've realized I'm hazy on the details. @Anne Baanen: I think I remember you made the changes -- did you do anything other than how simp processes instance arguments to simp lemmas?

[Eric Wieser]

Perhaps there's a compromise here where [...] allows Subsingleton checking (when checking canonicity)

[Eric Wieser]

That would eliminate issues with Decidable and Fintype

[Kyle Miller]

To make that reliable, I think we need to defer synthesizing these instances until after unification has a chance to fill them in. If we just turn the isDefEq check off, then there might be enough information to solve for a non-defeq instance sooner, or to decide to throw a "cannot synthesize instance" error.

[Anne Baanen]

Kyle Miller said:

I know Lean 3 community edition had changes related to typeclass instance synthesis, which we made use of in mathlib, but I've realized I'm hazy on the details. Anne Baanen: I think I remember you made the changes -- did you do anything other than how simp processes instance arguments to simp lemmas?

The important changes are in leanprover-community/lean#657 and leanprover-community/lean#659. Previously in certain cases, the elaborator would stop when it could not synthesize an instance because it had metavariables, even though those metavariables can be filled in by out_params of an instance appearing later. I believe Lean 4 already takes into account these things when determining synthesis order, so it's not so relevant here.

[Kyle Miller]

Thanks. I tried porting a couple of the test files to Lean 4, and it does seem that Lean 4 takes these into account, and now I'm confused about what is the difference between Lean 3 and Lean 4.

I just read through elaborator code from Lean 3 to remind myself how typeclass instance synthesis worked, and it seems to have very similar logic to the Lean 4 version. It even has the defeq check, same as in Lean 4, so we can't say Lean 4 is any different from Lean 3 for resynthesizing instances so often, as least while elaborating.

I guess we need to find some concrete examples that demonstrate elaboration differences.

We can also do experiments by writing a term elaborator that transforms lemmas by converting instance implicit arguments to implicit arguments that can be inferred by unification.

[Anne Baanen]

I thought the difference was as you described in the original post: Lean 3 would not try to synthesize instances found by unification, but indeed I can't easily find in the 3 elaborator where these would be assigned.

[Anne Baanen]

I can't quickly come up with an example that shows the difference.

[Kyle Miller]

Yeah, but I haven't been able to find where in the elaborator Lean 3 wouldn't resynthesize instances during elaboration. Nothing checks that the metavariable is already assigned, and so long as it's an instance implicit argument, the argument gets synthesized.

Maybe one feature that gave us a different impression is the new behavior of @, since it doesn't fully switch arguments into being explicit arguments like it did in Lean 3, where in Lean 4 you have to write (_) instead of _ to make an instance implicit argument not synthesize.

[Anne Baanen]

Random thought right before I step into the shower: does the same hold for instances encountered when instance search is already going on? For example, let's say we have

class Foo (X : Type)
class Bar (X : Type)
class Baz (X : Type) [Foo X] extends Bar X

inductive P

instance P.foo : Foo P where
instance P.baz : Baz P where

example : Bar P := inferInstance -- Does this look for a `Foo P` instance or use the `Foo` argument to `P.bar`?

[Anne Baanen]

I should really wrap up for today but it feels like we might want to look in this direction. Maybe that also explains why #8386 seems to cause so many timeouts?

[Anne Baanen]

The idea seems correct! In Lean 3:

class Foo (X : Type)
class Bar (X : Type)
class Baz (X : Type) [Foo X] extends Bar X

inductive P

instance P.foo : Foo P := {}
instance P.baz : Baz P := {}

set_option trace.class_instances true
example : Bar P := infer_instance
/-
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : Bar P := @Baz.to_Bar ?x_1 ?x_2 ?x_3
[class_instances] (1) ?x_3 : @Baz P ?x_2 := P.baz
[class_instances] caching instance for @Baz P P.foo
P.baz
[class_instances] caching instance for Bar P
@Baz.to_Bar P P.foo P.baz
-/

in Lean 4:

class Foo (X : Type)
class Bar (X : Type)
class Baz (X : Type) [Foo X] extends Bar X

inductive P

instance P.foo : Foo P where
instance P.baz : Baz P where

set_option trace.Meta.synthInstance true in
example : Bar P := inferInstance -- Does this look for a `Foo P` instance or use the `Foo` argument to `P.bar`?
/-
[Meta.synthInstance] ✅ Bar P ▼
  [] new goal Bar P ▶
  [] ✅ apply @Baz.toBar to Bar P ▼
    [tryResolve] ✅ Bar P ≟ Bar P
    [] new goal Foo P ▶
  [] ✅ apply P.foo to Foo P ▼
    [tryResolve] ✅ Foo P ≟ Foo P
  [resume] propagating Foo P to subgoal Foo P of Bar P ▶
  [] ✅ apply P.baz to Baz P ▼
    [tryResolve] ✅ Baz P ≟ Baz P
  [resume] propagating Baz P to subgoal Baz P of Bar P ▶
  [] result Baz.toBar
-/