Overloads Mess Up in Imports and in Proofs

[HalflingHelper]

As discussed in our meeting, overloads from imports don't work, and overloads aren't resolved in proofs.

[HalflingHelper]

Proof Problem

union A { a }
union B { b }

define f : fn A -> bool = λ x { true }
define f : fn B -> bool = λ x { false }

print(f(a))
print(f(b))

theorem f_true : f(a)
proof
  definition f
end

theorem f_false : not f(b)
proof
  definition f
end

./overload_proof_bug.pf:17.3-17.15: could not find a place to apply definition of f in:
        not (f.0(b.3))