diff --git a/collects/typed-scheme/infer/constraint-structs.rkt b/collects/typed-scheme/infer/constraint-structs.rkt
index ea946d98f9..19cb25916a 100644
--- a/collects/typed-scheme/infer/constraint-structs.rkt
+++ b/collects/typed-scheme/infer/constraint-structs.rkt
@@ -4,22 +4,23 @@
 
 ;; S, T types
 ;; X a var
-(define-struct c (S X T) #:prefab)
+;; represents S <: X <: T
+(d-s/c c ([S Type/c] [X symbol?] [T Type/c]) #:transparent)
 
 ;; fixed : Listof[c]
 ;; rest : option[c]
-(define-struct dcon (fixed rest) #:prefab)
+(d-s/c dcon ([fixed (listof c?)] [rest (or/c c? #f)]) #:transparent)
 
 ;; fixed : Listof[c]
 ;; rest : c
-(define-struct dcon-exact (fixed rest) #:prefab)
+(d-s/c dcon-exact ([fixed (listof c?)] [rest c?]) #:transparent)
 
 ;; type : c
 ;; bound : var
-(define-struct dcon-dotted (type bound) #:prefab)
+(d-s/c dcon-dotted ([type c?] [bound symbol?]) #:transparent)
 
 ;; map : hash mapping variable to dcon or dcon-dotted
-(define-struct dmap (map) #:prefab)
+(d-s/c dmap ([map (hash/c symbol? (or/c dcon? dcon-exact? dcon-dotted?))]) #:transparent)
 
 ;; maps is a list of pairs of
 ;;    - functional maps from vars to c's
@@ -27,17 +28,13 @@
 ;; we need a bunch of mappings for each cset to handle case-lambda
 ;; because case-lambda can generate multiple possible solutions, and we
 ;; don't want to rule them out too early
-(define-struct cset (maps) #:prefab)
+(d-s/c cset ([maps (listof (cons/c (hash/c symbol? c?) dmap?))]) #:transparent)
 
 (define-match-expander c:
   (lambda (stx)
     (syntax-parse stx
       [(_ s x t)
-       #'(struct c ((app (lambda (v) (if (Type? v) v (Un))) s) x (app (lambda (v) (if (Type? v) v Univ)) t)))])))
+       #'(struct c (s x t))])))
 
-(p/c (struct c ([S (or/c boolean? Type?)] [X symbol?] [T (or/c boolean? Type?)]))
-     (struct dcon ([fixed (listof c?)] [rest (or/c c? false/c)]))
-     (struct dcon-exact ([fixed (listof c?)] [rest c?]))
-     (struct dcon-dotted ([type c?] [bound symbol?]))
-     (struct dmap ([map (hash/c symbol? (or/c dcon? dcon-exact? dcon-dotted?))]))
-     (struct cset ([maps (listof (cons/c (hash/c symbol? c?) dmap?))])))
+(provide (struct-out cset) (struct-out dmap) (struct-out dcon) (struct-out dcon-dotted) (struct-out dcon-exact) (struct-out c)
+         c:)
diff --git a/collects/typed-scheme/infer/dmap.rkt b/collects/typed-scheme/infer/dmap.rkt
index 7e2e3b3934..7f88f291ae 100644
--- a/collects/typed-scheme/infer/dmap.rkt
+++ b/collects/typed-scheme/infer/dmap.rkt
@@ -2,14 +2,15 @@
 
 (require "../utils/utils.rkt" 
 	 "signatures.rkt" "constraint-structs.rkt"
-	 (utils tc-utils)
+	 (utils tc-utils) racket/contract
 	 unstable/sequence unstable/hash scheme/match)
 
 (import constraints^)
 (export dmap^)
 
 ;; dcon-meet : dcon dcon -> dcon
-(define (dcon-meet dc1 dc2)
+(d/c (dcon-meet dc1 dc2)
+  (dcon? dcon? . -> . dcon?)
   (match* (dc1 dc2)
     [((struct dcon-exact (fixed1 rest1)) (or (struct dcon (fixed2 rest2))
                                              (struct dcon-exact (fixed2 rest2))))
@@ -20,6 +21,7 @@
                  [c2 fixed2])
         (c-meet c1 c2 (c-X c1)))
       (c-meet rest1 rest2 (c-X rest1)))]
+    ;; redo in the other order to call the first case
     [((struct dcon (fixed1 rest1)) (struct dcon-exact (fixed2 rest2)))
      (dcon-meet dc2 dc1)]
     [((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f)))
diff --git a/collects/typed-scheme/infer/infer-dummy.rkt b/collects/typed-scheme/infer/infer-dummy.rkt
index 1774cbd6e7..e2d54becf2 100644
--- a/collects/typed-scheme/infer/infer-dummy.rkt
+++ b/collects/typed-scheme/infer/infer-dummy.rkt
@@ -4,6 +4,6 @@
 (require (rep type-rep) (utils tc-utils) mzlib/trace)
 
 (define infer-param (make-parameter (lambda e (int-err "infer not initialized"))))
-(define (unify X S T) ((infer-param) X null S T (make-Univ) null null))
+(define (unify X S T) ((infer-param) X null S T (make-Univ)))
 ;(trace unify)
 (provide unify infer-param)
diff --git a/collects/typed-scheme/infer/infer-unit.rkt b/collects/typed-scheme/infer/infer-unit.rkt
index 92054adb1f..ae88264103 100644
--- a/collects/typed-scheme/infer/infer-unit.rkt
+++ b/collects/typed-scheme/infer/infer-unit.rkt
@@ -7,12 +7,12 @@
            "rep/free-variance.rkt" "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/rep-utils.rkt"
            "types/convenience.rkt" "types/union.rkt" "types/subtype.rkt" "types/remove-intersect.rkt" "types/resolve.rkt"
            "env/type-name-env.rkt" "env/index-env.rkt" "env/tvar-env.rkt")
-          make-env)
+          make-env -> ->* one-of/c)
          "constraint-structs.rkt"
 	 "signatures.rkt"                  
          scheme/match
          mzlib/etc
-         mzlib/trace
+         mzlib/trace racket/contract
 	 unstable/sequence unstable/list unstable/debug
          scheme/list)
 
@@ -68,275 +68,253 @@
 
 (define (move-vars-to-dmap cset dbound vars)
   (mover cset dbound vars
-         (lambda (cmap)
+         (λ (cmap)
            (make-dcon (for/list ([v vars])
                         (hash-ref cmap v 
-                                  (lambda () (int-err "No constraint for new var ~a" v))))
+                                  (λ () (int-err "No constraint for new var ~a" v))))
                       #f))))
 
 (define (move-rest-to-dmap cset dbound #:exact [exact? #f])
   (mover cset dbound (list dbound)
-         (lambda (cmap)
+         (λ (cmap)
            ((if exact? make-dcon-exact make-dcon)
             null
             (hash-ref cmap dbound
-                      (lambda () (int-err "No constraint for bound ~a" dbound)))))))
+                      (λ () (int-err "No constraint for bound ~a" dbound)))))))
 
 (define (move-vars+rest-to-dmap cset dbound vars #:exact [exact? #f])
-  (map/cset
-   (lambda (cmap dmap)
-     (cons (hash-remove* cmap vars)           
-            (dmap-meet 
-             (singleton-dmap 
-              dbound
-              ((if exact? make-dcon-exact make-dcon)
-               (for/list ([v vars])
-                 (hash-ref cmap v 
-                           (lambda () (int-err "No constraint for new var ~a" v))))
-               (hash-ref cmap dbound
-                         (lambda () (int-err "No constraint for bound ~a" dbound)))))
-             dmap)))
-   cset))
+  (mover cset dbound vars
+         (λ (cmap)
+           ((if exact? make-dcon-exact make-dcon)
+            (for/list ([v vars])
+              (hash-ref cmap v (λ () (int-err "No constraint for new var ~a" v))))
+            (hash-ref cmap dbound
+                      (λ () (int-err "No constraint for bound ~a" dbound)))))))
 
-;; t and s must be *latent* filters
-(define (cgen/filter V X t s)
-  (match* (t s)
+;; s and t must be *latent* filters
+(define (cgen/filter V X s t)
+  (match* (s t)
     [(e e) (empty-cset X)]
     [(e (Top:)) (empty-cset X)]
     ;; FIXME - is there something to be said about the logical ones?
-    [((TypeFilter: t p i) (TypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))]
-    [((NotTypeFilter: t p i) (NotTypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))]
-    [(_ _) (fail! t s)]))
+    [((TypeFilter: s p i) (TypeFilter: t p i)) (cset-meet (cgen V X s t) (cgen V X t s))]
+    [((NotTypeFilter: s p i) (NotTypeFilter: t p i)) (cset-meet (cgen V X s t) (cgen V X t s))]
+    [(_ _) (fail! s t)]))
 
-#;
-(define (cgen/filters V X ts ss)
-  (cond 
-    [(null? ss) (empty-cset X)]
-    ;; FIXME - this can be less conservative
-    [(= (length ts) (length ss))
-     (cset-meet* (for/list ([t ts] [s ss]) (cgen/filter V X t s)))]
-    [else (fail! ts ss)]))
-
-
-;; t and s must be *latent* filter sets
-(define (cgen/filter-set V X t s)
-  (match* (t s)
+;; s and t must be *latent* filter sets
+(define (cgen/filter-set V X s t)
+  (match* (s t)
     [(e e) (empty-cset X)]
-    [((FilterSet: t+ t-) (FilterSet: s+ s-))
-     (cset-meet (cgen/filter V X t+ s+) (cgen/filter V X t- s-))]
-    [(_ _) (fail! t s)]))
+    [((FilterSet: s+ s-) (FilterSet: t+ t-))
+     (cset-meet (cgen/filter V X s+ t+) (cgen/filter V X s- t-))]
+    [(_ _) (fail! s t)]))
 
-(define (cgen/object V X t s)
-  (match* (t s)
+(define (cgen/object V X s t)
+  (match* (s t)
     [(e e) (empty-cset X)]
     [(e (Empty:)) (empty-cset X)]
     ;; FIXME - do something here    
-    [(_ _) (fail! t s)]))
+    [(_ _) (fail! s t)]))
 
-(define (cgen/arr V X t-arr s-arr)
+(define (cgen/arr V X s-arr t-arr)
   (define (cg S T) (cgen V X S T))
-  (match* (t-arr s-arr)
-    [((arr: ts t #f #f '())
-      (arr: ss s #f #f '()))
-     (cset-meet* 
-      (list (cgen/list V X ss ts)
-            (cg t s)))]
-    [((arr: ts t t-rest #f '())
-      (arr: ss s s-rest #f '()))
+  (match* (s-arr t-arr)
+    ;; the simplest case - no rests, drests, keywords
+    [((arr: ss s #f #f '())
+      (arr: ts t #f #f '()))
+     (cset-meet* (list 
+                  ;; contravariant
+                  (cgen/list V X ts ss)
+                  ;; covariant
+                  (cg s t)))]
+    ;; just a rest arg, no drest, no keywords
+    [((arr: ss s s-rest #f '())
+      (arr: ts t t-rest #f '()))
      (let ([arg-mapping 
-            (cond [(and t-rest s-rest (<= (length ts) (length ss)))
-                   (cgen/list V X (cons s-rest ss) (cons t-rest (extend ss ts t-rest)))]
-                  [(and t-rest s-rest (>= (length ts) (length ss)))
-                   (cgen/list V X (cons s-rest (extend ts ss s-rest)) (cons t-rest ts))]
-                  [(and t-rest (not s-rest) (<= (length ts) (length ss)))
-                   (cgen/list V X ss (extend ss ts t-rest))]
-                  [(and s-rest (not t-rest) (>= (length ts) (length ss)))
-                   (cgen/list V X (extend ts ss s-rest) ts)]
-                  [else (fail! S T)])]
-           [ret-mapping (cg t s)])
-       (cset-meet*
-        (list arg-mapping ret-mapping)))]
-    [((arr: ts t #f (cons dty dbound) '())
-      (arr: ss s #f #f                '()))
-     (unless (memq dbound X)
-       (fail! S T))
-     (unless (<= (length ts) (length ss))
-       (fail! S T))
-     (let* ([num-vars (- (length ss) (length ts))]
-            [vars     (for/list ([n (in-range num-vars)])
-                        (gensym dbound))]
-            [new-tys  (for/list ([var vars])
-                        (substitute (make-F var) dbound dty))]
-            [new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f null) s-arr)])
-       (move-vars-to-dmap new-cset dbound vars))]
-    [((arr: ts t #f #f                '())
-      (arr: ss s #f (cons dty dbound) '()))
+            (cond 
+              ;; both rest args are present, so make them the same length
+              [(and s-rest t-rest)
+               (cgen/list V X (cons t-rest (extend ss ts t-rest)) (cons s-rest (extend ts ss s-rest)))]
+              ;; no rest arg on the right, so just pad the left and forget the rest arg
+              [(and s-rest (not t-rest) (<= (length ss) (length ts)))
+               (cgen/list V X ts (extend ts ss s-rest))]
+              ;; no rest arg on the left, or wrong number = fail
+              [else (fail! S T)])]
+           [ret-mapping (cg s t)])
+       (cset-meet* (list arg-mapping ret-mapping)))]
+    ;; dotted on the left, nothing on the right
+    [((arr: ss s #f (cons dty dbound) '())
+      (arr: ts t #f #f                '()))
      (unless (memq dbound X)
        (fail! S T))
      (unless (<= (length ss) (length ts))
        (fail! S T))
-     (let* ([num-vars (- (length ts) (length ss))]
-            [vars     (for/list ([n (in-range num-vars)])
+     (let* ([vars      (for/list ([n (in-range (- (length ts) (length ss)))])
+                         (gensym dbound))]
+            [new-tys   (for/list ([var vars])
+                         (substitute (make-F var) dbound dty))]
+            [new-s-arr (make-arr (append ss new-tys) s #f #f null)]
+            [new-cset  (cgen/arr V (append vars X) new-s-arr t-arr)])
+       (move-vars-to-dmap new-cset dbound vars))]
+    ;; dotted on the right, nothing on the left
+    [((arr: ss s #f #f                '())
+      (arr: ts t #f (cons dty dbound) '()))
+     (unless (memq dbound X)
+       (fail! S T))
+     (unless (<= (length ts) (length ss))
+       (fail! S T))
+     (let* ([vars     (for/list ([n (in-range (- (length ss) (length ts)))])
                         (gensym dbound))]
             [new-tys  (for/list ([var vars])
                         (substitute (make-F var) dbound dty))]
-            [new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f null))])
+            [new-t-arr (make-arr (append ts new-tys) t #f #f null)]
+            [new-cset (cgen/arr V (append vars X) s-arr new-t-arr)])
        (move-vars-to-dmap new-cset dbound vars))]
-    [((arr: ts t #f (cons t-dty dbound) '())
-      (arr: ss s #f (cons s-dty dbound) '()))
-     (unless (= (length ts) (length ss))
+    ;; this case is just for constrainting other variables, not dbound
+    [((arr: ss s #f (cons s-dty dbound) '())
+      (arr: ts t #f (cons t-dty dbound) '()))
+     (unless (= (length ss) (length ts))
        (fail! S T))
      ;; If we want to infer the dotted bound, then why is it in both types?
      (when (memq dbound X)
        (fail! S T))
-     (let* ([arg-mapping (cgen/list V X ss ts)]
-            [darg-mapping (cgen V X s-dty t-dty)]
-            [ret-mapping (cg t s)])
+     (let* ([arg-mapping (cgen/list V X ts ss)]
+            [darg-mapping (cgen V X t-dty s-dty)]
+            [ret-mapping (cg s t)])
        (cset-meet* 
         (list arg-mapping darg-mapping ret-mapping)))]
-    [((arr: ts t #f (cons t-dty dbound)  '())
-      (arr: ss s #f (cons s-dty dbound*) '()))
-     (unless (= (length ts) (length ss))
+    ;; bounds are different
+    [((arr: ss s #f (cons s-dty dbound)  '())
+      (arr: ts t #f (cons t-dty dbound*) '()))
+     (unless (= (length ss) (length ts))
        (fail! S T))
-     (let* ([arg-mapping (cgen/list V X ss ts)]
-            [darg-mapping (cgen V (cons dbound* X) s-dty t-dty)]
-            [ret-mapping (cg t s)])
+     (let* ([arg-mapping (cgen/list V X ts ss)]
+            ;; just add dbound as something that can be constrained
+            [darg-mapping (cgen V (cons dbound X) t-dty s-dty)]
+            [ret-mapping (cg s t)])
        (cset-meet* 
         (list arg-mapping darg-mapping ret-mapping)))]
-    [((arr: ts t t-rest #f                  '())
-      (arr: ss s #f     (cons s-dty dbound) '()))
+    [((arr: ss s s-rest #f                  '())
+      (arr: ts t #f     (cons t-dty dbound) '()))
      (unless (memq dbound X)
        (fail! S T))
-     (if (<= (length ts) (length ss))
+     (if (<= (length ss) (length ts))
          ;; the simple case
-         (let* ([arg-mapping (cgen/list V X ss (extend ss ts t-rest))]
-                [darg-mapping (move-rest-to-dmap (cgen V X s-dty t-rest) dbound)]
-                [ret-mapping (cg t s)])
+         (let* ([arg-mapping (cgen/list V X ts (extend ts ss s-rest))]
+                [darg-mapping (move-rest-to-dmap (cgen V X t-dty s-rest) dbound)]
+                [ret-mapping (cg s t)])
            (cset-meet* (list arg-mapping darg-mapping ret-mapping)))
          ;; the hard case
-         (let* ([num-vars (- (length ts) (length ss))]
-                [vars     (for/list ([n (in-range num-vars)])
+         (let* ([vars     (for/list ([n (in-range (- (length ss) (length ts)))])
                             (gensym dbound))]
                 [new-tys  (for/list ([var vars])
-                            (substitute (make-F var) dbound s-dty))]
-                [new-cset (cgen/arr V (append vars X) t-arr 
-                                    (make-arr (append ss new-tys) s #f (cons s-dty dbound) null))])
+                            (substitute (make-F var) dbound t-dty))]
+                [new-t-arr (make-arr (append ts new-tys) t #f (cons t-dty dbound) null)]
+                [new-cset (cgen/arr V (append vars X) s-arr new-t-arr)])
            (move-vars+rest-to-dmap new-cset dbound vars)))]
     ;; If dotted <: starred is correct, add it below.  Not sure it is.
-    [((arr: ts t #f     (cons t-dty dbound) '())
-      (arr: ss s s-rest #f                  '()))
+    [((arr: ss s #f     (cons s-dty dbound) '())
+      (arr: ts t t-rest #f                  '()))
      (unless (memq dbound X)
        (fail! S T))
-     (cond [(< (length ts) (length ss))
+     (cond [(< (length ss) (length ts))
             ;; the hard case
-            (let* ([num-vars (- (length ss) (length ts))]
-                   [vars     (for/list ([n (in-range num-vars)])
+            (let* ([vars     (for/list ([n (in-range (- (length ts) (length ss)))])
                                (gensym dbound))]
                    [new-tys  (for/list ([var vars])
-                               (substitute (make-F var) dbound t-dty))]
-                   [arg-mapping (cgen/list V (append vars X) ss (append ts new-tys))]
-                   [darg-mapping (cgen V X s-rest t-dty)]
-                   [ret-mapping (cg t s)]
-                   [new-cset
-                    (cset-meet* (list arg-mapping darg-mapping ret-mapping))])
+                               (substitute (make-F var) dbound s-dty))]
+                   [new-s-arr (make-arr (append ss new-tys) s #f (cons s-dty dbound) null)]
+                   [new-cset (cgen/arr V (append vars X) new-s-arr t-arr)])
               (move-vars+rest-to-dmap new-cset dbound vars #:exact #t))]
            [else
             ;; the simple case
-            (let* ([arg-mapping (cgen/list V X (extend ts ss s-rest) ts)]
-                   [darg-mapping (move-rest-to-dmap (cgen V X s-rest t-dty) dbound #:exact #t)]
-                   [ret-mapping (cg t s)])
+            (let* ([arg-mapping (cgen/list V X (extend ss ts t-rest) ss)]
+                   [darg-mapping (move-rest-to-dmap (cgen V X t-rest s-dty) dbound #:exact #t)]
+                   [ret-mapping (cg s t)])
               (cset-meet* (list arg-mapping darg-mapping ret-mapping)))])]
     [(_ _) (fail! S T)]))
 
-;; determine constraints on the variables in X that would make S a subtype of T
-;; the resulting constraints will not mention V
-(define (cgen V X S T)
+;; V : a set of variables not to mention in the constraints
+;; X : the set of variables to be constrained
+;; S : a type to be the subtype of T
+;; T : a type
+;; produces a cset which determines a substitution that makes S a subtype of T
+;; implements the V |-_X S <: T => C judgment from Pierce+Turner
+(d/c (cgen V X S T)
+  ((listof symbol?) (listof symbol?) Type? Type? . -> . cset?)
+  ;; useful quick loop
   (define (cg S T) (cgen V X S T))
+  ;; this places no constraints on any variables in X
   (define empty (empty-cset X))
-  (define (singleton S X T)
-    (insert empty X S T))
+  ;; this constrains just x (which is a single var)
+  (define (singleton S x T)
+    (insert empty x S T))
+  ;; if we've been around this loop before, we're done (for rec types)
   (if (seen? S T)
       empty
       (parameterize ([match-equality-test (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))]
+                     ;; remember S and T, and obtain everything we've seen from the context
+                     ;; we can't make this an argument since we may call back and forth with subtyping, for example
                      [current-seen (remember S T (current-seen))])
-        (match* 
-            (S T)
+        (match* (S T)
+          ;; if they're equal, no constraints are necessary (CG-Refl)
           [(a a) empty]
+          ;; CG-Top
           [(_ (Univ:)) empty]
 
+          ;; refinements are erased to their bound
           [((Refinement: S _ _) T)
            (cg S T)]
 
-          [((F: (? (lambda (e) (memq e X)) v)) S)
-           (when (match S
-                   [(F: v*)
-                    (and (bound-index? v*) (not (bound-tvar? v*)))]
-                   [_ #f])
-             (fail! S T))
-           (singleton (Un) v (var-demote S V))]
+          ;; variables that are in X and should be constrained
+          ;; all other variables are compatible only with themselves
+          [((F: (? (λ (e) (memq e X)) v)) T)
+           (match T
+             ;; only possible when v* is an index
+             [(F: v*) (when (and (bound-index? v*) (not (bound-tvar? v*)))
+                        (fail! S T))]
+             [_ (void)])
+           ;; constrain v to be below T (but don't mention V)
+           (singleton (Un) v (var-demote T V))]
           [(S (F: (? (lambda (e) (memq e X)) v)))
-           (when (match S
-                   [(F: v*)
-                    (and (bound-index? v*) (not (bound-tvar? v*)))]
-                   [_ #f])
-             (fail! S T))
+           (match S
+             [(F: v*) (when (and (bound-index? v*) (not (bound-tvar? v*)))
+                        (fail! S T))]
+             [_ (void)])
+           ;; constrain v to be above S (but don't mention V)
            (singleton (var-promote S V) v Univ)]
-
-          ;; two unions with the same number of elements, so we just try to unify them pairwise
-          #;[((Union: l1) (Union: l2))
-             (=> unmatch)
-             (unless (= (length l1) (length l2))
-               (unmatch))
-             (cgen-union V X l1 l2)]
           
-          #;[((Poly: v1 b1) (Poly: v2 b2))
-             (unless (= (length v1) (length v2))
-               (fail! S T))
-             (let ([b2* (subst-all (map list v2 v1) b2)])
-               (cg b1 b2*))]
+          ;; constrain b1 to be below T, but don't mention the new vars
+          [((Poly: v1 b1) T) (cgen (append v1 V) X b1 T)]
           
-          #;[((PolyDots: (list v1 ... r1) b1) (PolyDots: (list v2 ... r2) b2))
-             (unless (= (length v1) (length v2))
-               (fail! S T))
-             (let ([b2* (substitute-dotted v1 v1 v2 (subst-all (map list v2 v1) b2))])
-               (cg b1 b2*))]
+          ;; constrain *each* element of es to be below T, and then combine the constraints
+          [((Union: es) T) (cset-meet* (cons empty (for/list ([e es]) (cg e T))))]
           
-          [((Poly: v1 b1) T)
-           (cgen (append v1 V) X b1 T)]
-          
-          #;[((PolyDots: (list v1 ... r1) b1) T)
-             (let ([b1* (var-demote b1 (cons r1 v1))])
-               (cg b1* T))]
-          
-          #;
-          [((Poly-unsafe: n b) (Poly-unsafe: n* b*))
-           (unless (= n n*)
-             (fail! S T))
-           (cg b b*)]
-          
-          
-          [((Union: es) S) (cset-meet* (cons empty (for/list ([e es]) (cg e S))))]
-          ;; we might want to use multiple csets here, but I don't think it makes a difference
-          [(S (Union: es)) (or
-                            (for/or 
-                             ([e es]) 
-                             (with-handlers
-                                 ([exn:infer? (lambda _ #f)])
-                               (cg S e)))
-                            (fail! S T))]
+          ;; find *an* element of es which can be made to be a supertype of S
+          ;; FIXME: we're using multiple csets here, but I don't think it makes a difference 
+          ;; not using multiple csets will break for: ???
+          [(S (Union: es)) 
+           (cset-combine
+            (filter values
+                    (for/list ([e es]) 
+                      (with-handlers ([exn:infer? (λ _ #f)]) (cg S e)))))]
           
+          ;; two structs with the same name and parent
+          ;; just check pairwise on the fields
+          ;; FIXME - wrong for mutable structs!
           [((Struct: nm p flds proc _ _ _ _ _) (Struct: nm p flds* proc* _ _ _ _ _))
            (let-values ([(flds flds*)
                          (cond [(and proc proc*)
                                 (values (cons proc flds) (cons proc* flds*))]
-                               [(or proc proc*)
-                                (fail! S T)]
                                [else (values flds flds*)])])
              (cgen/list V X flds flds*))]
+          
+          ;; two struct names, need to resolve b/c one could be a parent
           [((Name: n) (Name: n*))
            (if (free-identifier=? n n*)
                null
-               (fail! S T))]
+               (cg (resolve-once S) (resolve-once T)))]
+          ;; pairs are pointwise
           [((Pair: a b) (Pair: a* b*))
            (cset-meet (cg a a*) (cg b b*))]
           ;; sequences are covariant
@@ -362,108 +340,126 @@
            (cg t t*)]
           [((Hashtable: k v) (Sequence: (list k* v*)))
            (cgen/list V X (list k v) (list k* v*))]
+          ;; ListDots can be below a Listof
           ;; must be above mu unfolding
           [((ListDots: s-dty dbound) (Listof: t-elem))
            (when (memq dbound X) (fail! S T))
            (cgen V X (substitute Univ dbound s-dty) t-elem)]
+          ;; two ListDots with the same bound, just check the element type
           [((ListDots: s-dty dbound) (ListDots: t-dty dbound))
            (when (memq dbound X) (fail! S T))
-           (cgen V X s-dty t-dty)]          
+           (cgen V X s-dty t-dty)]
+          
+          ;; this constrains `dbound' to be |ts| - |ss|
+          [((ListDots: s-dty dbound) (List: ts))
+           (unless (memq dbound X) (fail! S T))
+           
+           (let* ([vars     (for/list ([n (in-range (length ts))])
+                              (gensym dbound))]
+                  ;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated
+                  [new-tys  (for/list ([var vars])
+                              (substitute (make-F var) dbound s-dty))]
+                  ;; generate constraints on the prefixes, and on the dummy types
+                  [new-cset (cgen/list V (append vars X) new-tys ts)])
+             ;; now take all the dummy types, and use them to constrain dbound appropriately
+             (move-vars-to-dmap new-cset dbound vars))]
+          
           ;; if we have two mu's, we rename them to have the same variable
           ;; and then compare the bodies
+          ;; This relies on (B 0) only unifying with itself, and thus only hitting the first case of this `match'
           [((Mu-unsafe: s) (Mu-unsafe: t)) 
            (cg s t)]
+          
           ;; other mu's just get unfolded
           [(s (? Mu? t)) (cg s (unfold t))]
           [((? Mu? s) t) (cg (unfold s) t)]
-          ;; type application          
-          [((App: (Name: n) args _)
-            (App: (Name: n*) args* _))
-           (unless (free-identifier=? n n*)
-             (fail! S T))
-             (cg (resolve-once S) (resolve-once T))]
+                    
+          ;; resolve applications
           [((App: _ _ _) _) (cg (resolve-once S) T)]
           [(_ (App: _ _ _)) (cg S (resolve-once T))]
+          
+          ;; values are covariant
           [((Values: ss) (Values: ts))
            (unless (= (length ss) (length ts))
              (fail! ss ts))
            (cgen/list V X ss ts)]
-          [((Values: ss) (ValuesDots: ts t-dty dbound))
-           (unless (>= (length ss) (length ts))
-             (fail! ss ts))
-           (unless (memq dbound X)
-             (fail! S T))
-           (let* ([num-vars (- (length ss) (length ts))]
-                  [vars     (for/list ([n (in-range num-vars)])
-                              (gensym dbound))]
-                  [new-tys  (for/list ([var vars])
-                              (substitute (make-F var) dbound t-dty))]
-                  [new-cset (cgen/list V (append vars X) ss (append ts new-tys))])
-             (move-vars-to-dmap new-cset dbound vars))]
+          
+          ;; this constrains `dbound' to be |ts| - |ss|
           [((ValuesDots: ss s-dty dbound) (Values: ts))
-           (unless (>= (length ts) (length ss))
-             (fail! ss ts))
-           (unless (memq dbound X)
-             (fail! S T))
-           (let* ([num-vars (- (length ts) (length ss))]
-                  [vars     (for/list ([n (in-range num-vars)])
+           (unless (>= (length ts) (length ss)) (fail! ss ts))
+           (unless (memq dbound X) (fail! S T))
+           
+           (let* ([vars     (for/list ([n (in-range (- (length ts) (length ss)))])
                               (gensym dbound))]
+                  ;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated
                   [new-tys  (for/list ([var vars])
                               (substitute (make-F var) dbound s-dty))]
+                  ;; generate constraints on the prefixes, and on the dummy types
                   [new-cset (cgen/list V (append vars X) (append ss new-tys) ts)])
+             ;; now take all the dummy types, and use them to constrain dbound appropriately
              (move-vars-to-dmap new-cset dbound vars))]
+          
+          ;; identical bounds - just unify pairwise
           [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
            (when (memq dbound X) (fail! ss ts))          
            (cgen/list V X (cons s-dty ss) (cons t-dty ts))]
+          ;; vectors are invariant - generate constraints *both* ways
           [((Vector: e) (Vector: e*))
            (cset-meet (cg e e*) (cg e* e))]
+          ;; boxes are invariant - generate constraints *both* ways
           [((Box: e) (Box: e*))
            (cset-meet (cg e e*) (cg e* e))]
           [((MPair: s t) (MPair: s* t*))
            (cset-meet* (list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))]
           [((Channel: e) (Channel: e*))
            (cset-meet (cg e e*) (cg e* e))]
+          ;; we assume all HTs are mutable at the moment
           [((Hashtable: s1 s2) (Hashtable: t1 t2))
            ;; for mutable hash tables, both are invariant
            (cset-meet* (list (cg t1 s1) (cg s1 t1) (cg t2 s2) (cg s2 t2)))]
+          ;; syntax is covariant
           [((Syntax: s1) (Syntax: s2))
            (cg s1 s2)]
           ;; parameters are just like one-arg functions
           [((Param: in1 out1) (Param: in2 out2))
            (cset-meet (cg in2 in1) (cg out1 out2))]
+          ;; every function is trivially below top-arr
           [((Function: _)
             (Function: (list (top-arr:))))
            empty]
-          [((Function: (list t-arr ...))
-            (Function: (list s-arr ...)))
-           (=> unmatch)
-           (cset-combine
-            (filter 
-             values ;; only generate the successful csets
-             (for*/list 
-              ([t-arr t-arr] [s-arr s-arr])
-              (with-handlers ([exn:infer? (lambda (_) #f)])
-                (cgen/arr V X t-arr s-arr)))))]
-          ;; this is overly conservative
+          [((Function: (list s-arr ...))
+            (Function: (list t-arr ...)))
+           (cset-meet*
+            (for/list ([t-arr t-arr])
+              ;; for each element of t-arr, we need to get at least one element of s-arr that works
+              (let ([results (filter values
+                                     (for/list ([s-arr s-arr])
+                                       (with-handlers ([exn:infer? (lambda (_) #f)])
+                                         (cgen/arr V X s-arr t-arr))))])
+                ;; ensure that something produces a constraint set
+                (when (null? results) (fail! S T))
+                (cset-combine results))))]
+          ;; check each element
           [((Result: s f-s o-s)
             (Result: t f-t o-t))
            (cset-meet* (list (cg s t) 
                              (cgen/filter-set V X f-s f-t)
                              (cgen/object V X o-s o-t)))]
           [(_ _)
-           (cond [(subtype S T) empty]
-                 ;; or, nothing worked, and we fail
-                 [else (fail! S T)])]))))
+           (cond 
+             ;; subtypes are easy - should this go earlier?
+             [(subtype S T) empty]
+             ;; or, nothing worked, and we fail
+             [else (fail! S T)])]))))
 
-(define (check-vars must-vars subst)
-  (and (for/and ([v must-vars])
-                (assq v subst))
-       subst))
-
-(define (subst-gen C R must-vars)
+(d/c (subst-gen C R)
+  (cset? Type? . -> . (or/c #f list?))
+  ;; fixme - should handle these separately
+  (define must-vars (append (fv R) (fi R)))
   (define (constraint->type v #:variable [variable #f])
     (match v
       [(struct c (S X T))
+       ;; fixme - handle free indexes, remove Dotted
        (let ([var (hash-ref (free-vars* R) (or variable X) Constant)])
          ;(printf "variance was: ~a~nR was ~a~nX was ~a~nS T ~a ~a~n" var R (or variable X) S T)
          (evcase var 
@@ -471,28 +467,36 @@
                  [Covariant S]
                  [Contravariant T]
                  [Invariant S]
-                 [Dotted T]))]))
+                 [Dotted T]))]))  
   (match (car (cset-maps C))
-    [(cons cmap (struct dmap (dm)))
-     (check-vars
-      must-vars
-      (append 
-       (for/list ([(k dc) (in-hash dm)])
-         (match dc
-           [(struct dcon (fixed rest))
-            (list k
-                  (for/list ([f fixed])
-                    (constraint->type f #:variable k))
-                  (and rest (constraint->type rest)))]
-           [(struct dcon-exact (fixed rest))
-            (list k
-                  (for/list ([f fixed])
-                    (constraint->type f #:variable k))
-                  (constraint->type rest))]))
-       (for/list ([(k v) (in-hash cmap)])
-         (list k (constraint->type v)))))]))
+    [(cons cmap (dmap dm))
+     (let ([subst (append 
+                   (for/list ([(k dc) (in-hash dm)])
+                     (match dc
+                       [(dcon fixed rest)
+                        (list k
+                              (for/list ([f fixed])
+                                (constraint->type f #:variable k))
+                              (and rest (constraint->type rest)))]
+                       [(dcon-exact fixed rest)
+                        (list k
+                              (for/list ([f fixed])
+                                (constraint->type f #:variable k))
+                              (constraint->type rest))]))
+                   (for/list ([(k v) (in-hash cmap)])
+                     (list k (constraint->type v))))])
+       ;; verify that we got all the important variables
+       (and (for/and ([v must-vars])
+              (assq v subst))
+            subst))]))
 
-(define (cgen/list V X S T)
+;; V : a set of variables not to mention in the constraints
+;; X : the set of variables to be constrained
+;; S : a list of types to be the subtypes of T
+;; T : a list of types
+;; produces a cset which determines a substitution that makes the Ss subtypes of the Ts
+(d/c (cgen/list V X S T)
+  ((listof symbol?) (listof symbol?) (listof Type?) (listof Type?) . -> . cset?)
   (unless (= (length S) (length T))
     (fail! S T))
   (cset-meet* (for/list ([s S] [t T]) (cgen V X s t))))
@@ -502,25 +506,23 @@
 ;; S : actual argument types
 ;; T : formal argument types
 ;; R : result type
-;; must-vars : variables that must be in the substitution
-;; must-idxs : index variables that must be in the substitution
 ;; expected : boolean
 ;; returns a substitution
 ;; if R is #f, we don't care about the substituion
 ;; just return a boolean result
-(define (infer X Y S T R must-vars must-idxs [expected #f])
+(define (infer X Y S T R [expected #f])
   (with-handlers ([exn:infer? (lambda _ #f)])  
     (let* ([cs (cgen/list null (append X Y) S T)]
            [cs* (if expected 
                     (cset-meet cs (cgen null (append X Y) R expected))
                     cs)])
-          (subst-gen cs* R (append must-vars must-idxs)))))
+          (if R (subst-gen cs* R) #t))))
 
 ;; like infer, but T-var is the vararg type:
-(define (infer/vararg X Y S T T-var R must-vars must-idxs [expected #f])
+(define (infer/vararg X Y S T T-var R [expected #f])
   (define new-T (if T-var (extend S T T-var) T))
   (and ((length S) . >= . (length T))
-       (infer X Y S new-T R must-vars must-idxs expected)))
+       (infer X Y S new-T R expected)))
 
 ;; like infer, but dotted-var is the bound on the ...
 ;; and T-dotted is the repeated type
@@ -537,7 +539,7 @@
            [cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)]
            [cs (cset-meet cs-short cs-dotted*)])
       (if (not expected)
-          (subst-gen cs R must-vars)
-          (subst-gen (cset-meet cs (cgen null X R expected)) R must-vars)))))
+          (subst-gen cs R)
+          (subst-gen (cset-meet cs (cgen null X R expected)) R)))))
 
 ;(trace cgen)
diff --git a/collects/typed-scheme/infer/restrict.rkt b/collects/typed-scheme/infer/restrict.rkt
index 9779332f85..b0825050fd 100644
--- a/collects/typed-scheme/infer/restrict.rkt
+++ b/collects/typed-scheme/infer/restrict.rkt
@@ -23,7 +23,7 @@
     [(subtype t1 t2) t1] ;; already a subtype          
     [(match t2
        [(Poly: vars t)
-        (let ([subst (infer vars null (list t1) (list t) t1 (fv t1) (fi t1))])
+        (let ([subst (infer vars null (list t1) (list t) t1)])
           (and subst (restrict* t1 (subst-all subst t1))))]
        [_ #f])]           
     [(Union? t1) (union-map (lambda (e) (restrict* e t2)) t1)]
diff --git a/collects/typed-scheme/infer/signatures.rkt b/collects/typed-scheme/infer/signatures.rkt
index f9b80aa538..fb5457012d 100644
--- a/collects/typed-scheme/infer/signatures.rkt
+++ b/collects/typed-scheme/infer/signatures.rkt
@@ -39,11 +39,7 @@
                 ;; domain
                 (listof Type?)
                 ;; range
-                Type?
-                ;; free variables                
-                (listof symbol?)
-                ;; free indexes
-                (listof symbol?))
+                (or/c #f Type?))
                ;; optional expected type
                ((or/c #f Type?)) 
                . ->* . any)]
@@ -58,11 +54,7 @@
                        ;; rest
                        (or/c #f Type?)
                        ;; range
-                       Type?
-                       ;; free variables
-                       (listof symbol?)
-                       ;; free indexes
-                       (listof symbol?))
+                       (or/c #f Type?))
                       ;; [optional] expected type
                       ((or/c #f Type?)) . ->* . any)]
    [cnt infer/dots (((listof symbol?) 
diff --git a/collects/typed-scheme/rep/type-rep.rkt b/collects/typed-scheme/rep/type-rep.rkt
index 4e9b861adc..bc3ff7ec36 100644
--- a/collects/typed-scheme/rep/type-rep.rkt
+++ b/collects/typed-scheme/rep/type-rep.rkt
@@ -227,7 +227,7 @@
 
 ;; name : symbol
 ;; parent : Struct
-;; flds : Listof[Cons[Type,Bool]] type and mutability
+;; flds : Listof[Type]
 ;; proc : Function Type
 ;; poly? : is this a polymorphic type?
 ;; pred-id : identifier for the predicate of the struct
diff --git a/collects/typed-scheme/typecheck/tc-app.rkt b/collects/typed-scheme/typecheck/tc-app.rkt
index 11cdf7f3b6..b88879308e 100644
--- a/collects/typed-scheme/typecheck/tc-app.rkt
+++ b/collects/typed-scheme/typecheck/tc-app.rkt
@@ -324,9 +324,7 @@
                                    (cons (make-Listof (car rests*))
                                          (car doms*))
                                    (car rests*)
-                                   (car rngs*)
-                                   (fv (car rngs*))
-                                   (fi (car rngs*))))
+                                   (car rngs*)))
                 => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
                ;; actual work, when we have a * function and ... final arg
                [(and (car rests*)
@@ -338,9 +336,7 @@
                                    (cons (make-Listof (car rests*))
                                          (car doms*))
                                    (car rests*)
-                                   (car rngs*)
-                                   (fv (car rngs*))
-                                   (fi (car rngs*))))
+                                   (car rngs*)))
                 => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
                ;; ... function, ... arg
                [(and (car drests*)                     
@@ -349,7 +345,7 @@
                      (= (length (car doms*))
                         (length arg-tys))
                      (infer vars null (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) 
-                            (car rngs*) (fv (car rngs*)) (fi (car rngs*))))
+                            (car rngs*)))
                 => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
                ;; if nothing matches, around the loop again
                [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
@@ -381,8 +377,7 @@
                                    (cons (make-Listof (car rests*))
                                          (car doms*))
                                    (car rests*)
-                                   (car rngs*)
-                                   (fv (car rngs*)) (fi (car rngs*))))
+                                   (car rngs*)))
                 => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
                ;; actual work, when we have a * function and ... final arg
                [(and (car rests*)
@@ -394,8 +389,7 @@
                                    (cons (make-Listof (car rests*))
                                          (car doms*))
                                    (car rests*)
-                                   (car rngs*)
-                                   (fv (car rngs*)) (fi (car rngs*))))
+                                   (car rngs*)))
                 => (lambda (substitution) 
                      (do-ret (subst-all substitution (car rngs*))))]
                ;; ... function, ... arg, same bound on ...
@@ -407,8 +401,7 @@
                      (infer fixed-vars (list dotted-var)
                             (cons tail-ty arg-tys)
                             (cons (car (car drests*)) (car doms*))
-                            (car rngs*) 
-                            (fv (car rngs*)) (fi (car rngs*))))
+                            (car rngs*)))
                 => (lambda (substitution)
                      (do-ret (subst-all substitution (car rngs*))))]
                ;; ... function, ... arg, different bound on ...
@@ -423,8 +416,7 @@
                          (infer fixed-vars (list dotted-var)
                                 (cons tail-ty arg-tys) 
                                 (cons (car (car drests*)) (car doms*)) 
-                                (car rngs*)
-                                (fv (car rngs*)) (fi (car rngs*))))))
+                                (car rngs*)))))
                 => (lambda (substitution) 
                      (define drest-bound (cdr (car drests*)))
                      (do-ret (substitute-dotted (cadr (assq drest-bound substitution))
@@ -621,7 +613,7 @@
           (fail))
         (match (map single-value (syntax->list #'pos-args))
           [(list (tc-result1: argtys-t) ...)
-           (let* ([subst (infer vars null argtys-t dom rng (fv rng) (fi rng) (and expected (tc-results->values expected)))])
+           (let* ([subst (infer vars null argtys-t dom rng (and expected (tc-results->values expected)))])
              (tc-keywords form (list (subst-all subst ar))
                           (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected))])]
        [(tc-result1: (Function: arities)) 
@@ -839,7 +831,7 @@
                        (if drest
                            (infer/dots fixed-vars dotted-var argtys-t dom (car drest) rng (fv rng) 
                                        #:expected (and expected (tc-results->values expected)))
-                           (infer/vararg fixed-vars (list dotted-var) argtys-t dom rest rng (fv rng) (fi rng)
+                           (infer/vararg fixed-vars (list dotted-var) argtys-t dom rest rng
                                          (and expected (tc-results->values expected)))))
                      t argtys expected)]
     ;; regular polymorphic functions without dotted rest, and without mandatory keyword args
@@ -854,7 +846,7 @@
                      (lambda (dom _ rest a) ((if rest <= =) (length dom) (length argtys)))
                      ;; only try to infer the free vars of the rng (which includes the vars in filters/objects)
                      ;; note that we have to use argtys-t here, since argtys is a list of tc-results
-                     (lambda (dom rng rest a) (infer/vararg vars null argtys-t dom rest rng (fv rng) (fi rng) (and expected (tc-results->values expected))))
+                     (lambda (dom rng rest a) (infer/vararg vars null argtys-t dom rest rng (and expected (tc-results->values expected))))
                      t argtys expected)]
     ;; procedural structs
     [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _ _))) _)