Prerequisites
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))) := rflExpected 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.
Prerequisites
Description
It's possible to make the following happen:
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.
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 typeStarRing' RReproduces 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.04Additional Information
The issue shows up here and here in the mathlib port. Reported here on Zulip.