diff --git a/src/Init/Data.lean b/src/Init/Data.lean
index 9f9f8037a7fb..ac4b205d730a 100644
--- a/src/Init/Data.lean
+++ b/src/Init/Data.lean
@@ -38,6 +38,7 @@ public import Init.Data.Queue
 public import Init.Data.Sum
 public import Init.Data.BEq
 public import Init.Data.Subtype
+public import Init.Data.Erased
 public import Init.Data.ULift
 public import Init.Data.PLift
 public import Init.Data.Zero
diff --git a/src/Init/Data/Erased.lean b/src/Init/Data/Erased.lean
new file mode 100644
index 000000000000..8c7d3ddf7f68
--- /dev/null
+++ b/src/Init/Data/Erased.lean
@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Sebastian Graf
+-/
+module
+
+prelude
+public import Init.Classical
+public import Init.Ext
+import Init.Grind.Attr
+
+public section
+
+/-- A value hidden from compiled code. `Erased.mk 42` erases to a dummy at runtime, and
+proofs recover the `42` as `(Erased.mk 42).out`. -/
+@[expose] def Erased (α : Sort u) : Sort (max 1 u) :=
+  { s : α → Prop // ∃ a, (a = ·) = s }
+
+namespace Erased
+
+/-- Hides `a` in an `Erased α`. Compiled code drops the argument. -/
+@[expose, macro_inline] def mk {α : Sort u} (a : α) : Erased α :=
+  ⟨fun b => a = b, a, rfl⟩
+
+/-- The value hidden in `e`, available to proofs only. -/
+noncomputable def out {α : Sort u} (e : Erased α) : α :=
+  Classical.choose e.property
+
+@[simp, grind =] theorem out_mk {α : Sort u} (a : α) : (mk a).out = a :=
+  cast (congrFun (Classical.choose_spec (mk a).property) a).symm rfl
+
+@[simp, grind =] theorem mk_out {α : Sort u} (e : Erased α) : mk e.out = e := by
+  cases e with
+  | mk s h => exact Subtype.ext (Classical.choose_spec h)
+
+@[ext] theorem out_inj {α : Sort u} {a b : Erased α} (h : a.out = b.out) : a = b := by
+  rw [← mk_out a, ← mk_out b, h]
+
+@[simp, grind =] theorem mk_inj {α : Sort u} {a b : α} : mk a = mk b ↔ a = b :=
+  ⟨fun h => by have := congrArg out h; rwa [out_mk, out_mk] at this, fun h => h ▸ rfl⟩
+
+end Erased
diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index 3e905cc1a9f2..1b8ba44b17a2 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -447,6 +447,8 @@ private def checkComputable (ref : Name) : M Unit := do
   -- `noncomputable section`, where the failure to compile the `_unsafe_rec` version is tolerated and
   -- only that auxiliary is marked `noncomputable`, leaving `ref` itself unmarked.
   if isNoncomputable (← getEnv) ref || isNoncomputable (← getEnv) (mkUnsafeRecName ref) then
+    if ref == `Erased.out then
+      throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition: it depends on 'Erased.out', which recovers the value of an erased variable. An erased variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'."
     throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName ref}', which is 'noncomputable'"
   else if getOriginalConstKind? (← getEnv) ref matches some .axiom | some .quot | some .induct | some .thm then
     throwNamedError lean.dependsOnNoncomputable f!"`{ref}` not supported by code generator; consider marking definition as `noncomputable`"
diff --git a/src/Lean/Elab/BuiltinDo/For.lean b/src/Lean/Elab/BuiltinDo/For.lean
index 7c628bdad90e..27d6c4e9a678 100644
--- a/src/Lean/Elab/BuiltinDo/For.lean
+++ b/src/Lean/Elab/BuiltinDo/For.lean
@@ -6,6 +6,7 @@ Authors: Sebastian Graf
 module
 
 prelude
+meta import Init.Data.Erased
 public import Lean.Elab.BuiltinDo.Basic
 meta import Lean.Parser.Do
 meta import Std.WP.Gadget.ForIn
@@ -169,10 +170,22 @@ structure ForInApp where
   σ : Expr
   /-- The pattern naming the loop's mutable variables in the state tuple. -/
   statePat : Term
+  /-- The erased variables among the loop's mutable variables; annotations bind their `.out`
+  projections over the state tuple. -/
+  erasedMutVars : Array MutVar := #[]
+
+/-- Bind the `.out` projection of each erased variable over `e`, so that an annotation names erased
+variables at their underlying type. The `+zeta` substitutes the binding away at elaboration, so
+annotation goals carry the projection inline like the compiled body does. -/
+private def ForInApp.wrapErasedProjs (g : ForInApp) (e : Term) : DoElabM Term := do
+  let mut e := e
+  for mv in g.erasedMutVars do
+    e ← `(let +zeta $(mv.ident):ident := Erased.out $(⟨mv.ident.raw⟩); $e)
+  return e
 
 /-- Abstract `e` over the loop's state tuple, so that `e` may name the loop's mutable variables. -/
-private def ForInApp.mkStateFun (g : ForInApp) (e : Term) : DoElabM Term :=
-  `(fun $(g.statePat) => $e)
+private def ForInApp.mkStateFun (g : ForInApp) (e : Term) : DoElabM Term := do
+  `(fun $(g.statePat) => $(← g.wrapErasedProjs e))
 
 /-- Elaborate the gadget application that replaces the loop. The gadgets live downstream of this
 module, so `gadget` is an unresolved name that resolves in the user's context. -/
@@ -242,7 +255,7 @@ private def mkForInLoopGadget (g : ForInApp)
     -- unfolded type, and a specification's instance arguments are synthesized before the check that
     -- would unfold it.
     return ((invClause : Syntax), ← `($(mkIdent ``Std.WP.WhileInvariant.mk)
-      fun $exitVar:ident $(g.statePat) => $invBody))
+      fun $exitVar:ident $(g.statePat) => $(← g.wrapErasedProjs invBody)))
   let varArg? ← dec?.mapM fun decClause => do
     let (binders, body) ← match decClause with
       | `(doLoopDecreasing| decreasing $binders* => $body) => pure (binders, body)
@@ -296,17 +309,17 @@ private def mkForInLoopGadget (g : ForInApp)
         | some e => mkSome oldReturnCont.resultType e
       defs := defs.push returnVar
     for x in loopMutVars do
-      let defn ← getLocalDeclFromUserName x.getId
-      Term.addTermInfo' x.ident defn.toExpr
+      Term.addTermInfo' x.ident (← getFVarFromUserName x.getId)
+      let v ← x.stateValue
       -- ForIn forces the mut tuple into the universe mi.u: that of the do block result type.
       -- If we don't do this, then we are stuck on solving constraints such as
       --   `max ?u.46 ?u.47 =?= max (max ?u.22 ?u.46) ?u.47`
       -- It's important we do this as a separate isLevelDefEq check on the decremented level because
       -- otherwise (`ensureHasType (mkSort mi.u.succ)`) we are stuck on constraints like
       --   `max (?u+1) (?v+1) =?= ?u+1`
-      let u ← getDecLevel defn.type
+      let u ← getDecLevel (← inferType v)
       discard <| isLevelDefEq u mi.u
-      defs := defs.push defn.toExpr
+      defs := defs.push v
     if info.returnsEarly && loopMutVars.isEmpty then
       defs := defs.push (mkConst ``Unit.unit)
     return defs
@@ -367,7 +380,8 @@ private def mkForInLoopGadget (g : ForInApp)
   let mut forIn := mkApp app body
   unless inv?.isNone && dec?.isNone do
     let g : ForInApp :=
-      { xs, init := preS, body, σ, statePat := ← mkStatePat loopMutVars info.returnsEarly }
+      { xs, init := preS, body, σ, statePat := ← mkStatePat loopMutVars info.returnsEarly,
+        erasedMutVars := loopMutVars.filter (·.erased) }
     if (← instantiateMVars ρ).isConstOf ``Lean.Loop then
       if let some e ← mkForInLoopGadget g inv? dec? then forIn := e
     else if let some decClause := dec? then
diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index 25c53116c1ba..6d04a6c55d13 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -6,6 +6,7 @@ Authors: Sebastian Graf
 module
 
 prelude
+meta import Init.Data.Erased
 public import Lean.Elab.Do.Basic
 meta import Lean.Parser.Do
 import Lean.Elab.BuiltinDo.Basic
@@ -13,25 +14,47 @@ import Lean.Elab.Do.PatternVar
 
 public section
 
+-- The `erased` doElem quotations below need the current stage's parser until stage0 catches up.
+set_option internal.parseQuotWithCurrentStage true
+
 namespace Lean.Elab.Do
 
 open Lean.Parser.Term
 open Lean.Meta
 
 inductive LetOrReassign
-  | let (mutTk? : Option Syntax)
+  | let (mutTk? : Option Syntax) (erased : Bool)
   | have
   | reassign
 
 def LetOrReassign.getLetMutTk? (letOrReassign : LetOrReassign) : Option Syntax :=
   match letOrReassign with
-  | .let mutTk? => mutTk?
-  | _           => none
+  | .let mutTk? _ => mutTk?
+  | _             => none
+
+def LetOrReassign.isErasedDecl (letOrReassign : LetOrReassign) : Bool :=
+  match letOrReassign with
+  | .let _ erased => erased
+  | _            => false
+
+def isErased (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Bool := do
+  match letOrReassign with
+  | .let _ erased => return erased
+  | .reassign    =>
+    let some v := vars[0]? | return false
+    let some mv ← findMutVar? v.getId | return false
+    return mv.erased
+  | _            => return false
 
 def LetOrReassign.checkMutVars (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit :=
   match letOrReassign with
   | .reassign => do
     throwUnlessMutVarsDeclared vars
+    -- Reassigning an erased variable wraps its value, which only the single-variable form can do.
+    unless vars.size == 1 do
+      for v in vars do
+        if ((← findMutVar? v.getId).map (·.erased)).getD false then
+          throwErrorAt v "an erased variable takes a plain reassignment, as in `{v.getId} := e`"
   | _         => checkMutVarsForShadowing vars
 
 def LetOrReassign.registerReassignAliasInfo (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit := do
@@ -39,19 +62,13 @@ def LetOrReassign.registerReassignAliasInfo (letOrReassign : LetOrReassign) (var
     for var in vars do
       registerMutVarAlias var.getId
 
-def elabDoLetOrReassignWith (hint : MessageData) (letOrReassign : LetOrReassign) (vars : Array Ident)
-    (k : DoElabM Expr) (elabBody : (body : Term) → TermElabM Expr) : DoElabM Expr := do
-  -- letOrReassign.checkMutVars vars -- Should be done by the caller!
-  let elabCont : DoElabM Expr := do
-    declareMutVars? letOrReassign.getLetMutTk? vars do
-      letOrReassign.registerReassignAliasInfo vars
-      k
-  doElabToSyntax hint elabCont fun body => elabBody body
-
 def elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) : DoElabM Expr := do
-  declareMutVars? letOrReassign.getLetMutTk? vars do
+  declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isErasedDecl do
     letOrReassign.registerReassignAliasInfo vars
-    k
+    if ← isErased letOrReassign vars then
+      vars.foldr (init := k) withErasedProj
+    else
+      k
 
 private def pushTypeIntoReassignment (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl) : TermElabM (TSyntax ``letDecl) := do
   if letOrReassign matches .reassign then
@@ -83,14 +100,25 @@ private def checkLetConfigInDo (config : Term.LetConfig) : DoElabM Unit := do
   if config.generalize then
     throwError "`+generalize` is not supported in `do` blocks"
 
+/-- Wrap an erased binding `x : t := e` as `x : Erased t := Erased.mk e`. For a reassignment,
+`pushTypeIntoReassignment` has already checked the ascription and pinned `t`. -/
+private def wrapErasedDecl (decl : TSyntax ``letDecl) : DoElabM (TSyntax ``letDecl) := do
+  let `(letDecl| $x:ident $[: $t?]? := $e) := decl
+    | throwUnsupportedSyntax
+  match t? with
+  | some t => `(letDecl| $x:ident : Erased $t := Erased.mk ($e : $t))
+  | none   => `(letDecl| $x:ident := Erased.mk $e)
+
 partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl)
     (tk : Syntax) (dec : DoElemCont) : DoElabM Expr := do
   checkLetConfigInDo config
   let vars ← getLetDeclVars decl
   letOrReassign.checkMutVars vars
   let dec ← dec.ensureUnitAt tk
+  let isErased ← isErased letOrReassign vars
   -- Some decl preprocessing on the patterns and expected types:
   let decl ← pushTypeIntoReassignment letOrReassign decl
+  let decl ← if isErased then wrapErasedDecl decl else pure decl
   let mγ ← mkMonadApp (← read).doBlockResultType
   match decl with
   | `(letDecl| $decl:letEqnsDecl) =>
@@ -137,10 +165,9 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
     trace[Elab.let.decl] "{id.getId} : {type} := {val}"
     withLetDecl id.getId (kind := kind) type val (nondep := nondep) fun x => do
       Term.addLocalVarInfo id x
-      elabWithReassignments letOrReassign vars do
       match config.eq? with
       | none =>
-        let body ← dec.continueWithUnit
+        let body ← elabWithReassignments letOrReassign vars dec.continueWithUnit
         if config.zeta then
           pure <| (← body.abstractM #[x]).instantiate1 val
         else
@@ -149,7 +176,7 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
         let hTy ← mkEq x val
         withLetDecl h.getId hTy (← mkEqRefl x) (nondep := true) fun h' => do
           Term.addLocalVarInfo h h'
-          let body ← dec.continueWithUnit
+          let body ← elabWithReassignments letOrReassign vars dec.continueWithUnit
           if config.zeta then
             pure <| (← body.abstractM #[x, h']).instantiateRev #[val, ← mkEqRefl val]
           else if nondep then
@@ -159,44 +186,6 @@ 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]) (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
-      | .reassign, none =>
-        let decl ← getLocalDeclFromUserName x.getId
-        some <$> Term.exprToSyntax decl.type
-      | _, _ => pure xType?
-    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x <| dec.continueWithUnit)
-      (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
-    let x := mkIdentFrom pattern (← mkFreshUserName `__x)
-    elabDoIdDecl x patType? rhs do
-      match letOrReassign, otherwise? with
-      | .let mutTk?, some otherwise =>
-        elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x | $otherwise $(rest?)?)) dec
-      | .let mutTk?, _ =>
-        elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x)) dec
-      | .have, some _otherwise =>
-        throwUnsupportedSyntax
-      | .have, _ =>
-        elabDoElem (← `(doElem| have $pattern:term := $x)) dec
-      | .reassign, _ =>
-        -- otherwise? is always `none`, because there is no `doReassignElse`
-        unless rest?.isNone do
-          throwError "reassignment with `|` (i.e., \"else clause\") is not supported"
-        elabDoElem (← `(doElem| $pattern:term := $x)) dec
-  | _ => throwUnsupportedSyntax
-
 private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letConfig)
     (mutTk? : Option Syntax) (initConfig : Term.LetConfig := {}) : DoElabM Term.LetConfig := do
   if mutTk?.isSome && !letConfigStx.raw[0].getArgs.isEmpty then
@@ -206,7 +195,20 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
 @[builtin_doElem_elab Lean.Parser.Term.doLet] def elabDoLet : DoElab := fun stx dec => do
   let `(doLet| let%$tk $[mut%$mutTk?]? $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
   let config ← getLetConfigAndCheckMut config mutTk?
-  elabDoLetOrReassign config (.let mutTk?) decl tk dec
+  elabDoLetOrReassign config (.let mutTk? false) decl tk dec
+
+@[builtin_doElem_elab Lean.Parser.Term.doErased] def elabDoErased : DoElab := fun stx dec => do
+  let `(doErased| erased%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? := $e) := stx | throwUnsupportedSyntax
+  elabDoLetOrReassign {} (.let mutTk? true) (← `(letDecl| $x:ident $[: $t?]? := $e)) tk dec
+
+@[builtin_macro Lean.Parser.Term.doErasedArrow] def expandDoErasedArrow : Macro := fun stx => do
+  match stx with
+  | `(doErasedArrow| erased%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? ← $rhs) =>
+    let y := mkIdentFrom x (← MonadQuotation.addMacroScope `__x)
+    let letElem ← `(doElem| let $y:ident $[: $t?]? ← $rhs)
+    let erasedElem : TSyntax `doElem := ⟨(← `(doErased| erased%$tk $[mut%$mutTk?]? $x:ident := $y)).raw⟩
+    `(doElem| do $letElem:doElem; $erasedElem:doElem)
+  | _ => Macro.throwUnsupported
 
 @[builtin_doElem_elab Lean.Parser.Term.doHave] def elabDoHave : DoElab := fun stx dec => do
   let `(doHave| have%$tk $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
@@ -241,7 +243,7 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
     | throwUnsupportedSyntax
   let config ← getLetConfigAndCheckMut cfg mutTk?
   checkLetConfigInDo config
-  let letOrReassign := LetOrReassign.let mutTk?
+  let letOrReassign := LetOrReassign.let mutTk? false
   let vars ← getPatternVarsEx pattern
   letOrReassign.checkMutVars vars
   let mut body ← body?.getDM `(doSeqIndent|pure PUnit.unit)
@@ -260,12 +262,42 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   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 tk dec
+  match decl with
+  | `(doIdDecl| $x:ident $[: $xType?]? ← $rhs) =>
+    checkMutVarsForShadowing #[x]
+    let dec ← dec.ensureUnitAt tk
+    elabDoIdDecl x xType? rhs (declareMutVar? mutTk? x false <| dec.continueWithUnit)
+      (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)
+  -- No `ensureUnitAt` here: the else form swallows the rest of the block into `rest?`, so the
+  -- element keeps `dec`'s result type.
+  | `(doPatDecl| $pattern:term $[: $patType?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
+    let rest? := rest?.join
+    let x := mkIdentFrom pattern (← mkFreshUserName `__x)
+    elabDoIdDecl x patType? rhs do
+      match otherwise? with
+      | some otherwise =>
+        elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x | $otherwise $(rest?)?)) dec
+      | none =>
+        elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x)) dec
+  | _ => throwUnsupportedSyntax
 
 @[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do
   match stx with
-  | `(doReassignArrow| $decl:doIdDecl) =>
-    elabDoArrow .reassign decl decl dec
-  | `(doReassignArrow| $decl:doPatDecl) =>
-    elabDoArrow .reassign decl decl dec
+  | `(doReassignArrow| $x:ident $[: $t?]? ← $rhs) =>
+    throwUnlessMutVarDeclared x
+    -- Pin the variable's declared type on the bind, so a type error blames the action.
+    let t ← match t? with
+      | some t => pure t
+      | none   => Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
+    let y := mkIdentFrom x (← mkFreshUserName `__x)
+    elabDoIdDecl y (some t) rhs (elabDoElem (← `(doElem| $x:ident := $y)) dec) (kind := dec.kind)
+  | `(doReassignArrow| $pat:term $[: $t?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
+    unless otherwise?.isNone && rest?.join.isNone do
+      throwError "reassignment with `|` (i.e., \"else clause\") is not supported"
+    let y := mkIdentFrom pat (← mkFreshUserName `__x)
+    elabDoIdDecl y t? rhs (elabDoElem (← `(doElem| $pat:term := $y)) dec) (kind := dec.kind)
   | _ => throwUnsupportedSyntax
diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index c09624fdcb4d..29330123cc41 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -6,6 +6,7 @@ Authors: Sebastian Graf
 module
 
 prelude
+meta import Init.Data.Erased
 public import Lean.Elab.Do.InferControlInfo
 public import Lean.Elab.Binders
 import Lean.Meta.ProdN
@@ -99,10 +100,12 @@ def CodeLiveness.lub (a b : CodeLiveness) : CodeLiveness :=
 
 /-- A mutable variable declared by `let mut` in a `do` block. -/
 structure MutVar where
-  /-- The identifier of the `let mut` declaration. -/
+  /-- The identifier of the `let mut` or `erased mut` declaration. -/
   ident : Ident
-  /-- The `FVarId` of the initial binding produced by `let mut`. -/
+  /-- The `FVarId` of the initial binding produced by the declaration. -/
   baseId : FVarId
+  /-- Whether the variable comes from `erased mut`. -/
+  erased : Bool
   deriving Inhabited
 
 /-- The raw `Name` of a `mut` variable, as found in the local context. -/
@@ -336,30 +339,30 @@ def DoOps.default : DoOps where
     return mkApp (← read).monadInfo.m α
 
 /-- Register the given name as that of a `mut` variable. -/
-def declareMutVar (x : Ident) (k : DoElabM α) : DoElabM α := do
+def declareMutVar (x : Ident) (erased : Bool) (k : DoElabM α) : DoElabM α := do
   let fvar ← getFVarFromUserName x.getId
-  let mutVar : MutVar := { ident := x, baseId := fvar.fvarId! }
+  let mutVar : MutVar := { ident := x, baseId := fvar.fvarId!, erased }
   withReader (fun ctx => { ctx with
     mutVars := ctx.mutVars.push mutVar,
     mutVarDefs := ctx.mutVarDefs.insert x.getId mutVar,
   }) k
 
 /-- Register the given names as that of `mut` variables. -/
-def declareMutVars (xs : Array Ident) (k : DoElabM α) : DoElabM α := do
+def declareMutVars (xs : Array Ident) (erased : Bool) (k : DoElabM α) : DoElabM α := do
   let fvars ← xs.mapM (getFVarFromUserName ·.getId)
-  let newMutVars : Array MutVar := xs.zipWith (fun x fvar => { ident := x, baseId := fvar.fvarId! }) fvars
+  let newMutVars : Array MutVar := xs.zipWith (fun x fvar => { ident := x, baseId := fvar.fvarId!, erased }) fvars
   withReader (fun ctx => { ctx with
     mutVars := ctx.mutVars ++ newMutVars,
     mutVarDefs := ctx.mutVarDefs.insertMany (newMutVars.map fun mutVar => (mutVar.getId, mutVar)),
   }) k
 
 /-- Register the given name as that of a `mut` variable if the syntax token `mut` is present. -/
-def declareMutVar? (mutTk? : Option Syntax) (x : Ident) (k : DoElabM α) : DoElabM α :=
-  if mutTk?.isSome then declareMutVar x k else k
+def declareMutVar? (mutTk? : Option Syntax) (x : Ident) (erased : Bool) (k : DoElabM α) : DoElabM α :=
+  if mutTk?.isSome then declareMutVar x erased k else k
 
 /-- Register the given names as that of `mut` variables if the syntax token `mut` is present. -/
-def declareMutVars? (mutTk? : Option Syntax) (xs : Array Ident) (k : DoElabM α) : DoElabM α :=
-  if mutTk?.isSome then declareMutVars xs k else k
+def declareMutVars? (mutTk? : Option Syntax) (xs : Array Ident) (erased : Bool) (k : DoElabM α) : DoElabM α :=
+  if mutTk?.isSome then declareMutVars xs erased k else k
 
 /-- Look up a declared `mut` variable by its raw `Name`. -/
 def findMutVar? (n : Name) : DoElabM (Option MutVar) := do
@@ -602,14 +605,55 @@ def registerMutVarAlias (x : Name) : DoElabM Unit := do
     if id != baseMutVar.baseId then
       pushInfoLeaf <| .ofFVarAliasInfo (baseMutVar.mkAliasInfo id)
 
+/-- Bind `x` to `carried.out` at the underlying type while `k` runs, and zeta-substitute the
+binding away, so the source name reaches proofs and never compiled code. The newest binding of
+`x` must be the carried `Erased` binding. -/
+def withErasedProj (x : Ident) (k : DoElabM Expr) (info : Bool := true) : DoElabM Expr := do
+  let carried ← getLocalDeclFromUserName x.getId
+  let_expr c@Erased t ← carried.type
+    | throwError "the carried binding of erased variable `{x.getId}` has type{indentExpr carried.type}\ninstead of an `Erased` type"
+  let outVal := mkApp2 (mkConst ``Erased.out c.constLevels!) t carried.toExpr
+  withLetDecl x.getId t outVal (nondep := true) fun xv => do
+    if info then
+      Term.addLocalVarInfo x xv
+    -- Uses of `x` resolve to the projection, so alias it to the variable's base binding for
+    -- find-references and rename.
+    let baseId := ((← findMutVar? x.getId).map (·.baseId)).getD carried.fvarId
+    pushInfoLeaf <| .ofFVarAliasInfo { userName := x.getId, id := xv.fvarId!, baseId }
+    let body ← k
+    return (← body.abstractM #[xv]).instantiate1 outVal
+
+/-- Bind the `.out` projection of each erased variable among `mutVars` around `k`. -/
+def withErasedProjs (mutVars : Array MutVar) (k : DoElabM Expr) (info : Bool := true) : DoElabM Expr :=
+  (mutVars.filter (·.erased)).foldr (init := k) fun mv k => withErasedProj mv.ident k info
+
+/-- `Erased.mk e`, which erases `e` in compiled code. -/
+def mkErasedMkApp (e : Expr) : MetaM Expr := do
+  let t ← inferType e
+  return mkApp2 (mkConst ``Erased.mk [← getLevel t]) t e
+
+/-- The type of `mv`'s slot in runtime state (tuples, join parameters): an erased variable's slot
+carries the `Erased` value. -/
+def MutVar.stateType (mv : MutVar) : MetaM Expr := do
+  let t := (← getLocalDeclFromUserName mv.getId).type
+  if mv.erased then return mkApp (mkConst ``Erased [← getLevel t]) t else return t
+
+/-- The current value of `mv` as packed into runtime state. -/
+def MutVar.stateValue (mv : MutVar) : MetaM Expr := do
+  let v := (← getLocalDeclFromUserName mv.getId).toExpr
+  if mv.erased then mkErasedMkApp v else return v
+
 /--
 Given a list of mut vars `vars` and an FVar `tupleVar` binding a tuple, bind the mut vars to the
 fields of the tuple and call `k` in the resulting local context.
 -/
-def bindMutVarsFromTuple (vars : List Name) (tupleVar : FVarId) (k : DoElabM Expr) : DoElabM Expr :=
-  do go vars tupleVar (← tupleVar.getType) #[]
+def bindMutVarsFromTuple (vars : List Name) (tupleVar : FVarId) (k : DoElabM Expr) : DoElabM Expr := do
+  let erasedVars := (← read).mutVars.filter fun mv => mv.erased && vars.contains mv.getId
+  -- Like the erased rebindings themselves, the projections contribute only aliases here.
+  let k := withErasedProjs erasedVars k (info := false)
+  go vars tupleVar (← tupleVar.getType) #[] k
 where
-  go vars tupleVar tupleTy letFVars := do
+  go vars tupleVar tupleTy letFVars k := do
     let tuple := mkFVar tupleVar
     match vars with
     | []  => mkLetFVars letFVars (← k)
@@ -629,7 +673,7 @@ where
       withLetDecl x fstTy fst fun xf => do
         registerMutVarAlias x
         withLetDecl (← tupleVar.getUserName) sndTy snd fun r => do
-          go xs r.fvarId! sndTy (letFVars |>.push xf |>.push r)
+          go xs r.fvarId! sndTy (letFVars |>.push xf |>.push r) k
 
 /--
   Backtrackable state for the `TermElabM` monad.
@@ -683,12 +727,11 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
   let γ := (← read).doBlockResultType
   let mγ ← mkMonadApp γ
   let mutVars := (← read).mutVars |>.filter (callerInfo.reassigns.contains ·.getId)
-  let mutVarNames := mutVars.map (·.getId)
   let joinName ← mkFreshUserName `__do_jp
   -- σ is the tuple type of the mut vars, or mγ if jumpCount = 0. Hence it is either level mi.u or mi.v.
   -- let σ ← mkFreshTypeMVar (userName := `σ)
-  let mutDecls ← mutVarNames.mapM (getLocalDeclFromUserName ·)
-  let mutTypes := mutDecls.map (·.type)
+  -- An erased variable's join parameter carries the `Erased` value; its projection rebinds below.
+  let mutTypes ← mutVars.mapM (·.stateType)
   let joinTy ← mkArrow nondupDec.resultType (← mkArrowN mutTypes mγ)
   let joinRhsMVar ← mkFreshExprSyntheticOpaqueMVar joinTy
   withLetDecl joinName joinTy joinRhsMVar (kind := .implDetail) (nondep := true) fun jp => do
@@ -697,9 +740,8 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     let result ← getFVarFromUserName nondupDec.resultName
     let mut e := mkApp jp' result
     for x in mutVars do
-      let newX ← getFVarFromUserName x.getId
-      Term.addTermInfo' x.ident newX
-      e := mkApp e (← getFVarFromUserName x.getId)
+      Term.addTermInfo' x.ident (← getFVarFromUserName x.getId)
+      e := mkApp e (← x.stateValue)
     return e
 
   let elabBody :=
@@ -710,9 +752,9 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
 
   let joinRhs ← joinRhsMVar.mvarId!.withContext do
     withLocalDeclD nondupDec.resultName nondupDec.resultType fun r => do
-    withLocalDeclsDND (mutDecls.map fun (d : LocalDecl) => (d.userName, d.type)) fun muts => do
+    withLocalDeclsDND ((mutVars.zip mutTypes).map fun (mv, t) => (mv.getId, t)) fun muts => do
     for (x, newX) in mutVars.zip muts do Term.addTermInfo' x.ident newX
-    let e ← (nondupDec.withDeadCodeFromInfo callerInfo).k
+    let e ← withErasedProjs mutVars (nondupDec.withDeadCodeFromInfo callerInfo).k
     mkLambdaFVars (#[r] ++ muts) e
   unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do
     joinRhsMVar.mvarId!.withContext do
diff --git a/src/Lean/Elab/Do/Control.lean b/src/Lean/Elab/Do/Control.lean
index afef07b33d86..e93239baf5cf 100644
--- a/src/Lean/Elab/Do/Control.lean
+++ b/src/Lean/Elab/Do/Control.lean
@@ -45,9 +45,8 @@ def ControlStack.stateT (baseMonadInfo : MonadInfo) (muts : Array MutVar) (σ :
     -- `e : StateT σ m α`. Fetch the state tuple `s : σ` and apply it to `e`, `e.run s`.
     -- See also `StateT.monadControl.liftWith`.
     let mutExprs ← muts.mapM fun x => do
-      let defn ← getLocalDeclFromUserName x.getId
-      Term.addTermInfo' x.ident defn.toExpr
-      pure defn.toExpr
+      Term.addTermInfo' x.ident (← getFVarFromUserName x.getId)
+      x.stateValue
     let (tuple, tupleTy) ← mkProdMkN mutExprs baseMonadInfo.u
     unless ← isDefEq tupleTy σ do -- just for sanity; maybe delete in the future
       throwError "State tuple type mismatch: expected {σ}, got {tupleTy}. This is a bug in the `do` elaborator."
@@ -64,7 +63,7 @@ def ControlStack.stateT (baseMonadInfo : MonadInfo) (muts : Array MutVar) (σ :
     base.restoreCont { resultName, resultType, k }
 where
   mutVarNames := muts.map (·.getId)
-  getσ := do mkProdN (← mutVarNames.mapM (LocalDecl.type <$> getLocalDeclFromUserName ·)) baseMonadInfo.u
+  getσ := do mkProdN (← muts.mapM (·.stateType)) baseMonadInfo.u
   stM α := return mkApp2 (mkConst ``Prod [baseMonadInfo.u, baseMonadInfo.u]) α (← getσ) -- NB: muts `σ` might have been refined by dependent pattern matches
 
 def ControlStack.optionT (baseMonadInfo : MonadInfo) (optionTWrapper casesOnWrapper : Name)
@@ -209,9 +208,8 @@ structure EffectForwarder where
 def EffectForwarder.ofCont (info : ControlInfo) (dec : DoElemCont) : DoElabM EffectForwarder := do
   let mi := (← read).monadInfo
   let reassignedMutVars := (← read).mutVars |>.filter (info.reassigns.contains ·.getId)
-  let reassignedMutVarNames := reassignedMutVars.map (·.getId)
   let ρ := (← getReturnCont).resultType
-  let σ ← mkProdN (← reassignedMutVarNames.mapM (LocalDecl.type <$> getLocalDeclFromUserName ·)) mi.u
+  let σ ← mkProdN (← reassignedMutVars.mapM (·.stateType)) mi.u
 
   let needEarlyReturn := if info.returnsEarly then some ρ else none
   let needBreak := info.breaks && (← getBreakCont).isSome
diff --git a/src/Lean/Elab/Do/InferControlInfo.lean b/src/Lean/Elab/Do/InferControlInfo.lean
index f7669e6274e3..c46ca91996ec 100644
--- a/src/Lean/Elab/Do/InferControlInfo.lean
+++ b/src/Lean/Elab/Do/InferControlInfo.lean
@@ -13,6 +13,9 @@ import Lean.Elab.Do.PatternVar
 
 public section
 
+-- The `erased` doElem quotations below need the current stage's parser until stage0 catches up.
+set_option internal.parseQuotWithCurrentStage true
+
 namespace Lean.Elab.Do
 
 open Lean Meta Parser.Term
@@ -157,6 +160,7 @@ partial def ofElem (stx : DoElem) : TermElabM ControlInfo := do
     ofLetOrReassign #[] none otherwise body?
   | `(doElem| let $[mut]? $_:letConfig $decl) =>
     ofLetOrReassignArrow false decl
+  | `(doErased| erased $[mut]? $_) => return .pure
   | `(doElem| $decl:letIdDeclNoBinders) =>
     ofLetOrReassign (← getLetIdDeclVars ⟨decl⟩) none none none
   | `(doElem| $decl:letPatDecl) =>
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 4de4f788ff9f..92fc8a4455d1 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -109,6 +109,13 @@ Motivations:
 def letIdDeclNoBinders := leading_parser
   atomic (node ``letId ident >> pushNone >> optType >> " := ") >> termParser
 
+/-- `erased x := e` declares a verification-only variable; `mut` allows reassignment. -/
+@[builtin_doElem_parser default+10] def doErased := leading_parser
+  nonReservedSymbol "erased " (includeIdent := true) >> optional "mut " >> letIdDeclNoBinders
+/-- `erased x ← act` runs `act` and hides its result in a verification-only variable. -/
+@[builtin_doElem_parser default+10] def doErasedArrow := leading_parser
+  nonReservedSymbol "erased " (includeIdent := true) >> optional "mut " >> doIdDecl
+
 @[builtin_doElem_parser] def doReassign      := leading_parser
   notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl)
 
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 3baec9ac0fdd..d96a46b866db 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,6 +1,6 @@
 #include "util/options.h"
 
-// [ ] Check box to force CI to test stage 2 and run update-stage0 on PR merge
+// [x] Check box to force CI to test stage 2 and run update-stage0 on PR merge
 // (any other change to this file will do the same; ALL changes should be made to the stage0/ copy)
 
 namespace lean {
diff --git a/tests/elab/erased.lean b/tests/elab/erased.lean
index 5f05656e5837..fe85abd14ce5 100644
--- a/tests/elab/erased.lean
+++ b/tests/elab/erased.lean
@@ -4,14 +4,14 @@ import Lean
   of `erased α` are erased in the VM in the same way as types
   and proofs. This can be used to track data without storing it
   literally. -/
-def Erased (α : Sort u) : Sort max 1 u :=
+def ErasedS (α : Sort u) : Sort max 1 u :=
   Σ's : α → Prop, ∃ a, (fun b => a = b) = s
 
-namespace Erased
+namespace ErasedS
 
 /-- Erase a value. -/
 @[inline]
-def mk {α} (a : α) : Erased α :=
+def mk {α} (a : α) : ErasedS α :=
   ⟨fun b => a = b, a, rfl⟩
 
 open Lean.Compiler
@@ -21,11 +21,11 @@ set_option pp.letVarTypes true
 set_option trace.Compiler.saveMono true
 /--
 trace: [Compiler.saveMono] size: 1
-    def Erased.mk._redArg (_dummy : lcVoid) : PSigma lcErased lcAny :=
+    def ErasedS.mk._redArg (_dummy : lcVoid) : PSigma lcErased lcAny :=
       let _x.1 : PSigma lcErased lcAny := PSigma.mk ◾ ◾ ◾ ◾;
       return _x.1
 [Compiler.saveMono] size: 1
-    def Erased.mk (α : lcErased) (a : lcAny) : PSigma lcErased lcAny :=
+    def ErasedS.mk (α : lcErased) (a : lcAny) : PSigma lcErased lcAny :=
       let _x.1 : PSigma lcErased lcAny := PSigma.mk ◾ ◾ ◾ ◾;
       return _x.1
 ---
@@ -43,7 +43,7 @@ trace: [Compiler.saveMono] size: 5
 [Compiler.saveMono] size: 9
     def _private.elab.erased.0._eval (a : @&Lean.Elab.Command.Context) (a : @&lcAny) (a.1 : lcVoid) : EST.Out
       Lean.Exception lcAny PUnit :=
-      let _x.2 : String := "Erased";
+      let _x.2 : String := "ErasedS";
       let _x.3 : String := "mk";
       let _x.4 : Lean.Name := Lean.Name.mkStr2 _x.2 _x.3;
       let _x.5 : Nat := 1;
@@ -58,4 +58,4 @@ trace: [Compiler.saveMono] size: 5
       return _x.10
 -/
 #guard_msgs in
-run_meta Lean.Compiler.compile #[``Erased.mk]
+run_meta Lean.Compiler.compile #[``ErasedS.mk]
diff --git a/tests/elab/formatTerm.lean b/tests/elab/formatTerm.lean
index db1d2e4c5299..730394759573 100644
--- a/tests/elab/formatTerm.lean
+++ b/tests/elab/formatTerm.lean
@@ -85,3 +85,8 @@ def foo : a b c d e f g a b c d e f g h where
   1 = 1 := rfl)
 
 #eval fmt `(by rw [] at h)
+
+-- `erased` is its own declaration form beside `let` and `have`
+#eval fmt `(do erased trace := 0; pure ())
+#eval fmt `(do erased mut trace : List Nat := []; trace := x :: trace.out)
+#eval fmt `(do erased mut n ← counter)
diff --git a/tests/elab/formatTerm.lean.out.expected b/tests/elab/formatTerm.lean.out.expected
index f03c982e5fdd..10104d663186 100644
--- a/tests/elab/formatTerm.lean.out.expected
+++ b/tests/elab/formatTerm.lean.out.expected
@@ -142,3 +142,11 @@ calc
   1 = 1 := rfl✝
   1 = 1 := rfl✝
 by rw [] at h✝
+do
+  erased trace✝ := 0;
+  pure✝ ()
+do
+  erased mut trace✝ : List✝ Nat✝ := [];
+  trace✝ := x✝ :: trace.out✝
+do
+  erased mut n✝ ← counter✝
diff --git a/tests/elab/intrinsicVerification.lean b/tests/elab/intrinsicVerification.lean
index 5ad1bd98405a..1f8a23410804 100644
--- a/tests/elab/intrinsicVerification.lean
+++ b/tests/elab/intrinsicVerification.lean
@@ -889,3 +889,123 @@ def onOneLine (k : Nat) : Id Nat given (n : Nat) requires k = n ensures r => r =
 /-- info: onOneLine.spec : ∀ (k n : Nat), ⦃ k = n ⦄ onOneLine k ⦃ fun r => r = n ⦄ -/
 #guard_msgs in
 #check @onOneLine.spec
+
+/-! ## Erased state
+
+`erased` declares verification-only state. The variable reads at its underlying type everywhere,
+its carried `Erased` binding erases in compiled code, and its slot in a loop's state tuple holds
+a dummy. -/
+
+def erasedSumEvens (xs : List Nat) : Id Nat
+    ensures r => r % 2 = 0 := do
+  let mut acc := 0
+  erased mut seen : List Nat := []
+  for x in xs invariant _pre _suff => acc = 2 * seen.length do
+    acc := acc + 2
+    seen := x :: seen
+  return acc
+
+/-- info: 6 -/
+#guard_msgs in
+#eval erasedSumEvens [1, 2, 3]
+
+/-! An existential `ensures` takes its witness from an erased variable: the invariant carries the
+witness, and the exit condition instantiates the existential from it. -/
+
+def erasedDoubleSum (xs : List Nat) : Id Nat
+    ensures r => ∃ n, r = 2 * n := do
+  let mut acc := 0
+  erased mut half : Nat := 0
+  for x in xs invariant _pre _suff => acc = 2 * half do
+    acc := acc + x + x
+    half := half + x
+  return acc
+
+/-- info: 12 -/
+#guard_msgs in
+#eval erasedDoubleSum [1, 2, 3]
+
+/-! The declaration forms: `erased` with and without `mut`, reassignment with an ascription, and
+monadic binds (the action runs, its result erases). -/
+
+def erasedForms : Id Nat := do
+  erased y := 5
+  erased mut x := 1
+  x := x + y
+  x : Nat := 2
+  erased z ← pure 3
+  erased mut m ← pure 4
+  m := m + z
+  pure 0
+
+/-- info: 0 -/
+#guard_msgs in
+#eval erasedForms
+
+/-! An erased variable reassigned in a branch flows through the join point. -/
+
+def erasedBranch (b : Bool) : Id Nat
+    ensures r => r = 0 := do
+  erased mut n : Nat := 0
+  if b then
+    n := n + 1
+  else
+    n := n + 2
+  assert n > 0
+  return 0
+
+/-- info: 0 -/
+#guard_msgs in
+#eval erasedBranch true
+
+/-! An erased value reaching compiled code is rejected through the noncomputability of
+`Erased.out`. -/
+
+/--
+error: failed to compile definition: it depends on 'Erased.out', which recovers the value of an erased variable. An erased variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'.
+-/
+#guard_msgs in
+def erasedLeak (xs : List Nat) : Id Nat := do
+  erased mut seen : List Nat := []
+  for x in xs do
+    seen := x :: seen
+  return seen.length
+
+/-! An erased reassignment checks a contradicting type ascription like a plain one. -/
+
+/--
+error: Type mismatch
+  g
+has type
+  Int
+but is expected to have type
+  Nat
+-/
+#guard_msgs in
+def erasedAscriptionMismatch : Id Nat := do
+  erased mut g : Int := 0
+  g : Nat := 1
+  pure 0
+
+/-! `erased` stays a regular identifier at a doElem head when no erased shape parses. -/
+
+def erasedAsIdent (erased : Nat → Id Unit) : Id Nat := do
+  erased 5
+  let mut erased := 1
+  erased := erased + 1
+  erased ← pure 3
+  pure erased
+
+/-- info: 3 -/
+#guard_msgs in
+#eval erasedAsIdent fun _ => pure ()
+
+/-! An erased variable stays out of pattern reassignments. -/
+
+/-- error: an erased variable takes a plain reassignment, as in `g := e` -/
+#guard_msgs in
+def erasedPatReassign : Id Nat := do
+  let mut a := 1
+  erased mut g := 2
+  (a, g) := (3, 4)
+  pure a
diff --git a/tests/elab/usesOfNoncomputable.lean b/tests/elab/usesOfNoncomputable.lean
index 97d46d39b91d..edbd0cc1004e 100644
--- a/tests/elab/usesOfNoncomputable.lean
+++ b/tests/elab/usesOfNoncomputable.lean
@@ -41,17 +41,7 @@ error: failed to compile definition, consider marking it as 'noncomputable' beca
 #guard_msgs in
 def test9 (a : Nat) : V := ⟨a, badFun a⟩
 
-universe u
-
-def Erased (α : Sort u) : Sort max 1 u :=
-  { s : α → Prop // ∃ a, (a = ·) = s }
-
-@[macro_inline] def Erased.mk {α} (a : α) : Erased α :=
-  ⟨fun b => a = b, a, rfl⟩
-
-noncomputable def Erased.out {α} : Erased α → α
-  | ⟨_, h⟩ => Classical.choose h
-
+-- `Erased.mk` is `macro_inline`, so its argument erases and `.out` inside it compiles.
 structure Foo where
   spec : Erased Nat
   data : Nat
@@ -61,7 +51,7 @@ def test10 : Foo where
   data := 0
 
 /--
-error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Erased.out', which is 'noncomputable'
+error: failed to compile definition: it depends on 'Erased.out', which recovers the value of an erased variable. An erased variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'.
 -/
 #guard_msgs in
 def test11 : Foo where