elaboration in calc

Stream: lean4

[Heather Macbeth]

I am cross-posting a question of @Rob Lewis from the #mathlib4 stream. Does calc elaborate differently (and arguably "worse") in later lines than in the first line? 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

[Heather Macbeth]

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

Would it be possible to change elaboration so that the good error message appears in all cases?

[Mario Carneiro]

It seems unlikely with the typeclass based approaches to calc, since each equation is elaborated separately and they are combined by Trans. The issue is that _ = 2 ^ n on its own typechecks, as an equality in Nat

[Heather Macbeth]

Something has changed here since Lean 3, right? In Lean 3 I get the same (useful) error message on both these two:

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

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

[Sebastian Ullrich]

Lean 4 calc is a complete reimplementation. It looks like we should replace the _ with an mvar of the previous type before elaboration.

[Heather Macbeth]

That would be great as far as I'm concerned. I opened an issue lean4#2040 to record the suggestion.