When do "placeholder contexts" get synthesized?

Stream: lean4

[Thomas Murrills]

If you wind up with an Expr that contains .natural metavariables, you get hit with a serious (kernel) declaration has metavariables ... error, as metavariables aren't allowed in the kernel. But if you start with the syntax mkHole stx before elaboration, you get a different error: don't know how to synthesize placeholder context: ... presumably(?) during elaboration.

My question is: is there any way to have something that behaves like mkHole stx in this regard but which is an Expr? (My expectation was that mkHole stx corresponded to a natural metavariable, but I'm not so sure.) Or, is "synthesizing placeholder contexts" exclusively an elaboration-stage activity? (I'm betting on the latter, but thought I'd check!)

[Thomas Murrills]

Ok, after I sent this I realized I should look at the elaboration function for the syntax node kind that mkHole creates, and I figured out how to replicate the don't know how to synthesize placeholder context... behavior:

After creating the mvar expression with e.g. mkFreshExprMVar, run registerMVarErrorHoleInfo mvar.mvarId! stx (where stx is just whatever syntax originated the hole, i suppose), and it'll treat it as a "placeholder context". :)

I'm still not entirely sure what this really does, though...does it really just change how the error is handled?

[Sebastian Ullrich]

So just to clarify: there is no such thing as "synthesizing placeholder contexts". The error message is "don't know how to synthesize placeholder", with a "context" hint on the next line.

[Thomas Murrills]

ah! I see! That makes a lot more sense. :) (It all appears inline in VScode, and my infoview is small enough that it appeared like word wrapping, so I couldn't tell.)