Higher-order unification is pretty hard when you also have eta-equality for record types and definitional proof irrelevance. There's just too many ways for variables to disguise themselves as other things.

For example, consider a constraint _f u =?= v : B where u : A:

• If u is a variable x, then we can just solve it with _f := \(x : A) -> v.

• If u is eta-equivalent to a specific variable x, say u = (fst x , snd x), then we can eta-contract it and still solve the equation.

• If the type of u is a unit type, then it is eta-equivalent to any variable of the same type, so if there are two variables x : A and y : A then we don't know which one to eta-expand u to. Luckily, in this case it does not really matter since we can just prune the dependency of the metavariable and solve it as _f = \(_ : A) -> v.

• The fun really starts when you add definitional proof irrelevance into the mix. If the type A is in Prop (or sProp for the roosters here) then u is definitionally equal to any variable of type A, but also pruning the dependency of the metavariable could now lose solutions since A might be an empty type! So what do you do then, do you just try all the variables in the context to see if they have the right type? What if there's a variable in the context of a record type that has a (possibly nested) field of type A? Do we then need to first eta-expand the context variable? If there are multiple choices, do we then need to pick one that makes the variables in the arguments to the metavariable linear? This all feels way too complex and ad-hoc.