chore: document replaceUnsafeM issue

Declarations with `@[elab_as_elim]` could elaborate as type-incorrect
expressions. Reported by Jireh Loreaux [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bug.20in.20revert/near/450522157).

(In principle the elabAsElim routine could revert fvars appearing in the
expected type that depend on the discriminants (if the discriminants are
fvars) to increase the likelihood of type correctness, but that's at the
cost of some complexity to both the elaborator and to the user.)

src/Init/Ext.lean

@@ -24,15 +24,16 @@ syntax extFlat := atomic("(" &"flat" " := " &"false" ")")
 /--
 Registers an extensionality theorem.
 
-* When `@[ext]` is applied to a structure, it generates `.ext` and `.ext_iff` theorems and registers
-  them for the `ext` tactic.
-
-* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an `ext_iff` theorem.
+* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an "`ext_iff`" theorem.
   The name of the theorem is from adding the suffix `_iff` to the theorem name.
 
-* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the lemma. Higher-priority lemmas are chosen first, and the default is `1000`.
+* When `@[ext]` is applied to a structure, it generates an `.ext` theorem and applies the `@[ext]` attribute to it.
+  The result is an `.ext` and an `.ext_iff` theorem with the `.ext` theorem registered for the `ext` tactic.
 
-* The flag `@[ext (iff := false)]` prevents it from generating an `ext_iff` theorem.
+* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the `ext` lemma.
+  Higher-priority lemmas are chosen first, and the default is `1000`.
+
+* The flag `@[ext (iff := false)]` disables generating an `ext_iff` theorem.
 
 * The flag `@[ext (flat := false)]` causes generated structure extensionality theorems to show inherited fields based on their representation,
   rather than flattening the parents' fields into the lemma's equality hypotheses.

src/Init/Util.lean

@@ -45,6 +45,13 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
 @[extern "lean_ptr_addr"]
 unsafe opaque ptrAddrUnsafe {α : Type u} (a : @& α) : USize
 
+/--
+Returns `true` if `a` is an exclusive object.
+We say an object is exclusive if it is single-threaded and its reference counter is 1.
+-/
+@[extern "lean_is_exclusive_obj"]
+unsafe opaque isExclusiveUnsafe {α : Type u} (a : @& α) : Bool
+
 set_option linter.unusedVariables.funArgs false in
 @[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
   k (ptrAddrUnsafe a)

src/Lean/Data/RBMap.lean

@@ -80,6 +80,10 @@ protected def max : RBNode α β → Option (Sigma (fun k => β k))
 def singleton (k : α) (v : β k) : RBNode α β :=
   node red leaf k v leaf
 
+def isSingleton : RBNode α β → Bool
+  | node _ leaf _ _ leaf => true
+  | _ => false
+
 -- the first half of Okasaki's `balance`, concerning red-red sequences in the left child
 @[inline] def balance1 : RBNode α β → (a : α) → β a → RBNode α β → RBNode α β
   | node red (node red a kx vx b) ky vy c, kz, vz, d
@@ -269,6 +273,9 @@ variable {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering
 def depth (f : Nat → Nat → Nat) (t : RBMap α β cmp) : Nat :=
   t.val.depth f
 
+def isSingleton (t : RBMap α β cmp) : Bool :=
+  t.val.isSingleton
+
 @[inline] def fold (f : σ → α → β → σ) : (init : σ) → RBMap α β cmp → σ
   | b, ⟨t, _⟩ => t.fold f b
 

src/Lean/Elab/App.lean

@@ -742,7 +742,10 @@ def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do
     let motiveBody ← kabstract motive discr
     /- We use `transform (usedLetOnly := true)` to eliminate unnecessary let-expressions. -/
     let discrType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType discr))
-    return Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
+    let motive := Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
+    unless (← isTypeCorrect motive) do
+      throwError "failed to elaborate eliminator, motive is not type correct:{indentD motive}"
+    return motive
 
 /-- If the eliminator is over-applied, we "revert" the extra arguments. -/
 def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) :=

src/Lean/Elab/MutualDef.lean

@@ -728,12 +728,26 @@ def insertReplacementForLetRecs (r : Replacement) (letRecClosures : List LetRecC
   letRecClosures.foldl (init := r) fun r c =>
     r.insert c.toLift.fvarId c.closed
 
+def isApplicable (r : Replacement) (e : Expr) : Bool :=
+  Option.isSome <| e.findExt? fun e =>
+    if e.hasFVar then
+      match e with
+      | .fvar fvarId => if r.contains fvarId then .found else .done
+      | _ => .visit
+    else
+      .done
+
 def Replacement.apply (r : Replacement) (e : Expr) : Expr :=
-  e.replace fun e => match e with
-    | .fvar fvarId => match r.find? fvarId with
-      | some c => some c
-      | _      => none
-    | _ => none
+  -- Remark: if `r` is not a singlenton, then declaration is using `mutual` or `let rec`,
+  -- and there is a big chance `isApplicable r e` is true.
+  if r.isSingleton && !isApplicable r e then
+    e
+  else
+    e.replace fun e => match e with
+      | .fvar fvarId => match r.find? fvarId with
+        | some c => some c
+        | _      => none
+      | _ => none
 
 def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainVals : Array Expr)
     : TermElabM (Array PreDefinition) :=

src/Lean/Elab/Tactic/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
+import Lean.Meta.Tactic.Util
 import Lean.Elab.Term
 
 namespace Lean.Elab
@@ -398,12 +399,19 @@ def ensureHasNoMVars (e : Expr) : TacticM Unit := do
   if e.hasExprMVar then
     throwError "tactic failed, resulting expression contains metavariables{indentExpr e}"
 
-/-- Close main goal using the given expression. If `checkUnassigned == true`, then `val` must not contain unassigned metavariables. -/
-def closeMainGoal (val : Expr) (checkUnassigned := true): TacticM Unit := do
+/--
+Closes main goal using the given expression.
+If `checkUnassigned == true`, then `val` must not contain unassigned metavariables.
+Returns `true` if `val` was successfully used to close the goal.
+-/
+def closeMainGoal (tacName : Name) (val : Expr) (checkUnassigned := true): TacticM Unit := do
   if checkUnassigned then
     ensureHasNoMVars val
-  (← getMainGoal).assign val
-  replaceMainGoal []
+  let mvarId ← getMainGoal
+  if (← mvarId.checkedAssign val) then
+    replaceMainGoal []
+  else
+    throwTacticEx tacName mvarId m!"attempting to close the goal using{indentExpr val}\nthis is often due occurs-check failure"
 
 @[inline] def liftMetaMAtMain (x : MVarId → MetaM α) : TacticM α := do
   withMainContext do x (← getMainGoal)

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -56,9 +56,9 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpo
     return e
 
 /-- Try to close main goal using `x target`, where `target` is the type of the main goal.  -/
-def closeMainGoalUsing (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit :=
+def closeMainGoalUsing (tacName : Name) (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit :=
   withMainContext do
-    closeMainGoal (checkUnassigned := checkUnassigned) (← x (← getMainTarget))
+    closeMainGoal (tacName := tacName) (checkUnassigned := checkUnassigned) (← x (← getMainTarget))
 
 def logUnassignedAndAbort (mvarIds : Array MVarId) : TacticM Unit := do
    if (← Term.logUnassignedUsingErrorInfos mvarIds) then
@@ -68,13 +68,14 @@ def filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) : MetaM (Ar
   let mctx ← getMCtx
   return mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved
 
-@[builtin_tactic «exact»] def evalExact : Tactic := fun stx =>
+@[builtin_tactic «exact»] def evalExact : Tactic := fun stx => do
   match stx with
-  | `(tactic| exact $e) => closeMainGoalUsing (checkUnassigned := false) fun type => do
-    let mvarCounterSaved := (← getMCtx).mvarCounter
-    let r ← elabTermEnsuringType e type
-    logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
-    return r
+  | `(tactic| exact $e) =>
+    closeMainGoalUsing `exact (checkUnassigned := false) fun type => do
+      let mvarCounterSaved := (← getMCtx).mvarCounter
+      let r ← elabTermEnsuringType e type
+      logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
+      return r
   | _ => throwUnsupportedSyntax
 
 def sortMVarIdArrayByIndex [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) : m (Array MVarId) := do
@@ -393,7 +394,7 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := do
   return inst
 
 @[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
-  closeMainGoalUsing fun expectedType => do
+  closeMainGoalUsing `decide fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let d ← instantiateMVars d
@@ -472,7 +473,7 @@ private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Na
   pure auxName
 
 @[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ =>
-  closeMainGoalUsing fun expectedType => do
+  closeMainGoalUsing `nativeDecide fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d

src/Lean/Elab/Tactic/Ext.lean

@@ -74,16 +74,16 @@ def mkExtIffType (extThmName : Name) : MetaM Expr := withLCtx {} {} do
     let some (_, x, y) := ty.eq? | failNotEq
     let some xIdx := args.findIdx? (· == x) | failNotEq
     let some yIdx := args.findIdx? (· == y) | failNotEq
-    unless xIdx == yIdx + 1 || xIdx + 1 == yIdx do
+    unless xIdx + 1 == yIdx do
       throwError "expecting {x} and {y} to be consecutive arguments"
-    let startIdx := max xIdx yIdx + 1
+    let startIdx := yIdx + 1
     let toRevert := args[startIdx:].toArray
     let fvars ← toRevert.foldlM (init := {}) (fun st e => return collectFVars st (← inferType e))
     for fvar in toRevert do
       unless ← Meta.isProof fvar do
-        throwError "argument {fvar} is not a proof, which is not supported"
+        throwError "argument {fvar} is not a proof, which is not supported for arguments after {x} and {y}"
       if fvars.fvarSet.contains fvar.fvarId! then
-        throwError "argument {fvar} is depended upon, which is not supported"
+        throwError "argument {fvar} is depended upon, which is not supported for arguments after {x} and {y}"
     let conj := mkAndN (← toRevert.mapM (inferType ·)).toList
     -- Make everything implicit except for inst implicits
     let mut newBis := #[]
@@ -104,27 +104,31 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
     throwError "'{structName}' is not a structure"
   let extName := structName.mkStr "ext"
   unless (← getEnv).contains extName do
-    Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do
-      let type ← mkExtType structName flat
-      let pf ← withSynthesize do
-        let indVal ← getConstInfoInduct structName
-        let params := Array.mkArray indVal.numParams (← `(_))
-        Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
-          -- introduce the params, do cases on 'x' and 'y', and then substitute each equation
-          (← `(by intro $params* {..} {..}; intros; subst_eqs; rfl))
-      let pf ← instantiateMVars pf
-      if pf.hasMVar then throwError "(internal error) synthesized ext proof contains metavariables{indentD pf}"
-      let info ← getConstInfo structName
-      addDecl <| Declaration.thmDecl {
-        name := extName
-        type
-        value := pf
-        levelParams := info.levelParams
-      }
-      modifyEnv fun env => addProtected env extName
-      Lean.addDeclarationRanges extName {
-        range := ← getDeclarationRange (← getRef)
-        selectionRange := ← getDeclarationRange (← getRef) }
+    try
+      Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do
+        let type ← mkExtType structName flat
+        let pf ← withSynthesize do
+          let indVal ← getConstInfoInduct structName
+          let params := Array.mkArray indVal.numParams (← `(_))
+          Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
+            -- introduce the params, do cases on 'x' and 'y', and then substitute each equation
+            (← `(by intro $params* {..} {..}; intros; subst_eqs; rfl))
+        let pf ← instantiateMVars pf
+        if pf.hasMVar then throwError "(internal error) synthesized ext proof contains metavariables{indentD pf}"
+        let info ← getConstInfo structName
+        addDecl <| Declaration.thmDecl {
+          name := extName
+          type
+          value := pf
+          levelParams := info.levelParams
+        }
+        modifyEnv fun env => addProtected env extName
+        Lean.addDeclarationRanges extName {
+          range := ← getDeclarationRange (← getRef)
+          selectionRange := ← getDeclarationRange (← getRef) }
+    catch e =>
+      throwError m!"\
+        Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}"
   return extName
 
 /--
@@ -138,29 +142,35 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
     | .str n s => .str n (s ++ "_iff")
     | _ => .str extName "ext_iff"
   unless (← getEnv).contains extIffName do
-    let info ← getConstInfo extName
-    Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do
-      let type ← mkExtIffType extName
-      let pf ← withSynthesize do
-        Elab.Term.elabTermEnsuringType (expectedType? := type) <| ← `(by
-          intros
-          refine ⟨?_, ?_⟩
-          · intro h; cases h; and_intros <;> (intros; first | rfl | simp | fail "Failed to prove converse of ext theorem")
-          · intro; (repeat cases ‹_ ∧ _›); apply $(mkCIdent extName) <;> assumption)
-      let pf ← instantiateMVars pf
-      if pf.hasMVar then throwError "(internal error) synthesized ext_iff proof contains metavariables{indentD pf}"
-      addDecl <| Declaration.thmDecl {
-        name := extIffName
-        type
-        value := pf
-        levelParams := info.levelParams
-      }
-      -- Only declarations in a namespace can be protected:
-      unless extIffName.isAtomic do
-        modifyEnv fun env => addProtected env extIffName
-      Lean.addDeclarationRanges extIffName {
-        range := ← getDeclarationRange (← getRef)
-        selectionRange := ← getDeclarationRange (← getRef) }
+    try
+      let info ← getConstInfo extName
+      Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do
+        let type ← mkExtIffType extName
+        let pf ← withSynthesize do
+          Elab.Term.elabTermEnsuringType (expectedType? := type) <| ← `(by
+            intros
+            refine ⟨?_, ?_⟩
+            · intro h; cases h; and_intros <;> (intros; first | rfl | simp | fail "Failed to prove converse of ext theorem")
+            · intro; (repeat cases ‹_ ∧ _›); apply $(mkCIdent extName) <;> assumption)
+        let pf ← instantiateMVars pf
+        if pf.hasMVar then throwError "(internal error) synthesized ext_iff proof contains metavariables{indentD pf}"
+        addDecl <| Declaration.thmDecl {
+          name := extIffName
+          type
+          value := pf
+          levelParams := info.levelParams
+        }
+        -- Only declarations in a namespace can be protected:
+        unless extIffName.isAtomic do
+          modifyEnv fun env => addProtected env extIffName
+        Lean.addDeclarationRanges extIffName {
+          range := ← getDeclarationRange (← getRef)
+          selectionRange := ← getDeclarationRange (← getRef) }
+    catch e =>
+      throwError m!"\
+        Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\
+        \n\
+        Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem."
   return extIffName
 
 

src/Lean/Meta/Basic.lean

@@ -1865,9 +1865,13 @@ abbrev isDefEqGuarded (t s : Expr) : MetaM Bool :=
 def isDefEqNoConstantApprox (t s : Expr) : MetaM Bool :=
   approxDefEq <| isDefEq t s
 
-/-- Shorthand for `isDefEq (mkMVar mvarId) val` -/
-def _root_.Lean.MVarId.checkedAssign (mvarId : MVarId) (val : Expr) : MetaM Bool :=
-  isDefEq (mkMVar mvarId) val
+/--
+Returns `true` if `mvarId := val` was successfully assigned.
+This method uses the same assignment validation performed by `isDefEq`, but it does not check whether the types match.
+-/
+-- Remark: this method is implemented at `ExprDefEq`
+@[extern "lean_checked_assign"]
+opaque _root_.Lean.MVarId.checkedAssign (mvarId : MVarId) (val : Expr) : MetaM Bool
 
 /--
   Eta expand the given expression.

src/Lean/Meta/ExprDefEq.lean

@@ -1046,6 +1046,15 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O
       return none
     return some v
 
+-- Implementation for `_root_.Lean.MVarId.checkedAssign`
+@[export lean_checked_assign]
+def checkedAssignImpl (mvarId : MVarId) (val : Expr) : MetaM Bool := do
+  if let some val ← checkAssignment mvarId #[] val then
+    mvarId.assign val
+    return true
+  else
+    return false
+
 private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool :=
   match v with
   | .mdata _ e   => processAssignmentFOApproxAux mvar args e

src/Lean/Util/PtrSet.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Hashable
 import Lean.Data.HashSet
+import Lean.Data.HashMap
 
 namespace Lean
 
@@ -33,4 +34,22 @@ unsafe abbrev PtrSet.insert (s : PtrSet α) (a : α) : PtrSet α :=
 unsafe abbrev PtrSet.contains (s : PtrSet α) (a : α) : Bool :=
   HashSet.contains s { value := a }
 
+/--
+Map of pointers. It is a low-level auxiliary datastructure used for traversing DAGs.
+-/
+unsafe def PtrMap (α : Type) (β : Type) :=
+  HashMap (Ptr α) β
+
+unsafe def mkPtrMap {α β : Type} (capacity : Nat := 64) : PtrMap α β :=
+  mkHashMap capacity
+
+unsafe abbrev PtrMap.insert (s : PtrMap α β) (a : α) (b : β) : PtrMap α β :=
+  HashMap.insert s { value := a } b
+
+unsafe abbrev PtrMap.contains (s : PtrMap α β) (a : α) : Bool :=
+  HashMap.contains s { value := a }
+
+unsafe abbrev PtrMap.find? (s : PtrMap α β) (a : α) : Option β :=
+  HashMap.find? s { value := a }
+
 end Lean

src/Lean/Util/ReplaceExpr.lean

@@ -5,74 +5,59 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
 -/
 prelude
 import Lean.Expr
+import Lean.Util.PtrSet
 
 namespace Lean
 namespace Expr
 
 namespace ReplaceImpl
 
-structure Cache where
-  size : USize
-  -- First `size` elements are the keys.
-  -- Second `size` elements are the results.
-  keysResults : Array NonScalar -- Either Expr or Unit (disjoint memory representation)
+unsafe abbrev ReplaceM := StateM (PtrMap Expr Expr)
 
-unsafe def Cache.new (e : Expr) : Cache :=
-  -- scale size with approximate number of subterms up to 8k
-  -- make sure size is coprime with power of two for collision avoidance
-  let size := (1 <<< min (max e.approxDepth.toUSize 1) 13) - 1
-  { size, keysResults := mkArray (2 * size).toNat (unsafeCast ()) }
-
-@[inline]
-unsafe def Cache.keyIdx (c : Cache) (key : Expr) : USize :=
-  ptrAddrUnsafe key % c.size
-
-@[inline]
-unsafe def Cache.resultIdx (c : Cache) (key : Expr) : USize :=
-  c.keyIdx key + c.size
-
-@[inline]
-unsafe def Cache.hasResultFor (c : Cache) (key : Expr) : Bool :=
-  have : (c.keyIdx key).toNat < c.keysResults.size := lcProof
-  ptrEq (unsafeCast key) c.keysResults[c.keyIdx key]
-
-@[inline]
-unsafe def Cache.getResultFor (c : Cache) (key : Expr) : Expr :=
-  have : (c.resultIdx key).toNat < c.keysResults.size := lcProof
-  unsafeCast c.keysResults[c.resultIdx key]
-
-unsafe def Cache.store (c : Cache) (key result : Expr) : Cache :=
-  { c with keysResults := c.keysResults
-    |>.uset (c.keyIdx key) (unsafeCast key) lcProof
-    |>.uset (c.resultIdx key) (unsafeCast result) lcProof }
-
-abbrev ReplaceM := StateM Cache
-
-@[inline]
-unsafe def cache (key : Expr) (result : Expr) : ReplaceM Expr := do
-  modify (·.store key result)
+unsafe def cache (key : Expr) (exclusive : Bool)  (result : Expr) : ReplaceM Expr := do
+  unless exclusive do
+    modify (·.insert key result)
   pure result
 
 @[specialize]
 unsafe def replaceUnsafeM (f? : Expr → Option Expr) (e : Expr) : ReplaceM Expr := do
   let rec @[specialize] visit (e : Expr) := do
-    if (← get).hasResultFor e then
-      return (← get).getResultFor e
-    else match f? e with
-      | some eNew => cache e eNew
+    /-
+    TODO: We need better control over RC operations to ensure
+    the following (unsafe) optimization is correctly applied.
+    Optimization goal: only cache results for shared objects.
+
+    The main problem is that the current code generator ignores borrow annotations
+    for code written in Lean. These annotations are only taken into account for extern functions.
+
+    Moveover, the borrow inference heuristic currently tags `e` as "owned" since it may be stored
+    in the cache and is used in "update" functions.
+    Thus, when visiting `e` sub-expressions the code generator increases their RC
+    because we are recursively invoking `visit` :(
+
+    Thus, to fix this issue, we must
+    1- Take borrow annotations into account for code written in Lean.
+    2- Mark `e` is borrowed (i.e., `(e : @& Expr)`)
+    -/
+    let excl := isExclusiveUnsafe e
+    unless excl do
+      if let some result := (← get).find? e then
+        return result
+    match f? e with
+      | some eNew => cache e excl eNew
       | none      => match e with
-        | Expr.forallE _ d b _   => cache e <| e.updateForallE! (← visit d) (← visit b)
-        | Expr.lam _ d b _       => cache e <| e.updateLambdaE! (← visit d) (← visit b)
-        | Expr.mdata _ b         => cache e <| e.updateMData! (← visit b)
-        | Expr.letE _ t v b _    => cache e <| e.updateLet! (← visit t) (← visit v) (← visit b)
-        | Expr.app f a           => cache e <| e.updateApp! (← visit f) (← visit a)
-        | Expr.proj _ _ b        => cache e <| e.updateProj! (← visit b)
-        | e                      => pure e
+        | .forallE _ d b _   => cache e excl <| e.updateForallE! (← visit d) (← visit b)
+        | .lam _ d b _       => cache e excl <| e.updateLambdaE! (← visit d) (← visit b)
+        | .mdata _ b         => cache e excl <| e.updateMData! (← visit b)
+        | .letE _ t v b _    => cache e excl <| e.updateLet! (← visit t) (← visit v) (← visit b)
+        | .app f a           => cache e excl <| e.updateApp! (← visit f) (← visit a)
+        | .proj _ _ b        => cache e excl <| e.updateProj! (← visit b)
+        | e                  => return e
   visit e
 
 @[inline]
 unsafe def replaceUnsafe (f? : Expr → Option Expr) (e : Expr) : Expr :=
-  (replaceUnsafeM f? e).run' (Cache.new e)
+  (replaceUnsafeM f? e).run' mkPtrMap
 
 end ReplaceImpl
 

src/include/lean/lean.h

@@ -481,6 +481,10 @@ static inline bool lean_is_exclusive(lean_object * o) {
     }
 }
 
+static inline uint8_t lean_is_exclusive_obj(lean_object * o) {
+    return lean_is_exclusive(o);
+}
+
 static inline bool lean_is_shared(lean_object * o) {
     if (LEAN_LIKELY(lean_is_st(o))) {
         return o->m_rc > 1;
@@ -1133,6 +1137,17 @@ static inline void * lean_get_external_data(lean_object * o) {
     return lean_to_external(o)->m_data;
 }
 
+static inline lean_object * lean_set_external_data(lean_object * o, void * data) {
+    if (lean_is_exclusive(o)) {
+        lean_to_external(o)->m_data = data;
+        return o;
+    } else {
+        lean_object * o_new = lean_alloc_external(lean_get_external_class(o), data);
+        lean_dec_ref(o);
+        return o_new;
+    }
+}
+
 /* Natural numbers */
 
 #define LEAN_MAX_SMALL_NAT (SIZE_MAX >> 1)

src/runtime/sharecommon.cpp

@@ -358,30 +358,16 @@ class sharecommon_quick_fn {
         return result;
     }
 
-    lean_object * visit_sarray(lean_object * a) {
-        lean_object * r = check_cache(a);
-        if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
-
-        size_t sz        = lean_sarray_size(a);
-        unsigned elem_sz = lean_sarray_elem_size(a);
-        lean_sarray_object * new_a = (lean_sarray_object*)lean_alloc_sarray(elem_sz, sz, sz);
-        memcpy(new_a->m_data, lean_to_sarray(a)->m_data, elem_sz*sz);
-        return save(a, (lean_object*)new_a);
-    }
-
-    lean_object * visit_string(lean_object * a) {
-        lean_object * r = check_cache(a);
-        if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
-
-        size_t sz     = lean_string_size(a);
-        size_t len    = lean_string_len(a);
-        lean_string_object * new_a = (lean_string_object*)lean_alloc_string(sz, sz, len);
-        lean_set_st_header((lean_object*)new_a, LeanString, 0);
-        new_a->m_size     = sz;
-        new_a->m_capacity = sz;
-        new_a->m_length   = len;
-        memcpy(new_a->m_data, lean_to_string(a)->m_data, sz);
-        return save(a, (lean_object*)new_a);
+    // `sarray` and `string`
+    lean_object * visit_terminal(lean_object * a) {
+        auto it = m_set.find(a);
+        if (it == m_set.end()) {
+            m_set.insert(a);
+        } else {
+            a = *it;
+        }
+        lean_inc_ref(a);
+        return a;
     }
 
     lean_object * visit_array(lean_object * a) {
@@ -399,7 +385,6 @@ class sharecommon_quick_fn {
     lean_object * visit_ctor(lean_object * a) {
         lean_object * r = check_cache(a);
         if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
-
         unsigned num_objs      = lean_ctor_num_objs(a);
         unsigned tag           = lean_ptr_tag(a);
         unsigned sz            = lean_object_byte_size(a);
@@ -442,9 +427,9 @@ public:
         case LeanRef:             lean_inc_ref(a); return a;
         case LeanExternal:        lean_inc_ref(a); return a;
         case LeanReserved:        lean_inc_ref(a); return a;
+        case LeanScalarArray:     return visit_terminal(a);
+        case LeanString:          return visit_terminal(a);
         case LeanArray:           return visit_array(a);
-        case LeanScalarArray:     return visit_sarray(a);
-        case LeanString:          return visit_string(a);
         default:                  return visit_ctor(a);
         }
     }

tests/lean/elabAsElim.lean

@@ -87,3 +87,12 @@ noncomputable def f : Nat → Nat :=
 
 example : ∀ x, x ≥ 0 :=
   Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih)
+
+@[elab_as_elim]
+def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry
+
+example {n : Type} {T : n} : T = T := Foo.induction n -- motive is not type correct
+
+example {n : Type} : {T : n} → T = T := Foo.induction n -- motive is not type correct
+
+example {n : Type} : {T : n} → T = T := @(Foo.induction n)

tests/lean/elabAsElim.lean.expected.out

@@ -1,3 +1,8 @@
 elabAsElim.lean:9:2-9:14: error: failed to elaborate eliminator, insufficient number of arguments, expected type:
   Nat
 elabAsElim.lean:26:2-26:24: error: failed to elaborate eliminator, unused named arguments: [a]
+elabAsElim.lean:92:4-92:17: warning: declaration uses 'sorry'
+elabAsElim.lean:94:38-94:53: error: failed to elaborate eliminator, motive is not type correct:
+  fun x => T = T
+elabAsElim.lean:96:40-96:55: error: failed to elaborate eliminator, motive is not type correct:
+  fun x => T✝ = T✝

tests/lean/run/2243.lean

@@ -2,7 +2,7 @@ import Lean
 
 open Lean Elab Tactic in
 elab "exact_false" : tactic =>
-  closeMainGoal (mkConst ``Bool.false)
+  closeMainGoal `exact_false (mkConst ``Bool.false)
 
 def f (b : Bool := by exact_false) : Nat := bif b then 1 else 0
 

tests/lean/run/4773.lean

@@ -0,0 +1,11 @@
+/--
+error: tactic 'exact' failed, attempting to close the goal using
+  ?loop
+this is often due occurs-check failure
+case loop
+⊢ False
+-/
+#guard_msgs in
+example : False := by
+  refine ?loop
+  exact ?loop

tests/lean/run/ext.lean

@@ -138,3 +138,35 @@ attribute [local ext] Subsingleton.elim
 /-- info: Subsingleton.elim_iff.{u} {α : Sort u} [h : Subsingleton α] {a b : α} : a = b ↔ True -/
 #guard_msgs in #check Subsingleton.elim_iff
 end
+
+
+/-!
+More informative error (issue #4758)
+-/
+
+/--
+warning: declaration uses 'sorry'
+---
+error: Failed to generate an 'ext_iff' theorem from 'weird_prod_ext': argument f is not a proof, which is not supported for arguments after p and q
+
+Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem.
+-/
+#guard_msgs in
+@[ext]
+theorem weird_prod_ext (p q : α × β)
+    (f : α → α') (g : β → β') -- (hf : Function.Injective f) (hg : Function.Injective g)
+    (h : f p.1 = f q.1) (h' : g p.2 = g q.2) :
+  p = q := sorry
+
+/--
+error: Failed to generate an 'ext_iff' theorem from 'ext'': argument h1 is depended upon, which is not supported for arguments after p and q
+
+Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem.
+-/
+#guard_msgs in
+@[ext]
+theorem Sigma.ext' {β : α → Type _} (p q : (i : α) × β i)
+    (h1 : p.1 = q.1)
+    (h2 : h1 ▸ p.2 = q.2) :
+    p = q := by
+  cases p; cases q; cases h1; cases h2; rfl