When you add restrictions to make equalities like this decidable, it usually means less things are equal to each other if that makes sense so the problem is bei

When you add restrictions to make equalities like this decidable, it usually means less things are equal to each other if that makes sense so the problem is being pushed elsewhere somewhat. For example, Coq has decidable equality which is crudely described as "simplify both sides as much as possible and if they're syntactically the same then they're equal". So this could be equal depending on how you define plus: plus(1, plus(1, x)) = plus(2, x) but this wouldn't be: plus(1, plus(1, x)) = plus(x, 2) Long story but "plus" is usually defined by recursion on the first argument and when you put the "x" as the first argument the type checker cannot simplify "plus(x, 2)" any further so it isn't able to simplify both sides to the same form, therefore they're not equal. So this makes equality decidability but now things you intuitively think of as equal aren't equal.