What are temporary metavariables?

Stream: general

[Jannis Limperg]

There are lots of functions for dealing with 'temporary metavariables' in init.meta.type_context. Could anyone explain what these are (as opposed to non-temporary metas)?

[Simon Hudon]

I think @Edward Ayers is the best person to answer this

[Edward Ayers]

The problem is that metavariables are too slow for some things like matching and rewriting. Because in order to perform a unification you need to carry round a metavariable context and do lots of checks. Temporary metavariables are used in the internals of lean when it needs to unify / match things very quickly. The best description of them is here in the source code.

[Jannis Limperg]

Thank you, that comment was very helpful! Unfortunately, based on this, it seems like temporary metas don't work for my application.

Follow-up: If I create a regular meta, can I use it to perform some unification, get the meta assignment (if any) and throw the meta away? Or will Lean be unhappy because the meta remains unassigned?

[Jannis Limperg]

Also, based on the comment, it seems like I can't freeze individual metas (i.e. prevent them from being assigned); I can only freeze the entire left-hand side and/or right-hand side of a unification problem. Is that accurate?

[Gabriel Ebner]

You could assign local constants to the meta-variables. This also prevents them from being assigned (with something else).

[Edward Ayers]

Gabriel is right

[Edward Ayers]

but you can now also get the assignment directly with type_context.get_assignment

[Edward Ayers]

The idea of type_context was that tactic has a restrictive interface to make it difficult to make a badly formed expression. Whereas the type_context lets you modify the metavariable context and local context directly

[Jannis Limperg]

Gabriel Ebner said:

You could assign local constants to the meta-variables. This also prevents them from being assigned (with something else).

Okay, but if I use this to freeze a meta, then I can't unfreeze it any more, right? I guess I could overwrite the assignment with a new meta.

Edward Ayers said:

but you can now also get the assignment directly with type_context.get_assignment

Right. I'll try to use this and some regular metas; let's see if Lean is okay with that.

[Edward Ayers]

Once you've assigned a meta to a local, you can't unassign it from tactic. You would have to instantiate the assignment local with a new meta.

[Jannis Limperg]

Okay, thanks. Next question (sorry, I'm just finding my way around the API): Is it correct that when unification fails, I can't tell whether this is because the terms cannot be unified or whether the unification strategy is just not powerful enough? I want to distinguish between the unification failures for zero =?= suc x and 2 * x =?= 3 * y.

[Gabriel Ebner]

No. As you can probably imagine, non-unifiability is hard to determine.

[Jannis Limperg]

Okay, I can see how that would be difficult.