Revert last change.

collects/typed-scheme/private/base-env.ss

@@ -196,7 +196,7 @@
      (min (->* (list N) N N))
      [values  (make-Poly '(a) (-> (-v a) (-v a)))]
      [vector-ref 
-      (make-Poly (list 'a) ((make-Vector (-v a)) -Integer . -> . (-v a)))]
+      (make-Poly (list 'a) ((make-Vector (-v a)) N . -> . (-v a)))]
      [build-vector (-poly (a) (-Integer (-Integer . -> . a) . -> . (make-Vector a)))]
      [build-list (-poly (a) (-Integer (-Integer . -> . a) . -> . (-lst a)))]
      [reverse (make-Poly '(a) (-> (make-lst (-v a)) (make-lst (-v a))))]
@@ -323,7 +323,7 @@
      
      [match:error ((list) Univ . ->* . (Un))]
      
-     [vector-set! (-poly (a) (-> (make-Vector a) -Integer a -Void))]
+     [vector-set! (-poly (a) (-> (make-Vector a) N a -Void))]
      
      [vector->list (-poly (a) (-> (make-Vector a) (-lst a)))]
      [list->vector (-poly (a) (-> (-lst a) (make-Vector a)))]
@@ -353,13 +353,13 @@
      [make-vector
       (-poly (a)
              (cl->
-              [(-Integer) (make-Vector -Integer)]
+              [(N) (make-Vector N)]
-              [(-Integer a) (make-Vector a)]))]
+              [(N a) (make-Vector a)]))]
      
      [file-exists? (-Pathlike . -> . B)]
      [string->symbol (-String . -> . Sym)]
      [symbol->string (Sym . -> . -String)]
-     [vector-length (-poly (a) ((make-Vector a) . -> . -Integer))]
+     [vector-length (-poly (a) ((make-Vector a) . -> . N))]
      
      [call-with-input-file (-poly (a) 
                                   (cl->

collects/typed-scheme/private/constraints.ss

@@ -80,8 +80,9 @@
       (make-cset maps))]
    [(_ _) (int-err "Got non-cset: ~a ~a" x y)]))
 
-(define (cset-meet* args #:X [X null])
+(define (cset-meet* args)
-  (for/fold ([c (empty-cset X)])
+  (for/fold ([c (make-cset (list (cons (make-immutable-hash null)
+                                       (make-dmap (make-immutable-hash null)))))])
     ([a args])
     (cset-meet a c)))
 

collects/typed-scheme/private/infer-unit.ss

@@ -370,7 +370,7 @@
          (list k (constraint->type v)))))]))
 
 (define (cgen/list V X S T)
-  (cset-meet* #:X X (for/list ([s S] [t T]) (cgen V X s t))))
+  (cset-meet* (for/list ([s S] [t T]) (cgen V X s t))))
 
 ;; X : variables to infer
 ;; S : actual argument types

collects/typed-scheme/private/tc-app-unit.ss

@@ -374,6 +374,11 @@
                                               (Function: (list (arr: doms rngs #f #f thn-effs els-effs) ...)))
                                        (PolyDots: (list vars ... _)
                                                   (Function: (list (arr: doms rngs #f #f thn-effs els-effs) ...)))))))
+         ;(printf "Typechecking poly app~nftype:          ~a~n" ftype)
+         ;(printf "ftype again:    ~a~n" ftype)
+         ;(printf "resolved ftype: ~a : ~a~n" (equal? rft ftype) rft)
+         ;(printf "reresolving: ~a~n" (resolve-tc-result ftype))
+         ;(printf "argtypes: ~a~ndoms: ~a~n" argtypes doms)
          (for-each (lambda (x) (unless (not (or (PolyDots? x) (Poly? x)))
                                  (tc-error "Polymorphic argument ~a to polymorphic function not allowed" x)))
                    argtypes)
@@ -394,11 +399,28 @@
                                         (stringify msg-vars)))])]
                  [(and (= (length (car doms*))
                           (length argtypes))
-                       (infer (fv/list (cons (car rngs*) (car doms*))) argtypes (car doms*) (car rngs*) (fv (car rngs*)) expected))
+                        (infer (fv/list (cons (car rngs*) (car doms*))) argtypes (car doms*) (car rngs*) (fv (car rngs*)) expected))
                   => (lambda (substitution)
                        (or expected
-                           (ret (subst-all substitution (car rngs*)))))]
+                           (let* ([s (lambda (t) (subst-all substitution t))]
-                 ;; otherwise, try the next element of the case-lambda
+                                  [new-doms* (map s (car doms*))])
+                             (if (andmap subtype argtypes new-doms*)
+                                 (ret (subst-all substitution (car rngs*)))
+                                 ;; FIXME
+                                 ;; should be an error here, something went horribly wrong!!!
+                                 (begin 
+				   #;
+                                   (printf "substitution was bad~n args: ~a ~n new-doms: ~a~n~a~n" argtypes new-doms* substitution)
+                                   (loop (cdr doms*) (cdr rngs*)))))))]
+                             #|
+                           (printf "subst is:~a~nret is: ~a~nvars is: ~a~nresult is:~a~n" substitution (car rngs*) vars 
+                                   (subst-all substitution (car rngs*)))
+                           (printf "new-doms*: ~a~n" new-doms*)
+                           (printf "orig doms* is: ~a~n" (car doms*))
+                           (printf "argtypes: ~a~n" argtypes)
+                           (int-err "Inconsistent substitution - arguments not subtypes")))
+                       #;(printf "subst is:~a~nret is: ~a~nvars is: ~a~n" substitution (car rngs*) vars)
+                       )]|#
                  [else (loop (cdr doms*) (cdr rngs*))]))]
         ;; polymorphic varargs
         [(tc-result: (and t
@@ -414,7 +436,12 @@
            (cond 
              [(and expected substitution) expected]
              [substitution
-              (ret (subst-all substitution rng))]
+              (let* ([s (lambda (t) (subst-all substitution t))]
+                     [new-dom (map s dom)]
+                     [new-rest (s rest)])                                  
+                (unless (subtypes/varargs argtypes new-dom new-rest)
+                  (int-err "Inconsistent substitution - arguments not subtypes"))
+                (ret (subst-all substitution rng)))]
              [else (tc-error/expr #:return (ret (Un))
                                   (string-append
                                    "No polymorphic function domain matched in function application:~n"