full support for sequence types in for forms

fix #974

Author: capfredf

typed-racket-lib/typed-racket/base-env/base-special-env.rkt

@@ -78,25 +78,24 @@
           (-> -Symbol -String (-> a -Boolean) (-> a -Nat) a -Nat (Un (-val #f) -Nat) -Nat (-values (list a -Index -Index -Index))))]
   ;; make-sequence
   [(make-template-identifier 'make-sequence 'racket/private/for)
-   (-poly (a b)
+   (-polydots (a b)
           (let ([seq-vals
-                 (lambda (a)
+                 (lambda (a b)
                    (-values (list
-                             (-> Univ (-values a))
+                             (-> Univ (-values-dots (list a) b 'b))
                              (Un (-> Univ Univ) (-val #f))
                              (-> Univ Univ)
                              Univ
                              (Un (-> Univ Univ) (-val #f))
-                             (Un (->* a Univ) (-val #f))
-                             (Un (->* (cons Univ a) Univ) (-val #f)))))])
+                             (Un (->... (list a) (b b) Univ) (-val #f))
+                             (Un (->... (list Univ a) (b b) Univ) (-val #f)))))])
             (cl->*
-             (-> Univ -Byte         (seq-vals (list -Byte)))
-             (-> Univ -Index        (seq-vals (list -Index)))
+             (-> Univ -Byte         (seq-vals -Byte b))
+             (-> Univ -Index        (seq-vals -Index b))
              ;; Generous. Negative numbers aren't allowed.
-             (-> Univ -Fixnum       (seq-vals (list -NonNegFixnum)))
-             (-> Univ -Int          (seq-vals (list -Nat)))
-             (-> Univ (-seq a) (seq-vals (list a)))
-             (-> Univ (-seq a b) (seq-vals (list a b))))))]
+             (-> Univ -Fixnum       (seq-vals -NonNegFixnum b))
+             (-> Univ -Int          (seq-vals -Nat b))
+             (->* (list Univ (-seq-dots (list a) b 'b)) (seq-vals a b)))))]
   ;; check-range
   [(make-template-identifier 'check-range 'racket/private/for)
    (-> Univ Univ Univ -Void)]

typed-racket-lib/typed-racket/infer/infer-unit.rkt

@@ -927,7 +927,7 @@
                    [(? variance:co?) (i-subst null)]
                    [(? variance:contra?) (i-subst/starred null Univ)]
                    ;; TODO figure out if there is a better subst here
-                   [(? variance:inv) (i-subst null)]))))
+                   [(? variance:inv?) (i-subst null)]))))
      S))
   (define (build-subst m)
     (match m

typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-special.rkt

@@ -48,9 +48,7 @@
         [(tc-result1: (and t Poly?))
          (tc-expr/check #'quo (ret Univ))
          (tc/funapp #'op #'(quo arg)
-                    (instantiate-poly t (list-extend (list Univ Univ)
-                                                     i-anns
-                                                     Univ))
+                    (instantiate-poly t i-anns)
                     (list (ret Univ) (single-value #'arg))
                     expected)]))
   ;; special-case for not - flip the props

typed-racket-test/succeed/gh-issue-974.rkt

@@ -0,0 +1,14 @@
+#lang typed/racket
+
+(define-type In-Integer (-> (Listof (List Integer Number Float)) (Sequenceof Integer Number Float)))
+
+(: test-int (-> In-Integer (Listof (List Integer Number Float)) Number))
+(define (test-int in-ints ints)
+  (for/sum : Number ([([a : Integer] [b : Number] [c : Float]) (in-ints ints)])
+    (+ a b c)))
+
+(for/list : (Listof Integer) ([i : Integer (list 0 1)])
+  (+ i 1))
+
+(for/list : (Listof Integer) ([i : Integer (in-list (list 0 1))])
+  (+ i 1))