fix: classify negative literals in grind by their syntactic type (#16341)

This PR fixes the `grind` internal error "linarith term has not been
internalized" on negative numerals such as `-1 : T`, where `T` unfolds
to `Int` and has an ordered `IntModule` instance but no `CommRing`
instance.

`getLitKind` unfolded `T` with `whnfD`, so it classified `-1 : T` as a
literal and `internalize` skipped the inner `1`. `linarith` reifies `-1
: T` as the negation of `1` and needs that `1`. A negative literal's
type must now be literally `Int`, `Int8`, `Int16`, `Int32`, or `Int64`,
as in `isInterpreted`. The `Int8`..`Int64` goals from #16286 already
succeed since #16298 and are included as regression tests.

Closes #16286

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>