feat: heterogeneous Append experiment

@Kha This one required a bunch of manual fixes. The main issue is that
before we added the string interpolation feature, we created
`MessageData`s using `++` and coercions. For example, given
`(e : Expr)`, we would write
```
let msg : MessageData := "type: " ++ e
```
and rely on the coercions `String -> MessageData` and
`Expr -> MessageData`, and the instance `Append MessageData`.
However, heterogeneous operators "block" the expected type propagation downwards.
This kind of code is obsolete now since we can write a more compact
version using string interpolation
```
let msg := m!"type: {e}"
```

src/Init/Coe.lean

@@ -181,3 +181,9 @@ instance [CoeTC α β] [Mod β] : HMod α β β where
 
 instance [CoeTC α β] [Mod β] : HMod β α β where
   hMod a b := Mod.mod a b
+
+instance [CoeTC α β] [Append β] : HAppend α β β where
+  hAppend a b := Append.append a b
+
+instance [CoeTC α β] [Append β] : HAppend β α β where
+  hAppend a b := Append.append a b

src/Init/Notation.lean

@@ -43,7 +43,7 @@ infixl:35 " && " => and
 infixl:30 " || " => or
 notation:max "!" b:40 => not b
 
-infixl:65 " ++ " => Append.append
+infixl:65 " ++ " => HAppend.hAppend
 infixr:67 " :: " => List.cons
 
 infixr:2   " <|> " => OrElse.orElse

src/Init/Prelude.lean

@@ -373,7 +373,10 @@ class HMod (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   hMod : α → β → γ
 
 class HPow (α : Type u) (β : Type v) (γ : outParam (Type w)) where
-  hPow : α → β → α
+  hPow : α → β → γ
+
+class HAppend (α : Type u) (β : Type v) (γ : outParam (Type w)) where
+  hAppend : α → β → γ
 
 class Add (α : Type u) where
   add : α → α → α
@@ -429,10 +432,14 @@ instance [Mod α] : HMod α α α where
 instance [Pow α] : HPow α α α where
   hPow a b := Pow.pow a b
 
+@[defaultInstance 1]
+instance [Append α] : HAppend α α α where
+  hAppend a b := Append.append a b
+
 open HAdd (hAdd)
 open HMul (hMul)
 open HPow (hPow)
-open Append (append)
+open HAppend (hAppend)
 
 @[reducible] def GreaterEq {α : Type u} [HasLessEq α] (a b : α) : Prop := LessEq b a
 @[reducible] def Greater {α : Type u} [HasLess α] (a b : α) : Prop     := Less b a
@@ -1778,7 +1785,7 @@ def MacroScopesView.review (view : MacroScopesView) : Name :=
   match view.scopes with
   | List.nil      => view.name
   | List.cons _ _ =>
-    let base := (Name.mkStr (append (append (Name.mkStr view.name "_@") view.imported) view.mainModule) "_hyg")
+    let base := (Name.mkStr (hAppend (hAppend (Name.mkStr view.name "_@") view.imported) view.mainModule) "_hyg")
     view.scopes.foldl Name.mkNum base
 
 private def assembleParts : List Name → Name → Name
@@ -1825,12 +1832,12 @@ def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
     | true  => Name.mkNum n scp
     | false =>
       { view with
-        imported   := view.scopes.foldl Name.mkNum (append view.imported view.mainModule),
+        imported   := view.scopes.foldl Name.mkNum (hAppend view.imported view.mainModule),
         mainModule := mainModule,
         scopes     := List.cons scp List.nil
       }.review
   | false =>
-    Name.mkNum (Name.mkStr (append (Name.mkStr n "_@") mainModule) "_hyg") scp
+    Name.mkNum (Name.mkStr (hAppend (Name.mkStr n "_@") mainModule) "_hyg") scp
 
 @[inline] def MonadQuotation.addMacroScope {m : Type → Type} [MonadQuotation m] [Monad m] (n : Name) : m Name :=
   bind getMainModule     fun mainModule =>

src/Lean/Compiler/ConstFolding.lean

@@ -10,8 +10,8 @@ import Lean.Compiler.Util
 
 namespace Lean.Compiler
 
-def BinFoldFn := Bool → Expr → Expr → Option Expr
-def UnFoldFn  := Bool → Expr → Option Expr
+abbrev BinFoldFn := Bool → Expr → Expr → Option Expr
+abbrev UnFoldFn  := Bool → Expr → Option Expr
 
 def mkUIntTypeName (nbytes : Nat) : Name :=
   Name.mkSimple ("UInt" ++ toString nbytes)

src/Lean/Compiler/InitAttr.lean

@@ -36,10 +36,10 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) : IO
         let initFnName ← resolveGlobalConstNoOverload initFnName
         let initDecl ← getConstInfo initFnName
         match getIOTypeArg initDecl.type with
-        | none => throwError ("initialization function '" ++ initFnName ++ "' must have type of the form `IO <type>`")
+        | none => throwError! "initialization function '{initFnName}' must have type of the form `IO <type>`"
         | some initTypeArg =>
           if decl.type == initTypeArg then pure initFnName
-          else throwError ("initialization function '" ++ initFnName ++ "' type mismatch")
+          else throwError! "initialization function '{initFnName}' type mismatch"
       | _ => match stx with
         | Syntax.missing =>
           if isIOUnit decl.type then pure Name.anonymous

src/Lean/Data/Json/Basic.lean

@@ -52,7 +52,7 @@ protected def toString : JsonNumber → String
     -- grow exponentially in the value of exponent.
     let exp := 9 + (countDigits m : Int) - (e : Int)
     let exp := if exp < 0 then exp else 0
-    let f := 10 ^ (e - exp.natAbs)
+    let f := (10:Int) ^ (e - exp.natAbs)
     let left := m / f
     let right := (f : Int) + m % f
     let rightUntrimmed := right.repr.mkIterator.next.remainingToString

src/Lean/Elab/App.lean

@@ -833,7 +833,7 @@ private def toMessageData (ex : Exception) : TermElabM MessageData := do
       pure m!"{exPosition.line}:{exPosition.column} {ex.toMessageData}"
 
 private def toMessageList (msgs : Array MessageData) : MessageData :=
-  indentD (MessageData.joinSep msgs.toList (Format.line ++ Format.line))
+  indentD (MessageData.joinSep msgs.toList m!"\n\n")
 
 private def mergeFailures {α} (failures : Array TermElabResult) : TermElabM α := do
   let msgs ← failures.mapM fun failure =>

src/Lean/Elab/Attributes.lean

@@ -13,7 +13,7 @@ structure Attribute where
   args : Syntax := Syntax.missing
 
 instance : ToFormat Attribute := ⟨fun attr =>
-  Format.bracket "@[" (toString attr.name ++ (if attr.args.isMissing then "" else toString attr.args)) "]"⟩
+  Format.bracket "@[" f!"{attr.name}{if attr.args.isMissing then "" else toString attr.args}" "]"⟩
 
 instance : Inhabited Attribute := ⟨{ name := arbitrary }⟩
 

src/Lean/Elab/Command.lean

@@ -239,7 +239,7 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit :=
           let k := stx.getKind;
           match table.find? k with
           | some elabFns => elabCommandUsing s stx elabFns
-          | none         => throwError ("elaboration function for '" ++ toString k ++ "' has not been implemented")
+          | none         => throwError! "elaboration function for '{k}' has not been implemented"
     | _ => throwError "unexpected command"
 
 /-- Adapt a syntax transformation to a regular, command-producing elaborator. -/

src/Lean/Elab/DeclModifiers.lean

@@ -54,15 +54,15 @@ def Modifiers.addAttribute (modifiers : Modifiers) (attr : Attribute) : Modifier
 instance : ToFormat Modifiers := ⟨fun m =>
   let components : List Format :=
     (match m.docString with
-     | some str => ["/--" ++ str ++ "-/"]
+     | some str => [f!"/--{str}-/"]
      | none     => [])
     ++ (match m.visibility with
      | Visibility.regular   => []
-     | Visibility.protected => ["protected"]
-     | Visibility.private   => ["private"])
-    ++ (if m.isNoncomputable then ["noncomputable"] else [])
-    ++ (if m.isPartial then ["partial"] else [])
-    ++ (if m.isUnsafe then ["unsafe"] else [])
+     | Visibility.protected => [f!"protected"]
+     | Visibility.private   => [f!"private"])
+    ++ (if m.isNoncomputable then [f!"noncomputable"] else [])
+    ++ (if m.isPartial then [f!"partial"] else [])
+    ++ (if m.isUnsafe then [f!"unsafe"] else [])
     ++ m.attrs.toList.map (fun attr => fmt attr)
   Format.bracket "{" (Format.joinSep components ("," ++ Format.line)) "}"⟩
 

src/Lean/Elab/Do.lean

@@ -175,7 +175,7 @@ partial def CodeBlocl.toMessageData (codeBlock : CodeBlock) : MessageData :=
     | Code.«return» _ v           => m!"return {v} {us}"
     | Code.«match» _ ds t alts    =>
       m!"match {ds} with"
-      ++ alts.foldl (init := "") fun acc alt => acc ++ m!"\n| {alt.patterns} => {loop alt.rhs}"
+      ++ alts.foldl (init := m!"") fun acc alt => acc ++ m!"\n| {alt.patterns} => {loop alt.rhs}"
   loop codeBlock.code
 
 /- Return true if the give code contains an exit point that satisfies `p` -/

src/Lean/Elab/Level.lean

@@ -74,7 +74,7 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
       if (← read).autoBoundImplicit && isValidAutoBoundLevelName paramName then
         modify fun s => { s with levelNames := paramName :: s.levelNames }
       else
-        throwError ("unknown universe level " ++ paramName)
+        throwError! "unknown universe level '{paramName}'"
     return mkLevelParam paramName
   else if kind == `Lean.Parser.Level.addLit then
     let lvl ← elabLevel (stx.getArg 0)

src/Lean/Elab/Log.lean

@@ -68,7 +68,7 @@ def logException [MonadLiftT IO m] (ex : Exception) : m Unit := do
   | Exception.internal id _ =>
     unless id == abortExceptionId do
       let name ← id.getName
-      logError ("internal exception: " ++ name)
+      logError m!"internal exception: {name}"
 
 def logTrace (cls : Name) (msgData : MessageData) : m Unit := do
   logInfo (MessageData.tagged cls msgData)

src/Lean/Elab/Print.lean

@@ -15,7 +15,7 @@ private def lparamsToMessageData (lparams : List Name) : MessageData :=
   match lparams with
   | []    => ""
   | u::us => do
-    let mut m : MessageData := ".{" ++ u
+    let mut m := m!".\{{u}"
     for u in us do
       m := m ++ ", " ++ u
     return m ++ "}"

src/Lean/Elab/Quotation.lean

@@ -200,7 +200,7 @@ private def getHeadInfo (alt : Alt) : HeadInfo :=
       -- Splices should only appear inside a nullKind node, see next case
       if isAntiquotSplice quoted then unconditional $ fun _ => throwErrorAt quoted "unexpected antiquotation splice"
       else if anti.isIdent then { kind := kind, rhsFn :=  fun rhs => `(let $anti := discr; $rhs) }
-      else unconditional fun _ => throwErrorAt anti ("match_syntax: antiquotation must be variable " ++ toString anti)
+      else unconditional fun _ => throwErrorAt! anti "match_syntax: antiquotation must be variable {anti}"
     else if isAntiquotSplicePat quoted && quoted.getArgs.size == 1 then
       -- quotation is a single antiquotation splice => bind args array
       let anti := getAntiquotTerm quoted[0]
@@ -212,7 +212,7 @@ private def getHeadInfo (alt : Alt) : HeadInfo :=
       let argPats := quoted.getArgs.map (pat.setArg 1);
       { kind := quoted.getKind, argPats := argPats }
   else
-    unconditional $ fun _ => throwErrorAt pat ("match_syntax: unexpected pattern kind " ++ toString pat)
+    unconditional $ fun _ => throwErrorAt! pat "match_syntax: unexpected pattern kind {pat}"
 
 -- Assuming that the first pattern of the alternative is taken, replace it with patterns (if any) for its
 -- child nodes.

src/Lean/Elab/Syntax.lean

@@ -237,7 +237,8 @@ def «syntax»      := parser! "syntax " >> optPrecedence >> optKindPrio >> many
 @[builtinCommandElab «syntax»] def elabSyntax : CommandElab := fun stx => do
   let env ← getEnv
   let cat := stx[5].getId.eraseMacroScopes
-  unless (Parser.isParserCategory env cat) do throwErrorAt stx[5] ("unknown category '" ++ cat ++ "'")
+  unless (Parser.isParserCategory env cat) do
+    throwErrorAt! stx[5] "unknown category '{cat}'"
   let syntaxParser := stx[3]
   -- If the user did not provide an explicit precedence, we assign `maxPrec` to atom-like syntax and `leadPrec` otherwise.
   let precDefault  := if isAtomLikeSyntax syntaxParser then Parser.maxPrec else Parser.leadPrec

src/Lean/Elab/SyntheticMVars.lean

@@ -109,8 +109,8 @@ private def synthesizeSyntheticMVar (mvarSyntheticDecl : SyntheticMVarDecl) (pos
   Return `true` if at least one of them was synthesized. -/
 private def synthesizeSyntheticMVarsStep (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool := do
   let ctx ← read
-  traceAtCmdPos `Elab.resuming $ fun _ =>
-    fmt "resuming synthetic metavariables, mayPostpone: " ++ fmt ctx.mayPostpone ++ ", postponeOnError: " ++ toString postponeOnError
+  traceAtCmdPos `Elab.resuming fun _ =>
+    m!"resuming synthetic metavariables, mayPostpone: {ctx.mayPostpone}, postponeOnError: {postponeOnError}"
   let s ← get
   let syntheticMVars    := s.syntheticMVars
   let numSyntheticMVars := syntheticMVars.length

src/Lean/Elab/Tactic/Basic.lean

@@ -16,7 +16,7 @@ namespace Lean.Elab
 open Meta
 
 def goalsToMessageData (goals : List MVarId) : MessageData :=
-  MessageData.joinSep (goals.map $ MessageData.ofGoal) (Format.line ++ Format.line)
+  MessageData.joinSep (goals.map $ MessageData.ofGoal) m!"\n\n"
 
 def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit := do
   throwError! "unsolved goals\n{goalsToMessageData goals}"

src/Lean/Elab/Term.lean

@@ -850,7 +850,7 @@ private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : Term
   an error is found. -/
 private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool)
     : List TermElab → TermElabM Expr
-  | []                => do throwError! "unexpected syntax{MessageData.nestD (Format.line ++ stx)}"
+  | []                => do throwError! "unexpected syntax{indentD stx}"
   | (elabFn::elabFns) => do
     try
       elabFn stx expectedType?

src/Lean/Elab/Util.lean

@@ -53,10 +53,10 @@ def addMacroStack {m} [Monad m] [MonadOptions m] (msgData : MessageData) (macroS
   match macroStack with
   | []             => pure msgData
   | stack@(top::_) =>
-    let msgData := msgData ++ Format.line ++ "with resulting expansion" ++ MessageData.nest 2 (Format.line ++ top.after)
+    let msgData := msgData ++ Format.line ++ "with resulting expansion" ++ indentD top.after
     pure $ stack.foldl
       (fun (msgData : MessageData) (elem : MacroStackElem) =>
-        msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ elem.before))
+        msgData ++ Format.line ++ "while expanding" ++ indentD elem.before)
       msgData
 
 def checkSyntaxNodeKind (k : Name) : AttrM Name := do

src/Lean/Message.lean

@@ -126,7 +126,7 @@ def joinSep : List MessageData → MessageData → MessageData
   | a::as, sep => a ++ sep ++ joinSep as sep
 def ofList: List MessageData → MessageData
   | [] => "[]"
-  | xs => sbracket $ joinSep xs ("," ++ Format.line)
+  | xs => sbracket $ joinSep xs (ofFormat "," ++ Format.line)
 def ofArray (msgs : Array MessageData) : MessageData :=
   ofList msgs.toList
 
@@ -216,40 +216,6 @@ def indentD (msg : MessageData) : MessageData :=
 def indentExpr (e : Expr) : MessageData :=
   indentD e
 
-namespace KernelException
-
-private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData :=
-  MessageData.withContext { env := env, mctx := {}, lctx := lctx, opts := opts } msg
-
-def toMessageData (e : KernelException) (opts : Options) : MessageData :=
-  match e with
-  | unknownConstant env constName       => mkCtx env {} opts $ "(kernel) unknown constant " ++ constName
-  | alreadyDeclared env constName       => mkCtx env {} opts $ "(kernel) constant has already been declared " ++ constName
-  | declTypeMismatch env decl givenType =>
-    let process (n : Name) (expectedType : Expr) : MessageData :=
-      "(kernel) declaration type mismatch " ++ n
-      ++ Format.line ++ "has type" ++ indentExpr givenType
-      ++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType;
-    match decl with
-    | Declaration.defnDecl { name := n, type := type, .. } => process n type
-    | Declaration.thmDecl { name := n, type := type, .. }  => process n type
-    | _ => "(kernel) declaration type mismatch" -- TODO fix type checker, type mismatch for mutual decls does not have enough information
-  | declHasMVars env constName _        => mkCtx env {} opts $ "(kernel) declaration has metavariables " ++ constName
-  | declHasFVars env constName _        => mkCtx env {} opts $ "(kernel) declaration has free variables " ++ constName
-  | funExpected env lctx e              => mkCtx env lctx opts $ "(kernel) function expected" ++ indentExpr e
-  | typeExpected env lctx e             => mkCtx env lctx opts $ "(kernel) type expected" ++ indentExpr e
-  | letTypeMismatch  env lctx n _ _     => mkCtx env lctx opts $ "(kernel) let-declaration type mismatch " ++ n
-  | exprTypeMismatch env lctx e _       => mkCtx env lctx opts $ "(kernel) type mismatch at " ++ indentExpr e
-  | appTypeMismatch  env lctx e fnType argType =>
-    mkCtx env lctx opts $
-      "application type mismatch" ++ indentExpr e
-      ++ Format.line ++ "argument has type" ++ indentExpr argType
-      ++ Format.line ++ "but function has type" ++ indentExpr fnType
-  | invalidProj env lctx e              => mkCtx env lctx opts $ "(kernel) invalid projection" ++ indentExpr e
-  | other msg                           => "(kernel) " ++ msg
-
-end KernelException
-
 class AddMessageContext (m : Type → Type) where
   addMessageContext : MessageData → m MessageData
 
@@ -298,4 +264,33 @@ syntax:max "m!" interpolatedStr(term) : term
 macro_rules
   | `(m! $interpStr) => do interpStr.expandInterpolatedStr (← `(MessageData)) (← `(toMessageData))
 
+
+namespace KernelException
+
+private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData :=
+  MessageData.withContext { env := env, mctx := {}, lctx := lctx, opts := opts } msg
+
+def toMessageData (e : KernelException) (opts : Options) : MessageData :=
+  match e with
+  | unknownConstant env constName       => mkCtx env {} opts m!"(kernel) unknown constant '{constName}'"
+  | alreadyDeclared env constName       => mkCtx env {} opts m!"(kernel) constant has already been declared '{constName}'"
+  | declTypeMismatch env decl givenType =>
+    let process (n : Name) (expectedType : Expr) : MessageData :=
+      m!"(kernel) declaration type mismatch, '{n}' has type{indentExpr givenType}\n, but it is expected to have type{indentExpr expectedType}";
+    match decl with
+    | Declaration.defnDecl { name := n, type := type, .. } => process n type
+    | Declaration.thmDecl { name := n, type := type, .. }  => process n type
+    | _ => "(kernel) declaration type mismatch" -- TODO fix type checker, type mismatch for mutual decls does not have enough information
+  | declHasMVars env constName _        => mkCtx env {} opts m!"(kernel) declaration has metavariables '{constName}'"
+  | declHasFVars env constName _        => mkCtx env {} opts m!"(kernel) declaration has free variables '{constName}'"
+  | funExpected env lctx e              => mkCtx env lctx opts m!"(kernel) function expected{indentExpr e}"
+  | typeExpected env lctx e             => mkCtx env lctx opts m!"(kernel) type expected{indentExpr e}"
+  | letTypeMismatch  env lctx n _ _     => mkCtx env lctx opts m!"(kernel) let-declaration type mismatch '{n}'"
+  | exprTypeMismatch env lctx e _       => mkCtx env lctx opts m!"(kernel) type mismatch at{indentExpr e}"
+  | appTypeMismatch  env lctx e fnType argType =>
+    mkCtx env lctx opts m!"application type mismatch{indentExpr e}\nargument has type{indentExpr argType}\nbut function has type{indentExpr fnType}"
+  | invalidProj env lctx e              => mkCtx env lctx opts m!"(kernel) invalid projection{indentExpr e}"
+  | other msg                           => m!"(kernel) {msg}"
+
+end KernelException
 end Lean

src/Lean/Meta/Match/Basic.lean

@@ -112,8 +112,8 @@ instance : Inhabited Alt := ⟨⟨arbitrary, 0, arbitrary, [], []⟩⟩
 
 partial def toMessageData (alt : Alt) : MetaM MessageData := do
   withExistingLocalDecls alt.fvarDecls do
-    let msg : List MessageData := alt.fvarDecls.map fun d => d.toExpr ++ ":(" ++ d.type ++ ")"
-    let msg : MessageData := msg ++ " |- " ++ (alt.patterns.map Pattern.toMessageData) ++ " => " ++ alt.rhs
+    let msg : List MessageData := alt.fvarDecls.map fun d => m!"{d.toExpr}:({d.type})"
+    let msg : MessageData := m!"{msg} |- {alt.patterns.map Pattern.toMessageData} => {alt.rhs}"
     addMessageContext msg
 
 def applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt :=
@@ -218,7 +218,7 @@ partial def varsToUnderscore : Example → Example
 partial def toMessageData : Example → MessageData
   | var fvarId        => mkFVar fvarId
   | ctor ctorName []  => mkConst ctorName
-  | ctor ctorName exs => "(" ++ mkConst ctorName ++ exs.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil ++ ")"
+  | ctor ctorName exs => m!"({mkConst ctorName}{exs.foldl (fun msg pat => m!"{msg} {toMessageData pat}") Format.nil})"
   | arrayLit exs      => "#" ++ MessageData.ofList (exs.map toMessageData)
   | val e             => e
   | underscore        => "_"
@@ -242,11 +242,8 @@ instance : Inhabited Problem := ⟨{ mvarId := arbitrary, vars := [], alts := []
 def Problem.toMessageData (p : Problem) : MetaM MessageData :=
   withGoalOf p do
     let alts ← p.alts.mapM Alt.toMessageData
-    let vars ← p.vars.mapM fun x => do let xType ← inferType x; pure (x ++ ":(" ++ xType ++ ")" : MessageData)
-    return "remaining variables: " ++ vars
-      ++ Format.line ++ "alternatives:" ++ indentD (MessageData.joinSep alts Format.line)
-      ++ Format.line ++ "examples: " ++ examplesToMessageData p.examples
-      ++ Format.line
+    let vars ← p.vars.mapM fun x => do let xType ← inferType x; pure m!"{x}:({xType})"
+    return m!"remaining variables: {vars}\nalternatives:{indentD (MessageData.joinSep alts Format.line)}\nexamples:{examplesToMessageData p.examples}\n"
 
 abbrev CounterExample := List Example
 

src/Lean/Meta/Match/Match.lean

@@ -564,9 +564,9 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
   let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
   let motiveType ← mkForallFVars majors (mkSort uElimGen)
   withLocalDeclD `motive motiveType fun motive => do
-  trace! `Meta.Match.debug ("motiveType: " ++ motiveType)
+  trace[Meta.Match.debug]! "motiveType: {motiveType}"
   let mvarType  := mkAppN motive majors
-  trace! `Meta.Match.debug ("target: " ++ mvarType)
+  trace[Meta.Match.debug]! "target: {mvarType}"
   withAlts motive lhss fun alts minors => do
     let mvar ← mkFreshExprMVar mvarType
     let examples := majors.toList.map fun major => Example.var major.fvarId!
@@ -574,7 +574,7 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
     let args := #[motive] ++ majors ++ minors.map Prod.fst
     let type ← mkForallFVars args mvarType
     let val  ← mkLambdaFVars args mvar
-    trace! `Meta.Match.debug ("matcher value: " ++ val ++ "\ntype: " ++ type)
+    trace[Meta.Match.debug]! "matcher value: {val}\ntype: {type}"
     /- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example,
        for compiling `src/Init/Data/Int`. It is needed because the compiler uses `Int.decLt`
        for generating code for `Int.casesOn` applications, but `Int.casesOn` is used to
@@ -587,7 +587,7 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
        ```
        which is defined **before** `Int.decLt` -/
     let matcher ← mkAuxDefinition matcherName type val (compile := generateMatcherCode (← getOptions))
-    trace! `Meta.Match.debug ("matcher levels: " ++ toString matcher.getAppFn.constLevels! ++ ", uElim: " ++ toString uElimGen)
+    trace[Meta.Match.debug]! "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
     let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen
     isLevelDefEq uElimGen uElim
     addMatcherInfo matcherName { numParams := matcher.getAppNumArgs, numDiscrs := numDiscrs, altNumParams := minors.map Prod.snd, uElimPos? := uElimPos? }

src/Lean/Meta/SynthInstance.lean

@@ -419,10 +419,10 @@ def resume : SynthM Unit := do
     match (← tryAnswer cNode.mctx mvar answer) with
     | none      => pure ()
     | some mctx =>
-      withMCtx mctx $ traceM `Meta.synthInstance.resume do
+      withMCtx mctx <| traceM `Meta.synthInstance.resume do
         let goal    ← inferType cNode.mvar
         let subgoal ← inferType mvar
-        pure (goal ++ " <== " ++ subgoal)
+        pure m!"{goal} <== {subgoal}"
       consume { key := cNode.key, mvar := cNode.mvar, subgoals := rest, mctx := mctx }
 
 def step : SynthM Bool := do

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -258,7 +258,7 @@ partial def delabFor : Name → Delab
 
 def delab : Delab := do
   let k ← getExprKind
-  delabFor k <|> (liftM $ show MetaM Syntax from throwError $ "don't know how to delaborate '" ++ toString k ++ "'")
+  delabFor k <|> (liftM $ show MetaM Syntax from throwError! "don't know how to delaborate '{k}'")
 
 unsafe def mkAppUnexpanderAttribute : IO (KeyedDeclsAttribute Unexpander) :=
   KeyedDeclsAttribute.init {

src/Lean/PrettyPrinter/Formatter.lean

@@ -65,7 +65,7 @@ unsafe def mkFormatterAttribute : IO (KeyedDeclsAttribute Formatter) :=
         -- `isValidSyntaxNodeKind` is updated only in the next stage for new `[builtin*Parser]`s, but we try to
         -- synthesize a formatter for it immediately, so we just check for a declaration in this case
         if (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id then pure id
-        else throwError ("invalid [formatter] argument, unknown syntax kind '" ++ toString id ++ "'")
+        else throwError! "invalid [formatter] argument, unknown syntax kind '{id}'"
       | none    => throwError "invalid [formatter] argument, expected identifier"
   } `Lean.PrettyPrinter.formatterAttribute
 @[builtinInit mkFormatterAttribute] constant formatterAttribute : KeyedDeclsAttribute Formatter
@@ -175,7 +175,7 @@ def withAntiquot.formatter (antiP p : Formatter) : Formatter :=
 @[combinatorFormatter Lean.Parser.categoryParser]
 def categoryParser.formatter (cat : Name) : Formatter := group $ indent do
   let stx ← getCur
-  trace[PrettyPrinter.format]! "formatting {MessageData.nest 2 (Format.line ++ fmt stx)}"
+  trace[PrettyPrinter.format]! "formatting {indentD (fmt stx)}"
   if stx.getKind == `choice then
     visitArgs do
       -- format only last choice

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -126,7 +126,7 @@ unsafe def mkParenthesizerAttribute : IO (KeyedDeclsAttribute Parenthesizer) :=
         -- `isValidSyntaxNodeKind` is updated only in the next stage for new `[builtin*Parser]`s, but we try to
         -- synthesize a parenthesizer for it immediately, so we just check for a declaration in this case
         if (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id then pure id
-        else throwError ("invalid [parenthesizer] argument, unknown syntax kind '" ++ toString id ++ "'")
+        else throwError! "invalid [parenthesizer] argument, unknown syntax kind '{id}'"
       | none    => throwError "invalid [parenthesizer] argument, expected identifier"
   } `Lean.PrettyPrinter.parenthesizerAttribute
 @[builtinInit mkParenthesizerAttribute] constant parenthesizerAttribute : KeyedDeclsAttribute Parenthesizer
@@ -149,7 +149,7 @@ unsafe def mkCategoryParenthesizerAttribute : IO (KeyedDeclsAttribute CategoryPa
       match attrParamSyntaxToIdentifier args with
       | some id =>
         if Parser.isParserCategory env id then pure id
-        else throwError ("invalid [parenthesizer] argument, unknown parser category '" ++ toString id ++ "'")
+        else throwError! "invalid [parenthesizer] argument, unknown parser category '{toString id}'"
       | none    => throwError "invalid [parenthesizer] argument, expected identifier"
   } `Lean.PrettyPrinter.categoryParenthesizerAttribute
 @[builtinInit mkCategoryParenthesizerAttribute] constant categoryParenthesizerAttribute : KeyedDeclsAttribute CategoryParenthesizer
@@ -208,7 +208,7 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
   let st ← get
   -- reset precs for the recursive call
   set { stxTrav := st.stxTrav : State }
-  trace[PrettyPrinter.parenthesize]! "parenthesizing (cont := {(st.contPrec, st.contCat)}){MessageData.nest 2 (line ++ fmt stx)}"
+  trace[PrettyPrinter.parenthesize]! "parenthesizing (cont := {(st.contPrec, st.contCat)}){indentD (fmt stx)}"
   x
   let { minPrec := some minPrec, trailPrec := trailPrec, trailCat := trailCat, .. } ← get
     | panic! s!"maybeParenthesize: visited a syntax tree without precedences?!{line ++ fmt stx}"
@@ -228,7 +228,7 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
         let stx := (stx.setHeadInfo { hi with trailing := "".toSubstring }).setTailInfo { ti with leading := "".toSubstring }
         setCur stx
       | _, _ => setCur (mkParen stx)
-      let stx ← getCur; trace! `PrettyPrinter.parenthesize ("parenthesized: " ++ stx.formatStx none)
+      let stx ← getCur; trace! `PrettyPrinter.parenthesize m!"parenthesized: {stx.formatStx none}"
       goLeft
       -- after parenthesization, there is no more trailing parser
       modify (fun st => { st with contPrec := Parser.maxPrec, contCat := cat, trailPrec := none })

tests/lean/PPRoundtrip.lean

@@ -23,7 +23,7 @@ match Parser.runParserCategory env `term s "<input>" with
 | Except.ok stx'' => do
   let e' ← elabTermAndSynthesize stx'' none <* throwErrorIfErrors
   unless (← isDefEq e e') do
-    throwErrorAt stx (fmt "failed to round-trip" ++ line ++ fmt e ++ line ++ fmt e')
+    throwErrorAt stx (m!"failed to round-trip" ++ line ++ fmt e ++ line ++ fmt e')
 
 -- set_option trace.PrettyPrinter.parenthesize true
 set_option format.width 20

tests/lean/autoBoundImplicits2.lean.expected.out

@@ -1,10 +1,10 @@
 autoBoundImplicits2.lean:9:0: error: invalid auto implicit argument 'b', it depends on explicitly provided argument 'n'
 g1 : ?m → ?m
-autoBoundImplicits2.lean:30:17: error: unknown universe level u
+autoBoundImplicits2.lean:30:17: error: unknown universe level 'u'
 autoBoundImplicits2.lean:30:37: error: type expected
 failed to synthesize instance
   CoeSort (sorryAx (Sort _)) ?m
-autoBoundImplicits2.lean:33:17: error: unknown universe level β
+autoBoundImplicits2.lean:33:17: error: unknown universe level 'β'
 autoBoundImplicits2.lean:33:90: error: type expected
 failed to synthesize instance
   CoeSort (sorryAx (Sort _)) ?m

tests/lean/doSeqRightIssue.lean.expected.out

@@ -1 +1 @@
-doSeqRightIssue.lean:5:24: error: unknown universe level v
+doSeqRightIssue.lean:5:24: error: unknown universe level 'v'

tests/lean/run/choiceMacroRules.lean

@@ -5,7 +5,7 @@ macro_rules [myAdd1]
 | `($a +++ $b) => `(Nat.add $a $b)
 
 macro_rules [myAdd2]
-| `($a +++ $b) => `($a ++ $b)
+| `($a +++ $b) => `(Append.append $a $b)
 
 #check (1:Nat) +++ 3
 
@@ -18,10 +18,3 @@ rfl
 
 theorem tst2 : ([1, 2] +++ [3, 4]) = [1, 2] ++ [3, 4] :=
 rfl
-
-syntax:65 [myAdd3] term "++" term:65 : term
-
-macro_rules [myAdd3]
-| `($a ++ $b) => `($a + $b)
-
-#check (1:Nat) ++ 2

tests/lean/run/depElim1.lean

@@ -170,7 +170,7 @@ withDepElimFrom ex numPats fun majors alts => do
   unless r.counterExamples.isEmpty do
     throwError m!"missing cases:\n{counterExamplesToMessageData r.counterExamples}"
   unless r.unusedAltIdxs.isEmpty do
-    throwError ("unused alternatives: " ++ toString (r.unusedAltIdxs.map fun idx => "#" ++ toString (idx+1)))
+    throwError (m!"unused alternatives: " ++ toString (r.unusedAltIdxs.map fun idx => "#" ++ toString (idx+1)))
   let cinfo ← getConstInfo elimName
   IO.println (toString cinfo.name ++ " : " ++ toString cinfo.type)
   pure ()

tests/lean/run/meta7.lean

@@ -86,7 +86,7 @@ let ⟨zId, nId, subst⟩ ← assertAfter m.mvarId! x.fvarId! `z nat val;
 print m;
 print (← ppGoal nId);
 withMVarContext nId do {
-  print (subst.apply x ++ " " ++ subst.apply y ++ " " ++ mkFVar zId);
+  print m!"{subst.apply x} {subst.apply y} {mkFVar zId}";
   assignExprMVar nId (← mkAppM `Add.add #[subst.apply x, mkFVar zId]);
   print (mkMVar nId)
 };
@@ -127,7 +127,7 @@ let ⟨zId, nId, subst⟩ ← assertAfter m.mvarId! y.fvarId! `z nat val;
 print m;
 print (← ppGoal nId);
 withMVarContext nId do {
-  print (subst.apply x ++ " " ++ subst.apply y ++ " " ++ mkFVar zId);
+  print m!"{subst.apply x} {subst.apply y} {mkFVar zId}";
   assignExprMVar nId (← mkAppM `Add.add #[subst.apply x, mkFVar zId]);
   print (mkMVar nId)
 };

tests/lean/run/overloaded.lean

@@ -10,7 +10,7 @@ open B
 #check g x
 
 macro "foo!" x:term : term => `($x + (1:Nat))
-macro "foo!" x:term : term => `($x ++ " world")
+macro "foo!" x:term : term => `(Append.append $x " world")
 
 #check f (foo! 1)
 #check g (foo! "hello")

tests/lean/run/termElab.lean

@@ -10,7 +10,7 @@ let opt ← getOptions;
 let stx ← `(forall (a b : Nat), Nat);
 IO.println "message 1"; -- This message goes direct to stdio. It will be displayed before trace messages.
 let e ← elabTermAndSynthesize stx none;
-logDbgTrace (">>> " ++ e); -- display message when `trace.Elab.debug` is true
+logDbgTrace m!">>> {e}"; -- display message when `trace.Elab.debug` is true
 IO.println "message 2"
 
 #eval tst1
@@ -21,7 +21,7 @@ let a := mkIdent `a;
 let b := mkIdent `b;
 let stx ← `((fun ($a : Type) (x : $a) => @id $a x) _ 1);
 let e ← elabTermAndSynthesize stx none;
-logDbgTrace (">>> " ++ e);
+logDbgTrace m!">>> {e}";
 throwErrorIfErrors
 
 #eval tst2

tests/lean/run/trace.lean

@@ -9,7 +9,7 @@ structure MyState :=
 abbrev M := CoreM
 
 def tst1 : M Unit :=
-do trace! `module ("hello" ++ MessageData.nest 9 (Format.line ++ "world"));
+do trace! `module (m!"hello" ++ MessageData.nest 9 (m!"\n" ++ "world"));
    trace! `module.aux "another message";
    pure ()
 
@@ -37,7 +37,7 @@ do traceCtx `module $ do {
    trace! `bughunt "at end of tst3";
    -- Messages are computed lazily. The following message will only be computed
    -- if `trace.slow is active.
-   trace! `slow ("slow message: " ++ toString (slow b))
+   trace! `slow (m!"slow message: " ++ toString (slow b))
 
 def run (x : M Unit) : M Unit :=
 withReader