Special-case (- x 1) for use in loops.

original commit: 7f300a2c4f9d934522a3b3ba3d5c949b5bd075ed

collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt

@@ -802,6 +802,11 @@
                              (eq? 'r x)
                              (eq? 's x)))
                 (make-pred-ty (t:Un (-val 'q) (-val 'r) (-val 's)))]
+        [tc-e (let: ([x : Exact-Positive-Integer 1])
+                (vector-ref #("a" "b") x)
+                (vector-ref #("a" "b") (sub1 x))
+                (vector-ref #("a" "b") (- x 1)))
+              -String]
         )
   (test-suite
    "check-type tests"

collects/typed-scheme/typecheck/tc-app.rkt

@@ -508,6 +508,12 @@
         (tc-error/expr "expected ~a, but got ~a" t (make-HeterogenousVector (map tc-expr/t (syntax->list #'(args ...)))))
         expected]
        [_ (int-err "bad expected: ~a" expected)])]
+    ;; special case for `-' used like `sub1'
+    [(#%plain-app (~and op (~literal -)) v (~and arg2 ((~literal quote) 1)))
+     (match-let ([(tc-result1: t) (single-value #'v)])
+       (if (subtype t -ExactPositiveInteger)
+           (ret -Nat)
+           (tc/funapp #'op #'(v arg2) (single-value #'op) (list (ret t) (single-value #'arg2)) expected)))]
     ;; call-with-values
     [(#%plain-app call-with-values prod con)
      (match (tc/funapp #'prod #'() (single-value #'prod) null #f)