Unknown identifier in `do` block inside tactic mode

Local variables appearing on the last line of a do block inside tactic mode cause an incorrect "unknown identifier" error:

example (foo bar : list ℤ) : false :=
begin
  have : do { x ← bar, foo } = bar >> foo := rfl, -- unknown identifier 'foo'
  calc do { x ← bar, foo } = bar >> foo : rfl, -- unknown identifier 'foo'
  admit
end

It seems to happen regardless of the tactic used, e.g. writing calc instead of have also causes the same error.

The error only occurs for local names, globals are fine. Also, replacing it with an underscore, or putting the do block in term mode, will work:

example (foo bar : list ℤ) : false :=
begin
  have : do { x ← bar, _ } = bar >> foo := rfl, -- works
  have : do { x ← bar, list.nil } = [] := sorry, -- works
  admit
end

example (foo bar : list ℤ) : false :=
have this : do { x ← bar, foo } = bar >> foo, from rfl, -- works
sorry

Reproduce the reported examples in Lean 3, comparing tactic-mode do blocks with the term-mode and global-name cases shown in the issue. Trace the tactic-mode elaboration path for the final local expression; done means local names no longer produce an incorrect unknown-identifier error while the documented working cases remain valid.