diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index c8e9b69a..f845addc 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -57,7 +57,7 @@
 [eqv? (-> Univ Univ B)]
 [equal? (-> Univ Univ B)]
 [even? (-> N B)]
-[assert (-poly (a) (-> (*Un a (-val #f)) a))]
+[assert (-poly (a) (-> (Un a (-val #f)) a))]
 [gensym (cl-> [(Sym) Sym]
               [() Sym])]
 [string-append (->* null -String -String)]
@@ -251,8 +251,8 @@
                               . -> . 
                               (-values (list (-pair b (-val '())) N N N))))]
 
-[call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))]
-[call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))]
+[call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
+[call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
 
 [quotient (-Integer -Integer . -> . -Integer)]
 [remainder (-Integer -Integer . -> . -Integer)]
@@ -276,9 +276,9 @@
  (let ([?outp   (-opt -Output-Port)]
        [?N      (-opt N)]
        [optlist (lambda (t) (-opt (-lst (-opt t))))]
-       [-StrRx  (*Un -String -Regexp -PRegexp)]
-       [-BtsRx  (*Un -Bytes  -Byte-Regexp -Byte-PRegexp)]
-       [-InpBts (*Un -Input-Port -Bytes)])
+       [-StrRx  (Un -String -Regexp -PRegexp)]
+       [-BtsRx  (Un -Bytes  -Byte-Regexp -Byte-PRegexp)]
+       [-InpBts (Un -Input-Port -Bytes)])
    (cl-> [(-StrRx   -String           ) (optlist -String)]
          [(-StrRx   -String N         ) (optlist -String)]
          [(-StrRx   -String N ?N      ) (optlist -String)]
@@ -294,9 +294,9 @@
 
 [regexp-match*
  (let ([?N      (-opt N)]
-       [-StrRx  (*Un -String -Regexp -PRegexp)]
-       [-BtsRx  (*Un -Bytes  -Byte-Regexp -Byte-PRegexp)]
-       [-InpBts (*Un -Input-Port -Bytes)])
+       [-StrRx  (Un -String -Regexp -PRegexp)]
+       [-BtsRx  (Un -Bytes  -Byte-Regexp -Byte-PRegexp)]
+       [-InpBts (Un -Input-Port -Bytes)])
    (cl->*
     (-StrRx   -String [N ?N] . ->opt . (-lst -String))
     (-BtsRx   -String [N ?N] . ->opt . (-lst -Bytes))
@@ -315,17 +315,17 @@
  (let ([?outp   (-opt -Output-Port)]
        [?N      (-opt N)]
        [optlist (lambda (t) (-opt (-lst (-opt t))))]
-       [-StrRx  (*Un -String -Regexp -PRegexp)]
-       [-BtsRx  (*Un -Bytes  -Byte-Regexp -Byte-PRegexp)]
-       [-InpBts (*Un -Input-Port -Bytes)])
+       [-StrRx  (Un -String -Regexp -PRegexp)]
+       [-BtsRx  (Un -Bytes  -Byte-Regexp -Byte-PRegexp)]
+       [-InpBts (Un -Input-Port -Bytes)])
    (->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (optlist (-pair -Nat -Nat))))]
 [regexp-match-positions*
  (let ([?outp   (-opt -Output-Port)]
        [?N      (-opt N)]
        [optlist (lambda (t) (-opt (-lst (-opt t))))]
-       [-StrRx  (*Un -String -Regexp -PRegexp)]
-       [-BtsRx  (*Un -Bytes  -Byte-Regexp -Byte-PRegexp)]
-       [-InpBts (*Un -Input-Port -Bytes)])
+       [-StrRx  (Un -String -Regexp -PRegexp)]
+       [-BtsRx  (Un -Bytes  -Byte-Regexp -Byte-PRegexp)]
+       [-InpBts (Un -Input-Port -Bytes)])
    (->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (-lst (-pair -Nat -Nat))))]
 #;
 [regexp-match-peek-positions*]
@@ -443,8 +443,8 @@
 [hash-map (-poly (a b c) ((-HT a b) (a b . -> . c) . -> . (-lst c)))]
 [hash-ref (-poly (a b c)
                  (cl-> [((-HT a b) a) b]
-                       [((-HT a b) a (-> c)) (*Un b c)]
-                       [((-HT a b) a c) (*Un b c)]))]
+                       [((-HT a b) a (-> c)) (Un b c)]
+                       [((-HT a b) a c) (Un b c)]))]
 #;[hash-table-index (-poly (a b) ((-HT a b) a b . -> . -Void))]
 
 [bytes (->* (list) N -Bytes)]
@@ -464,7 +464,7 @@
 [force (-poly (a) (-> (-Promise a) a))]
 [bytes<? (->* (list -Bytes) -Bytes B)]
 [regexp-replace*
- (cl->* (-Pattern (*Un -Bytes -String) (*Un -Bytes -String) . -> . -Bytes)
+ (cl->* (-Pattern (Un -Bytes -String) (Un -Bytes -String) . -> . -Bytes)
         (-Pattern -String -String . -> . -String))]
 [peek-char
  (cl->* [-> -Char]
@@ -503,7 +503,7 @@
 
 [delete-file (-> -Pathlike -Void)]
 [make-namespace (cl->* (-> -Namespace)
-                       (-> (*Un (-val 'empty) (-val 'initial)) -Namespace))]
+                       (-> (Un (-val 'empty) (-val 'initial)) -Namespace))]
 [make-base-namespace (-> -Namespace)]
 [eval (-> -Sexp Univ)]
 
diff --git a/collects/typed-scheme/private/type-abbrev.ss b/collects/typed-scheme/private/type-abbrev.ss
index 3a33b0f3..6ee393d4 100644
--- a/collects/typed-scheme/private/type-abbrev.ss
+++ b/collects/typed-scheme/private/type-abbrev.ss
@@ -179,8 +179,8 @@
 (define -Listof (-poly (list-elem) (make-Listof list-elem)))
 
 (define -lst make-Listof)
-(define -Sexp (-mu x (*Un Sym N B -String (-val null) (-pair x x))))
-(define -Port (*Un -Input-Port -Output-Port))
+(define -Sexp (-mu x (*Un N B Sym -String (-val null) (-pair x x))))
+(define -Port (*Un -Output-Port -Input-Port))
 
 (define (-lst* #:tail [tail (-val null)] . args)
   (if (null? args)
@@ -199,9 +199,9 @@
      (->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
     [(t) (make-pred-ty (list Univ) B t)]))
 
-(define -Pathlike (*Un -Path -String))
-(define -Pathlike* (*Un (-val 'up) (-val 'same) -Path -String))
-(define -Pattern (*Un -String -Bytes -Regexp -Byte-Regexp -PRegexp -Byte-PRegexp))
+(define -Pathlike (*Un -String -Path))
+(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same)))
+(define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String))
 (define -Byte N)
 
 (define (-Tuple l)
@@ -220,16 +220,13 @@
 (define Any-Syntax ;(-Syntax Univ)
   (-mu x
        (-Syntax (*Un 
-                 (-mu y (*Un (-pair x (*Un x y)) (-val '())))
-                 (make-Vector x)
-                 (make-Box x)
                  N
                  B
-		 -Keyword
+                 Sym
                  -String
-                 Sym))))
+		 -Keyword                 
+                 (-mu y (*Un (-val '()) (-pair x (*Un x y))))
+                 (make-Vector x)
+                 (make-Box x)))))
 
-(define Ident (-Syntax Sym))
-
-;; DO NOT USE if t contains #f
-(define (-opt t) (*Un (-val #f) t))
\ No newline at end of file
+(define Ident (-Syntax Sym))
\ 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 e8a8849f..a3f41d0a 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -78,3 +78,7 @@
 
 (define-syntax-rule (->opt args ... [opt ...] res)
   (opt-fn (list args ...) (list opt ...) res))
+
+
+;; DO NOT USE if t contains #f
+(define (-opt t) (Un (-val #f) t))
\ No newline at end of file
diff --git a/collects/typed-scheme/rep/effect-rep.ss b/collects/typed-scheme/rep/effect-rep.ss
index 96f8768c..dd755d1f 100644
--- a/collects/typed-scheme/rep/effect-rep.ss
+++ b/collects/typed-scheme/rep/effect-rep.ss
@@ -9,29 +9,29 @@
 (de False-Effect () [#:frees #f] [#:fold-rhs #:base])
 
 ;; v is an identifier
-(de Var-True-Effect (v) [#:intern (hash-id v)] [#:frees #f] [#:fold-rhs #:base])
+(de Var-True-Effect ([v identifier?]) [#:intern (hash-id v)] [#:frees #f] [#:fold-rhs #:base])
 
 ;; v is an identifier
-(de Var-False-Effect (v) [#:intern (hash-id v)] [#:frees #f] [#:fold-rhs #:base])
+(de Var-False-Effect ([v identifier?]) [#:intern (hash-id v)] [#:frees #f] [#:fold-rhs #:base])
 
 ;; t is a Type
 ;; v is an identifier
-(de Restrict-Effect (t v) [#:intern (list t (hash-id v))] [#:frees (free-vars* t) (free-idxs* t)]
+(de Restrict-Effect ([t Type?] [v identifier?]) [#:intern (list t (hash-id v))] [#:frees (free-vars* t) (free-idxs* t)]
     [#:fold-rhs (*Restrict-Effect (type-rec-id t) v)])
 
 ;; t is a Type
 ;; v is an identifier
-(de Remove-Effect (t v) 
+(de Remove-Effect ([t Type?] [v identifier?]) 
     [#:intern (list t (hash-id v))]
     [#:frees (free-vars* t) (free-idxs* t)]
     [#:fold-rhs (*Remove-Effect (type-rec-id t) v)])
 
 ;; t is a Type
-(de Latent-Restrict-Effect (t) [#:frees (free-vars* t) (free-idxs* t)]
+(de Latent-Restrict-Effect ([t Type?]) [#:frees (free-vars* t) (free-idxs* t)]
     [#:fold-rhs (*Latent-Restrict-Effect (type-rec-id t))])
 
 ;; t is a Type
-(de Latent-Remove-Effect (t) [#:frees (free-vars* t) (free-idxs* t)]
+(de Latent-Remove-Effect ([t Type?]) [#:frees (free-vars* t) (free-idxs* t)]
     [#:fold-rhs (*Latent-Remove-Effect (type-rec-id t))])
 
 (de Latent-Var-True-Effect () [#:frees #f] [#:fold-rhs #:base])
diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss
index 2d2ecc7d..f0a4b87c 100644
--- a/collects/typed-scheme/rep/rep-utils.ss
+++ b/collects/typed-scheme/rep/rep-utils.ss
@@ -7,6 +7,7 @@
          "free-variance.ss"
          "interning.ss"
          mzlib/etc
+         scheme/contract
          (for-syntax 
           stxclass
           scheme/base
@@ -40,14 +41,25 @@
 (define-for-syntax effect-rec-id #'effect-rec-id)
 (define-for-syntax fold-target #'fold-target)
 
+(define-for-syntax enable-contracts? #t)
+
 (provide (for-syntax type-rec-id effect-rec-id fold-target))
 
 (define-syntaxes (dt de)
   (let ()
+    (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
-      (pattern (i:id ...)))
+      #:attributes ((i 1) (cnt 1) fs)
+      (pattern (oci:opt-cnt-id ...)               
+               #:with (i ...) #'(oci.i ...)
+               #:with (cnt ...) #'(oci.cnt ...)
+               #:with fs #'(i ...)))
     (define (combiner f flds)
       (syntax-parse flds
         [() #'empty-hash-table]
@@ -74,14 +86,18 @@
 				     [[#:intern intern?:expr]] #:opt
 				     [[#:frees . frees:frees-pat]] #:opt
 				     [[#:fold-rhs fold-rhs:fold-pat]] #:opt
+                                     [[#:contract cnt:expr]] #:opt
 				     [no-provide?:no-provide-kw] #:opt) ...*)
 	   (with-syntax* 
 	     ([ex (mk-id #'nm #'nm ":")]
 	      [kw-stx (string->keyword (symbol->string #'nm.datum))]
 	      [parent par]
-	      [(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds) #f #t #'nm)]
+	      [(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds.fs) #f #t #'nm)]
 	      [*maker (mk-id #'nm "*" #'nm)]
 	      [**maker (mk-id #'nm "**" #'nm)]
+              [*maker-cnt (if enable-contracts?
+                              (or #'cnt #'(flds.cnt ... . -> . pred))
+                              #'any/c)]
 	      [ht-stx ht-stx]
 	      [bfs-fold-rhs (cond [#'fold-rhs #`(lambda (tr er) #,#'fold-rhs.e)]
 				  [else #'(lambda (type-rec-id effect-rec-id) 
@@ -90,32 +106,33 @@
 			    #'(begin)                                 
 			    #`(begin 
 				(provide ex pred acc ...)
-				(provide (rename-out [*maker maker]))))]
+				(provide/contract (rename *maker maker *maker-cnt))))]
 	      [intern 
-	       (let ([mk (lambda (int) #`(defintern (**maker . flds) maker #,int #:extra-arg key-expr))])
-		 (syntax-parse #'flds
+	       (let ([mk (lambda (int) #`(defintern (**maker . flds.fs) maker #,int #:extra-arg key-expr))])
+		 (syntax-parse #'flds.fs
 		   [_ #:when #'intern?
 		    (mk #'intern?)]
 		   [() (mk #'#f)]
 		   [(f) (mk #'f)]
-		   [_ (mk #'(list . flds))]))]
-	      [frees 
-	       (with-syntax ([(f1 f2) (if #'frees
-					  #'(frees.f1 frees.f2)
-					  (list (combiner #'free-vars* #'flds)
-						(combiner #'free-idxs* #'flds)))])
-			    (quasisyntax/loc stx
-					     (define (*maker . flds)
-					       (define v (**maker . flds))
-					       (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)))])
+		   [_ (mk #'(list . flds.fs))]))]
+              [frees 
+               (with-syntax ([(f1 f2) (if #'frees
+                                          #'(frees.f1 frees.f2)
+                                          (list (combiner #'free-vars* #'flds.fs)
+                                                (combiner #'free-idxs* #'flds.fs)))])
+                 (quasisyntax/loc stx
+                   (with-contract nm ([*maker *maker-cnt])
+                     (define (*maker . flds.fs)
+                       (define v (**maker . flds.fs))
+                       (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
-		 (define-struct (nm parent) flds #:inspector #f)
+		 (define-struct (nm parent) flds.fs #:inspector #f)
 		 (define-match-expander ex
 		   (lambda (s)
 		     (syntax-parse s 
@@ -123,7 +140,7 @@
 			#:with pat (syntax/loc s (_ _ . fs))
 			(syntax/loc s (struct nm pat))])))
 		 (begin-for-syntax
-		  (hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx)))
+		  (hash-set! ht-stx 'kw-stx (list #'ex #'flds.fs bfs-fold-rhs #'#,stx)))
 		 intern
 		 provides
 		 frees))])))
diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss
index ea2d2017..1bc93fea 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -4,6 +4,7 @@
 (require (utils tc-utils) 
 	 "rep-utils.ss" "effect-rep.ss" "free-variance.ss"
          mzlib/trace scheme/match
+         scheme/contract
          (for-syntax scheme/base))
 
 (define name-table (make-weak-hasheq))
@@ -13,26 +14,36 @@
 ;; Type is defined in rep-utils.ss
 
 ;; t must be a Type
-(dt Scope (t) [#:key (Type-key t)])
+(dt Scope ([t Type?]) [#:key (Type-key t)])
+
+(define (scope-depth k)
+  (flat-named-contract 
+   (format "Scope of depth ~a" k)
+   (lambda (sc)
+     (define (f k sc)
+       (cond [(= 0 k) (not (Scope? sc))]
+             [(not (Scope? sc)) #f]
+             [else (f (sub1 k) (Scope-t sc))]))
+     (f k sc))))
 
 ;; this is ONLY used when a type error ocurrs
 (dt Error () [#:frees #f] [#:fold-rhs #:base])
 
 ;; i is an nat
-(dt B (i)
+(dt B ([i natural-number/c])
     [#:frees empty-hash-table (make-immutable-hasheq (list (cons i Covariant)))]
     [#:fold-rhs #:base])
 
 ;; n is a Name
-(dt F (n) [#:frees (make-immutable-hasheq (list (cons n Covariant))) empty-hash-table] [#:fold-rhs #:base])
+(dt F ([n symbol?]) [#:frees (make-immutable-hasheq (list (cons n Covariant))) empty-hash-table] [#:fold-rhs #:base])
 
 ;; id is an Identifier
-(dt Name (id) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
+(dt Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
 
 ;; rator is a type
 ;; rands is a list of types
 ;; stx is the syntax of the pair of parens
-(dt App (rator rands stx)
+(dt App ([rator Type?] [rands (listof Type?)] [stx syntax?])
     [#:intern (list rator rands)]
     [#:frees (combine-frees (map free-vars* (cons rator rands)))
              (combine-frees (map free-idxs* (cons rator rands)))]
@@ -41,19 +52,19 @@
                       stx)])
 
 ;; left and right are Types
-(dt Pair (left right) [#:key 'pair])
+(dt Pair ([left Type?] [right Type?]) [#:key 'pair])
 
 ;; elem is a Type
-(dt Vector (elem) 
+(dt Vector ([elem Type?]) 
     [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]
     [#:key 'vector])
 
 ;; elem is a Type
-(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]
+(dt Box ([elem Type?]) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]
     [#:key 'box])  
 
 ;; name is a Symbol (not a Name)
-(dt Base (name contract) [#:frees #f] [#:fold-rhs #:base] [#:intern name]
+(dt Base ([name symbol?] [contract syntax?]) [#:frees #f] [#:fold-rhs #:base] [#:intern name]
     [#:key (case name
 	     [(Number Integer) 'number]
 	     [(Boolean) 'boolean]
@@ -63,13 +74,17 @@
 	     [else #f])])
 
 ;; body is a Scope
-(dt Mu (body) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))]
+(dt Mu ([body (scope-depth 1)]) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))]
     [#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))]
     [#:key (Type-key body)])    
 
 ;; n is how many variables are bound here
 ;; body is a Scope
 (dt Poly (n body) #:no-provide 
+    [#:contract (->d ([n natural-number/c]
+                      [body (scope-depth n)])
+                     ()
+                     [result Poly?])]
     [#:frees (free-vars* body) (without-below n (free-idxs* body))]
     [#:fold-rhs (let ([body* (remove-scopes n body)])
                   (*Poly n (add-scopes n (type-rec-id body*))))]
@@ -79,6 +94,10 @@
 ;; there are n-1 'normal' vars and 1 ... var
 ;; body is a Scope
 (dt PolyDots (n body) #:no-provide
+    [#:contract (->d ([n natural-number/c]
+                      [body (scope-depth n)])
+                     ()
+                     [result PolyDots?])]
     [#:key (Type-key body)]
     [#:frees (free-vars* body) (without-below n (free-idxs* body))]
     [#:fold-rhs (let ([body* (remove-scopes n body)])
@@ -86,32 +105,13 @@
 
 ;; pred : identifier
 ;; cert : syntax certifier
-(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred])
-
-;; name : symbol
-;; parent : Struct
-;; flds : Listof[Type]
-;; proc : Function Type
-;; poly? : is this a polymorphic type?
-;; pred-id : identifier for the predicate of the struct
-;; cert : syntax certifier for pred-id
-(dt Struct (name parent flds proc poly? pred-id cert)
-    [#: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))
-                         poly?
-                         pred-id
-                         cert)]
-    [#:key (gensym)])
+(dt Opaque ([pred identifier?] [cert procedure?]) 
+    [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred])
 
 ;; kw : keyword?
 ;; ty : Type
 ;; required? : Boolean
-(dt Keyword (kw ty required?)
+(dt Keyword ([kw keyword?] [ty Type?] [required? boolean?])
     [#:frees (free-vars* ty)
              (free-idxs* ty)]
     [#:fold-rhs (*Keyword kw (type-rec-id ty) required?)]
@@ -126,7 +126,13 @@
 ;; thn-eff : Effect
 ;; els-eff : Effect
 ;; arr is NOT a Type
-(dt arr (dom rng rest drest kws thn-eff els-eff)
+(dt arr ([dom (listof Type?)] 
+         [rng Type?]
+         [rest (or/c #f Type?)] 
+         [drest (or/c #f (cons/c Type? (or/c natural-number/c symbol?)))]
+         [kws (listof Keyword?)]
+         [thn-eff (listof Effect?)]
+         [els-eff (listof Effect?)])
     [#:key 'procedure]
     [#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null)
                                                                                 (map Keyword-ty kws)
@@ -163,11 +169,42 @@
 (dt top-arr ()
     [#:frees #f] [#:fold-rhs #:base])
 
+(define arr/c (or/c top-arr? arr?))
+
 ;; arities : Listof[arr]
-(dt Function (arities) [#:frees (combine-frees (map free-vars* arities))
-                                (combine-frees (map free-idxs* arities))]
+(dt Function ([arities (listof arr/c)])
+    [#:frees (combine-frees (map free-vars* arities))
+             (combine-frees (map free-idxs* arities))]
     [#:fold-rhs (*Function (map type-rec-id arities))])
 
+
+;; name : symbol
+;; parent : Struct
+;; flds : Listof[Type]
+;; proc : Function Type
+;; poly? : is this a polymorphic type?
+;; pred-id : identifier for the predicate of the struct
+;; cert : syntax certifier for pred-id
+(dt Struct ([name symbol?] 
+            [parent (or/c #f Struct? Name?)] 
+            [flds (listof Type?)]
+            [proc (or/c #f Function?)]
+            [poly? boolean?] 
+            [pred-id identifier?]
+            [cert procedure?])
+    [#: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))
+                         poly?
+                         pred-id
+                         cert)]
+    [#:key (gensym)])
+
+
 ;; v : Scheme Value
 (dt Value (v) [#:frees #f] [#:fold-rhs #:base] [#:key (cond [(number? v) 'number]
 							    [(boolean? v) 'boolean]
@@ -175,8 +212,20 @@
 							    [else #f])])
 
 ;; elems : Listof[Type]
-(dt Union (elems) [#:frees (combine-frees (map free-vars* elems))
-                           (combine-frees (map free-idxs* elems))]
+(dt Union ([elems (and/c (listof Type?)
+                         (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?)))]) 
+    [#: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
@@ -188,14 +237,14 @@
 (dt Univ () [#:frees #f] [#:fold-rhs #:base])
 
 ;; types : Listof[Type]
-(dt Values (types) 
+(dt Values ([types (listof Type?)]) 
     #:no-provide
     [#:frees (combine-frees (map free-vars* types))
              (combine-frees (map free-idxs* types))]
     [#:fold-rhs (*Values (map type-rec-id types))]
     [#:key 'values])
 
-(dt ValuesDots (types dty dbound) 
+(dt ValuesDots ([types (listof Type?)] [dty Type?] [dbound (or/c symbol? natural-number/c)]) 
     [#:frees (combine-frees (map free-vars* (cons dty types)))
              (combine-frees (map free-idxs* (cons dty types)))]
     [#:fold-rhs (*ValuesDots (map type-rec-id types) (type-rec-id dty) dbound)]
@@ -203,19 +252,21 @@
 
 ;; in : Type
 ;; out : Type
-(dt Param (in out) [#:key 'parameter])
+(dt Param ([in Type?] [out Type?]) [#:key 'parameter])
 
 ;; key : Type
 ;; value : Type
-(dt Hashtable (key value) [#:key 'hash])
+(dt Hashtable ([key Type?] [value Type?]) [#:key 'hash])
 
 ;; t : Type
-(dt Syntax (t) [#:key 'syntax])
+(dt Syntax ([t Type?]) [#:key 'syntax])
 
 ;; pos-flds  : (Listof Type)
 ;; name-flds : (Listof (Tuple Symbol Type Boolean))
 ;; methods   : (Listof (Tuple Symbol Function))
-(dt Class (pos-flds name-flds methods)
+(dt Class ([pos-flds (listof Type?)] 
+           [name-flds (listof (list/c symbol? Type? boolean?))]
+           [methods (listof (list/c symbol? Function?))])
     [#:frees (combine-frees
               (map free-vars* (append pos-flds 
                                       (map cadr name-flds)
@@ -238,7 +289,7 @@
                     (map list mname (map type-rec-id mty)))])])
 
 ;; cls : Class
-(dt Instance (cls) [#:key 'instance])
+(dt Instance ([cls Class?]) [#:key 'instance])
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss
index 485bc20b..8cb1559c 100644
--- a/collects/typed-scheme/utils/utils.ss
+++ b/collects/typed-scheme/utils/utils.ss
@@ -166,7 +166,7 @@
       [(_ val)
        #'(? (lambda (x) (equal? val x)))])))
 
-(define-for-syntax printing? #t)
+(define-for-syntax printing? #f)
 
 (define print-type* (box (lambda _ (error "print-type* not yet defined"))))
 (define print-effect* (box (lambda _ (error "print-effect* not yet defined"))))