Synthesization order

Stream: lean4

[Peter Nelson]

What is wrong with this?

import Mathlib.Tactic

class P1 (n : ℕ) : Prop where
  (p : 37 < n)

class P2 (m n : ℕ) : Prop where
  (p : 37 < n)
  (q : n < m)

instance foo (m n : ℕ) [h : P2 m n] : P1 n :=
  ⟨h.p⟩

/-
cannot find synthesization order for instance foo with type
  ∀ (m n : ℕ) [h : P2 m n], P1 n
all remaining arguments have metavariables:
  P2 ?m n
  -/

foo works fine as a theorem, but can't be an instance apparently. What is the reason typeclass search can't find something like that?

[Kyle Miller]

I think it would work if m were an out_param on P2. The problem is that you need to figure out a value of m from n somehow in the foo instance, and P2 does not determine m from n.