Why failing to unify?

Stream: new members

[Martin C. Martin]

import Mathlib.Algebra.Field.Basic

example {F : Type _} [Field F]  : ∀ x : (ℕ → F), (1 : F) • x = x := by
  intro b
  apply one_smul

fails with:

tactic 'apply' failed, failed to unify
  1 • ?b = ?b
with
  1 • b = b

Looks easy to unify to me...

[Martin C. Martin]

Another clue, when I explicitly provide the b argument, I get:

application type mismatch
  @one_smul b
argument
  b
has type
  ℕ → F : Type ?u.2
but is expected to have type
  Type ?u.761 : Type (?u.761 + 1)

[Pedro Sánchez Terraf]

If you import Mathlib.Tactic it works :thinking:

[Kyle Miller]

It appears to be a missing instance, docs#Pi.mulAction

Adding import Mathlib.GroupTheory.GroupAction.Pi works

[Martin C. Martin]

Thanks! I would have hoped for a better error message, but the fix certainly gets me un-stuck.

[Patrick Massot]

This is an extremely common error message that ranks pretty high in the list of frustrating error messages. It always means the type of ?b should have type class instances that the type of b hasn't. Somehow we need the error message to mention those type classes. @David Thrane Christiansen that would be a very nice target in your error message improving quest.

[Kevin Buzzard]

It's not so much a frustrating error message as a very confusing one, and probably both Patrick and I have seen many people confused by it.

[Yongyi Chen]

Does anything about typeclasses appear when you hover over ?b in the infoview?
Edit: Back at computer, and looks like nope.

[Bolton Bailey]

For people wanting to know how to make progress in this kind of situation: When you see the question mark like that, it generally means that Lean doesn't know what variable is supposed to go there. This can be a hint that providing more variables explicitly can be helpful. For example, if you write

import Mathlib.Algebra.Field.Basic

example {F : Type _} [Field F]  : ∀ x : (ℕ → F), (1 : F) • x = x := by
  intro b
  apply one_smul F b

you get the "failed to synthesize instance" error, which hopefully should clue you in that you need to import the file with the instance.