Unknown constant and invalid field notation

Stream: mathlib4

[Ashley Blacquiere]

Shouldn't the two checks on Group.mul produce something other than an error here? I know #check Mul.mul g h works in this case, but shouldn't .mul be accessible on Group as well?

import Mathlib

variable {G : Type*} [Group G]
variable (g h : G)

#check g * h -- g * h : G
#check Group.mul g h -- unknown constant 'Group.mul'
#check @Group.mul g h -- invalid use of field notation with '@' modifier

[Kyle Miller]

That's odd, you have to do #check Group.toDivInvMonoid.mul g h

[Ashley Blacquiere]

Huh. Ya, that does work. Interestingly #check DivInvMonoid.mul g h also returns 'unknown constant'.

[Kyle Miller]

If you can make a mathlib-free mwe that would be helpful for creating a Lean issue for this, but if not I'll get around to doing it eventually.

[Ashley Blacquiere]

Something like this?

class A (α : Type) where
  a : α → α

class B (β : Type) extends A β where
  b : β → β

instance : B Nat where
  a := Nat.succ
  b := Nat.pred

variable {X : Type} [B X]
variable (x : X)

#check B.b x -- B.b x : X
#check B.a x -- unknown constant 'B.a'
#check @B.a -- invalid use of field notation with '@' modifier
#check A.a x -- A.a x : X

I guess B.a x shouldn't really type check, so I should get a "failed to synthesize instance" error, correct?