Instance synthesis (almost) infinite recursion

Stream: lean4

[Christian Merten]

Consider the following MWE:

class Foo (X : Type) : Prop where

set_option trace.Meta.synthInstance true

example {X Y : Type} [inst : Foo Y]
    (h : ∀ {X Y : Type} [Foo Y], 3 = 3 → Foo X) (hY : ¬3 = 3) : Foo X := by
  have : Foo Y := inferInstance
  sorry

This succeeds, but if you look at the synthInstance trace, you can see that it first tries to repetively use h to deduce Foo Y. After going on for hundreds of iterations, the trace finally get smaller again and it backtracks until eventually using inst.

This appeared while looking at (the non Mathlib-free)

import Mathlib.Tactic.WLOG

class Foo (X : Type) : Prop where

set_option trace.Meta.synthInstance true

example {X Y : Type} [Foo Y] : Foo X := by
  wlog hY : 3 = 3
  · /-
    X Y : Type
    inst✝ : Foo Y
    this : ∀ {X Y : Type} [inst : Foo Y], 3 = 3 → Foo X
    hY : ¬3 = 3
    ⊢ Foo X
    -/
    have : Foo Y := inferInstance
    sorry
  sorry

where the same phenomenon arises, but now the instance search times out. I strongly suspect this has nothing to do with wlog, but I couldn't get the first example to fail without it. The latter example can be fixed with set_option synthInstance.maxSize 50.

I assume instance search is depth first. Is there a way to prevent this from happening?

[Daniel Weber]

Note that instance : ∀ {X Y : Type} [Foo Y], 3 = 3 → Foo X := sorry is a bad instance, because there's no valid synthesization order. Perhaps a similar check could be done before using local parameters in typeclass search

[Andrew Yang]

Let me guess: wlog is missing some withMainContext

[Christian Merten]

Andrew Yang said:

Let me guess: wlog is missing some withMainContext

Not sure, because if we make the goal a bit worse, it also fails without wlog:

class Foo (X : Type) : Prop where

set_option trace.Meta.synthInstance true

example {X Y : Type} [inst : Foo Y]
    (h : ∀ {X Y : Type} [Foo Y], 3 = 3 → Foo Y → Foo Y → Foo Y → Foo Y → Foo Y → Foo Y → Foo Y → Foo X)
    (hY : ¬3 = 3) : Foo X := by
  have : Foo Y := inferInstance
  sorry