opening a namespace can affect elaboration

As reported by @b-mehta on Zulip in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60open.20finset.60.20changes.20truth.20of.20goal/near/304982461
it is possible that simply opening a namespace which contains overloaded function names can cause the argument types to be elaborated differently, even if the overloaded function does not apply

def foo1.bar (x y : ℤ) := x ≠ y
def foo2.bar (x y : ℕ) := true

open foo1
def my_statement1 (k : ℕ) := bar (0 : ℤ) (k - 0)
open foo2

def my_statement (k : ℕ) := bar (0 : ℤ) (k - 0)

set_option pp.all true
#print my_statement1
#print my_statement
example : my_statement 1 :=
begin
  rw [my_statement],
  simp only [foo1.bar, int.coe_nat_one],
  intro h,
  cases h,
end

example : ¬ my_statement 1 :=
begin
  rw [my_statement],
  simp [foo1.bar, int.coe_nat_zero],
end

Start by reproducing the two namespace-opening examples in a Lean 3 development environment and compare the elaborated results shown by #print. The issue names no source files or tests; trace the elaboration path affected by overloaded names, and consider the work complete when opening foo2 no longer changes the behavior of my_statement.