perf: simdutf8

This PR adds two validation checks to `addInstance` that provide early
feedback for common mistakes in instance declarations:

1. **Non-class instance check**: errors when an instance target type is
not a type class. This catches the common mistake of writing `instance`
for a plain structure. Previously handled by the `nonClassInstance`
linter in Batteries (`Batteries.Tactic.Lint.TypeClass`), this is now
checked directly at declaration time.

2. **Impossible argument check**: errors when an instance has arguments
that cannot be inferred by instance synthesis. Specifically, it flags
arguments that are not instance-implicit and do not appear in any
subsequent instance-implicit argument or in the return type. Previously
such instances would be silently accepted but could never be
synthesised.

Supersedes #13237 and #13333.

src/Init/Data/Order/LemmasExtra.lean

@@ -87,7 +87,7 @@ public theorem IsLinearOrder.of_ord {α : Type u} [LE α] [Ord α] [LawfulOrderO
 /--
 This lemma derives a `LawfulOrderLT α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [LawfulOrderOrd α]
     (lt_iff_compare_eq_lt : ∀ a b : α, a < b ↔ compare a b = .lt) :
     LawfulOrderLT α where
   lt_iff a b := by
@@ -96,7 +96,7 @@ public instance LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [Law
 /--
 This lemma derives a `LawfulOrderBEq α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [LawfulOrderOrd α]
     (beq_iff_compare_eq_eq : ∀ a b : α, a == b ↔ compare a b = .eq) :
     LawfulOrderBEq α where
   beq_iff_le_and_ge := by
@@ -105,7 +105,7 @@ public instance LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderInf α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
     (compare_min_isLE_iff : ∀ a b c : α,
         (compare a (min b c)).isLE ↔ (compare a b).isLE ∧ (compare a c).isLE) :
     LawfulOrderInf α where
@@ -114,7 +114,7 @@ public instance LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderMin α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
     (compare_min_isLE_iff : ∀ a b c : α,
         (compare a (min b c)).isLE ↔ (compare a b).isLE ∧ (compare a c).isLE)
     (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
@@ -125,7 +125,7 @@ public instance LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderSup α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
     (compare_max_isLE_iff : ∀ a b c : α,
         (compare (max a b) c).isLE ↔ (compare a c).isLE ∧ (compare b c).isLE) :
     LawfulOrderSup α where
@@ -134,7 +134,7 @@ public instance LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderMax α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderMax.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderMax.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
     (compare_max_isLE_iff : ∀ a b c : α,
         (compare (max a b) c).isLE ↔ (compare a c).isLE ∧ (compare b c).isLE)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :

src/Init/While.lean

@@ -35,21 +35,23 @@ instance [Monad m] : ForIn m Loop Unit where
 syntax "repeat " doSeq : doElem
 
 macro_rules
-  | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
+  | `(doElem| repeat%$tk $seq) => `(doElem| for%$tk _ in Loop.mk do $seq)
 
 syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
 
 macro_rules
-  | `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h:ident : $cond then $seq else break)
+  | `(doElem| while%$tk $h : $cond do $seq) =>
+    `(doElem| repeat%$tk if $h:ident : $cond then $seq else break)
 
 syntax "while " termBeforeDo " do " doSeq : doElem
 
 macro_rules
-  | `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
+  | `(doElem| while%$tk $cond do $seq) => `(doElem| repeat%$tk if $cond then $seq else break)
 
 syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
 
 macro_rules
-  | `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
+  | `(doElem| repeat%$tk $seq until $cond) =>
+    `(doElem| repeat%$tk do $seq:doSeq; if $cond then break)
 
 end Lean

src/Lean/Compiler/LCNF/ExpandResetReuse.lean

@@ -90,6 +90,22 @@ partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (Cod
         | break
       if !(w == z && targetId == x) then
         break
+      if mask[i]!.isSome then
+        /-
+        Suppose we encounter a situation like
+        ```
+        let x.1 := proj[0] y
+        inc x.1
+        let x.2 := proj[0] y
+        inc x.2
+        ```
+        The `inc x.2` will already have been removed. If we don't perform this check we will also
+        remove `inc x.1` and have effectively removed two refcounts while only one was legal.
+        -/
+        keep := keep.push d
+        keep := keep.push d'
+        ds := ds.pop.pop
+        continue
       /-
       Found
       ```

src/Lean/Elab/BuiltinDo/Basic.lean

@@ -21,7 +21,8 @@ def elabDoIdDecl (x : Ident) (xType? : Option Term) (rhs : TSyntax `doElem) (k :
   let xType ← Term.elabType (xType?.getD (mkHole x))
   let lctx ← getLCtx
   let ctx ← read
-  elabDoElem rhs <| .mk (kind := kind) x.getId xType do
+  let ref ← getRef -- store the surrounding reference for error messages in `k`
+  elabDoElem rhs <| .mk (kind := kind) x.getId xType do withRef ref do
     withLCtxKeepingMutVarDefs lctx ctx x.getId do
       Term.addLocalVarInfo x (← getFVarFromUserName x.getId)
       k

src/Lean/Elab/BuiltinDo/For.lean

@@ -23,7 +23,7 @@ open Lean.Meta
   | `(doFor| for $[$_ : ]? $_:ident in $_ do $_) =>
     -- This is the target form of the expander, handled by `elabDoFor` below.
     Macro.throwUnsupported
-  | `(doFor| for $decls:doForDecl,* do $body) =>
+  | `(doFor| for%$tk $decls:doForDecl,* do $body) =>
     let decls := decls.getElems
     let `(doForDecl| $[$h? : ]? $pattern in $xs) := decls[0]! | Macro.throwUnsupported
     let mut doElems := #[]
@@ -74,12 +74,13 @@ open Lean.Meta
           | some ($y, s') =>
             $s:ident := s'
             do $body)
-    doElems := doElems.push (← `(doSeqItem| for $[$h? : ]? $x:ident in $xs do $body))
+    doElems := doElems.push (← `(doSeqItem| for%$tk $[$h? : ]? $x:ident in $xs do $body))
     `(doElem| do $doElems*)
   | _ => Macro.throwUnsupported
 
 @[builtin_doElem_elab Lean.Parser.Term.doFor] def elabDoFor : DoElab := fun stx dec => do
-  let `(doFor| for $[$h? : ]? $x:ident in $xs do $body) := stx | throwUnsupportedSyntax
+  let `(doFor| for%$tk $[$h? : ]? $x:ident in $xs do $body) := stx | throwUnsupportedSyntax
+  let dec ← dec.ensureUnitAt tk
   checkMutVarsForShadowing #[x]
   let uα ← mkFreshLevelMVar
   let uρ ← mkFreshLevelMVar
@@ -124,9 +125,6 @@ open Lean.Meta
       defs := defs.push (mkConst ``Unit.unit)
     return defs
 
-  unless ← isDefEq dec.resultType (← mkPUnit) do
-    logError m!"Type mismatch. `for` loops have result type {← mkPUnit}, but the rest of the `do` sequence expected {dec.resultType}."
-
   let (preS, σ) ← mkProdMkN (← useLoopMutVars none) mi.u
 
   let (app, p?) ← match h? with

src/Lean/Elab/BuiltinDo/If.lean

@@ -17,6 +17,7 @@ namespace Lean.Elab.Do
 open Lean.Parser.Term
 open Lean.Meta
 
+open InternalSyntax in
 /--
 If the given syntax is a `doIf`, return an equivalent `doIf` that has an `else` but no `else if`s or
 `if let`s.
@@ -25,8 +26,8 @@ If the given syntax is a `doIf`, return an equivalent `doIf` that has an `else`
   match stx with
   | `(doElem|if $_:doIfProp then $_ else $_) =>
     Macro.throwUnsupported
-  | `(doElem|if $cond:doIfCond then $t $[else if $conds:doIfCond then $ts]* $[else $e?]?) => do
-    let mut e : Syntax ← e?.getDM `(doSeq|pure PUnit.unit)
+  | `(doElem|if%$tk $cond:doIfCond then $t $[else if%$tks $conds:doIfCond then $ts]* $[else $e?]?) => do
+    let mut e : Syntax ← e?.getDM `(doSeq| skip%$tk)
     let mut eIsSeq := true
     for (cond, t) in Array.zip (conds.reverse.push cond) (ts.reverse.push t) do
       e ← if eIsSeq then pure e else `(doSeq|$(⟨e⟩):doElem)

src/Lean/Elab/BuiltinDo/Let.lean

@@ -88,17 +88,18 @@ private def checkLetConfigInDo (config : Term.LetConfig) : DoElabM Unit := do
     throwError "`+generalize` is not supported in `do` blocks"
 
 partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl)
-    (dec : DoElemCont) : DoElabM Expr := do
+    (tk : Syntax) (dec : DoElemCont) : DoElabM Expr := do
   checkLetConfigInDo config
   let vars ← getLetDeclVars decl
   letOrReassign.checkMutVars vars
+  let dec ← dec.ensureUnitAt tk
   -- Some decl preprocessing on the patterns and expected types:
   let decl ← pushTypeIntoReassignment letOrReassign decl
   let mγ ← mkMonadicType (← read).doBlockResultType
   match decl with
   | `(letDecl| $decl:letEqnsDecl) =>
     let declNew ← `(letDecl| $(⟨← liftMacroM <| Term.expandLetEqnsDecl decl⟩):letIdDecl)
-    return ← Term.withMacroExpansion decl declNew <| elabDoLetOrReassign config letOrReassign declNew dec
+    return ← Term.withMacroExpansion decl declNew <| elabDoLetOrReassign config letOrReassign declNew tk dec
   | `(letDecl| $pattern:term $[: $xType?]? := $rhs) =>
     let rhs ← match xType? with | some xType => `(($rhs : $xType)) | none => pure rhs
     let contElab : DoElabM Expr := elabWithReassignments letOrReassign vars dec.continueWithUnit
@@ -162,10 +163,11 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
             mkLetFVars #[x, h'] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
   | _ => throwUnsupportedSyntax
 
-def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``doPatDecl]) (dec : DoElemCont) : DoElabM Expr := do
+def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``doPatDecl]) (tk : Syntax) (dec : DoElemCont) : DoElabM Expr := do
   match stx with
   | `(doIdDecl| $x:ident $[: $xType?]? ← $rhs) =>
     letOrReassign.checkMutVars #[x]
+    let dec ← dec.ensureUnitAt tk
     -- For plain variable reassignment, we know the expected type of the reassigned variable and
     -- propagate it eagerly via type ascription if the user hasn't provided one themselves:
     let xType? ← match letOrReassign, xType? with
@@ -177,6 +179,7 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
       (kind := dec.kind)
   | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
+    let dec ← dec.ensureUnitAt tk
     elabDoIdDecl x patType? rhs dec.continueWithUnit (kind := dec.kind)
   | `(doPatDecl| $pattern:term $[: $patType?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
     let rest? := rest?.join
@@ -205,17 +208,18 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   Term.mkLetConfig letConfigStx initConfig
 
 @[builtin_doElem_elab Lean.Parser.Term.doLet] def elabDoLet : DoElab := fun stx dec => do
-  let `(doLet| let $[mut%$mutTk?]? $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
+  let `(doLet| let%$tk $[mut%$mutTk?]? $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
   let config ← getLetConfigAndCheckMut config mutTk?
-  elabDoLetOrReassign config (.let mutTk?) decl dec
+  elabDoLetOrReassign config (.let mutTk?) decl tk dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doHave] def elabDoHave : DoElab := fun stx dec => do
-  let `(doHave| have $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
+  let `(doHave| have%$tk $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
   let config ← Term.mkLetConfig config { nondep := true }
-  elabDoLetOrReassign config .have decl dec
+  elabDoLetOrReassign config .have decl tk dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetRec] def elabDoLetRec : DoElab := fun stx dec => do
-  let `(doLetRec| let rec $decls:letRecDecls) := stx | throwUnsupportedSyntax
+  let `(doLetRec| let%$tk rec $decls:letRecDecls) := stx | throwUnsupportedSyntax
+  let dec ← dec.ensureUnitAt tk
   let vars ← getLetRecDeclsVars decls
   let mγ ← mkMonadicType (← read).doBlockResultType
   doElabToSyntax m!"let rec body of group {vars}" dec.continueWithUnit fun body => do
@@ -227,13 +231,13 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
 @[builtin_doElem_elab Lean.Parser.Term.doReassign] def elabDoReassign : DoElab := fun stx dec => do
   -- def doReassign := letIdDeclNoBinders <|> letPatDecl
   match stx with
-  | `(doReassign| $x:ident $[: $xType?]? := $rhs) =>
+  | `(doReassign| $x:ident $[: $xType?]? :=%$tk $rhs) =>
     let decl : TSyntax ``letIdDecl ← `(letIdDecl| $x:ident $[: $xType?]? := $rhs)
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-    elabDoLetOrReassign {} .reassign decl dec
+    elabDoLetOrReassign {} .reassign decl tk dec
   | `(doReassign| $decl:letPatDecl) =>
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-    elabDoLetOrReassign {} .reassign decl dec
+    elabDoLetOrReassign {} .reassign decl decl dec
   | _ => throwUnsupportedSyntax
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetElse] def elabDoLetElse : DoElab := fun stx dec => do
@@ -255,17 +259,17 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
     elabDoElem (← `(doElem| match $rhs:term with | $pattern => $body:doSeqIndent | _ => $otherwise:doSeqIndent)) dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetArrow] def elabDoLetArrow : DoElab := fun stx dec => do
-  let `(doLetArrow| let $[mut%$mutTk?]? $cfg:letConfig $decl) := stx | throwUnsupportedSyntax
+  let `(doLetArrow| let%$tk $[mut%$mutTk?]? $cfg:letConfig $decl) := stx | throwUnsupportedSyntax
   let config ← getLetConfigAndCheckMut cfg mutTk?
   checkLetConfigInDo config
   if config.nondep || config.usedOnly || config.zeta || config.eq?.isSome then
     throwErrorAt cfg "configuration options are not supported with `←`"
-  elabDoArrow (.let mutTk?) decl dec
+  elabDoArrow (.let mutTk?) decl tk dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do
   match stx with
   | `(doReassignArrow| $decl:doIdDecl) =>
-    elabDoArrow .reassign decl dec
+    elabDoArrow .reassign decl decl dec
   | `(doReassignArrow| $decl:doPatDecl) =>
-    elabDoArrow .reassign decl dec
+    elabDoArrow .reassign decl decl dec
   | _ => throwUnsupportedSyntax

src/Lean/Elab/BuiltinDo/Misc.lean

@@ -16,6 +16,12 @@ namespace Lean.Elab.Do
 open Lean.Parser.Term
 open Lean.Meta
 
+open InternalSyntax in
+@[builtin_doElem_elab Lean.Parser.Term.InternalSyntax.doSkip] def elabDoSkip : DoElab := fun stx dec => do
+  let `(doSkip| skip%$tk) := stx | throwUnsupportedSyntax
+  let dec ← dec.ensureUnitAt tk
+  dec.continueWithUnit
+
 @[builtin_doElem_elab Lean.Parser.Term.doExpr] def elabDoExpr : DoElab := fun stx dec => do
   let `(doExpr| $e:term) := stx | throwUnsupportedSyntax
   let mα ← mkMonadicType dec.resultType
@@ -26,24 +32,28 @@ open Lean.Meta
   let `(doNested| do $doSeq) := stx | throwUnsupportedSyntax
   elabDoSeq ⟨doSeq.raw⟩ dec
 
+open InternalSyntax in
 @[builtin_doElem_elab Lean.Parser.Term.doUnless] def elabDoUnless : DoElab := fun stx dec => do
-  let `(doUnless| unless $cond do $body) := stx | throwUnsupportedSyntax
-  elabDoElem (← `(doElem| if $cond then pure PUnit.unit else $body)) dec
+  let `(doUnless| unless%$tk $cond do $body) := stx | throwUnsupportedSyntax
+  elabDoElem (← `(doElem| if $cond then skip%$tk else $body)) dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doDbgTrace] def elabDoDbgTrace : DoElab := fun stx dec => do
-  let `(doDbgTrace| dbg_trace $msg:term) := stx | throwUnsupportedSyntax
+  let `(doDbgTrace| dbg_trace%$tk $msg:term) := stx | throwUnsupportedSyntax
   let mγ ← mkMonadicType (← read).doBlockResultType
+  let dec ← dec.ensureUnitAt tk
   doElabToSyntax "dbg_trace body" dec.continueWithUnit fun body => do
   Term.elabTerm (← `(dbg_trace $msg; $body)) mγ
 
 @[builtin_doElem_elab Lean.Parser.Term.doAssert] def elabDoAssert : DoElab := fun stx dec => do
-  let `(doAssert| assert! $cond) := stx | throwUnsupportedSyntax
+  let `(doAssert| assert!%$tk $cond) := stx | throwUnsupportedSyntax
   let mγ ← mkMonadicType (← read).doBlockResultType
+  let dec ← dec.ensureUnitAt tk
   doElabToSyntax "assert! body" dec.continueWithUnit fun body => do
   Term.elabTerm (← `(assert! $cond; $body)) mγ
 
 @[builtin_doElem_elab Lean.Parser.Term.doDebugAssert] def elabDoDebugAssert : DoElab := fun stx dec => do
-  let `(doDebugAssert| debug_assert! $cond) := stx | throwUnsupportedSyntax
+  let `(doDebugAssert| debug_assert!%$tk $cond) := stx | throwUnsupportedSyntax
   let mγ ← mkMonadicType (← read).doBlockResultType
+  let dec ← dec.ensureUnitAt tk
   doElabToSyntax "debug_assert! body" dec.continueWithUnit fun body => do
   Term.elabTerm (← `(debug_assert! $cond; $body)) mγ

src/Lean/Elab/Deriving/Basic.lean

@@ -220,7 +220,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             instName ← liftMacroM <| mkUnusedBaseName instName
             if isPrivateName declName then
               instName := mkPrivateName env instName
-            let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
+            let isMeta := (← read).isMetaSection || isMarkedMeta (← getEnv) declName
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
                 wrapInstance result.instVal result.instType
@@ -255,11 +255,12 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             logInfoAt cmdRef m!"Try this: {newText}"
         throwError "failed to derive instance because it depends on \
           `{.ofConstName noncompRef}`, which is noncomputable"
+    let isMeta := (← read).isMetaSection || isMarkedMeta (← getEnv) declName
     if isNoncomputable || (← read).isNoncomputableSection then
       addDecl <| Declaration.defnDecl decl
       modifyEnv (addNoncomputable · instName)
     else
-      addAndCompile <| Declaration.defnDecl decl
+      addAndCompile (Declaration.defnDecl decl) (markMeta := isMeta)
   trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`"
   -- For Prop-typed instances (theorems), skip `implicit_reducible` since reducibility hints are
   -- irrelevant for theorems. This matches the behavior of the handwritten `instance` command

src/Lean/Elab/Do/Basic.lean

@@ -374,14 +374,60 @@ def withLCtxKeepingMutVarDefs (oldLCtx : LocalContext) (oldCtx : Context) (resul
     mutVarDefs := oldMutVarDefs
   }) k
 
+def mkMonadicResultTypeMismatchError (contType : Expr) (elementType : Expr) : MessageData :=
+  m!"Type mismatch. The `do` element has monadic result type{indentExpr elementType}\n\
+    but the rest of the `do` block has monadic result type{indentExpr contType}"
+
+/--
+Given a continuation `dec`, a reference `ref`, and an element result type `elementType`, returns a
+continuation derived from `dec` with result type `elementType`.
+If `dec` already has result type `elementType`, simply returns `dec`.
+Otherwise, an error is logged and a new continuation is returned that calls `dec` with `sorry` as a
+result. The error is reported at `ref`.
+-/
+def DoElemCont.ensureHasTypeAt (dec : DoElemCont) (ref : Syntax) (elementType : Expr) : DoElabM DoElemCont := do
+  if ← isDefEqGuarded dec.resultType elementType then
+    return dec
+  let errMessage := mkMonadicResultTypeMismatchError dec.resultType elementType
+  unless (← readThe Term.Context).errToSorry do
+    throwErrorAt ref errMessage
+  logErrorAt ref errMessage
+  return {
+    resultName := ← mkFreshUserName `__r
+    resultType := elementType
+    k := do
+      mapLetDecl dec.resultName dec.resultType (← mkSorry dec.resultType true)
+          (nondep := true) (kind := .implDetail) fun _ => dec.k
+    kind := dec.kind
+  }
+
+/--
+Given a continuation `dec` and a reference `ref`, returns a continuation derived from `dec` with result type `PUnit`.
+If `dec` already has result type `PUnit`, simply returns `dec`. Otherwise, an error is logged and a
+new continuation is returned that calls `dec` with `sorry` as a result. The error is reported at `ref`.
+-/
+def DoElemCont.ensureUnitAt (dec : DoElemCont) (ref : Syntax) : DoElabM DoElemCont := do
+  dec.ensureHasTypeAt ref (← mkPUnit)
+
+/--
+Given a continuation `dec`, returns a continuation derived from `dec` with result type `PUnit`.
+If `dec` already has result type `PUnit`, simply returns `dec`. Otherwise, an error is logged and a
+new continuation is returned that calls `dec` with `sorry` as a result.
+-/
+def DoElemCont.ensureUnit (dec : DoElemCont) : DoElabM DoElemCont := do
+  dec.ensureUnitAt (← getRef)
+
 /--
 Return `$e >>= fun ($dec.resultName : $dec.resultType) => $(← dec.k)`, cancelling
 the bind if `$(← dec.k)` is `pure $dec.resultName` or `e` is some `pure` computation.
 -/
 def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr := do
+  -- let eResultTy ← mkFreshResultType
+  -- let e ← Term.ensureHasType (← mkMonadicType eResultTy) e
+  -- let dec ← dec.ensureHasType eResultTy
   let x := dec.resultName
-  let eResultTy := dec.resultType
   let k := dec.k
+  let eResultTy := dec.resultType
   -- The .ofBinderName below is mainly to interpret `__do_lift` binders as implementation details.
   let declKind := .ofBinderName x
   let kResultTy ← mkFreshResultType `kResultTy
@@ -421,9 +467,8 @@ Return `let $k.resultName : PUnit := PUnit.unit; $(← k.k)`, ensuring that the
 is `PUnit` and then immediately zeta-reduce the `let`.
 -/
 def DoElemCont.continueWithUnit (dec : DoElemCont) : DoElabM Expr := do
-  let unit ← mkPUnitUnit
-  discard <| Term.ensureHasType dec.resultType unit
-  mapLetDeclZeta dec.resultName (← mkPUnit) unit (nondep := true) (kind := .ofBinderName dec.resultName) fun _ =>
+  let dec ← dec.ensureUnit
+  mapLetDeclZeta dec.resultName (← mkPUnit) (← mkPUnitUnit) (nondep := true) (kind := .ofBinderName dec.resultName) fun _ =>
     dec.k
 
 /-- Elaborate the `DoElemCont` with the `deadCode` flag set to `deadSyntactically` to emit warnings. -/
@@ -604,6 +649,7 @@ def enterFinally (resultType : Expr) (k : DoElabM Expr) : DoElabM Expr := do
 /-- Extracts `MonadInfo` and monadic result type `α` from the expected type of a `do` block `m α`. -/
 private partial def extractMonadInfo (expectedType? : Option Expr) : Term.TermElabM (MonadInfo × Expr) := do
   let some expectedType := expectedType? | mkUnknownMonadResult
+  let expectedType ← instantiateMVars expectedType
   let extractStep? (type : Expr) : Term.TermElabM (Option (MonadInfo × Expr)) := do
     let .app m resultType := type.consumeMData | return none
     unless ← isType resultType do return none

src/Lean/Elab/Do/InferControlInfo.lean

@@ -79,6 +79,7 @@ builtin_initialize controlInfoElemAttribute : KeyedDeclsAttribute ControlInfoHan
 
 namespace InferControlInfo
 
+open InternalSyntax in
 mutual
 
 partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
@@ -152,6 +153,7 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     let finInfo ← ofOptionSeq finSeq?
     return info.sequence finInfo
   -- Misc
+  | `(doElem| skip) => return .pure
   | `(doElem| dbg_trace $_) => return .pure
   | `(doElem| assert! $_) => return .pure
   | `(doElem| debug_assert! $_) => return .pure

src/Lean/Elab/Do/Legacy.lean

@@ -1815,6 +1815,13 @@ mutual
               return mkTerminalAction term
             else
               return mkSeq term (← doSeqToCode doElems)
+          else if k == ``Parser.Term.InternalSyntax.doSkip then
+            -- In the legacy elaborator, `skip` is treated as `pure PUnit.unit`.
+            let term ← withRef doElem `(pure PUnit.unit)
+            if doElems.isEmpty then
+              return mkTerminalAction term
+            else
+              return mkSeq term (← doSeqToCode doElems)
           else
             throwError "unexpected do-element of kind {doElem.getKind}:\n{doElem}"
 end

src/Lean/Elab/Idbg.lean

@@ -364,8 +364,9 @@ def elabIdbgTerm : TermElab := fun stx expectedType? => do
 
 @[builtin_doElem_elab Lean.Parser.Term.doIdbg]
 def elabDoIdbg : DoElab := fun stx dec => do
-  let `(Lean.Parser.Term.doIdbg| idbg $e) := stx | throwUnsupportedSyntax
+  let `(Lean.Parser.Term.doIdbg| idbg%$tk $e) := stx | throwUnsupportedSyntax
   let mγ ← mkMonadicType (← read).doBlockResultType
+  let dec ← dec.ensureUnitAt tk
   doElabToSyntax "idbg body" dec.continueWithUnit fun body => do
     elabIdbgCore (e := e) (body := body) (ref := stx) mγ
 

src/Lean/Elab/Inductive.lean

@@ -73,6 +73,8 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoi
         throwError "Constructor cannot be `protected` because it is in a `private` inductive datatype"
       checkValidCtorModifier ctorModifiers
       let ctorName := ctor.getIdAt 3
+      if ctorName.hasMacroScopes && isCoinductive then
+        throwError "Coinductive predicates are not allowed inside of macro scopes"
       let ctorName := declName ++ ctorName
       let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
       let (binders, type?) := expandOptDeclSig ctor[4]

src/Lean/Meta/Instances.lean

@@ -229,8 +229,33 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
 
   return synthed
 
+def checkImpossibleInstance (c : Expr) : MetaM Unit := do
+  let cTy ← inferType c
+  forallTelescopeReducing cTy fun args ty => do
+    let argTys ← args.mapM inferType
+    let impossibleArgs ← args.zipIdx.filterMapM fun (arg, i) => do
+      let fv := arg.fvarId!
+      if (← fv.getDecl).binderInfo.isInstImplicit then return none
+      if ty.containsFVar fv then return none
+      if argTys[i+1:].any (·.containsFVar fv) then return none
+      return some m!"{arg} : {← inferType arg}"
+    if impossibleArgs.isEmpty then return
+    let impossibleArgs := MessageData.joinSep impossibleArgs.toList ", "
+    throwError m!"Instance {c} has arguments "
+      ++ impossibleArgs
+      ++ " that are impossible to infer. Those arguments are not instance-implicit and do not appear in another instance-implicit argument or the return type."
+
+def checkNonClassInstance (declName : Name) (c : Expr) : MetaM Unit := do
+  let type ← inferType c
+  forallTelescopeReducing type fun _ target => do
+    unless (← isClass? target).isSome do
+      unless target.isSorry do
+      throwError m!"instance `{declName}` target `{target}` is not a type class."
+
 def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
   let c ← mkConstWithLevelParams declName
+  checkImpossibleInstance c
+  checkNonClassInstance declName c
   let keys ← mkInstanceKey c
   let status ← getReducibilityStatus declName
   unless status matches .reducible | .implicitReducible do

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -51,7 +51,7 @@ register_builtin_option debug.tactic.simp.checkDefEqAttr : Bool := {
 }
 
 register_builtin_option warning.simp.varHead : Bool := {
-  defValue := false
+  defValue := true
   descr := "If true, warns when the head symbol of the left-hand side of a `@[simp]` theorem \
     is a variable. Such lemmas are tried on every simp step, which can be slow."
 }

src/Std/Data/DHashMap/RawDecidableEquiv.lean

@@ -18,7 +18,7 @@ open Std.DHashMap.Internal
 
 namespace Std.DHashMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+def instDecidableEquiv {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   Raw₀.decidableEquiv ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ h₁ h₂
 
 end Std.DHashMap.Raw

src/Std/Data/DTreeMap/Raw/DecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.DTreeMap.Internal.Impl
 
 namespace Std.DTreeMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+def instDecidableEquiv {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := decidableEquiv t₁.1 t₂.1 h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

src/Std/Data/HashMap/RawDecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.DHashMap.Raw
 
 namespace Std.HashMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Hashable α] [BEq β] [LawfulBEq β] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+def instDecidableEquiv {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Hashable α] [BEq β] [LawfulBEq β] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   let : Decidable (m₁.1 ~m m₂.1) := DHashMap.Raw.instDecidableEquiv h₁.out h₂.out;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
 

src/Std/Data/HashSet/RawDecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.HashMap.Raw
 
 namespace Std.HashSet.Raw
 
-instance instDecidableEquiv {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+def instDecidableEquiv {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   let : Decidable (m₁.1 ~m m₂.1) := HashMap.Raw.instDecidableEquiv h₁.out h₂.out;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
 

src/Std/Data/TreeMap/Raw/DecidableEquiv.lean

@@ -20,7 +20,7 @@ open Std.DTreeMap.Raw
 
 namespace Std.TreeMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+def instDecidableEquiv {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := DTreeMap.Raw.instDecidableEquiv h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

src/Std/Data/TreeSet/Raw/DecidableEquiv.lean

@@ -20,7 +20,7 @@ open Std.TreeMap.Raw
 
 namespace Std.TreeSet.Raw
 
-instance instDecidableEquiv {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+def instDecidableEquiv {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := TreeMap.Raw.instDecidableEquiv h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

src/lake/Lake/Util/Family.lean

@@ -154,6 +154,7 @@ public class FamilyOut {α : Type u} {β : Type v} (f : α → β) (a : α) (b :
 -- Simplifies proofs involving open type families.
 -- Scoped to avoid slowing down `simp` in downstream projects (the discrimination
 -- tree key is `_`, so it would be attempted on every goal).
+set_option warning.simp.varHead false in
 attribute [scoped simp] FamilyOut.fam_eq
 
 public instance [FamilyDef f a b] : FamilyOut f a b where

src/runtime/CMakeLists.txt

@@ -5,6 +5,7 @@ set(
   mpz.cpp
   utf8.cpp
   object.cpp
+  simdutf.cpp
   apply.cpp
   exception.cpp
   interrupt.cpp

src/runtime/io.cpp

@@ -752,6 +752,7 @@ extern "C" LEAN_EXPORT obj_res lean_windows_get_next_transition(b_obj_arg timezo
     u_strToUTF8(dst_name, sizeof(dst_name), &dst_name_len, tzID, tzIDLength, &status);
 
     if (U_FAILURE(status)) {
+        ucal_close(cal);
         return lean_io_result_mk_error(lean_mk_io_error_invalid_argument(EINVAL, mk_string("failed to convert DST name to UTF-8")));
     }
 
@@ -1397,7 +1398,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path() {
     memset(dest, 0, PATH_MAX);
     pid_t pid = getpid();
     snprintf(path, PATH_MAX, "/proc/%d/exe", pid);
-    if (readlink(path, dest, PATH_MAX) == -1) {
+    if (readlink(path, dest, PATH_MAX - 1) == -1) {
         return io_result_mk_error("failed to locate application");
     } else {
         return io_result_mk_ok(mk_string(dest));

src/runtime/object.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "runtime/buffer.h"
 #include "runtime/io.h"
 #include "runtime/hash.h"
+#include "simdutf.h"
 
 #if defined(__GLIBC__) || defined(__APPLE__)
     #define LEAN_SUPPORTS_BACKTRACE 1
@@ -1978,15 +1979,16 @@ object * lean_mk_string_lossy_recover(char const * s, size_t sz, size_t pos, siz
 
 extern "C" LEAN_EXPORT object * lean_mk_string_from_bytes(char const * s, size_t sz) {
     size_t pos = 0, i = 0;
-    if (validate_utf8((const uint8_t *)s, sz, pos, i)) {
-        return lean_mk_string_unchecked(s, pos, i);
+    simdutf::result res = simdutf::validate_utf8_with_errors(s, sz);
+    if (res.error == simdutf::error_code::SUCCESS) {
+        return lean_mk_string_unchecked(s, sz, res.count);
     } else {
         return lean_mk_string_lossy_recover(s, sz, pos, i);
     }
 }
 
 extern "C" LEAN_EXPORT object * lean_mk_string_from_bytes_unchecked(char const * s, size_t sz) {
-    return lean_mk_string_unchecked(s, sz, utf8_strlen(s, sz));
+    return lean_mk_string_unchecked(s, sz, simdutf::count_utf8(s, sz));
 }
 
 extern "C" LEAN_EXPORT object * lean_mk_string(char const * s) {
@@ -2009,8 +2011,7 @@ extern "C" LEAN_EXPORT obj_res lean_string_from_utf8_unchecked(obj_arg a) {
 }
 
 extern "C" LEAN_EXPORT uint8 lean_string_validate_utf8(b_obj_arg a) {
-    size_t pos = 0, i = 0;
-    return validate_utf8(lean_sarray_cptr(a), lean_sarray_size(a), pos, i);
+    return simdutf::validate_utf8((const char*)lean_sarray_cptr(a), lean_sarray_size(a));
 }
 
 extern "C" LEAN_EXPORT obj_res lean_string_to_utf8(b_obj_arg s) {

src/runtime/utf8.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "runtime/debug.h"
 #include "runtime/optional.h"
+#include "runtime/simdutf.h"
 #include "runtime/utf8.h"
 
 namespace lean {

tests/compile/large_closure_bug.lean

@@ -68,10 +68,10 @@ def ExtractNonDet.bind :
     dsimp [Bind.bind, NonDetT.bind]; constructor
     intro y; apply ExtractNonDet.bind <;> solve_by_elim
 
-instance ExtractNonDet.pure' : ExtractNonDet (Pure.pure (f := NonDetT m) x) := by
+def ExtractNonDet.pure' : ExtractNonDet (Pure.pure (f := NonDetT m) x) := by
   dsimp [Pure.pure, NonDetT.pure]; constructor
 
-instance ExtractNonDet.liftM (x : m α) :
+def ExtractNonDet.liftM (x : m α) :
   ExtractNonDet (liftM (n := NonDetT m) x) := by
     dsimp [_root_.liftM, monadLift, MonadLift.monadLift]; constructor
     intro y; apply ExtractNonDet.pure'

tests/elab/13313.lean

@@ -0,0 +1,45 @@
+module
+
+-- Test that `deriving` inside a `public meta section` produces meta instances
+
+public meta section
+
+-- Delta deriving for definitions
+@[expose] def Foo := Nat
+deriving BEq
+
+-- Meta definitions should be able to use the derived instance
+def test (a b : Foo) : Bool := a == b
+
+-- Standalone deriving instance for definitions
+@[expose] def Bar := Nat
+deriving instance Hashable for Bar
+
+def testBar (a : Bar) : UInt64 := hash a
+
+-- Handler-based deriving for inductives
+inductive Baz where
+  | a | b
+deriving BEq, Repr, Hashable
+
+def testBaz (x y : Baz) : Bool := x == y
+
+-- DecidableEq for meta enums
+inductive Qux where
+  | x | y | z
+deriving DecidableEq
+
+def testDecEq (a b : Qux) : Bool := a == b
+
+end
+
+-- Outside any `meta section`: explicit `meta def` should also produce meta delta-derived instances.
+-- This exercises the `isMarkedMeta (← getEnv) declName` branch in `processDefDeriving`.
+public section
+
+@[expose] meta def Quux := Nat
+deriving BEq
+
+meta def testQuux (a b : Quux) : Bool := a == b
+
+end

tests/elab/13407.lean

@@ -0,0 +1,64 @@
+module
+
+/-! Regression test for issue 13407 -/
+
+inductive Result (α : Type) where | ok (x : α) | err
+instance : Monad Result where
+  pure x := .ok x
+  bind s f := match s with | .ok x => f x | .err => .err
+instance : Coe α (Result α) where coe x := .ok x
+
+structure Int' (bits : Nat) where val : Nat
+
+def Int'.wrap (n : Int) (bits : Nat) : Int' bits := ⟨(n % (2^bits : Int)).toNat⟩
+
+def Int'.toInt (x : Int' bits) : Int :=
+  if x.val < 2^(bits - 1) then ↑x.val else ↑x.val - ↑(2^bits)
+
+instance (n : Nat) : OfNat (Int' bits) n where ofNat := ⟨n % (2^bits)⟩
+instance : Neg (Int' bits) where neg x := Int'.wrap (-Int'.toInt x) bits
+instance : Repr (Int' bits) := ⟨fun x _ => repr (Int'.toInt x)⟩
+
+class BinOp1 (α β : Type) (γ : outParam Type) where binOp1 : α → β → γ
+class BinOp2 (α β : Type) (γ : outParam Type) where binOp2 : α → β → γ
+class UnaryOp (α : Type) (β : outParam Type) where unaryOp : α → β
+class Cast (α β : Type) where cast : α → Result β
+
+instance : BinOp1 (Int' b) (Int' b) (Result (Int' b)) where
+  binOp1 a c := .ok (Int'.wrap (a.toInt + c.toInt) b)
+
+instance : BinOp1 (Int' l) (Int' r) (Result (Int' l)) where
+  binOp1 a c := .ok (Int'.wrap (a.toInt + c.toInt) l)
+
+instance : BinOp2 (Int' b) (Int' b) (Result (Int' b)) where
+  binOp2 a c := .ok (Int'.wrap (a.toInt + c.toInt) b)
+
+instance : UnaryOp (Int' b) (Result (Int' b)) where
+  unaryOp a := .ok (Int'.wrap (-(a.toInt + 1)) b)
+
+instance : Cast (Int' n) (Int' m) where
+  cast x := .ok (Int'.wrap x.toInt m)
+
+set_option linter.unusedVariables false
+
+def helper (_ : Nat) : Result (Int' 64) := UnaryOp.unaryOp (1 : Int' 64)
+
+def test (a : Nat) : Result (Int' 16) := do
+  let x ← UnaryOp.unaryOp (1 : Int' 16)
+  let y ← BinOp2.binOp2
+        (← (Cast.cast (← helper a) : Result (Int' 128)))
+        (← BinOp1.binOp1
+              (← (Cast.cast (← helper a) : Result (Int' 128)))
+              (← BinOp2.binOp2
+                    (← BinOp1.binOp1 (10 : Int' 128) (1 : Int' 128))
+                    (← BinOp2.binOp2 (7 : Int' 128) (3 : Int' 128))))
+  BinOp1.binOp1
+    (← (Cast.cast (← (Cast.cast y : Result (Int' 128))) : Result (Int' 16)))
+    (← BinOp2.binOp2 x (← BinOp2.binOp2 x x))
+
+/-- info: 11 -/
+#guard_msgs in
+#eval do
+  match test 0 with
+  | .ok v => IO.println (repr v)
+  | .err => IO.println "ERR"

tests/elab/13415.lean

@@ -0,0 +1,13 @@
+macro "co " x:ident : command => do
+  `(coinductive $x : Prop where | ok)
+
+/-- error: Coinductive predicates are not allowed inside of macro scopes -/
+#guard_msgs in
+co f
+
+macro "co2" : command => do
+  `(coinductive test : Prop where | ctor)
+
+/-- error: Coinductive predicates are not allowed inside of macro scopes -/
+#guard_msgs in
+co2

tests/elab/5672.lean

@@ -20,7 +20,8 @@ Uses `def` variable inclusion rules
 -/
 section
 variable (x : Nat)
-instance b : A := by
+@[reducible]
+def b : A := by
   cases x <;> exact {}
 /-- info: b (x : Nat) : A -/
 #guard_msgs in #check b

tests/elab/impossibleInstance.lean

@@ -0,0 +1,22 @@
+class MyClass (α : Type u) where
+  point : α
+
+/--
+error: Instance @bad1 has arguments n : Nat that are impossible to infer. Those arguments are not instance-implicit and do not appear in another instance-implicit argument or the return type.
+---
+warning: declaration uses `sorry`
+-/
+#guard_msgs in
+instance bad1 {α : Type} [Inhabited α] (n : Nat) : MyClass α := sorry
+
+/--
+error: Instance @bad2 has arguments n : Nat, m : Nat that are impossible to infer. Those arguments are not instance-implicit and do not appear in another instance-implicit argument or the return type.
+---
+warning: declaration uses `sorry`
+-/
+#guard_msgs in
+instance bad2 {α : Type} [Inhabited α] (n m : Nat) : MyClass α := sorry
+
+/-- warning: declaration uses `sorry` -/
+#guard_msgs in
+instance good {α : Type} [Inhabited α] : MyClass α := sorry

tests/elab/isDefEqProjIssue.lean

@@ -77,10 +77,12 @@ class Foo where
   x : Nat
   y : Nat
 
-instance f (x : Nat) : Foo :=
+@[reducible]
+def f (x : Nat) : Foo :=
   { x, y := ack 10 10 }
 
-instance g (x : Nat) : Foo :=
+@[reducible]
+def g (x : Nat) : Foo :=
   { x, y := ack 10 11 }
 
 open Lean Meta

tests/elab/issue12846.lean

@@ -0,0 +1,108 @@
+module
+
+set_option backward.do.legacy false
+
+-- Original issue: `let x ← value` as last element in non-Unit do block
+/--
+error: Type mismatch. The `do` element has monadic result type
+  Unit
+but the rest of the `do` block has monadic result type
+  Bool
+-/
+#guard_msgs in
+def test_letArrow : IO Bool := do
+  let a ← pure 25
+
+/--
+error: Type mismatch. The `do` element has monadic result type
+  Unit
+but the rest of the `do` block has monadic result type
+  Bool
+-/
+#guard_msgs in
+def test_let : IO Bool := do
+  let a := 25
+
+-- `have` as last element
+/--
+error: Type mismatch. The `do` element has monadic result type
+  Unit
+but the rest of the `do` block has monadic result type
+  Bool
+-/
+#guard_msgs in
+def test_have : IO Bool := do
+  have a := 25
+
+-- `let rec` as last element
+/--
+error: Type mismatch. The `do` element has monadic result type
+  Unit
+but the rest of the `do` block has monadic result type
+  Bool
+-/
+#guard_msgs in
+def test_letRec : IO Bool := do
+  let rec f : Nat → Nat
+    | 0 => 0
+    | n + 1 => f n
+
+-- `for` as last element
+/--
+error: Type mismatch. The `do` element has monadic result type
+  Unit
+but the rest of the `do` block has monadic result type
+  Bool
+-/
+#guard_msgs in
+def test_for : IO Bool := do
+  for _ in [1, 2, 3] do
+    pure ()
+
+-- `dbg_trace` as last element
+/--
+error: Type mismatch. The `do` element has monadic result type
+  Unit
+but the rest of the `do` block has monadic result type
+  Bool
+-/
+#guard_msgs in
+def test_dbgTrace : IO Bool := do
+  dbg_trace "hello"
+
+-- `assert!` as last element
+/--
+error: Type mismatch. The `do` element has monadic result type
+  Unit
+but the rest of the `do` block has monadic result type
+  Bool
+-/
+#guard_msgs in
+def test_assert : IO Bool := do
+  assert! true
+
+-- `if` without else as last element
+/--
+error: Application type mismatch: The argument
+  ()
+has type
+  Unit
+but is expected to have type
+  Bool
+in the application
+  pure ()
+---
+error: Type mismatch. The `do` element has monadic result type
+  Unit
+but the rest of the `do` block has monadic result type
+  Bool
+-/
+#guard_msgs in
+def test_if_no_else : IO Bool := do
+  if true then
+    pure ()
+
+-- `if` with else works fine when branches match the result type
+#guard_msgs in
+def test_if_else_ok : IO Bool := do
+  if true then pure true else pure false

tests/elab/newdo.lean

@@ -26,11 +26,7 @@ Many of these are extracted from our code base.
     x := x + 1
   return ⟨3, by decide⟩
 
--- Regression test cases of what's broken in the legacy do elaborator:
-example : Unit := (Id.run do  let n ← if true then pure 3 else pure 42)
 example : Unit := (Id.run do let n ← if true then pure 3 else pure 42)
-example := (Id.run do  let mut x := 0; x ← return 10)
-example := (Id.run do let mut x := 0; x ← return 10)
 
 -- Another complicated `match` that would need to generalize the join point type if it was dependent
 example (x : Nat) : Id (Fin (x + 2)) := do
@@ -211,8 +207,8 @@ trace: [Elab.do] let x := 42;
               else
                 let x := x + i;
                 pure (ForInStep.yield (none, x))
-    let __r : Option ?m.185 := __s.fst
-    let x : ?m.185 := __s.snd
+    let __r : Option ?m.170 := __s.fst
+    let x : ?m.170 := __s.snd
     match __r with
       | some r => pure r
       | none =>

tests/elab/nonClassInstance.lean

@@ -0,0 +1,37 @@
+/-! Registering an instance whose target type is not a class should warn. -/
+
+structure Foo where
+  x : Nat
+
+class Bar where
+  x : Nat
+
+/-- error: instance `instFoo` target `Foo` is not a type class. -/
+#guard_msgs in
+instance instFoo : Foo := ⟨0⟩
+
+-- Applying @[instance] to a non-class def should also warn
+def instFoo2 : Foo := ⟨1⟩
+
+/-- error: instance `instFoo2` target `Foo` is not a type class. -/
+#guard_msgs in
+attribute [instance] instFoo2
+
+-- No warning for a proper class instance
+#guard_msgs in
+instance : Bar := ⟨0⟩
+
+-- No warning for a class instance with parameters
+class Baz (α : Type) where
+  x : α
+
+#guard_msgs in
+instance : Baz Nat := ⟨0⟩
+
+-- Warning for non-class with parameters
+structure Qux (α : Type) where
+  x : α
+
+/-- error: instance `instQux` target `Qux Nat` is not a type class. -/
+#guard_msgs in
+instance instQux : Qux Nat := ⟨0⟩

tests/elab/simpVarHead.lean

@@ -1,5 +1,3 @@
-set_option warning.simp.varHead true
-
 section
 theorem broken1 (x : Nat) : x = x + 0 := by simp
 

tests/elab/simp_proj_transparency_issue.lean

@@ -2,11 +2,11 @@ structure Foo where
   x : Nat
   y : Nat := 10
 
-@[instance]
+@[implicit_reducible]
 def f (x : Nat) : Foo :=
   { x := x + x }
 
-@[instance]
+@[implicit_reducible]
 def g (x : Nat) : Foo :=
   { x := x + x }
 

tests/elab/simp_proj_transparency_issue.lean.out.expected

@@ -1,2 +0,0 @@
-simp_proj_transparency_issue.lean:5:2-5:10: warning: instance `f` must be marked with `@[reducible]` or `@[implicit_reducible]`
-simp_proj_transparency_issue.lean:9:2-9:10: warning: instance `g` must be marked with `@[reducible]` or `@[implicit_reducible]`

tests/elab/test_simp_reducible_class.lean

@@ -17,7 +17,8 @@ namespace SimpReducibleClassField
 class X where
   x : Nat
 
-instance instX (n : Nat) : X where
+@[implicit_reducible]
+def instX (n : Nat) : X where
   x := n
 
 -- Test 1: plain simp, semireducible X.x (works on master)

tests/elab_fail/doNotation1.lean.out.expected

@@ -49,18 +49,7 @@ doNotation1.lean:78:21-78:31: error: typeclass instance problem is stuck
 Note: Lean will not try to resolve this typeclass instance problem because the type argument to `ToString` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.
 
 Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-doNotation1.lean:82:0-83:9: error: Type mismatch. `for` loops have result type Unit, but the rest of the `do` sequence expected List (Nat × Nat).
-doNotation1.lean:83:7-83:9: error: Application type mismatch: The argument
-  ()
-has type
+doNotation1.lean:82:0-82:3: error: Type mismatch. The `do` element has monadic result type
   Unit
-but is expected to have type
-  List (Nat × Nat)
-in the application
-  pure ()
-doNotation1.lean:82:0-83:9: error: Type mismatch
-  ()
-has type
-  Unit
-but is expected to have type
+but the rest of the `do` block has monadic result type
   List (Nat × Nat)

tests/elab_fail/linterUnusedVariables.lean

@@ -154,7 +154,7 @@ class Baz (α : Type) where
     let y := 5
     3
 
-instance instBaz (α β : Type) : Baz α where
+@[reducible] def instBaz (α β : Type) : Baz α where
   baz (x : Nat) := 5
 
 

tests/elab_fail/linterUnusedVariables.lean.out.expected

@@ -52,7 +52,7 @@ Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:154:8-154:9: warning: unused variable `y`
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:157:20-157:21: warning: unused variable `β`
+linterUnusedVariables.lean:157:28-157:29: warning: unused variable `β`
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:158:7-158:8: warning: unused variable `x`