Should types be unified when unifying lambdas?

[atennapel]

I was looking at your implementation of Setoid Type Theory and I saw that there you do have types for lambda parameters in your core language. But during unification \(x : A). t1 ~ \(x : B). t2 then A ~ B is not unifed. Is there are a reason to not unify the types of lambda parameters?

[AndrasKovacs]

The precondition of unification is that the types of the sides are the same. When we get to unify two lambdas, we know that the types are the same, hence the domain types are also the same, so it's redundant to unify them.

[atennapel]

Ah yes, that makes total sense, thanks.