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/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/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss
index 472524a4..c5e10464 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 0980881a..82a8f823 100644
--- a/collects/typed-scheme/infer/infer-unit.ss
+++ b/collects/typed-scheme/infer/infer-unit.ss
@@ -322,7 +322,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/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss
index a1d4ae6e..8bc39839 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/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss
index fe192c15..3372f3fe 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -196,7 +196,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
@@ -204,22 +204,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
diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss
index 9bc405ca..75c04c36 100644
--- a/collects/typed-scheme/typecheck/tc-app.ss
+++ b/collects/typed-scheme/typecheck/tc-app.ss
@@ -708,7 +708,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 c009e869..1be93033 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))
 
@@ -44,12 +44,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 424cb02e..510b3422 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/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss
index 5fb3610b..57688d1c 100644
--- a/collects/typed-scheme/types/abbrev.ss
+++ b/collects/typed-scheme/types/abbrev.ss
@@ -77,7 +77,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)))
 
@@ -256,8 +256,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))
 
 (define (-filter t [p null] [i 0])
   (make-LTypeFilter t p i))
diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss
index 2092712c..c2ab6366 100644
--- a/collects/typed-scheme/types/printer.ss
+++ b/collects/typed-scheme/types/printer.ss
@@ -166,8 +166,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 7b1e5a52..64cbbc2c 100644
--- a/collects/typed-scheme/types/subtype.ss
+++ b/collects/typed-scheme/types/subtype.ss
@@ -306,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