feat: make it possible to use dot notation in m! strings

[kmill]

This default instance makes it possible to write things like m!"the constant is {.ofConstName n}".

Breaking change: This weakly causes terms to have a type of MessageData if their type is otherwise unknown. For example:

• m!"... {x} ..." can cause x to have type MessageData, causing the let definition of x to fail to elaborate. Fix: give x an explicit type.
• Arithmetic expressions in m! strings may need a type ascription. For example, if the type of i is unknown at the time the arithmetic expression is elaborated, then m!"... {i + 1} ..." can fail saying that it cannot find an HAdd Nat Nat MessageData instance. Two fixes: either ensure that the type of i is known, or add a type ascription to guide the MessageData coercion, like m!"... {(i + 1 : Nat)} ...".

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5857 build failed against this PR. (2024-10-27 02:51:14) View Log
• 🟡 Mathlib branch lean-pr-testing-5857 build against this PR was cancelled. (2024-10-27 16:29:52) View Log
• ❌ Mathlib branch lean-pr-testing-5857 built against this PR, but testing failed. (2024-10-27 17:07:22) View Log
• ✅ Mathlib branch lean-pr-testing-5857 has successfully built against this PR. (2024-10-27 18:07:27) View Log

[nomeata]

Breaking change: arithmetic expressions in m! strings may need a type ascription, for example m!"... {i + 1} ..." -> m!"... {(i + 1 : Nat)} ...".

Is that only when the type of i is otherwise unknown, or now always? Does it affect plain m!"{i}"?

(Maybe include the answers in the description so that they make it to the release notes.)

[kmill]

@nomeata It affects {i} too when the type of i is unknown, but only if it's still unknown by the time default instances apply. The mathlib breakage so far has been a case where the default instance chose to apply, causing i to become MessageData, causing the let binding for i to fail to elaborate.

For i + 1, the special thing here is that the binop elaborator isn't able to do postponement if it fails to calculate a type for the expression, so it falls back to letting HAdd.hAdd elaborate like usual.

[nomeata]

Ok, sounds reasonable and matches the expectation that interpolatoin behaves like an implicit toMessageData.