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.
The error messages
don't know how to synthesize placeholderare displaying an incorrectcontextafter commit 7842036.For example:
produces the error message
instead of
Commit 7842036 avoids the use of delayed abstractions when creating bindings (lambda/pi/let). The idea is simple for every metavariable
?moccurring in the body of the bindere, revert all locals in?mthat are being abstracted, and obtain?m1. Then,?mis replaced with?m1 x_1 ... x_nwherex_1 ... x_nare the reverted locals.The body of the theorem is just a placeholder which is elaborated into
?m. The local context of?mcontainsa,bandh. Then, when we abstracta b h, we obtainfun (a b : nat) (h : a = b), ?m_1 a b h, and the assignment?m := ?m_1 a b h. Then, the methodelaborator::ensure_no_unassigned_metavarsincorrectly produces an error message for?m_1which 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?minstead of?m_1.