Default values lost for structure fields with types dependent on parent structures

[ghost]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

variable (α : Type _)

-- First example
structure A extends LE α where
  foo : True
structure B extends LE α where
  bar : ∀ a b : α, a ≤ b → True
structure C extends A α, B α

structure D extends C α where
  foo := trivial
structure E extends C α where
  bar _ _ _ := trivial

-- Works
example : D α where
  le := Eq
  bar _ _ _ := trivial
-- Doesn't work without specifying bar
example : E α where
  le := Eq
  foo := trivial
  -- bar _ _ _ := trivial

-- Second example
structure X where
  transform : α → α

structure A₁ extends X α where
  foo : True
structure B₁ extends X α where
  bar : ∀ a, transform a = transform (transform a) → True
structure C₁ extends A₁ α, B₁ α

structure D₁ extends C₁ α where
  foo := trivial
structure E₁ extends C₁ α where
  bar _ _ := trivial

example : D₁ α where
  transform := id
  bar := fun _ _ => trivial
example : E₁ α where
  transform := id
  foo := trivial
  -- bar _ _ := trivial

Expected behavior: the bar field is filled with the default supplied in the definition of E. However, it is not.

Reproduces how often: 100%

Versions

nightly-2023-04-07 (commit 9aeae67)

Additional Information

This seems to be related to the fact that the type of bar depends on LE α/X α.
In fact, in my original code involving Preorder α rather than LE α (which I was not able to reduce to a reproducible small test case), constructing the Preorder instance first with have : Preorder α := { ... }; { ... } allowed the field to be inferred.

[kmill]

Minimized further:

structure A (α : Type u) where
  p : Prop
  bar : p → True

structure B (α : Type _) extends A α where
  bar _ := trivial

-- Doesn't work without specifying bar
example : B α where
  p := False

I don't know if this represents the entire issue yet.