regression: typeclass synthesis in structure definitions

Stream: lean4

[Julien Marquet-Wagner]

I have these definitions that work in v4.08.0 but not in v4.19.0 and above.
v4.08.0 accepts the following, but v4.19.0 reports it failed to synthesize the appropriate HMul instances.

structure PointedMagma where
  α : Type
  one : α
  mul : α → α → α

instance : CoeSort PointedMagma Type where
  coe := PointedMagma.α

instance (M : PointedMagma) : OfNat M (nat_lit 1) where
  ofNat := M.one

instance (M : PointedMagma) : Mul M where
  mul := M.mul

/- this is where the problem is -/
structure Group extends PointedMagma where
  one_mul : ∀ a : α, 1 * a = a
  mul_one : ∀ a : α, a * 1 = a
  assoc : ∀ a b c : α, (a * b) * c = a * (b * c)

---

another example in the same vein

class Hom (α : Type) (β : Type) where
  hom : α → β → Type

infixr:10 " ⟶ " => Hom.hom

structure Quiver where
  obj : Type
  hom : obj → obj → Type

instance : CoeSort Quiver Type where
  coe := Quiver.obj

instance (Q : Quiver) : Hom Q Q where
  hom := Q.hom

/- same problem here -/
structure CategoryStruct extends Quiver where
  id : (a : obj) → a ⟶ a
  comp : {a b c : obj} → (a ⟶ b) → (b ⟶ c) → (a ⟶ c)

[Julien Marquet-Wagner]

I've tried this on old nightlies:

• works on nightly-2025-03-22
• breaks on nightly-2025-03-24

I guess this points to lean4#7302.

[Floris van Doorn]

(cc @Kyle Miller )

[Kyle Miller]

Thanks for the report @Julien Marquet-Wagner.

The proximal cause for this difference in behavior is that the structure command used to construct a local context of the form

toPointedMagma : PointedMagma
α : Type := toPointedMagma.α
one : toPointedMagma.α := toPointedMagma.one
mul : toPointedMagma.α → toPointedMagma.α → toPointedMagma.α := toPointedMagma.mul

but now the relationship between parent projections and fields has been inverted:

α : Type
one : α
mul : α → α → α
toPointedMagma : PointedMagma := { α := α, one := one, mul := mul }

The motivation for this change is that the first sort of local context was a source of continuing issues, and it was hard to make sure that during elaboration all parents were treated equally.

[Kyle Miller]

That your first example ever worked at all is fairly delicate. For example, you should find that the following modification would break it on v4.08.0:

structure Carrier where
  α : Type

structure Group extends Carrier, PointedMagma where
  one_mul : ∀ a : α, 1 * a = a
  mul_one : ∀ a : α, a * 1 = a
  assoc : ∀ a b c : α, (a * b) * c = a * (b * c)

So, how did elaboration succeed before?

• The elaborated type of the Mul instance is (M : PointedMagma) -> Mul M.α
• In one_mul, when you have a : α, by definition this is a : toPointedMagma.α, and so it can pick up on this Mul instance due to having the right form.

The reason the Carrier parent breaks this scheme is that the new local context is

toCarrier : Carrier
α : Type := toCarrier.α
one : α
mul : α → α → α

and so now we have a : toCarrier.α, which is not of the right form for picking up the Mul instance.

[Kyle Miller]

I understand that this is a regression for you, which I am sorry about. There are some features that I added in with lean4#7302 that help with some instances of this, but I can't get them to work here. (See this comment.)

[Kyle Miller]

I'd like to get structures-with-carriers to work somehow. One idea that came up before, for another extends problem, is having a way to mark instances so that they get automatically added to the local context (for example, marking the Mul instance so that it gets transformed and added as a local instance).

An idea that just came to mind is adding local unification hints like

unif_hint (α : Type) (p : PointedMagma) where
  p =?= { α, one := ???, mul := ??? : PointedMagma }
  ⊢ α =?= p.α

where each ??? is filled in with the corresponding field in the local context.

[Kyle Miller]

The recommended way to work with algebraic structures is as "unbundled" classes, like so.

class PointedMagma (α : Type) where
  one : α
  mul : α → α → α

instance {α : Type} [PointedMagma α] : OfNat α (nat_lit 1) where
  ofNat := PointedMagma.one

instance {α : Type} [PointedMagma α] : Mul α where
  mul := PointedMagma.mul

class Group (α : Type) extends PointedMagma α where
  one_mul : ∀ a : α, 1 * a = a
  mul_one : ∀ a : α, a * 1 = a
  assoc : ∀ a b c : α, (a * b) * c = a * (b * c)

Then you can create "bundled" versions, and if you add a CoeSort instance and mark the instance field as being an instance using attribute, then you get a relatively seamless experience between bundled and unbundled points of view.

structure BundledGroup where
  α : Type
  [inst : Group α]

attribute [instance] BundledGroup.inst

instance : CoeSort BundledGroup Type where
  coe := BundledGroup.α

Example: proving a theorem using the Group laws:

example (G : BundledGroup) (x : G) : 1 * x * 1 = x := by
  rw [Group.one_mul, Group.mul_one]

Example: creating a bundled group from a Group:

instance : Group Nat where
  one := 0
  mul := Nat.add
  one_mul := Nat.zero_add
  mul_one := Nat.add_zero
  assoc := Nat.add_assoc

example : BundledGroup := BundledGroup.mk Nat

[Kyle Miller]

I've been kicking around the idea of adding a Rocq-like feature where you could mark α as being the carrier using some sort of syntax, and it would automatically construct the CoeSort instance for you. Perhaps this is how one indicates which field should participate in the local unification hint scheme?

There's also been an idea of somehow making it easier to go back and forth between the bundled and unbundled versions, without needing to write any boilerplate. For example, one could imagine something where

structure PointedMagma where
  carrier α : Type
  one : α
  mul : α → α → α

would actually define something like

class PointedMagma (α : Type) where
  one : α
  mul : α → α → α
structure BundledPointedMagma where
  α : Type
  [instPointedMagma : PointedMagma α]
attribute [instance] BundledPointedMagma.instPointedMagma
instance : CoeSort BundledPointedMagma Type where
  coe := BundledPointedMagma.α

and then an elaborator feature could have (M : PointedMagma) magically be interpreted as (M : BundledPointedMagma). (I tried simulating this with CoeDep, but that doesn't appear to work without explicit ascriptions like (PointedMagma : Type 1).)

[Julien Marquet-Wagner]

Thanks for the very detailed answer, @Kyle Miller :)