Field missing on diamond-shaped instances

jthulhu commented 2 weeks ago

Prerequisites

Please put an X between the brackets as you perform the following steps:

[X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
[X] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

In the following example

class A

class B extends A where
  b : Unit

class C extends A, B

instance : A where

instance : B where
  b := ()

instance : C where

The last line produces an error fields missing: 'b'. If, instead, I change the order of the inherited classes of C, as such

class C extends B, A

then it works.

Versions

Tried both on my computer (Lean 4.12.0 on NixOS/nixpkgs unstable) and on live.lean-lang.org.

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

Kha commented 1 week ago

Do you have a practical example? Deriving from A multiple times isn't very, and one wonders if that should even be allowed.

jthulhu commented 1 week ago

Deriving from A multiple times indirectly seems very useful to me, to encode mathematical structure. A common pattern could be "A Foo is an algbera over this signature. A Foo is said to be potatoe-like if .... A Foo is said to be carrot-like if .... A Foo is said to be complete if it is both potatoe-like and carrot-like, and ...." This would be encoded as

class Foo where ...
class Potatoe extends Foo where ...
class Carrot extends Foo where ...
class Complete extends Potatoe, Carrot where ...

If you refer to deriving from A both directly and indirectly (ie. exactly the example I gave), then I agree it is less clear that this might be practically useful, as, in my example, one could simply remove the direct inheritance from C to A in the definition of C, and still refer to the fields of A in those of C, because they are available through B.

The case where it might still makes sense to have this duplicate dependency is in cases where B and C have an abstraction boundary between them, and C does not know that B extends A (this could be the case because B doesn't want removing A to be a breaking change, so they don't include the fact that they inherit from A in their declared interface).

kmill commented 1 week ago

Having discretionary parents is fine and supported(). One problem here is that A should* come after B, since with the current order, name resolution will visit A before B even though A is a parent of B. You can check this using set_option structure.strictResolutionOrder true, where it complains about the order of the parents

class C extends A, B
/-
failed to compute strict resolution order:
- parent 'A' must come after parent 'B'
-/

This is not the underlying problem for this issue however. Instead, it's that structure instance elaboration currently only looks for instances to fill in fields for parents that are represented as "subobjects". Supporting non-subobject parents is planned, and I'll use this issue to track the feature. Here's an an artificial example that doesn't have the strictResolutionOrder failure:

class A where
  a : Unit

class B where
  a : Unit

class C extends A, B
class C' extends B, A

instance : B where
  a := ()

instance : C where -- fields missing: 'a'

instance : C' where -- succeeds

(*) @Kha We want this because there exist class hierarchies that need them to be able to deduce strict resolution orders.

leanprover / lean4