Confusing error message for type class resolution failures

[david-christiansen]

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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[grindingpeon]

I am curious to how you would debug such an statement, @david-christiansen. I am a newcomer to lean and getting this exact error at the moment (and it confuses me :smile:)

The error turns up here:

(I am doing some math from this course)

[david-christiansen]

The error happens when Lean hasn't gotten enough type information to figure out which instance of a type class to use. This can usually be worked out by adding a type annotation somewhere - probably one of the arguments of the operation or lemma at which the error occurs.

[grindingpeon]

Thank you very much for the answer. I guess I will have to do some digging on type classes :smiley:

[semorrison]

It does seem like this error message could usefully contain a user-actionable sentence, e.g. "Specifying more arguments to a function or operation, or providing the expected type, may resolve this problem."