typeclass inference failure

[kbuzzard]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

An incomprehensible (to me) typeclass inference failure.

Context

The issue presented here has been minimised from an occurrence in the wild in mathlib. The Zulip discussion is here

Steps to Reproduce

class Zero (α : Type) where
  zero : α

class AddCommGroup (α : Type) extends Zero α where

class Ring (α : Type) extends Zero α, AddCommGroup α

class Module (R : Type) (M : Type) [Zero R] [Zero M] where

instance (R : Type) [Zero R] : Module R R := ⟨⟩

structure Submodule (R : Type) (M : Type) [Zero R] [Zero M] [Module R M] : Type where

class HasQuotient (A : outParam <| Type) (B : Type) where
  quotient' : B → Type

instance Submodule.hasQuotient {R : Type} {M : Type} [Ring R] [AddCommGroup M]
  [Module R M]: HasQuotient M (Submodule R M) := ⟨fun _ => M⟩

def Synonym (M : Type) [Zero M] := M

instance Synonym.zero {G : Type} [Zero G] : Zero (Synonym G) := ⟨(Zero.zero : G)⟩

instance Synonym.addCommGroup {G : Type} [AddCommGroup G] : AddCommGroup (Synonym G) :=
  { Synonym.zero with }

instance Synonym.module (M : Type) {R : Type} [Zero R] [Zero M] [Module R M] :
    Module R (Synonym M) := { }

variable (R : Type) [Ring R]

-- set_option trace.Meta.synthInstance true in
#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- fails

-- the trace indicates that this is the instance which typeclass inference gives up on,
-- but it's easily found
noncomputable instance : AddCommGroup (Synonym R) := inferInstance

-- and now the original `#synth` works fine
#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- works

The relevant part of the failing trace is

[Meta.synthInstance] ❌ HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) ▼
  [] new goal HasQuotient _tc.0 (Submodule R (Synonym (Synonym R))) ▶
  [] ❌ apply @Submodule.hasQuotient to HasQuotient ?m.647 (Submodule R (Synonym (Synonym R))) ▼
    [tryResolve] ❌ HasQuotient ?m.647 (Submodule R (Synonym (Synonym R))) ≟ HasQuotient ?m.650 (Submodule ?m.649 ?m.650) ▼
      [] ✅ Ring R ▶
      [] ❌ AddCommGroup (Synonym (Synonym R)) ▼
        [] new goal AddCommGroup (Synonym (Synonym R)) ▶
        [] ❌ apply @Synonym.addCommGroup to AddCommGroup (Synonym (Synonym R)) ▼
          [tryResolve] ❌ AddCommGroup (Synonym (Synonym R)) ≟ AddCommGroup (Synonym ?m.663) ▼
            [] ❌ AddCommGroup (Synonym R) ▼
              [] new goal AddCommGroup (Synonym R) ▶
              [] ❌ apply @Synonym.addCommGroup to AddCommGroup (Synonym R) ▼
                [tryResolve] ❌ AddCommGroup (Synonym R) ≟ AddCommGroup (Synonym ?m.667)

and the last line is the mystery: I don't know how to get tryResolve to tell me why it's failing to let ?m.667 be R.

Expected behavior:

The first #synth works.

Actual behavior: [Clear and concise description of what actually happens]

The first #synth fails, but starts to work again once I add the shortcut instance explicitly.

Versions

Lean (version 4.6.0-rc1, x86_64-unknown-linux-gnu, commit 5cc0c3f145ff, Release)

[OS version]

Ubuntu 22.04

Additional Information

There has been more discussion on the Zulip thread since I opened this issue, which may be of some use (in particular some fingers are being pointed at discrimination trees, but I'm not competent enough to know if this is a red herring or not).

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[kim-em]

Is this synthPendingDepth, as in #3927?

[kbuzzard]

(just to clarify: the fix now is to add set_option maxSynthPendingDepth 2 in before the failing declaration)

[kmill]

As of #5920, this set_option maxSynthPendingDepth 2 fix is no longer necessary (at least according to the test case in lean/run/3313.lean).