Fix type of quotient on fixnums.

Closes PR13466.

original commit: 32b3dfc528169609bc05a8fc769da5166d5a2858

collects/tests/typed-racket/optimizer/tests/invalid-fxquotient.rkt

@@ -0,0 +1,11 @@
+#;
+(
+TR missed opt: invalid-fxquotient.rkt 10:21 (quotient fixnum-min -1) -- out of fixnum range
+#f
+)
+
+#lang typed/racket/base
+
+(define: fixnum-min : Nonpositive-Fixnum (assert (- (expt 2 30)) fixnum?))
+(define: q : Natural (quotient fixnum-min -1)) ; this can't be optimized safely
+(fixnum? q) ; should return #f

collects/tests/typed-racket/succeed/pr12678.rkt

@@ -0,0 +1,9 @@
+#lang typed/racket
+
+(define: memo : (HashTable Natural String)  (make-immutable-hash empty))
+(define strs '("Hello" "Goodbye"))
+
+(for/fold: : (HashTable Natural String)
+    ([memo : (HashTable Natural String)  (make-immutable-hash empty)])
+    ([i : Natural  (in-naturals)] [str : String  (in-list strs)])
+  (hash-set memo i str))

collects/tests/typed-racket/succeed/pr13412.rkt

@@ -0,0 +1,12 @@
+#lang typed/racket
+
+(define-type (Tree A) (U (Listof A) (node A)))
+(struct: (A) node ([val : A]
+                   [left : (Tree A)]
+                   [right : (Tree A)]))
+
+(: tree-set (All (A) (A (Tree A) -> (Tree A))))
+(define (tree-set y t)
+  (cond [(node? t)  (node y (node-left t) (node-right t))]
+        [else  (list y)]))
+

collects/typed-racket/base-env/base-env-numeric.rkt

@@ -1336,7 +1336,7 @@
   ;; we don't have equivalent for fixnums:
   ;; (quotient min-fixnum -1) -> max-fixnum + 1
   (commutative-binop -NonNegFixnum -NonPosFixnum -NonPosFixnum)
-  (-NonPosFixnum -NonPosFixnum . -> . -NonNegFixnum)
+  (-NonPosFixnum -NonPosFixnum . -> . -Nat)
   (-NonNegFixnum -Nat . -> . -NonNegFixnum)
   (-NonNegFixnum -Int . -> . -Fixnum)
   (binop -Nat)

collects/typed-racket/typecheck/tc-app/tc-app-lambda.rkt

@@ -6,7 +6,7 @@
          syntax/parse racket/match racket/list
          syntax/parse/experimental/reflect
          unstable/sequence
-         (typecheck signatures tc-funapp check-below find-annotation )
+         (typecheck signatures tc-funapp find-annotation)
          (types abbrev utils generalize type-table)
          (private type-annotation)
          (rep type-rep)
@@ -98,7 +98,7 @@
                  (let* ([infer-t (or (type-annotation f #:infer #t)
                                      (find-annotation #'(begin . body*) f))])
                    (if infer-t
-                       (check-below (tc-expr/t ac) infer-t)
+                       (tc-expr/check/t ac (ret infer-t))
                        (generalize (tc-expr/t ac)))))])
        (add-typeof-expr lam (tc/rec-lambda/check form args body lp ts expected))
        expected)]))

collects/typed-racket/types/current-seen.rkt

@@ -0,0 +1,13 @@
+#lang racket/base
+(require "../utils/utils.rkt")
+(require (rep type-rep))
+
+(provide (all-defined-out))
+
+(define current-seen (make-parameter null))
+(define (currently-subtyping?) (not (null? (current-seen))))
+
+(define (seen-before s t) (cons (Type-seq s) (Type-seq t)))
+(define (remember s t A) (cons (seen-before s t) A))
+(define (seen? s t) (member (seen-before s t) (current-seen)))
+

collects/typed-racket/types/resolve.rkt

@@ -4,7 +4,7 @@
 (require (rep type-rep rep-utils free-variance)
          (env type-name-env)
          (utils tc-utils)
-         (types utils)
+         (types utils current-seen)
          racket/match
          racket/contract
          racket/format)
@@ -82,7 +82,7 @@
                   [(App: r r* s)
                    (resolve-app r r* s)]
                   [(Name: _) (resolve-name t)])])
-        (when r*
+        (when (and r* (not (currently-subtyping?)))
           (hash-set! resolver-cache seq r*))
         r*)))
 

collects/typed-racket/types/subtype.rkt

@@ -2,7 +2,7 @@
 (require (except-in "../utils/utils.rkt" infer)
          (rep type-rep filter-rep object-rep rep-utils)
          (utils tc-utils)
-         (types utils resolve base-abbrev numeric-tower substitute)
+         (types utils resolve base-abbrev numeric-tower substitute current-seen)
          (env type-name-env)
          racket/match unstable/match
          racket/function
@@ -24,14 +24,6 @@
   (syntax-rules ()
     [(_ s t) (raise (make-exn:subtype "subtyping failed" (current-continuation-marks) s t))]))
 
-;; data structures for remembering things on recursive calls
-(define (empty-set) '())
-
-(define current-seen (make-parameter (empty-set)))
-
-(define (seen-before s t) (cons (Type-seq s) (Type-seq t)))
-(define (remember s t A) (cons (seen-before s t) A))
-(define (seen? s t) (member (seen-before s t) (current-seen)))
 
 (define subtype-cache (make-hash))
 (define (cache-types s t)
@@ -54,7 +46,8 @@
     (define result (handle-failure (and (subtype* (current-seen) s t) #t)))
     ;(printf "subtype cache miss ~a ~a\n" s t)
     result)
-  (hash-ref! subtype-cache k new-val))
+  ((if (currently-subtyping?) hash-ref hash-ref!)
+   subtype-cache k new-val))
 
 ;; are all the s's subtypes of all the t's?
 ;; [type] [type] -> boolean
@@ -162,7 +155,7 @@
 (define (subtypes/varargs args dom rst)
   (with-handlers
       ([exn:subtype? (lambda _ #f)])
-    (subtypes*/varargs (empty-set) args dom rst)))
+    (subtypes*/varargs null args dom rst)))
 
 (define (subtypes*/varargs A0 argtys dom rst)
   (let loop-varargs ([dom dom] [argtys argtys] [A A0])