diff --git a/collects/tests/typed-scheme/fail/with-type-bug.ss b/collects/tests/typed-scheme/fail/with-type-bug.ss
new file mode 100644
index 00000000..0fcb77db
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/with-type-bug.ss
@@ -0,0 +1,5 @@
+#;
+(exn-pred exn:fail:contract?)
+#lang scheme
+(require (prefix-in T: typed/scheme))
+((T:with-type #:result (T:Integer T:-> T:Integer) add1) 1/2)
diff --git a/collects/tests/typed-scheme/succeed/provide-poly-struct.ss b/collects/tests/typed-scheme/succeed/provide-poly-struct.ss
new file mode 100644
index 00000000..3fc0efad
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/provide-poly-struct.ss
@@ -0,0 +1,12 @@
+#lang scheme/load
+
+(module m typed-scheme
+  (define-struct: (A) x ([v : A]))
+  (provide make-x x-v))
+
+(module n scheme
+  (require 'm)
+  (x-v (make-x 1)))
+
+(require 'm)
+(require 'n)
diff --git a/collects/tests/typed-scheme/succeed/sequences.ss b/collects/tests/typed-scheme/succeed/sequences.ss
index c584ad85..00a162ef 100644
--- a/collects/tests/typed-scheme/succeed/sequences.ss
+++ b/collects/tests/typed-scheme/succeed/sequences.ss
@@ -7,3 +7,4 @@
 (ann (for ([z (open-input-string "foobar")]) (add1 z)) Void)
 
 (ann (for ([z (in-list (list 1 2 3))]) (add1 z)) Void)
+(ann (for ([z (in-vector (vector 1 2 3))]) (add1 z)) Void)
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
index f8962ec0..c6f68f75 100644
--- a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
@@ -112,10 +112,11 @@
    
    [(-values (list -Number)) (-values (list Univ))]
    
-   [(-poly (a) ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number a) null)) . -> . (-lst a)))
-    ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number (-pair -Number (-v a))) null)) . -> . (-lst (-pair -Number (-v a))))]
-   [(-poly (a) ((-struct 'bar #f (list -Number a) null) . -> . (-lst a)))
-    ((-struct 'bar #f (list -Number (-pair -Number (-v a))) null) . -> . (-lst (-pair -Number (-v a))))]
+   [(-poly (a) ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number a) null #'values)) . -> . (-lst a)))
+    ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number (-pair -Number (-v a))) null #'values)) 
+     . -> . (-lst (-pair -Number (-v a))))]
+   [(-poly (a) ((-struct 'bar #f (list -Number a) null #'values) . -> . (-lst a)))
+    ((-struct 'bar #f (list -Number (-pair -Number (-v a))) null #'values) . -> . (-lst (-pair -Number (-v a))))]
    
    [(-poly (a) (a . -> . (make-Listof a))) ((-v b) . -> . (make-Listof (-v b)))]
    [(-poly (a) (a . -> . (make-Listof a))) ((-pair -Number (-v b)) . -> . (make-Listof (-pair -Number (-v b))))]
diff --git a/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss
index e49e57cf..43022800 100644
--- a/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss
@@ -37,10 +37,14 @@
    [(-mu x (Un -Number -Symbol x)) (-mu y (Un -Number -Symbol y))]     
    ;; found bug
    [FAIL (Un (-mu heap-node 
-                  (-struct 'heap-node #f (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty))) null)) 
+                  (-struct 'heap-node #f
+                           (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty)))
+                           null #'values)) 
              (-base 'heap-empty))
          (Un (-mu heap-node 
-                  (-struct 'heap-node #f (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty))) null)) 
+                  (-struct 'heap-node #f
+                           (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty)))
+                           null #'values)) 
              (-base 'heap-empty))]))
 
 (define-go
diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index 64da1f72..14a0bd85 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -11,6 +11,8 @@
 	 (rep type-rep filter-rep object-rep)
          (rename-in (types utils union convenience abbrev)
                     [Un t:Un]
+                    [true-lfilter -true-lfilter]
+pecheck-tests.ss
                     [true-filter -true-filter]
                     [-> t:->])
          (utils tc-utils utils)
@@ -138,10 +140,10 @@
         (tc-e/t 3 -Pos)
         (tc-e/t "foo" -String)
         (tc-e (+ 3 4) -Pos)
-        [tc-e/t (lambda: () 3) (t:-> -Pos : -true-filter)]
-        [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : -true-filter)]
-        [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : -true-filter)]
-        [tc-e/t (lambda () 3) (t:-> -Pos : -true-filter)]
+        [tc-e/t (lambda: () 3) (t:-> -Pos : -true-lfilter)]
+        [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : -true-lfilter)]
+        [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : -true-lfilter)]
+        [tc-e/t (lambda () 3) (t:-> -Pos : -true-lfilter)]
         [tc-e (values 3 4) #:ret (ret (list -Pos -Pos) (list -true-filter -true-filter))]
         [tc-e (cons 3 4) (-pair -Pos -Pos)]
         [tc-e (cons 3 (ann '() : (Listof Integer))) (make-Listof -Integer)]
@@ -479,11 +481,12 @@
         [tc-e/t (let* ([z 1]
                        [p? (lambda: ([x : Any]) (number? z))])
                   (lambda: ([x : Any]) (if (p? x) 11 12)))
-                (t:-> Univ -Pos : -true-filter)]
+                (t:-> Univ -Pos : -true-lfilter)]
         [tc-e/t (let* ([z 1]
                        [p? (lambda: ([x : Any]) (number? z))])
                   (lambda: ([x : Any]) (if (p? x) x 12)))
-                (make-pred-ty Univ Univ (-val #f) 0 null)]
+                (t:-> Univ Univ : (-LFS (list (-not-filter (-val #f))) (list (-filter (-val #f)))) : (make-LPath null 0))]
+;                (make-pred-ty Univ Univ (-val #f) 0 null)]
         [tc-e/t (let* ([z (ann 1 : Any)]
                        [p? (lambda: ([x : Any]) (not (number? z)))])
                   (lambda: ([x : Any]) (if (p? x) x 12)))
@@ -491,7 +494,7 @@
         [tc-e/t (let* ([z 1]
                        [p? (lambda: ([x : Any]) (not (number? z)))])
                   (lambda: ([x : Any]) (if (p? x) x 12)))
-                (t:-> Univ -Pos : -true-filter)]
+                (t:-> Univ -Pos : -true-lfilter)]
         [tc-e/t (let* ([z 1]
                        [p? (lambda: ([x : Any]) z)])
                   (lambda: ([x : Any]) (if (p? x) x 12)))
@@ -660,7 +663,7 @@
         
         ;; instantiating dotted terms
         [tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer)
-                (-Integer B -Integer . t:-> . -Pos : -true-filter)]
+                (-Integer B -Integer . t:-> . -Pos : -true-lfilter)]
         [tc-e/t (inst (plambda: (a ...) [xs : (a ... a -> Integer) ... a] 3) Integer Boolean Integer)
                 ((-Integer B -Integer . t:-> . -Integer)
                  (-Integer B -Integer . t:-> . -Integer)
@@ -725,13 +728,13 @@
                    (lambda: ([y : (a ... a -> Number)])
                      (apply y zs))
                    ys)))
-              (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-filter))]
+              (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-lfilter))]
         [tc-e/t (plambda: (a ...) [ys : (a ... a -> Number) *]
                 (lambda: [zs : a ... a]
                   (map (lambda: ([y : (a ... a -> Number)])
                          (apply y zs))
                        ys)))
-              (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-filter))]
+              (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-lfilter))]
         
         [tc-e/t (lambda: ((x : (All (t) t)))
                        ((inst (inst x (All (t) (t -> t))) 
diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss
index 71726887..12753748 100644
--- a/collects/typed-scheme/env/init-envs.ss
+++ b/collects/typed-scheme/env/init-envs.ss
@@ -1,10 +1,10 @@
 #lang scheme/base
 (provide (all-defined-out))
-(require "../utils/utils.ss")
-
-(require "type-env.ss" 
+(require "../utils/utils.ss"
+         "type-env.ss" 
 	 "type-name-env.ss"
 	 "type-alias-env.ss"
+         unstable/struct
          (rep type-rep object-rep filter-rep rep-utils)
 	 (for-template (rep type-rep object-rep filter-rep) 
 		       (types union)
@@ -25,11 +25,12 @@
     [(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))]
-    [(Struct: name parent flds proc poly? pred-id cert acc-ids)
+    [(Struct: name parent flds proc poly? pred-id cert acc-ids maker-id)
      `(make-Struct ,(sub name) ,(sub parent) 
                    ,(sub flds) ,(sub proc) ,(sub poly?)
                    (quote-syntax ,pred-id) (syntax-local-certifier)
-                   (list ,@(for/list ([a acc-ids]) `(quote-syntax ,a))))]
+                   (list ,@(for/list ([a acc-ids]) `(quote-syntax ,a)))
+                   (quote-syntax ,maker-id))]
     [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
     [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
     [(Refinement: parent pred cert) `(make-Refinement ,(sub parent)
diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss
index a70e4378..26ee1ee2 100644
--- a/collects/typed-scheme/infer/infer-unit.ss
+++ b/collects/typed-scheme/infer/infer-unit.ss
@@ -330,7 +330,7 @@
                                (cg S e)))
                             (fail! S T))]
           
-          [((Struct: nm p flds proc _ _ _ _) (Struct: nm p flds* proc* _ _ _ _))
+          [((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*))]
diff --git a/collects/typed-scheme/module-info.ss b/collects/typed-scheme/module-info.ss
new file mode 100644
index 00000000..864540fe
--- /dev/null
+++ b/collects/typed-scheme/module-info.ss
@@ -0,0 +1,18 @@
+#lang scheme/base
+(require typed-scheme/typed-reader)
+(provide module-info configure)
+
+(define ((module-info arg) key default)
+  (case key
+    [(configure-runtime) `(#(typed-scheme/module-info configure ()))]
+    [else default]))
+
+;; options currently always empty
+(define (configure options)
+  (namespace-require 'scheme/base)
+  (eval '(begin 
+           (require (for-syntax typed-scheme/utils/tc-utils scheme/base))
+           (begin-for-syntax (set-box! typed-context? #t)))
+        (current-namespace))
+  (current-readtable readtable))
+
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 8a120f92..278a9558 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -651,7 +651,9 @@
 ;; unsafe
 
 [unsafe-vector-ref (-poly (a) ((-vec a) -Nat . -> . a))]
+[unsafe-vector*-ref (-poly (a) ((-vec a) -Nat . -> . a))]
 [unsafe-vector-length (-poly (a) ((-vec a) . -> . -Nat))]
+[unsafe-vector*-length (-poly (a) ((-vec a) . -> . -Nat))]
 [unsafe-car (-poly (a b) 
               (cl->*
                (->acc (list (-pair a b)) a (list -car))))]
diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss
index d1b0c647..8c568284 100644
--- a/collects/typed-scheme/private/type-contract.ss
+++ b/collects/typed-scheme/private/type-contract.ss
@@ -160,25 +160,33 @@
            #;#'class?           
            #'(class/c (name fcn-cnt) ... (init [by-name-init by-name-cnt] ...)))]
         [(Value: '()) #'null?]
-        [(Struct: nm par flds proc poly? pred? cert acc-ids)
+        [(Struct: nm par flds proc poly? pred? cert acc-ids maker-id)
          (cond 
            [(assf (λ (t) (type-equal? t ty)) structs-seen)
             =>
-            (lambda (pr)
-              (cdr pr))]
+            cdr]
            [proc (exit (fail))]
-               [poly? 
-                (with-syntax* ([(x rec) (generate-temporaries '(x rec))]
-                               [(fld-cnts ...)
-                                (for/list ([fty flds]
-                                           [f-acc acc-ids])
-                                  #`(#,(t->c fty #:seen (cons (cons ty #'rec) structs-seen))
-                                     (#,f-acc x)))])
-                              #`(flat-rec-contract 
-                                 rec
-                                 '#,(syntax-e pred?)
-                                 (lambda (x) (and fld-cnts ...))))]
-               [else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])]
+           [poly? 
+            (with-syntax* ([(rec blame val) (generate-temporaries '(rec blame val))]
+                           [maker maker-id]
+                           [cnt-name nm]
+                           [(fld-cnts ...)
+                            (for/list ([fty flds]
+                                       [f-acc acc-ids])
+                              #`(((contract-projection
+                                   #,(t->c fty #:seen (cons (cons ty #'(recursive-contract rec)) structs-seen)))
+                                  blame)
+                                 (#,f-acc val)))])
+              #`(letrec ([rec 
+                          (make-contract 
+                           #:name 'cnt-name
+                           #:first-order #,pred?
+                           #:projection 
+                           (lambda (blame)
+                             (lambda (val)
+                               (maker fld-cnts ...))))])
+                  rec))]
+           [else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])]
         [(Syntax: (Base: 'Symbol _)) #'identifier?]
         [(Syntax: t) #`(syntax/c #,(t->c t))]
         [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
diff --git a/collects/typed-scheme/rep/filter-rep.ss b/collects/typed-scheme/rep/filter-rep.ss
index 44be1a90..99736e28 100644
--- a/collects/typed-scheme/rep/filter-rep.ss
+++ b/collects/typed-scheme/rep/filter-rep.ss
@@ -14,26 +14,22 @@
    'FilterSet
    (λ (e) (or (FilterSet? e) (NoFilter? e)))))
 
+(provide Filter/c FilterSet/c)
 
-#;(define LatentFilter/c
-  (flat-named-contract
-   'LatentFilter
-   (λ (e)
-     (and (LatentFilter? e) (not (LFilterSet? e))))))
-
-(provide Filter/c FilterSet/c); LatentFilter/c  LatentFilterSet/c index/c)
+(define name-ref/c (or/c identifier? integer?))
+(define (hash-name v) (if (identifier? v) (hash-id v) v))
 
 (df Bot () [#:fold-rhs #:base])
 (df Top () [#:fold-rhs #:base])
 
-(df TypeFilter ([t Type?] [p (listof PathElem?)] [v identifier?])
-  [#:intern (list t p (hash-id v))]
+(df TypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
+  [#:intern (list t p (hash-name v))]
   [#:frees (combine-frees (map free-vars* (cons t p)))
 	   (combine-frees (map free-idxs* (cons t p)))]
   [#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
 
-(df NotTypeFilter ([t Type?] [p (listof PathElem?)] [v identifier?])
-  [#:intern (list t p (hash-id v))]
+(df NotTypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
+  [#:intern (list t p (hash-name v))]
   [#:frees (combine-frees (map free-vars* (cons t p)))
 	   (combine-frees (map free-idxs* (cons t p)))]
   [#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
@@ -69,49 +65,5 @@
 ;; should only be used for parsing type annotations and expected types
 (df NoFilter () [#:fold-rhs #:base])
 
-#|
-(define index/c (or/c natural-number/c keyword?))
-
-(dlf LBot () [#:fold-rhs #:base])
-
-(dlf LTypeFilter ([t Type?] [p (listof PathElem?)] [idx index/c])
-  [#:frees (lambda (frees*) (combine-frees (map (compose make-invariant frees*) (cons t p))))]
-  [#:fold-rhs (*LTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)])
-
-(dlf LNotTypeFilter ([t Type?] [p (listof PathElem?)] [idx index/c])
-  [#:frees (lambda (frees*) (combine-frees (map (compose make-invariant frees*) (cons t p))))]
-  [#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)])
-
-
-
-;; implication
-(dlf LImpFilter ([a (non-empty-listof LatentFilter/c)] [c (non-empty-listof LatentFilter/c)])
-     [#:frees (combine-frees (map free-vars* (append a c)))
-              (combine-frees (map free-idxs* (append a c)))])
-
-
-(dlf LFilterSet (thn els)
-     [#:frees (combine-frees (map free-vars* (append thn els)))
-	      (combine-frees (map free-idxs* (append thn els)))]
-     [#:fold-rhs (*LFilterSet (map latentfilter-rec-id thn) (map latentfilter-rec-id els))]
-     [#:contract (->d ([t (cond [(ormap LBot? t)
-                                 (list/c LBot?)]
-                                [(ormap LBot? e)
-                                 (flat-named-contract "e was LBot" (list/c))]
-                                [else (listof LatentFilter/c)])]
-                       [e (cond [(ormap LBot? e)
-                                 (list/c LBot?)]
-                                [(ormap LBot? t)
-                                 (flat-named-contract "t was LBot" (list/c))]
-                                [else (listof LatentFilter/c)])])
-                      (#:syntax [stx #f])
-                      [result LFilterSet?])])
-
-(define LatentFilterSet/c
-  (flat-named-contract
-   'LatentFilterSet
-   (λ (e) (or (LFilterSet? e)))))
-|#
-
 (define (filter-equal? a b) (= (Rep-seq a) (Rep-seq b)))
 (provide filter-equal?)
\ No newline at end of file
diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss
index da99c9dd..4daacc7d 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -150,11 +150,9 @@
          [rng (or/c Values? ValuesDots?)]
          [rest (or/c #f Type/c)] 
          [drest (or/c #f (cons/c Type/c (or/c natural-number/c symbol?)))]
-         [kws (listof Keyword?)]
-         ;; order is: fixed, rest/drest, keywords
-         [names (listof identifier?)])
+         [kws (listof Keyword?)])
     #:no-provide
-    [#:intern (list dom rng rest drest kws (map hash-id names))]
+    [#:intern (list dom rng rest drest kws)]
     [#:frees (combine-frees 
               (append (map (compose flip-variances free-vars*) 
                            (append (if rest (list rest) null)
@@ -183,8 +181,7 @@
                       (type-rec-id rng)
                       (and rest (type-rec-id rest))
                       (and drest (cons (type-rec-id (car drest)) (cdr drest)))
-                      (map type-rec-id kws)
-                      names)])
+                      (map type-rec-id kws))])
 
 ;; top-arr is the supertype of all function types
 (dt top-arr () [#:fold-rhs #:base])
@@ -201,7 +198,7 @@
 
 ;; name : symbol
 ;; parent : Struct
-;; flds : Listof[Type]
+;; flds : Listof[Cons[Type,Bool]] type and mutability
 ;; proc : Function Type
 ;; poly? : is this a polymorphic type?
 ;; pred-id : identifier for the predicate of the struct
@@ -209,22 +206,34 @@
 (dt Struct ([name symbol?] 
             [parent (or/c #f Struct? Name?)] 
             [flds (listof Type/c)]
+            #;
+            [flds (listof (cons/c Type/c boolean?))]
             [proc (or/c #f Function?)]
             [poly? boolean?] 
             [pred-id identifier?]
             [cert procedure?]
-            [acc-ids (listof identifier?)])
+            [acc-ids (listof identifier?)]
+            [maker-id identifier?])
     [#:intern (list name parent flds proc)]
-    [#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) (if parent (list parent) null) flds)))
-             (combine-frees (map free-idxs* (append (if proc (list proc) null) (if parent (list parent) null) flds)))]
+    [#:frees (combine-frees (map free-vars* (append (if proc (list proc) null)
+                                                    (if parent (list parent) null) 
+                                                    
+                                                    flds #;(map car flds))))
+             (combine-frees (map free-idxs* (append (if proc (list proc) null)
+                                                    (if parent (list parent) null)
+                                                    flds #;(map car flds))))]
     [#:fold-rhs (*Struct name 
                          (and parent (type-rec-id parent))
                          (map type-rec-id flds)
+                         #;
+                         (for/list ([(t m?) (in-pairs (in-list flds))])
+                           (cons (type-rec-id t) m?))
                          (and proc (type-rec-id proc))
                          poly?
                          pred-id
                          cert
-                         acc-ids)]
+                         acc-ids
+                         maker-id)]
     [#:key #f])
 
 ;; A structure type descriptor
@@ -401,7 +410,7 @@
        ;; necessary to avoid infinite loops
        [#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
        ;; functions 
-       [#:arr dom rng rest drest kws names
+       [#:arr dom rng rest drest kws
               (*arr (map sb dom)
                     (sb rng)
                     (if rest (sb rest) #f)
@@ -447,7 +456,7 @@
        ;; necessary to avoid infinite loops
        [#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
        ;; functions
-       [#:arr dom rng rest drest kws names
+       [#:arr dom rng rest drest kws
               (*arr (map sb dom)
                     (sb rng)
                     (if rest (sb rest) #f)
@@ -455,8 +464,7 @@
                         (cons (sb (car drest))
                               (if (eqv? (cdr drest) (+ count outer)) (F-n image) (cdr drest)))
                         #f)
-                    (map sb kws)
-                    names)]
+                    (map sb kws))]
        [#:ValuesDots rs dty dbound
                      (*ValuesDots (map sb rs)
                                   (sb dty)
diff --git a/collects/typed-scheme/scribblings/begin.scrbl b/collects/typed-scheme/scribblings/begin.scrbl
index 61a32344..011f28aa 100644
--- a/collects/typed-scheme/scribblings/begin.scrbl
+++ b/collects/typed-scheme/scribblings/begin.scrbl
@@ -36,22 +36,22 @@ form from @schememodname[scheme]---when porting a program from
 @schememodname[scheme] to @schememodname[typed/scheme], uses of
 @scheme[define-struct] should be changed to @scheme[define-struct:].
 
-@schemeblock[(: mag (pt -> Real))]
+@schemeblock[(: mag (pt -> Number))]
 
-This declares that @scheme[mag] has the type @scheme[(pt -> Real)].
+This declares that @scheme[mag] has the type @scheme[(pt -> Number)].
 @;{@scheme[mag] must be defined at the top-level of the module containing
 the declaration.}
 
-The type @scheme[(pt -> Real)] is a function type, that is, the type
+The type @scheme[(pt -> Number)] is a function type, that is, the type
 of a procedure.  The input type, or domain, is a single argument of
 type @scheme[pt], which refers to an instance of the @scheme[pt]
 structure.  The @scheme[->] both indicates that this is a function
 type and separates the domain from  the range, or output type, in this
-case @scheme[Real].
+case @scheme[Number].
 
 @schemeblock[
 (define (mag p)
-  (sqrt (sqr (pt-x p)) (sqr (pt-y p))))
+  (sqrt (+ (sqr (pt-x p)) (sqr (pt-y p)))))
 ]
 
 This definition is unchanged from the untyped version of the code.
diff --git a/collects/typed-scheme/scribblings/quick.scrbl b/collects/typed-scheme/scribblings/quick.scrbl
index a46bcc31..b0b7c25c 100644
--- a/collects/typed-scheme/scribblings/quick.scrbl
+++ b/collects/typed-scheme/scribblings/quick.scrbl
@@ -28,9 +28,9 @@ language:
 typed/scheme
 (define-struct: pt ([x : Real] [y : Real]))
 
-(: mag (pt -> Real))
+(: mag (pt -> Number))
 (define (mag p)
-  (sqrt (sqr (pt-x p)) (sqr (pt-y p))))
+  (sqrt (+ (sqr (pt-x p)) (sqr (pt-y p)))))
 ]
 )
 
@@ -40,7 +40,7 @@ scheme
 
 (code:contract mag : pt -> number)
 (define (mag p)
-  (sqrt (sqr (pt-x p)) (sqr (pt-y p))))
+  (sqrt (+ (sqr (pt-x p)) (sqr (pt-y p)))))
 ]
 
 Here is the same program, in @schememodname[typed/scheme]:
diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss
index 85d7a0e8..3ca42df5 100644
--- a/collects/typed-scheme/typecheck/tc-app.ss
+++ b/collects/typed-scheme/typecheck/tc-app.ss
@@ -696,7 +696,7 @@
                      (lambda (dom rng rest a) (infer/vararg vars argtys-t dom rest rng (fv rng) (and expected (tc-results->values expected))))
                      t argtys expected)]
     ;; procedural structs
-    [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _))) _)
+    [((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)]
     ;; parameters are functions too
     [((tc-result1: (Param: in out)) (list)) (ret out)]
diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss
index 3efea8a9..bd97da2e 100644
--- a/collects/typed-scheme/typecheck/tc-envops.ss
+++ b/collects/typed-scheme/typecheck/tc-envops.ss
@@ -11,7 +11,7 @@
          (types resolve)
          (only-in (env type-environments lexical-env) env? update-type/lexical env-map env-props replace-props)
          scheme/contract scheme/match
-         mzlib/trace unstable/debug
+         mzlib/trace unstable/debug unstable/struct
          (typecheck tc-metafunctions)
          (for-syntax scheme/base))
 
@@ -42,12 +42,15 @@
      (make-Syntax (update t (make-NotTypeFilter u rst x)))]
     
     ;; struct ops
-    [((Struct: nm par flds proc poly pred cert acc-ids) 
+    [((Struct: nm par flds proc poly pred cert acc-ids maker-id) 
       (TypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))     
-     (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-TypeFilter u rst x)))) proc poly pred cert acc-ids)]
-    [((Struct: nm par flds proc poly pred cert acc-ids) 
+     (make-Struct nm par 
+                  (replace-nth flds idx 
+                               (lambda (e) (update e (make-TypeFilter u rst x))))
+                  proc poly pred cert acc-ids maker-id)]
+    [((Struct: nm par flds proc poly pred cert acc-ids maker-id) 
       (NotTypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))
-     (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))) proc poly pred cert acc-ids)]
+     (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))) proc poly pred cert acc-ids maker-id)]
     
     ;; otherwise
     [(t (TypeFilter: u (list) _))
diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss
index 265ccd41..17713d0e 100644
--- a/collects/typed-scheme/typecheck/tc-structs.ss
+++ b/collects/typed-scheme/typecheck/tc-structs.ss
@@ -76,7 +76,7 @@
 ;; Option[Struct-Ty] -> Listof[Type]
 (define (get-parent-flds p)
   (match p
-    [(Struct: _ _ flds _ _ _ _ _) flds]
+    [(Struct: _ _ flds _ _ _ _ _ _) flds]
     [(Name: n) (get-parent-flds (lookup-type-name n))]
     [#f null]))
 
@@ -99,7 +99,7 @@
   (define-values (struct-type-id maker pred getters setters) (struct-names nm flds setters?))
   (let* ([name (syntax-e nm)]
          [fld-types (append parent-field-types types)]
-         [sty (make-Struct name parent fld-types proc-ty poly? pred (syntax-local-certifier) getters)]
+         [sty (make-Struct name parent fld-types proc-ty poly? pred (syntax-local-certifier) getters (or maker* maker))]
          [external-fld-types/no-parent types]
          [external-fld-types fld-types])
     (if type-only
diff --git a/collects/typed-scheme/typed-reader.ss b/collects/typed-scheme/typed-reader.ss
index ebce7135..3313c542 100644
--- a/collects/typed-scheme/typed-reader.ss
+++ b/collects/typed-scheme/typed-reader.ss
@@ -83,4 +83,4 @@
   (parameterize ([current-readtable readtable])
     (read-syntax src port)))
 
-(provide (rename-out [*read read] [*read-syntax read-syntax]))
+(provide readtable (rename-out [*read read] [*read-syntax read-syntax]))
diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss
index c4c28ab4..14e9afd7 100644
--- a/collects/typed-scheme/types/abbrev.ss
+++ b/collects/typed-scheme/types/abbrev.ss
@@ -76,7 +76,7 @@
 (define make-promise-ty
   (let ([s (string->uninterned-symbol "Promise")])
     (lambda (t)
-      (make-Struct s #f (list t) #f #f #'promise? values (list #'values)))))
+      (make-Struct s #f (list t) #f #f #'promise? values (list #'values) #'values))))
 
 (define -Listof (-poly (list-elem) (make-Listof list-elem)))
 
@@ -271,8 +271,8 @@
 (define (make-arr-dots dom rng dty dbound)
   (make-arr* dom rng #:drest (cons dty dbound)))
 
-(define (-struct name parent flds accs [proc #f] [poly #f] [pred #'dummy] [cert values])
-  (make-Struct name parent flds proc poly pred cert accs))
+(define (-struct name parent flds accs constructor [proc #f] [poly #f] [pred #'dummy] [cert values])
+  (make-Struct name parent flds proc poly pred cert accs constructor))
 
 (d/c (-filter t i [p null])
      (c:->* (Type/c identifier?) ((listof PathElem?)) Filter/c)
@@ -362,6 +362,8 @@
 
 (define true-filter (-FS -top -bot))
 (define false-filter (-FS -bot -top))
+(define true-lfilter (-FS -top -bot))
+(define false-lfilter (-FS -bot -top))
 
 (define (opt-fn args opt-args result)
   (apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])                         
diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss
index 45eb107b..5867999e 100644
--- a/collects/typed-scheme/types/printer.ss
+++ b/collects/typed-scheme/types/printer.ss
@@ -145,8 +145,8 @@
      (fp "~a" (cons 'List (tuple-elems t)))]
     [(Base: n cnt) (fp "~a" n)]      
     [(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))]
-    [(Struct: 'Promise par (list fld) proc _ _ _ _) (fp "(Promise ~a)" fld)]      
-    [(Struct: nm par flds proc _ _ _ _) 
+    [(Struct: 'Promise par (list fld) proc _ _ _ _ _) (fp "(Promise ~a)" fld)]      
+    [(Struct: nm par flds proc _ _ _ _ _) 
      (fp "#(struct:~a ~a" nm flds)
      (when proc
        (fp " ~a" proc))
diff --git a/collects/typed-scheme/types/remove-intersect.ss b/collects/typed-scheme/types/remove-intersect.ss
index dbf1c41b..cbb0e55b 100644
--- a/collects/typed-scheme/types/remove-intersect.ss
+++ b/collects/typed-scheme/types/remove-intersect.ss
@@ -50,18 +50,18 @@
          [(or (list (Pair: _ _) _)
               (list _ (Pair: _ _)))
           #f]
-         [(or (list (Value: '()) (Struct: n _ flds _ _ _ _ _))
-              (list (Struct: n _ flds _ _ _ _ _) (Value: '())))
+         [(or (list (Value: '()) (Struct: n _ flds _ _ _ _ _ _))
+              (list (Struct: n _ flds _ _ _ _ _ _) (Value: '())))
           #f]
-         [(list (Struct: n _ flds _ _ _ _ _)
-                (Struct: n _ flds* _ _ _ _ _))
+         [(list (Struct: n _ flds _ _ _ _ _ _)
+                (Struct: n _ flds* _ _ _ _ _ _))
           (for/and ([f flds] [f* flds*]) (overlap f f*))]
          ;; n and n* must be different, so there's no overlap
-         [(list (Struct: n #f flds _ _ _ _ _)
-                (Struct: n* #f flds* _ _ _ _ _))
+         [(list (Struct: n #f flds _ _ _ _ _ _)
+                (Struct: n* #f flds* _ _ _ _ _ _))
           #f]
-         [(list (Struct: n p flds _ _ _ _ _)
-                (Struct: n* p* flds* _ _ _ _ _))
+         [(list (Struct: n p flds _ _ _ _ _ _)
+                (Struct: n* p* flds* _ _ _ _ _ _))
           (and (= (length flds) (length flds*)) (for/and ([f flds] [f* flds*]) (overlap f f*)))]
          [else #t])])))
 
diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss
index 2916c993..b7663e71 100644
--- a/collects/typed-scheme/types/subtype.ss
+++ b/collects/typed-scheme/types/subtype.ss
@@ -5,7 +5,7 @@
 	 (types utils comparison resolve abbrev)
          (env type-name-env)
          (only-in (infer infer-dummy) unify)
-         scheme/match unstable/match unstable/debug
+         scheme/match unstable/match
          mzlib/trace (rename-in scheme/contract
                                 [-> c->]
                                 [->* c->*])
@@ -186,10 +186,11 @@
   (match arrs
     [(list (and a1 (arr: dom1 rng1 #f #f '() names)) (arr: dom rng #f #f '()) ...)
      (cond
-      [(null? dom) a1]
-      [(not (apply = (length dom1) (map length dom))) #f]
-      [(not (foldl type-equal? rng1 rng)) #f]
-      [else (make-arr (apply map (lambda args (make-Union (sort args type<?))) (cons dom1 dom)) rng1 #f #f '() names)])]
+       [(null? dom) (make-arr dom1 rng1 #f #f '() names)]
+       [(not (apply = (length dom1) (map length dom))) #f]
+       [(not (for/and ([rng2 (in-list rng)]) (type-equal? rng1 rng2)))
+        #f]
+       [else (make-arr (apply map (lambda args (make-Union (sort args type<?))) (cons dom1 dom)) rng1 #f #f '() names)])]
     [_ #f]))
 
 
@@ -198,7 +199,8 @@
 ;; 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 (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))]
+  (define =t (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b))))
+  (parameterize ([match-equality-test =t]
                  [current-seen A])
     (let ([ks (Type-key s)] [kt (Type-key t)])
       (cond 
@@ -223,26 +225,26 @@
 	      [((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
 	      ;; now we encode the numeric hierarchy - bletch	      
 	      [((Base: 'Integer _) (Base: 'Number _)) A0]
-	      [((Base: 'Flonum _)  (== -Real type-equal?)) A0]
-	      [((Base: 'Integer _)  (== -Real type-equal?)) A0]
+	      [((Base: 'Flonum _)  (== -Real =t)) A0]
+	      [((Base: 'Integer _)  (== -Real =t)) A0]
 	      [((Base: 'Flonum _)  (Base: 'Number _)) A0]
 	      [((Base: 'Exact-Rational _) (Base: 'Number _)) A0]
 	      [((Base: 'Integer _) (Base: 'Exact-Rational _)) A0]
 	      [((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Rational _)) A0]
 	      [((Base: 'Exact-Positive-Integer _) (Base: 'Number _)) A0]
-	      [((Base: 'Exact-Positive-Integer _) (== -Nat type-equal?)) A0]
+	      [((Base: 'Exact-Positive-Integer _) (== -Nat =t)) A0]
 	      [((Base: 'Exact-Positive-Integer _) (Base: 'Integer _)) A0]
-	      [((== -Nat type-equal?) (Base: 'Number _)) A0]
-	      [((== -Nat type-equal?) (Base: 'Exact-Rational _)) A0]
-	      [((== -Nat type-equal?) (Base: 'Integer _)) A0]
+	      [((== -Nat =t) (Base: 'Number _)) A0]
+	      [((== -Nat =t) (Base: 'Exact-Rational _)) A0]
+	      [((== -Nat =t) (Base: 'Integer _)) A0]
 
 	      ;; values are subtypes of their "type"
 	      [((Value: (? exact-integer? n)) (Base: 'Integer _)) A0]
 	      [((Value: (and n (? number?) (? exact?) (? rational?))) (Base: 'Exact-Rational _)) A0]
-	      [((Value: (? exact-nonnegative-integer? n)) (== -Nat type-equal?)) A0]
+	      [((Value: (? exact-nonnegative-integer? n)) (== -Nat =t)) A0]
 	      [((Value: (? exact-positive-integer? n)) (Base: 'Exact-Positive-Integer _)) A0]	      
 	      [((Value: (? inexact-real? n)) (Base: 'Flonum _)) A0]
-	      [((Value: (? real? n)) (== -Real type-equal?)) A0]
+	      [((Value: (? real? n)) (== -Real =t)) A0]
 	      [((Value: (? number? n)) (Base: 'Number _)) A0]
 
               [((Value: (? keyword?)) (Base: 'Keyword _)) A0]
@@ -304,22 +306,22 @@
 	      [(s (Union: es)) (or (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)
                                    (fail! s t))]
 	      ;; subtyping on immutable structs is covariant
-	      [((Struct: nm _ flds #f _ _ _ _) (Struct: nm _ flds* #f _ _ _ _))
+	      [((Struct: nm _ flds #f _ _ _ _ _) (Struct: nm _ flds* #f _ _ _ _ _))
 	       (subtypes* A0 flds flds*)]
-	      [((Struct: nm _ flds proc _ _ _ _) (Struct: nm _ flds* proc* _ _ _ _))
+	      [((Struct: nm _ flds proc _ _ _ _ _) (Struct: nm _ flds* proc* _ _ _ _ _))
 	       (subtypes* A0 (cons proc flds) (cons proc* flds*))]
-              [((Struct: _ _ _ _ _ _ _ _) (StructTop: (? (lambda (s2) (type-equal? s2 s)))))
+              [((Struct: _ _ _ _ _ _ _ _ _) (StructTop: (? (lambda (s2) (type-equal? s2 s)))))
                A0]
               [((Box: _) (BoxTop:)) A0]
               [((Vector: _) (VectorTop:)) A0]
               [((MPair: _ _) (MPairTop:)) A0]
               [((Hashtable: _ _) (HashtableTop:)) A0]
 	      ;; subtyping on structs follows the declared hierarchy
-	      [((Struct: nm (? Type? parent) flds proc _ _ _ _) other) 
+	      [((Struct: nm (? Type? parent) flds proc _ _ _ _ _) other) 
                ;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
 	       (subtype* A0 parent other)]
 	      ;; Promises are covariant
-	      [((Struct: 'Promise _ (list t) _ _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _ _)) (subtype* A0 t t*)]
+	      [((Struct: 'Promise _ (list t) _ _ _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _ _ _)) (subtype* A0 t t*)]
 	      ;; subtyping on values is pointwise
 	      [((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
               ;; trivial case for Result
diff --git a/collects/typed/scheme/base/lang/reader.ss b/collects/typed/scheme/base/lang/reader.ss
index f276a7b4..ce8f8d0f 100644
--- a/collects/typed/scheme/base/lang/reader.ss
+++ b/collects/typed/scheme/base/lang/reader.ss
@@ -4,5 +4,15 @@ typed/scheme/base
 
 #:read r:read
 #:read-syntax r:read-syntax
+#:info make-info
+#:module-info make-module-info
+
+(define (make-info key default use-default)
+  (case key
+    [else (use-default key default)]))
+
+(define make-module-info
+  `#(typed-scheme/module-info module-info ()))
+
 
 (require (prefix-in r: typed-scheme/typed-reader))
diff --git a/collects/typed/scheme/lang/reader.ss b/collects/typed/scheme/lang/reader.ss
index e5397c57..3a91f1a7 100644
--- a/collects/typed/scheme/lang/reader.ss
+++ b/collects/typed/scheme/lang/reader.ss
@@ -4,5 +4,15 @@ typed/scheme
 
 #:read r:read
 #:read-syntax r:read-syntax
+#:info make-info
+#:module-info make-module-info
+
+(define (make-info key default use-default)
+  (case key
+    [else (use-default key default)]))
+
+(define make-module-info
+  `#(typed-scheme/module-info module-info ()))
+
 
 (require (prefix-in r: typed-scheme/typed-reader))