Investigate whether substitutions for type inference should be scoped

[umazalakain]

Does the application of solutions need to be scoped? Add the following test case:

((dt1 : data) -> _x) _x
((dt2 : data) -> dt2) _x

inference creates a new type variable dt and substitutes dt1 |-> dt and dt2 |-> dt:

((dt : data) -> _x) _x
((dt : data) -> dt) _x

then inference creates a constraint _x ~ dt resulting in the substitution _x |-> dt applying this substitution globally gives

((dt : data) -> dt) dt
((dt : data) -> dt) dt

however note that here the function argument dt is not bound: the expression is ill-scoped.