Zulip Chat Archive

Stream: general

Topic: Dot notation Polymorphism via coercions

Luiz Carlos Rumbelsperger Viana (Dec 21 2020 at 14:18):

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 (Dec 21 2020 at 19:17):

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 ?

Last updated: Dec 20 2023 at 11:08 UTC