Dot notation Polymorphism via coercions

Stream: general

[Luiz Carlos Rumbelsperger Viana]

Someone might have asked this before but I couldn't quite find it, so here it goes.
Consider the following:

structure A :=
    (n : ℕ)

def A.next (x : A) := x.n + 1

structure B extends A :=
  (m : ℕ)

def my_B : B := { n := 1, m := 1 }

instance B_has_coe : has_coe B A := ⟨B.to_A⟩

#check my_B.to_A.next   -- works regardless of coe
#check A.next my_B          -- works because of coe
#check my_B.next              -- doesn't work at all

#print lean.version -- (3, 21, 0)

Couldn't the last #check be made to work so we could have dot notation polymorphism?

[Mario Carneiro]

the to_A insertion when you use a sub-structure is actually completely separate from coercion. It would actually be pretty hard to use coercion because elaboration of dot notation happens really early, during name resolution, before we have all the typing information and certainly before we have solved any typeclass problems like has_coe B ?