synthetic vs non synthetic meta variables

Stream: lean4

[Henrik Böving]

I've been reading up on the term elaboration implementation in order to see how it works and its special thing seems to be the creation of "synthetic metavariables" in order to postpone execution of the elaborator that is currently running to a later point in time so some type inference can figure stuff out or w/e. As far as I understand it the difference between synthetic and plain metavariables, is that syntheticones have a way attached to them that they are meant to be solved with, the SyntheticMVarKind. (is this correct)?

The things I'm wondering are:

• there is a kind tactic, my first thought was that this is what is used whenever we meet a tactic block so term elaboration can setup the tactic environment and call the tactic block but why do we do this with another meta variable instead of straight away running the tactic block?
• where do non synthetic meta variables come from, for example when I have a call to a generic function I can see in the elaboration trace that initially the type parameters are meta variables as well, I'm guessing non synthetic ones since the way to close them isn't exactly obvious from the beginning? Who is responsible for creating and closing those, for the closing part I'm guessing the type inference algorithm (where does that live?))?

[Leonardo de Moura]

(is this correct)?

There are more details, but the big picture you have described is correct.

we do this with another meta variable instead of straight away running the tactic block?

When we process the by ..., the local context and target type are often full of metavariables. These holes are usually only filled with information we obtain elaborating the rest of the declaration.

where do non synthetic meta variables come from,

Implicit { .. } arguments, and they are "filled" by solving typing constraints (i.e., invoking isDefEq).