Automatically provide implicit coercions for inheritance

Stream: general

[Marvin]

Here shows you can emulate hierarchical inheritance modeling using structure B extends A

structure Element where
  position : Int × Int
structure Canvas extends Element

which to my understanding is syntax sugar for composition going on under the hood.

When practically working with inheritance, we want liskov-substitution to work -- passing a Canvas to functions that expect an Element

def f(_ : Element) := ()

axiom c : Canvas
def y := f c
--          ^ error
-- application type mismatch f c
-- argument c has type Canvas : Type
-- but is expected to have type Element : Type

Of course the reality in Lean is that c is only a Canvas and not an Element, but a method to explicitly convert is provided built-in that we can use.

def y := f c.toElement

it works, but is clunky and tedious.

We can create an implicit coercion to make this feel natural again.

instance : Coe Canvas Element where
  coe := Canvas.toElement

def y := f c -- works

The problem is that you must manually create this boilerplate for every scenario like this.

Since the language already wants to let developers act as if inheritance is a somewhat supported feature with the extends syntax sugar, and since it already set as a precedent for causing certain functionality like .toElement to be included free of any manual labor from developers, I would like to propose that we also provide the instance : Coe Canvas Element where coe := Canvas.toElement declaration to be available implicitly, no manual ceremony beyond writing extends.

Is this technically feasible to implement? Looking forward to hearing feedback, thanks!

[Kim Morrison]

Have you tried this out in practice? For example start writing these instances in Mathlib and tell us how badly it goes. :-)

[Marvin]

I'm quite new to the language so I admit I'm not sure how this would interact across all the use cases. Is it just ambiguity and reasoning about code difficulties you're talking about, or maybe implicit look up conflicts in the compiler when multiple instances exist? Why would this go badly? I'm not doubting you, I'd like to learn more so I don't make messes in my own projects.