Feature request: change in calc elaboration

[hrmacbeth]

The current approach to calc elaboration gives behaviour that is inconsistent between the first line and later lines, in a way that was surprising to me until explained, and and may be confusing to novices. Consider the following examples:

example (n : Nat) (a : Int) : a = 22 :=
  calc
    a = 2 ^ n := sorry -- good error message
    _ = (22 : Int) := sorry

example (n : Nat) (a : Int) : a = 22 :=
  calc
    a = (37 : Int) := sorry
    _ = 2 ^ n := sorry -- bad error message
    _ = (22 : Int) := sorry

example (n : Nat) (a : Int) : a = (2 : Int) ^ n :=
  calc
    a = (37 : Int) := sorry
    _ = 2 ^ n := sorry -- bad error message

In all these examples 2 ^ n fails to typecheck, because there's no HPow Nat Nat Int instance in core Lean. But the error messages are different. In the first case (with the expression in the first line of the calc) we get the useful error message

failed to synthesize instance
  HPow Nat Nat Int

whereas in the other cases (with the expression in later lines of the calc) we get a perplexing error message

invalid 'calc' step, left-hand-side is 
  ?m.381 : Nat
previous right-hand-side is
  37 : Int

By contrast, in Lean 3 the same (useful) error message appears in the first line and subsequently:

example (n : nat) (a : int) : a = 22 :=
  calc
    a = 2 ^ n : sorry -- good error message
    ... = (22 : int) : sorry

example (n : nat) (a : int) : a = 22 :=
  calc
    a = (37 : int) : sorry
    ... = 2 ^ n : sorry -- good error message
    ... = (22 : int) : sorry

On Zulip, @Kha proposes a fix:

It looks like we should replace the _ with an mvar of the previous type before elaboration.

I am recording that as a feature request here.