Extending unification logic

[lcnr]

What is this

This is a design document for const generics. Any discussions about its content should be on zulip. The conclusions of these discussions should then be edited back into this issue. Please do not post any comments directly in this issue.

Content

There are quite a few possible ways to extend our unification logic for generic constants.
It is still unclear which if these possible extensions we are going to add, but at least
some of these feel necessary to sensibly unify generic constants.

Evaluating subtrees

Given N + (1 + 3) and N + 4, we have to evaluate 1 + 3 for this to unify

Associativity

Given (N + 1) + M and N + (1 + M), we have to deal with associativity for this to unify

Commutativity

Given 1 + N and N + 1, we have to deal with commutativity for this to unify