Instance search without type

Stream: lean4

[Patrick Massot]

In

class One₁ (α : Type) where
  one : α

class ZeroOne₁ (α : Type) extends One₁ α where
  zero : α

set_option trace.Meta.synthInstance true in
example {α : Type} [ZeroOne₁ α] : α := One₁.one

I get the following trace:

[Meta.synthInstance] 💥 One₁ ?m.33 ▼
  [] new goal One₁ ?m.33 ▼
    [instances] #[@ZeroOne₁.toOne₁]
  [] ✅ apply @ZeroOne₁.toOne₁ to One₁ ?m.33 ▼
    [tryResolve] ✅ One₁ ?m.33 ≟ One₁ ?m.33
    [] new goal ZeroOne₁ ?m.33 ▼
      [instances] #[inst✝]
  [] 💥 apply inst✝ to ZeroOne₁ ?m.33 ▼
    [tryResolve] 💥 ZeroOne₁ ?m.33 ≟ ZeroOne₁ α

[Meta.synthInstance] ✅ One₁ α ▼
  [] new goal One₁ α ▶
  [] ✅ apply @ZeroOne₁.toOne₁ to One₁ α ▶
  [] ✅ apply inst✝ to ZeroOne₁ α ▶
  [resume] propagating ZeroOne₁ α to subgoal ZeroOne₁ α of One₁ α ▶
  [] result ZeroOne₁.toOne₁

I'm baffled by the first try. Is this desired or expected?

[Sebastian Ullrich]

By "try" you mean the entire synthInstance invocation?

[Patrick Massot]

Yes, searching for One₁ ?m.33

[Patrick Massot]

and then failing to solve ZeroOne₁ ?m.33 ≟ ZeroOne₁ α

[Eric Wieser]

Is the idea here that it first tries to work out if it should be solving an outParam?

[Sebastian Ullrich]

No, this is one of I believe Lean 4's lesser-known features: typeclass inference can find instances even if the class type still contains metavariables as long as those mvars do not affect the search. The search is supposed to fail ("explode") relatively quickly like here if an mvar is in the way, but I don't think it is known yet how that plays out in mathlib4 across the board

[Patrick Massot]

Sebastian, I understand this but it does not explain why Lean tries this before trying the search that eventually succeeds in this case. Is that an elaboration order issue?