Could not unify polymorphic class

Stream: lean4

[Leni Aniva]

Consider this very contrived example:

example : ∀ (a b: List Nat), List Nat := by
  intro a b

After the intro tactic, the current goal becomes

a b : List Nat
⊢ List Nat

Then the tactic apply HAppend.hAppend fails due to this:

failed to synthesize
  HAppend ?α ?β (List Nat)

but curiously, this is fine:

  apply _ ++ _

is there a way to make apply HAppend.hAppend succeed here?

[Leni Aniva]

I think apply HAppend.hAppend should succeed and it should generate metavariables for the two type arguments ?α ?β

[François G. Dorais]

I understand this is probably a mwe, but it's usually a bad idea to use tactic mode to generate data terms. This case is very simple so tactic mode probably produces the same term in the end but this is just easier:

example : ∀ (a b: List Nat), List Nat := HAppend.hAppend

In a proof of a theorem in tactic mode, when the arity of application is known in advance it is often a good idea to use refine instead of apply.

[Damiano Testa]

In your example, this also works: apply (HAppend.hAppend).

[Damiano Testa]

If you want the two type arguments to appear as goals (and the HAppend instance), then you can use apply @HAppend.hAppend _ _ _ ?_ ?_ ?_.

[Damiano Testa]

One more:

  apply HAppend.hAppend (self := ?_)

As far as I understand, this specifically asks apply to create a goal for self : HAppend α β γ and this is enough of a hint.

[Kevin Buzzard]

I am so totally confused by this thread :-) Maybe I shouldn't worry though, maybe this is all an artifact of using tactic mode to make data?

[Eric Wieser]

I think this is quite related to #mathlib4 > term vs by exact term, since

example (a b: List Nat) : List Nat := by
  exact HAppend.hAppend _ _

gives a different error to

example (a b: List Nat) : List Nat :=
  HAppend.hAppend _ _