type class inference fails at unification?

Stream: mathlib4

[Jireh Loreaux]

In porting RingTheory.Ideal.Basic I ran into this issue with typeclass inference. It's not a problem with new structures because Semiring.toModule works. It seems like Lean sets up a trivial unification problem for itself and then fails to solve it. I don't understand any further than this.

@Gabriel Ebner I tried to make a non-mathlib mwe but couldn't get it to reproduce.

import Mathlib.Algebra.Module.Basic

-- note: priority of `Semiring.toModule` is set
-- to 910 because it always applies
example [Ring R] : Module R R := Semiring.toModule -- succeeds

set_option trace.Meta.synthInstance true

example [Ring R] : Module R R := inferInstance -- fails

/-
[Meta.synthInstance] ❌ Module R R ▼
  [] new goal Module R R ▶
  [] ❌ apply @Semiring.toModule to Module R R ▼
    [tryResolve] ❌ Module R R ≟ Module ?m.888 ?m.888
-/

example [Semiring R] : Module R R := inferInstance -- succeeds

attempted MWE

class Foo (R : Type _) where
  X : Nat

class SuperFoo (R : Type _) where
  Y : Nat

instance (priority := 200) SuperFoo.toFoo [SuperFoo R] : Foo R where
  X := @SuperFoo.Y R _

class Bar (R : Type _) where
  Z : Nat

instance Foo.toBar [Foo R] : Bar R where
  Z := @Foo.X R _

class Baz (R S : Type _) [Foo R] [Bar R] where
  U : Nat
  V : Nat

instance (priority := 910) Foo.toBaz [Foo R] : Baz R R where
  U := @Foo.X R _
  V := @Foo.X R _

example [Foo R] : Baz R R := inferInstance
example [SuperFoo R] : Baz R R := inferInstance -- succeeds, so doesn't reproduce the problem.

[Eric Wieser]

This looks like exactly lean4#2074 to me

[Eric Wieser]

Which _is_ a problem with new structures, it's the ones in the implicit arguments that you can't see

[Jireh Loreaux]

Then why does it succeed with Semiring.toModule without any extra help?

[Eric Wieser]

Because unification uses structure eta but TC search doesn't

[Eric Wieser]

And structure eta is needed to make new-style structures behave

[Arien Malec]

Is this the same issue as my https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Default.20HSMul.20for.20!4.232212/near/327415103 ?

[Jireh Loreaux]

Ah, so is the point that when I call Semiring.toModule the implicit arguments get filled via unification and that resolves the issue with structure eta, and then the remaining type class inference succeeds because it doesn't have metavariables?

[Eric Wieser]

That sounds right to me

[Eric Wieser]

From the github issue, we had precisely this example before at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Algebra.2EPeriodic.20!4.231963/near/325949252

[Eric Wieser]

So far the approach is basically "pretend that NonAssocRing doesn't exist (by deinstancing it) and wait for a fix upstream in Lean"

[Eric Wieser]

Searching for porting note referencing 2074 should find examples of the former

[Jireh Loreaux]

sorry, I should have checked lean4#2074, but I had convinced myself it wasn't structure eta for the (incorrect) reasons above.