Heterogeneous `==`

[divarvel]

Currently, the haskell and rust implementations (amongst others) produce an error on the following expression: 1 == true.

While this makes sense to refuse this expression in a typed language (the equivalent expression would not type check in rust or haskell), this behaviour is a bit more surprising in an untyped langage where such an expression would usually evaluate to false instead of blowing up.

The specification does not explicitly cover this case, and i think it should.

My preference would go to have heterogeneous equality comparisons to not blow up and evaluate to false for two reasons:

1. out of consistency with untyped languages like JS (or not-very-well typed languages like java);
2. out of consistency with set inclusion, which is morally equivalent to comparing a value with all values in a set for equality. This operation returns false in the case of heterogeneous values;
3. because it makes sense in a un(i)typed language: in rust and haskell, all term types are defined in a Term sum type, which defines == by first comparing the constructors, and then values if the constructors are the same (this is why 2. holds).

[Geal]

it also makes sense in the context of unification between facts: if we're matching between facts, and the term we are matching on has different types on both sides, they do not match, but it does not blow up the entire execution