Inference binds to explicit identifiers and no occurs check for Nats

[bastian-koepcke]

In the inference, the cases for when we bind a value to an identifier are unclear.

It is possible that we bind a value to an explicit identifier. This is generally not possible as long as the identifier is not constraint to that value. Instead throw an error.

Related to that is the problem that there is no occurs check for Nats:

• a nat may be equal to an expression that contains itself such as n = n/1
• when substituting n for n/1 there may be a large or unlimitted recursion

Solution: check the constraints/equalities, but do not substitute