Add shallow equality to the full-imperative pipeline

[brunnerant]

This PR adds up to the PR #862 and adds the following:

• Shallow equality: a new type of equality, denoted by =~ (and !=~ for its negation, though that notation can be changed if we want something easier to type ;) ) was introduced. Semantically, it corresponds to normal equality on erased terms after the imperative phase. Intuitively, that amounts to comparing values without following references on the heap.
• Equality (==) is now forbidden on values that "touch" the heap. Here, "touch" means that a value might contain a reference to the heap, or transitively contains a value that touches the heap.

[vkuncak]

This branch is out of date but the point is still relevant. It's a question of design if we want a different symbol for equality that is restricted to references in full imperative phase.

[samarion]

Shouldn't we be using Scala's eq and ne for reference equality?

[vkuncak]

The way I see it, there can be user-defined equality and system-provided equality. User defined equality is something that we can support by helping users not define non-sensical congruences, but ultimatley it's up to user. System-provided equality is something we should have and keep it meaningful. When we talk about immutable structures, all we need to settle is how to treat functions. When we talk about mutable structures, then due to possible cycles it's not entirely clear what a system provided equality would be short of reference equality.

Our encoding would end up using some equality after encoding of heap. We can of course disable this for the user, but then specification language becomes more limited. The overall story is rather messy for something as fundamental as equality, so it would be good to discuss it and document it. This PR would be may or may not be a good place for it...

[samarion]

Agreed about the different notions of equality, although I would stay away from user-defined equality for now since it's a significant project. A simple preliminary solution would be to only support surface-level ==, !=, eq and ne when the Scala notions coincides with the system notion.

In a second stage, we could then introduce === and =!= operators which denote a more theoretical notion of equality (TBD) and provide some support in the type-checker to construct equality proofs. Finally, we could allow user-level equality as long as it is consistent with === and =!= (but we might want to handle this through type classes, not dynamic dispatch).

Anyway, I think the first step is the most important one for now and shouldn't require too much work. I think @romac already implemented some part (or all?) of this in the SoundEquality tree sanitizer check.