diff --git a/collects/typed-scheme/infer/constraint-structs.ss b/collects/typed-scheme/infer/constraint-structs.ss
index a676a8fbd5..1fbf974271 100644
--- a/collects/typed-scheme/infer/constraint-structs.ss
+++ b/collects/typed-scheme/infer/constraint-structs.ss
@@ -1,6 +1,6 @@
 #lang scheme/base
 
-(require "../utils/utils.ss" (rep type-rep) scheme/contract)
+(require "../utils/utils.ss" (rep type-rep) scheme/contract scheme/match (for-syntax scheme/base syntax/parse))
 
 ;; S, T types
 ;; X a var
@@ -29,7 +29,13 @@
 ;; don't want to rule them out too early
 (define-struct cset (maps) #:prefab)
 
-(p/c (struct c ([S Type?] [X symbol?] [T Type?]))
+(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)))])))
+
+(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?]))
diff --git a/collects/typed-scheme/infer/constraints.ss b/collects/typed-scheme/infer/constraints.ss
index 54d0495dd9..b08341d4b5 100644
--- a/collects/typed-scheme/infer/constraints.ss
+++ b/collects/typed-scheme/infer/constraints.ss
@@ -13,7 +13,7 @@
 
 
 (define-values (fail-sym exn:infer?)
-  (let ([sym (gensym)])
+  (let ([sym (gensym 'infer-fail)])
     (values sym (lambda (s) (eq? s sym)))))
 
 ;; why does this have to be duplicated?
diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss
index 265371b10d..eff88dd22e 100644
--- a/collects/typed-scheme/infer/infer-unit.ss
+++ b/collects/typed-scheme/infer/infer-unit.ss
@@ -12,7 +12,7 @@
          scheme/match
          mzlib/etc
          mzlib/trace
-	 unstable/sequence unstable/list
+	 unstable/sequence unstable/list unstable/debug
          scheme/list)
 
 (import dmap^ constraints^ promote-demote^)
@@ -254,7 +254,7 @@
     (insert empty X S T))
   (if (seen? S T)
       empty
-      (parameterize ([match-equality-test type-equal?]
+      (parameterize ([match-equality-test (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))]
                      [current-seen (remember S T (current-seen))])
         (match* 
             (S T)
@@ -428,7 +428,7 @@
     (match v
       [(struct c (S X T))
        (let ([var (hash-ref (free-vars* R) (or variable X) Constant)])
-         ;(printf "variance was: ~a~nR was ~a~nX was ~a~n" var R (or variable X))
+         ;(printf "variance was: ~a~nR was ~a~nX was ~a~nS T ~a ~a~n" var R (or variable X) S T)
          (evcase var 
                  [Constant S]
                  [Covariant S]
@@ -440,7 +440,7 @@
      (check-vars
       must-vars
       (append 
-       (for/list ([(k dc) dm])
+       (for/list ([(k dc) (in-hash dm)])
          (match dc
            [(struct dcon (fixed rest))
             (list k
@@ -452,7 +452,7 @@
                   (for/list ([f fixed])
                     (constraint->type f #:variable k))
                   (constraint->type rest))]))
-       (for/list ([(k v) cmap])
+       (for/list ([(k v) (in-hash cmap)])
          (list k (constraint->type v)))))]))
 
 (define (cgen/list V X S T)
diff --git a/collects/typed-scheme/private/base-env-indexing-abs.ss b/collects/typed-scheme/private/base-env-indexing-abs.ss
index 61bdf5b612..1676ca26bd 100644
--- a/collects/typed-scheme/private/base-env-indexing-abs.ss
+++ b/collects/typed-scheme/private/base-env-indexing-abs.ss
@@ -44,6 +44,18 @@
        (-StrRx   -String [N ?N ?outp] . ->opt . (optlist -String))
        (-BtsRx   -String [N ?N ?outp] . ->opt . (optlist -Bytes))
        (-Pattern -InpBts [N ?N ?outp] . ->opt . (optlist -Bytes))))]
+   [regexp-match?
+    (let ([?outp   (-opt -Output-Port)]
+          [N       -Nat]
+          [?N      (-opt -Nat)]
+          [optlist (lambda (t) (-opt (-lst (-opt t))))]
+          [-StrRx  (Un -String -Regexp -PRegexp)]
+          [-BtsRx  (Un -Bytes  -Byte-Regexp -Byte-PRegexp)]
+          [-InpBts (Un -Input-Port -Bytes)])
+      (cl->*
+       (-StrRx   -String [N ?N ?outp] . ->opt . -Boolean)
+       (-BtsRx   -String [N ?N ?outp] . ->opt . -Boolean)
+       (-Pattern -InpBts [N ?N ?outp] . ->opt . -Boolean)))]
    [regexp-match*
     (let ([N       -Nat]
           [?N      (-opt -Nat)]
diff --git a/collects/typed-scheme/rep/filter-rep.ss b/collects/typed-scheme/rep/filter-rep.ss
index e3a95d3000..1ae4f5ab6b 100644
--- a/collects/typed-scheme/rep/filter-rep.ss
+++ b/collects/typed-scheme/rep/filter-rep.ss
@@ -43,14 +43,14 @@
      [#:contract (->d ([t (cond [(ormap Bot? t)
                                  (list/c Bot?)]
                                 [(ormap Bot? e)
-                                 (list/c)]
+                                 (flat-named-contract "e was Bot" (list/c))]
                                 [else (listof Filter/c)])]
                        [e (cond [(ormap Bot? e)
                                  (list/c Bot?)]
                                 [(ormap Bot? t)
-                                 (list/c)]
+                                 (flat-named-contract "t was Bot" (list/c))]
                                 [else (listof Filter/c)])])
-                      ()
+                      (#:syntax [stx #f])
                       [result FilterSet?])])
 
 ;; represents no info about the filters of this expression
@@ -82,14 +82,14 @@
      [#:contract (->d ([t (cond [(ormap LBot? t)
                                  (list/c LBot?)]
                                 [(ormap LBot? e)
-                                 (list/c)]
+                                 (flat-named-contract "e was LBot" (list/c))]
                                 [else (listof LatentFilter/c)])]
                        [e (cond [(ormap LBot? e)
                                  (list/c LBot?)]
                                 [(ormap LBot? t)
-                                 (list/c)]
+                                 (flat-named-contract "t was LBot" (list/c))]
                                 [else (listof LatentFilter/c)])])
-                      ()
+                      (#:syntax [stx #f])
                       [result LFilterSet?])])
 
 (define FilterSet/c
diff --git a/collects/typed-scheme/rep/free-variance.ss b/collects/typed-scheme/rep/free-variance.ss
index 6b87ae6316..c42f9c6bb1 100644
--- a/collects/typed-scheme/rep/free-variance.ss
+++ b/collects/typed-scheme/rep/free-variance.ss
@@ -4,9 +4,12 @@
          (utils tc-utils) scheme/list
          mzlib/etc scheme/contract)
 
+(provide Covariant Contravariant Invariant Constant Dotted
+         combine-frees flip-variances without-below unless-in-table empty-hash-table
+         fix-bound make-invariant variance?)
+
 ;; 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)
@@ -19,31 +22,11 @@
     (values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted))))
 
 
-(provide Covariant Contravariant Invariant Constant Dotted)
-
 (define (variance? e)
   (memq e (list 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 tbl) val) (hash-ref tbl val #f))
-
-(define (free-idxs* t)
-  (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" t))))
-(define (free-vars* t)
-  (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table" t))))
-
 (define empty-hash-table (make-immutable-hasheq null))
 
-(p/c [free-vars* (-> (input/c var-table) (hash/c symbol? variance?))]
-     [free-idxs* (-> (input/c index-table) (hash/c exact-nonnegative-integer? variance?))])
-
-(provide empty-hash-table make-invariant)
-
 ;; frees = HT[Idx,Variance] where Idx is either Symbol or Number
 ;; (listof frees) -> frees
 (define (combine-frees freess)    
@@ -78,8 +61,7 @@
 (define (flip-variances vs)
   (hash-map* 
    (lambda (k v) 
-     (evcase 
-         v
+     (evcase v
        [Covariant Contravariant]
        [Contravariant Covariant]
        [v v]))
@@ -102,9 +84,6 @@
        (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)
diff --git a/collects/typed-scheme/rep/interning.ss b/collects/typed-scheme/rep/interning.ss
index 3dfd9aeffb..4a44449d69 100644
--- a/collects/typed-scheme/rep/interning.ss
+++ b/collects/typed-scheme/rep/interning.ss
@@ -5,21 +5,27 @@
 (provide defintern hash-id)
 
 (define-syntax (defintern stx)
+  (define-splicing-syntax-class extra-kw-spec
+    (pattern (~seq kw:keyword [name:id default:expr])
+             #:with formal #'(kw [name default])))
+  (define-splicing-syntax-class extra-spec
+    (pattern ek:extra-kw-spec
+             #:with e #'ek.name)
+    (pattern e:expr))
   (syntax-parse stx
-    [(_ name+args make-name key (~optional (~seq #:extra-arg e:expr)) ...)
-     (if (attribute e)
-         #'(defintern name+args (lambda () (make-hash #;'weak)) make-name key #:extra-arg e)
-         #'(defintern name+args (lambda () (make-hash #;'weak)) make-name key))]
-    [(_ (*name:id arg:id ...) make-ht make-name key-expr (~seq #:extra-arg e:expr) ...)
-     #'(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)))))))]))
+    [(_ name+args make-name key #:extra-args e ...)
+     #'(defintern name+args (lambda () (make-hash)) make-name key #:extra-args e ...)]
+    [(_ (*name:id arg:id ...) make-ht make-name key-expr #:extra-args . (~and ((~seq es:extra-spec) ...) ((~or (~seq ek:extra-kw-spec) e:expr) ...)))
+     (with-syntax ([((extra-formals ...) ...) #'(ek.formal ...)])
+       #'(define *name
+           (let ([table (make-ht)])
+             (lambda (arg ... extra-formals ... ...)
+               (let ([key key-expr])
+                 (hash-ref table key
+                           (lambda ()
+                             (let ([new (make-name (count!) es.e ... arg ...)])
+                               (hash-set! table key new)
+                               new))))))))]))
 
 (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 a0de7c5a30..8721b91305 100644
--- a/collects/typed-scheme/rep/rep-utils.ss
+++ b/collects/typed-scheme/rep/rep-utils.ss
@@ -25,22 +25,26 @@
 
 (provide == defintern hash-id (for-syntax fold-target))
 
+(define-struct Rep (seq free-vars free-idxs stx))
+
 (define-for-syntax fold-target #'fold-target)
+(define-for-syntax default-fields (list #'seq #'free-vars #'free-idxs #'stx))
 
 (define-for-syntax (mk par ht-stx key?)
   (define-syntax-class opt-cnt-id
     #:attributes (i cnt)
     (pattern i:id
              #:with cnt #'any/c)
-    (pattern [i:id cnt]))
-  (define-syntax-class no-provide-kw
-    (pattern #:no-provide))
-  (define-syntax-class idlist
-    #:attributes ((i 1) (cnt 1) fs)
+    (pattern [i:id cnt]))  
+  ;; fields
+  (define-syntax-class (idlist name)
+    #:attributes ((i 1) (cnt 1) fs maker pred (acc 1))
     (pattern (oci:opt-cnt-id ...)               
              #:with (i ...) #'(oci.i ...)
              #:with (cnt ...) #'(oci.cnt ...)
-             #:with fs #'(i ...)))
+             #:with fs #'(i ...)
+             #:with (_ maker pred acc ...) (build-struct-names name (syntax->list #'fs) #f #t name)))
+  
   (define (combiner f flds)
     (syntax-parse flds
       [() #'empty-hash-table]
@@ -48,130 +52,91 @@
       [(e ...) #`(combine-frees (list (#,f e) ...))]))
   (define-splicing-syntax-class frees-pat
     #:transparent
-    #:attributes (f1 f2 def)
-    (pattern (~seq f1:expr f2:expr)
-             #:with def #'(begin))
+    #:attributes (f1 f2)
+    (pattern (~seq f1:expr f2:expr))
     (pattern #f
              #:with f1 #'empty-hash-table
-             #:with f2 #'empty-hash-table
-             #:with def #'(begin))
+             #:with f2 #'empty-hash-table)
     (pattern e:expr
-             #:with id (generate-temporary)
-             #:with def #'(define id e)
-             #:with f1 #'(id free-vars*)
-             #:with f2 #'(id free-idxs*)))
-  (define-syntax-class fold-pat
+             #:with f1 #'(e Rep-free-vars)
+             #:with f2 #'(e Rep-free-idxs)))
+  (define-syntax-class (fold-pat fold-name)
     #:transparent
-    #:attributes (e)
+    #:attributes (e proc)
     (pattern #:base
-             #:with e fold-target)
+             #:with e fold-target
+             #:with proc #`(procedure-rename
+                            (lambda () #,fold-target)
+                            '#,fold-name))
     (pattern ex:expr
-             #:with e #'#'ex))
+             #:with e #'#'ex
+             #:with proc #`(procedure-rename
+                            (lambda () #'ex)
+                            '#,fold-name)))
+  (define-syntax-class form-nm
+    (pattern nm:id
+             #:with ex (format-id #'nm "~a:" #'nm)
+             #:with fold (format-id #f "~a-fold" #'nm)
+             #:with kw (string->keyword (symbol->string (syntax-e #'nm)))
+             #:with *maker (format-id #'nm "*~a" #'nm)))
   (lambda (stx)          
     (syntax-parse stx 
-      [(dform nm:id flds:idlist (~or 
-                                 (~optional [#:key key-expr:expr])
-                                 (~optional [#:intern intern?:expr])
-                                 (~optional [#:frees frees:frees-pat])
-                                 (~optional [#:fold-rhs fold-rhs:fold-pat])
-                                 (~optional [#:contract cnt:expr])
-                                 (~optional no-provide?:no-provide-kw)) ...)
-       (with-syntax* 
-        ([ex (format-id #'nm "~a:" #'nm)]
-         [fold-name (format-id #f "~a-fold" #'nm)]
-         [kw-stx (string->keyword (symbol->string (attribute nm.datum)))]
-         [parent par]
-         [(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds.fs) #f #t #'nm)]
-         [*maker (format-id #'nm "*~a" #'nm)]
-         [**maker (format-id #'nm "**~a" #'nm)]
-         [*maker-cnt (if enable-contracts?
-                         (or (attribute cnt) #'(flds.cnt ... . -> . pred))
-                         #'any/c)]
-         [ht-stx ht-stx]
-         [bfs-fold-rhs (cond [(attribute fold-rhs)
-                              #`(procedure-rename
-                                 (lambda () #,#'fold-rhs.e)
-                                 'fold-name)]
-                             ;; otherwise we assume that everything is a type, 
-                             ;; and recur on all the arguments
-                             [else #'(procedure-rename
-                                      (lambda () 
-                                        #`(*maker (#,type-rec-id flds.i) ...))
-                                      'fold-name)])]
+      [(dform nm:form-nm
+              (~var flds (idlist #'nm))
+              (~or 
+               (~optional (~and (~fail #:unless key? "#:key not allowed")
+                                [#:key key-expr:expr])
+                          #:defaults ([key-expr #'#f]))
+               (~optional [#:intern intern?:expr]
+                          #:defaults
+                          ([intern? (syntax-parse #'flds.fs
+                                      [() #'#f]
+                                      [(f) #'f]
+                                      [(fs ...) #'(list fs ...)])]))
+               (~optional [#:frees frees:frees-pat]
+                          #:defaults 
+                          ([frees.f1 (combiner #'Rep-free-vars #'flds.fs)]
+                           [frees.f2 (combiner #'Rep-free-idxs #'flds.fs)]))
+               (~optional [#:fold-rhs (~var fold-rhs (fold-pat #'nm.fold))]
+                          #:defaults
+                          ([fold-rhs.proc
+                            #'(procedure-rename
+                               (lambda () 
+                                 #`(nm.*maker (#,type-rec-id flds.i) ...))
+                               'nm.fold)]))
+               (~optional [#:contract cnt:expr]
+                          #:defaults ([cnt #'((flds.cnt ...) (#:syntax (or/c syntax? #f)) . ->* . flds.pred)]))
+               (~optional (~and #:no-provide no-provide?))) ...)
+       (with-syntax
+        ([(ign-pats ...) (append (map (lambda (x) #'_) default-fields) (if key? (list #'_) (list)))]
+         ;; has to be down here to refer to #'cnt
          [provides (if (attribute no-provide?)
-                       #'(begin)                                 
-                       #`(begin 
-                           (provide #;nm ex pred acc ...)
-                           (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? #'(_ _) #'(_))]
-         [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)))])
-            (quasisyntax/loc stx
-		(w/c nm ([*maker *maker-cnt])
-                   (define (*maker . flds.fs)
-                     (define v (**maker . flds.fs))
-                     frees-def
-                     (unless-in-table 
-                      var-table v
-                      (define fvs f1)
-                      (define fis f2)
-                      (hash-set! var-table v fvs)
-                      (hash-set! index-table v fis))
-                     v))))])
+                       #'(begin)
+                       #'(begin 
+                           (provide nm.ex flds.pred flds.acc ...)
+                           (p/c (rename nm.*maker flds.maker cnt))))])
         #`(begin
-            (define-struct (nm parent) flds.fs #:inspector #f)
-            (define-match-expander ex
+            (define-struct (nm #,par) flds.fs #:inspector #f)
+            (define-match-expander nm.ex
               (lambda (s)
                 (syntax-parse s 
                   [(_ . fs) 
                    #:with pat (syntax/loc s (ign-pats ... . fs))
                    (syntax/loc s (struct nm pat))])))
             (begin-for-syntax
-              (hash-set! ht-stx 'kw-stx (list #'ex #'flds.fs bfs-fold-rhs #'#,stx)))
-            (w/c nm ()
-		 intern
-		 frees)
-	    provides))])))
+              (hash-set! #,ht-stx 'nm.kw (list #'nm.ex #'flds.fs fold-rhs.proc #f)))
+            #,(quasisyntax/loc stx
+                (w/c nm ([nm.*maker cnt])
+                     #,(quasisyntax/loc #'nm
+                         (defintern (nm.*maker . flds.fs) flds.maker intern?
+                           #:extra-args
+                           frees.f1 frees.f2 #:syntax [orig-stx #f] 
+                           #,@(if key? (list #'key-expr) null)))))
+            provides))])))
 
 (define-for-syntax (mk-fold ht type-rec-id rec-ids kws)
   (lambda (stx)
-    (define new-ht (hash-copy ht))
-    (define (mk-matcher kw) 
-      (datum->syntax stx (string->symbol (string-append (keyword->string kw) ":"))))
-    (define/contract (put k lst)
-      (keyword? (list/c syntax?
-                        syntax?
-                        (-> syntax?)
-                        syntax?) 
-                . -> . void?)
-      (hash-set! new-ht k lst))
-    (define (add-clause cl)
-      (syntax-parse cl
-        [(kw:keyword #:matcher mtch pats ... expr)
-         (put (syntax-e #'kw) (list #'mtch 
-                                    (syntax/loc cl (pats ...))
-                                    (lambda () #'expr)
-                                    cl))]
-        [(kw:keyword pats ... expr) 
-         (put (syntax-e #'kw) (list (mk-matcher (syntax-e #'kw)) 
-                                    (syntax/loc cl (pats ...))
-                                    (lambda () #'expr)
-                                    cl))]))
+    (define new-ht (hash-copy ht))    
     (define-syntax-class clause
       (pattern  
        (k:keyword #:matcher mtch pats ... e:expr)
@@ -183,111 +148,105 @@
       (pattern
        (k:keyword pats ... e:expr) 
        #:attr kw (syntax-e #'k)
-       #:attr val (list (mk-matcher (attribute kw)) 
+       #:attr val (list (format-id stx "~a:" (attribute kw))
                         (syntax/loc this-syntax (pats ...))
                         (lambda () #'e)
                         this-syntax)))
     (define (gen-clause k v)
       (match v
         [(list match-ex pats body-f src)
-         (let ([pat (quasisyntax/loc src (#,match-ex  . #,pats))])
-           (quasisyntax/loc src (#,pat #,(body-f))))]))
+         (let ([pat (quasisyntax/loc (or stx stx) (#,match-ex  . #,pats))])
+           (quasisyntax/loc (or src stx) (#,pat #,(body-f))))]))
     (define-syntax-class (keyword-in kws)
       #:attributes (datum)
       (pattern k:keyword
-               #:fail-unless (memq (attribute k.datum) kws) #f
+               #:fail-unless (memq (attribute k.datum) kws) (format "expected keyword in ~a" kws)
                #:attr datum (attribute k.datum)))
     (define-syntax-class (sized-list kws)
       #:description (format "keyword expr pairs matching with keywords in the list ~a" kws)
-      (pattern ((~or (~seq k e:expr)) ...)
-               #:declare k (keyword-in kws)
-               #:fail-unless (equal? (length (attribute k.datum)) (length (remove-duplicates (attribute k.datum)))) #f
+      (pattern ((~or (~seq (~var k (keyword-in kws)) e:expr)) ...)
+               #:when (equal? (length (attribute k.datum)) 
+                              (length (remove-duplicates (attribute k.datum))))
                #:attr mapping (for/hash ([k* (attribute k.datum)]
                                          [e* (attribute e)])
-                                (values k* e*))
-               ))
+                                (values k* e*))))
     (syntax-parse stx
-      [(tc recs ty clauses:clause ...)
-       #:declare recs (sized-list kws)
-       (begin 
-         (for ([k (attribute clauses.kw)]
-               [v (attribute clauses.val)])
-           (put k v))
-         (with-syntax ([(let-clauses ...)
-                        (for/list ([rec-id rec-ids]
-                                   [k kws])
-                          #`[#,rec-id #,(hash-ref (attribute recs.mapping) k
-                                                  #'values)])])
-           #`(let (let-clauses ...
-                   [#,fold-target ty])
-               ;; then generate the fold
-               #,(quasisyntax/loc stx
-                   (match #,fold-target
-                     #,@(hash-map new-ht gen-clause))))))])))
+      [(tc (~var recs (sized-list kws)) ty clauses:clause ...)
+       (for ([k (attribute clauses.kw)]
+             [v (attribute clauses.val)])
+         (hash-set! new-ht k v))
+       (with-syntax ([(let-clauses ...)
+                      (for/list ([rec-id rec-ids]
+                                 [k kws])
+                        #`[#,rec-id #,(hash-ref (attribute recs.mapping) k
+                                                #'values)])]
+                     [(match-clauses ...)
+                      (hash-map new-ht gen-clause)])
+         #`(let (let-clauses ...
+                 [#,fold-target ty])
+             ;; then generate the fold
+             #,(quasisyntax/loc stx
+                 (match #,fold-target
+                   match-clauses ...))))])))
 
 
-(define-syntax (make-prim-type stx)
-  (define default-flds #'(seq))
+(define-syntax (make-prim-type stx)    
   (define-syntax-class type-name-base
-    #:attributes (i lower-s first-letter key? (fld-names 1))
+    #:attributes (i d-id key? (fld-names 1))
     #:transparent
-    (pattern i:id
-             #:attr lower-s (string-downcase (symbol->string (attribute i.datum)))
-             #:with (fld-names ...) default-flds
-	     #:with key? #'#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
-             #:attr first-letter (symbol->string (attribute d-name.datum)))
-    (pattern [i:id #:key]
-             #:with (fld-names ...) (datum->syntax #f (append (syntax->list default-flds) 
-                                                              (syntax->list #'(key))))
-             #:attr lower-s (string-downcase (symbol->string (attribute i.datum)))
-	     #:with key? #'#t
-             #:attr first-letter (string-ref (attribute lower-s) 0)))
+    (pattern [i:id (~optional (~and #:key
+                                    (~bind [key? #'#t]
+                                           [(fld-names 1) (list #'key)]))
+                              #:defaults ([key? #'#f]
+                                          [(fld-names 1) null]))
+                   #:d d-id:id]))
   (define-syntax-class type-name
     #:transparent
     #:auto-nested-attributes
     (pattern :type-name-base
+             #:with lower-s (string->symbol (string-downcase (symbol->string (syntax-e #'i))))
              #:with name #'i
-             #:with keyword (datum->syntax #f (string->keyword (symbol->string (syntax-e #'i))))
+             #:with keyword (string->keyword (symbol->string (syntax-e #'i)))
              #:with tmp-rec-id (generate-temporary)
-             #:with case (format-id #'i "~a-case" (attribute lower-s))
-             #:with printer (format-id #'i "print-~a*" (attribute lower-s))
-             #: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 case (format-id #'i "~a-case" #'lower-s)
+             #:with printer (format-id #'i "print-~a*" #'lower-s)
+             #:with ht (format-id #'i "~a-name-ht" #'lower-s)
+             #:with rec-id (format-id #'i "~a-rec-id" #'lower-s)
              #:with (_ _ pred? accs ...)
-                    (datum->syntax #f (build-struct-names #'name (syntax->list #'(fld-names ...)) #f #t #'name))))
+                    (build-struct-names #'name (syntax->list #'(fld-names ...)) #f #t #'name)))
   (syntax-parse stx
     [(_ i:type-name ...)
-     (with-syntax* ([(fresh-ids ...) (generate-temporaries #'(i.name ...))]
-                    [(default-ids ...) (generate-temporaries #'(i.name ...))]
-                    [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 ... ...
-                    (for-syntax i.ht ... i.rec-id ...))
-           (define-syntax i.d-id (mk #'i.name #'i.ht i.key?)) ...
-           (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-for-syntax i.rec-id #'i.rec-id) ...   
-           (provide i.case ...)           
-           (define-syntaxes (i.case ...)
-             (let ()               
-               (apply values
-                      (map (lambda (ht) 
-                             (mk-fold ht 
-                                      (car (list #'i.rec-id ...))
-                                      (list #'i.rec-id ...)
-                                      '(i.keyword ...)))
-                           (list i.ht ...)))))))]))
+     #'(begin
+         (provide i.d-id ... i.printer ... i.name ... i.pred? ... i.accs ... ...
+                  (for-syntax i.ht ... i.rec-id ...))
+         (define-syntax i.d-id (mk #'i.name #'i.ht i.key?)) ...
+         (define-for-syntax i.ht (make-hasheq)) ...
+         (define-struct/printer (i.name Rep) (i.fld-names ...) (lambda (a b c) ((unbox i.printer) a b c))) ...
+         (define-for-syntax i.rec-id #'i.rec-id) ...   
+         (provide i.case ...)           
+         (define-syntaxes (i.case ...)
+           (let ()               
+             (apply values
+                    (map (lambda (ht) 
+                           (define rec-ids (list i.rec-id ...))
+                           (mk-fold ht 
+                                    (car rec-ids)
+                                    rec-ids
+                                    '(i.keyword ...)))
+                         (list i.ht ...))))))]))
 
-(make-prim-type [Type #:key]
-                Filter
-                [LatentFilter #:d lf]
-                Object 
-                [LatentObject #:d lo]
-                [PathElem #:d pe])
+(make-prim-type [Type #:key #:d dt]
+                [Filter #:d df]
+                [LatentFilter #:d dlf]
+                [Object #:d do] 
+                [LatentObject #:d dlo]
+                [PathElem #:d dpe])
+
+(provide PathElem? (rename-out [Rep-seq Type-seq]
+                               [Rep-free-vars free-vars*]
+                               [Rep-free-idxs free-idxs*]))
+
+(p/c (struct Rep ([seq exact-nonnegative-integer?] 
+                  [free-vars (hash/c symbol? variance?)] 
+                  [free-idxs (hash/c exact-nonnegative-integer? variance?)]
+                  [stx (or/c #f syntax?)])))
diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss
index 1627f7af55..e9355e4d0b 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -100,7 +100,7 @@
 (dt Poly (n body) #:no-provide 
     [#:contract (->d ([n natural-number/c]
                       [body (scope-depth n)])
-                     ()
+                     (#:syntax [stx (or/c #f syntax?)])
                      [result Poly?])]
     [#:frees (free-vars* body) (without-below n (free-idxs* body))]
     [#:fold-rhs (let ([body* (remove-scopes n body)])
@@ -113,7 +113,7 @@
 (dt PolyDots (n body) #:no-provide
     [#:contract (->d ([n natural-number/c]
                       [body (scope-depth n)])
-                     ()
+                     (#:syntax [stx (or/c #f syntax?)])
                      [result PolyDots?])]
     [#:key (Type-key body)]
     [#:frees (free-vars* body) (without-below n (free-idxs* body))]
@@ -238,25 +238,24 @@
 ;; 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?)))]) 
+                           (or (null? es)
+                               (let-values ([(sorted? k)
+                                             (for/fold ([sorted? #t]
+                                                        [last (car es)])
+                                               ([e (cdr es)])
+                                               (values
+                                                (and sorted? (type<? last e))
+                                                e))])
+                                 sorted?))))]) 
     [#:frees (combine-frees (map free-vars* elems))
              (combine-frees (map free-idxs* elems))]
     [#:fold-rhs ((get-union-maker) (map type-rec-id elems))]
     [#:key (let loop ([res null] [ts elems])
-	     (if (null? ts) res
-		 (let ([k (Type-key (car ts))])
-		   (cond [(pair? k) (loop (append k res) (cdr ts))]
-			 [k (loop (cons k res) (cdr ts))]
-			 [else #f]))))])
+             (if (null? ts) res
+                 (let ([k (Type-key (car ts))])
+                   (cond [(pair? k) (loop (append k res) (cdr ts))]
+                         [k (loop (cons k res) (cdr ts))]
+                         [else #f]))))])
     
 (dt Univ () [#:frees #f] [#:fold-rhs #:base])
 
@@ -327,7 +326,8 @@
 
 ;; remove-dups: List[Type] -> List[Type]
 ;; removes duplicate types from a SORTED list
-(define (remove-dups types)
+(d/c (remove-dups types)
+  ((listof Rep?) . -> . (listof Rep?))
   (cond [(null? types) types]
         [(null? (cdr types)) types]
         [(type-equal? (car types) (cadr types)) (remove-dups (cdr types))]
@@ -349,15 +349,16 @@
         [_ (int-err "Tried to remove too many scopes: ~a" sc)])))
 
 ;; type equality
-(define type-equal? eq?)
+(d/c (type-equal? s t) (Rep? Rep? . -> . boolean?) (eq? (Rep-seq s) (Rep-seq t)))
 
 ;; inequality - good
+(d/c (type<? s t)
+  (Rep? Rep? . -> . boolean?)
+  (< (Rep-seq s) (Rep-seq t)))
 
-(define (type<? s t)
-  (< (Type-seq s) (Type-seq t)))
-
-(define (type-compare s t)
-  (cond [(eq? s t) 0]
+(d/c (type-compare s t)
+  (Rep? Rep? . -> . (or/c -1 0 1))
+  (cond [(type-equal? s t) 0]
         [(type<? s t) 1]
         [else -1]))
 
@@ -614,7 +615,7 @@
  Poly-n
  PolyDots-n
  free-vars*
- type-equal? type-compare type<?
+ type-compare type<?
  remove-dups
  sub-lf sub-lo sub-pe
  Values: Values? Values-rs
@@ -628,4 +629,6 @@
              [Poly-body* Poly-body]
              [PolyDots-body* PolyDots-body]))
 
+(p/c [type-equal? (Rep? Rep? . -> . boolean?)])
+
 ;(trace unfold)
diff --git a/collects/typed-scheme/typecheck/check-subforms-unit.ss b/collects/typed-scheme/typecheck/check-subforms-unit.ss
index 037822e2ee..945df04d88 100644
--- a/collects/typed-scheme/typecheck/check-subforms-unit.ss
+++ b/collects/typed-scheme/typecheck/check-subforms-unit.ss
@@ -3,7 +3,7 @@
 (require "../utils/utils.ss"
 	 syntax/kerncase
 	 syntax/parse
-         scheme/match
+         scheme/match unstable/debug
          "signatures.ss" "tc-metafunctions.ss"
          (types utils convenience union subtype)
 	 (utils tc-utils)
@@ -14,7 +14,7 @@
 
 ;; find the subexpressions that need to be typechecked in an ignored form
 ;; syntax -> any
-(define (check-subforms/with-handlers form)
+(define (check-subforms/with-handlers form [expected #f])
   (define handler-tys '())
   (define body-ty #f)    
   (define (get-result-ty t)
diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss
index ccb0cb5e85..9bc405ca06 100644
--- a/collects/typed-scheme/typecheck/tc-app.ss
+++ b/collects/typed-scheme/typecheck/tc-app.ss
@@ -511,13 +511,13 @@
     [(#%plain-app do-make-object cl (#%plain-app list . pos-args) (#%plain-app list (#%plain-app cons 'names named-args) ...))
      (check-do-make-object #'cl #'pos-args #'(names ...) #'(named-args ...))]
     ;; ormap/andmap of ... argument
-    [(#%plain-app or/andmap:id f arg)
-     #:fail-unless (or (free-identifier=? #'or/andmap #'ormap)
-                       (free-identifier=? #'or/andmap #'andmap)) #f
-     #:fail-unless (with-handlers ([exn:fail? (lambda _ #f)])
-                     (tc/dots #'arg)
-                     #t) #f
-     (let-values ([(ty bound) (tc/dots #'arg)])
+    [(#%plain-app (~or (~literal andmap) (~literal ormap)) f arg)
+     #:attr ty+bound
+     (with-handlers ([exn:fail? (lambda _ #f)])
+       (let-values ([(ty bound) (tc/dots #'arg)])
+         (list ty bound)))
+     #:when (attribute ty+bound)
+     (match-let ([(list ty bound) (attribute ty+bound)])
        (parameterize ([current-tvars (extend-env (list bound)
                                                  (list (make-DottedBoth (make-F bound)))
                                                  (current-tvars))])
diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss
index 6121a49fb5..6b31b3937b 100644
--- a/collects/typed-scheme/typecheck/tc-expr-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss
@@ -259,7 +259,7 @@
                                              (with-lexical-env/extend 
                                               (list or-part) (list (restrict t1 (-val #f))) (single-value e2 expected)))]
                     [t1* (remove t1 (-val #f))]
-                    [f1* (-FS fs+ (list (make-Bot)))])
+                    [f1* (-FS null (list (make-Bot)))])
          ;; if we have the same number of values in both cases
          (let ([r (combine-filter f1 f1* f2 t1* t2 o1 o2)])
            (if expected 
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index 2e790129d2..186c32507a 100644
--- a/collects/typed-scheme/typecheck/tc-metafunctions.ss
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -79,9 +79,12 @@
     [(ImpFilter: as cs)
      (let ([a* (apply append (for/list ([f as]) (abo xs idxs f)))]
            [c* (apply append (for/list ([f cs]) (abo xs idxs f)))])
-       (if (< (length a*) (length as)) ;; if we removed some things, we can't be sure
-           null
-           (list (make-LImpFilter a* c*))))]
+       (cond [(< (length a*) (length as)) ;; if we removed some things, we can't be sure
+              null]
+             [(null? c*) ;; this clause is now useless
+              null]
+             [else
+              (list (make-LImpFilter a* c*))]))]
     [_ null]))
 
 (define (merge-filter-sets fs)
@@ -118,8 +121,8 @@
   (define (idx= lf)
     (match lf
       [(LBot:) #t]
-      [(LNotTypeFilter: _ _ idx*) (type-equal? idx* idx)]
-      [(LTypeFilter: _ _ idx*) (type-equal? idx* idx)]))
+      [(LNotTypeFilter: _ _ idx*) (= idx* idx)]
+      [(LTypeFilter: _ _ idx*) (= idx* idx)]))
   (match lf
     [(LFilterSet: lf+ lf-)
      (make-LFilterSet (filter idx= lf+) (filter idx= lf-))]))
diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss
index 617d2693bb..49c7d942a3 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 (rep type-rep object-rep filter-rep rep-utils)
 	 "printer.ss" "utils.ss"
          (utils tc-utils)
          scheme/list
@@ -26,7 +26,7 @@
 (define -box make-Box)
 (define -vec make-Vector)
 (define -LFS make-LFilterSet)
-(define -FS make-FilterSet)
+(define-syntax -FS (make-rename-transformer #'make-FilterSet))
 
 (define-syntax *Un
   (syntax-rules ()
@@ -36,9 +36,7 @@
 (define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
 
 (define (-lst* #:tail [tail (-val null)] . args)
-  (if (null? args)
-      tail
-      (-pair (car args) (apply -lst* #:tail tail (cdr args)))))
+  (for/fold ([tl tail]) ([a (reverse args)]) (-pair a tl)))
 
 (define (-Tuple l)
   (foldr -pair (-val '()) l))
@@ -68,8 +66,10 @@
   (make-Result t f o))
 
 (d/c (-values args)
-     (c:-> (listof Type/c) Values?)
-     (make-Values (for/list ([i args]) (-result i))))
+     (c:-> (listof Type/c) (or/c Type/c Values?))
+     (match args
+       ;[(list t) t]
+       [_ (make-Values (for/list ([i args]) (-result i)))]))
 
 ;; basic types
 
diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss
index 15d818f675..4bcc45407f 100644
--- a/collects/typed-scheme/types/convenience.ss
+++ b/collects/typed-scheme/types/convenience.ss
@@ -14,6 +14,7 @@
          make-Name make-ValuesDots make-Function
          (rep-out filter-rep object-rep))
 
+
 (define (one-of/c . args)
   (apply Un (map -val args)))
 
@@ -53,7 +54,6 @@
                  (*Un (-val '())
                       (-pair (-Syntax e)
                              (*Un (-Syntax e) list)))))))
-
 (define Any-Syntax (-Syntax In-Syntax))
 
 (define (-Sexpof t)
diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss
index 936646a4b5..bf018ad186 100644
--- a/collects/typed-scheme/types/subtype.ss
+++ b/collects/typed-scheme/types/subtype.ss
@@ -200,7 +200,7 @@
 ;; potentially raises exn:subtype, when the algorithm fails
 ;; is s a subtype of t, taking into account constraints A
 (define (subtype* A s t)
-  (parameterize ([match-equality-test type-equal?]
+  (parameterize ([match-equality-test (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))]
                  [current-seen A])
     (let ([ks (Type-key s)] [kt (Type-key t)])
       (cond 
diff --git a/collects/typed-scheme/types/union.ss b/collects/typed-scheme/types/union.ss
index 5019cada22..488d715ffb 100644
--- a/collects/typed-scheme/types/union.ss
+++ b/collects/typed-scheme/types/union.ss
@@ -19,7 +19,9 @@
 (define (flat t)
   (match t
     [(Union: es) es]
-    [_ (list t)]))    
+    [(Values: (list (Result: (Union: es) _ _))) es]
+    [(Values: (list (Result: t _ _))) (list t)]
+    [_ (list t)]))
 
 (define (remove-subtypes ts)
   (let loop ([ts* ts] [result '()])
@@ -44,7 +46,7 @@
        (cond
          [(null? types) (make-union* null)]
          [(null? (cdr types)) (car types)]           
-         [else (make-union* (foldr union2 '() (remove-subtypes types)))]))]))
+         [else (make-union* (sort (foldr union2 '() (remove-subtypes types)) type<?))]))]))
 
 (define (u-maker args) (apply Un args))
 
diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss
index 8e3d6f7362..7706c32709 100644
--- a/collects/typed-scheme/utils/utils.ss
+++ b/collects/typed-scheme/utils/utils.ss
@@ -150,17 +150,18 @@ at least theoretically.
 (define custom-printer (make-parameter #t))
   
 (define-syntax (define-struct/printer stx)
-  (syntax-case stx ()
-    [(form name (flds ...) printer)
-     #`(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]))
-         #f)]))
+  (syntax-parse stx
+    [(form name (flds ...) printer:expr)
+     #`(define-struct name (flds ...) 
+         #:property prop:custom-write 
+         #,(if printing? 
+               #'(lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))
+               #'pseudo-printer)
+         #:inspector #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?'