typeclass inference failure

[kbuzzard]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

It's possible to make the following happen:

theorem starGizmo_foo [CommRing R] [StarRing' R] (x : R) : starGizmo x = x := rfl
-- error: failed to synthesize instance
--  StarRing' R

even though the instance is right there in the local context. This is very confusing for users and is showing up in the mathlib port.

Steps to Reproduce

Here's a MWE with some debugging output. The classes are just stripped from mathlib.

class NonUnitalNonAssocSemiring (α : Type u)

class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α

class Semiring (α : Type u) extends NonUnitalSemiring α

class NonUnitalCommSemiring (α : Type u) extends NonUnitalSemiring α

class CommSemiring (R : Type u) extends Semiring R

class NonUnitalNonAssocRing (α : Type u) extends NonUnitalNonAssocSemiring α

class NonUnitalRing (α : Type _) extends NonUnitalNonAssocRing α, NonUnitalSemiring α

class Ring (R : Type u) extends Semiring R

class NonUnitalCommRing (α : Type u) extends NonUnitalRing α

class CommRing (α : Type u) extends Ring α

instance (priority := 100) NonUnitalCommRing.toNonUnitalCommSemiring [s : NonUnitalCommRing α] :
    NonUnitalCommSemiring α :=
  { s with }

instance (priority := 100) CommRing.toCommSemiring [s : CommRing α] : CommSemiring α :=
  { s with }

instance (priority := 100) CommSemiring.toNonUnitalCommSemiring [s : CommSemiring α] :
    NonUnitalCommSemiring α :=
  { s with }

instance (priority := 100) CommRing.toNonUnitalCommRing [s : CommRing α] : NonUnitalCommRing α :=
  { s with }

-- Two routes from CommRing to NonUnitalSemiring:
-- 1 : via CommSemiring -> NonUnitalCommSemiring
-- 2 : via NonUnitalCommRing -> NonUnitalRing

class StarRing' (R : Type _) [NonUnitalSemiring R]
def starGizmo [CommSemiring R] [StarRing' R] : R → R := id
theorem starGizmo_foo [CommRing R] [StarRing' R] (x : R) : starGizmo x = x := rfl
-- error: failed to synthesize instance
--  StarRing' R

/-

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

[Meta.synthInstance] ❌ @StarRing' R
      (@NonUnitalCommSemiring.toNonUnitalSemiring R
        (@CommSemiring.toNonUnitalCommSemiring R (@CommRing.toCommSemiring R inst✝¹))) ▼
  [] new goal @StarRing' R
        (@NonUnitalCommSemiring.toNonUnitalSemiring R
          (@CommSemiring.toNonUnitalCommSemiring R (@CommRing.toCommSemiring R inst✝¹))) ▶
  [] ❌ apply inst✝ to @StarRing' R
        (@NonUnitalCommSemiring.toNonUnitalSemiring R
          (@CommSemiring.toNonUnitalCommSemiring R (@CommRing.toCommSemiring R inst✝¹))) ▼
    [tryResolve] ❌ @StarRing' R
          (@NonUnitalCommSemiring.toNonUnitalSemiring R
            (@CommSemiring.toNonUnitalCommSemiring R
              (@CommRing.toCommSemiring R
                inst✝¹))) ≟ @StarRing' R
          (@NonUnitalRing.toNonUnitalSemiring R
            (@NonUnitalCommRing.toNonUnitalRing R (@CommRing.toNonUnitalCommRing R inst✝¹)))
-/

example (inst : CommRing R) : @StarRing' R
          (@NonUnitalCommSemiring.toNonUnitalSemiring R
            (@CommSemiring.toNonUnitalCommSemiring R
              (@CommRing.toCommSemiring R
                inst))) = @StarRing' R
          (@NonUnitalRing.toNonUnitalSemiring R
            (@NonUnitalCommRing.toNonUnitalRing R (@CommRing.toNonUnitalCommRing R inst))) := rfl

Expected behavior: [What you expect to happen]

I would not expect the error.

Actual behavior: [What actually happens]

Looking at the logs, it seems that the [tryResolve] line is failing to unify two defeq terms of type StarRing' R

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

Lean (version 4.0.0-nightly-2023-01-29, commit 38a0d1e3733e, Release) on Ubuntu 22.04

Additional Information

The issue shows up here and here in the mathlib port. Reported here on Zulip.

[eric-wieser]

A likely related issue appears here on Zulip, where

example {α} [Ring α] : Module α α := inferInstance

fails to work in mathlib4.

[rwbarton]

I know you're not going to like this, but this is actually currently working as designed.
The path through CommSemiring -> NonUnitalCommSemiring consists of projections to the first parent class. That is, the instance looks like inst✝.1.1.1, where inst✝ : CommRing R is our original instance.
The other path is an application of CommSemiring.toNonUnitalCommSemiring, which means it is an application of the constructor for NonUnitalCommSemiring. (Basically, it looks like NonUnitalCommSemiring.mk inst✝.1.1.1.1 ....)
Since eta for classes is disabled during instance synthesis, that means the two paths are not definitionally equal. (It says "disable eta for structures that are not classes", but it really means "enable eta only for structures that are not classes".)

[eric-wieser]

That is actually what I expected the problem was when I've mentioned this being a "new-style-structure problem"; the same issue would occur in Lean3 with new-style structures, but doesn't occur with old-style structures as every base class unfolds to a constructor rather than a projection. I think I had hoped that structure eta made this not matter.

So I think we either need to work out a way to make structure eta apply here, or we need to use old-style structures in mathlib4 (either via custom syntax we build ourselves, or by writing every base class instance manually.

[rwbarton]

Here is a version of the issue that only uses extends, and with easier to understand class names.

class A (α : Type u)

class B (α : Type u) extends A α

class C (α : Type u) extends B α

class D (α : Type u) extends B α

class E (α : Type u) extends C α, D α

class F (α : Type u) extends A α

class G (α : Type u) extends F α, B α

class H (α : Type u) extends C α

class I (α : Type u) extends G α, D α

class J (α : Type u) extends H α, I α, E α

class StarRing' (R : Type 0) [B R]
def starGizmo [E R] [StarRing' R] : R → R := id

set_option pp.explicit true in
theorem starGizmo_foo [J R] [StarRing' R] (x : R) : starGizmo x = x := rfl

-- theorem T (i : J R) : (@D.toB.{0} R (@E.toD.{0} R (@J.toE.{0} R i))) = i.toB := rfl

[gebner]

@rwbarton Thank you for the thorough debugging. #2093

[gebner]

I had to revert 15a045e for now. We can apply that commit again after we have adopted a solution to #1986, #2055, and co.

[gebner]

#2003 didn't completely solve the performance issues uncovered by #2103. Please expect some further delays here.

[eric-wieser]

Can we re-enable this fix behind a set_option command, so that in the meantime we can diagnose whether inference failures would be fixed by this or are something else?

[gebner]

Can we re-enable this fix behind a set_option command, so that in the meantime we can diagnose whether inference failures would be fixed by this or are something else?

set_option synthInstance.etaExperiment true. Please only use for testing.

[eric-wieser]

Thanks! That was adcca17 I assume.

[semorrison]

This can now be closed, as #2210 has been merged.