fix: unnecessary NatModules in grind linarith

This PR fixes a performance issue in `grind linarith`. It was creating
unnecessary `NatModule`/`IntModule` structures for commutative rings
without an order. This kind of type should be handled by `grind ring` only.

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

@@ -214,8 +214,14 @@ where
     let isPartialInst? ← mkIsPartialOrderInst? u type leInst?
     let isLinearInst? ← mkIsLinearOrderInst? u type leInst?
     if (← getConfig).ring && ringId?.isSome && isPreorderInst?.isNone then
-      -- If `type` is a `CommRing`, but it is not even a preorder, there is no point in use this module.
-      -- `ring` module should handle it.
+      /-
+      If the type is a `Ring` **and** is not even a preorder **and** `grind ring` is enabled,
+      we let `grind ring` process the equalities and disequalities. There is no
+      point in using `linarith` in this case.
+      **IMPORTANT** We mark the type as a "forbiddenNatModule". It would be pointless to recheck everything in
+      in `getNatStructId?`
+      -/
+      modify' fun s => { s with forbiddenNatModules := s.forbiddenNatModules.insert { expr := type } }
       return none
     let commRingInst? ← getCommRingInst? ringId?
     let ringInst? ← mkRingInst? u type commRingInst?
@@ -229,6 +235,8 @@ where
     let isPreorderInst? := if orderedAddInst?.isNone then none else isPreorderInst?
     -- preorderInst? may have been reset, check again whether this module is needed.
     if (← getConfig).ring && ringId?.isSome && isPreorderInst?.isNone then
+      -- See comment above
+      modify' fun s => { s with forbiddenNatModules := s.forbiddenNatModules.insert { expr := type } }
       return none
     let isPartialInst? ← checkToFieldDefEq? leInst? isPreorderInst? isPartialInst? ``Std.IsPartialOrder.toIsPreorder u type
     let isLinearInst? ← checkToFieldDefEq? leInst? isPartialInst? isLinearInst? ``Std.IsLinearOrder.toIsPartialOrder u type
@@ -303,6 +311,7 @@ private def mkNatModuleInst? (u : Level) (type : Expr) : GoalM (Option Expr) :=
 
 def getNatStructId? (type : Expr) : GoalM (Option Nat) := do
   unless (← getConfig).linarith do return none
+  if (← get').forbiddenNatModules.contains { expr := type } then return none
   if (← isCutsatType type) then return none
   if let some id? := (← get').natTypeIdOf.find? { expr := type } then
     return id?

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

@@ -247,6 +247,12 @@ structure State where
   typeIdOf : PHashMap ExprPtr (Option Nat) := {}
   /- Mapping from expressions/terms to their structure ids. -/
   exprToStructId : PHashMap ExprPtr Nat := {}
+  /--
+  Some types are unordered rings, so we do not process them in `linarith`.
+  When such types are detected in `getStructId?`, we add them to the set
+  `forbiddenNatModules` to avoid reprocessing them in `getNatStructId?`.
+  -/
+  forbiddenNatModules : PHashSet ExprPtr := {}
   /-- `NatModule`. We support them using the envelope `OfNatModule.Q` -/
   natStructs : Array NatStruct := {}
   /--