Zulip Chat Archive

Stream: new members

Topic: Why failing to unify?

Martin C. Martin (Dec 04 2023 at 19:31):

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
  1  b = b

Looks easy to unify to me...

Martin C. Martin (Dec 04 2023 at 19:34):

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

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

Pedro Sánchez Terraf (Dec 04 2023 at 19:35):

If you import Mathlib.Tactic it works :thinking:

Kyle Miller (Dec 04 2023 at 19:37):

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

Adding import Mathlib.GroupTheory.GroupAction.Pi works

Martin C. Martin (Dec 04 2023 at 19:38):

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

Patrick Massot (Dec 04 2023 at 19:44):

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 (Dec 05 2023 at 00:10):

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 (Dec 05 2023 at 01:33):

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

Bolton Bailey (Dec 06 2023 at 14:41):

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.

Last updated: Dec 20 2023 at 11:08 UTC