class Steep::Subtyping::Constraints

def add(var, sub_type: nil, super_type: nil)
  subs, supers = dictionary[var]
  if super_type && !super_type.is_a?(AST::Types::Top)
    supers << eliminate_variable(super_type, to: AST::Types::Top.new)
  end
  if sub_type && !sub_type.is_a?(AST::Types::Bot)
    subs << eliminate_variable(sub_type, to: AST::Types::Bot.new)
  end
  super_fvs = supers.each.with_object(Set.new) do |type, fvs|
    fvs.merge(type.free_variables)
  end
  sub_fvs = subs.each.with_object(Set.new) do |type, fvs|
    fvs.merge(type.free_variables)
  end
  unless super_fvs.disjoint?(unknowns) || sub_fvs.disjoint?(unknowns)
    raise UnsatisfiedInvariantError.new(
      reason: UnsatisfiedInvariantError::UnknownsFreeVariableNotDisjoint.new(
        var: var,
        lower_bound: sub_type,
        upper_bound: super_type
      ),
      constraints: self
    )
  end
end