Special treatment of effect unification variables in type-inference

Since type-inference is a separate phase from effect inference, the type-checker must treat unification variables of kind effect with special care. The motivating example is a first-class handler:
```
let x = handler e₁ end
```
If the type of e₁ contains effect unification variable a, that should be equal to the handled effect, but we will know it during the effect inference, the naive type-checker could generalize it at the let-definition, which will result in a variable escaping its scope. In order to avoid such problem, current implementation sets all unification variables of the effect kind to `TEffect` placeholder at the place of generalization. However, such an approach leads to generating unnecessary equality constraints on effects that are parameters to effect capability passed around. Such effects could be just unified by the type inference. A better approach could be to set effect unification variables to `TEffect` only on (potential) binders of effects, and to do it only for those unification variables that are linked to the scope of the binder.