fix: classify negative literals in grind by their syntactic type

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

@@ -80,6 +80,9 @@ inductive LitKind where
 /--
 Classifies the application `e`. For example, `BitVec` and `Fin` are parametric literals, but `Nat` is not.
 The types of nonparametric literals are reduced using `whnfD`, but `BitVec` and `Fin` must occur syntactically.
+The type of a negative literal `-n` must also occur syntactically because `internalize` does not visit `n`:
+the ring normalizer, used for `Int`, `Int8`, `Int16`, `Int32`, and `Int64`, treats `-n` as a constant, but
+`linarith` reifies `-n : α` for `def α := Int` as the negation of the variable `n`.
 `internalize` does not add literal applications to the congruence table.
 -/
 def getLitKind (e : Expr) : MetaM LitKind := do
@@ -99,7 +102,7 @@ def getLitKind (e : Expr) : MetaM LitKind := do
   | Neg.neg _ _ a =>
     let_expr OfNat.ofNat type n _ ← a | return .notLit
     unless n.consumeMData.isRawNatLit do return .notLit
-    let .const declName _ := (← whnfD type).getAppFn | return .notLit
+    let .const declName _ := type.consumeMData | return .notLit
     if declName == ``Int || declName == ``Int8 || declName == ``Int16 || declName == ``Int32 || declName == ``Int64 then
       return .nonParametric
     return .notLit

tests/elab/16286.lean

@@ -0,0 +1,36 @@
+open Lean Grind
+
+/-!
+Regression test for #16286: `grind` treats a negative literal such as `-1 : Int8` as a literal and
+does not internalize the numeral `1` inside it, but `linarith` reified `-1` as the negation of a
+variable `1` and failed with "linarith term has not been internalized".
+-/
+
+example (x : Int8) (h : -1 ≤ x) : -2 ≤ x := by grind_linarith
+example (x : Int16) (h : -1 ≤ x) : -2 ≤ x := by grind_linarith
+example (x : Int32) (h : -1 ≤ x) : -2 ≤ x := by grind_linarith
+example (x : Int64) (h : -1 ≤ x) : -2 ≤ x := by grind_linarith
+
+/-!
+`T` is an ordered `IntModule` but not a `CommRing`, so `linarith` reifies `-1 : T` itself, as the
+negation of the variable `1`. Thus, `-1 : T` is not a literal even though `T` reduces to `Int`.
+-/
+
+def T := Int
+instance : IntModule T := inferInstanceAs (IntModule Int)
+instance : LE T := inferInstanceAs (LE Int)
+instance : LT T := inferInstanceAs (LT Int)
+instance : Std.IsPreorder T := inferInstanceAs (Std.IsPreorder Int)
+instance : Std.IsLinearOrder T := inferInstanceAs (Std.IsLinearOrder Int)
+instance : Std.LawfulOrderLT T := inferInstanceAs (Std.LawfulOrderLT Int)
+instance : OrderedAdd T := inferInstanceAs (OrderedAdd Int)
+instance : OfNat T n := inferInstanceAs (OfNat Int n)
+
+example (x y : T) (h₁ : x ≤ -1) (h₂ : y ≤ x) : y ≤ -1 := by grind_linarith
+example (x y : T) (h₁ : x ≤ -1) (h₂ : y ≤ x) : y ≤ -1 := by grind
+
+example (x : T) (h : x + 1 ≤ 0) : x ≤ -1 := by grind_linarith
+example (x : T) (h : x ≤ -1) : x + 1 ≤ 0 := by grind_linarith
+example (x : T) (h : x ≠ -1) (h' : x + 1 = 0) : False := by grind_linarith
+
+example (x y : T) (h₁ : x + 1 ≤ 0) (h₂ : y ≤ x) : y ≤ -1 := by grind