Unification with free variables of structure type

Stream: lean4

[Rish Vaishnav]

I was wondering how Lean is going about unifying up (down b) and b in this definition from the prelude:

theorem PLift.up_down {α : Sort u} (b : PLift α) : Eq (up (down b)) b := rfl

My guess is that expands b to up (down b) (where it knows not to infinitely expand b in the LHS because it's already been projected), and more generally, if we have any structure

structure Test (α : Sort u) : Type u where
  a1 : α
  a2 : α
  ...
  an : α

and a free variable t : Test, unification will expand t wherever it occurs to Test.mk t.a1 t.a2 ... t.an. Is my suspicion correct? I'm trying to find where in the code this expansion happens, I found toCtorWhenStructure in src/Lean/Meta/WHNF.lean but it looks like that only applies to recursor applications.

[Rish Vaishnav]

Aha, I found try_eta_struct in src/kernel/typechecker.cpp. Is there an equivalent somewhere in the Lean codebase?

[Kevin Buzzard]

I don't think Lean will expand b to up (down b), it's more likely simplifying up (down b) back to b (probably using eta for structures).

[Rish Vaishnav]

Yeah from the typechecker code it looks like it's not actually doing any expansion, it's actually checking for specifically this case:

 /** \brief check whether \c s is of the form <tt>mk t.1 ... t.n</tt> */
bool type_checker::try_eta_struct_core(expr const & t, expr const & s) { ... }

bool try_eta_struct(expr const & t, expr const & s) {
     return try_eta_struct_core(t, s) || try_eta_struct_core(s, t);
}

(and try_eta_struct is called from is_def_eq)