Confusing error message for type class resolution failures

Description

New users who work in Lean may reasonably write:

def add1 x := x + 1

which is accepted due to the default instance for OfNat 1 Nat.

But if they then also reasonably write

def times x y := x * y

they get this message:

typeclass instance problem is stuck, it is often due to metavariables
  HMul ?m.5498 (?m.5486 x) (?m.5487 x y)

This is not particularly actionable, and it's quite intimidating (what's a metavariable? what's a type class? What's that big number next to the question mark for? What in the world is HMul?). In classroom settings, failures to find Num instances is a common source of difficulty for students learning Haskell, so there is good reason to think that this will be an issue for Lean learners too.

Versions

Lean (version 4.3.0, commit 734ce1ef2f62, Release)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the two Lean definitions from the issue and inspect where the typeclass-resolution failure is reported. The work is done when the failure is communicated in an actionable way for new Lean users without the current intimidating metavariable and HMul details.