Bad error message when tactic for filling default field value fails

[leodemoura]

structure Foo where
  val : String
  len : Nat := val.length
  inv : val.length = len := by decide

def test2 : Foo := { -- The error message just says "failed to reduce to 'true'\n  false"
  val := "abc"
  len := 5
}

The error should say that Lean failed to initialize field inv using the specified tactic.

[girving]

I hit this just now. Here's a Zulip discussion with an in-the-wild example, and another (not fully) minimized test case:

variable {α : Type}

class Yop (α : Type) where
  yop : α → α

class Nop (α : Type) [Yop α] where
  nop : ∀ x : α, Yop.yop x = x := by intro; rfl

structure A where
  x : Nat

instance : Yop A where
  yop a := ⟨a.x + 1⟩

instance : Nop A where
  -- `nop` is not defined, but the error message does not mention `nop`:
  --   tactic 'rfl' failed, equality lhs
  --     Yop.yop x✝
  --   is not definitionally equal to rhs
  --     x✝
  --   α: Type
  --   x✝: A
  --   ⊢ Yop.yop x✝ = x✝

[mattrobball]

This comes up quite often, eg when using aesop as an autoparam.