When type checking proof terms, how does unification come into play after elaboration to the core language of Calculus of Inductive Constructions?
Specifically, when dealing with properties of equalities like transitivity and symmetry, I find it challenging to comprehend where the unification of variables occurs when proving statements like forall x y, x = y -> y = x by pattern matching on refl x x.
Additional context: I am aware that unification is necessary in the extended language of Coq, particularly when introducing existential variables and implicitly instantiating them. However, when reviewing the documentation on the core typing rules of Coq, I could not find any explicit mention of unification.
The answer is simple: there is no unification in the kernel.
In the particular case you mention, you can look at a proof term, which will look something like
fun x y (e : x = y) =>
match e as e' in _ = y' return y' = x with
| eq_refl => eq_refl
end
I intentionally included the return clause: this is where the interesting things are happening. This clause binds multiple variable: one for each index of the inductive type (here, equality has one index, so there is one bound variable y'), and an extra one (here e') for the scrutinee (the term matched on, here e). In each branch, these bound variables are replaced by the specific indices for the given constructor, and this constructor itself. For instance, for equality there is just one branch, where y' is replaced by x (and e' by eq_refl). If each branch type-check against its "specialized version" of the return clause, then the whole pattern-matching has a type obtained from the return clause by replacing the variable for the indices by the indices of the scrutinee, and the last on by the scrutinee itself.
All in all, this mechanism might look like unification, because it relates different instances of the same dependent type: the one in the branches, and the one of the whole pattern-matching. But while during elaboration the return clause can be inferred by Coq using unification (alleviating the user from giving it by hand), once a suitable one has been found there is no unification any more.