elaboration and unification

Stream: general

[Paul van Wamelen]

Can someone suggest a good reference for learning more about what exactly is meant by 'elaboration' and 'unification'? I have a vague feel for what they are but would like to learn more.

[Kevin Buzzard]

My very vague understanding of what's going on here is that in principle elaboration and unification are just the study of filling in certain kinds of blanks. For example when you apply some theorem of the form a = b to a goal of f x = 37 the elaborator figures out that a is going to be f x and b is going to be 37. However the issue is that sometimes the elaborator has to solve a gigantic logic problem, and how it solves it is very system specific, so now I have to start talking about Lean and because I'm just going from experience rather than reading the C++ code or meta Lean code (neither of which I understand) things will now start to get hazier.

Lean has this attribute system, where you can just stick a "tag" like simp or no_lint docstring or irreducible or even a tag which you made up yourself, onto a definition or theorem. These tags don't change the definition or theorem in any way, but they change the way various internal systems treat the definition or theorem. For example tagging a theorem with simp makes the simplifier aware of it. There are several tags which you can attach to things which change the way Lean elaborates them, for example elab_as_eliminator or elab_simple, and these slightly change the way the (presumably rather complicated) elaborator works when it's trying to fill in all the {} and _ gaps in the term which it's trying to complete. We've seen examples recently where elaboration can fail for all sorts of obscure reasons, and then someone like Mario or Reid or one of the other people who _do_ know what's going on comes along and suggests a very minor tweak and all of a sudden things are working again.

[Paul van Wamelen]

Isn't "figures out that a is going to be f x and b is going to be 37" unification? And elaboration is basically filling in underscores and other stuff that the user didn't supply explicitly?
Are there some settings or traces that can show me what elaboration does?

[Mario Carneiro]

Elaboration is the whole proof script -> proof process, which includes unification, type class inference, and running tactics

[Mario Carneiro]

unification is specifically "A : T needs to have type T' here so T = T' and therefore this and that metavariable can be assigned"