chore: CI: ignore compile_bench/channel in Linux Reldebug

This PR fixes git revision detection in worktrees where the worktree's
gitdir path passes through another git repository.

The vendored `GetGitRevisionDescription.cmake` module detects worktrees
and then calls `_git_find_closest_git_dir` to find the shared git
directory by walking up the filesystem looking for a `.git` entry. This
fails when the worktree's gitdir is stored inside another git repository
(e.g. when the project is a git submodule whose objects live at
`~/.git/modules/...` and `~` is itself a git repo) — the walk finds the
wrong `.git`.

The fix reads the `commondir` file that git places in every worktree's
gitdir, which directly points to the shared git object directory. Falls
back to the old filesystem walk if `commondir` doesn't exist (shouldn't
happen with any modern git, but safe to keep).

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

.claude/CLAUDE.md

@@ -66,6 +66,8 @@ To rebuild individual stage 2 modules without a full `make stage2`, use Lake dir
 cd build/release/stage2 && lake build Init.Prelude
 ```
 
+To run tests in stage2, replace `-C build/release` from above with `-C build/release/stage2`.
+
 ## New features
 
 When asked to implement new features:

.github/workflows/ci.yml

@@ -305,7 +305,8 @@ jobs:
                 "test": true,
                 "CMAKE_PRESET": "reldebug",
                 // * `elab_bench/big_do` crashes with exit code 134
-                "CTEST_OPTIONS": "-E 'elab_bench/big_do'",
+                // * `compile_bench/channel` randomly segfaults
+                "CTEST_OPTIONS": "-E 'elab_bench/big_do|compile_bench/channel'",
               },
               {
                 "name": "Linux fsanitize",

src/Init/Data/Array/Basic.lean

@@ -802,6 +802,7 @@ Examples:
 def firstM {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Array α) : m β :=
   go 0
 where
+  @[specialize]
   go (i : Nat) : m β :=
     if hlt : i < as.size then
       f as[i] <|> go (i+1)
@@ -1264,7 +1265,7 @@ Examples:
 -/
 @[inline, expose]
 def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
-  let rec loop (j : Nat) :=
+  let rec @[specialize] loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none

src/Init/Data/List/Basic.lean

@@ -282,6 +282,7 @@ The lexicographic order with respect to `lt` is:
 * `as.lex [] = false` is `false`
 * `(a :: as).lex (b :: bs)` is true if `lt a b` or `a == b` and `lex lt as bs` is true.
 -/
+@[specialize]
 def lex [BEq α] (l₁ l₂ : List α) (lt : α → α → Bool := by exact (· < ·)) : Bool :=
   match l₁, l₂ with
   | [],      _ :: _  => true
@@ -1004,6 +1005,7 @@ Examples:
  * `[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 4) = [8, 3, 2, 4, 2, 7, 4]`
  * `[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 100) = []`
 -/
+@[specialize]
 def dropWhile (p : α → Bool) : List α → List α
   | []   => []
   | a::l => match p a with
@@ -1460,9 +1462,11 @@ Examples:
 ["circle", "square", "triangle"]
 ```
 -/
+@[inline]
 def modifyTailIdx (l : List α) (i : Nat) (f : List α → List α) : List α :=
   go i l
 where
+  @[specialize]
   go : Nat → List α → List α
   | 0, l => f l
   | _+1, [] => []
@@ -1498,6 +1502,7 @@ Examples:
  * `[1, 2, 3].modify 2 (· * 10) = [1, 2, 30]`
  * `[1, 2, 3].modify 3 (· * 10) = [1, 2, 3]`
 -/
+@[inline]
 def modify (l : List α) (i : Nat) (f : α → α) : List α :=
   l.modifyTailIdx i (modifyHead f)
 
@@ -1604,6 +1609,7 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1`
 * `[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none`
 -/
+@[specialize]
 def find? (p : α → Bool) : List α → Option α
   | []    => none
   | a::as => match p a with
@@ -1626,6 +1632,7 @@ Examples:
  * `[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
  * `[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
+@[specialize]
 def findSome? (f : α → Option β) : List α → Option β
   | []    => none
   | a::as => match f a with
@@ -1649,6 +1656,7 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 5) = some 2`
 * `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 1) = none`
 -/
+@[specialize]
 def findRev? (p : α → Bool) : List α → Option α
   | []    => none
   | a::as => match findRev? p as with
@@ -1667,6 +1675,7 @@ Examples:
  * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 5 then some (10 * x) else none) = some 20`
  * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
+@[specialize]
 def findSomeRev? (f : α → Option β) : List α → Option β
   | []    => none
   | a::as => match findSomeRev? f as with
@@ -1717,9 +1726,11 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4`
 * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none`
 -/
+@[inline]
 def findIdx? (p : α → Bool) (l : List α) : Option Nat :=
   go l 0
 where
+  @[specialize]
   go : List α → Nat → Option Nat
   | [], _ => none
   | a :: l, i => if p a then some i else go l (i + 1)
@@ -1750,6 +1761,7 @@ Examples:
 @[inline] def findFinIdx? (p : α → Bool) (l : List α) : Option (Fin l.length) :=
   go l 0 (by simp)
 where
+  @[specialize]
   go : (l' : List α) → (i : Nat) → (h : l'.length + i = l.length) → Option (Fin l.length)
   | [], _, _ => none
   | a :: l, i, h =>
@@ -1886,7 +1898,7 @@ Examples:
 * `[2, 4, 5, 6].any (· % 2 = 0) = true`
 * `[2, 4, 5, 6].any (· % 2 = 1) = true`
 -/
-@[suggest_for List.some]
+@[suggest_for List.some, specialize]
 def any : (l : List α) → (p : α → Bool) → Bool
   | [], _ => false
   | h :: t, p => p h || any t p
@@ -1906,7 +1918,7 @@ Examples:
 * `[2, 4, 6].all (· % 2 = 0) = true`
 * `[2, 4, 5, 6].all (· % 2 = 0) = false`
 -/
-@[suggest_for List.every]
+@[suggest_for List.every, specialize]
 def all : List α → (α → Bool) → Bool
   | [], _ => true
   | h :: t, p => p h && all t p
@@ -2007,6 +2019,7 @@ Examples:
 * `[1, 2, 3].zipWithAll Prod.mk [5, 6] = [(some 1, some 5), (some 2, some 6), (some 3, none)]`
 * `[x₁, x₂].zipWithAll f [y] = [f (some x₁) (some y), f (some x₂) none]`
 -/
+@[specialize]
 def zipWithAll (f : Option α → Option β → γ) : List α → List β → List γ
   | [], bs => bs.map fun b => f none (some b)
   | a :: as, [] => (a :: as).map fun a => f (some a) none

src/Init/Data/List/Control.lean

@@ -444,8 +444,8 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as :
     intro b
     cases b <;> simp
 
-@[inline, expose] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
-  let rec @[specialize] loop : (as' : List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
+@[inline, expose] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : @& List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop : (as' : @& List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
     | [], b, _    => pure b
     | a::as', b, h => do
       have : a ∈ as := by

src/Lean/Compiler/InitAttr.lean

@@ -54,7 +54,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
     descr := "initialization procedure for global references"
     -- We want to run `[init]` in declaration order
     preserveOrder := true
-    getParam := fun declName stx => do
+    getParam := fun declName stx => withoutExporting do
       let decl ← getConstInfo declName
       match (← Attribute.Builtin.getIdent? stx) with
       | some initFnName =>
@@ -149,8 +149,6 @@ def setBuiltinInitAttr (env : Environment) (declName : Name) (initFnName : Name
 def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit :=
   -- can always be private, not referenced directly except through emitted C code
   withoutExporting do
-  -- TODO: needs an update-stage0 + prefer_native=true for breaking symbol name
-  withExporting do
     let name ← mkAuxDeclName (kind := `_regBuiltin ++ forDecl)
     let type := mkApp (mkConst `IO) (mkConst `Unit)
     let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque,

src/Lean/Data/PersistentArray.lean

@@ -227,7 +227,7 @@ variable {β : Type v}
 set_option linter.unusedVariables.funArgs false in
 @[specialize]
 partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [inh : Inhabited β]
-    (f : α → β → m (ForInStep β)) (n : PersistentArrayNode α) (b : β) : m (ForInStep β) := do
+    (f : α → β → m (ForInStep β)) (n : @&PersistentArrayNode α) (b : β) : m (ForInStep β) := do
   let mut b := b
   match n with
   | leaf vs =>
@@ -243,7 +243,7 @@ partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
       | ForInStep.yield bNew => b := bNew
     return ForInStep.yield b
 
-@[specialize] protected def forIn (t : PersistentArray α) (init : β) (f : α → β → m (ForInStep β)) : m β := do
+@[specialize] protected def forIn (t : @&PersistentArray α) (init : β) (f : α → β → m (ForInStep β)) : m β := do
   match (← forInAux (inh := ⟨init⟩) f t.root init) with
   | ForInStep.done b  => pure b
   | ForInStep.yield b =>

src/Lean/Data/PersistentHashMap.lean

@@ -153,7 +153,7 @@ partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.s
     else findAtAux keys vals heq (i+1) k
   else none
 
-partial def findAux [BEq α] : Node α β → USize → α → Option β
+partial def findAux [BEq α] : @&Node α β → USize → α → Option β
   | Node.entries entries, h, k =>
     let j     := (mod2Shift h shift).toNat
     match entries[j]! with
@@ -162,7 +162,7 @@ partial def findAux [BEq α] : Node α β → USize → α → Option β
     | Entry.entry k' v => if k == k' then some v else none
   | Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k
 
-def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option β
+def find? {_ : BEq α} {_ : Hashable α} : @&PersistentHashMap α β → α → Option β
   | { root }, k => findAux root (hash k |>.toUSize) k
 
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
@@ -184,7 +184,7 @@ partial def findEntryAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : k
     else findEntryAtAux keys vals heq (i+1) k
   else none
 
-partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α × β)
+partial def findEntryAux [BEq α] : @&Node α β → USize → α → Option (α × β)
   | Node.entries entries, h, k =>
     let j     := (mod2Shift h shift).toNat
     match entries[j]! with
@@ -193,7 +193,7 @@ partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α
     | Entry.entry k' v => if k == k' then some (k', v) else none
   | Node.collision keys vals heq, _, k => findEntryAtAux keys vals heq 0 k
 
-def findEntry? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option (α × β)
+def findEntry? {_ : BEq α} {_ : Hashable α} : @&PersistentHashMap α β → α → Option (α × β)
   | { root }, k => findEntryAux root (hash k |>.toUSize) k
 
 partial def findKeyDAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) (k₀ : α) : α :=
@@ -320,7 +320,7 @@ def foldl {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ
   Id.run <| map.foldlM (pure <| f · · ·) init
 
 protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
-    (map : PersistentHashMap α β) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ := do
+    (map : @&PersistentHashMap α β) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ := do
   let intoError : ForInStep σ → Except σ σ
   | .done s => .error s
   | .yield s => .ok s

src/Lean/Data/Trie.lean

@@ -131,9 +131,9 @@ partial def find? (t : Trie α) (s : String) : Option α :=
   loop 0 t
 
 /-- Returns an `Array` of all values in the trie, in no particular order. -/
-partial def values (t : Trie α) : Array α := go t |>.run #[] |>.2
+partial def values (t : @&Trie α) : Array α := go t |>.run #[] |>.2
   where
-    go : Trie α → StateM (Array α) Unit
+    go : @&Trie α → StateM (Array α) Unit
       | leaf a? => do
         if let some a := a? then
           modify (·.push a)

src/Lean/Elab/App.lean

@@ -13,6 +13,7 @@ public import Lean.IdentifierSuggestion
 import all Lean.Elab.ErrorUtils
 import Lean.Elab.DeprecatedArg
 import Init.Omega
+import Init.Data.List.MapIdx
 
 public section
 
@@ -1299,13 +1300,13 @@ where
 inductive LValResolution where
   /-- When applied to `f`, effectively expands to `BaseStruct.fieldName (self := Struct.toBase f)`.
   This is a special named argument where it suppresses any explicit arguments depending on it so that type parameters don't need to be supplied. -/
-  | projFn   (baseStructName : Name) (structName : Name) (fieldName : Name)
+  | projFn   (baseStructName : Name) (structName : Name) (fieldName : Name) (levels : List Level)
   /-- Similar to `projFn`, but for extracting field indexed by `idx`. Works for one-constructor inductive types in general. -/
   | projIdx  (structName : Name) (idx : Nat)
   /-- When applied to `f`, effectively expands to `constName ... (Struct.toBase f)`, with the argument placed in the correct
   positional argument if possible, or otherwise as a named argument. The `Struct.toBase` is not present if `baseStructName == structName`,
   in which case these do not need to be structures. Supports generalized field notation. -/
-  | const    (baseStructName : Name) (structName : Name) (constName : Name)
+  | const    (baseStructName : Name) (structName : Name) (constName : Name) (levels : List Level)
   /-- Like `const`, but with `fvar` instead of `constName`.
   The `baseName` is the base name of the type to search for in the parameter list. -/
   | localRec (baseName : Name) (fvar : Expr)
@@ -1380,7 +1381,7 @@ private def reverseFieldLookup (env : Environment) (fieldName : String) :=
 
 private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
   match eType.getAppFn, lval with
-  | .const structName _, LVal.fieldIdx ref idx =>
+  | .const structName _, LVal.fieldIdx ref idx levels =>
     if idx == 0 then
       throwError "Invalid projection: Index must be greater than 0"
     let env ← getEnv
@@ -1393,10 +1394,14 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       if idx - 1 < numFields then
         if isStructure env structName then
           let fieldNames := getStructureFields env structName
-          return LValResolution.projFn structName structName fieldNames[idx - 1]!
+          return LValResolution.projFn structName structName fieldNames[idx - 1]! levels
         else
           /- `structName` was declared using `inductive` command.
             So, we don't projection functions for it. Thus, we use `Expr.proj` -/
+          unless levels.isEmpty do
+            throwError "Invalid projection: Explicit universe levels are only supported for inductive types \
+              defined using the `structure` command. \
+              The expression{indentExpr e}\nhas type{inlineExpr eType}which is not a `structure`."
           return LValResolution.projIdx structName (idx - 1)
       else
         if numFields == 0 then
@@ -1409,31 +1414,33 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
           ++ MessageData.note m!"The expression{indentExpr e}\nhas type{inlineExpr eType}which has only \
           {numFields} field{numFields.plural}"
           ++ tupleHint
-  | .const structName _, LVal.fieldName ref fieldName _ _ => withRef ref do
+  | .const structName _, LVal.fieldName ref fieldName levels _ _ => withRef ref do
     let env ← getEnv
     if isStructure env structName then
       if let some baseStructName := findField? env structName (Name.mkSimple fieldName) then
-        return LValResolution.projFn baseStructName structName (Name.mkSimple fieldName)
+        return LValResolution.projFn baseStructName structName (Name.mkSimple fieldName) levels
     -- Search the local context first
     let fullName := Name.mkStr (privateToUserName structName) fieldName
     for localDecl in (← getLCtx) do
       if localDecl.isAuxDecl then
         if let some localDeclFullName := (← getLCtx).auxDeclToFullName.get? localDecl.fvarId then
           if fullName == privateToUserName localDeclFullName then
+            unless levels.isEmpty do
+              throwInvalidExplicitUniversesForLocal localDecl.toExpr
             /- LVal notation is being used to make a "local" recursive call. -/
             return LValResolution.localRec structName localDecl.toExpr
     -- Then search the environment
     if let some (baseStructName, fullName) ← findMethod? structName (.mkSimple fieldName) then
-      return LValResolution.const baseStructName structName fullName
+      return LValResolution.const baseStructName structName fullName levels
     throwInvalidFieldAt ref fieldName fullName
       -- Suggest a potential unreachable private name as hint. This does not cover structure
       -- inheritance, nor `import all`.
       (declHint := (mkPrivateName env structName).mkStr fieldName)
 
-  | .forallE .., LVal.fieldName ref fieldName suffix? fullRef =>
+  | .forallE .., LVal.fieldName ref fieldName levels suffix? fullRef =>
     let fullName := Name.str `Function fieldName
     if (← getEnv).contains fullName then
-      return LValResolution.const `Function `Function fullName
+      return LValResolution.const `Function `Function fullName levels
     match e.getAppFn, suffix? with
     | Expr.const c _, some suffix =>
       throwUnknownNameWithSuggestions (idOrConst := "constant")  (ref? := fullRef) (c ++ suffix)
@@ -1443,7 +1450,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     throwError "Invalid projection: Projections cannot be used on functions, and{indentExpr e}\n\
       has function type{inlineExprTrailing eType}"
 
-  | .mvar .., .fieldName _ fieldName _ _ =>
+  | .mvar .., .fieldName _ fieldName levels _ _ =>
     let hint := match reverseFieldLookup (← getEnv) fieldName with
       | #[] => MessageData.nil
       | #[opt] => .hint' m!"Consider replacing the field projection `.{fieldName}` with a call to the function `{.ofConstName opt}`."
@@ -1451,13 +1458,13 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
           {MessageData.joinSep (opts.toList.map (indentD m!"• `{.ofConstName ·}`")) .nil}"
     throwNamedError lean.invalidField (m!"Invalid field notation: Type of{indentExpr e}\nis not \
       known; cannot resolve field `{fieldName}`" ++ hint)
-  | .mvar .., .fieldIdx _ i  =>
+  | .mvar .., .fieldIdx _ i _ =>
     throwError m!"Invalid projection: Type of{indentExpr e}\nis not known; cannot resolve \
       projection `{i}`"
 
   | _, _ =>
     match e.getAppFn, lval with
-    | Expr.const c _, .fieldName _ref _fieldName (some suffix) fullRef =>
+    | Expr.const c _, .fieldName _ref _fieldName _levels (some suffix) fullRef =>
       throwUnknownNameWithSuggestions (idOrConst := "constant") (ref? := fullRef) (c ++ suffix)
     | _, .fieldName .. =>
       throwNamedError lean.invalidField m!"Invalid field notation: Field projection operates on \
@@ -1706,12 +1713,12 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       let f ← mkProjAndCheck structName idx f
       let f ← addTermInfo lval.getRef f
       loop f lvals
-    | LValResolution.projFn baseStructName structName fieldName =>
+    | LValResolution.projFn baseStructName structName fieldName levels =>
       let f ← mkBaseProjections baseStructName structName f
       let some info := getFieldInfo? (← getEnv) baseStructName fieldName | unreachable!
       if (← isInaccessiblePrivateName info.projFn) then
         throwError "Field `{fieldName}` from structure `{structName}` is private"
-      let projFn ← withRef lval.getRef <| mkConst info.projFn
+      let projFn ← withRef lval.getRef <| mkConst info.projFn levels
       let projFn ← addProjTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true }
@@ -1719,9 +1726,9 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       else
         let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
         loop f lvals
-    | LValResolution.const baseStructName structName constName =>
+    | LValResolution.const baseStructName structName constName levels =>
       let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
-      let projFn ← withRef lval.getRef <| mkConst constName
+      let projFn ← withRef lval.getRef <| mkConst constName levels
       let projFn ← addProjTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let (args, namedArgs) ← addLValArg baseStructName f args namedArgs projFn explicit
@@ -1772,15 +1779,19 @@ false, no elaboration function executed by `x` will reset it to
 /--
 Elaborates the resolutions of a function. The `fns` array is the output of `resolveName'`.
 -/
-private def elabAppFnResolutions (fRef : Syntax) (fns : List (Expr × Syntax × List Syntax)) (lvals : List LVal)
+private def elabAppFnResolutions (fRef : Syntax) (fns : List (Expr × Syntax × List Syntax × List Level)) (lvals : List LVal)
     (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool)
     (acc : Array (TermElabResult Expr)) (forceTermInfo : Bool := false) :
     TermElabM (Array (TermElabResult Expr)) := do
   let overloaded := overloaded || fns.length > 1
   -- Set `errToSorry` to `false` if `fns` > 1. See comment above about the interaction between `errToSorry` and `observing`.
   withReader (fun ctx => { ctx with errToSorry := fns.length == 1 && ctx.errToSorry }) do
-    fns.foldlM (init := acc) fun acc (f, fIdent, fields) => do
-      let lvals' := toLVals fields (first := true)
+    fns.foldlM (init := acc) fun acc (f, fIdent, fields, projLevels) => do
+      let lastIdx := fields.length - 1
+      let lvals' := fields.mapIdx fun idx field =>
+        let suffix? := if idx == 0       then some <| toName fields else none
+        let levels  := if idx == lastIdx then projLevels            else []
+        LVal.fieldName field field.getId.getString! levels suffix? fRef
       let s ← observing do
         checkDeprecated fIdent f
         let f ← addTermInfo fIdent f expectedType? (force := forceTermInfo)
@@ -1794,11 +1805,6 @@ where
       | field :: fields => .mkStr (go fields) field.getId.toString
     go fields.reverse
 
-  toLVals : List Syntax → (first : Bool) → List LVal
-    | [],            _     => []
-    | field::fields, true  => .fieldName field field.getId.getString! (toName (field::fields)) fRef :: toLVals fields false
-    | field::fields, false => .fieldName field field.getId.getString! none fRef :: toLVals fields false
-
 private def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level) (lvals : List LVal)
     (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool)
     (acc : Array (TermElabResult Expr)) :
@@ -1832,7 +1838,7 @@ To infer a namespace from the expected type, we do the following operations:
 - if the type is of the form `c x₁ ... xₙ` with `c` a constant, then try using `c` as the namespace,
   and if that doesn't work, try unfolding the expression and continuing.
 -/
-private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do
+private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax × List Level)) := do
   unless id.isAtomic do
     throwError "Invalid dotted identifier notation: The name `{id}` must be atomic"
   tryPostponeIfNoneOrMVar expectedType?
@@ -1844,7 +1850,7 @@ private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitU
   withForallBody expectedType fun resultType => do
     go resultType expectedType #[]
 where
-  throwNoExpectedType := do
+  throwNoExpectedType {α} : TermElabM α := do
     let hint ← match reverseFieldLookup (← getEnv) (id.getString!) with
       | #[] => pure MessageData.nil
       | suggestions =>
@@ -1863,7 +1869,7 @@ where
         withForallBody body k
     else
       k type
-  go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM (List (Expr × Syntax × List Syntax)) := do
+  go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM (List (Expr × Syntax × List Syntax × List Level)) := do
     let resultType ← instantiateMVars resultType
     let resultTypeFn := resultType.getAppFn
     try
@@ -1880,11 +1886,11 @@ where
           |>.filter (fun (_, fieldList) => fieldList.isEmpty)
           |>.map Prod.fst
         if !candidates.isEmpty then
-          candidates.mapM fun resolvedName => return (← mkConst resolvedName explicitUnivs, ← getRef, [])
+          candidates.mapM fun resolvedName => return (← mkConst resolvedName explicitUnivs, ← getRef, [], [])
         else if let some (fvar, []) ← resolveLocalName fullName then
           unless explicitUnivs.isEmpty do
             throwInvalidExplicitUniversesForLocal fvar
-          return [(fvar, ← getRef, [])]
+          return [(fvar, ← getRef, [], [])]
         else
           throwUnknownIdentifierAt (← getRef) (declHint := fullName) <| m!"Unknown constant `{.ofConstName fullName}`"
             ++ .note m!"Inferred this name from the expected resulting type of `.{id}`:{indentExpr expectedType}"
@@ -1914,26 +1920,37 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     withReader (fun ctx => { ctx with errToSorry := false }) do
       f.getArgs.foldlM (init := acc) fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc
   else
-    let elabFieldName (e field : Syntax) (explicit : Bool) := do
-      let newLVals := field.identComponents.map fun comp =>
-        -- We use `none` in `suffix?` since `field` can't be part of a composite name
-        LVal.fieldName comp comp.getId.getString! none f
+    let elabFieldName (e field : Syntax) (explicitUnivs : List Level) := do
+      let comps := field.identComponents
+      let lastIdx := comps.length - 1
+      let newLVals := comps.mapIdx fun idx comp =>
+        let levels := if idx = lastIdx then explicitUnivs else []
+        let suffix? := none -- We use `none` since the field can't be part of a composite name
+        LVal.fieldName comp comp.getId.getString! levels suffix? f
       elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    let elabFieldIdx (e idxStx : Syntax) (explicit : Bool) := do
+    let elabFieldIdx (e idxStx : Syntax) (explicitUnivs : List Level) := do
       let some idx := idxStx.isFieldIdx?
         | throwError "Internal error: Unexpected field index syntax `{idxStx}`"
-      elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) (explicit : Bool) : TermElabM (Array (TermElabResult Expr)) := do
+      elabAppFn e (LVal.fieldIdx idxStx idx explicitUnivs :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
+    let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) : TermElabM (Array (TermElabResult Expr)) := do
       let res ← withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes explicitUnivs expectedType?
       -- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns
       elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true)
     match f with
-    | `($(e).$idx:fieldIdx) => elabFieldIdx e idx explicit
-    | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx explicit
-    | `($(e).$field:ident) => elabFieldName e field explicit
-    | `($e |>.$field:ident) => elabFieldName e field explicit
-    | `(@$(e).$idx:fieldIdx) => elabFieldIdx e idx (explicit := true)
-    | `(@$(e).$field:ident) => elabFieldName e field (explicit := true)
+    | `($(e).$idx:fieldIdx)
+    | `($e |>.$idx:fieldIdx) =>
+      elabFieldIdx e idx []
+    | `($(e).$idx:fieldIdx.{$us,*})
+    | `($e |>.$idx:fieldIdx.{$us,*}) =>
+      let us ← elabExplicitUnivs us
+      elabFieldIdx e idx us
+    | `($(e).$field:ident)
+    | `($e |>.$field:ident) =>
+      elabFieldName e field []
+    | `($(e).$field:ident.{$us,*})
+    | `($e |>.$field:ident.{$us,*}) =>
+      let us ← elabExplicitUnivs us
+      elabFieldName e field us
     | `($_:ident@$_:term) =>
       throwError m!"Expected a function, but found the named pattern{indentD f}"
         ++ .note m!"Named patterns `<identifier>@<term>` can only be used when pattern-matching"
@@ -1942,12 +1959,15 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `($id:ident.{$us,*}) => do
       let us ← elabExplicitUnivs us
       elabAppFnId id us lvals namedArgs args expectedType? explicit ellipsis overloaded acc
-    | `(.$id:ident) => elabDottedIdent id [] explicit
+    | `(.$id:ident) => elabDottedIdent id []
     | `(.$id:ident.{$us,*}) =>
       let us ← elabExplicitUnivs us
-      elabDottedIdent id us explicit
+      elabDottedIdent id us
     | `(@$_:ident)
     | `(@$_:ident.{$_us,*})
+    | `(@$(_).$_:fieldIdx)
+    | `(@$(_).$_:ident)
+    | `(@$(_).$_:ident.{$_us,*})
     | `(@.$_:ident)
     | `(@.$_:ident.{$_us,*}) =>
       elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
@@ -2084,10 +2104,10 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 @[builtin_term_elab dotIdent] def elabDotIdent : TermElab := elabAtom
 @[builtin_term_elab explicitUniv] def elabExplicitUniv : TermElab := elabAtom
 @[builtin_term_elab pipeProj] def elabPipeProj : TermElab
-  | `($e |>.%$tk$f $args*), expectedType? =>
+  | `($e |>.%$tk$f$[.{$us?,*}]? $args*), expectedType? =>
     universeConstraintsCheckpoint do
       let (namedArgs, args, ellipsis) ← expandArgs args
-      let mut stx ← `($e |>.%$tk$f)
+      let mut stx ← `($e |>.%$tk$f$[.{$us?,*}]?)
       if let (some startPos, some stopPos) := (e.raw.getPos?, f.raw.getTailPos?) then
         stx := ⟨stx.raw.setInfo <| .synthetic (canonical := true) startPos stopPos⟩
       elabAppAux stx namedArgs args (ellipsis := ellipsis) expectedType?
@@ -2095,15 +2115,16 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 
 @[builtin_term_elab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
   match stx with
-  | `(@$_:ident)           => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
-  | `(@$_:ident.{$_us,*})  => elabAtom stx expectedType?
-  | `(@$(_).$_:fieldIdx)   => elabAtom stx expectedType?
-  | `(@$(_).$_:ident)      => elabAtom stx expectedType?
-  | `(@.$_:ident)          => elabAtom stx expectedType?
-  | `(@.$_:ident.{$_us,*}) => elabAtom stx expectedType?
-  | `(@($t))               => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
-  | `(@$t)                 => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
-  | _                      => throwUnsupportedSyntax
+  | `(@$_:ident)               => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
+  | `(@$_:ident.{$_us,*})      => elabAtom stx expectedType?
+  | `(@$(_).$_:fieldIdx)       => elabAtom stx expectedType?
+  | `(@$(_).$_:ident)          => elabAtom stx expectedType?
+  | `(@$(_).$_:ident.{$_us,*}) => elabAtom stx expectedType?
+  | `(@.$_:ident)              => elabAtom stx expectedType?
+  | `(@.$_:ident.{$_us,*})     => elabAtom stx expectedType?
+  | `(@($t))                   => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | `(@$t)                     => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | _                          => throwUnsupportedSyntax
 
 @[builtin_term_elab choice] def elabChoice : TermElab := elabAtom
 @[builtin_term_elab proj] def elabProj : TermElab := elabAtom

src/Lean/Elab/DeclModifiers.lean

@@ -65,9 +65,28 @@ def Visibility.isPublic : Visibility → Bool
   | .public    => true
   | _          => false
 
+/--
+Returns whether the given visibility modifier should be interpreted as `public` in the current
+environment.
+
+NOTE: `Environment.isExporting` defaults to `false` when command elaborators are invoked for
+backward compatibility. It needs to be initialized apropriately first before calling this function
+as e.g. done in `elabDeclaration`.
+-/
 def Visibility.isInferredPublic (env : Environment) (v : Visibility) : Bool :=
   if env.isExporting || !env.header.isModule then !v.isPrivate else v.isPublic
 
+/-- Converts optional visibility syntax to a `Visibility` value. -/
+def elabVisibility [Monad m] [MonadError m] (vis? : Option (TSyntax ``Parser.Command.visibility)) :
+    m Visibility :=
+  match vis? with
+  | none   => pure .regular
+  | some v =>
+    match v with
+    | `(Parser.Command.visibility| private) => pure .private
+    | `(Parser.Command.visibility| public) => pure .public
+    | _ => throwErrorAt v "unexpected visibility modifier"
+
 /-- Whether a declaration is default, partial or nonrec. -/
 inductive RecKind where
   | «partial» | «nonrec» | default
@@ -183,13 +202,7 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
     else
       RecKind.nonrec
   let docString? := docCommentStx.getOptional?.map (TSyntax.mk ·, doc.verso.get (← getOptions))
-  let visibility ← match visibilityStx.getOptional? with
-    | none   => pure .regular
-    | some v =>
-      match v with
-      | `(Parser.Command.visibility| private) => pure .private
-      | `(Parser.Command.visibility| public) => pure .public
-      | _ => throwErrorAt v "unexpected visibility modifier"
+  let visibility ← elabVisibility (visibilityStx.getOptional?.map (⟨·⟩))
   let isProtected := !protectedStx.isNone
   let attrs ← match attrsStx.getOptional? with
     | none       => pure #[]

src/Lean/Elab/Declaration.lean

@@ -340,31 +340,29 @@ def elabMutual : CommandElab := fun stx => do
 
 @[builtin_command_elab Lean.Parser.Command.«initialize»] def elabInitialize : CommandElab
   | stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ←]? $doSeq) => do
+    withExporting (isExporting := (← getScope).isPublic) do
     let attrId := mkIdentFrom stx <| if kw.raw[0].isToken "initialize" then `init else `builtin_init
     if let (some id, some type) := (id?, type?) then
       let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(vis?)? $[meta%$meta?]? $[unsafe%$unsafe?]?) := stx[0]
         | throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
       let defStx ← `($[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ∅),*] $(vis?)? $[meta%$meta?]? opaque $id : $type)
       let mut fullId := (← getCurrNamespace) ++ id.getId
-      if vis?.any (·.raw.isOfKind ``Parser.Command.private) then
+      let visibility ← elabVisibility vis?
+      if !visibility.isInferredPublic (← getEnv) then
         fullId := mkPrivateName (← getEnv) fullId
       -- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as
       -- otherwise the info context created by `with_decl_name` will be incomplete and break the
       -- call hierarchy
       addDeclarationRangesForBuiltin fullId ⟨defStx.raw[0]⟩ defStx.raw[1]
-      let vis := Parser.Command.visibility.ofBool (!isPrivateName fullId)
       elabCommand (← `(
-        $vis:visibility $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
+        @[no_expose] private $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
         $defStx:command))
     else
       let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(_)? $[meta%$meta?]? $[unsafe%$unsafe?]?) := declModifiers
         | throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
       let attrs := (attrs?.map (·.getElems)).getD #[]
       let attrs := attrs.push (← `(Lean.Parser.Term.attrInstance| $attrId:ident))
-      -- `[builtin_init]` can be private as it is used for local codegen only but `[init]` must be
-      -- available for the interpreter.
-      let vis := Parser.Command.visibility.ofBool (attrId.getId == `init)
-      elabCommand (← `($[$doc?:docComment]? @[$[$attrs],*] $vis:visibility $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO Unit := do $doSeq))
+      elabCommand (← `($[$doc?:docComment]? @[no_expose, $[$attrs],*] private $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO Unit := do $doSeq))
   | _ => throwUnsupportedSyntax
 
 builtin_initialize

src/Lean/Elab/Deriving/Inhabited.lean

@@ -25,25 +25,23 @@ private def mkInhabitedInstanceUsing (inductiveTypeName : Name) (ctorName : Name
   | none =>
     return false
 where
-  addLocalInstancesForParamsAux {α} (k : LocalInst2Index → TermElabM α) : List Expr → Nat → LocalInst2Index → TermElabM α
-    | [], _, map    => k map
-    | x::xs, i, map =>
+  addLocalInstancesForParamsAux {α} (k : Array Expr → LocalInst2Index → TermElabM α) : List Expr → Nat → Array Expr → LocalInst2Index → TermElabM α
+    | [],    _, insts, map => k insts map
+    | x::xs, i, insts, map =>
       try
         let instType ← mkAppM `Inhabited #[x]
-        if (← isTypeCorrect instType) then
-          withLocalDeclD (← mkFreshUserName `inst) instType fun inst => do
-            trace[Elab.Deriving.inhabited] "adding local instance {instType}"
-            addLocalInstancesForParamsAux k xs (i+1) (map.insert inst.fvarId! i)
-        else
-          addLocalInstancesForParamsAux k xs (i+1) map
+        check instType
+        withLocalDecl (← mkFreshUserName `inst) .instImplicit instType fun inst => do
+          trace[Elab.Deriving.inhabited] "adding local instance {instType}"
+          addLocalInstancesForParamsAux k xs (i+1) (insts.push inst) (map.insert inst.fvarId! i)
       catch _ =>
-        addLocalInstancesForParamsAux k xs (i+1) map
+        addLocalInstancesForParamsAux k xs (i+1) insts map
 
-  addLocalInstancesForParams {α} (xs : Array Expr) (k : LocalInst2Index → TermElabM α) : TermElabM α := do
+  addLocalInstancesForParams {α} (xs : Array Expr) (k : Array Expr → LocalInst2Index → TermElabM α) : TermElabM α := do
     if addHypotheses then
-      addLocalInstancesForParamsAux k xs.toList 0 {}
+      addLocalInstancesForParamsAux k xs.toList 0 #[] {}
     else
-      k {}
+      k #[] {}
 
   collectUsedLocalsInsts (usedInstIdxs : IndexSet) (localInst2Index : LocalInst2Index) (e : Expr) : IndexSet :=
     if localInst2Index.isEmpty then
@@ -58,58 +56,88 @@ where
       runST (fun _ => visit |>.run usedInstIdxs) |>.2
 
   /-- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters
-     at position `i` and `i ∈ assumingParamIdxs`. -/
-  mkInstanceCmdWith (assumingParamIdxs : IndexSet) : TermElabM Syntax := do
-    let ctx ← Deriving.mkContext ``Inhabited "inhabited" inductiveTypeName
+     at position `i` and `i ∈ usedInstIdxs`. -/
+  mkInstanceCmdWith (instId : Ident) (usedInstIdxs : IndexSet) (auxFunId : Ident) : TermElabM Syntax := do
     let indVal ← getConstInfoInduct inductiveTypeName
-    let ctorVal ← getConstInfoCtor ctorName
     let mut indArgs := #[]
     let mut binders := #[]
     for i in *...indVal.numParams + indVal.numIndices do
       let arg := mkIdent (← mkFreshUserName `a)
       indArgs := indArgs.push arg
-      let binder ← `(bracketedBinderF| { $arg:ident })
-      binders := binders.push binder
-      if assumingParamIdxs.contains i then
-        let binder ← `(bracketedBinderF| [Inhabited $arg:ident ])
-        binders := binders.push binder
+      binders := binders.push <| ← `(bracketedBinderF| { $arg:ident })
+      if usedInstIdxs.contains i then
+        binders := binders.push <| ← `(bracketedBinderF| [Inhabited $arg:ident ])
     let type ← `(@$(mkCIdent inductiveTypeName):ident $indArgs:ident*)
-    let mut ctorArgs := #[]
-    for _ in *...ctorVal.numParams do
-      ctorArgs := ctorArgs.push (← `(_))
-    for _ in *...ctorVal.numFields do
-      ctorArgs := ctorArgs.push (← ``(Inhabited.default))
-    let val ← `(@$(mkIdent ctorName):ident $ctorArgs*)
-    let ctx ← mkContext ``Inhabited "default" inductiveTypeName
-    let auxFunName := ctx.auxFunNames[0]!
-    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type := $val
-      instance $(mkIdent ctx.instName):ident $binders:bracketedBinder* : Inhabited $type := ⟨$(mkIdent auxFunName)⟩)
+    `(instance $instId:ident $binders:bracketedBinder* : Inhabited $type := ⟨$auxFunId⟩)
 
+  solveMVarsWithDefault (e : Expr) : TermElabM Unit := do
+    let mvarIds ← getMVarsNoDelayed e
+    mvarIds.forM fun mvarId => mvarId.withContext do
+      unless ← mvarId.isAssigned do
+        let type ← mvarId.getType
+        withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"synthesizing Inhabited instance for{inlineExprTrailing type}") do
+          let val ← mkDefault type
+          mvarId.assign val
+          trace[Elab.Deriving.inhabited] "value:{inlineExprTrailing val}"
 
-  mkInstanceCmd? : TermElabM (Option Syntax) := do
-    let ctorVal ← getConstInfoCtor ctorName
-    forallTelescopeReducing ctorVal.type fun xs _ =>
-      addLocalInstancesForParams xs[*...ctorVal.numParams] fun localInst2Index => do
-        let mut usedInstIdxs := {}
-        let mut ok := true
-        for h : i in ctorVal.numParams...xs.size do
-          let x := xs[i]
-          let instType ← mkAppM `Inhabited #[(← inferType x)]
-          trace[Elab.Deriving.inhabited] "checking {instType} for `{ctorName}`"
-          match (← trySynthInstance instType) with
-          | LOption.some e =>
-            usedInstIdxs := collectUsedLocalsInsts usedInstIdxs localInst2Index e
-          | _ =>
-            trace[Elab.Deriving.inhabited] "failed to generate instance using `{ctorName}` {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}"
-            ok := false
-            break
-        if !ok then
-          return none
+  mkDefaultValue (indVal : InductiveVal) : TermElabM (Expr × Expr × IndexSet) := do
+    let us := indVal.levelParams.map Level.param
+    forallTelescopeReducing indVal.type fun xs _ =>
+    withImplicitBinderInfos xs do
+    addLocalInstancesForParams xs[0...indVal.numParams] fun insts localInst2Index => do
+      let type := mkAppN (.const inductiveTypeName us) xs
+      let val ←
+        if isStructure (← getEnv) inductiveTypeName then
+          withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using structure instance elaborator") do
+            let stx ← `(structInst| {..})
+            withoutErrToSorry <| elabTermAndSynthesize stx type
         else
-          trace[Elab.Deriving.inhabited] "inhabited instance using `{ctorName}` {if addHypotheses then "(assuming parameters are inhabited)" else ""} {usedInstIdxs.toList}"
-          let cmd ← mkInstanceCmdWith usedInstIdxs
-          trace[Elab.Deriving.inhabited] "\n{cmd}"
-          return some cmd
+          withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using constructor `{.ofConstName ctorName}`") do
+            let val := mkAppN (.const ctorName us) xs[0...indVal.numParams]
+            let (mvars, _, type') ← forallMetaTelescopeReducing (← inferType val)
+            unless ← isDefEq type type' do
+              throwError "cannot unify{indentExpr type}\nand type of constructor{indentExpr type'}"
+            pure <| mkAppN val mvars
+      solveMVarsWithDefault val
+      let val ← instantiateMVars val
+      if val.hasMVar then
+        throwError "default value contains metavariables{inlineExprTrailing val}"
+      let fvars := Lean.collectFVars {} val
+      let insts' := insts.filter fvars.visitedExpr.contains
+      let usedInstIdxs := collectUsedLocalsInsts {} localInst2Index val
+      assert! insts'.size == usedInstIdxs.size
+      trace[Elab.Deriving.inhabited] "inhabited instance using{inlineExpr val}{if insts'.isEmpty then m!"" else m!"(assuming parameters {insts'} are inhabited)"}"
+      let xs' := xs ++ insts'
+      let auxType ← mkForallFVars xs' type
+      let auxVal ← mkLambdaFVars xs' val
+      return (auxType, auxVal, usedInstIdxs)
+
+  mkInstanceCmd? : TermElabM (Option Syntax) :=
+    withExporting (isExporting := !isPrivateName ctorName) do
+      let ctx ← mkContext ``Inhabited "default" inductiveTypeName
+      let auxFunName := (← getCurrNamespace) ++ ctx.auxFunNames[0]!
+      let indVal ← getConstInfoInduct inductiveTypeName
+      let (auxType, auxVal, usedInstIdxs) ←
+        try
+          withDeclName auxFunName do mkDefaultValue indVal
+        catch e =>
+          trace[Elab.Deriving.inhabited] "error: {e.toMessageData}"
+          return none
+      addDecl <| .defnDecl <| ← mkDefinitionValInferringUnsafe
+        (name        := auxFunName)
+        (levelParams := indVal.levelParams)
+        (type        := auxType)
+        (value       := auxVal)
+        (hints       := ReducibilityHints.regular (getMaxHeight (← getEnv) auxVal + 1))
+      if isMarkedMeta (← getEnv) inductiveTypeName then
+        modifyEnv (markMeta · auxFunName)
+      unless (← read).isNoncomputableSection do
+        compileDecls #[auxFunName]
+      enableRealizationsForConst auxFunName
+      trace[Elab.Deriving.inhabited] "defined {.ofConstName auxFunName}"
+      let cmd ← mkInstanceCmdWith (mkIdent ctx.instName) usedInstIdxs (mkCIdent auxFunName)
+      trace[Elab.Deriving.inhabited] "\n{cmd}"
+      return some cmd
 
 private def mkInhabitedInstance (declName : Name) : CommandElabM Unit := do
   withoutExposeFromCtors declName do

src/Lean/Elab/Import.lean

@@ -10,6 +10,7 @@ public import Lean.Parser.Module
 meta import Lean.Parser.Module
 import Lean.Compiler.ModPkgExt
 public import Lean.DeprecatedModule
+import Init.Data.String.Modify
 
 public section
 
@@ -97,6 +98,43 @@ def checkDeprecatedImports
       | none => messages
     | none => messages
 
+private def osForbiddenChars : Array Char :=
+  #['<', '>', '"', '|', '?', '*', '!']
+
+private def osForbiddenNames : Array String :=
+  #["CON", "PRN", "AUX", "NUL",
+    "COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9",
+    "COM¹", "COM²", "COM³",
+    "LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9",
+    "LPT¹", "LPT²", "LPT³"]
+
+private def checkComponentPortability (comp : String) : Option String :=
+  if osForbiddenNames.contains comp.toUpper then
+    some s!"'{comp}' is a reserved file name on some operating systems"
+  else if let some c := osForbiddenChars.find? (comp.contains ·) then
+    some s!"contains character '{c}' which is forbidden on some operating systems"
+  else
+    none
+
+def checkModuleNamePortability
+    (mainModule : Name) (inputCtx : Parser.InputContext) (startPos : String.Pos.Raw)
+    (messages : MessageLog) : MessageLog :=
+  go mainModule messages
+where
+  go : Name → MessageLog → MessageLog
+    | .anonymous, messages => messages
+    | .str parent s, messages =>
+      let messages := match checkComponentPortability s with
+        | some reason => messages.add {
+            fileName := inputCtx.fileName
+            pos := inputCtx.fileMap.toPosition startPos
+            severity := .error
+            data := s!"module name '{mainModule}' is not portable: {reason}"
+          }
+        | none => messages
+      go parent messages
+    | .num parent _, messages => go parent messages
+
 def processHeaderCore
     (startPos : String.Pos.Raw) (imports : Array Import) (isModule : Bool)
     (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext)
@@ -124,6 +162,7 @@ def processHeaderCore
     pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
   let env := env.setMainModule mainModule |>.setModulePackage package?
   let messages := checkDeprecatedImports env imports opts inputCtx startPos messages headerStx? origHeaderStx?
+  let messages := checkModuleNamePortability mainModule inputCtx startPos messages
   return (env, messages)
 
 /--

src/Lean/Elab/Quotation/Precheck.lean

@@ -113,7 +113,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
     if (← read).quotLCtx.contains val then
       return
     let rs ← try resolveName stx val [] [] catch _ => pure []
-    for (e, _) in rs do
+    for (e, _, _) in rs do
       match e with
       | Expr.fvar _      .. =>
         if quotPrecheck.allowSectionVars.get (← getOptions) && (← isSectionVariable e) then

src/Lean/Elab/Term/TermElabM.lean

@@ -232,7 +232,10 @@ structure TacticFinishedSnapshot extends Language.Snapshot where
   state? : Option SavedState
   /-- Untyped snapshots from `logSnapshotTask`, saved at this level for cancellation. -/
   moreSnaps : Array (SnapshotTask SnapshotTree)
-deriving Inhabited
+
+instance : Inhabited TacticFinishedSnapshot where
+  default := { toSnapshot := default, state? := default, moreSnaps := default }
+
 instance : ToSnapshotTree TacticFinishedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, s.moreSnaps⟩
 
@@ -246,7 +249,10 @@ structure TacticParsedSnapshot extends Language.Snapshot where
   finished : SnapshotTask TacticFinishedSnapshot
   /-- Tasks for subsequent, potentially parallel, tactic steps. -/
   next     : Array (SnapshotTask TacticParsedSnapshot) := #[]
-deriving Inhabited
+
+instance : Inhabited TacticParsedSnapshot where
+  default := { toSnapshot := default, stx := default, finished := default }
+
 partial instance : ToSnapshotTree TacticParsedSnapshot where
   toSnapshotTree := go where
     go := fun s => ⟨s.toSnapshot,
@@ -627,13 +633,13 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl
   `[LVal.fieldName "foo", LVal.fieldIdx 1]`.
 -/
 inductive LVal where
-  | fieldIdx  (ref : Syntax) (i : Nat)
+  | fieldIdx  (ref : Syntax) (i : Nat) (levels : List Level)
   /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierarchical/composite name.
   `ref` is the syntax object representing the field. `fullRef` includes the LHS. -/
-  | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (fullRef : Syntax)
+  | fieldName (ref : Syntax) (name : String) (levels : List Level) (suffix? : Option Name) (fullRef : Syntax)
 
 def LVal.getRef : LVal → Syntax
-  | .fieldIdx ref _    => ref
+  | .fieldIdx ref ..   => ref
   | .fieldName ref ..  => ref
 
 def LVal.isFieldName : LVal → Bool
@@ -642,8 +648,11 @@ def LVal.isFieldName : LVal → Bool
 
 instance : ToString LVal where
   toString
-    | .fieldIdx _ i     => toString i
-    | .fieldName _ n .. => n
+    | .fieldIdx _ i levels ..  => toString i ++ levelsToString levels
+    | .fieldName _ n levels .. => n ++ levelsToString levels
+where
+  levelsToString levels :=
+    if levels.isEmpty then "" else ".{" ++ String.intercalate "," (levels.map toString) ++ "}"
 
 /-- Return the name of the declaration being elaborated if available. -/
 def getDeclName? : TermElabM (Option Name) := return (← read).declName?
@@ -2111,8 +2120,10 @@ def checkDeprecated (ref : Syntax) (e : Expr) : TermElabM Unit := do
 @[inline] def withoutCheckDeprecated [MonadWithReaderOf Context m] : m α → m α :=
   withTheReader Context (fun ctx => { ctx with checkDeprecated := false })
 
-private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
+private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String × List Level)) := do
   candidates.foldlM (init := []) fun result (declName, projs) => do
+    -- levels apply to the last projection, not the constant
+    let (constLevels, projLevels) := if projs.isEmpty then (explicitLevels, []) else ([], explicitLevels)
     -- TODO: better support for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail.
     /-
     We disable `checkDeprecated` here because there may be many overloaded symbols.
@@ -2121,25 +2132,38 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
     At `elabAppFnId`, we perform the check when converting the list returned by `resolveName'` into a list of
     `TermElabResult`s.
     -/
-    let const ← withoutCheckDeprecated <| mkConst declName explicitLevels
-    return (const, projs) :: result
+    let const ← withoutCheckDeprecated <| mkConst declName constLevels
+    return (const, projs, projLevels) :: result
 
 def throwInvalidExplicitUniversesForLocal {α} (e : Expr) : TermElabM α :=
   throwError "invalid use of explicit universe parameters, `{e}` is a local variable"
 
-def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
+/--
+  Gives all resolutions of the name `n`.
+
+- `explicitLevels` provides a prefix of level parameters to the constant. For resolutions with a projection
+  component, the levels are not used, since they must apply to the last projection, not the constant.
+  In that case, the third component of the tuple is `explicitLevels`.
+-/
+def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String × List Level)) := do
   addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
+  let processLocal (e : Expr) (projs : List String) := do
+    if projs.isEmpty then
+      if explicitLevels.isEmpty then
+        return [(e, [], [])]
+      else
+        throwInvalidExplicitUniversesForLocal e
+    else
+      return [(e, projs, explicitLevels)]
   if let some (e, projs) ← resolveLocalName n then
-    unless explicitLevels.isEmpty do
-      throwInvalidExplicitUniversesForLocal e
-    return [(e, projs)]
+    return ← processLocal e projs
   let preresolved := preresolved.filterMap fun
     | .decl n projs => some (n, projs)
     | _             => none
   -- check for section variable capture by a quotation
   let ctx ← read
   if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
-    return [(e, projs)]  -- section variables should shadow global decls
+    return ← processLocal e projs  -- section variables should shadow global decls
   if preresolved.isEmpty then
     mkConsts (← realizeGlobalName n) explicitLevels
   else
@@ -2148,14 +2172,17 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved
 /--
   Similar to `resolveName`, but creates identifiers for the main part and each projection with position information derived from `ident`.
   Example: Assume resolveName `v.head.bla.boo` produces `(v.head, ["bla", "boo"])`, then this method produces
-  `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. -/
-def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (Name × List (Expr × Syntax × List Syntax)) := do
+  `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`.
+
+  See the comment there about `explicitLevels` and the meaning of the `List Level` component of the returned tuple.
+-/
+def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (Name × List (Expr × Syntax × List Syntax × List Level)) := do
   let .ident _ _ n preresolved := ident
     | throwError "identifier expected"
   let r ← resolveName ident n preresolved explicitLevels expectedType?
-  let rc ← r.mapM fun (c, fields) => do
+  let rc ← r.mapM fun (c, fields, levels) => do
     let ids := ident.identComponents (nFields? := fields.length)
-    return (c, ids.head!, ids.tail!)
+    return (c, ids.head!, ids.tail!, levels)
   return (n, rc)
 
 
@@ -2163,7 +2190,7 @@ def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (
   match stx with
   | .ident _ _ val preresolved =>
     let rs ← try resolveName stx val preresolved [] catch _ => pure []
-    let rs := rs.filter fun ⟨_, projs⟩ => projs.isEmpty
+    let rs := rs.filter fun ⟨_, projs, _⟩ => projs.isEmpty
     let fs := rs.map fun (f, _) => f
     match fs with
     | []  => return none

src/Lean/Environment.lean

@@ -616,7 +616,13 @@ structure Environment where
   /--
   Indicates whether the environment is being used in an exported context, i.e. whether it should
   provide access to only the data to be imported by other modules participating in the module
-  system.
+  system. Apart from controlling access, some operations such as `mkAuxDeclName` may also change
+  their output based on this flag.
+
+  By default, `isExporting` is set to false when command elaborators are invoked such that they have
+  access to the full local environment. Use `with(out)Exporting` to modify based on context. For
+  example, `elabDeclaration` sets it based on `(← getScope).isPublic` on the top level, then
+  `elabMutualDef` may switch from public to private when e.g. entering the proof of a theorem.
   -/
   isExporting : Bool := false
 deriving Nonempty

src/Lean/Language/Basic.lean

@@ -67,7 +67,9 @@ structure Snapshot where
   `diagnostics`) occurred that prevents processing of the remainder of the file.
   -/
   isFatal := false
-deriving Inhabited
+
+instance : Inhabited Snapshot where
+  default := { desc := "", diagnostics := default }
 
 /-- Range that is marked as being processed by the server while a task is running. -/
 inductive SnapshotTask.ReportingRange where
@@ -236,7 +238,10 @@ partial def SnapshotTask.cancelRec [ToSnapshotTree α] (t : SnapshotTask α) : B
 
 /-- Snapshot type without child nodes. -/
 structure SnapshotLeaf extends Snapshot
-deriving Inhabited, TypeName
+deriving TypeName
+
+instance : Inhabited SnapshotLeaf where
+  default := { toSnapshot := default }
 
 instance : ToSnapshotTree SnapshotLeaf where
   toSnapshotTree s := SnapshotTree.mk s.toSnapshot #[]

src/Lean/Meta/Sym/Arith/Classify.lean

@@ -44,26 +44,6 @@ private def getNoZeroDivInst? (u : Level) (type : Expr) : SymM (Option Expr) :=
   let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type natModuleInst
   Sym.synthInstance? noZeroDivType
 
-private def getPowIdentityInst? (u : Level) (type : Expr) : SymM (Option (Expr × Expr × Nat)) := do withNewMCtxDepth do
-  -- We use a fresh metavar for `CommSemiring` (unlike `getIsCharInst?` which pins the semiring)
-  -- because `PowIdentity` instances may be declared against a canonical `CommSemiring` instance
-  -- that is not definitionally equal to `CommRing.toCommSemiring`. The synthesized `csInst` is
-  -- stored and used in proof terms to ensure type-correctness.
-  let csInst ← mkFreshExprMVar (mkApp (mkConst ``Grind.CommSemiring [u]) type)
-  let p ← mkFreshExprMVar (mkConst ``Nat)
-  let powIdentityType := mkApp3 (mkConst ``Grind.PowIdentity [u]) type csInst p
-  let some inst ← synthInstance? powIdentityType | return none
-  let csInst ← instantiateMVars csInst
-  let p ← instantiateMVars p
-  let some pVal ← evalNat? p | return none
-  return some (inst, csInst, pVal)
-
-private def mkAddRightCancelInst? (u : Level) (type : Expr) : SymM (Option Expr) := do
-  let add := mkApp (mkConst ``Add [u]) type
-  let some addInst ← synthInstance? add | return none
-  let addRightCancel := mkApp2 (mkConst ``Grind.AddRightCancel [u]) type addInst
-  synthInstance? addRightCancel
-
 /-- Try to classify `type` as a `CommRing`. Returns the ring id on success. -/
 private def tryCommRing? (type : Expr) : SymM (Option Nat) := do
   let u ← getDecLevel type
@@ -75,12 +55,11 @@ private def tryCommRing? (type : Expr) : SymM (Option Nat) := do
   let charInst? ← getIsCharInst? u type semiringInst
   let noZeroDivInst? ← getNoZeroDivInst? u type
   let fieldInst? ← Sym.synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
-  let powIdentityInst? ← getPowIdentityInst? u type
   let semiringId? := none
   let id := (← getArithState).rings.size
   let ring : CommRing := {
     id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
-    commRingInst, charInst?, noZeroDivInst?, fieldInst?, powIdentityInst?
+    commRingInst, charInst?, noZeroDivInst?, fieldInst?,
   }
   modifyArithState fun s => { s with rings := s.rings.push ring }
   return some id
@@ -117,14 +96,13 @@ private def tryCommSemiring? (type : Expr) : SymM (Option Nat) := do
   let commSemiring := mkApp (mkConst ``Grind.CommSemiring [u]) type
   let some commSemiringInst ← Sym.synthInstance? commSemiring | return none
   let semiringInst := mkApp2 (mkConst ``Grind.CommSemiring.toSemiring [u]) type commSemiringInst
-  let addRightCancelInst? ← mkAddRightCancelInst? u type
   let q ← shareCommon (← Sym.canon (mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [u]) type semiringInst))
   -- The envelope `Q` type must be classifiable as a CommRing.
   let some ringId ← tryCacheAndCommRing? q
     | reportIssue! "unexpected failure initializing ring{indentExpr q}"; return none
   let id := (← getArithState).semirings.size
   let semiring : CommSemiring := {
-    id, type, ringId, u, semiringInst, commSemiringInst, addRightCancelInst?
+    id, type, ringId, u, semiringInst, commSemiringInst
   }
   modifyArithState fun s => { s with semirings := s.semirings.push semiring }
   -- Link the envelope ring back to this semiring

src/Lean/Meta/Sym/Arith/MonadCanon.lean

@@ -6,8 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Arith.Types
-public import Lean.Meta.Sym.Canon
-public import Lean.Meta.Sym.SynthInstance
 public section
 namespace Lean.Meta.Sym.Arith
 
@@ -35,8 +33,4 @@ def MonadCanon.synthInstance [Monad m] [MonadError m] [MonadCanon m] (type : Exp
     | throwError "failed to find instance{indentExpr type}"
   return inst
 
-instance : MonadCanon SymM where
-  canonExpr := canon
-  synthInstance? := Sym.synthInstance?
-
 end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadVar.lean

@@ -21,12 +21,12 @@ instance (m n) [MonadLift m n] [MonadGetVar m] : MonadGetVar n where
 
 /-- Create or lookup a variable for a Lean expression. Used by reification. -/
 class MonadMkVar (m : Type → Type) where
-  mkVar : Expr → (gen : Nat) → m Var
+  mkVar : Expr → m Var
 
 export MonadMkVar (mkVar)
 
 @[always_inline]
 instance (m n) [MonadLift m n] [MonadMkVar m] : MonadMkVar n where
-  mkVar e gen := liftM (mkVar e gen : m Var)
+  mkVar e := liftM (mkVar e : m Var)
 
 end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Reify.lean

@@ -57,12 +57,12 @@ If `skipVar` is `true`, returns `none` if `e` is not an interpreted ring term
 (used for equalities/disequalities). If `false`, treats non-interpreted terms
 as variables (used for inequalities).
 -/
-partial def reifyRing? (e : Expr) (skipVar : Bool := true) (gen : Nat) : m (Option RingExpr) := do
+partial def reifyRing? (e : Expr) (skipVar : Bool := true) : m (Option RingExpr) := do
   let toVar (e : Expr) : m RingExpr := do
-    return .var (← mkVar e gen)
+    return .var (← mkVar e)
   let asVar (e : Expr) : m RingExpr := do
     reportRingAppIssue e
-    return .var (← mkVar e gen)
+    return .var (← mkVar e)
   let rec go (e : Expr) : m RingExpr := do
     match_expr e with
     | HAdd.hAdd _ _ _ i a b =>
@@ -151,12 +151,12 @@ private def reportSemiringAppIssue [MonadLiftT SymM m] (e : Expr) : m Unit := do
 Converts a Lean expression `e` into a `SemiringExpr`.
 Only recognizes `add`, `mul`, `pow`, `natCast`, and numerals (no `sub`, `neg`, `intCast`).
 -/
-partial def reifySemiring? (e : Expr) (gen : Nat) : m (Option SemiringExpr) := do
+partial def reifySemiring? (e : Expr) : m (Option SemiringExpr) := do
   let toVar (e : Expr) : m SemiringExpr := do
-    return .var (← mkVar e gen)
+    return .var (← mkVar e)
   let asVar (e : Expr) : m SemiringExpr := do
     reportSemiringAppIssue e
-    return .var (← mkVar e gen)
+    return .var (← mkVar e)
   let rec go (e : Expr) : m SemiringExpr := do
     match_expr e with
     | HAdd.hAdd _ _ _ i a b =>

src/Lean/Meta/Sym/Arith/Types.lean

@@ -71,8 +71,6 @@ structure CommRing extends Ring where
   noZeroDivInst?     : Option Expr
   /-- `Field` instance for `type` if available. -/
   fieldInst?         : Option Expr
-  /-- `PowIdentity` instance, the synthesized `CommSemiring` instance, and exponent `p` if available. -/
-  powIdentityInst? : Option (Expr × Expr × Nat) := none
   deriving Inhabited
 
 /--
@@ -81,12 +79,12 @@ Recall that `CommSemiring` types are normalized using the `OfSemiring.Q` envelop
 -/
 structure CommSemiring extends Semiring where
   /-- Id of the envelope ring `OfSemiring.Q type` -/
-  ringId              : Nat
+  ringId             : Nat
   /-- `CommSemiring` instance for `type` -/
-  commSemiringInst    : Expr
+  commSemiringInst   : Expr
   /-- `AddRightCancel` instance for `type` if available. -/
-  addRightCancelInst? : Option Expr := none
-  toQFn?              : Option Expr := none
+  addRightCancelInst? : Option (Option Expr) := none
+  toQFn?             : Option Expr := none
   deriving Inhabited
 
 /-- Result of classifying a type's algebraic structure. -/
@@ -98,11 +96,6 @@ inductive ClassifyResult where
   | /-- No algebraic structure found. -/ none
   deriving Inhabited
 
-def ClassifyResult.toOption : ClassifyResult → Option Nat
- | .commRing id | .nonCommRing id
- | .commSemiring id | .nonCommSemiring id => some id
- | .none => .none
-
 /-- Arith type classification state, stored as a `SymExtension`. -/
 structure State where
   /-- Exponent threshold for `HPow` evaluation. -/
@@ -141,20 +134,4 @@ def withExpThreshold (exp : Nat) (k : SymM α) : SymM α := do
   setExpThreshold exp
   try k finally setExpThreshold oldExp
 
-def getCommRingOfId (id : Nat) : SymM CommRing := do
-  let s ← getArithState
-  return s.rings[id]!
-
-def getNonCommRingOfId (id : Nat) : SymM Ring := do
-  let s ← getArithState
-  return s.ncRings[id]!
-
-def getCommSemiringOfId (id : Nat) : SymM CommSemiring := do
-  let s ← getArithState
-  return s.semirings[id]!
-
-def getNonCommSemiringOfId (id : Nat) : SymM Semiring := do
-  let s ← getArithState
-  return s.ncSemirings[id]!
-
 end Lean.Meta.Sym.Arith

src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean

@@ -12,12 +12,17 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadSemiring
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Action
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Power
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Denote
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 builtin_initialize registerTraceClass `grind.ring

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Denote.lean

@@ -1,32 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
-public import Lean.Meta.Sym.Arith.DenoteExpr
-
-namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
-/-!
-Helper functions for converting reified terms back into their denotations.
--/
-
-variable [Monad M] [MonadGetVar M] [MonadError M] [MonadLiftT MetaM M] [MonadCanon M] [MonadRing M]
-
-def mkEq (a b : Expr) : M Expr := do
-  let r ← getRing
-  return mkApp3 (mkConst ``Eq [r.u.succ]) r.type a b
-
-public def EqCnstr.denoteExpr (c : EqCnstr) : M Expr := do
-  mkEq (← denotePoly c.p) (← denoteNum 0)
-
-public def PolyDerivation.denoteExpr (d : PolyDerivation) : M Expr := do
-  denotePoly d.p
-
-public def DiseqCnstr.denoteExpr (c : DiseqCnstr) : M Expr := do
-  return mkNot (← mkEq (← c.d.denoteExpr) (← denoteNum 0))
-
-end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+public section
+namespace Lean.Meta.Grind.Arith.CommRing
+open Sym.Arith
+/-!
+Helper functions for converting reified terms back into their denotations.
+-/
+
+variable [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadCanon M] [MonadRing M]
+
+def denoteNum (k : Int) : M Expr := do
+  let ring ← getRing
+  let n := mkRawNatLit k.natAbs
+  let ofNatInst ← if let some inst ← synthInstance? (mkApp2 (mkConst ``OfNat [ring.u]) ring.type n) then
+    pure inst
+  else
+    pure <| mkApp3 (mkConst ``Grind.Semiring.ofNat [ring.u]) ring.type ring.semiringInst n
+  let n := mkApp3 (mkConst ``OfNat.ofNat [ring.u]) ring.type n ofNatInst
+  if k < 0 then
+    return mkApp (← getNegFn) n
+  else
+    return n
+
+def _root_.Lean.Grind.CommRing.Power.denoteExpr (pw : Power) : M Expr := do
+  let x := (← getRing).vars[pw.x]!
+  if pw.k == 1 then
+    return x
+  else
+    return mkApp2 (← getPowFn) x (toExpr pw.k)
+
+def _root_.Lean.Grind.CommRing.Mon.denoteExpr (m : Mon) : M Expr := do
+  match m with
+  | .unit => denoteNum 1
+  | .mult pw m => go m (← pw.denoteExpr)
+where
+  go (m : Mon) (acc : Expr) : M Expr := do
+    match m with
+    | .unit => return acc
+    | .mult pw m => go m (mkApp2 (← getMulFn) acc (← pw.denoteExpr))
+
+def _root_.Lean.Grind.CommRing.Poly.denoteExpr (p : Poly) : M Expr := do
+  match p with
+  | .num k => denoteNum k
+  | .add k m p => go p (← denoteTerm k m)
+where
+  denoteTerm (k : Int) (m : Mon) : M Expr := do
+    if k == 1 then
+      m.denoteExpr
+    else
+      return mkApp2 (← getMulFn) (← denoteNum k) (← m.denoteExpr)
+
+  go (p : Poly) (acc : Expr) : M Expr := do
+    match p with
+    | .num 0 => return acc
+    | .num k => return mkApp2 (← getAddFn) acc (← denoteNum k)
+    | .add k m p => go p (mkApp2 (← getAddFn) acc (← denoteTerm k m))
+
+@[specialize]
+private def denoteExprCore (getVar : Nat → Expr) (e : RingExpr) : M Expr := do
+  go e
+where
+  go : RingExpr → M Expr
+  | .num k => denoteNum k
+  | .natCast k => return mkApp (← getNatCastFn) (mkNatLit k)
+  | .intCast k => return mkApp (← getIntCastFn) (mkIntLit k)
+  | .var x => return getVar x
+  | .add a b => return mkApp2 (← getAddFn) (← go a) (← go b)
+  | .sub a b => return mkApp2 (← getSubFn) (← go a) (← go b)
+  | .mul a b => return mkApp2 (← getMulFn) (← go a) (← go b)
+  | .pow a k => return mkApp2 (← getPowFn) (← go a) (toExpr k)
+  | .neg a => return mkApp (← getNegFn) (← go a)
+
+def _root_.Lean.Grind.CommRing.Expr.denoteExpr (e : RingExpr) : M Expr := do
+  let ring ← getRing
+  denoteExprCore (fun x => ring.vars[x]!) e
+
+def _root_.Lean.Grind.CommRing.Expr.denoteExpr' (vars : Array Expr) (e : RingExpr) : M Expr := do
+  denoteExprCore (fun x => vars[x]!) e
+
+private def mkEq (a b : Expr) : M Expr := do
+  let r ← getRing
+  return mkApp3 (mkConst ``Eq [r.u.succ]) r.type a b
+
+def EqCnstr.denoteExpr (c : EqCnstr) : M Expr := do
+  mkEq (← c.p.denoteExpr) (← denoteNum 0)
+
+def PolyDerivation.denoteExpr (d : PolyDerivation) : M Expr := do
+  d.p.denoteExpr
+
+def DiseqCnstr.denoteExpr (c : DiseqCnstr) : M Expr := do
+  return mkNot (← mkEq (← c.d.denoteExpr) (← denoteNum 0))
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -9,7 +9,9 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
 public section
 namespace Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
+public section
+namespace Lean.Meta.Grind.Arith.CommRing
+open Sym.Arith
+variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m]
+
+section
+variable [MonadRing m]
+
+def checkInst (declName : Name) (inst inst' : Expr) : MetaM Unit := do
+  unless (← isDefEqI inst inst') do
+    throwError "error while initializing `grind ring` operators:\ninstance for `{declName}` {indentExpr inst}\nis not definitionally equal to the expected one {indentExpr inst'}\nwhen only reducible definitions and instances are reduced"
+
+def mkUnaryFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
+  let inst ← MonadCanon.synthInstance <| mkApp (mkConst instDeclName [u]) type
+  checkInst declName inst expectedInst
+  canonExpr <| mkApp2 (mkConst declName [u]) type inst
+
+def mkBinHomoFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
+  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst instDeclName [u, u, u]) type type type
+  checkInst declName inst expectedInst
+  canonExpr <| mkApp4 (mkConst declName [u, u, u]) type type type inst
+
+def mkPowFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
+  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
+  let inst' := mkApp2 (mkConst ``Grind.Semiring.npow [u]) type semiringInst
+  checkInst ``HPow.hPow inst inst'
+  canonExpr <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type inst
+
+def mkNatCastFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
+  let inst' := mkApp2 (mkConst ``Grind.Semiring.natCast [u]) type semiringInst
+  let instType := mkApp (mkConst ``NatCast [u]) type
+  -- Note that `Semiring.natCast` is not registered as a global instance
+  -- (to avoid introducing unwanted coercions)
+  -- so merely having a `Semiring α` instance
+  -- does not guarantee that an `NatCast α` will be available.
+  -- When both are present we verify that they are defeq,
+  -- and otherwise fall back to the field of the `Semiring α` instance that we already have.
+  let inst ← match (← MonadCanon.synthInstance? instType) with
+  | none => pure inst'
+  | some inst => checkInst ``NatCast.natCast inst inst'; pure inst
+  canonExpr <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst
+
+def getAddFn : m Expr := do
+  let ring ← getRing
+  if let some addFn := ring.addFn? then return addFn
+  let expectedInst := mkApp2 (mkConst ``instHAdd [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Semiring.toAdd [ring.u]) ring.type ring.semiringInst
+  let addFn ← mkBinHomoFn ring.type ring.u ``HAdd ``HAdd.hAdd expectedInst
+  modifyRing fun s => { s with addFn? := some addFn }
+  return addFn
+
+def getSubFn : m Expr := do
+  let ring ← getRing
+  if let some subFn := ring.subFn? then return subFn
+  let expectedInst := mkApp2 (mkConst ``instHSub [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Ring.toSub [ring.u]) ring.type ring.ringInst
+  let subFn ← mkBinHomoFn ring.type ring.u ``HSub ``HSub.hSub expectedInst
+  modifyRing fun s => { s with subFn? := some subFn }
+  return subFn
+
+def getMulFn : m Expr := do
+  let ring ← getRing
+  if let some mulFn := ring.mulFn? then return mulFn
+  let expectedInst := mkApp2 (mkConst ``instHMul [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Semiring.toMul [ring.u]) ring.type ring.semiringInst
+  let mulFn ← mkBinHomoFn ring.type ring.u ``HMul ``HMul.hMul expectedInst
+  modifyRing fun s => { s with mulFn? := some mulFn }
+  return mulFn
+
+def getNegFn : m Expr := do
+  let ring ← getRing
+  if let some negFn := ring.negFn? then return negFn
+  let expectedInst := mkApp2 (mkConst ``Grind.Ring.toNeg [ring.u]) ring.type ring.ringInst
+  let negFn ← mkUnaryFn ring.type ring.u ``Neg ``Neg.neg expectedInst
+  modifyRing fun s => { s with negFn? := some negFn }
+  return negFn
+
+def getPowFn : m Expr := do
+  let ring ← getRing
+  if let some powFn := ring.powFn? then return powFn
+  let powFn ← mkPowFn ring.u ring.type ring.semiringInst
+  modifyRing fun s => { s with powFn? := some powFn }
+  return powFn
+
+def getIntCastFn : m Expr := do
+  let ring ← getRing
+  if let some intCastFn := ring.intCastFn? then return intCastFn
+  let inst' := mkApp2 (mkConst ``Grind.Ring.intCast [ring.u]) ring.type ring.ringInst
+  let instType := mkApp (mkConst ``IntCast [ring.u]) ring.type
+  -- Note that `Ring.intCast` is not registered as a global instance
+  -- (to avoid introducing unwanted coercions)
+  -- so merely having a `Ring α` instance
+  -- does not guarantee that an `IntCast α` will be available.
+  -- When both are present we verify that they are defeq,
+  -- and otherwise fall back to the field of the `Ring α` instance that we already have.
+  let inst ← match (← MonadCanon.synthInstance? instType) with
+    | none => pure inst'
+    | some inst => checkInst ``Int.cast inst inst'; pure inst
+  let intCastFn ← canonExpr <| mkApp2 (mkConst ``IntCast.intCast [ring.u]) ring.type inst
+  modifyRing fun s => { s with intCastFn? := some intCastFn }
+  return intCastFn
+
+def getNatCastFn : m Expr := do
+  let ring ← getRing
+  if let some natCastFn := ring.natCastFn? then return natCastFn
+  let natCastFn ← mkNatCastFn ring.u ring.type ring.semiringInst
+  modifyRing fun s => { s with natCastFn? := some natCastFn }
+  return natCastFn
+
+private def mkOne (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
+  let n := mkRawNatLit 1
+  let ofNatInst := mkApp3 (mkConst ``Grind.Semiring.ofNat [u]) type semiringInst n
+  canonExpr <| mkApp3 (mkConst ``OfNat.ofNat [u]) type n ofNatInst
+
+def getOne [MonadLiftT GoalM m] : m Expr := do
+  let ring ← getRing
+  if let some one := ring.one? then return one
+  let one ← mkOne ring.u ring.type ring.semiringInst
+  modifyRing fun s => { s with one? := some one }
+  internalize one 0
+  return one
+end
+
+section
+variable [MonadCommRing m]
+
+def getInvFn : m Expr := do
+  let ring ← getCommRing
+  let some fieldInst := ring.fieldInst?
+    | throwError "`grind` internal error, type is not a field{indentExpr ring.type}"
+  if let some invFn := ring.invFn? then return invFn
+  let expectedInst := mkApp2 (mkConst ``Grind.Field.toInv [ring.u]) ring.type fieldInst
+  let invFn ← mkUnaryFn ring.type ring.u ``Inv ``Inv.inv expectedInst
+  modifyCommRing fun s => { s with invFn? := some invFn }
+  return invFn
+end
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean

@@ -6,16 +6,12 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
-import Lean.Meta.Sym.Arith.Reify
-import Lean.Meta.Sym.Arith.DenoteExpr
-import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
-import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
-import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Util
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym Arith
 
 /-- If `e` is a function application supported by the `CommRing` module, return its type. -/
 private def getType? (e : Expr) : Option Expr :=
@@ -84,8 +80,8 @@ private def processInv (e inst a : Expr) : RingM Unit := do
   unless (← isInvInst inst) do return ()
   let ring ← getCommRing
   let some fieldInst := ring.fieldInst? | return ()
-  if (← getCommRingEntry).invSet.contains a then return ()
-  modifyCommRingEntry fun s => { s with invSet := s.invSet.insert a }
+  if (← getCommRing).invSet.contains a then return ()
+  modifyCommRing fun s => { s with invSet := s.invSet.insert a }
   if let some k ← toInt? a then
     if k == 0 then
       /-
@@ -123,9 +119,8 @@ push the equation `x ^ p = x` as a new fact into grind.
 private def processPowIdentityVars : RingM Unit := do
   let ring ← getCommRing
   let some (powIdentityInst, csInst, p) := ring.powIdentityInst? | return ()
-  let ringEntry ← getCommRingEntry
-  let startIdx := ringEntry.powIdentityVarCount
-  let vars := ringEntry.vars
+  let startIdx := ring.powIdentityVarCount
+  let vars := ring.toRing.vars
   if startIdx >= vars.size then return ()
   for i in [startIdx:vars.size] do
     let x := vars[i]!
@@ -134,7 +129,7 @@ private def processPowIdentityVars : RingM Unit := do
     let proof := mkApp5 (mkConst ``Grind.PowIdentity.pow_eq [ring.u])
       ring.type csInst (mkNatLit p) powIdentityInst x
     pushNewFact proof
-  modifyCommRingEntry fun s => { s with powIdentityVarCount := vars.size }
+  modifyCommRing fun s => { s with powIdentityVarCount := vars.size }
 
 /-- Returns `true` if `e` is a term `a⁻¹`. -/
 private def internalizeInv (e : Expr) : GoalM Bool := do
@@ -153,34 +148,33 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   if (← internalizeInv e) then return ()
   let some type := getType? e | return ()
   if isForbiddenParent parent? then return ()
-  let gen ← getGeneration e
   if let some ringId ← getCommRingId? type then RingM.run ringId do
-    let some re ← reifyRing? e (gen := gen) | return ()
+    let some re ← reify? e | return ()
     trace_goal[grind.ring.internalize] "[{ringId}]: {e}"
     setTermRingId e
     ringExt.markTerm e
-    modifyCommRingEntry fun s => { s with
+    modifyCommRing fun s => { s with
       denote := s.denote.insert { expr := e } re
       denoteEntries := s.denoteEntries.push (e, re)
     }
     processPowIdentityVars
   else if let some semiringId ← getCommSemiringId? type then SemiringM.run semiringId do
-    let some re ← reifySemiring? e (gen := gen) | return ()
+    let some re ← sreify? e | return ()
     trace_goal[grind.ring.internalize] "semiring [{semiringId}]: {e}"
     setTermSemiringId e
     ringExt.markTerm e
-    modifyCommSemiringEntry fun s => { s with denote := s.denote.insert { expr := e } re }
+    modifySemiring fun s => { s with denote := s.denote.insert { expr := e } re }
   else if let some ncRingId ← getNonCommRingId? type then NonCommRingM.run ncRingId do
-    let some re ← reifyRing? e (gen := gen) | return ()
+    let some re ← ncreify? e | return ()
     trace_goal[grind.ring.internalize] "(non-comm) ring [{ncRingId}]: {e}"
     setTermNonCommRingId e
     ringExt.markTerm e
-    modifyRingEntry fun s => { s with denote := s.denote.insert { expr := e } re }
+    modifyRing fun s => { s with denote := s.denote.insert { expr := e } re }
   else if let some ncSemiringId ← getNonCommSemiringId? type then NonCommSemiringM.run ncSemiringId do
-    let some re ← reifySemiring? e (gen := gen) | return ()
+    let some re ← ncsreify? e | return ()
     trace_goal[grind.ring.internalize] "(non-comm) semiring [{ncSemiringId}]: {e}"
     setTermNonCommSemiringId e
     ringExt.markTerm e
-    modifySemiringEntry fun s => { s with denote := s.denote.insert { expr := e } re }
+    modifySemiring fun s => { s with denote := s.denote.insert { expr := e } re }
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean

@@ -9,7 +9,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 import Lean.Meta.Sym.Arith.Poly
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-/-
+
 private def checkVars : RingM Unit := do
   let s ← getRing
   let mut num := 0
@@ -42,14 +42,11 @@ private def checkDiseqs : RingM Unit := do
   for c in (← getCommRing).diseqs do
     checkPoly c.d.p
 
--/
-
 private def checkRingInvs : RingM Unit := do
-  -- checkVars
-  -- checkBasis
-  -- checkQueue
-  -- checkDiseqs
-  return ()
+  checkVars
+  checkBasis
+  checkQueue
+  checkDiseqs
 
 def checkInvariants : GoalM Unit := do
   if (← isDebugEnabled) then

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Arith.MonadCanon
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public section
+namespace Lean.Meta.Grind.Arith.CommRing
+
+class MonadRing (m : Type → Type) where
+  getRing : m Ring
+  modifyRing : (Ring → Ring) → m Unit
+
+export MonadRing (getRing modifyRing)
+
+@[always_inline]
+instance (m n) [MonadLift m n] [MonadRing m] : MonadRing n where
+  getRing    := liftM (getRing : m Ring)
+  modifyRing f := liftM (modifyRing f : m Unit)
+
+class MonadCommRing (m : Type → Type) where
+  getCommRing : m CommRing
+  modifyCommRing : (CommRing → CommRing) → m Unit
+
+export MonadCommRing (getCommRing modifyCommRing)
+
+@[always_inline]
+instance (m n) [MonadLift m n] [MonadCommRing m] : MonadCommRing n where
+  getCommRing      := liftM (getCommRing : m CommRing)
+  modifyCommRing f := liftM (modifyCommRing f : m Unit)
+
+@[always_inline]
+instance (m) [Monad m] [MonadCommRing m] : MonadRing m where
+  getRing := return (← getCommRing).toRing
+  modifyRing f := modifyCommRing fun s => { s with toRing := f s.toRing }
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadSemiring.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Arith.MonadCanon
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public section
+namespace Lean.Meta.Grind.Arith.CommRing
+
+class MonadSemiring (m : Type → Type) where
+  getSemiring : m Semiring
+  modifySemiring : (Semiring → Semiring) → m Unit
+
+export MonadSemiring (getSemiring modifySemiring)
+
+@[always_inline]
+instance (m n) [MonadLift m n] [MonadSemiring m] : MonadSemiring n where
+  getSemiring    := liftM (getSemiring : m Semiring)
+  modifySemiring f := liftM (modifySemiring f : m Unit)
+
+class MonadCommSemiring (m : Type → Type) where
+  getCommSemiring : m CommSemiring
+  modifyCommSemiring : (CommSemiring → CommSemiring) → m Unit
+
+export MonadCommSemiring (getCommSemiring modifyCommSemiring)
+
+@[always_inline]
+instance (m n) [MonadLift m n] [MonadCommSemiring m] : MonadCommSemiring n where
+  getCommSemiring      := liftM (getCommSemiring : m CommSemiring)
+  modifyCommSemiring f := liftM (modifyCommSemiring f : m Unit)
+
+@[always_inline]
+instance (m) [Monad m] [MonadCommSemiring m] : MonadSemiring m where
+  getSemiring := return (← getCommSemiring).toSemiring
+  modifySemiring f := modifyCommSemiring fun s => { s with toSemiring := f s.toSemiring }
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.lean

@@ -9,30 +9,30 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 open Sym.Arith
-
 structure NonCommRingM.Context where
   ringId : Nat
-  symRingId : Nat
 
 /-- We don't want to keep carrying the `RingId` around. -/
 abbrev NonCommRingM := ReaderT NonCommRingM.Context GoalM
 
-abbrev NonCommRingM.run (ringId : Nat) (x : NonCommRingM α) : GoalM α := do
-  let s ← get'
-  let symRingId := s.ncRings[ringId]!.symId
-  x { ringId, symRingId }
+abbrev NonCommRingM.run (ringId : Nat) (x : NonCommRingM α) : GoalM α :=
+  x { ringId }
+
+instance : MonadCanon NonCommRingM where
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
 
 protected def NonCommRingM.getRing : NonCommRingM Ring := do
-  let s ← getArithState
-  let ringId := (← read).symRingId
+  let s ← get'
+  let ringId := (← read).ringId
   if h : ringId < s.ncRings.size then
     return s.ncRings[ringId]
   else
     throwError "`grind` internal error, invalid ringId"
 
 protected def NonCommRingM.modifyRing (f : Ring → Ring) : NonCommRingM Unit := do
-  let ringId := (← read).symRingId
-  modifyArithState fun s => { s with ncRings := s.ncRings.modify ringId f }
+  let ringId := (← read).ringId
+  modify' fun s => { s with ncRings := s.ncRings.modify ringId f }
 
 instance : MonadRing NonCommRingM where
   getRing := NonCommRingM.getRing
@@ -49,37 +49,7 @@ def setTermNonCommRingId (e : Expr) : NonCommRingM Unit := do
     return ()
   modify' fun s => { s with exprToNCRingId := s.exprToNCRingId.insert { expr := e } ringId }
 
-def getRingEntry : NonCommRingM RingEntry := do
-  let s ← get'
-  let ringId := (← read).ringId
-  if h : ringId < s.ncRings.size then
-    return s.ncRings[ringId]
-  else
-    throwError "`grind` internal error, invalid ringId"
-
-def modifyRingEntry (f : RingEntry → RingEntry) : NonCommRingM Unit := do
-  let ringId := (← read).ringId
-  modify' fun s => { s with ncRings := s.ncRings.modify ringId f }
-
-def mkNonCommVar (e : Expr) (gen : Nat) : NonCommRingM Var := do
-  unless (← alreadyInternalized e) do
-    internalize e gen
-  let s ← getRingEntry
-  if let some var := s.varMap.find? { expr := e } then
-    return var
-  let var : Var := s.vars.size
-  modifyRingEntry fun s => { s with
-    vars       := s.vars.push e
-    varMap     := s.varMap.insert { expr := e } var
-  }
-  setTermNonCommRingId e
-  ringExt.markTerm e
-  return var
-
-instance : MonadMkVar NonCommRingM where
-  mkVar := mkNonCommVar
-
-instance : MonadGetVar NonCommRingM where
-  getVar x := return (← getRingEntry).vars[x]!
+instance : MonadSetTermId NonCommRingM where
+  setTermId e := setTermNonCommRingId e
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommSemiringM.lean

@@ -8,47 +8,36 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
+open Sym.Arith (MonadCanon)
 
 structure NonCommSemiringM.Context where
   semiringId : Nat
-  symSemiringId : Nat
 
 abbrev NonCommSemiringM := ReaderT NonCommSemiringM.Context GoalM
 
-abbrev NonCommSemiringM.run (semiringId : Nat) (x : NonCommSemiringM α) : GoalM α := do
-  let s ← get'
-  let symSemiringId := s.ncSemirings[semiringId]!.symId
-  x { semiringId, symSemiringId }
+abbrev NonCommSemiringM.run (semiringId : Nat) (x : NonCommSemiringM α) : GoalM α :=
+  x { semiringId }
+
+instance : MonadCanon NonCommSemiringM where
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
 
 protected def NonCommSemiringM.getSemiring : NonCommSemiringM Semiring := do
-  let s ← getArithState
-  let semiringId := (← read).symSemiringId
+  let s ← get'
+  let semiringId := (← read).semiringId
   if h : semiringId < s.ncSemirings.size then
     return s.ncSemirings[semiringId]
   else
     throwError "`grind` internal error, invalid semiringId"
 
 protected def NonCommSemiringM.modifySemiring (f : Semiring → Semiring) : NonCommSemiringM Unit := do
-  let semiringId := (← read).symSemiringId
-  modifyArithState fun s => { s with ncSemirings := s.ncSemirings.modify semiringId f }
+  let semiringId := (← read).semiringId
+  modify' fun s => { s with ncSemirings := s.ncSemirings.modify semiringId f }
 
 instance : MonadSemiring NonCommSemiringM where
   getSemiring := NonCommSemiringM.getSemiring
   modifySemiring := NonCommSemiringM.modifySemiring
 
-def getSemiringEntry : NonCommSemiringM SemiringEntry := do
-  let s ← get'
-  let semiringId := (← read).semiringId
-  if h : semiringId < s.ncSemirings.size then
-    return s.ncSemirings[semiringId]
-  else
-    throwError "`grind` internal error, invalid semiringId"
-
-def modifySemiringEntry (f : SemiringEntry → SemiringEntry) : NonCommSemiringM Unit := do
-  let semiringId := (← read).semiringId
-  modify' fun s => { s with ncSemirings := s.ncSemirings.modify semiringId f }
-
 def getTermNonCommSemiringId? (e : Expr) : GoalM (Option Nat) := do
     return (← get').exprToNCSemiringId.find? { expr := e }
 
@@ -60,25 +49,7 @@ def setTermNonCommSemiringId (e : Expr) : NonCommSemiringM Unit := do
     return ()
   modify' fun s => { s with exprToNCSemiringId := s.exprToNCSemiringId.insert { expr := e } semiringId }
 
-def mkNonCommSVar (e : Expr) (gen : Nat) : NonCommSemiringM Var := do
-  unless (← alreadyInternalized e) do
-    internalize e gen
-  let s ← getSemiringEntry
-  if let some var := s.varMap.find? { expr := e } then
-    return var
-  let var : Var := s.vars.size
-  modifySemiringEntry fun s => { s with
-    vars       := s.vars.push e
-    varMap     := s.varMap.insert { expr := e } var
-  }
-  setTermNonCommSemiringId e
-  ringExt.markTerm e
-  return var
-
-instance : MonadMkVar NonCommSemiringM where
-  mkVar := mkNonCommSVar
-
-instance : MonadGetVar NonCommSemiringM where
-  getVar x := return (← getSemiringEntry).vars[x]!
+instance : MonadSetTermId NonCommSemiringM where
+  setTermId e := setTermNonCommSemiringId e
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean

@@ -6,26 +6,21 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Denote
-import Lean.Meta.Sym.Arith.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Init.Omega
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 open Sym.Arith
 
-private abbrev M := StateT (CommRing × CommRingEntry) MetaM
+private abbrev M := StateT CommRing MetaM
 
 private instance : MonadCanon M where
   canonExpr e := return e
   synthInstance? e := Meta.synthInstance? e none
 
 private instance : MonadCommRing M where
-  getCommRing := return (← get).1
-  modifyCommRing f := modify fun (r, e) => (f r, e)
-
-private instance : MonadGetVar M where
-  getVar x := return (← get).2.vars[x]!
+  getCommRing := get
+  modifyCommRing := modify
 
 private def toOption (cls : Name) (header : Thunk MessageData) (msgs : Array MessageData) : Option MessageData :=
   if msgs.isEmpty then
@@ -36,18 +31,15 @@ private def toOption (cls : Name) (header : Thunk MessageData) (msgs : Array Mes
 private def push (msgs : Array MessageData) (msg? : Option MessageData) : Array MessageData :=
   if let some msg := msg? then msgs.push msg else msgs
 
-private def getCommRingEntry : M CommRingEntry :=
-  return (← get).2
-
 private def ppBasis? : M (Option MessageData) := do
   let mut basis := #[]
-  for c in (← getCommRingEntry).basis do
+  for c in (← getCommRing).basis do
     basis := basis.push (toTraceElem (← c.denoteExpr))
   return toOption `basis "Basis" basis
 
 private def ppDiseqs? : M (Option MessageData) := do
   let mut diseqs := #[]
-  for d in (← getCommRingEntry).diseqs do
+  for d in (← getCommRing).diseqs do
     diseqs := diseqs.push (toTraceElem (← d.denoteExpr))
   return toOption `diseqs "Disequalities" diseqs
 
@@ -59,12 +51,9 @@ private def ppRing? : M (Option MessageData) := do
 
 def pp? (goal : Goal) : MetaM (Option MessageData) := do
   let mut msgs := #[]
-  for ringEntry in (← ringExt.getStateCore goal).rings do
-    -- let ring ← getCommRingOfId ringEntry.symId
-    -- let some msg ← ppRing? |>.run' (_, ringEntry) | pure ()
-    -- msgs := msgs.push msg
-    -- TODO: fix
-    pure ()
+  for ring in (← ringExt.getStateCore goal).rings do
+    let some msg ← ppRing? |>.run' ring | pure ()
+    msgs := msgs.push msg
   if msgs.isEmpty then
     return none
   else if h : msgs.size = 1 then

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean

@@ -8,18 +8,17 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Denote
 import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
-import Lean.Meta.Sym.Arith.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Sym.Arith.ToExpr
 import Lean.Meta.Sym.Arith.VarRename
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
+open Sym.Arith (MonadCanon)
 
 /--
 Returns a context of type `RArray α` containing the variables `vars` where
@@ -58,7 +57,7 @@ private def throwNoNatZeroDivisors : RingM α := do
 
 private def getPolyConst (p : Poly) : RingM Int := do
   let .num k := p
-    | throwError "`grind` internal error, constant polynomial expected {indentExpr (← denotePoly p)}"
+    | throwError "`grind` internal error, constant polynomial expected {indentExpr (← p.denoteExpr)}"
   return k
 
 structure ProofM.State where
@@ -136,9 +135,6 @@ private def getSemiringIdOf : RingM Nat := do
 private def getSemiringOf : RingM CommSemiring := do
   SemiringM.run (← getSemiringIdOf) do getCommSemiring
 
-private def getSemiringEntryOf : RingM CommSemiringEntry := do
-  SemiringM.run (← getSemiringIdOf) do getCommSemiringEntry
-
 private def mkSemiringPrefix (declName : Name) : ProofM Expr := do
   let sctx ← getSContext
   let semiring ← getSemiringOf
@@ -147,7 +143,7 @@ private def mkSemiringPrefix (declName : Name) : ProofM Expr := do
 private def mkSemiringAddRightCancelPrefix (declName : Name) : ProofM Expr := do
   let sctx ← getSContext
   let semiring ← getSemiringOf
-  let some addRightCancelInst ← SemiringM.run (← getSemiringIdOf) do return (← getCommSemiring).addRightCancelInst?
+  let some addRightCancelInst ← SemiringM.run (← getSemiringIdOf) do getAddRightCancelInst?
     | throwError "`grind` internal error, `AddRightCancel` instance is not available"
   return mkApp4 (mkConst declName [semiring.u]) semiring.type semiring.semiringInst addRightCancelInst sctx
 
@@ -245,7 +241,7 @@ private def mkContext (h : Expr) : ProofM Expr := do
     collectMapVars (← get).exprDecls (·.collectVars) <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := (← getCommRingEntry).vars
+  let vars         := (← getRing).vars
   let vars         := vars'.map fun x => vars[x]!
   let h := mkLetOfMap (← get).polyDecls h `p (mkConst ``Grind.CommRing.Poly) fun p => toExpr <| p.renameVars varRename
   let h := mkLetOfMap (← get).monDecls h `m (mkConst ``Grind.CommRing.Mon) fun m => toExpr <| m.renameVars varRename
@@ -262,12 +258,11 @@ private def mkContext (h : Expr) : ProofM Expr := do
 private def mkSemiringContext (h : Expr) : ProofM Expr := do
   let some sctx := (← read).sctx? | return h
   let some semiringId := (← getCommRing).semiringId? | return h
-  let semiring      ← getSemiringOf
-  let semiringEntry ← getSemiringEntryOf
+  let semiring ← getSemiringOf
   let usedVars     := collectMapVars (← get).sexprDecls (·.collectVars) {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := vars'.map fun x => semiringEntry.vars[x]!
+  let vars         := vars'.map fun x => semiring.vars[x]!
   let h := mkLetOfMap (← get).sexprDecls h `s (mkConst ``Grind.CommRing.Expr) fun s => toExpr <| s.renameVars varRename
   let h := h.abstract #[sctx]
   if h.hasLooseBVars then
@@ -332,7 +327,7 @@ def setSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : SemiringM Unit :
   let usedVars     := sa.collectVars >> sb.collectVars <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := (← getCommSemiringEntry).vars
+  let vars         := (← getSemiring).vars
   let vars         := vars'.map fun x => vars[x]!
   let sa           := sa.renameVars varRename
   let sb           := sb.renameVars varRename
@@ -347,12 +342,11 @@ terms s.t. `ra.toPoly_nc == rb.toPoly_nc`, close the goal.
 -/
 def setNonCommRingDiseqUnsat (a b : Expr) (ra rb : RingExpr) : NonCommRingM Unit := do
   let ring ← getRing
-  let ringEntry ← getRingEntry
   let hne ← mkDiseqProof a b
   let usedVars     := ra.collectVars >> rb.collectVars <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := ringEntry.vars
+  let vars         := ring.vars
   let vars         := vars'.map fun x => vars[x]!
   let ra           := ra.renameVars varRename
   let rb           := rb.renameVars varRename
@@ -370,12 +364,11 @@ terms s.t. `sa.toPolyS_nc == sb.toPolyS_nc`, close the goal.
 -/
 def setNonCommSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : NonCommSemiringM Unit := do
   let semiring ← getSemiring
-  let semiringEntry ← getSemiringEntry
   let hne ← mkDiseqProof a b
   let usedVars     := sa.collectVars >> sb.collectVars <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := semiringEntry.vars
+  let vars         := semiring.vars
   let vars         := vars'.map fun x => vars[x]!
   let sa           := sa.renameVars varRename
   let sb           := sb.renameVars varRename
@@ -404,8 +397,7 @@ private def norm (vars : PArray Expr) (lhs rhs lhs' rhs' : RingExpr) : NormResul
 
 def mkLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let ringEntry ← getCommRingEntry
-  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -417,8 +409,7 @@ def mkLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs
 
 def mkLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let ringEntry ← getCommRingEntry
-  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -430,8 +421,7 @@ def mkLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst :
 
 def mkEqIffProof (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let ringEntry ← getCommRingEntry
-  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr [ring.u]) ring.type ring.commRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -446,8 +436,7 @@ Given `e` and `e'` s.t. `e.toPoly == e'.toPoly`, returns a proof that `e.denote
 -/
 def mkTermEqProof (e e' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let ringEntry ← getCommRingEntry
-  let { lhs, lhs', vars, .. } := norm ringEntry.vars e (.num 0) e' (.num 0)
+  let { lhs, lhs', vars, .. } := norm ring.vars e (.num 0) e' (.num 0)
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.Expr.eq_of_toPoly_eq [ring.u]) ring.type ring.commRingInst
   let h := mkApp4 h ctx (toExpr lhs) (toExpr lhs') eagerReflBoolTrue
@@ -457,8 +446,7 @@ def mkTermEqProof (e e' : RingExpr) : RingM Expr := do
 
 def mkNonCommLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let ringEntry ← getRingEntry
-  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -470,8 +458,7 @@ def mkNonCommLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (l
 
 def mkNonCommLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let ringEntry ← getRingEntry
-  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -483,8 +470,7 @@ def mkNonCommLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRin
 
 def mkNonCommEqIffProof (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let ringEntry ← getRingEntry
-  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr_nc [ring.u]) ring.type ring.ringInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -499,8 +485,7 @@ Given `e` and `e'` s.t. `e.toPoly_nc == e'.toPoly_nc`, returns a proof that `e.d
 -/
 def mkNonCommTermEqProof (e e' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let ringEntry ← getRingEntry
-  let { lhs, lhs', vars, .. } := norm ringEntry.vars e (.num 0) e' (.num 0)
+  let { lhs, lhs', vars, .. } := norm ring.vars e (.num 0) e' (.num 0)
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.Expr.eq_of_toPoly_nc_eq [ring.u]) ring.type ring.ringInst
   let h := mkApp4 h ctx (toExpr lhs) (toExpr lhs') eagerReflBoolTrue

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean

@@ -0,0 +1,203 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
+public section
+namespace Lean.Meta.Grind.Arith.CommRing
+open Sym.Arith (MonadCanon)
+
+variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m]
+
+def isAddInst (inst : Expr) : m Bool :=
+  return isSameExpr (← getAddFn).appArg! inst
+def isMulInst (inst : Expr) : m Bool :=
+  return isSameExpr (← getMulFn).appArg! inst
+def isSubInst (inst : Expr) : m Bool :=
+  return isSameExpr (← getSubFn).appArg! inst
+def isNegInst (inst : Expr) : m Bool :=
+  return isSameExpr (← getNegFn).appArg! inst
+def isPowInst (inst : Expr) : m Bool :=
+  return isSameExpr (← getPowFn).appArg! inst
+def isIntCastInst (inst : Expr) : m Bool :=
+  return isSameExpr (← getIntCastFn).appArg! inst
+def isNatCastInst (inst : Expr) : m Bool :=
+  return isSameExpr (← getNatCastFn).appArg! inst
+
+private def reportAppIssue (e : Expr) : GoalM Unit := do
+  reportIssue! "ring term with unexpected instance{indentExpr e}"
+
+variable [MonadLiftT GoalM m] [MonadSetTermId m]
+
+/--
+Converts a Lean expression `e` in the `CommRing` into a `CommRing.Expr` object.
+
+If `skipVar` is `true`, then the result is `none` if `e` is not an interpreted `CommRing` term.
+We use `skipVar := false` when processing inequalities, and `skipVar := true` for equalities and disequalities
+-/
+partial def reifyCore? (e : Expr) (skipVar : Bool) (gen : Nat) : m (Option RingExpr) := do
+  let mkVar (e : Expr) : m Var := do
+    if (← alreadyInternalized e) then
+      mkVarCore e
+    else
+      internalize e gen
+      mkVarCore e
+  let toVar (e : Expr) : m RingExpr := do
+    return .var (← mkVar e)
+  let asVar (e : Expr) : m RingExpr := do
+    reportAppIssue e
+    return .var (← mkVar e)
+  let rec go (e : Expr) : m RingExpr := do
+    match_expr e with
+    | HAdd.hAdd _ _ _ i a b =>
+      if (← isAddInst i) then return .add (← go a) (← go b) else asVar e
+    | HMul.hMul _ _ _ i a b =>
+      if (← isMulInst i) then return .mul (← go a) (← go b) else asVar e
+    | HSub.hSub _ _ _ i a b =>
+      if (← isSubInst i) then return .sub (← go a) (← go b) else asVar e
+    | HPow.hPow _ _ _ i a b =>
+      let some k ← getNatValue? b | toVar e
+      if (← isPowInst i) then return .pow (← go a) k else asVar e
+    | Neg.neg _ i a =>
+      if (← isNegInst i) then return .neg (← go a) else asVar e
+    | IntCast.intCast _ i a =>
+      if (← isIntCastInst i) then
+        let some k ← getIntValue? a | toVar e
+        return .intCast k
+      else
+        asVar e
+    | NatCast.natCast _ i a =>
+      if (← isNatCastInst i) then
+        let some k ← getNatValue? a | toVar e
+        return .natCast k
+      else
+        asVar e
+    | OfNat.ofNat _ n _ =>
+      let some k ← getNatValue? n | toVar e
+      return .num k
+    | BitVec.ofNat _ n =>
+      let some k ← getNatValue? n | toVar e
+      return .num k
+    | _ => toVar e
+  let toTopVar (e : Expr) : m (Option RingExpr) := do
+    if skipVar then
+      return none
+    else
+      return some (← toVar e)
+  let asTopVar (e : Expr) : m (Option RingExpr) := do
+    reportAppIssue e
+    toTopVar e
+  match_expr e with
+  | HAdd.hAdd _ _ _ i a b =>
+    if (← isAddInst i) then return some (.add (← go a) (← go b)) else asTopVar e
+  | HMul.hMul _ _ _ i a b =>
+    if (← isMulInst i) then return some (.mul (← go a) (← go b)) else asTopVar e
+  | HSub.hSub _ _ _ i a b =>
+    if (← isSubInst i) then return some (.sub (← go a) (← go b)) else asTopVar e
+  | HPow.hPow _ _ _ i a b =>
+    let some k ← getNatValue? b | asTopVar e
+    if (← isPowInst i) then return some (.pow (← go a) k) else asTopVar e
+  | Neg.neg _ i a =>
+    if (← isNegInst i) then return some (.neg (← go a)) else asTopVar e
+  | IntCast.intCast _ i a =>
+    if (← isIntCastInst i) then
+      let some k ← getIntValue? a | toTopVar e
+      return some (.intCast k)
+    else
+      asTopVar e
+  | NatCast.natCast _ i a =>
+    if (← isNatCastInst i) then
+      let some k ← getNatValue? a | toTopVar e
+      return some (.natCast k)
+    else
+      asTopVar e
+  | OfNat.ofNat _ n _ =>
+    let some k ← getNatValue? n | asTopVar e
+    return some (.num k)
+  | _ => toTopVar e
+
+/-- Reify ring expression. -/
+def reify? (e : Expr) (skipVar := true) (gen : Nat := 0) : RingM (Option RingExpr) := do
+  reifyCore? e skipVar gen
+
+/-- Reify non-commutative ring expression. -/
+def ncreify? (e : Expr) (skipVar := true) (gen : Nat := 0) : NonCommRingM (Option RingExpr) := do
+  reifyCore? e skipVar gen
+
+private def reportSAppIssue (e : Expr) : GoalM Unit := do
+  reportIssue! "semiring term with unexpected instance{indentExpr e}"
+
+section
+variable [MonadLiftT GoalM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] [MonadSetTermId m]
+
+/--
+Similar to `reify?` but for `CommSemiring`
+-/
+partial def sreifyCore? (e : Expr) : m (Option SemiringExpr) := do
+  let mkVar (e : Expr) : m Var := do
+    unless (← alreadyInternalized e) do
+      internalize e 0
+    mkSVarCore e
+  let toVar (e : Expr) : m SemiringExpr := do
+    return .var (← mkVar e)
+  let asVar (e : Expr) : m SemiringExpr := do
+    reportSAppIssue e
+    return .var (← mkVar e)
+  let rec go (e : Expr) : m SemiringExpr := do
+    match_expr e with
+    | HAdd.hAdd _ _ _ i a b =>
+      if isSameExpr (← getAddFn').appArg! i then return .add (← go a) (← go b) else asVar e
+    | HMul.hMul _ _ _ i a b =>
+      if isSameExpr (← getMulFn').appArg! i then return .mul (← go a) (← go b) else asVar e
+    | HPow.hPow _ _ _ i a b =>
+      let some k ← getNatValue? b | toVar e
+      if isSameExpr (← getPowFn').appArg! i then return .pow (← go a) k else asVar e
+    | NatCast.natCast _ i a =>
+      if isSameExpr (← getNatCastFn').appArg! i then
+        let some k ← getNatValue? a | toVar e
+        return .num k
+      else
+        asVar e
+    | OfNat.ofNat _ n _ =>
+      let some k ← getNatValue? n | toVar e
+      return .num k
+    | _ => toVar e
+  let toTopVar (e : Expr) : m (Option SemiringExpr) := do
+    return some (← toVar e)
+  let asTopVar (e : Expr) : m (Option SemiringExpr) := do
+    reportSAppIssue e
+    toTopVar e
+  match_expr e with
+  | HAdd.hAdd _ _ _ i a b =>
+    if isSameExpr (← getAddFn').appArg! i then return some (.add (← go a) (← go b)) else asTopVar e
+  | HMul.hMul _ _ _ i a b =>
+    if isSameExpr (← getMulFn').appArg! i then return some (.mul (← go a) (← go b)) else asTopVar e
+  | HPow.hPow _ _ _ i a b =>
+    let some k ← getNatValue? b | return none
+    if isSameExpr (← getPowFn').appArg! i then return some (.pow (← go a) k) else asTopVar e
+  | NatCast.natCast _ i a =>
+    if isSameExpr (← getNatCastFn').appArg! i then
+      let some k ← getNatValue? a | toTopVar e
+      return some (.num k)
+    else
+      asTopVar e
+  | OfNat.ofNat _ n _ =>
+    let some k ← getNatValue? n | asTopVar e
+    return some (.num k)
+  | _ => toTopVar e
+
+end
+
+/-- Reify semiring expression. -/
+def sreify? (e : Expr) : SemiringM (Option SemiringExpr) := do
+  sreifyCore? e
+
+/-- Reify non-commutative semiring expression. -/
+def ncsreify? (e : Expr) : NonCommSemiringM (Option SemiringExpr) := do
+  sreifyCore? e
+
+end  Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean

@@ -7,10 +7,9 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 import Lean.Meta.Tactic.Grind.Arith.Insts
-import Lean.Meta.Sym.Arith.Classify
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym Arith
+
 /--
 Returns the ring id for the given type if there is a `CommRing` instance for it.
 
@@ -20,75 +19,104 @@ This function will also perform sanity-checks
 It also caches the functions representing `+`, `*`, `-`, `^`, and `intCast`.
 -/
 def getCommRingId? (type : Expr) : GoalM (Option Nat) := do
-  if let some result := (← get').typeClassify.find? { expr := type } then
-    let .commRing id := result | return none
-    return some id
+  if let some id? := (← get').typeIdOf.find? { expr := type } then
+    return id?
   else
-    let result ← go?
-    modify' fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
-    return result.toOption
+    let id? ← go?
+    modify' fun s => { s with typeIdOf := s.typeIdOf.insert { expr := type } id? }
+    return id?
 where
-  go? : GoalM ClassifyResult := do
-    let .commRing symId ← classify? type | return .none
+  go? : GoalM (Option Nat) := do
+    let u ← getDecLevel type
+    let commRing := mkApp (mkConst ``Grind.CommRing [u]) type
+    let some commRingInst ← synthInstance? commRing | return none
+    let ringInst := mkApp2 (mkConst ``Grind.CommRing.toRing [u]) type commRingInst
+    let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
+    let commSemiringInst := mkApp2 (mkConst ``Grind.CommRing.toCommSemiring [u]) type semiringInst
+    trace_goal[grind.ring] "new ring: {type}"
+    let charInst? ← getIsCharInst? u type semiringInst
+    let noZeroDivInst? ← getNoZeroDivInst? u type
+    trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
+    let fieldInst? ← synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
+    let powIdentityInst? ← getPowIdentityInst? u type
+    trace_goal[grind.ring] "PowIdentity available: {powIdentityInst?.isSome}"
+    let semiringId? := none
     let id := (← get').rings.size
-    modify' fun s => { s with rings := s.rings.push { symId, id } }
-    return .commRing id
+    let ring : CommRing := {
+      id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
+      commRingInst, charInst?, noZeroDivInst?, fieldInst?, powIdentityInst?,
+    }
+    modify' fun s => { s with rings := s.rings.push ring }
+    return some id
 
 /--
 Returns the ring id for the given type if there is a `Ring` instance for it.
 This function is invoked only when `getCommRingId?` returns `none`.
 -/
 def getNonCommRingId? (type : Expr) : GoalM (Option Nat) := do
-  if let some result := (← get').typeClassify.find? { expr := type } then
-    let .nonCommRing id := result | return none
-    return some id
+  if let some id? := (← get').nctypeIdOf.find? { expr := type } then
+    return id?
   else
-    let result ← go?
-    modify' fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
-    return result.toOption
+    let id? ← go?
+    modify' fun s => { s with nctypeIdOf := s.nctypeIdOf.insert { expr := type } id? }
+    return id?
 where
-  go? : GoalM ClassifyResult := do
-    let .nonCommRing symId ← classify? type | return .none
+  go? : GoalM (Option Nat) := do
+    let u ← getDecLevel type
+    let ring := mkApp (mkConst ``Grind.Ring [u]) type
+    let some ringInst ← synthInstance? ring | return none
+    let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
+    trace_goal[grind.ring] "new ring: {type}"
+    let charInst? ← getIsCharInst? u type semiringInst
     let id := (← get').ncRings.size
-    modify' fun s => { s with ncRings := s.ncRings.push { symId, id } }
-    return .nonCommRing id
+    let ring : Ring := {
+      id, type, u, semiringInst, ringInst, charInst?
+    }
+    modify' fun s => { s with ncRings := s.ncRings.push ring }
+    return some id
 
 private def setCommSemiringId (ringId : Nat) (semiringId : Nat) : GoalM Unit := do
   RingM.run ringId do modifyCommRing fun s => { s with semiringId? := some semiringId }
 
 def getCommSemiringId? (type : Expr) : GoalM (Option Nat) := do
-  if let some result := (← get').typeClassify.find? { expr := type } then
-    let .commSemiring id := result | return .none
-    return some id
+  if let some id? := (← get').stypeIdOf.find? { expr := type } then
+    return id?
   else
-    let result ← go?
-    modify' fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
-    return result.toOption
+    let id? ← go?
+    modify' fun s => { s with stypeIdOf := s.stypeIdOf.insert { expr := type } id? }
+    return id?
 where
-  go? : GoalM ClassifyResult := do
-    let .commSemiring symId ← classify? type | return .none
-    let s ← getCommSemiringOfId symId
-    let r ← getCommRingOfId s.ringId
-    let some ringId ← getCommRingId? r.type
-      | throwError "`grind` unexpected failure, failure to initialize ring{indentExpr r.type}"
+  go? : GoalM (Option Nat) := do
+    let u ← getDecLevel type
+    let commSemiring := mkApp (mkConst ``Grind.CommSemiring [u]) type
+    let some commSemiringInst ← synthInstance? commSemiring | return none
+    let semiringInst := mkApp2 (mkConst ``Grind.CommSemiring.toSemiring [u]) type commSemiringInst
+    let q ← shareCommon (← canon (mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [u]) type semiringInst))
+    let some ringId ← getCommRingId? q
+      | throwError "`grind` unexpected failure, failure to initialize ring{indentExpr q}"
     let id := (← get').semirings.size
-    modify' fun s => { s with semirings := s.semirings.push { symId, id, ringId } }
+    let semiring : CommSemiring := {
+      id, type, ringId, u, semiringInst, commSemiringInst
+    }
+    modify' fun s => { s with semirings := s.semirings.push semiring }
     setCommSemiringId ringId id
-    return .commSemiring id
+    return some id
 
 def getNonCommSemiringId? (type : Expr) : GoalM (Option Nat) := do
-  if let some result := (← get').typeClassify.find? { expr := type } then
-    let .nonCommSemiring id := result | return .none
-    return some id
+  if let some id? := (← get').ncstypeIdOf.find? { expr := type } then
+    return id?
   else
-    let result ← go?
-    modify' fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
-    return result.toOption
+    let id? ← go?
+    modify' fun s => { s with ncstypeIdOf := s.ncstypeIdOf.insert { expr := type } id? }
+    return id?
 where
-  go? : GoalM ClassifyResult := do
-    let .nonCommSemiring symId ← classify? type | return .none
+  go? : GoalM (Option Nat) := do
+    let u ← getDecLevel type
+    let semiring := mkApp (mkConst ``Grind.Semiring [u]) type
+    let some semiringInst ← synthInstance? semiring | return none
     let id := (← get').ncSemirings.size
-    modify' fun s => { s with ncSemirings := s.ncSemirings.push { symId, id } }
-    return .nonCommSemiring id
+    let semiring : Semiring := { id, type, u, semiringInst }
+    modify' fun s => { s with ncSemirings := s.ncSemirings.push semiring }
+    return some id
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean

@@ -5,11 +5,8 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public import Lean.Meta.Tactic.Grind.SynthInstance
-public import Lean.Meta.Sym.Arith.MonadRing
-public import Lean.Meta.Sym.Arith.MonadVar
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 open Sym.Arith
@@ -22,7 +19,6 @@ def incSteps (n : Nat := 1) : GoalM Unit := do
 
 structure RingM.Context where
   ringId : Nat
-  symRingId : Nat
   /--
   If `checkCoeffDvd` is `true`, then when using a polynomial `k*m - p`
   to simplify `.. + k'*m*m_2 + ...`, the substitution is performed IF
@@ -39,34 +35,17 @@ structure RingM.Context where
 /-- We don't want to keep carrying the `RingId` around. -/
 abbrev RingM := ReaderT RingM.Context GoalM
 
-abbrev RingM.run (ringId : Nat) (x : RingM α) : GoalM α := do
-  let s ← get'
-  let symRingId := s.rings[ringId]!.symId
-  x { ringId, symRingId }
+abbrev RingM.run (ringId : Nat) (x : RingM α) : GoalM α :=
+  x { ringId }
 
 abbrev getRingId : RingM Nat :=
   return (← read).ringId
 
-abbrev getSymRingId : RingM Nat :=
-  return (← read).symRingId
+instance : MonadCanon RingM where
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
 
 protected def RingM.getCommRing : RingM CommRing := do
-  let s ← getArithState
-  let symRingId ← getSymRingId
-  if h : symRingId < s.rings.size then
-    return s.rings[symRingId]
-  else
-    throwError "`grind` internal error, invalid ringId"
-
-protected def RingM.modifyCommRing (f : CommRing → CommRing) : RingM Unit := do
-  let symRingId ← getSymRingId
-  modifyArithState fun s => { s with rings := s.rings.modify symRingId f }
-
-instance : MonadCommRing RingM where
-  getCommRing := RingM.getCommRing
-  modifyCommRing := RingM.modifyCommRing
-
-def getCommRingEntry : RingM CommRingEntry := do
   let s ← get'
   let ringId ← getRingId
   if h : ringId < s.rings.size then
@@ -74,10 +53,14 @@ def getCommRingEntry : RingM CommRingEntry := do
   else
     throwError "`grind` internal error, invalid ringId"
 
-def modifyCommRingEntry (f : CommRingEntry → CommRingEntry) : RingM Unit := do
+protected def RingM.modifyCommRing (f : CommRing → CommRing) : RingM Unit := do
   let ringId ← getRingId
   modify' fun s => { s with rings := s.rings.modify ringId f }
 
+instance : MonadCommRing RingM where
+  getCommRing := RingM.getCommRing
+  modifyCommRing := RingM.modifyCommRing
+
 abbrev withCheckCoeffDvd (x : RingM α) : RingM α :=
   withReader (fun ctx => { ctx with checkCoeffDvd := true }) x
 
@@ -129,14 +112,17 @@ def isField : RingM Bool :=
   return (← getCommRing).fieldInst?.isSome
 
 def isQueueEmpty : RingM Bool :=
-  return (← getCommRingEntry).queue.isEmpty
+  return (← getCommRing).queue.isEmpty
 
 def getNext? : RingM (Option EqCnstr) := do
-  let some c := (← getCommRingEntry).queue.min? | return none
-  modifyCommRingEntry fun s => { s with queue := s.queue.erase c }
+  let some c := (← getCommRing).queue.min? | return none
+  modifyCommRing fun s => { s with queue := s.queue.erase c }
   incSteps
   return some c
 
+class MonadSetTermId (m : Type → Type) where
+  setTermId : Expr → m Unit
+
 def setTermRingId (e : Expr) : RingM Unit := do
   let ringId ← getRingId
   if let some ringId' ← getTermRingId? e then
@@ -145,25 +131,23 @@ def setTermRingId (e : Expr) : RingM Unit := do
     return ()
   modify' fun s => { s with exprToRingId := s.exprToRingId.insert { expr := e } ringId }
 
-def mkVar (e : Expr) (gen : Nat) : RingM Var := do
-  unless (← alreadyInternalized e) do
-    internalize e gen
-  let s ← getCommRingEntry
+def mkVarCore [MonadLiftT GoalM m] [Monad m] [MonadRing m] [MonadSetTermId m] (e : Expr) : m Var := do
+  let s ← getRing
   if let some var := s.varMap.find? { expr := e } then
     return var
   let var : Var := s.vars.size
-  modifyCommRingEntry fun s => { s with
+  modifyRing fun s => { s with
     vars       := s.vars.push e
     varMap     := s.varMap.insert { expr := e } var
   }
-  setTermRingId e
+  MonadSetTermId.setTermId e
   ringExt.markTerm e
   return var
 
-instance : MonadMkVar RingM where
-  mkVar := CommRing.mkVar
+instance : MonadSetTermId RingM where
+  setTermId e := setTermRingId e
 
-instance : MonadGetVar RingM where
-  getVar x := return (← getCommRingEntry).vars[x]!
+def mkVar (e : Expr) : RingM Var :=
+  mkVarCore e
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean

@@ -121,7 +121,7 @@ def _root_.Lean.Grind.CommRing.Mon.findInvNumeralVar? (m : Mon) : RingM (Option
   match m with
   | .unit => return none
   | .mult pw m =>
-    let e := (← getCommRingEntry).vars[pw.x]!
+    let e := (← getRing).vars[pw.x]!
     let_expr Inv.inv _ _ a := e | m.findInvNumeralVar?
     let_expr OfNat.ofNat _ n _ := a | m.findInvNumeralVar?
     let some n ← getNatValue? n | m.findInvNumeralVar?

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean

@@ -6,44 +6,46 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
-public import Lean.Meta.Sym.Arith.MonadSemiring
-public import Lean.Meta.Sym.Arith.MonadVar
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadSemiring
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 open Sym.Arith
 
 structure SemiringM.Context where
-  semiringId    : Nat
-  symSemiringId : Nat
+  semiringId : Nat
 
 abbrev SemiringM := ReaderT SemiringM.Context GoalM
 
-abbrev SemiringM.run (semiringId : Nat) (x : SemiringM α) : GoalM α := do
-  let s ← get'
-  let symSemiringId := s.semirings[semiringId]!.symId
-  x { semiringId, symSemiringId }
+abbrev SemiringM.run (semiringId : Nat) (x : SemiringM α) : GoalM α :=
+  x { semiringId }
 
 abbrev getSemiringId : SemiringM Nat :=
   return (← read).semiringId
 
+instance : MonadCanon SemiringM where
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
+
 protected def SemiringM.getCommSemiring : SemiringM CommSemiring := do
-  let s ← getArithState
-  let semiringId := (← read).symSemiringId
+  let s ← get'
+  let semiringId ← getSemiringId
   if h : semiringId < s.semirings.size then
     return s.semirings[semiringId]
   else
     throwError "`grind` internal error, invalid semiringId"
 
 @[inline] protected def SemiringM.modifyCommSemiring (f : CommSemiring → CommSemiring) : SemiringM Unit := do
-  let semiringId := (← read).symSemiringId
-  modifyArithState fun s => { s with semirings := s.semirings.modify semiringId f }
+  let semiringId ← getSemiringId
+  modify' fun s => { s with semirings := s.semirings.modify semiringId f }
 
 instance : MonadCommSemiring SemiringM where
   getCommSemiring := SemiringM.getCommSemiring
   modifyCommSemiring := SemiringM.modifyCommSemiring
 
 protected def SemiringM.getCommRing : SemiringM CommRing := do
-  let s ← getArithState
+  let s ← get'
   let ringId := (← getCommSemiring).ringId
   if h : ringId < s.rings.size then
     return s.rings[ringId]
@@ -52,59 +54,12 @@ protected def SemiringM.getCommRing : SemiringM CommRing := do
 
 protected def SemiringM.modifyCommRing (f : CommRing → CommRing) : SemiringM Unit := do
   let ringId := (← getCommSemiring).ringId
-  modifyArithState fun s => { s with rings := s.rings.modify ringId f }
+  modify' fun s => { s with rings := s.rings.modify ringId f }
 
 instance : MonadCommRing SemiringM where
  getCommRing := SemiringM.getCommRing
  modifyCommRing := SemiringM.modifyCommRing
 
-def getCommSemiringEntry : SemiringM CommSemiringEntry := do
-  let s ← get'
-  let semiringId := (← read).semiringId
-  if h : semiringId < s.semirings.size then
-    return s.semirings[semiringId]
-  else
-    throwError "`grind` internal error, invalid semiringId"
-
-def modifyCommSemiringEntry (f : CommSemiringEntry → CommSemiringEntry) : SemiringM Unit := do
-  let semiringId := (← read).semiringId
-  modify' fun s => { s with semirings := s.semirings.modify semiringId f }
-
-def getTermSemiringId? (e : Expr) : GoalM (Option Nat) := do
-  return (← get').exprToSemiringId.find? { expr := e }
-
-def setTermSemiringId (e : Expr) : SemiringM Unit := do
-  let semiringId ← getSemiringId
-  if let some semiringId' ← getTermSemiringId? e then
-    unless semiringId' == semiringId do
-      reportIssue! "expression in two different semirings{indentExpr e}"
-    return ()
-  modify' fun s => { s with exprToSemiringId := s.exprToSemiringId.insert { expr := e } semiringId }
-
-/-- Similar to `mkVarCore` but for `Semiring`s -/
-def mkSVar (e : Expr) (gen : Nat) : SemiringM Var := do
-  unless (← alreadyInternalized e) do
-    internalize e gen
-  let s ← getCommSemiringEntry
-  if let some var := s.varMap.find? { expr := e } then
-    return var
-  let var : Var := s.vars.size
-  modifyCommSemiringEntry fun s => { s with
-    vars       := s.vars.push e
-    varMap     := s.varMap.insert { expr := e } var
-  }
-  setTermSemiringId e
-  ringExt.markTerm e
-  return var
-
-instance : MonadMkVar SemiringM where
-  mkVar := mkSVar
-
-instance : MonadGetVar SemiringM where
-  getVar x := return (← getCommSemiringEntry).vars[x]!
-
-
-/-
 def getToQFn : SemiringM Expr := do
   let s ← getCommSemiring
   if let some toQFn := s.toQFn? then return toQFn
@@ -160,6 +115,37 @@ def getNatCastFn' : m Expr := do
 
 end
 
+def getTermSemiringId? (e : Expr) : GoalM (Option Nat) := do
+  return (← get').exprToSemiringId.find? { expr := e }
+
+def setTermSemiringId (e : Expr) : SemiringM Unit := do
+  let semiringId ← getSemiringId
+  if let some semiringId' ← getTermSemiringId? e then
+    unless semiringId' == semiringId do
+      reportIssue! "expression in two different semirings{indentExpr e}"
+    return ()
+  modify' fun s => { s with exprToSemiringId := s.exprToSemiringId.insert { expr := e } semiringId }
+
+instance : MonadSetTermId SemiringM where
+  setTermId e := setTermSemiringId e
+
+/-- Similar to `mkVarCore` but for `Semiring`s -/
+def mkSVarCore [MonadLiftT GoalM m] [Monad m] [MonadSemiring m] [MonadSetTermId m] (e : Expr) : m Var := do
+  let s ← getSemiring
+  if let some var := s.varMap.find? { expr := e } then
+    return var
+  let var : Var := s.vars.size
+  modifySemiring fun s => { s with
+    vars       := s.vars.push e
+    varMap     := s.varMap.insert { expr := e } var
+  }
+  MonadSetTermId.setTermId e
+  ringExt.markTerm e
+  return var
+
+def mkSVar (e : Expr) : SemiringM Var := do
+  mkSVarCore e
+
 def _root_.Lean.Grind.CommRing.Expr.denoteAsRingExpr (e : SemiringExpr) : SemiringM Expr := do
   shareCommon (← go e)
 where
@@ -172,6 +158,4 @@ where
   | .pow a k => return mkApp2 (← getPowFn) (← go a) (toExpr k)
   | .neg .. | .sub .. | .intCast .. => unreachable!
 
--/
-
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean

@@ -7,7 +7,6 @@ module
 prelude
 public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Sym.Arith.Types
 import Lean.Meta.Sym.Arith.Poly
 public section
 
@@ -145,9 +144,17 @@ structure DiseqCnstr where
   ofSemiring? : Option (SemiringExpr × SemiringExpr)
 
 /-- Shared state for non-commutative and commutative semirings. -/
-structure SemiringEntry where
-  symId          : Nat
+structure Semiring where
   id             : Nat
+  type           : Expr
+  /-- Cached `getDecLevel type` -/
+  u              : Level
+  /-- `Semiring` instance for `type` -/
+  semiringInst   : Expr
+  addFn?         : Option Expr := none
+  mulFn?         : Option Expr := none
+  powFn?         : Option Expr := none
+  natCastFn?     : Option Expr := none
   /-- Mapping from Lean expressions to their representations as `SemiringExpr` -/
   denote         : PHashMap ExprPtr SemiringExpr := {}
   /--
@@ -160,9 +167,25 @@ structure SemiringEntry where
   deriving Inhabited
 
 /-- Shared state for non-commutative and commutative rings. -/
-structure RingEntry where
-  symId          : Nat
+structure Ring where
   id             : Nat
+  type           : Expr
+  /-- Cached `getDecLevel type` -/
+  u              : Level
+  /-- `Ring` instance for `type` -/
+  ringInst       : Expr
+  /-- `Semiring` instance for `type` -/
+  semiringInst   : Expr
+  /-- `IsCharP` instance for `type` if available. -/
+  charInst?      : Option (Expr × Nat)
+  addFn?         : Option Expr := none
+  mulFn?         : Option Expr := none
+  subFn?         : Option Expr := none
+  negFn?         : Option Expr := none
+  powFn?         : Option Expr := none
+  intCastFn?     : Option Expr := none
+  natCastFn?     : Option Expr := none
+  one?           : Option Expr := none
   /--
   Mapping from variables to their denotations.
   Remark each variable can be in only one ring.
@@ -175,7 +198,24 @@ structure RingEntry where
   deriving Inhabited
 
 /-- State for each `CommRing` processed by this module. -/
-structure CommRingEntry extends RingEntry where
+structure CommRing extends Ring where
+  /-- Inverse if `fieldInst?` is `some inst` -/
+  invFn?         : Option Expr := none
+  /--
+  If this is a `OfSemiring.Q α` ring, this field contain the
+  `semiringId` for `α`.
+  -/
+  semiringId?    : Option Nat
+  /-- `CommSemiring` instance for `type` -/
+  commSemiringInst   : Expr
+  /-- `CommRing` instance for `type` -/
+  commRingInst   : Expr
+  /-- `NoNatZeroDivisors` instance for `type` if available. -/
+  noZeroDivInst? : Option Expr
+  /-- `Field` instance for `type` if available. -/
+  fieldInst?     : Option Expr
+  /-- `PowIdentity` instance, the synthesized `CommSemiring` instance, and exponent `p` if available. -/
+  powIdentityInst? : Option (Expr × Expr × Nat) := none
   /-- `denoteEntries` is `denote` as a `PArray` for deterministic traversal. -/
   denoteEntries  : PArray (Expr × RingExpr) := {}
   /-- Next unique id for `EqCnstr`s. -/
@@ -214,36 +254,62 @@ structure CommRingEntry extends RingEntry where
 State for each `CommSemiring` processed by this module.
 Recall that `CommSemiring` are processed using the envelop `OfCommSemiring.Q`
 -/
-structure CommSemiringEntry extends SemiringEntry where
-  /-- Id for `CommRingEntry` associated with `OfCommSemiring.Q` -/
-  ringId : Nat
+structure CommSemiring extends Semiring where
+  /-- Id for `OfCommSemiring.Q` -/
+  ringId         : Nat
+  /-- `CommSemiring` instance for `type` -/
+  commSemiringInst   : Expr
+  /-- `AddRightCancel` instance for `type` if available. -/
+  addRightCancelInst? : Option (Option Expr) := none
+  toQFn?         : Option Expr := none
   deriving Inhabited
 
-export Sym.Arith (ClassifyResult)
-
 /-- State for all `CommRing` types detected by `grind`. -/
 structure State where
   /--
   Commutative rings.
   We expect to find a small number of rings in a given goal. Thus, using `Array` is fine here.
   -/
-  rings : Array CommRingEntry := {}
-  /-- Commutative semirings. We support them using the envelope `OfCommRing.Q` -/
-  semirings : Array CommSemiringEntry := {}
-  /-- Non commutative rings. -/
-  ncRings : Array RingEntry := {}
-  /-- Non commutative semirings. -/
-  ncSemirings : Array SemiringEntry := {}
-  /-- Mapping from types to their classification result. Caches failures as `.none`. -/
-  typeClassify : PHashMap ExprPtr ClassifyResult := {}
+  rings : Array CommRing := {}
+  /--
+  Mapping from types to its "ring id". We cache failures using `none`.
+  `typeIdOf[type]` is `some id`, then `id < rings.size`. -/
+  typeIdOf : PHashMap ExprPtr (Option Nat) := {}
   /- Mapping from expressions/terms to their ring ids. -/
   exprToRingId : PHashMap ExprPtr Nat := {}
-  /- Mapping from expressions/terms to their semiring ids. -/
+  /-- Commutative semirings. We support them using the envelope `OfCommRing.Q` -/
+  semirings : Array CommSemiring := {}
+  /--
+  Mapping from types to its "semiring id". We cache failures using `none`.
+  `stypeIdOf[type]` is `some id`, then `id < semirings.size`.
+  If a type is in this map, it is not in `typeIdOf`.
+  -/
+  stypeIdOf : PHashMap ExprPtr (Option Nat) := {}
+  /-
+  Mapping from expressions/terms to their semiring ids.
+  If an expression is in this map, it is not in `exprToRingId`.
+  -/
   exprToSemiringId : PHashMap ExprPtr Nat := {}
+  /--
+  Non commutative rings.
+  -/
+  ncRings : Array Ring := {}
   /- Mapping from expressions/terms to their (non-commutative) ring ids. -/
   exprToNCRingId : PHashMap ExprPtr Nat := {}
+  /--
+  Mapping from types to its "ring id". We cache failures using `none`.
+  `nctypeIdOf[type]` is `some id`, then `id < ncRings.size`. -/
+  nctypeIdOf : PHashMap ExprPtr (Option Nat) := {}
+  /--
+  Non commutative semirings.
+  -/
+  ncSemirings : Array Semiring := {}
   /- Mapping from expressions/terms to their (non-commutative) semiring ids. -/
   exprToNCSemiringId : PHashMap ExprPtr Nat := {}
+  /--
+  Mapping from types to its "semiring id". We cache failures using `none`.
+  `ncstypeIdOf[type]` is `some id`, then `id < ncSemirings.size`. -/
+  ncstypeIdOf : PHashMap ExprPtr (Option Nat) := {}
   steps := 0
   deriving Inhabited
 

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean

@@ -10,12 +10,11 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
-import Lean.Meta.Sym.Arith.Reify
-import Lean.Meta.Sym.Arith.DenoteExpr
 public section
 namespace Lean.Meta.Grind.Arith.Cutsat
-open Sym Arith
 /-!
 CommRing interface for cutsat. We use it to normalize nonlinear polynomials.
 -/
@@ -46,9 +45,9 @@ def _root_.Int.Linear.Poly.normCommRing? (p : Poly) : GoalM (Option (CommRing.Ri
     -- Internalized operators instead of `mkIntMul` and `mkIntAdd`
     let e ← shareCommon (← canon e)
     let gen ← p.getGeneration
-    let some re ← reifyRing? e (gen := gen) | return none
+    let some re ← CommRing.reify? e (gen := gen) | return none
     let some p' ← re.toPolyM? | return none
-    let e' ← denotePoly p'
+    let e' ← p'.denoteExpr
     let e' ← preprocessLight e'
     /-
     **Note**: We are reusing the `IntModule` virtual parent.

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -174,7 +174,7 @@ private def mkContext
 private def mkRingContext (h : Expr) : ProofM Expr := do
   unless (← get').usedCommRing do return h
   let some ringId ← getIntRingId? | return h
-  let vars ← CommRing.RingM.run ringId do return (← CommRing.getCommRingEntry).vars
+  let vars ← CommRing.RingM.run ringId do return (← CommRing.getRing).vars
   let usedVars     := collectMapVars (← get).ringPolyDecls (·.collectVars) >> collectMapVars (← get).ringExprDecls (·.collectVars) <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'

src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean

@@ -8,7 +8,7 @@ prelude
 import Lean.Meta.Tactic.Grind.Arith.Util
 public import Lean.Meta.Tactic.Grind.Arith.Linear.Util
 import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Sym.Arith.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public section
 namespace Lean.Meta.Grind.Arith.Linear
 /-!
@@ -69,9 +69,7 @@ private def denoteNum (k : Int) : LinearM Expr := do
 def _root_.Lean.Grind.CommRing.Poly.denoteAsIntModuleExpr (p : Grind.CommRing.Poly) : LinearM Expr := do
   match p with
   | .num k => denoteNum k
-  | .add _k _m _p =>
-    -- TODO: FIX
-    return default -- mkApp2 (← getStruct).addFn (mkApp2 (← getStruct).zsmulFn (mkIntLit k) (← m.denoteExpr)) (← denoteAsIntModuleExpr p)
+  | .add k m p => return mkApp2 (← getStruct).addFn (mkApp2 (← getStruct).zsmulFn (mkIntLit k) (← m.denoteExpr)) (← denoteAsIntModuleExpr p)
 
 def _root_.Lean.Grind.CommRing.Poly.toIntModuleExpr (p : Grind.CommRing.Poly) (generation := 0) : LinearM Expr := do
   let e ← p.denoteAsIntModuleExpr

src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean

@@ -6,13 +6,12 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.Linear.Den
 import Lean.Meta.Tactic.Grind.Arith.Linear.StructId
 import Lean.Meta.Tactic.Grind.Arith.Linear.Reify
 import Lean.Meta.Tactic.Grind.Arith.Linear.Proof
-import Lean.Meta.Sym.Arith.Reify
 namespace Lean.Meta.Grind.Arith.Linear
-open Sym Arith
 
 def isInstOf (fn? : Option Expr) (inst : Expr) : Bool :=
   if let some fn := fn? then
@@ -40,9 +39,8 @@ public def IneqCnstr.assert (c : IneqCnstr) : LinearM Unit := do
       resetAssignmentFrom x
 
 def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue : Bool) : LinearM Unit := do
-  let gen ← getGeneration e
-  let some lhs ← withRingM <| reifyRing? lhs (skipVar := false) (gen := gen) | return ()
-  let some rhs ← withRingM <| reifyRing? rhs (skipVar := false) (gen := gen) | return ()
+  let some lhs ← withRingM <| CommRing.reify? lhs (skipVar := false) | return ()
+  let some rhs ← withRingM <| CommRing.reify? rhs (skipVar := false) | return ()
   let generation ← getGeneration e
   if eqTrue then
     let p := (lhs.sub rhs).toPoly

src/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.lean

@@ -9,7 +9,7 @@ public import Lean.Meta.Tactic.Grind.Arith.Linear.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.Linear
-open Sym.Arith (MonadCanon MonadRing)
+open Sym.Arith (MonadCanon)
 
 def get' : GoalM State := do
   linearExt.getState
@@ -52,10 +52,8 @@ instance : MonadGetStruct LinearM where
 open CommRing
 
 def getRingCore? (ringId? : Option Nat) : GoalM (Option Ring) := do
-  let some _ringId := ringId? | return none
-  -- TODO: FIX
-  -- RingM.run ringId do return some (← getRing)
-  return none
+  let some ringId := ringId? | return none
+  RingM.run ringId do return some (← getRing)
 
 def throwNotRing : LinearM α :=
   throwError "`grind linarith` internal error, structure is not a ring"
@@ -77,10 +75,9 @@ def LinearM.getRing : LinearM Ring := do
 
 instance : MonadRing LinearM where
   getRing := LinearM.getRing
-  modifyRing _f := do
-    let some _ringId := (← getStruct).ringId? | throwNotCommRing
-    -- RingM.run ringId do modifyRing f
-    -- TODO: FIX
+  modifyRing f := do
+    let some ringId := (← getStruct).ringId? | throwNotCommRing
+    RingM.run ringId do modifyRing f
 
 def withRingM (x : RingM α) : LinearM α := do
   let some ringId := (← getStruct).ringId?

src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean

@@ -123,8 +123,6 @@ private def mkContext (h : Expr) : ProofM Expr := do
 
 private def mkRingContext (h : Expr) : ProofM Expr := do
   unless (← isCommRing) do return h
-  throwError "NIY"
-/-
   let ring ← withRingM do CommRing.getRing
   let vars := ring.vars
   let ringVarDecls := (← get).ringVarDecls
@@ -146,7 +144,6 @@ private def mkRingContext (h : Expr) : ProofM Expr := do
     return .letE `rctx ctxType ctxVal h (nondep := false)
   else
     return h
--/
 
 private abbrev withProofContext (x : ProofM Expr) : LinearM Expr := do
   let ctx := mkFVar (← mkFreshFVarId)

src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean

@@ -6,14 +6,13 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.Linear.Den
+import Lean.Meta.Tactic.Grind.Arith.Linear.Reify
 import Lean.Meta.Tactic.Grind.Arith.Linear.IneqCnstr
 import Lean.Meta.Tactic.Grind.Arith.Linear.Proof
-import Lean.Meta.Tactic.Grind.Arith.Linear.Reify
-import Lean.Meta.Sym.Arith.Reify
 public section
 namespace Lean.Meta.Grind.Arith.Linear
-open Sym Arith
 
 private def _root_.Lean.Grind.Linarith.Poly.substVar (p : Poly) : LinearM (Option (Var × EqCnstr × Poly)) := do
   let some (a, x, c) ← p.findVarToSubst | return none
@@ -48,8 +47,8 @@ private def inSameStruct? (a b : Expr) : GoalM (Option Nat) := do
   return structId
 
 private def processNewCommRingEq' (a b : Expr) : LinearM Unit := do
-  let some lhs ← withRingM <| reifyRing? a (skipVar := false) (gen := (← getGeneration a)) | return ()
-  let some rhs ← withRingM <| reifyRing? b (skipVar := false) (gen := (← getGeneration a)) | return ()
+  let some lhs ← withRingM <| CommRing.reify? a (skipVar := false) | return ()
+  let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return ()
   let generation := max (← getGeneration a) (← getGeneration b)
   let p := (lhs.sub rhs).toPoly
   let c : RingEqCnstr := { p, h := .core a b lhs rhs }
@@ -295,8 +294,8 @@ def processNewEq (a b : Expr) : GoalM Unit := do
       processNewNatModuleEq a b
 
 private def processNewCommRingDiseq (a b : Expr) : LinearM Unit := do
-  let some lhs ← withRingM <| reifyRing? a (skipVar := false) (← getGeneration a) | return ()
-  let some rhs ← withRingM <| reifyRing? b (skipVar := false) (← getGeneration b) | return ()
+  let some lhs ← withRingM <| CommRing.reify? a (skipVar := false) | return ()
+  let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return ()
   let p := (lhs.sub rhs).toPoly
   let c : RingDiseqCnstr := { p, h := .core a b lhs rhs }
   let c ← c.cleanupDenominators

src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean

@@ -14,7 +14,6 @@ import Lean.Meta.Tactic.Grind.Arith.Insts
 import Init.Grind.Module.Envelope
 public section
 namespace Lean.Meta.Grind.Arith.Linear
-open Sym Arith
 
 private def preprocess (e : Expr) : GoalM Expr := do
   shareCommon (← canon e)
@@ -67,7 +66,7 @@ private def isCutsatType (type : Expr) : GoalM Bool := do
 
 private def getCommRingInst? (ringId? : Option Nat) : GoalM (Option Expr) := do
   let some ringId := ringId? | return none
-  return some (← CommRing.RingM.run ringId do return (← getCommRing).commRingInst)
+  return some (← CommRing.RingM.run ringId do return (← CommRing.getCommRing).commRingInst)
 
 private def mkRingInst? (u : Level) (type : Expr) (commRingInst? : Option Expr) : GoalM (Option Expr) := do
   if let some commRingInst := commRingInst? then

src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean

@@ -12,7 +12,7 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
 public import Lean.Meta.Tactic.Grind.PropagatorAttr
 public section
 namespace Lean.Meta.Grind.Arith
-open Sym Arith
+
 /-!
 This file defines propagators for `Nat` operators that have simprocs associated with them, but do not
 have support in satellite solvers. The goal is to workaround a nasty interaction between

src/Lean/Meta/Tactic/Grind/Order/Internalize.lean

@@ -10,6 +10,8 @@ import Init.Data.Int.OfNat
 import Init.Grind.Module.Envelope
 import Init.Grind.Order
 import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 import Lean.Meta.Tactic.Grind.Order.StructId

src/Lean/Meta/Tactic/Grind/Order/StructId.lean

@@ -11,7 +11,6 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 public section
 namespace Lean.Meta.Grind.Order
-open Sym Arith
 
 private def preprocess (e : Expr) : GoalM Expr := do
   shareCommon (← canon e)

src/Lean/Meta/WrapInstance.lean

@@ -9,8 +9,8 @@ prelude
 public import Lean.Meta.Closure
 public import Lean.Meta.SynthInstance
 public import Lean.Meta.CtorRecognizer
-
-public section
+public import Lean.Meta.AppBuilder
+import Lean.Structure
 
 /-!
 # Instance Wrapping
@@ -25,22 +25,30 @@ Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
 `wrapInstance` constructs a result instance as follows, executing all steps at
 `instances` transparency:
 
-1. If `I'` is not a class, return `i` unchanged.
+1. If `I'` is not a class application, return `i` unchanged.
 2. If `I'` is a proposition, wrap `i` in an auxiliary theorem of type `I'` and return it
    (controlled by `backward.inferInstanceAs.wrap.instances`).
 3. Reduce `i` to whnf.
-4. If `i` is not a constructor application: if the type of `i` is already defeq to `I'`,
+4. If `i` is not a constructor application: if `I` is already defeq to `I'`,
    return `i`; otherwise wrap it in an auxiliary definition of type `I'` and return it
    (controlled by `backward.inferInstanceAs.wrap.instances`).
-5. Otherwise, for `i = ctor a₁ ... aₙ` with `ctor : C ?p₁ ... ?pₙ`:
-   - Unify `C ?p₁ ... ?pₙ` with `I'`.
-   - Return a new application `ctor a₁' ... aₙ' : I'` where each `aᵢ'` is constructed as:
+5. Otherwise, if `i` is an application of `ctor` of class `C`:
+   - Unify the conclusion of the type of `ctor` with `I'` to obtain adjusted field type `Fᵢ'` for
+     each field.
+   - Return a new application `ctor ... : I'` where the fields are adjusted as follows:
      - If the field type is a proposition: assign directly if types are defeq, otherwise
        wrap in an auxiliary theorem.
-     - If the field type is a class: first try to reuse an existing synthesized instance
-       for the target type (controlled by `backward.inferInstanceAs.wrap.reuseSubInstances`);
-       if that fails, recurse with source instance `aᵢ` and expected type `?pᵢ`.
-     - Otherwise (data field): assign directly if types are defeq, otherwise wrap in an
+     - If the field is a parent field (subobject) `p : P`: first try to reuse an existing
+       instance that can be synthesized for `P` (controlled by
+       `backward.inferInstanceAs.wrap.reuseSubInstances`) in order to preserve defeqs; if that
+       fails, recurse.
+     - If it is a field of a flattened parent class `C'` and
+       `backward.inferInstanceAs.wrap.reuseSubInstances` is true, try synthesizing an instance of
+       `C'` for `I'` and if successful, use the corresponding projection of the found instance in
+       order to preserve defeqs; otherwise, continue.
+       - Specifically, construct the chain of base projections from `C` to `C'` applied to `_ : I'`
+         and infer its type to obtain an appropriate application of `C'` for the instance search.
+     - Otherwise (non-inherited data field): assign directly if types are defeq, otherwise wrap in an
        auxiliary definition to fix the type (controlled by `backward.inferInstanceAs.wrap.data`).
 
 ## Options
@@ -56,34 +64,36 @@ Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
 
 namespace Lean.Meta
 
-register_builtin_option backward.inferInstanceAs.wrap : Bool := {
+public register_builtin_option backward.inferInstanceAs.wrap : Bool := {
   defValue := true
   descr := "wrap instance bodies in `inferInstanceAs` and the default `deriving` handler"
 }
 
-register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
+public register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
   defValue := true
   descr := "when recursing into sub-instances, reuse existing instances for the target type instead of re-wrapping them, which can be important to avoid non-defeq instance diamonds"
 }
 
-register_builtin_option backward.inferInstanceAs.wrap.instances : Bool := {
+public register_builtin_option backward.inferInstanceAs.wrap.instances : Bool := {
   defValue := true
   descr := "wrap non-reducible instances in auxiliary definitions to fix their types"
 }
 
-register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
+public register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
   defValue := true
   descr := "wrap data fields in auxiliary definitions to fix their types"
 }
 
 builtin_initialize registerTraceClass `Meta.wrapInstance
 
+open Meta
+
 /--
 Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
 Non-instance-implicit arguments are assigned from the original application's arguments.
 If the function is over-applied, extra arguments are preserved.
 -/
-def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
+public def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
   let fn := type.getAppFn
   let args := type.getAppArgs
   let (mvars, bis, _) ← forallMetaTelescope (← inferType fn)
@@ -93,11 +103,38 @@ def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
   let args := mvars ++ args.drop mvars.size
   instantiateMVars (mkAppN fn args)
 
+partial def getFieldOrigin (structName field : Name) : MetaM (Name × StructureFieldInfo) := do
+  let env ← getEnv
+  for parent in getStructureParentInfo env structName do
+    if (findField? env parent.structName field).isSome then
+      return ← getFieldOrigin parent.structName field
+  let some fi := getFieldInfo? env structName field
+    | throwError "no such field {field} in {structName}"
+  return (structName, fi)
+
+/-- Projects application of a structure type to corresponding application of a parent structure. -/
+def getParentStructType? (structName parentStructName : Name) (structType : Expr) : MetaM (Option Expr) := OptionT.run do
+  let env ← getEnv
+  let some path := getPathToBaseStructure? env parentStructName structName | failure
+  withLocalDeclD `self structType fun self => do
+    let proj ← path.foldlM (init := self) fun e projFn => do
+      let ty ← whnf (← inferType e)
+      let .const _ us := ty.getAppFn
+        | trace[Meta.wrapInstance] "could not reduce type `{ty}`"
+          failure
+      let params := ty.getAppArgs
+      pure <| mkApp (mkAppN (.const projFn us) params) e
+    let projTy ← whnf <| ← inferType proj
+    if projTy.containsFVar self.fvarId! then
+      trace[Meta.wrapInstance] "parent type depends on instance fields{indentExpr projTy}"
+      failure
+    return projTy
+
 /--
 Wrap an instance value so its type matches the expected type exactly.
 See the module docstring for the full algorithm specification.
 -/
-partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
+public partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
     (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
   withTraceNode `Meta.wrapInstance
       (fun _ => return m!"type: {expectedType}") do
@@ -155,8 +192,10 @@ partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
           else
             trace[Meta.wrapInstance] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
             mvarId.assign (← mkAuxTheorem argExpectedType arg (zetaDelta := true))
+          continue
+
         -- Recurse into instance arguments of the constructor
-        else if (← isClass? argExpectedType).isSome then
+        if (← isClass? argExpectedType).isSome then
           if backward.inferInstanceAs.wrap.reuseSubInstances.get (← getOptions) then
             -- Reuse existing instance for the target type if any. This is especially important when recursing
             -- as it guarantees subinstances of overlapping instances are defeq under more than just
@@ -170,22 +209,35 @@ partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
 
           mvarId.assign (← wrapInstance arg argExpectedType (compile := compile)
             (logCompileErrors := logCompileErrors) (isMeta := isMeta))
-        else
-          -- For data fields, assign directly or wrap in aux def to fix types.
-          if backward.inferInstanceAs.wrap.data.get (← getOptions) then
-            let argType ← inferType arg
-            if ← isDefEq argExpectedType argType then
-              mvarId.assign arg
-            else
-              let name ← mkAuxDeclName
-              mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
-              setInlineAttribute name
-              if isMeta then modifyEnv (markMeta · name)
-              if compile then
-                compileDecls (logErrors := logCompileErrors) #[name]
-              enableRealizationsForConst name
-          else
-            mvarId.assign arg
-      return mkAppN f (← mvars.mapM instantiateMVars)
+          continue
 
-end Lean.Meta
+        if backward.inferInstanceAs.wrap.reuseSubInstances.get (← getOptions) then
+          let (baseClassName, fieldInfo) ← getFieldOrigin className mvarDecl.userName
+          if baseClassName != className then
+            trace[Meta.wrapInstance] "found inherited field `{mvarDecl.userName}` from parent `{baseClassName}`"
+            if let some baseClassType ← getParentStructType? className baseClassName expectedType then
+              try
+                if let .some existingBaseClassInst ← trySynthInstance baseClassType then
+                  trace[Meta.wrapInstance] "using projection of existing instance `{existingBaseClassInst}`"
+                  mvarId.assign (← mkProjection existingBaseClassInst fieldInfo.fieldName)
+                  continue
+                trace[Meta.wrapInstance] "did not find existing instance for `{baseClassName}`"
+              catch e =>
+                trace[Meta.wrapInstance] "error when attempting to reuse existing instance for `{baseClassName}`: {e.toMessageData}"
+
+        -- For data fields, assign directly or wrap in aux def to fix types.
+        if backward.inferInstanceAs.wrap.data.get (← getOptions) then
+          let argType ← inferType arg
+          if ← isDefEq argExpectedType argType then
+            mvarId.assign arg
+          else
+            let name ← mkAuxDeclName
+            mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
+            setInlineAttribute name
+            if isMeta then modifyEnv (markMeta · name)
+            if compile then
+              compileDecls (logErrors := logCompileErrors) #[name]
+            enableRealizationsForConst name
+        else
+          mvarId.assign arg
+      return mkAppN f (← mvars.mapM instantiateMVars)

src/Lean/Parser/Basic.lean

@@ -1115,11 +1115,6 @@ def symbolNoAntiquot (sym : String) : Parser :=
   { info := symbolInfo sym
     fn   := symbolFn sym }
 
-def checkTailNoWs (prev : Syntax) : Bool :=
-  match prev.getTailInfo with
-  | .original _ _ trailing _ => trailing.stopPos == trailing.startPos
-  | _                        => false
-
 /-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
     parsing local tokens that have not been added to the token table (but may have
     been so by some unrelated code).
@@ -1168,13 +1163,18 @@ partial def strAux (sym : String) (errorMsg : String) (j : String.Pos.Raw) :Pars
       else parse (j.next' sym h₁) c (s.next' c i h₂)
   parse j
 
+private def pickNonNone (stack : SyntaxStack) : Syntax :=
+  match stack.toSubarray.findRev? fun stx => !stx.isNone with
+  | none => Syntax.missing
+  | some stx => stx
+
 def checkTailWs (prev : Syntax) : Bool :=
   match prev.getTailInfo with
   | .original _ _ trailing _ => trailing.stopPos > trailing.startPos
   | _                        => false
 
 def checkWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
-  let prev := s.stxStack.back
+  let prev := pickNonNone s.stxStack
   if checkTailWs prev then s else s.mkError errorMsg
 
 /-- The `ws` parser requires that there is some whitespace at this location.
@@ -1202,10 +1202,10 @@ This parser has arity 0 - it does not capture anything. -/
   info := epsilonInfo
   fn   := checkLinebreakBeforeFn errorMsg
 
-private def pickNonNone (stack : SyntaxStack) : Syntax :=
-  match stack.toSubarray.findRev? fun stx => !stx.isNone with
-  | none => Syntax.missing
-  | some stx => stx
+def checkTailNoWs (prev : Syntax) : Bool :=
+  match prev.getTailInfo with
+  | .original _ _ trailing _ => trailing.stopPos == trailing.startPos
+  | _                        => false
 
 def checkNoWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
   let prev := pickNonNone s.stxStack

src/Lean/Parser/Command.lean

@@ -122,7 +122,9 @@ def declModifiers (inline : Bool) := leading_parser
 /-- `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names -/
 -- @[builtin_doc] -- FIXME: suppress the hover
 def declId := leading_parser
-  ident >> optional (".{" >> sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}")
+  ident >>
+  optional (checkNoWsBefore "no space before '.{'" >> ".{" >>
+    sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}")
 /-- `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` -/
 -- @[builtin_doc] -- FIXME: suppress the hover
 def declSig := leading_parser

src/Lean/Parser/Term.lean

@@ -889,14 +889,21 @@ def isIdent (stx : Syntax) : Bool :=
   -- antiquotations should also be allowed where an identifier is expected
   stx.isAntiquot || stx.isIdent
 
-def isIdentOrDotIdent (stx : Syntax) : Bool :=
-  isIdent stx || stx.isOfKind ``dotIdent
+/-- Predicate for what `explicitUniv` can follow. It is only meant to be used on an identifier
+that becomes the head constant of an application. -/
+def isIdentOrDotIdentOrProj (stx : Syntax) : Bool :=
+  isIdent stx || stx.isOfKind ``dotIdent || stx.isOfKind ``proj
 
-/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
-@[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser
-  checkStackTop isIdentOrDotIdent "expected preceding identifier" >>
+/-- Syntax for `.{u, ...}` itself. Generally the `explicitUniv` trailing parser suffices.
+However, for `e |>.x.{u} a1 a2 a3` notation we need to be able to express explicit universes in the
+middle of the syntax. -/
+def explicitUnivSuffix : Parser :=
   checkNoWsBefore "no space before '.{'" >> ".{" >>
   sepBy1 levelParser ", " >> "}"
+/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
+@[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser
+  checkStackTop isIdentOrDotIdentOrProj "expected preceding identifier" >>
+  explicitUnivSuffix
 /-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
 If present, the identifier `h` is bound to a proof of `x = e`. -/
 @[builtin_term_parser] def namedPattern : TrailingParser := trailing_parser
@@ -909,7 +916,7 @@ If present, the identifier `h` is bound to a proof of `x = e`. -/
 It is especially useful for avoiding parentheses with repeated applications.
 -/
 @[builtin_term_parser] def pipeProj   := trailing_parser:minPrec
-  " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument
+  " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> optional explicitUnivSuffix >> many argument
 @[builtin_term_parser] def pipeCompletion := trailing_parser:minPrec
   " |>."
 

src/cmake/Modules/GetGitRevisionDescription.cmake

@@ -134,7 +134,16 @@ function(get_git_head_revision _refspecvar _hashvar)
       #
       string(REGEX REPLACE "gitdir: (.*)$" "\\1" git_worktree_dir ${worktree_ref})
       string(STRIP ${git_worktree_dir} git_worktree_dir)
-      _git_find_closest_git_dir("${git_worktree_dir}" GIT_DIR)
+      # Use the commondir file to find the shared git directory, rather than
+      # walking up the filesystem (which can find the wrong .git if the
+      # worktree gitdir is inside another git repository).
+      if(EXISTS "${git_worktree_dir}/commondir")
+        file(READ "${git_worktree_dir}/commondir" commondir_ref)
+        string(STRIP "${commondir_ref}" commondir_ref)
+        get_filename_component(GIT_DIR "${git_worktree_dir}/${commondir_ref}" ABSOLUTE)
+      else()
+        _git_find_closest_git_dir("${git_worktree_dir}" GIT_DIR)
+      endif()
       set(HEAD_SOURCE_FILE "${git_worktree_dir}/HEAD")
     endif()
   else()

src/lake/Lake/Build/Library.lean

@@ -24,6 +24,11 @@ namespace Lake
 
 /-! ## Build Lean & Static Lib -/
 
+private structure ModuleCollection where
+  mods : Array Module := #[]
+  modSet : ModuleSet := ∅
+  hasErrors : Bool := false
+
 /--
 Collect the local modules of a library.
 That is, the modules from `getModuleArray` plus their local transitive imports.
@@ -31,23 +36,27 @@ That is, the modules from `getModuleArray` plus their local transitive imports.
 private partial def LeanLib.recCollectLocalModules
   (self : LeanLib) : FetchM (Job (Array Module))
 := ensureJob do
-  let mut mods := #[]
-  let mut modSet := ModuleSet.empty
+  let mut col : ModuleCollection := {}
   for mod in (← self.getModuleArray) do
-    (mods, modSet) ← go mod mods modSet
-  return Job.pure mods
+    col ← go mod col
+  if col.hasErrors then
+    -- This is not considered a fatal error because we want the modules
+    -- built to provide better error categorization in the monitor.
+    logError s!"{self.name}: some modules have bad imports"
+  return Job.pure col.mods
 where
-  go root mods modSet := do
-    let mut mods := mods
-    let mut modSet := modSet
-    unless modSet.contains root do
-      modSet := modSet.insert root
-      let imps ← (← root.imports.fetch).await
+  go root col := do
+    let mut col := col
+    unless col.modSet.contains root do
+      col := {col with modSet := col.modSet.insert root}
+      -- We discard errors here as they will be reported later when the module is built.
+      let some imps ← (← root.imports.fetch).wait?
+        | return {col with hasErrors := true}
       for mod in imps do
         if mod.lib.name = self.name then
-          (mods, modSet) ← go mod mods modSet
-      mods := mods.push root
-    return (mods, modSet)
+          col ← go mod col
+      col := {col with mods := col.mods.push root}
+    return col
 
 /-- The `LibraryFacetConfig` for the builtin `modulesFacet`. -/
 private def LeanLib.modulesFacetConfig : LibraryFacetConfig modulesFacet :=

src/lakefile.toml.in

@@ -76,7 +76,7 @@ globs = ["Lake.*"]
 defaultFacets = ["static", "static.export"]
 # Load the previous stage's lake native code into lake's build process in order to prevent ABI
 # breakages from affecting bootstrapping.
-moreLeanArgs = ["--plugin", "${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
+weakLeanArgs = ["--plugin", "${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
 
 [[lean_lib]]
 name = "LakeMain"