chore: changes to placate coercions

src/Init/NotationExtra.lean

@@ -170,7 +170,7 @@ macro_rules
 macro_rules
   | `(%[ $[$x],* | $k ]) =>
     if x.size < 8 then
-      x.foldrM (init := k) fun x k =>
+      x.foldrM (β := TSyntax `term) (init := k) fun x k =>
         `(List.cons $x $k)
     else
       let m := x.size / 2

src/Lean/Elab/Deriving/Repr.lean

@@ -58,7 +58,7 @@ where
         for _ in [:indVal.numIndices] do
           patterns := patterns.push (← `(_))
         let mut ctorArgs := #[]
-        let mut rhs := Syntax.mkStrLit (toString ctorInfo.name)
+        let mut rhs : TSyntax `term := Syntax.mkStrLit (toString ctorInfo.name)
         rhs ← `(Format.text $rhs)
         -- add `_` for inductive parameters, they are inaccessible
         for _ in [:indVal.numParams] do

src/Lean/Elab/ElabRules.lean

@@ -88,9 +88,9 @@ def elabElab : CommandElab
     let name ← match name? with
       | some name => pure name.getId
       | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-    let pat := mkNode ((← getCurrNamespace) ++ name) patArgs
-    `($[$doc?:docComment]? $attrKind:attrKind syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat
-      $[$doc?:docComment]? elab_rules : $cat $[<= $expectedType?]? | `($pat) => $rhs) >>= elabCommand
+    let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩
+    `($[$doc?:docComment]? $attrKind:attrKind syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio):num) $[$stxParts]* : $cat
+      $[$doc?:docComment]? elab_rules : $cat $[<= $expectedType?]? | `($pat) => $rhs) >>= (elabCommand ·)
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Command

src/Lean/Elab/Quotation.lean

@@ -47,7 +47,7 @@ private def getSepFromSplice (splice : Syntax) : String :=
 private def getSepStxFromSplice (splice : Syntax) : Syntax := Unhygienic.run do
   match getSepFromSplice splice with
   | "" => `(mkNullNode) -- sepByIdent uses the null node for separator-less enumerations
-  | sep => `(mkAtom $(.mkStrLit sep))
+  | sep => `(mkAtom $(Syntax.mkStrLit sep))
 
 partial def mkTuple : Array Syntax → TermElabM Syntax
   | #[]  => `(Unit.unit)
@@ -151,7 +151,7 @@ private partial def quoteSyntax : Syntax → TermElabM (TSyntax `term)
                 | $[some $ids:ident],* => $(quote inner)
                 | $[_%$ids],*          => Array.empty)
             | _ =>
-              let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id $arr)) ids.back
+              let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back
               `(Array.map (fun $(← mkTuple ids) => $(inner[0])) $arr)
           let arr ← if k == `sepBy then
             `(mkSepArray $arr $(getSepStxFromSplice arg))

src/Lean/Hygiene.lean

@@ -95,9 +95,10 @@ def sanitizeName (userName : Name) : StateM NameSanitizerState Name := do
 
 private partial def sanitizeSyntaxAux : Syntax → StateM NameSanitizerState Syntax
   | stx@(Syntax.ident _ _ n _) => do
-    mkIdentFrom stx <$> match (← get).userName2Sanitized.find? n with
-    | some n' => pure n'
-    | none    => if n.hasMacroScopes then sanitizeName n else pure n
+    let n ← match (← get).userName2Sanitized.find? n with
+      | some n' => pure n'
+      | none    => if n.hasMacroScopes then sanitizeName n else pure n
+    return mkIdentFrom stx n
   | Syntax.node info k args => Syntax.node info k <$> args.mapM sanitizeSyntaxAux
   | stx => pure stx
 

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -274,7 +274,7 @@ def delabAppImplicit : Delab := do
               let v := param.defVal.get!
               if !v.hasLooseBVars && v == arg then pure none else delab
             else if !param.isRegularExplicit && param.defVal.isNone then
-              if ← getPPOption getPPAnalysisNamedArg <||> (pure (param.name == `motive) <&&> shouldShowMotive arg opts) then mkNamedArg param.name (← delab) else pure none
+              if ← getPPOption getPPAnalysisNamedArg <||> (pure (param.name == `motive) <&&> shouldShowMotive arg opts) then some <$> mkNamedArg param.name (← delab) else pure none
             else delab
       let argStxs := match argStx? with
         | none => argStxs

src/Lean/Server/Rpc/Deriving.lean

@@ -229,7 +229,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
       -- helpers for type name syntax
       let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
       let typeId := Syntax.mkApp (← `(@$(mkIdent indVal.name))) paramIds
-      let packetAppliedId := Syntax.mkApp (mkIdent packetNm) (st.uniqEncArgTypes.map mkIdent)
+      let packetAppliedId := Syntax.mkApp (mkIdent packetNm) (st.uniqEncArgTypes.map (mkIdent ·))
 
       `(variable $st.binders*