Unhelpful error message in case of a missing typeclass

[urkud]

Sometimes I get errors like

/mathlib/src/data/set/intervals/disjoint.lean:36:14: error: type mismatch at application
  not_le.mpr hx.left.right
term
  hx.left.right
has type
  x < b
but is expected to have type
  ?m_3 < ?m_4

The actual reason is a missing typeclass instance (I moved the code from decidable_linear_order to preorder and did not replace not_le.2 with not_le_of_lt yet).

The error message does not help a user to understand the source of the problem. When I see it, my first impression is "there is a bug in Lean because surely x < b matches ?m_3 < ?m_4".