String and MessageData for Nat

Stream: lean4

[Damiano Testa]

I was a little surprised that the code below does not work. Should I have expected it not to work?

import Lean.Elab.Command

run_cmd
  let con := 0  -- works with `let con : Nat := 0`
  let con := con + 1  -- this line is just for show, it can be removed and the issue persists
  Lean.logInfo m!"Step {con}"  -- comment this line and everything works

run_cmd
  let mut con := 0  -- works with `let mut con : Nat := 0`
  for i in [:1] do
    con := con + 1  -- this line is just for show, it can be removed and the issue persists
    Lean.logInfo m!"Step {con}"  -- comment this line and everything works
    continue

[Robin Arnez]

This is because of a few quirks in how things work here:

1. It sees {con} here, so first thing it thinks is that con must be a MessageData
2. It ends up with let con : MessageData := con + 1 which is not possible
   A type annotation or using {con.repr} fixes this issue because then you tell it that it can't be MessageData and it should try to convert it to a string first.

[Robin Arnez]

Still, this feels like it should be able to figure it out itself, seems to just be a quirk of the implementation.

[Damiano Testa]

I think that is sees m!"...{con}" first, so it tries a MessageData: it works if you try to produce an interpolated string via s!.

[Damiano Testa]

I was more curious of whether this is expected behaviour: it seems like a pretty common thing to do to have a counter that you increase and you print it.

[Robin Arnez]

I don't think this is really expected behavior but adding a type annotation is simple enough that it doesn't really matter.