Multiple inheritance/namespace resolution question

Stream: lean4

[Brendan Seamas Murphy]

Here is a toy example that demonstrates a thing I'm confused by:

structure X where
  base : Nat

structure A extends X where
  countA : Nat

structure B extends X where
  countB : Nat

namespace A

def getTwiceCountA (a : A) := a.countA * 2

end A

namespace B

def getTwiceCountB (b : B) := b.countB * 2

end B

structure C extends A, B

def getCounts (c : C) :=
  c.countA + c.countB

def getTwiceCounts (c : C) :=
  c.getTwiceCountA + c.getTwiceCountB

Why does getCounts work but getTwiceCounts does not?

[Brendan Seamas Murphy]

Note that this does work:

structure A where
  countA : Nat

structure B where
  countB : Nat

namespace A

def getTwiceCountA (a : A) := a.countA * 2

end A

namespace B

def getTwiceCountB (b : B) := b.countB * 2

end B

structure C extends A, B

def getCounts (c : C) :=
  c.countA + c.countB

def getTwiceCounts (c : C) :=
  c.getTwiceCountA + c.getTwiceCountB

[Kyle Miller]

It looks like it's because docs#Lean.Elab.Term.findMethod? uses docs#Lean.getParentStructures, which only returns parent structures that correspond to subobject fields.

The shared X causes only A to have a toA field; B is only represented by the countB field:

#check C.mk
-- C.mk (toA : A) (countB : ℕ) : C

I think this is a bug. Could you report it?

[Brendan Seamas Murphy]

Yeah, will do

[Brendan Seamas Murphy]

It's Lean.Elab.App.findMethod? btw

[Brendan Seamas Murphy]

https://github.com/leanprover/lean4/issues/3467