Failure of TC search in `simp` with `etaExperiment`.

Stream: lean4

[Scott Morrison]

During the porting meeting we discussed a problem I'd encountered where simp was failing to find instances when etaExperiment was on, even though inferInstance found these instances fine (with or with etaExperiment).

[Scott Morrison]

During the meeting I could only show an example within mathlib4, but I've now minimised.

[Scott Morrison]

theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True :=
  ⟨fun _ => ⟨⟩, fun _ => (Subsingleton.elim ..)⟩

class Unique (α : Sort u) extends Inhabited α where
  uniq : ∀ a : α, a = default

instance [Unique α] : Subsingleton α :=
  ⟨fun a b => Unique.uniq a ▸ Unique.uniq b ▸ rfl⟩

class Cat (obj : Type u) : Type max u (v + 1) where
  Hom : obj → obj → Type v

infixr:10 " ⟶ " => Cat.Hom

instance (α : Type u) : Cat.{u, u} α where
  Hom U V := ULift (PLift (U = V))

instance {α : Type u} (U V : α) : Subsingleton (U ⟶ V) := ⟨fun ⟨⟨x⟩⟩ ⟨⟨_⟩⟩ => by congr⟩

set_option pp.universes true
set_option trace.Meta.synthInstance true

-- This instance is found by `inferInstance`:
example {C : Type _} [Cat C] (X Y : C) [Unique (X ⟶ Y)] : Subsingleton (X ⟶ Y) :=
  inferInstance
  -- Succeeds with:
  -- [Meta.synthInstance] ✅ Subsingleton.{?u.8236 + 1} (Cat.Hom.{?u.8233, ?u.8236} X Y) ▼
  --   [] new goal Subsingleton.{?u.8236 + 1} (Cat.Hom.{?u.8233, ?u.8236} X Y) ▼
  --     [instances] #[instSubsingleton, @instSubsingleton_1.{?u.8281}, @instSubsingletonHomInstCat.{?u.8282}]
  --   [] ❌ apply @instSubsingletonHomInstCat.{?u.8282} to Subsingleton.{?u.8236 + 1} (Cat.Hom.{?u.8233, ?u.8236} X Y) ▼
  --     [tryResolve] ❌ Subsingleton.{?u.8236 + 1}
  --           (Cat.Hom.{?u.8233, ?u.8236} X Y) ≟ Subsingleton.{?u.8282 + 1} (Cat.Hom.{?u.8282, ?u.8282} ?m.8284 ?m.8285)
  --   [] ✅ apply @instSubsingleton_1.{?u.8236 + 1} to Subsingleton.{?u.8236 + 1} (Cat.Hom.{?u.8233, ?u.8236} X Y) ▼
  --     [tryResolve] ✅ Subsingleton.{?u.8236 + 1}
  --           (Cat.Hom.{?u.8233, ?u.8236} X Y) ≟ Subsingleton.{?u.8236 + 1} (Cat.Hom.{?u.8233, ?u.8236} X Y)
  --     [] new goal Unique.{?u.8236 + 1} (Cat.Hom.{?u.8233, ?u.8236} X Y) ▼
  --       [instances] #[inst✝]
  --   [] ✅ apply inst✝ to Unique.{?u.8236 + 1} (Cat.Hom.{?u.8233, ?u.8236} X Y) ▼
  --     [tryResolve] ✅ Unique.{?u.8236 + 1} (Cat.Hom.{?u.8233, ?u.8236} X Y) ≟ Unique.{?u.8236 + 1} (Cat.Hom.{?u.8233, ?u.8236} X Y)
  --   [resume] propagating Unique.{?u.8236 + 1}
  --         (Cat.Hom.{?u.8233, ?u.8236} X
  --           Y) to subgoal Unique.{?u.8236 + 1}
  --         (Cat.Hom.{?u.8233, ?u.8236} X Y) of Subsingleton.{?u.8236 + 1} (Cat.Hom.{?u.8233, ?u.8236} X Y) ▼
  --     [] size: 1
  --   [] result instSubsingleton_1.{?u.8236 + 1}

set_option synthInstance.etaExperiment true in
example {C : Type _} [Cat C] (X Y : C) [Unique (X ⟶ Y)] : Subsingleton (X ⟶ Y) :=
  inferInstance
  -- Still works with etaExperiment, with the same trace.

example {C : Type _} [Cat C] (X Y : C) [Unique (X ⟶ Y)] (f g : X ⟶ Y) : f = g := by
  simp only [eq_iff_true_of_subsingleton]
  -- Succeeds with identical trace.

set_option synthInstance.etaExperiment true in
example {C : Type _} [Cat C] (X Y : C) [Unique (X ⟶ Y)] (f g : X ⟶ Y) : f = g := by
  simp only [eq_iff_true_of_subsingleton]
  -- Fails with
  -- [Meta.synthInstance] 💥 Subsingleton.{?u.8454 + 1} (Cat.Hom.{?u.8451, ?u.8454} X Y) ▼
  --   [] new goal Subsingleton.{?u.8454 + 1} (Cat.Hom.{?u.8451, ?u.8454} X Y) ▼
  --     [instances] #[instSubsingleton, @instSubsingleton_1.{?u.8566}, @instSubsingletonHomInstCat.{?u.8567}]
  --   [] 💥 apply @instSubsingletonHomInstCat.{?u.8567} to Subsingleton.{?u.8454 + 1} (Cat.Hom.{?u.8451, ?u.8454} X Y) ▼
  --     [tryResolve] 💥 Subsingleton.{?u.8454 + 1}
  --           (Cat.Hom.{?u.8451, ?u.8454} X Y) ≟ Subsingleton.{?u.8567 + 1} (Cat.Hom.{?u.8567, ?u.8567} ?m.8569 ?m.8570)

[Scott Morrison]

Just pinging @Mario Carneiro and @Sebastian Ullrich as you were interested in this during the meeting.

[Scott Morrison]

apply Subsingleton.elim works in these cases, with or without etaExperiment, so that can be used as a workaround at least.

[Sebastian Ullrich]

@Scott Morrison Well this is a bit hairy. There is nothing wrong with etaExperiment here fundamentally, it simply makes the unifier make more progress, which has it encounter a universe constraint it would not encounter otherwise and which it cannot solve, bailing out instead.
Basically, with the experiment it tries harder to apply instSubsingletonHomInstCat, eventually testing whether the [Cat C] parameter is defeq to instance (α : Type u) : Cat.{u, u} α. But to check whether they even have the same type, it would have to tell whether [Cat C]'s objects and morphisms are in the same universe, which is unknown at this point, so it refuses to definitely answer whether this instance can be applied and does not try any further instances. Thus [Cat.{u,v] C] is another workaround.

[Scott Morrison]

I'm a bit surprised that "refuses to definitely answer" for one instance causes later instances to be ignored!

[Scott Morrison]

(i.e. shouldn't uncertainty about an instance be treated as a failure, rather than an abort?)

[Sebastian Ullrich]

Preferring more certain instances would change the instance order, it refuses to do that

[Scott Morrison]

I see. In this particular case, we can teach aesop that it is allowed to use Subsingleton.elim directly, so it won't matter that it can't simplify using eq_iff_true_of_subsingleton. But still it's fairly worrying. Add the explicit universe annotations [Cat.{u, v} C] is really not good: I think that's proposing we have to annotate every single instance in the library, because these simp lemmas are firing "unseen" in auto_param proofs, so it's hard to predict where the problems will be...

[Gabriel Ebner]

Some observations: the Cat instance is in an unnecessarily high universe, but this doesn't make a difference. Changing it to Cat.{u,0} causes the same error. ?u =?= 0 is just as stuck as ?u =?= ?v after all (with ?u, ?v nonassignable).

[Gabriel Ebner]

Changing example to theorem xample fixes the error. However, def xample doesn't. That's because theorem fixes the universes levels before elaborating the proof. Maybe we should do that for def/example as well.