Can `applyBindings` affect the semantics/result?

[bladyjoker]

I'm using applyBindings pervasively in https://github.com/mlabs-haskell/lambda-buffers/blob/401f8a920a557c71440795174da199a1e128c4f9/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs#L254.

It was very difficult to understand what's happening, but without it the whole thing just doesn't work. On multiple occasions I tried to debug this, and from what I can tell the 'variable sharing' business makes some unification (as on one side there's a variable) succeed when it shouldn't. This is 'fixed' by using applyBindings throughout to resolve any term completely so it doesn't contain shared variables.

I'd appreciate some advice here as it's my impressions that applyBindings should NOT be able to affect the semantics of a unification-fd program.

Thanks!