structure のダイアモンド継承に関する直観に反する例

/-- 神話生物 -/
structure MythicalCreature where
  large : Bool
deriving Repr

/-- モンスター -/
structure Monster extends MythicalCreature where
  vulnerability : String
deriving Repr

def troll : Monster where
  large := true
  vulnerability := "sunlight"

/-- お助け生物 -/
structure Helper extends MythicalCreature where
  assistance : String
  payment : String
deriving Repr

def nisse : Helper where
  large := false
  assistance := "household tasks"
  payment := "porridge"

/-- お助けモンスター. ダイアモンド継承した -/
structure MonstrousAssistant extends Monster, Helper where
deriving Repr

#check MonstrousAssistant.mk

/-- お助けトロル -/
def domesticatedTroll : MonstrousAssistant where
  large := false
  assistance := "heavy labor"
  payment := "toy goats"
  vulnerability := "sunlight"

#check domesticatedTroll.toMythicalCreature

structure Bird where
  flight : Bool
  -- MythicalCreature と同じフィールド名があると挙動がおかしくなることがある
  -- これ（同名のフィールド）を禁止すべきでは？
  large : Bool
deriving Repr

structure MonstrousBird extends Bird, Monster where
deriving Repr

/-
MonstrousBird.mk (toBird : Bird) (vulnerability : String) : MonstrousBird
-/
#check MonstrousBird.mk

def putera : MonstrousBird := {flight := true, large := true, vulnerability := "みず"}

#check putera.toMonster
#check_failure putera.toMythicalCreature

#print MonstrousAssistant.toHelper

-- self.large が Bird.large からとられていて， おかしそうに見える
-- 不思議
/-
@[reducible] def MonstrousBird.toMonster : MonstrousBird → Monster :=
fun self => { large := self.large, vulnerability := self.vulnerability }
-/
#print MonstrousBird.toMonster

Start by running the Lean examples in the issue and compare the displayed #check and #print output for MonstrousAssistant and MonstrousBird. Determine whether the duplicate large fields and generated projections are intended; done means the behavior is explained or a concrete change to the structure inheritance rules is specified.