global etaExperiment

Stream: mathlib4

[Scott Morrison]

In an attempt to understand better what is going on with etaExperiment, I tried turning it on for the entire build: !4#3744.

First, this results in some typeclass searches taking longer, so I increased synthInstance.maxHeartbeats globally too.

However I then start getting failures to find instances, in ways I don't really understand. I've annotated one of the typical failures in that PR, so you can see this in the diff.

An instance like:

set_option trace.Meta.synthInstance true in
example {J : Type _} [Category J] {C : Type _} [Category C] [HasTerminal C]
    (s : Cone ((Functor.const J).obj (⊤_ C))) : Subsingleton (s.pt ⟶ ⊤_ C) :=
  inferInstance

works fine in isolation, generating the trace messages:

  [Meta.synthInstance] ✅ Subsingleton (s.pt ⟶ ⊤_ C) ▼
  [] new goal Subsingleton (s.pt ⟶ ⊤_ C) ▶
  [] ❌ apply @Preorder.Preorder.subsingleton_hom to Subsingleton (s.pt ⟶ ⊤_ C) ▶
  [] ❌ apply instSubsingleton to Subsingleton (s.pt ⟶ ⊤_ C) ▶
  [] ✅ apply @Unique.instSubsingleton to Subsingleton (s.pt ⟶ ⊤_ C) ▼
    [tryResolve] ✅ Subsingleton (s.pt ⟶ ⊤_ C) ≟ Subsingleton (s.pt ⟶ ⊤_ C)
    [] new goal Unique (s.pt ⟶ ⊤_ C) ▼
      [instances] #[@CategoryTheory.Limits.uniqueToTerminal]
  [] ✅ apply @CategoryTheory.Limits.uniqueToTerminal to Unique (s.pt ⟶ ⊤_ C) ▼
    [tryResolve] ✅ Unique (s.pt ⟶ ⊤_ C) ≟ Unique (s.pt ⟶ ⊤_ C)
  [resume] propagating Unique (s.pt ⟶ ⊤_ C) to subgoal Unique (s.pt ⟶ ⊤_ C) of Subsingleton (s.pt ⟶ ⊤_ C) ▼
    [] size: 1
  [] result Unique.instSubsingleton

as you might hope. However in the actual proof, where we need to find this instance in simp only [eq_iff_true_of_subsingleton], we see the shorter trace output:

          [Meta.synthInstance] 💥 Subsingleton (s.pt ⟶ ⊤_ C) ▼
          [] new goal Subsingleton (s.pt ⟶ ⊤_ C) ▼
            [instances] #[@IsEmpty.instSubsingleton, @Unique.instSubsingleton, instSubsingleton, @Preorder.Preorder.subsingleton_hom]
          [] 💥 apply @Preorder.Preorder.subsingleton_hom to Subsingleton (s.pt ⟶ ⊤_ C) ▼
            [tryResolve] 💥 Subsingleton (s.pt ⟶ ⊤_ C) ≟ Subsingleton (?m.78176 ⟶ ?m.78177)

and Lean apparently gives up before trying the other options.

Going back to set_option synthInstance.etaExperiment false, Lean successfully finds the instance in both situations.

@Gabriel Ebner, any ideas what is going on here?

[Gabriel Ebner]

Without seeing more of the trace, this looks like the max u v issue.

[Scott Morrison]

@Gabriel Ebner, sorry, I should have posted a link here to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Failure.20of.20TC.20search.20in.20.60simp.60.20with.20.60etaExperiment.60.2E, where this example was minimized and diagnosed further.