Bogus error message: don't know how to synthesize placeholder

[leodemoura]

The error messages don't know how to synthesize placeholder are displaying an incorrect context after commit 7842036.
For example:

theorem foo (a b : nat) (h : a = b) : b = a :=
_

produces the error message

error: don't know how to synthesize placeholder
context:
⊢ ∀ (a b : ℕ), a = b → b = a

instead of

error: don't know how to synthesize placeholder
context:
a b : ℕ
h : a = b
⊢ b = a

Commit 7842036 avoids the use of delayed abstractions when creating bindings (lambda/pi/let). The idea is simple for every metavariable ?m occurring in the body of the binder e, revert all locals in ?m that are being abstracted, and obtain ?m1. Then, ?m is replaced with ?m1 x_1 ... x_n where x_1 ... x_n are the reverted locals.
The body of the theorem is just a placeholder which is elaborated into ?m. The local context of ?m contains a, b and h. Then, when we abstract a b h, we obtain fun (a b : nat) (h : a = b), ?m_1 a b h, and the assignment ?m := ?m_1 a b h. Then, the method elaborator::ensure_no_unassigned_metavars incorrectly produces an error message for ?m_1 which has an empty context.

@Kha This problem is quite annoying, but it is not worth fixing now since we will re-write the elaborator. In the new elaborator, we should use a different approach where we record the metavariable created for each placeholder _. Then, during finalization, we check whether these placeholders have been assigned or not. If they have been assigned to metavariables applications such as ?m_1 a b h, we just report the error for ?m instead of ?m_1.

[Kha]

Yes, I've just assumed that this will be fixed later. The fix sounds good.

[Kha]

fixed a while ago