Stick to strict pattern unification

[AndrasKovacs]

Page 11 of Abel & Pientka reveals that solving non-linear spines is only sound if the type of RHS is also well-formed. Since we don't yet have typed metas or unification, the obvious solution for now is to remove the non-linear voodoo and stick to strict pattern unification.

[atennapel]

So this simply means you should throw an error if a meta spine contains duplicate variables, correct?

[AndrasKovacs]

Correct.

[ice1000]

Speaking of typed meta/unify, would you like to address Twin types?

[AndrasKovacs]

Heterogeneous unification is not a good idea in general.

• Major complexity cost.
• Minor benefit in unification strength.
• Major performance cost, the most problematic is that we cannot skip unification of subterms which are completely determined by the type. For example, Agda does not unify (or even store) parameters of inductive types in constructors, because they are fully determined by the type. Given cons : (A : Set) -> A -> List A -> List A, if we use homogeneous unification on cons A x xs and cons A' x' xs', we already know that A is definitionally equal to A'. This optimization can be extended to rigid symbols (bound variables, postulates) other than constructors, and to definitions which are known to be definitionally injective (by some analysis). With heterogeneous unification, this doesn't work.

There's also a superior possible implementation in type theories with computing transports. For example, assume f : (a : A) -> B a -> C, and we want to unify f a b with f a' b' at C. Assume that unify a a' returns with unsolved constraints. Vanilla homogeneous unification cannot progress here, and heterogeneous unification can, because it can unify b and b' even though they are not known to have the same type. However, if coercions compute, we can do the following: have p : a = a' as a propositional equality returned by unify a a', then unify coe (ap B p) b with b'.

This way, we keep all benefits of homogeneous unification, and depending on how strongly our coercions compute, we get precise solutions to heterogeneous equations as well.

[AndrasKovacs]

This issue is solved now.