diff --git a/collects/typed-scheme/lang/reader.ss b/collects/typed-scheme/lang/reader.ss
index 6af4b48a..27442278 100644
--- a/collects/typed-scheme/lang/reader.ss
+++ b/collects/typed-scheme/lang/reader.ss
@@ -1,14 +1,14 @@
-(module reader scheme/base
-  (require (prefix-in r: "../typed-reader.ss")
-	   (only-in syntax/module-reader wrap-read-all))
-  
-  (define (*read in)
-    (wrap-read-all 'typed-scheme in r:read))
-  
-  (define (*read-syntax src in)
-    (wrap-read-all 'typed-scheme
-		   in
-		   (lambda (in)
-		     (r:read-syntax src in))))
-  
-  (provide (rename-out [*read read] [*read-syntax read-syntax])))
+#lang scheme/base
+(require (prefix-in r: "../typed-reader.ss")
+         (only-in syntax/module-reader wrap-read-all))
+
+(define (*read in)
+  (wrap-read-all 'typed-scheme in r:read))
+
+(define (*read-syntax src in)
+  (wrap-read-all 'typed-scheme
+                 in
+                 (lambda (in)
+                   (r:read-syntax src in))))
+
+(provide (rename-out [*read read] [*read-syntax read-syntax]))
diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss
index bd7722be..b8b87b6c 100644
--- a/collects/typed-scheme/private/extra-procs.ss
+++ b/collects/typed-scheme/private/extra-procs.ss
@@ -1,9 +1,7 @@
-(module extra-procs mzscheme  
-  (provide assert)    
-  
-  (define (assert v)
-    (unless v
-      (error "Assertion failed - value was #f"))
-    v)
+#lang scheme/base
+(provide assert)    
 
-  )
+(define (assert v)
+  (unless v
+    (error "Assertion failed - value was #f"))
+  v)
diff --git a/collects/typed-scheme/private/mutated-vars.ss b/collects/typed-scheme/private/mutated-vars.ss
index 3b3778f4..da057e5d 100644
--- a/collects/typed-scheme/private/mutated-vars.ss
+++ b/collects/typed-scheme/private/mutated-vars.ss
@@ -1,52 +1,50 @@
-(module mutated-vars mzscheme
-    
-  (require-for-template mzscheme)
-  (require (lib "boundmap.ss" "syntax")
-           (lib "kerncase.ss" "syntax")
-           (lib "trace.ss"))
-  
-  ;; mapping telling whether an identifer is mutated
-  ;; maps id -> boolean
-  (define table (make-module-identifier-mapping))
-  
-  ;; find and add to mapping all the set!'ed variables in form
+#lang scheme/base
+
+(require (for-template scheme/base)
+         syntax/boundmap syntax/kerncase
+         mzlib/trace)
+
+;; mapping telling whether an identifer is mutated
+;; maps id -> boolean
+(define table (make-module-identifier-mapping))
+
+;; find and add to mapping all the set!'ed variables in form
+;; syntax -> void
+(define (find-mutated-vars form)
   ;; syntax -> void
-  (define (find-mutated-vars form)
-    ;; syntax -> void
-    (define (fmv/list lstx)
-      (for-each find-mutated-vars (syntax->list lstx)))
-    ;(printf "called with ~a~n" (syntax-object->datum form))
-    (kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal require/typed-internal #%app lambda)     
-      ;; what we care about: set!
-      [(set! v e)
-       (begin
-         ;(printf "mutated var found: ~a~n" (syntax-e #'v))
-         (module-identifier-mapping-put! table #'v #t))]
-      [(define-values (var ...) expr)
-       (find-mutated-vars #'expr)]
-      [(#%app . rest) (fmv/list #'rest)]
-      [(begin . rest) (fmv/list #'rest)]
-      [(begin0 . rest) (fmv/list #'rest)]
-      [(lambda _ . rest) (fmv/list #'rest)]
-      [(case-lambda (_ . rest) ...) (for-each fmv/list (syntax->list #'(rest ...)))]
-      [(if e1 e2) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e2))]
-      [(if e1 e2 e3) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e1) (find-mutated-vars #'e3))]
-      [(with-continuation-mark e1 e2 e3) (begin (find-mutated-vars #'e1) 
-                                                (find-mutated-vars #'e1)
-                                                (find-mutated-vars #'e3))]
-      [(let-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
-                                           (fmv/list #'b))]
-      [(letrec-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
-                                              (fmv/list #'b))]  
-      ;; all the other forms don't have any expression subforms (like #%top)
-      [_ (void)]))
-  
-  ;(trace find-mutated-vars)
-  
-  ;; checks to see if a particular variable is ever set!'d
-  ;; is-var-mutated? : identifier -> boolean
-  (define (is-var-mutated? id) (module-identifier-mapping-get table id (lambda _ #f)))
-  
-  (provide find-mutated-vars is-var-mutated?)
-  
-  )
+  (define (fmv/list lstx)
+    (for-each find-mutated-vars (syntax->list lstx)))
+  ;(printf "called with ~a~n" (syntax-object->datum form))
+  (kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal require/typed-internal #%app lambda)     
+    ;; what we care about: set!
+    [(set! v e)
+     (begin
+       ;(printf "mutated var found: ~a~n" (syntax-e #'v))
+       (module-identifier-mapping-put! table #'v #t))]
+    [(define-values (var ...) expr)
+     (find-mutated-vars #'expr)]
+    [(#%app . rest) (fmv/list #'rest)]
+    [(begin . rest) (fmv/list #'rest)]
+    [(begin0 . rest) (fmv/list #'rest)]
+    [(lambda _ . rest) (fmv/list #'rest)]
+    [(case-lambda (_ . rest) ...) (for-each fmv/list (syntax->list #'(rest ...)))]
+    [(if e1 e2) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e2))]
+    [(if e1 e2 e3) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e1) (find-mutated-vars #'e3))]
+    [(with-continuation-mark e1 e2 e3) (begin (find-mutated-vars #'e1) 
+                                              (find-mutated-vars #'e1)
+                                              (find-mutated-vars #'e3))]
+    [(let-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
+                                         (fmv/list #'b))]
+    [(letrec-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
+                                            (fmv/list #'b))]  
+    ;; all the other forms don't have any expression subforms (like #%top)
+    [_ (void)]))
+
+;(trace find-mutated-vars)
+
+;; checks to see if a particular variable is ever set!'d
+;; is-var-mutated? : identifier -> boolean
+(define (is-var-mutated? id) (module-identifier-mapping-get table id (lambda _ #f)))
+
+(provide find-mutated-vars is-var-mutated?)
+
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index 8bd050d5..33330dee 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -7,14 +7,12 @@
          (only-in "type-effect-convenience.ss" [make-arr* make-arr])
          "tc-utils.ss"
          "union.ss"
-         (lib "stx.ss" "syntax")
+         syntax/stx
          (except-in "type-environments.ss")
          "type-name-env.ss"
          "type-alias-env.ss"
          "type-utils.ss"
-         (only-in (lib "list.ss") foldl foldr)
-         #;(except-in (lib "list.ss"  "srfi" "1") unfold remove)
-         (lib "plt-match.ss"))
+         scheme/match)
 
 (define enable-mu-parsing (make-parameter #t))
 
diff --git a/collects/typed-scheme/private/require-contract.ss b/collects/typed-scheme/private/require-contract.ss
index c6157919..265b06a2 100644
--- a/collects/typed-scheme/private/require-contract.ss
+++ b/collects/typed-scheme/private/require-contract.ss
@@ -19,22 +19,3 @@
     [(require/contract nm cnt lib)
      #`(begin (require (only-in lib [nm tmp]))     
               (define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen #'#,stx)))]))
-#|
-(module a mzscheme
-  (provide x)
-  (define (x a) 'hi))
-
-(module z mzscheme
-  (require require-contract)
-  
-  (require (lib "contract.ss"))
-  
-  (define-struct b (X Y))
-  
-  (require/contract x (b? . -> . b?) a )
-  
-  (x 'no)
-  )
-
-(require z)
-|#
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index 898768d9..530af57f 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -1,231 +1,227 @@
-(module type-effect-convenience scheme/base
-  
-  (require "type-rep.ss" 
-           "effect-rep.ss"
-           mzlib/plt-match
-           "type-comparison.ss"
-           "type-effect-printer.ss"
-           "union.ss"
-           "subtype.ss"
-           "type-utils.ss"
-           (lib "list.ss")
-           scheme/promise
-           (prefix-in 1: srfi/1)
-           (for-syntax scheme/base))
-  
-  (provide (all-defined-out))
-    
-  
-  (define (-vet id) (make-Var-True-Effect id))
-  (define (-vef id) (make-Var-False-Effect id))
-  
-  (define -rem make-Remove-Effect)
-  (define -rest make-Restrict-Effect)
-  
-  (define (var->type-eff eff)
-    (match eff
-      [(Var-True-Effect: v) (make-Remove-Effect (make-Value #f) v)]
-      [(Var-False-Effect: v) (make-Restrict-Effect (make-Value #f) v)]
-      [_ eff]))
-  
-  (define ((add-var v) eff)
-    (match eff
-      [(Latent-Var-True-Effect:) (-vet v)]
-      [(Latent-Var-False-Effect:) (-vef v)]
-      [(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)]
-      [(Latent-Remove-Effect: t) (make-Remove-Effect t v)]
-      [(True-Effect:) eff]
-      [(False-Effect:) eff]
-      [_ (error 'internal-tc-error "can't add var to effect ~a" eff)]))
-  
-  (define-syntax ->
-    (syntax-rules (:)
-      [(_ dom ... rng)
-       (->* (list dom ...) rng)]
-      [(_ dom ... rng : eff1 eff2)
-       (->* (list dom ...) : eff1 eff2)]))
-  (define-syntax ->*
-    (syntax-rules (:)
-      [(_ dom rng)       
-       (make-Function (list (make-arr* dom rng)))]
-      [(_ dom rst rng)
-       (make-Function (list (make-arr* dom rng rst)))]
-      [(_ dom rng : eff1 eff2)
-       (make-Function (list (make-arr* dom rng #f eff1 eff2)))]
-      [(_ dom rst rng : eff1 eff2)
-       (make-Function (list (make-arr* dom rng rst eff1 eff2)))]))
-  (define-syntax cl->
-    (syntax-rules (:)
-      [(_ [(dom ...) rng] ...)
-       (make-Function (list (make-arr* (list dom ...) rng) ...))]
-      [(_ [(dom ...) rng : eff1 eff2] ...)
-       (make-Function (list (make-arr* (list dom ...) rng #f eff1 eff2) ...))]
-      [(_ [(dom ...) rng rst : eff1 eff2] ...)
-       (make-Function (list (make-arr* (list dom ...) rng rst eff1 eff2) ...))]))
-  (define (cl->* . args)
-    (define (funty-arities f)
-      (match f
-        [(Function: as) as]))
-    (make-Function (map car (map funty-arities args))))
-  
-  (define make-arr*
-    (case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))]
-                 [(dom rng rest) (make-arr dom rng rest (list) (list))]
-                 [(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))
-  
-  (define N (make-Base 'Number))
-  (define -Integer (make-Base 'Integer))
-  (define B (make-Base 'Boolean))
-  (define Sym (make-Base 'Symbol))
-  (define -Void (make-Base 'Void))
-  (define -Bytes (make-Base 'Bytes))
-  (define -Regexp (make-Base 'Regexp))
-  (define -PRegexp (make-Base 'PRegexp))
-  (define -Byte-Regexp (make-Base 'Byte-Regexp))
-  (define -Byte-PRegexp (make-Base 'Byte-PRegexp))
-  (define -String (make-Base 'String))
-  (define -Keyword (make-Base 'Keyword))
-  (define -Char (make-Base 'Char))
-  (define -Syntax make-Syntax)
-  (define -Prompt-Tag (make-Base 'Prompt-Tag))
-  (define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set))
-  (define -Path (make-Base 'Path))
-  (define -Namespace (make-Base 'Namespace))
-  (define -Output-Port (make-Base 'Output-Port))
-  (define -Input-Port (make-Base 'Input-Port))  
-  
-  (define -HT make-Hashtable)
-  (define -Promise make-promise-ty)
+#lang scheme/base  
+(require "type-rep.ss" 
+         "effect-rep.ss"
+         scheme/match
+         "type-comparison.ss"
+         "type-effect-printer.ss"
+         "union.ss"
+         "subtype.ss"
+         "type-utils.ss"         
+         scheme/promise
+         (for-syntax scheme/base))
 
-  (define Univ (make-Univ))
-  
-  (define-syntax -v 
-    (syntax-rules ()
-      [(_ x) (make-F 'x)]))
-  
-  (define-syntax -poly
-    (syntax-rules ()
-      [(_ (vars ...) ty)
-       (let ([vars (-v vars)] ...)
-         (make-Poly (list 'vars ...) ty))]))
-  
-  (define-syntax -mu
-    (syntax-rules ()
-      [(_ var ty)
-       (let ([var (-v var)])
-         (make-Mu 'var ty))]))
-  
-  
-  (define -values make-Values)
-  
-  ;; produce the appropriate type of a list of types
-  ;; that is - if there is exactly one type, just produce it, otherwise produce a values-ty
-  ;; list[type] -> type
-  (define (list->values-ty l)
-    (if (= 1 (length l)) (car l) (-values l)))
-  
-  (define-syntax *Un
-    (syntax-rules ()
-      [(_ . args) (make-Union (list . args))]))
+(provide (all-defined-out))
 
-  
-  (define -pair make-Pair)
-  (define -base make-Base)
-  
-  (define -struct make-Struct)
-  (define -val make-Value)
-      
-  (define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
-  (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 (-lst* . args) (if (null? args)
-                             (-val null)
-                             (-pair (car args) (apply -lst* (cdr args)))))
-  
 
-  #;(define NE (-mu x (Un N (make-Listof x))))
-  (define -NE (-mu x (*Un N (-pair x (-pair Sym (-pair x (-val null)))))))
-  
-  (define (Un/eff . args)
-    (apply Un (map tc-result-t args)))
+(define (-vet id) (make-Var-True-Effect id))
+(define (-vef id) (make-Var-False-Effect id))
 
-  (define -Param make-Param)
-  
-  (define make-pred-ty
-    (case-lambda 
-      [(in out t)
-       (->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
-      [(t) (make-pred-ty (list Univ) B t)]))
+(define -rem make-Remove-Effect)
+(define -rest make-Restrict-Effect)
+
+(define (var->type-eff eff)
+  (match eff
+    [(Var-True-Effect: v) (make-Remove-Effect (make-Value #f) v)]
+    [(Var-False-Effect: v) (make-Restrict-Effect (make-Value #f) v)]
+    [_ eff]))
+
+(define ((add-var v) eff)
+  (match eff
+    [(Latent-Var-True-Effect:) (-vet v)]
+    [(Latent-Var-False-Effect:) (-vef v)]
+    [(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)]
+    [(Latent-Remove-Effect: t) (make-Remove-Effect t v)]
+    [(True-Effect:) eff]
+    [(False-Effect:) eff]
+    [_ (error 'internal-tc-error "can't add var to effect ~a" eff)]))
+
+(define-syntax ->
+  (syntax-rules (:)
+    [(_ dom ... rng)
+     (->* (list dom ...) rng)]
+    [(_ dom ... rng : eff1 eff2)
+     (->* (list dom ...) : eff1 eff2)]))
+(define-syntax ->*
+  (syntax-rules (:)
+    [(_ dom rng)       
+     (make-Function (list (make-arr* dom rng)))]
+    [(_ dom rst rng)
+     (make-Function (list (make-arr* dom rng rst)))]
+    [(_ dom rng : eff1 eff2)
+     (make-Function (list (make-arr* dom rng #f eff1 eff2)))]
+    [(_ dom rst rng : eff1 eff2)
+     (make-Function (list (make-arr* dom rng rst eff1 eff2)))]))
+(define-syntax cl->
+  (syntax-rules (:)
+    [(_ [(dom ...) rng] ...)
+     (make-Function (list (make-arr* (list dom ...) rng) ...))]
+    [(_ [(dom ...) rng : eff1 eff2] ...)
+     (make-Function (list (make-arr* (list dom ...) rng #f eff1 eff2) ...))]
+    [(_ [(dom ...) rng rst : eff1 eff2] ...)
+     (make-Function (list (make-arr* (list dom ...) rng rst eff1 eff2) ...))]))
+(define (cl->* . args)
+  (define (funty-arities f)
+    (match f
+      [(Function: as) as]))
+  (make-Function (map car (map funty-arities args))))
+
+(define make-arr*
+  (case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))]
+               [(dom rng rest) (make-arr dom rng rest (list) (list))]
+               [(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))
+
+(define N (make-Base 'Number))
+(define -Integer (make-Base 'Integer))
+(define B (make-Base 'Boolean))
+(define Sym (make-Base 'Symbol))
+(define -Void (make-Base 'Void))
+(define -Bytes (make-Base 'Bytes))
+(define -Regexp (make-Base 'Regexp))
+(define -PRegexp (make-Base 'PRegexp))
+(define -Byte-Regexp (make-Base 'Byte-Regexp))
+(define -Byte-PRegexp (make-Base 'Byte-PRegexp))
+(define -String (make-Base 'String))
+(define -Keyword (make-Base 'Keyword))
+(define -Char (make-Base 'Char))
+(define -Syntax make-Syntax)
+(define -Prompt-Tag (make-Base 'Prompt-Tag))
+(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set))
+(define -Path (make-Base 'Path))
+(define -Namespace (make-Base 'Namespace))
+(define -Output-Port (make-Base 'Output-Port))
+(define -Input-Port (make-Base 'Input-Port))  
+
+(define -HT make-Hashtable)
+(define -Promise make-promise-ty)
+
+(define Univ (make-Univ))
+
+(define-syntax -v 
+  (syntax-rules ()
+    [(_ x) (make-F 'x)]))
+
+(define-syntax -poly
+  (syntax-rules ()
+    [(_ (vars ...) ty)
+     (let ([vars (-v vars)] ...)
+       (make-Poly (list 'vars ...) ty))]))
+
+(define-syntax -mu
+  (syntax-rules ()
+    [(_ var ty)
+     (let ([var (-v var)])
+       (make-Mu 'var ty))]))
+
+
+(define -values make-Values)
+
+;; produce the appropriate type of a list of types
+;; that is - if there is exactly one type, just produce it, otherwise produce a values-ty
+;; list[type] -> type
+(define (list->values-ty l)
+  (if (= 1 (length l)) (car l) (-values l)))
+
+(define-syntax *Un
+  (syntax-rules ()
+    [(_ . args) (make-Union (list . args))]))
+
+
+(define -pair make-Pair)
+(define -base make-Base)
+
+(define -struct make-Struct)
+(define -val make-Value)
+
+(define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
+(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 (-lst* . args) (if (null? args)
+                           (-val null)
+                           (-pair (car args) (apply -lst* (cdr args)))))
+
+
+#;(define NE (-mu x (Un N (make-Listof x))))
+(define -NE (-mu x (*Un N (-pair x (-pair Sym (-pair x (-val null)))))))
+
+(define (Un/eff . args)
+  (apply Un (map tc-result-t args)))
+
+(define -Param make-Param)
+
+(define make-pred-ty
+  (case-lambda 
+    [(in out t)
+     (->* 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 -Byte N)
+
+(define (-Tuple l)
+  (foldr -pair (-val '()) l))
+
+(define Any-Syntax 
+  (-mu x
+       (-Syntax (*Un 
+                 (-lst x)                       
+                 (-mu y (*Un x (-pair x y)))
+                 (make-Vector x)
+                 (make-Box x)
+                 N
+                 B
+                 -String
+                 Sym))))
+
+(define Ident (-Syntax Sym))
+
+;; DO NOT USE if t contains #f
+(define (-opt t) (*Un (-val #f) t))
+
+(define-syntax (make-env stx)
+  (syntax-case stx ()
+    [(_ e ...)
+     #`(list
+        #,@(map (lambda (e)
+                  (syntax-case e ()
+                    [(nm ty)
+                     (identifier? #'nm)
+                     #`(list  #'nm ty)]
+                    [(e ty extra-mods ...)
+                     #'(list (let ([new-ns
+                                    (let* ([ns (make-empty-namespace)])
+                                      (namespace-attach-module (current-namespace)
+                                                               'scheme/base
+                                                               ns)
+                                      ns)])
+                               (parameterize ([current-namespace new-ns])
+                                 (namespace-require 'extra-mods) ...
+                                 e))
+                             ty)]))
+                (syntax->list #'(e ...))))]))
+
+;; if t is of the form (Pair t* (Pair t* ... (Listof t*)))
+;; return t*
+;; otherwise, return t
+;; generalize : Type -> Type
+(define (generalize t)
+  (let/ec exit
+    (let loop ([t* t])
+      (match t*
+        [(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
+        [(Pair: t1 t2)
+         (let ([t-new (loop t2)])
+           (if (type-equal? (-lst t1) t-new)
+               t-new
+               (exit t)))]
+        [_ (exit 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 -Byte N)
-  
-  (define (-Tuple l)
-    (foldr -pair (-val '()) l))
-  
-  (define Any-Syntax 
-    (-mu x
-         (-Syntax (*Un 
-                       (-lst x)                       
-                       (-mu y (*Un x (-pair x y)))
-                       (make-Vector x)
-                       (make-Box x)
-                       N
-                       B
-                       -String
-                       Sym))))
-  
-  (define Ident (-Syntax Sym))
-  
-  ;; DO NOT USE if t contains #f
-  (define (-opt t) (*Un (-val #f) t))
-  
-  (define-syntax (make-env stx)
-    (syntax-case stx ()
-      [(_ e ...)
-       #`(list
-          #,@(map (lambda (e)
-                    (syntax-case e ()
-                      [(nm ty)
-                       (identifier? #'nm)
-                       #`(list  #'nm ty)]
-                      [(e ty extra-mods ...)
-                       #'(list (let ([new-ns
-                                      (let* ([ns (make-empty-namespace)])
-                                        (namespace-attach-module (current-namespace)
-                                                                 'scheme/base
-                                                                 ns)
-                                        ns)])
-                                 (parameterize ([current-namespace new-ns])
-                                   (namespace-require 'extra-mods) ...
-                                   e))
-                               ty)]))
-                  (syntax->list #'(e ...))))]))
-  
-  ;; if t is of the form (Pair t* (Pair t* ... (Listof t*)))
-  ;; return t*
-  ;; otherwise, return t
-  ;; generalize : Type -> Type
-  (define (generalize t)
-    (let/ec exit
-      (let loop ([t* t])
-        (match t*
-          [(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
-          [(Pair: t1 t2)
-           (let ([t-new (loop t2)])
-             (if (type-equal? (-lst t1) t-new)
-                 t-new
-                 (exit t)))]
-          [_ (exit t)]))))
 
-  
-  )
diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss
index c43c07e4..9cc23ebe 100644
--- a/collects/typed-scheme/private/type-effect-printer.ss
+++ b/collects/typed-scheme/private/type-effect-printer.ss
@@ -1,145 +1,141 @@
-(module type-effect-printer mzscheme
-  (require "type-rep.ss" "effect-rep.ss" "rep-utils.ss" "tc-utils.ss")
-  (require (lib "plt-match.ss"))
-  (require "planet-requires.ss")  
-  
-  ;; do we attempt to find instantiations of polymorphic types to print? 
-  ;; FIXME - currently broken
-  (define print-poly-types? #f)
-  ;; do we use simple type aliases in printing
-  (define print-aliases #t)
+#lang scheme/base
+(require "type-rep.ss" "effect-rep.ss" "rep-utils.ss" "tc-utils.ss" "planet-requires.ss" scheme/match)
 
-  ;; does t have a type name associated with it currently?
-  ;; has-name : Type -> Maybe[Symbol]
-  (define (has-name? t) 
-    (define ns ((current-type-names)))
-    (let/cc return
-      (unless print-aliases
-        (return #f))
-      (for-each
-       (lambda (pair)
-         (cond [(eq? t (cdr pair))
-                (return (car pair))]))
-       ns)
-      #f))
-      
-  ;; print out an effect
-  ;; print-effect : Effect Port Boolean -> Void
-  (define (print-effect c port write?)
-    (define (fp . args) (apply fprintf port args))    
-    (match c
-      [(Restrict-Effect: t v) (fp "(restrict ~a ~a)" t (syntax-e v))]
-      [(Remove-Effect: t v) (fp "(remove ~a ~a)" t (syntax-e v))]
-      [(Latent-Restrict-Effect: t) (fp "(restrict ~a)" t)]
-      [(Latent-Remove-Effect: t) (fp "(remove ~a)" t)]
-      [(Latent-Var-True-Effect:) (fp "(var #t)")]
-      [(Latent-Var-False-Effect:) (fp "(var #f)")]
-      [(True-Effect:) (fp "T")]
-      [(False-Effect:) (fp "F")]
-      [(Var-True-Effect: v) (fp "(var #t ~a)" (syntax-e v))]
-      [(Var-False-Effect: v) (fp "(var #f ~a)" (syntax-e v))]))
-  
-  
-  ;; print out a type
-  ;; print-type : Type Port Boolean -> Void
-  (define (print-type c port write?)
-    (define (fp . args) (apply fprintf port args)) 
-    (define (print-arr a)
-      (match a
-        [(top-arr:)
-         (fp "Procedure")]
-        [(arr: dom rng rest thn-eff els-eff)
-         (fp "(")
-         (for-each (lambda (t) (fp "~a " t)) dom)
-         (when rest
-           (fp "~a .. " rest))
-         (fp "-> ~a" rng)
-         (unless (and (null? thn-eff) (null? els-eff))
-           (fp " : ~a ~a" thn-eff els-eff))
-         (fp ")")]))
-    (define (tuple? t)
-      (match t
-        [(Pair: a (? tuple?)) #t]
-        [(Value: '()) #t]
-        [_ #f]))
-    (define (tuple-elems t)
-      (match t
-        [(Pair: a e) (cons a (tuple-elems e))]
-        [(Value: '()) null]))
-    ;(fp "~a~n" (Type-seq c))
-    (match c 
-      [(Univ:) (fp "Any")]
-      [(? has-name?) (fp "~a" (has-name? c))]
-      ;; names are just the printed as the original syntax
-      [(Name: stx) (fp "[~a]" (syntax-e stx))]
-      [(App: rator rands stx) 
-       (fp "~a" (cons rator rands))]
-      ;; special cases for lists
-      [(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
-       (fp "(Listof ~a)" elem-ty)]
-      [(Mu: var (Union: (list (Pair: elem-ty (F: var)) (Value: '()))))
-       (fp "(Listof ~a)" elem-ty)]
-      [(Value: v) (cond [(or (symbol? v) (null? v))
-                         (fp "'~a" v)]
-                        [else (fp "~a" v)])]
-      [(? tuple? t)
-       (fp "~a" (cons 'List (tuple-elems t)))]
-      [(Base: n) (fp "~a" n)]      
-      [(Opaque: pred _) (fp "(Opaque ~a)" (syntax-object->datum pred))]
-      [(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))
-        (fp ")")]
-      [(Function: arities)
-       (let ()         
-         (match arities
-           [(list) (fp "(case-lambda)")]
-           [(list a) (print-arr a)]
-           [(list a ...) (fp "(case-lambda ") (for-each print-arr a) (fp ")")]))]
-      [(arr: _ _ _ _ _) (print-arr c)]
-      [(Vector: e) (fp "(Vectorof ~a)" e)]
-      [(Box: e) (fp "(Box ~a)" e)]
-      [(Union: elems) (fp "~a" (cons 'U elems))]
-      [(Pair: l r) (fp "(Pair ~a ~a)" l r)]
-      [(F: nm) (fp "<~a>" nm)]      
-      [(Values: (list v ...)) (fp "~a" (cons 'values v))]
-      [(Param: in out) 
-       (if (equal? in out)
-           (fp "(Paramter ~a)" in)           
-           (fp "(Parameter ~a ~a)" in out))]
-      [(Hashtable: k v) (fp "(HashTable ~a ~a)" k v)]
-      #;
-      [(Poly-unsafe: n b) (fp "(unsafe-poly ~a ~a ~a)" (Type-seq c) n b)]
-      [(Poly-names: names body) 
-       #;(fprintf (current-error-port) "POLY SEQ: ~a~n" (Type-seq body))
-       (fp "(All ~a ~a)" names body)]
-      #;
-      [(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)]
-      [(Mu: x (Syntax: (Union: (list
-                                (Base: 'Number) 
-                                (Base: 'Boolean)
-                                (Base: 'Symbol)
-                                (Base: 'String)
-                                (Mu: var (Union: (list (Value: '()) (Pair: (F: x) (F: var)))))
-                                (Mu: y (Union: (list (F: x) (Pair: (F: x) (F: y)))))
-                                (Vector: (F: x))
-                                (Box: (F: x))))))
-       (fp "SyntaxObject")]
-      [(Mu-name: name body) (fp "(mu ~a ~a ~a)" (Type-seq c) name body)]
-      ;; FIXME - this should not be used
-      #;
-      [(Scope: sc) (fp "(Scope ~a)" sc)]
-      #;
-      [(B: idx) (fp "(B ~a)" idx)]      
-      [(Syntax: t) (fp "(Syntax ~a)" t)]
-      [(Instance: t) (fp "(Instance ~a)" t)]
-      [(Class: pf nf ms) (fp "(Class)")]
-      [else (fp "Unknown Type: ~a" (struct->vector c))]
-      ))
-  
-  (set-box! print-type* print-type)
-  (set-box! print-effect* print-effect)
-  
-  )
+;; do we attempt to find instantiations of polymorphic types to print? 
+;; FIXME - currently broken
+(define print-poly-types? #f)
+;; do we use simple type aliases in printing
+(define print-aliases #t)
+
+;; does t have a type name associated with it currently?
+;; has-name : Type -> Maybe[Symbol]
+(define (has-name? t) 
+  (define ns ((current-type-names)))
+  (let/cc return
+    (unless print-aliases
+      (return #f))
+    (for-each
+     (lambda (pair)
+       (cond [(eq? t (cdr pair))
+              (return (car pair))]))
+     ns)
+    #f))
+
+;; print out an effect
+;; print-effect : Effect Port Boolean -> Void
+(define (print-effect c port write?)
+  (define (fp . args) (apply fprintf port args))    
+  (match c
+    [(Restrict-Effect: t v) (fp "(restrict ~a ~a)" t (syntax-e v))]
+    [(Remove-Effect: t v) (fp "(remove ~a ~a)" t (syntax-e v))]
+    [(Latent-Restrict-Effect: t) (fp "(restrict ~a)" t)]
+    [(Latent-Remove-Effect: t) (fp "(remove ~a)" t)]
+    [(Latent-Var-True-Effect:) (fp "(var #t)")]
+    [(Latent-Var-False-Effect:) (fp "(var #f)")]
+    [(True-Effect:) (fp "T")]
+    [(False-Effect:) (fp "F")]
+    [(Var-True-Effect: v) (fp "(var #t ~a)" (syntax-e v))]
+    [(Var-False-Effect: v) (fp "(var #f ~a)" (syntax-e v))]))
+
+
+;; print out a type
+;; print-type : Type Port Boolean -> Void
+(define (print-type c port write?)
+  (define (fp . args) (apply fprintf port args)) 
+  (define (print-arr a)
+    (match a
+      [(top-arr:)
+       (fp "Procedure")]
+      [(arr: dom rng rest thn-eff els-eff)
+       (fp "(")
+       (for-each (lambda (t) (fp "~a " t)) dom)
+       (when rest
+         (fp "~a .. " rest))
+       (fp "-> ~a" rng)
+       (unless (and (null? thn-eff) (null? els-eff))
+         (fp " : ~a ~a" thn-eff els-eff))
+       (fp ")")]))
+  (define (tuple? t)
+    (match t
+      [(Pair: a (? tuple?)) #t]
+      [(Value: '()) #t]
+      [_ #f]))
+  (define (tuple-elems t)
+    (match t
+      [(Pair: a e) (cons a (tuple-elems e))]
+      [(Value: '()) null]))
+  ;(fp "~a~n" (Type-seq c))
+  (match c 
+    [(Univ:) (fp "Any")]
+    [(? has-name?) (fp "~a" (has-name? c))]
+    ;; names are just the printed as the original syntax
+    [(Name: stx) (fp "[~a]" (syntax-e stx))]
+    [(App: rator rands stx) 
+     (fp "~a" (cons rator rands))]
+    ;; special cases for lists
+    [(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
+     (fp "(Listof ~a)" elem-ty)]
+    [(Mu: var (Union: (list (Pair: elem-ty (F: var)) (Value: '()))))
+     (fp "(Listof ~a)" elem-ty)]
+    [(Value: v) (cond [(or (symbol? v) (null? v))
+                       (fp "'~a" v)]
+                      [else (fp "~a" v)])]
+    [(? tuple? t)
+     (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) 
+     (fp "#(struct:~a ~a" nm flds)
+     (when proc
+       (fp " ~a" proc))
+     (fp ")")]
+    [(Function: arities)
+     (let ()         
+       (match arities
+         [(list) (fp "(case-lambda)")]
+         [(list a) (print-arr a)]
+         [(list a ...) (fp "(case-lambda ") (for-each print-arr a) (fp ")")]))]
+    [(arr: _ _ _ _ _) (print-arr c)]
+    [(Vector: e) (fp "(Vectorof ~a)" e)]
+    [(Box: e) (fp "(Box ~a)" e)]
+    [(Union: elems) (fp "~a" (cons 'U elems))]
+    [(Pair: l r) (fp "(Pair ~a ~a)" l r)]
+    [(F: nm) (fp "<~a>" nm)]      
+    [(Values: (list v ...)) (fp "~a" (cons 'values v))]
+    [(Param: in out) 
+     (if (equal? in out)
+         (fp "(Paramter ~a)" in)           
+         (fp "(Parameter ~a ~a)" in out))]
+    [(Hashtable: k v) (fp "(HashTable ~a ~a)" k v)]
+    #;
+    [(Poly-unsafe: n b) (fp "(unsafe-poly ~a ~a ~a)" (Type-seq c) n b)]
+    [(Poly-names: names body) 
+     #;(fprintf (current-error-port) "POLY SEQ: ~a~n" (Type-seq body))
+     (fp "(All ~a ~a)" names body)]
+    #;
+    [(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)]
+    [(Mu: x (Syntax: (Union: (list
+                              (Base: 'Number) 
+                              (Base: 'Boolean)
+                              (Base: 'Symbol)
+                              (Base: 'String)
+                              (Mu: var (Union: (list (Value: '()) (Pair: (F: x) (F: var)))))
+                              (Mu: y (Union: (list (F: x) (Pair: (F: x) (F: y)))))
+                              (Vector: (F: x))
+                              (Box: (F: x))))))
+     (fp "SyntaxObject")]
+    [(Mu-name: name body) (fp "(mu ~a ~a ~a)" (Type-seq c) name body)]
+    ;; FIXME - this should not be used
+    #;
+    [(Scope: sc) (fp "(Scope ~a)" sc)]
+    #;
+    [(B: idx) (fp "(B ~a)" idx)]      
+    [(Syntax: t) (fp "(Syntax ~a)" t)]
+    [(Instance: t) (fp "(Instance ~a)" t)]
+    [(Class: pf nf ms) (fp "(Class)")]
+    [else (fp "Unknown Type: ~a" (struct->vector c))]
+    ))
+
+(set-box! print-type* print-type)
+(set-box! print-effect* print-effect)
diff --git a/collects/typed-scheme/private/union.ss b/collects/typed-scheme/private/union.ss
index 517ad141..36fa6365 100644
--- a/collects/typed-scheme/private/union.ss
+++ b/collects/typed-scheme/private/union.ss
@@ -1,62 +1,61 @@
-(module union mzscheme
-  
-  (require "type-rep.ss" "subtype.ss" "tc-utils.ss"
-           "type-effect-printer.ss" "rep-utils.ss"
-           "type-comparison.ss")
-  (require (lib "plt-match.ss") (lib "list.ss") (lib "trace.ss"))
-  
-  (provide Un #;(rename *Un Un))
-  
-  (define (make-union* set)
-    (match set
-      [(list t) t]
-      [_ (make-Union set)]))
-  
-  (define empty-union (make-Union null))
-  
-  (define (flat t) 
-    (match t
-      [(Union: es) es]
-      [_ (list t)]))    
-  #;(define (Values-types t) (match t [(Values: ts) ts]))
-  (define (remove-subtypes ts)
-    (let loop ([ts* ts] [result '()])
-      (cond [(null? ts*) (reverse result)]
-            [(ormap (lambda (t) (subtype (car ts*) t)) result) (loop (cdr ts*) result)]
-            [else (loop (cdr ts*) (cons (car ts*) result))])))
-  
-  (define Un
-    (case-lambda 
-      [() empty-union]
-      [args
-       ;; a is a Type (not a union type)
-       ;; b is a List[Type]
-       (define (union2 a b)     
-         (define b* (make-union* b))
-         (cond 
-           [(subtype a b*) (list b*)]
-           [(subtype b* a) (list a)]            
-           [else (cons a b)]))
-       #;(union-count!)    
-       (let ([types (remove-dups (sort (apply append (map flat args)) type<?))])
-         (cond
-           [(null? types) (make-union* null)]
-           [(null? (cdr types)) (car types)]           
-           [(ormap Values? types)
-            (if (andmap Values? types)
-                (make-Values (apply map Un (map Values-types types)))
-                (int-err "Un: should not take the union of multiple values with some other type: ~a" types))]
-           [else (make-union* #;(remove-subtypes types) (foldr union2 null types))]))]))
-  
-  #;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args)
-  
-  #;(define (*Un . args) (Un-intern args))
-  
-  ;(trace Un)
-  
-  (define (u-maker args) (apply Un args))
-  
-  ;(trace u-maker)
-  (set-union-maker! u-maker)
-  
-  )
+#lang scheme/base
+
+(require "type-rep.ss" "subtype.ss" "tc-utils.ss"
+         "type-effect-printer.ss" "rep-utils.ss"
+         "type-comparison.ss"
+         scheme/match mzlib/trace)
+
+(provide Un #;(rename *Un Un))
+
+(define (make-union* set)
+  (match set
+    [(list t) t]
+    [_ (make-Union set)]))
+
+(define empty-union (make-Union null))
+
+(define (flat t) 
+  (match t
+    [(Union: es) es]
+    [_ (list t)]))    
+#;(define (Values-types t) (match t [(Values: ts) ts]))
+(define (remove-subtypes ts)
+  (let loop ([ts* ts] [result '()])
+    (cond [(null? ts*) (reverse result)]
+          [(ormap (lambda (t) (subtype (car ts*) t)) result) (loop (cdr ts*) result)]
+          [else (loop (cdr ts*) (cons (car ts*) result))])))
+
+(define Un
+  (case-lambda 
+    [() empty-union]
+    [args
+     ;; a is a Type (not a union type)
+     ;; b is a List[Type]
+     (define (union2 a b)     
+       (define b* (make-union* b))
+       (cond 
+         [(subtype a b*) (list b*)]
+         [(subtype b* a) (list a)]            
+         [else (cons a b)]))
+     #;(union-count!)    
+     (let ([types (remove-dups (sort (apply append (map flat args)) type<?))])
+       (cond
+         [(null? types) (make-union* null)]
+         [(null? (cdr types)) (car types)]           
+         [(ormap Values? types)
+          (if (andmap Values? types)
+              (make-Values (apply map Un (map Values-types types)))
+              (int-err "Un: should not take the union of multiple values with some other type: ~a" types))]
+         [else (make-union* #;(remove-subtypes types) (foldr union2 null types))]))]))
+
+#;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args)
+
+#;(define (*Un . args) (Un-intern args))
+
+;(trace Un)
+
+(define (u-maker args) (apply Un args))
+
+;(trace u-maker)
+(set-union-maker! u-maker)
+
diff --git a/collects/typed-scheme/typed-reader.ss b/collects/typed-scheme/typed-reader.ss
index 1bf78355..7a14a18b 100644
--- a/collects/typed-scheme/typed-reader.ss
+++ b/collects/typed-scheme/typed-reader.ss
@@ -1,90 +1,88 @@
-(module typed-reader mzscheme
-  (require (lib "etc.ss"))
-  
-  (require-for-template "private/prims.ss")  
-  
-  ;; Provides raise-read-error and raise-read-eof-error
-  (require (lib "readerr.ss" "syntax"))
-  
-  (define (skip-whitespace port)
-    ;; Skips whitespace characters, sensitive to the current
-    ;; readtable's definition of whitespace
-    (let ([ch (peek-char port)])
-      (unless (eof-object? ch)
-        ;; Consult current readtable:
-        (let-values ([(like-ch/sym proc dispatch-proc) 
-                      (readtable-mapping (current-readtable) ch)])
-          ;; If like-ch/sym is whitespace, then ch is whitespace
-          (when (and (char? like-ch/sym)
-                     (char-whitespace? like-ch/sym))
-            (read-char port)
-            (skip-whitespace port))))))
-  
-  (define (skip-comments read-one port src)
-    ;; Recursive read, but skip comments and detect EOF
-    (let loop ()
-      (let ([v (read-one)])
-        (cond
-          [(special-comment? v) (loop)]
-          [(eof-object? v)
-           (let-values ([(l c p) (port-next-location port)])
-             (raise-read-eof-error "unexpected EOF in type annotation" src l c p 1))]
-          [else v]))))
+#lang scheme/base
 
-  (define (parse port read-one src)    
-    (skip-whitespace port)
-    (let ([name (read-one)])
-      (begin0
-        (begin (skip-whitespace port)
-               (let ([next (read-one)])
-                 (case (syntax-e next)
-                   ;; type annotation
-                   [(:) (skip-whitespace port)
-                        (syntax-property name 'type-label (syntax-object->datum (read-one)))]
-                   [(::) (skip-whitespace port)
-                         (datum->syntax-object name `(ann ,name : ,(read-one)))]
-                   [(@) (let ([elems (let loop ([es '()])
-                                       (skip-whitespace port)
-                                       (if (equal? #\} (peek-char port))
-                                           (reverse es)
-                                           (loop (cons (read-one) es))))])
-                          (datum->syntax-object name `(inst ,name : ,@elems)))]
-                   ;; arbitrary property annotation
-                   [(PROP) (skip-whitespace port)
-                           (let* ([prop-name (syntax-e (read-one))])   
-                             (skip-whitespace port)
-                             (syntax-property name prop-name (read-one)))]
-                   ;; type annotation
-                   [else (syntax-property name 'type-label (syntax-object->datum next))])))
-        (skip-whitespace port)
-        (let ([c (read-char port)])
-          #;(printf "char: ~a" c)
-          (unless (equal? #\} c)
-            (let-values ([(l c p) (port-next-location port)])
-              (raise-read-error (format "typed expression ~a not properly terminated" (syntax-object->datum name)) src l c p 1)))))))
-  
-  (define parse-id-type
-    (case-lambda
-      [(ch port src line col pos)
-       ;; `read-syntax' mode
-       (datum->syntax-object
-        #f
-        (parse port 
-                     (lambda () (read-syntax src port ))
-                     src)
-        (let-values ([(l c p) (port-next-location port)])
-          (list src line col pos (and pos (- p pos)))))]))
+(require (for-template "private/prims.ss"))  
 
-  (define readtable
-    (make-readtable #f #\{ 'dispatch-macro parse-id-type))
-  
-  (define (*read inp)
-    (parameterize ([current-readtable readtable])
-      (read inp)))
-  
-  (define (*read-syntax src port)
-    (parameterize ([current-readtable readtable])
-      (read-syntax src port)))
-  
-  (provide (rename *read read) (rename *read-syntax read-syntax))
-  )
+;; Provides raise-read-error and raise-read-eof-error
+(require syntax/readerr)
+
+(define (skip-whitespace port)
+  ;; Skips whitespace characters, sensitive to the current
+  ;; readtable's definition of whitespace
+  (let ([ch (peek-char port)])
+    (unless (eof-object? ch)
+      ;; Consult current readtable:
+      (let-values ([(like-ch/sym proc dispatch-proc) 
+                    (readtable-mapping (current-readtable) ch)])
+        ;; If like-ch/sym is whitespace, then ch is whitespace
+        (when (and (char? like-ch/sym)
+                   (char-whitespace? like-ch/sym))
+          (read-char port)
+          (skip-whitespace port))))))
+
+(define (skip-comments read-one port src)
+  ;; Recursive read, but skip comments and detect EOF
+  (let loop ()
+    (let ([v (read-one)])
+      (cond
+        [(special-comment? v) (loop)]
+        [(eof-object? v)
+         (let-values ([(l c p) (port-next-location port)])
+           (raise-read-eof-error "unexpected EOF in type annotation" src l c p 1))]
+        [else v]))))
+
+(define (parse port read-one src)    
+  (skip-whitespace port)
+  (let ([name (read-one)])
+    (begin0
+      (begin (skip-whitespace port)
+             (let ([next (read-one)])
+               (case (syntax-e next)
+                 ;; type annotation
+                 [(:) (skip-whitespace port)
+                      (syntax-property name 'type-label (syntax->datum (read-one)))]
+                 [(::) (skip-whitespace port)
+                       (datum->syntax name `(ann ,name : ,(read-one)))]
+                 [(@) (let ([elems (let loop ([es '()])
+                                     (skip-whitespace port)
+                                     (if (equal? #\} (peek-char port))
+                                         (reverse es)
+                                         (loop (cons (read-one) es))))])
+                        (datum->syntax name `(inst ,name : ,@elems)))]
+                 ;; arbitrary property annotation
+                 [(PROP) (skip-whitespace port)
+                         (let* ([prop-name (syntax-e (read-one))])   
+                           (skip-whitespace port)
+                           (syntax-property name prop-name (read-one)))]
+                 ;; type annotation
+                 [else (syntax-property name 'type-label (syntax->datum next))])))
+      (skip-whitespace port)
+      (let ([c (read-char port)])
+        #;(printf "char: ~a" c)
+        (unless (equal? #\} c)
+          (let-values ([(l c p) (port-next-location port)])
+            (raise-read-error (format "typed expression ~a not properly terminated" (syntax->datum name)) src l c p 1)))))))
+
+(define parse-id-type
+  (case-lambda
+    [(ch port src line col pos)
+     ;; `read-syntax' mode
+     (datum->syntax
+      #f
+      (parse port 
+             (lambda () (read-syntax src port ))
+             src)
+      (let-values ([(l c p) (port-next-location port)])
+        (list src line col pos (and pos (- p pos)))))]))
+
+(define readtable
+  (make-readtable #f #\{ 'dispatch-macro parse-id-type))
+
+(define (*read inp)
+  (parameterize ([current-readtable readtable])
+    (read inp)))
+
+(define (*read-syntax src port)
+  (parameterize ([current-readtable readtable])
+    (read-syntax src port)))
+
+(provide (rename-out [*read read] [*read-syntax read-syntax]))