Subtleties of type class method argument plicity

Stream: lean4

[David Thrane Christiansen]

I'm trying to discern exactly what causes some type class methods to get different plicities than others, and I have a theory that I'd appreciate confirmation or correction of. I couldn't find a description in TPiL4 or in the manual.

My theory: if a class C has a telescope (x1 : A1) ... (xn : An) at the top, then a method m : B will result in an accessor C.m that takes all xk : Ak arguments to C implicitly if they're mentioned in B, and explicitly if they are not, prior to the instance implicit [self : C x1 ... xn].

This seems to make sense to me, because the arguments that are not mentioned in m's type will not generally be solvable via unification, while those that are probably will be. This also matches some observations:

#check @OfNat.ofNat -- @OfNat.ofNat : {α : Type u_1} → (x : Nat) → [self : OfNat α x] → α

class A (α : Type u) (b : Nat) where
  a : α

#check @A.a -- @A.a : {α : Type u_1} → (b : Nat) → [self : A α b] → α

class B (α : Type u) (b : Nat) (β : Type v) where
  b : α

#check @B.b -- @B.b : {α : Type u_1} → (b : Nat) → (β : Type u_2) → [self : B α b β] → α

class C (α : Type u) (b : Nat) (β : Type v) where
  c : α → β

#check @C.c -- @C.c : {α : Type u_1} → (b : Nat) → {β : Type u_2} → [self : C α b β] → α → β