diff --git a/collects/tests/typed-scheme/fail/too-many-errors.ss b/collects/tests/typed-scheme/fail/too-many-errors.ss
new file mode 100644
index 00000000..6d726847
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/too-many-errors.ss
@@ -0,0 +1,11 @@
+#lang typed/scheme
+
+(: f : Number  -> Number)
+(define (f a b)
+ (+ a b))
+
+(define: (g [a : Number] [b : Number]) : Number
+ (+ a b))
+
+(f 1 2)
+(g 1 2)
diff --git a/collects/tests/typed-scheme/succeed/map-nonempty.ss b/collects/tests/typed-scheme/succeed/map-nonempty.ss
new file mode 100644
index 00000000..0fddf079
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/map-nonempty.ss
@@ -0,0 +1,6 @@
+#lang typed/scheme
+
+(: x (Pair Number (Listof Number)))
+(define x (cons 1 (list 1 2 3 4)))
+
+(apply max (ann (map add1 x) : (Pair Number (Listof Number))))
\ No newline at end of file
diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss
index 73d1a9a1..a92069c7 100644
--- a/collects/typed-scheme/env/init-envs.ss
+++ b/collects/typed-scheme/env/init-envs.ss
@@ -22,27 +22,28 @@
   (define (gen-constructor sym)
     (string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
   (match v
-    [(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq))]
-    [(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt))]
-    [(Name: stx) `(make-Name (quote-syntax ,stx))]
+    [(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq) ',(Type-name v))]
+    [(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt) ',(Type-name v))]
+    [(Name: stx) `(make-Name (quote-syntax ,stx) ',(Type-name v))]
     [(Struct: name parent flds proc poly? pred-id cert)
-     `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))]
-    [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
-    [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
+     `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier) ',(Type-name v))]
+    [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx) ',(Type-name v))]
+    [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier) ',(Type-name v))]
     [(Refinement: parent pred cert) `(make-Refinement ,(sub parent)
                                                       (quote-syntax ,pred)
-                                                      (syntax-local-certifier))]
-    [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
-    [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
-    [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]
+                                                      (syntax-local-certifier)
+                                                      ',(Type-name v))]
+    [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b) ',(Type-name v))]
+    [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b) ',(Type-name v))]
+    [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b) ',(Type-name v))]
     [(? (lambda (e) (or (LatentFilter? e)
                         (LatentObject? e)
                         (PathElem? e)))
         (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals))) 
      `(,(gen-constructor tag) ,@(map sub vals))]
     [(? (lambda (e) (or (Type? e)))
-        (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq vals))) 
-     `(,(gen-constructor tag) ,@(map sub vals))]
+        (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq name vals))) 
+     `(,(gen-constructor tag) ,@(map sub vals) ',name)]
     [_ (basic v)]))
 
 (define (bound-in-this-module id) 
diff --git a/collects/typed-scheme/infer/promote-demote.ss b/collects/typed-scheme/infer/promote-demote.ss
index 1eb261f1..316ed06b 100644
--- a/collects/typed-scheme/infer/promote-demote.ss
+++ b/collects/typed-scheme/infer/promote-demote.ss
@@ -1,7 +1,7 @@
 #lang scheme/unit
 
 (require "../utils/utils.ss")
-(require (rep type-rep rep-utils)
+(require (rep type-rep)         
 	 (types convenience union utils)
          "signatures.ss"
          scheme/list scheme/match)
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 0a2b64ee..98d2c9da 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -98,8 +98,13 @@
 [list? (make-pred-ty (-lst Univ))]
 [list (-poly (a) (->* '() a (-lst a)))]
 [procedure? (make-pred-ty top-func)]
-[map (-polydots (c a b) ((list ((list a) (b b) . ->... . c) (-lst a))
-                         ((-lst b) b) . ->... .(-lst c)))]
+[map (-polydots (c a b) 
+		(cl->*
+		 (-> (-> a c) (-pair a (-lst a)) (-pair c (-lst c)))
+		((list 
+		  ((list a) (b b) . ->... . c) 
+		  (-lst a))
+		 ((-lst b) b) . ->... .(-lst c))))]
 [for-each (-polydots (c a b) ((list ((list a) (b b) . ->... . Univ) (-lst a))
                               ((-lst b) b) . ->... . -Void))]
 [fold-left (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index 613c5a57..f3db1d68 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -238,12 +238,12 @@
          (lambda (t)
            ;(printf "found a type alias ~a~n" #'id)
            (add-type-name-reference #'id)
-           t)]
+           t #;(add-name t (syntax-e #'id)))]
         ;; if it's a type name, we just use the name
         [(lookup-type-name #'id (lambda () #f))
          (add-type-name-reference #'id)
          ;(printf "found a type name ~a~n" #'id)
-         (make-Name #'id)]
+         (add-name (make-Name #'id) (syntax-e #'id))]
         [(free-identifier=? #'id #'t:->)
          (tc-error/delayed "Incorrect use of -> type constructor")
          Err]
diff --git a/collects/typed-scheme/rep/free-variance.ss b/collects/typed-scheme/rep/free-variance.ss
index 7e4014e3..c53a5086 100644
--- a/collects/typed-scheme/rep/free-variance.ss
+++ b/collects/typed-scheme/rep/free-variance.ss
@@ -1,104 +1 @@
 #lang scheme/base
-(require "../utils/utils.ss")
-
-(require (for-syntax scheme/base)
-         (utils tc-utils)
-         mzlib/etc)
-
-;; this file contains support for calculating the free variables/indexes of types
-;; actual computation is done in rep-utils.ss  and type-rep.ss
-
-(define-values (Covariant Contravariant Invariant Constant Dotted)
-  (let ()
-    (define-struct Variance () #:inspector #f)
-    (define-struct (Covariant Variance) () #:inspector #f)
-    (define-struct (Contravariant Variance) () #:inspector #f)
-    (define-struct (Invariant Variance) () #:inspector #f)
-    (define-struct (Constant Variance) () #:inspector #f)
-    ;; not really a variance, but is disjoint with the others
-    (define-struct (Dotted Variance) () #:inspector #f)
-    (values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted))))
-
-
-(provide Covariant Contravariant Invariant Constant Dotted)
-
-;; hashtables for keeping track of free variables and indexes
-(define index-table (make-weak-hasheq))
-;; maps Type to List[Cons[Number,Variance]]
-(define var-table (make-weak-hasheq))
-;; maps Type to List[Cons[Symbol,Variance]]
-
-(define (free-idxs* t) (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" (syntax-e t)))))
-(define (free-vars* t) (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table" (syntax-e t)))))
-
-
-(define empty-hash-table (make-immutable-hasheq null))
-
-(provide free-vars* free-idxs* empty-hash-table make-invariant)
-
-;; frees = HT[Idx,Variance] where Idx is either Symbol or Number
-;; (listof frees) -> frees
-(define (combine-frees freess)    
-  (define ht (make-hasheq))
-  (define (combine-var v w)
-    (cond
-      [(eq? v w) v]
-      [(eq? v Dotted) w]
-      [(eq? w Dotted) v]
-      [(eq? v Constant) w]
-      [(eq? w Constant) v]
-      [else Invariant]))
-  (for* ([old-ht (in-list freess)]
-         [(sym var) (in-hash old-ht)])
-        (let* ([sym-var (hash-ref ht sym (lambda () #f))])
-          (if sym-var
-              (hash-set! ht sym (combine-var var sym-var))
-              (hash-set! ht sym var))))
-  ht)
-
-;; given a set of free variables, change bound to ...
-;; (if bound wasn't free, this will add it as Dotted
-;;  appropriately so that things that expect to see
-;;  it as "free" will -- fixes the case where the
-;;  dotted pre-type base doesn't use the bound).
-(define (fix-bound vs bound)
-  (define vs* (hash-map* (lambda (k v) v) vs))
-  (hash-set! vs* bound Dotted)
-  vs*)
-
-;; frees -> frees
-(define (flip-variances vs)
-  (hash-map* 
-   (lambda (k v) 
-     (evcase 
-         v
-       [Covariant Contravariant]
-       [Contravariant Covariant]
-       [v v]))
-   vs))
-
-(define (make-invariant vs)
-  (hash-map* 
-   (lambda (k v) Invariant)
-   vs))
-
-(define (hash-map* f ht)
-  (define new-ht (make-hasheq))
-  (for ([(k v) (in-hash ht)])
-     (hash-set! new-ht k (f k v)))
-  new-ht)
-
-(define (without-below n frees)
-  (define new-ht (make-hasheq))
-  (for ([(k v) (in-hash frees)])
-       (when (>= k n) (hash-set! new-ht k v)))
-  new-ht)
-
-(provide combine-frees flip-variances without-below unless-in-table var-table index-table empty-hash-table
-         fix-bound)
-
-(define-syntax (unless-in-table stx) 
-  (syntax-case stx ()
-    [(_ table val . body)
-     (quasisyntax/loc stx
-       (hash-ref table val #,(syntax/loc #'body (lambda () . body))))]))
diff --git a/collects/typed-scheme/rep/interning.ss b/collects/typed-scheme/rep/interning.ss
index 3dfd9aef..a370b34d 100644
--- a/collects/typed-scheme/rep/interning.ss
+++ b/collects/typed-scheme/rep/interning.ss
@@ -14,12 +14,9 @@
      #'(define *name
 	 (let ([table (make-ht)])
 	   (lambda (arg ...)
-	     (let ([key key-expr])
-	       (hash-ref table key
-			 (lambda ()
-			   (let ([new (make-name (count!) e ... arg ...)])
-			     (hash-set! table key new)
-			     new)))))))]))
+	     (let* ([key key-expr]
+                    [new-seq (hash-ref table key count!)])
+               (make-name new-seq e ... arg ...)))))]))
 
 (define (make-count!)  
   (let ([state 0])
diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss
index ca994b19..d1194589 100644
--- a/collects/typed-scheme/rep/rep-utils.ss
+++ b/collects/typed-scheme/rep/rep-utils.ss
@@ -2,9 +2,8 @@
 (require "../utils/utils.ss")
 
 (require mzlib/struct 
-         scheme/match
+         scheme/match scheme/list
          syntax/boundmap
-         "free-variance.ss"
          "interning.ss"
 	 unstable/syntax unstable/match
          mzlib/etc
@@ -25,9 +24,11 @@
 
 (provide == defintern hash-id (for-syntax fold-target))
 
+
+
 (define-for-syntax fold-target #'fold-target)
 
-(define-for-syntax (mk par ht-stx key?)
+(define-for-syntax (mk par ht-stx key? name?)
   (define-syntax-class opt-cnt-id
     #:attributes (i cnt)
     (pattern i:id
@@ -67,6 +68,8 @@
              #:with e fold-target)
     (pattern ex:expr
              #:with e #'#'ex))
+  (unless (equal? key? name?)
+    (error "key? not name"))
   (lambda (stx)          
     (syntax-parse stx 
       [(dform nm:id flds:idlist (~or 
@@ -85,7 +88,7 @@
          [*maker (format-id #'nm "*~a" #'nm)]
          [**maker (format-id #'nm "**~a" #'nm)]
          [*maker-cnt (if enable-contracts?
-                         (or (attribute cnt) #'(flds.cnt ... . -> . pred))
+                         (or (attribute cnt) #`((flds.cnt ...) #,(if name? #'(any/c) #'()) . ->* . pred))
                          #'any/c)]
          [ht-stx ht-stx]
          [bfs-fold-rhs (cond [(attribute fold-rhs)
@@ -105,26 +108,30 @@
                            (p/c (rename *maker maker *maker-cnt))))]
          [intern 
           (let ([mk (lambda (int) 
-		      (if key? 
-			  #`(defintern (**maker . flds.fs) maker #,int #:extra-arg #,(attribute key-expr))
-			  #`(defintern (**maker . flds.fs) maker #,int)))])
-         (syntax-parse #'flds.fs
-              [_  #:fail-unless (attribute intern?) #f
-                 (mk #'intern?)]
-              [() (mk #'#f)]
-              [(f) (mk #'f)]
-              [_ (mk #'(list . flds.fs))]))]
-         [(ign-pats ...) (if key? #'(_ _) #'(_))]
+                      (if (and key? name?)
+                          #`(defintern (**maker name-val . flds.fs) maker #,int #:extra-arg #,(attribute key-expr))
+                          #`(defintern (**maker . flds.fs) maker #,int)))])
+            (syntax-parse #'flds.fs
+                          [_  #:fail-unless (attribute intern?) #f
+                              (mk #'intern?)]
+                          [() (mk #'#f)]
+                          [(f) (mk #'f)]
+                          [_ (mk #'(list . flds.fs))]))]
+         [(ign-pats ...) (if (and name? key?) #'(_ _ _) #'(_))]
          [frees-def (if (attribute frees) #'frees.def #'(begin))]
          [frees 
           (with-syntax ([(f1 f2) (if (attribute frees)
                                      #'(frees.f1 frees.f2)
                                      (list (combiner #'free-vars* #'flds.fs)
-                                           (combiner #'free-idxs* #'flds.fs)))])
+                                           (combiner #'free-idxs* #'flds.fs)))]
+                        [(fs ...) #'flds.fs]
+                        [name-val-formal
+                         (if name? #'([name-val #f]) #'())]
+                        [name-val-expr (if name? #'(name-val) #'())])
             (quasisyntax/loc stx
 		(w/c nm ([*maker *maker-cnt])
-                   (define (*maker . flds.fs)
-                     (define v (**maker . flds.fs))
+                   (define (*maker fs ... #,@#'name-val-formal)
+                     (define v (**maker #,@#'name-val-expr fs ...))
                      frees-def
                      (unless-in-table 
                       var-table v
@@ -228,23 +235,29 @@
 (define-syntax (make-prim-type stx)
   (define default-flds #'(seq))
   (define-syntax-class type-name-base
-    #:attributes (i lower-s first-letter key? (fld-names 1))
+    #:attributes (i lower-s first-letter key? (fld-names 1) name?)
     #:transparent
     (pattern i:id
              #:attr lower-s (string-downcase (symbol->string (attribute i.datum)))
              #:with (fld-names ...) default-flds
 	     #:with key? #'#f
+	     #:with name? #'#f
              #:attr first-letter (string-ref (attribute lower-s) 0))
     (pattern [i:id #:d d-name:id]
              #:with (fld-names ...) default-flds
              #:attr lower-s (string-downcase (symbol->string (attribute i.datum)))
 	     #:with key? #'#f
+	     #:with name? #'#f
              #:attr first-letter (symbol->string (attribute d-name.datum)))
-    (pattern [i:id #:key]
+    (pattern [i:id #:key (~optional (~and name-kw #:name))]
              #:with (fld-names ...) (datum->syntax #f (append (syntax->list default-flds) 
-                                                              (syntax->list #'(key))))
+                                                              (list #'key)
+                                                              (if (attribute name-kw)
+                                                                  (list #'name)
+                                                                  null)))
              #:attr lower-s (string-downcase (symbol->string (attribute i.datum)))
 	     #:with key? #'#t
+	     #:with name? (if (attribute name-kw) #'#t #'#f)
              #:attr first-letter (string-ref (attribute lower-s) 0)))
   (define-syntax-class type-name
     #:transparent
@@ -258,7 +271,7 @@
              #:with ht (format-id #'i "~a-name-ht" (attribute lower-s))
              #:with rec-id (format-id #'i "~a-rec-id" (attribute lower-s))
              #:with d-id (format-id #'i "d~a" (attribute first-letter))
-             #:with (_ _ pred? accs ...)
+             #:with (_ _ pred? seq-acc accs ...)
                     (datum->syntax #f (build-struct-names #'name (syntax->list #'(fld-names ...)) #f #t #'name))))
   (syntax-parse stx
     [(_ i:type-name ...)
@@ -267,11 +280,15 @@
                     [fresh-ids-list #'(fresh-ids ...)]
                     [(anys ...) (for/list ([i (syntax->list #'fresh-ids-list)]) #'any/c)])
        #'(begin
-           (provide i.d-id ... i.printer ... i.name ... i.pred? ... i.accs ... ...
+           (provide i.d-id ... i.printer ... i.name ... i.pred? ... i.seq-acc ... i.accs ... ...
                     (for-syntax i.ht ... i.rec-id ...))
-           (define-syntax i.d-id (mk #'i.name #'i.ht i.key?)) ...
+           (define-syntax i.d-id (mk #'i.name #'i.ht i.key? i.name?)) ...
            (define-for-syntax i.ht (make-hasheq)) ...
-           (define-struct/printer i.name (i.fld-names ...) (lambda (a b c) ((unbox i.printer) a b c))) ...
+           (define-struct/printer i.name (i.fld-names ...) (lambda (a b c) ((unbox i.printer) a b c))
+             [prop:equal+hash (list (lambda (a b rec)
+                                      (eq? (i.seq-acc a) (i.seq-acc b)))
+                                    (lambda (a rec) (i.seq-acc a))
+                                    (lambda (a secondary) (secondary a)))]) ...
            (define-for-syntax i.rec-id #'i.rec-id) ...   
            (provide i.case ...)           
            (define-syntaxes (i.case ...)
@@ -284,9 +301,139 @@
                                       '(i.keyword ...)))
                            (list i.ht ...)))))))]))
 
-(make-prim-type [Type #:key]
+(make-prim-type [Type #:key #:name]
                 Filter
                 [LatentFilter #:d lf]
                 Object 
                 [LatentObject #:d lo]
                 [PathElem #:d pe])
+
+;; free-variance.ss starts here:
+
+(require "../utils/utils.ss")
+
+(require (for-syntax scheme/base)
+         (utils tc-utils)
+         scheme/contract
+         mzlib/etc)
+
+;; this file contains support for calculating the free variables/indexes of types
+;; actual computation is done in rep-utils.ss  and type-rep.ss
+
+(define-values (Covariant Contravariant Invariant Constant Dotted)
+  (let ()
+    (define-struct Variance () #:inspector #f)
+    (define-struct (Covariant Variance) () #:inspector #f)
+    (define-struct (Contravariant Variance) () #:inspector #f)
+    (define-struct (Invariant Variance) () #:inspector #f)
+    (define-struct (Constant Variance) () #:inspector #f)
+    ;; not really a variance, but is disjoint with the others
+    (define-struct (Dotted Variance) () #:inspector #f)
+    (values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted))))
+
+(define (variance? e)
+  (memq e (list Covariant Contravariant Invariant Constant Dotted)))
+
+
+(provide Covariant Contravariant Invariant Constant Dotted)
+
+;; hashtables for keeping track of free variables and indexes
+(define index-table (make-weak-hash))
+;; maps Type to List[Cons[Number,Variance]]
+(define var-table (make-weak-hash))
+;; maps Type to List[Cons[Symbol,Variance]]
+
+(define input/c (or/c Type? Filter? LatentFilter? Object? LatentObject? PathElem?))
+
+(d/c (free-idxs* t)
+     (->  input/c (hash/c integer? variance?))
+     (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" t))))
+(d/c (free-vars* t)
+     (-> input/c  (hash/c symbol? variance?))
+     (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table ~a" t (take (reverse (hash-map var-table list)) 20)))))
+
+
+(define empty-hash-table (make-immutable-hasheq null))
+
+;; Type? is not available here! grrr
+(p/c
+ [free-vars* (-> input/c  (hash/c symbol? variance?))]
+ [free-idxs* (-> input/c  (hash/c integer? variance?))])
+
+(provide empty-hash-table)
+
+;; frees = HT[Idx,Variance] where Idx is either Symbol or Number
+;; (listof frees) -> frees
+(define (combine-frees freess)    
+  (define ht (make-hasheq))
+  (define (combine-var v w)
+    (cond
+      [(eq? v w) v]
+      [(eq? v Dotted) w]
+      [(eq? w Dotted) v]
+      [(eq? v Constant) w]
+      [(eq? w Constant) v]
+      [else Invariant]))
+  (for* ([old-ht (in-list freess)]
+         [(sym var) (in-hash old-ht)])
+        (let* ([sym-var (hash-ref ht sym (lambda () #f))])
+          (if sym-var
+              (hash-set! ht sym (combine-var var sym-var))
+              (hash-set! ht sym var))))
+  ht)
+
+;; given a set of free variables, change bound to ...
+;; (if bound wasn't free, this will add it as Dotted
+;;  appropriately so that things that expect to see
+;;  it as "free" will -- fixes the case where the
+;;  dotted pre-type base doesn't use the bound).
+(define (fix-bound vs bound)
+  (define vs* (hash-map* (lambda (k v) v) vs))
+  (hash-set! vs* bound Dotted)
+  vs*)
+
+;; frees -> frees
+(define (flip-variances vs)
+  (hash-map* 
+   (lambda (k v) 
+     (evcase 
+         v
+       [Covariant Contravariant]
+       [Contravariant Covariant]
+       [v v]))
+   vs))
+
+(define (make-invariant vs)
+  (hash-map* 
+   (lambda (k v) Invariant)
+   vs))
+
+(define (hash-map* f ht)
+  (define new-ht (make-hasheq))
+  (for ([(k v) (in-hash ht)])
+     (hash-set! new-ht k (f k v)))
+  new-ht)
+
+(define (without-below n frees)
+  (define new-ht (make-hasheq))
+  (for ([(k v) (in-hash frees)])
+       (when (>= k n) (hash-set! new-ht k v)))
+  new-ht)
+
+(define table/c (hash/c (or/c integer? symbol?) variance?))
+
+(p/c [combine-frees (-> (listof table/c) table/c)]
+     [flip-variances (-> table/c table/c)]
+     [make-invariant (-> table/c table/c)]
+     [without-below (-> integer? table/c table/c)])
+
+(provide unless-in-table var-table index-table empty-hash-table fix-bound)
+
+(define-syntax (unless-in-table stx) 
+  (syntax-case stx ()
+    [(_ table val . body)
+     (quasisyntax/loc stx
+       (hash-ref table val #,(syntax/loc #'body (lambda () . body))))]))
+
+
+;; free-variance.ss ends here
diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss
index c3bd256e..a23d9c75 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -28,6 +28,8 @@
 ;; t must be a Type
 (dt Scope ([t (or/c Type/c Scope?)]) [#:key (Type-key t)])
 
+
+
 (define (scope-depth k)
   (flat-named-contract 
    (format "Scope of depth ~a" k)
@@ -100,7 +102,7 @@
 (dt Poly (n body) #:no-provide 
     [#:contract (->d ([n natural-number/c]
                       [body (scope-depth n)])
-                     ()
+                     ([_ any/c])
                      [result Poly?])]
     [#:frees (free-vars* body) (without-below n (free-idxs* body))]
     [#:fold-rhs (let ([body* (remove-scopes n body)])
@@ -113,7 +115,7 @@
 (dt PolyDots (n body) #:no-provide
     [#:contract (->d ([n natural-number/c]
                       [body (scope-depth n)])
-                     ()
+                     ([_ any/c])
                      [result PolyDots?])]
     [#:key (Type-key body)]
     [#:frees (free-vars* body) (without-below n (free-idxs* body))]
@@ -229,17 +231,21 @@
 
 ;; elems : Listof[Type]
 (dt Union ([elems (and/c (listof Type/c)                         
-                         (lambda (es)
-                           (let-values ([(sorted? k)
-                                         (for/fold ([sorted? #t]
-                                                    [last -1])
-                                           ([e es])
-                                           (let ([seq (Type-seq e)])
-                                             (values
-                                              (and sorted?
-                                                   (< last seq))
-                                              seq)))])
-                             sorted?)))]) 
+                         (flat-named-contract
+                          'sorted-types
+                          (lambda (es)
+                            (let-values ([(sorted? k)
+                                          (for/fold ([sorted? #t]
+                                                     [last -1])
+                                            ([e es])
+                                            (let ([seq (Type-seq e)])
+                                              (values
+                                               (and sorted?
+                                                    (< last seq))
+                                               seq)))])
+                              (unless sorted?
+                                (printf "seqs ~a~n" (map Type-seq es)))
+                              sorted?))))]) 
     [#:frees (combine-frees (map free-vars* elems))
              (combine-frees (map free-idxs* elems))]
     [#:fold-rhs ((get-union-maker) (map type-rec-id elems))]
@@ -341,7 +347,7 @@
         [_ (int-err "Tried to remove too many scopes: ~a" sc)])))
 
 ;; type equality
-(define type-equal? eq?)
+(define (type-equal? t1 t2) (eq? (Type-seq t1) (Type-seq t2)))
 
 ;; inequality - good
 
@@ -465,8 +471,8 @@
 #;(trace instantiate-many abstract-many)
 
 ;; the 'smart' constructor
-(define (Mu* name body)    
-  (let ([v (*Mu (abstract name body))])
+(define (Mu* name body [print-name #f])    
+  (let ([v (*Mu (abstract name body) print-name)])
     (hash-set! name-table v name)
     v))
 
@@ -477,9 +483,9 @@
      (instantiate (*F name) scope)]))
 
 ;; the 'smart' constructor
-(define (Poly* names body)
+(define (Poly* names body [print-name #f])
   (if (null? names) body
-      (let ([v (*Poly (length names) (abstract-many names body))])
+      (let ([v (*Poly (length names) (abstract-many names body) print-name)])
         (hash-set! name-table v names)
         v)))
 
@@ -492,9 +498,9 @@
      (instantiate-many (map *F names) scope)]))
 
 ;; the 'smart' constructor
-(define (PolyDots* names body)
+(define (PolyDots* names body [print-name #f])
   (if (null? names) body
-      (let ([v (*PolyDots (length names) (abstract-many names body))])
+      (let ([v (*PolyDots (length names) (abstract-many names body) print-name)])
         (hash-set! name-table v names)
         v)))
 
@@ -610,6 +616,7 @@
  remove-dups
  sub-lf sub-lo sub-pe
  Values: Values? Values-rs
+ Type-key Type-seq Type-name type-case
  (rename-out [Mu:* Mu:]               
              [Poly:* Poly:]
              [PolyDots:* PolyDots:]
diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss
index 4c214123..89a37e48 100644
--- a/collects/typed-scheme/typecheck/tc-app.ss
+++ b/collects/typed-scheme/typecheck/tc-app.ss
@@ -606,15 +606,33 @@
        #:return (or expected (ret (Un)))
        (string-append "No function domains matched in function application:\n"
                       (domain-mismatches t doms rests drests rngs argtys-t #f #f))))]
-    ;; polymorphic functions without dotted rest, and without mandatory keyword args
+    ;; any kind of polymorphic function
+    [((tc-result1: (and t (PolyDots: 
+                           (and vars (list fixed-vars ... dotted-var))
+                           (Function: (list (and arrs (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...))) ...)))))
+      (list (tc-result1: argtys-t) ...))
+     (handle-clauses (doms rngs rests drests arrs) f-stx args-stx
+                     ;; only try inference if the argument lengths are appropriate
+                     (lambda (dom _ rest drest a) 
+                       (cond [rest (<= (length dom) (length argtys))]
+                             [drest (and (<= (length dom) (length argtys))
+                                         (eq? dotted-var (cdr drest)))]
+                             [else (= (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 drest a) 
+                       (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 vars argtys-t dom rest rng (fv rng) 
+                                         (and expected (tc-results->values expected)))))
+                     t argtys expected)]
+    ;; regular polymorphic functions without dotted rest, and without mandatory keyword args
     [((tc-result1: 
        (and t
-            (or (Poly: 
-                 vars 
-                 (Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...)))
-                (PolyDots: 
-                 vars
-                 (Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...))))))
+            (Poly: 
+             vars 
+             (Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...)))))
       (list (tc-result1: argtys-t) ...))
      (handle-clauses (doms rngs rests arrs) f-stx args-stx
                      ;; only try inference if the argument lengths are appropriate
@@ -623,17 +641,6 @@
                      ;; 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 argtys-t dom rest rng (fv rng) (and expected (tc-results->values expected))))
                      t argtys expected)]
-    ;; polymorphic ... type
-    [((tc-result1: (and t (PolyDots: 
-                           (and vars (list fixed-vars ... dotted-var))
-                           (Function: (list (and arrs (arr: doms rngs (and #f rests) (cons dtys dbounds) (list (Keyword: _ _ #f) ...))) ...)))))
-      (list (tc-result1: argtys-t) ...))
-     (handle-clauses (doms dtys dbounds rngs arrs) f-stx args-stx
-                     (lambda (dom dty dbound rng arr) (and (<= (length dom) (length argtys))
-                                                           (eq? dotted-var dbound)))
-                     (lambda (dom dty dbound rng arr) 
-                       (infer/dots fixed-vars dotted-var argtys-t dom dty rng (fv rng) #:expected (and expected (tc-results->values expected))))
-                     t argtys expected)]
     ;; procedural structs
     [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _))) _)
      (tc/funapp f-stx #`(#,(syntax/loc f-stx dummy) . #,args-stx) (ret proc-ty) (cons ftype0 argtys) expected)]
diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss
index 4ebd614f..ea31a542 100644
--- a/collects/typed-scheme/types/abbrev.ss
+++ b/collects/typed-scheme/types/abbrev.ss
@@ -2,7 +2,7 @@
 
 (require "../utils/utils.ss")
 
-(require (rep type-rep object-rep filter-rep)
+(require (except-in (rep type-rep object-rep filter-rep rep-utils) Dotted)
 	 "printer.ss" "utils.ss"
          (utils tc-utils)
          scheme/list
@@ -15,8 +15,17 @@
 (provide (all-defined-out)
          (rename-out [make-Listof -lst]))
 
-;; convenient constructors
+(define (add-name type name)
+  (define-values (struct-type skipped?) (struct-info type))
+  (define mk (struct-type-make-constructor struct-type))
+  (define flds (vector->list (struct->vector type)))
+  (when skipped?
+    (error "shouldn't skip"))
+  (match flds
+    [(list* _ fld1 fld2 old-name flds)
+     (apply mk fld1 fld2 (or old-name name) flds)]))
 
+;; convenient constructors
 
 (define -App make-App)
 (define -pair make-Pair)
@@ -121,7 +130,7 @@
 
 (define -Zero (-val 0))
 (define -Real (*Un -Flonum -ExactRational))
-(define -ExactNonnegativeInteger (*Un -Zero -ExactPositiveInteger))
+(define -ExactNonnegativeInteger (*Un -ExactPositiveInteger -Zero))
 (define -Nat -ExactNonnegativeInteger)
 
 (define -Byte -Number)
diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss
index f281022b..17fb639e 100644
--- a/collects/typed-scheme/types/convenience.ss
+++ b/collects/typed-scheme/types/convenience.ss
@@ -46,19 +46,19 @@
 
 (define In-Syntax
   (-mu e
-       (*Un -Number -Boolean -Symbol -String -Keyword -Char
+       (*Un -Boolean -Symbol -String -Keyword -Char -Number
             (make-Vector (-Syntax e))
             (make-Box (-Syntax e))
             (-mu list
                  (*Un (-val '())
                       (-pair (-Syntax e)
-                             (*Un (-Syntax e) list)))))))
+                             (*Un list (-Syntax e))))))))
 
 (define Any-Syntax (-Syntax In-Syntax))
 
 (define (-Sexpof t)
   (-mu sexp
-       (Un -Number -Boolean -Symbol -String -Keyword -Char
+       (Un -Boolean -Symbol -String -Keyword -Char -Number
            (-val '())
            (-pair sexp sexp)
            (make-Vector sexp)
diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss
index 33d6602b..ac650fdb 100644
--- a/collects/typed-scheme/types/printer.ss
+++ b/collects/typed-scheme/types/printer.ss
@@ -131,6 +131,7 @@
       [(Value: '()) null]))
   (match c 
     [(Univ:) (fp "Any")]
+    [(? Type-name) (fp "~a" (Type-name c))]
     [(? has-name?) (fp "~a" (has-name? c))]
     ;; names are just the printed as the original syntax
     [(Name: stx) (fp "~a" (syntax-e stx))]
diff --git a/collects/typed-scheme/types/remove-intersect.ss b/collects/typed-scheme/types/remove-intersect.ss
index 1dce9f4d..8400f7e6 100644
--- a/collects/typed-scheme/types/remove-intersect.ss
+++ b/collects/typed-scheme/types/remove-intersect.ss
@@ -1,7 +1,8 @@
 #lang scheme/base
 
 (require "../utils/utils.ss" 
-	 (rep type-rep rep-utils)
+	 (rep type-rep)
+         (only-in (rep rep-utils) Type-key)
 	 (types union subtype resolve convenience utils)
          scheme/match mzlib/trace)
 
diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss
index be894406..a41c83f3 100644
--- a/collects/typed-scheme/types/subtype.ss
+++ b/collects/typed-scheme/types/subtype.ss
@@ -1,6 +1,6 @@
 #lang scheme/base
 (require "../utils/utils.ss"
-         (rep type-rep filter-rep object-rep rep-utils)
+         (except-in (rep type-rep filter-rep object-rep rep-utils) Dotted)
          (utils tc-utils)
 	 (types utils comparison resolve abbrev)
          (env type-name-env)
diff --git a/collects/typed-scheme/types/union.ss b/collects/typed-scheme/types/union.ss
index 5019cada..d71a07a6 100644
--- a/collects/typed-scheme/types/union.ss
+++ b/collects/typed-scheme/types/union.ss
@@ -2,7 +2,7 @@
 
 (require "../utils/utils.ss")
 
-(require (rep type-rep rep-utils)
+(require (rep type-rep)
 	 (utils tc-utils)
 	 (types utils subtype abbrev printer comparison)
          scheme/match mzlib/trace)
diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss
index affbc234..10b08828 100644
--- a/collects/typed-scheme/types/utils.ss
+++ b/collects/typed-scheme/types/utils.ss
@@ -2,9 +2,8 @@
 
 (require "../utils/utils.ss")
 
-(require (rep type-rep filter-rep object-rep rep-utils)
+(require (except-in (rep type-rep filter-rep object-rep rep-utils) Dotted)
          (utils tc-utils)
-         (only-in (rep free-variance) combine-frees)
          scheme/match
          scheme/list
          mzlib/trace
diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss
index 8300d461..77f5ae15 100644
--- a/collects/typed-scheme/utils/utils.ss
+++ b/collects/typed-scheme/utils/utils.ss
@@ -145,7 +145,7 @@ at least theoretically.
 ;; - 1 printers have to be defined at the same time as the structs
 ;; - 2 we want to support things printing corectly even when the custom printer is off
 
-(define-for-syntax printing? #t)
+(define-for-syntax printing? #f)
 
 (define-syntax-rule (defprinter t ...)
   (begin
@@ -170,16 +170,16 @@ at least theoretically.
   
 (define-syntax (define-struct/printer stx)
   (syntax-case stx ()
-    [(form name (flds ...) printer)
+    [(form name (flds ...) printer . props)
      #`(define-struct/properties name (flds ...) 
          #,(if printing?
-               #'([prop:custom-write (lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))]) 
-               #'([prop:custom-write pseudo-printer]))
+               #'([prop:custom-write (lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))] . props) 
+               #'([prop:custom-write pseudo-printer] . props))
          #f)]))
 
 
 ;; turn contracts on and off - off by default for performance.
-(define-for-syntax enable-contracts? #f)
+(define-for-syntax enable-contracts? #t)
 (provide (for-syntax enable-contracts?) p/c w/c cnt d-s/c d/c)
 
 ;; these are versions of the contract forms conditionalized by `enable-contracts?'
diff --git a/collects/typed/net/cgi.ss b/collects/typed/net/cgi.ss
index 9318478a..ee070c78 100644
--- a/collects/typed/net/cgi.ss
+++ b/collects/typed/net/cgi.ss
@@ -3,6 +3,7 @@
 (require typed/private/utils)
 
 (require-typed-struct cgi-error () net/cgi)
+
 (require-typed-struct (incomplete-%-suffix cgi-error)  ([chars : (Listof Char)]) net/cgi) 
 (require-typed-struct (invalid-%-suffix cgi-error)  ([char : Char]) net/cgi)