Type information system recovery

Question

I'm reading the TIE: Principled Reverse Engineering of Types in Binary Programs paper and I'm having hard time understanding one of the key algorithms presented in it, specifically in the equality constraint solving.

The algorithm is explained in section 6.3.1 and the gist of it is as follows:

Equality constraints are solved through unification. Unification is essentially a substitution process, where given S = T we replace all occurrences of S with T in our worklist C.

following by a pseudo code:

SolveEquality (S = T, C)
  if IsFreeVariable(S) then
    C = C[S\T] ; S= = S={S 7→ T} ;
  else if IsFreeVariable (T) then
    C = C[T\S] ; S= = S={T 7→ S} ;
  else if S = ptr(S1) and T = ptr(T1) then
    C = C ∪ {S1 = T1} ;
  else if S = {li : Si} and T = {li : Ti} then
    C = C ∪ {Si = Ti};
  else
    Drop Constraint
end

What I find hard to understand is the IsFreeVariable function as it's not explained anywhere. I that a variable is free is a context related property, and I'm assuming the context we need to look at is at the current function being decompiled, but what I boggles me is, what is exactly a free variable in a intermediate language in SSA form, given the terms S and T would always be terms of definitions inside the given function, hence bound and not free variables, unless we're talking about definitions not found in the functions like esp0 (given their intermediate language snippet example) which I assume I'm wrong since there's no way this conditions should only apply to these cases.

In high level programming language like given a function like so:

def foo(x):
  return x + y

it's easy to reason that x is bound in the context of the function and y is free in this context, but in intermediate representation of assembly, given in SSA form, what is exactly considered a free variable?