diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 64655ac1b9..a210f85d50 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -366,7 +366,7 @@
      [current-error-port (-Param -Output-Port -Output-Port)]
      [current-input-port (-Param -Input-Port -Input-Port)]
      [round (N . -> . N)]
-     [seconds->date (N . -> . (make-Struct 'date #f (list N N N N N N N N B N) #f))]
+     [seconds->date (N . -> . (make-Struct 'date #f (list N N N N N N N N B N) #f #f #'date?))]
      [current-seconds (-> N)]
      [sqrt (-> N N)]
      [path->string (-> -Path -String)]       
diff --git a/collects/typed-scheme/private/infer-ops.ss b/collects/typed-scheme/private/infer-ops.ss
index 8b1ebd19ef..97f42cc91c 100644
--- a/collects/typed-scheme/private/infer-ops.ss
+++ b/collects/typed-scheme/private/infer-ops.ss
@@ -188,7 +188,7 @@
                               (cgen V X 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/infer.ss b/collects/typed-scheme/private/infer.ss
index 3d4c1465ad..a7733ce2f8 100644
--- a/collects/typed-scheme/private/infer.ss
+++ b/collects/typed-scheme/private/infer.ss
@@ -287,7 +287,7 @@
         [(list (Syntax: s1) (Syntax: s2))
          (infer/int s1 s2 mapping flag)]
         ;; structs just recur
-        [(list (Struct: nm p flds proc) (Struct: nm p flds* proc*))
+        [(list (Struct: nm p flds proc _ _) (Struct: nm p flds* proc* _ _))
          (cond [(and proc proc*)
                 (infer/int/list (cons proc flds) (cons proc* flds*) mapping flag)]
                [(or proc proc*)
diff --git a/collects/typed-scheme/private/init-envs.ss b/collects/typed-scheme/private/init-envs.ss
index 6d46966dbc..f1821d2bd2 100644
--- a/collects/typed-scheme/private/init-envs.ss
+++ b/collects/typed-scheme/private/init-envs.ss
@@ -19,6 +19,8 @@
   (match v
     [(Union: elems) `(make-Union (list ,@(map sub elems)))]
     [(Name: stx) `(make-Name (quote-syntax ,stx))]
+    [(Struct: name parent flds proc poly? pred-id)
+     `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-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))]
     [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
diff --git a/collects/typed-scheme/private/rep-utils.ss b/collects/typed-scheme/private/rep-utils.ss
index a23d36b79d..23227f283d 100644
--- a/collects/typed-scheme/private/rep-utils.ss
+++ b/collects/typed-scheme/private/rep-utils.ss
@@ -150,7 +150,7 @@
                      (lambda (s)
                        (... 
                         (syntax-case s ()
-                          [(__ fs ...) (syntax/loc s (struct nm (_ fs ...)))]))))
+                          [(__ . fs) (quasisyntax/loc s (struct nm #, (syntax/loc #'fs (_ . fs))))]))))
                    (begin-for-syntax
                      (hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs)))
                    intern
diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss
index e2e5962397..655c9a9d80 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -214,12 +214,12 @@
               [(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
               [(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
               ;; subtyping on immutable structs is covariant
-              [(list (Struct: nm _ flds #f) (Struct: nm _ flds* #f))
+              [(list (Struct: nm _ flds #f _ _) (Struct: nm _ flds* #f _ _))
                (subtypes* A0 flds flds*)]
-              [(list (Struct: nm _ flds proc) (Struct: nm _ flds* proc*))
+              [(list (Struct: nm _ flds proc _ _) (Struct: nm _ flds* proc* _ _))
                (subtypes* A0 (cons proc flds) (cons proc* flds*))]
               ;; subtyping on structs follows the declared hierarchy
-              [(list (Struct: nm (? Type? parent) flds proc) other) 
+              [(list (Struct: nm (? Type? parent) flds proc _ _) other) 
                ;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
                (subtype* A0 parent other)]
               ;; applications and names are structs too
@@ -261,7 +261,7 @@
                      (subtype* A0 t other)
                      (fail! s t)))]
               ;; Promises are covariant
-              [(list (Struct: 'Promise _ (list t) _) (Struct: 'Promise _ (list t*) _)) (subtype* A0 t t*)]
+              [(list (Struct: 'Promise _ (list t) _ _ _) (Struct: 'Promise _ (list t*) _ _ _)) (subtype* A0 t t*)]
               ;; subtyping on values is pointwise
               [(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
               ;; single values shouldn't actually happen, but they're just like the type
diff --git a/collects/typed-scheme/private/syntax-traversal.ss b/collects/typed-scheme/private/syntax-traversal.ss
index 9bc373a904..247e91f258 100644
--- a/collects/typed-scheme/private/syntax-traversal.ss
+++ b/collects/typed-scheme/private/syntax-traversal.ss
@@ -40,6 +40,10 @@
 ;; given in `expanded'.
 (define (look-for-in-orig orig expanded lookfor)
   (define src (syntax-source orig))
+  ;(printf "orig : ~a~n" orig)
+  ;(printf "expanded : ~a~n" expanded)
+  ;(printf "lookfor : ~a~n" lookfor)
+  ;(printf "src : ~a~n" src)
   ;; we just might get a lookfor that is already in the original
    (let ([enclosing (enclosing-syntaxes-with-source expanded lookfor src)]
          [syntax-locs (make-hash)])
@@ -51,12 +55,15 @@
      (or
       ;; we just might get a lookfor that is already in the original
       (and (eq? src (syntax-source lookfor))
-           (hash-ref syntax-locs (syntax-loc lookfor) #f))
+           (hash-ref syntax-locs (syntax-loc lookfor) #f)
+           #;(printf "chose branch one: ~a~n" (hash-ref syntax-locs (syntax-loc lookfor) #f)))
            
       ;; look for some enclosing expression
       (and enclosing
-           (ormap (lambda (enc) (hash-ref syntax-locs (syntax-loc enc) #f))
-                  enclosing)))))
+           (begin0
+             (ormap (lambda (enc) (hash-ref syntax-locs (syntax-loc enc) #f))
+                    enclosing)
+             #;(printf "chose branch two ~a~n" enclosing))))))
 
 ;(trace look-for-in-orig)
 
diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss
index 4c033d949f..9fa1dadea9 100644
--- a/collects/typed-scheme/private/tc-app-unit.ss
+++ b/collects/typed-scheme/private/tc-app-unit.ss
@@ -204,7 +204,7 @@
                      [arg-els-effs arg-els-effs]
                      [args args-stx])
       (match ftype
-        [(tc-result: (and sty (Struct: _ _ _ (? Type? proc-ty))) thn-eff els-eff)
+        [(tc-result: (and sty (Struct: _ _ _ (? Type? proc-ty) _ _)) thn-eff els-eff)
          (outer-loop (ret proc-ty thn-eff els-eff)
                      (cons (tc-result-t ftype0) argtypes)
                      (cons (list) arg-thn-effs)
diff --git a/collects/typed-scheme/private/tc-structs.ss b/collects/typed-scheme/private/tc-structs.ss
index a79b73683c..a3ebef229e 100644
--- a/collects/typed-scheme/private/tc-structs.ss
+++ b/collects/typed-scheme/private/tc-structs.ss
@@ -1,8 +1,6 @@
 #lang scheme/base
 
-(require (lib "struct.ss" "syntax")
-         (lib "etc.ss")
-         "type-rep.ss" ;; doesn't need tests
+(require "type-rep.ss" ;; doesn't need tests
          "type-effect-convenience.ss" ;; maybe needs tests
          "type-env.ss" ;; maybe needs tests
          "type-utils.ss"
@@ -12,10 +10,12 @@
          "union.ss"
          "tc-utils.ss"
          "resolve-type.ss"
-         (lib "kerncase.ss" "syntax")
-         (lib "trace.ss")
-         (lib "kw.ss")
-         (lib "plt-match.ss"))
+         "def-binding.ss"
+         syntax/kerncase
+         syntax/struct
+         mzlib/trace         
+         scheme/match
+         (for-syntax scheme/base))
 
 
 (require (for-template scheme/base
@@ -80,7 +80,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]))
 
@@ -93,10 +93,13 @@
                          #:mutable [setters? #f]
                          #:proc-ty [proc-ty #f]
                          #:maker [maker #f]
-                         #:constructor-return [cret #f])
+                         #:constructor-return [cret #f]
+                         #:poly? [poly? #f])
+  ;; create the approriate names that define-struct will bind
+  (define-values (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)]
+         [sty (make-Struct name parent fld-types proc-ty poly? pred)]
          [external-fld-types/no-parent types]
          [external-fld-types fld-types])
     (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters? 
@@ -117,17 +120,23 @@
   (define-values (maker pred getters setters) (struct-names nm flds setters?))
   ;; the type name that is used in all the types
   (define name (type-wrapper (make-Name nm)))
-  ;; register the type name
+  ;; the list of names w/ types
+  (define bindings
+    (append 
+     (list (cons (or maker* maker) 
+                 (wrapper (->* external-fld-types (if cret cret name))))
+           (cons pred
+                 (make-pred-ty (wrapper name))))
+     (map (lambda (g t) (cons g (wrapper (->* (list name) t)))) getters external-fld-types/no-parent)
+     (if setters?
+         (map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) getters external-fld-types/no-parent)
+         null)))
   (register-type-name nm (wrapper sty))
-  ;; register the various function types
-  (register-type (or maker* maker) (wrapper (->* external-fld-types (if cret cret name))))
-  (register-types getters
-                  (map (lambda (t) (wrapper (->* (list name) t))) external-fld-types/no-parent))
-  (when setters?    
-    #;(printf "setters: ~a~n" (syntax-object->datum setters))
-    (register-types setters
-                    (map (lambda (t) (wrapper (->* (list name t) -Void))) external-fld-types/no-parent)))
-  (register-type pred (make-pred-ty (wrapper name))))
+  (for/list ([e bindings])
+    (let ([nm (car e)]
+          [t (cdr e)])
+      (register-type nm t)
+      (make-def-binding nm t))))
 
 ;; check and register types for a polymorphic define struct
 ;; tc/poly-struct : Listof[identifier] (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void
@@ -156,7 +165,8 @@
   (mk/register-sty nm flds parent-name parent-field-types types
                    ;; wrap everything in the approriate forall
                    #:wrapper (lambda (t) (make-Poly tvars t))
-                   #:type-wrapper (lambda (t) (make-App t new-tvars #f))))
+                   #:type-wrapper (lambda (t) (make-App t new-tvars #f))
+                   #:poly? #t))
 
 
 ;; typecheck a non-polymophic struct and register the approriate types
@@ -183,74 +193,20 @@
 ;; tc/builtin-struct : identifier identifier Listof[identifier] Listof[Type] Listof[Type] -> void
 (define (tc/builtin-struct nm parent flds tys parent-tys)
   (let ([parent* (if parent (make-Name parent) #f)])
-    (mk/register-sty nm flds parent* parent-tys tys #:mutable #t)))
+    (mk/register-sty nm flds parent* parent-tys tys
+                     #:mutable #t)))
 
 ;; syntax for tc/builtin-struct
-(define-syntax d-s 
-  (syntax-rules (:) 
+(define-syntax (d-s stx) 
+  (syntax-case stx (:) 
     [(_ (nm par) ([fld : ty] ...) (par-ty ...))
-     (tc/builtin-struct #'nm #'par
-                        (list #'fld ...)
-                        (list ty ...)
-                        (list par-ty ...))]
+     #'(tc/builtin-struct #'nm #'par
+                          (list #'fld ...)
+                          (list ty ...)
+                          (list par-ty ...))]
     [(_ nm ([fld : ty] ...) (par-ty ...))
-     (tc/builtin-struct #'nm #f
-                        (list #'fld ...)
-                        (list ty ...)
-                        (list par-ty ...))]))
+     #'(tc/builtin-struct #'nm #f
+                          (list #'fld ...)
+                          (list ty ...)
+                          (list par-ty ...))]))
 
-;; This is going away!
-#|
-
-;; parent-nm is an identifier with the name of the defined type
-;; variants is (list id id (list (cons id unparsed-type))) - first id is name of variant, second is name of maker, 
-;;     list is name of field w/ type
-;; top-pred is an identifier
-;; produces void
-(define (tc/define-type parent-nm top-pred variants)
-  ;; the symbol and type variable used for parsing
-  (define parent-sym (syntax-e parent-nm))
-  (define parent-tvar (make-F parent-sym))
-  
-  ;; create the initial struct type, which contains type variables
-  (define (mk-initial-variant nm fld-tys-stx)
-    ;; parse the types (recursiveness doesn't matter)
-    (define-values (fld-tys _) (FIXME parent-sym parent-tvar fld-tys-stx))     
-    (make-Struct (syntax-e nm) #f fld-tys #f))
-  
-  ;; create the union type that is the total type
-  (define (mk-un-ty parent-sym variant-struct-tys)
-    (make-Mu parent-sym (apply Un variant-struct-tys)))     
-  
-  ;; generate the names and call mk-variant
-  (define (mk-variant nm maker-name fld-names un-ty variant-struct-ty parent-nm)
-    ;; construct the actual type of this variant
-    (define variant-ty (subst parent-nm un-ty variant-struct-ty))
-    ;; the fields of this variant
-    (match-define (Struct: _ _ fld-types _) variant-ty)
-    ;; register all the types (with custon maker name)
-    (register-struct-types nm variant-ty fld-names fld-types fld-types #f #:maker maker-name))
-  
-  ;; all the names
-  (define variant-names (map car variants))
-  (define variant-makers (map cadr variants))
-  (define variant-flds (map caddr variants))    
-  ;; create the initial variants, which don't have the parent substituted in
-  (define variant-struct-tys (map (lambda (n flds) (mk-initial-variant n (map car flds))) variant-names variant-flds))
-  ;; just the names of each variant's fields
-  (define variant-fld-names (map (lambda (x) (map cdr x)) variant-flds))
-  
-  ;; the type of the parent
-  (define un-ty (mk-un-ty parent-sym variant-struct-tys))
-  
-  ;; register the types for the parent
-  (register-type top-pred (make-pred-ty un-ty))
-  (register-type-name parent-nm un-ty)
-  
-  ;; construct all the variants, and register the appropriate names
-  (for-each (lambda (nm mk fld-names sty) (mk-variant nm mk fld-names un-ty sty parent-sym))
-            variant-names variant-makers variant-fld-names variant-struct-tys))
-
-
-
-|#
diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss
index 8bc3de2ead..3e9f4a7968 100644
--- a/collects/typed-scheme/private/type-contract.ss
+++ b/collects/typed-scheme/private/type-contract.ss
@@ -18,7 +18,7 @@
  syntax/struct
  syntax/stx
  mzlib/trace
- (only-in scheme/contract -> ->* case-> cons/c flat-rec-contract)
+ (only-in scheme/contract -> ->* case-> cons/c flat-rec-contract provide/contract any/c)
  (for-template scheme/base scheme/contract (only-in scheme/class object% is-a?/c subclass?/c)))
 
 (define (define/fixup-contract? stx)
@@ -117,10 +117,12 @@
         [(Instance: _) #'(is-a?/c object%)]
         [(Class: _ _ _) #'(subclass?/c object%)]
         [(Value: '()) #'null?]
+        [(Struct: _ _ _ _ #f pred?) pred?]
         [(Syntax: (Base: 'Symbol)) #'identifier?]
         [(Syntax: t)
          (if (equal? ty Any-Syntax)
              #`syntax?
              #`(syntax/c #,(t->c t)))]
         [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x #,v)))]
-        [else (exit (fail))]))))
+        [else          
+         (exit (fail))]))))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index 9b7e4b97ff..000c832533 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -72,7 +72,7 @@
                [(dom rng rest eff1 eff2) (make-arr dom rng rest eff1 eff2)]))
 
 (define (make-promise-ty t)
-  (make-Struct (string->uninterned-symbol "Promise") #f (list t) #f))
+  (make-Struct (string->uninterned-symbol "Promise") #f (list t) #f #f #'promise?))
 
 (define N (make-Base 'Number))
 (define -Integer (make-Base 'Integer))
diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss
index 516819196d..cf5314c50d 100644
--- a/collects/typed-scheme/private/type-effect-printer.ss
+++ b/collects/typed-scheme/private/type-effect-printer.ss
@@ -84,8 +84,8 @@
      (fp "~a" (cons 'List (tuple-elems t)))]
     [(Base: n) (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/private/type-rep.ss b/collects/typed-scheme/private/type-rep.ss
index 9a2b968ff2..a09b1a669a 100644
--- a/collects/typed-scheme/private/type-rep.ss
+++ b/collects/typed-scheme/private/type-rep.ss
@@ -66,13 +66,16 @@
   ;; parent : Struct
   ;; flds : Listof[Type]
   ;; proc : Function Type
-  (dt Struct (name parent flds proc) 
+  (dt Struct (name parent flds proc poly? pred-id)
+      [#: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)))]
       [#:fold-rhs (*Struct name 
                            (and parent (type-rec-id parent))
                            (map type-rec-id flds)
-                           (and proc (type-rec-id proc)))])
+                           (and proc (type-rec-id proc))
+                           poly?
+                           pred-id)])
   
   ;; dom : Listof[Type]
   ;; rng : Type
diff --git a/collects/typed-scheme/private/unify.ss b/collects/typed-scheme/private/unify.ss
index 71eeb582f0..afbc39504e 100644
--- a/collects/typed-scheme/private/unify.ss
+++ b/collects/typed-scheme/private/unify.ss
@@ -72,7 +72,7 @@
       [(list (list (Param: t1 t2) (Param: s1 s2)) rest ...) 
        (unify/acc (list* (list t1 s1) (list t2 s2) rest) acc)]
       ;; structs
-      [(list (list (Struct: nm p elems proc) (Struct: nm p elems* proc*)) rest ...)
+      [(list (list (Struct: nm p elems proc _ _) (Struct: nm p elems* proc* _ _)) rest ...)
        (cond [(and proc proc*)
               (unify/acc (append rest (map list elems elems*) (list (list proc proc*))) acc)]
              [(or proc proc*) #f]