Okay so the issue is that in unification, if you try to unify I -Int 1 against I, it treats them as the same variable.

How is this handled in the non-function case, then? I should not be able to create a variable during execution that is treated as identical to one of the variables in the LHS of a rule, should I? Or am I still missing something?