diff --git a/collects/tests/typed-scheme/fail/bad-map-poly.ss b/collects/tests/typed-scheme/fail/bad-map-poly.ss
new file mode 100644
index 00000000..280bd9bc
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/bad-map-poly.ss
@@ -0,0 +1,15 @@
+#;
+(exn-pred exn:fail:contract? ".*interface for bad-map.*")
+#lang scheme/load
+
+(module bad-map scheme
+  (provide bad-map)
+  (define (bad-map f l)
+    (list (f 'quux))))
+
+(module use-bad-map typed-scheme
+  (require/typed 'bad-map
+                 [bad-map (All (A B) ((A -> B) (Listof A) -> (Listof B)))])
+  (bad-map add1 (list 12 13 14)))
+
+(require 'use-bad-map)
diff --git a/collects/tests/typed-scheme/succeed/apply-dots-list.ss b/collects/tests/typed-scheme/succeed/apply-dots-list.ss
new file mode 100644
index 00000000..d068a14e
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/apply-dots-list.ss
@@ -0,0 +1,25 @@
+
+;; Change the lang to scheme for untyped version
+#lang typed-scheme
+
+(define tests (list (list (λ() 1) 1 "test 1")
+                   (list (λ() 2) 2 "test 2")))
+
+; Comment out the type signature when running untyped
+(: check-all (All (A ...) ((List (-> A) A String) ... A -> Void)))
+(define (check-all . tests)
+ (let aux ([tests tests]
+           [num-passed 0])
+   (if (null? tests)
+       (printf "~a tests passed.~n" num-passed)
+       (let ((test (car tests)))
+         (let ((actual ((car test)))
+               (expected (cadr test))
+               (msg (caddr test)))
+           (if (equal? actual expected)
+               (aux (cdr tests) (+ num-passed 1))
+               (printf "Test failed: ~a. Expected ~a, got ~a.~n"
+                       msg expected actual)))))))
+
+(apply check-all tests) ; Works in untyped, but not in typed
+(check-all (car tests) (cadr tests)) ; Works in typed or untyped
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/no-bound-fl.ss b/collects/tests/typed-scheme/succeed/no-bound-fl.ss
new file mode 100644
index 00000000..1f9bd526
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/no-bound-fl.ss
@@ -0,0 +1,11 @@
+#lang typed-scheme
+
+(: fold-left (All (a b ...) ((a b ... -> a) a (Listof b) ... -> a)))
+(define (fold-left f a . bss)
+  (if (ormap null? bss)
+      a
+      (apply fold-left
+             f
+             (apply f a (map car bss))
+             (map cdr bss))))
+
diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
index e509fbb7..35b55618 100644
--- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
@@ -78,6 +78,10 @@
    [(All (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))]
    [(∀ (a) (Listof a)) (-poly (a) (make-Listof  a))]
    [(∀ (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))]
+   [(All (a ...) (a ... -> Number))
+    (-polydots (a) ((list) [a a] . ->... . N))]
+   [(All (a ...) (values a ...))
+    (-polydots (a) (make-ValuesDots (list) a 'a))]
    [(case-lambda (Number -> Boolean) (Number Number -> Number)) (cl-> [(N) B]
                                                                       [(N N) N])]
    [1 (-val 1)]
@@ -89,6 +93,8 @@
    
    [a (-v a) (extend-env (list 'a) (list (-v a))
                             initial-tvar-env)]
+   [(All (a ...) (a ... -> Number))
+    (-polydots (a) ((list) [a a] . ->... . N))]
    
    ))
 
diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss
index dc5dc330..396c94c4 100644
--- a/collects/typed-scheme/env/init-envs.ss
+++ b/collects/typed-scheme/env/init-envs.ss
@@ -29,6 +29,9 @@
      `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))]
     [(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)
+                                                      (quote-syntax ,pred)
+                                                      (syntax-local-certifier))]
     [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
     [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
     [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]
diff --git a/collects/typed-scheme/env/lexical-env.ss b/collects/typed-scheme/env/lexical-env.ss
index 9998ad3c..07f8134c 100644
--- a/collects/typed-scheme/env/lexical-env.ss
+++ b/collects/typed-scheme/env/lexical-env.ss
@@ -31,7 +31,7 @@
                                   =>
                                   (lambda (a)
                                     (-lst (substitute Univ (cdr a) (car a))))]
-                                 [else (lookup-fail (syntax-e i))]))))))
+                                 [else (lookup-fail i)]))))))
 
 ;; refine the type of i in the lexical env
 ;; (identifier type -> type) identifier -> environment
diff --git a/collects/typed-scheme/env/type-env.ss b/collects/typed-scheme/env/type-env.ss
index dda31d66..444aeebd 100644
--- a/collects/typed-scheme/env/type-env.ss
+++ b/collects/typed-scheme/env/type-env.ss
@@ -39,7 +39,7 @@
 ;; given an identifier, return the type associated with it
 ;; if none found, calls lookup-fail
 ;; identifier -> type 
-(define (lookup-type id [fail-handler (lambda () (lookup-fail (syntax-e id)))])
+(define (lookup-type id [fail-handler (lambda () (lookup-type-fail id))])
   (let ([v (module-identifier-mapping-get the-mapping id fail-handler)])
     (if (box? v) (unbox v) v)))
 
diff --git a/collects/typed-scheme/env/type-name-env.ss b/collects/typed-scheme/env/type-name-env.ss
index 4c35e9d6..7c41a3de 100644
--- a/collects/typed-scheme/env/type-name-env.ss
+++ b/collects/typed-scheme/env/type-name-env.ss
@@ -35,7 +35,7 @@
 ;; given an identifier, return the type associated with it
 ;; optional argument is failure continuation - default calls lookup-fail
 ;; identifier (-> error) -> type 
-(define (lookup-type-name id [k (lambda () (lookup-fail (syntax-e id)))])
+(define (lookup-type-name id [k (lambda () (lookup-type-fail id))])
   (begin0
     (module-identifier-mapping-get the-mapping id k)
     (add-type-name-reference id)))
diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss
index ea3648b0..18ff9b65 100644
--- a/collects/typed-scheme/infer/infer-unit.ss
+++ b/collects/typed-scheme/infer/infer-unit.ss
@@ -243,6 +243,9 @@
           [(a a) empty]
           [(_ (Univ:)) empty]
           
+          [((Refinement: S _ _) T)
+           (cg S T)]
+          
           [((F: (? (lambda (e) (memq e X)) v)) S)
            (when (match S
                    [(F: v*)
diff --git a/collects/typed-scheme/infer/infer.ss b/collects/typed-scheme/infer/infer.ss
index b8c37883..c660783e 100644
--- a/collects/typed-scheme/infer/infer.ss
+++ b/collects/typed-scheme/infer/infer.ss
@@ -3,10 +3,11 @@
 (require (except-in "../utils/utils.ss" infer))
 (require "infer-unit.ss" "constraints.ss" "dmap.ss" "signatures.ss"
          "restrict.ss" "promote-demote.ss"
-         (only-in scheme/unit provide-signature-elements)
+         (only-in scheme/unit provide-signature-elements
+                  define-values/invoke-unit/infer link)
          (utils unit-utils))
          
 (provide-signature-elements restrict^ infer^)
 
-(define-values/link-units/infer
-  infer@ constraints@ dmap@ restrict@ promote-demote@)
+(define-values/invoke-unit/infer
+  (link infer@ constraints@ dmap@ restrict@ promote-demote@))
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 2ce97160..3b6ce080 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -418,11 +418,12 @@
 [symbol->string (Sym . -> . -String)]
 [vector-length (-poly (a) ((-vec a) . -> . -Integer))]
 
-[call-with-input-file (-poly (a) (cl-> [(-String (-Port . -> . a))  a]
-                                       [(-String (-Port . -> . a) Sym)  a]))]
+[call-with-input-file (-poly (a) (-String (-Input-Port . -> . a) #:mode (Un (-val 'binary) (-val 'text)) #f . ->key .  a))]
+[call-with-output-file (-poly (a) (-String (-Output-Port . -> . a)
+                                   #:exists (one-of/c error 'append 'update 'replace 'truncate 'truncate/replace) #f
+                                   #:mode (Un (-val 'binary) (-val 'text)) #f 
+                                   . ->key .  a))]
 
-[call-with-output-file (-poly (a) (cl-> [(-String (-Port . -> . a))  a]
-                                        [(-String (-Port . -> . a) Sym)  a]))]
 [current-output-port (-Param -Output-Port -Output-Port)]
 [current-error-port (-Param -Output-Port -Output-Port)]
 [current-input-port (-Param -Input-Port -Input-Port)]
@@ -544,11 +545,29 @@
 [list->string ((-lst -Char) . -> . -String)]
 [string->list (-String . -> . (-lst -Char))]
 [sort (-poly (a) ((-lst a) (a a . -> . B) . -> . (-lst a)))]
+[find-system-path (Sym . -> . -Path)]
+
+;; scheme/cmdline
+
+[parse-command-line
+ (let ([mode-sym (one-of/c 'once-each 'once-any 'multi 'final 'help-labels)])
+   (-polydots (b a)
+              (cl->* (-Pathlike 
+                      (Un (-lst -String) (-vec -String))
+                      (-lst (-pair mode-sym (-lst (-lst Univ))))
+                      ((list Univ) [a a] . ->... . b)
+                      (-lst -String)
+                      . -> . b))))]
 
 ;; scheme/list
 [last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
                        . -> . 
                        (Un (-pair a a) (-pair a (-val '())))))]
+[remove-duplicates
+ (-poly (a)
+        (cl->*
+         ((-lst a) . -> . (-lst a))
+         ((-lst a) (a a . -> . Univ) . -> . (-lst a))))]
 
 ;; scheme/tcp
 [tcp-listener? (make-pred-ty -TCP-Listener)]
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index 0f8be85b..ef555e6c 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -8,7 +8,7 @@
          (utils tc-utils stxclass-util)
          syntax/stx
          stxclass stxclass/util
-         (env type-environments type-name-env type-alias-env)
+         (env type-environments type-name-env type-alias-env lexical-env)
          (prefix-in t: "base-types-extra.ss")
          scheme/match 
          (for-template scheme/base "base-types-extra.ss"))
@@ -296,6 +296,13 @@
         (map list
              (map syntax-e (syntax->list #'(mname ...)))
              (map parse-type (syntax->list #'(mty ...)))))]
+      [(Refinement p?)
+       (and (eq? (syntax-e #'Refinement) 'Refinement)
+            (identifier? #'p?))
+       (match (lookup-type/lexical #'p?)
+              [(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
+               (make-Refinement dom #'p? (syntax-local-certifier))]
+              [t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
       [(Instance t)
        (eq? (syntax-e #'Instance) 'Instance)
        (let ([v (parse-type #'t)])
diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index 696c9c63..a5ec8287 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -343,7 +343,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
                                             (list #'struct-info
                                                   #'maker
                                                   #'pred
-                                                  (list #'sel ...)
+                                                  (reverse (list #'sel ...))
                                                   (list mut ...)
                                                   #f))))
                        #,(internal #'(define-typed-struct-internal nm ([fld : ty] ...) #:type-only))
@@ -407,4 +407,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
     [(_ [i:id t] ...)
      (syntax/loc stx
        (begin (: i t) ...
-              (provide i ...)))]))
\ No newline at end of file
+              (provide i ...)))]))
+
+(define-syntax (declare-refinement stx)
+  (syntax-parse stx
+    [(_ p:id)
+     (quasisyntax/loc stx #,(internal #'(declare-refinement-internal p)))]))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss
index 930437b7..87377316 100644
--- a/collects/typed-scheme/private/type-contract.ss
+++ b/collects/typed-scheme/private/type-contract.ss
@@ -62,6 +62,8 @@
          #`(listof #,(t->c elem-ty))]
         [(? (lambda (e) (eq? t:Any-Syntax e))) #'syntax?]
         [(Base: sym cnt) cnt]
+        [(Refinement: par p? cert)
+         #`(and/c #,(t->c par) (flat-contract #,(cert p?)))]
         [(Union: elems) 
          (with-syntax 
              ([cnts (map t->c elems)])
@@ -100,7 +102,7 @@
         [(Pair: t1 t2)
          #`(cons/c #,(t->c t1) #,(t->c t2))]
         [(Opaque: p? cert)
-         #`(flat-contract #,(cert p?))]
+         #`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))]
         [(F: v) (cond [(assoc v (vars)) => (if pos? second third)]
                       [else (int-err "unknown var: ~a" v)])]
 	[(Poly: vs (and b (Function: _)))
@@ -122,7 +124,8 @@
         [(Instance: _) #'(is-a?/c object%)]
         [(Class: _ _ _) #'(subclass?/c object%)]
         [(Value: '()) #'null?]
-        [(Struct: _ _ _ _ #f pred? cert) (cert pred?)]
+        [(Struct: _ _ _ _ #f pred? cert) 
+         #`(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 bfd1605f..754884c0 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -201,7 +201,7 @@
                          poly?
                          pred-id
                          cert)]
-    [#:key (gensym)])
+    [#:key #f #;(gensym)])
 
 
 ;; v : Scheme Value
@@ -243,6 +243,17 @@
 ;; value : Type
 (dt Hashtable ([key Type/c] [value Type/c]) [#:key 'hash])
 
+;; parent : Type
+;; pred : Identifier
+;; cert : Certifier
+(dt Refinement (parent pred cert)
+    [#:key (Type-key parent)]
+    [#:intern (list parent (hash-id pred))]
+    [#:fold-rhs (*Refinement (type-rec-id parent) pred cert)]
+    [#:frees (free-vars* parent)
+             (free-idxs* parent)])
+    
+
 ;; t : Type
 (dt Syntax ([t Type/c]) [#:key 'syntax])
 
@@ -400,7 +411,7 @@
                     (map sb kws))]
        [#:ValuesDots rs dty dbound
                      (*ValuesDots (map sb rs)
-                                  (sb dty)                                  
+                                  (sb dty)
                                   (if (eqv? dbound (+ count outer)) (F-n image) dbound))]
        [#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
        [#:PolyDots n body* 
diff --git a/collects/typed-scheme/ts-guide.scrbl b/collects/typed-scheme/ts-guide.scrbl
index 079a86fb..d3af990c 100644
--- a/collects/typed-scheme/ts-guide.scrbl
+++ b/collects/typed-scheme/ts-guide.scrbl
@@ -62,11 +62,11 @@ typed-scheme
 
 There are two differences between these programs:
 
-@itemize{
+@itemize[
   @item*[@elem{The Language}]{@schememodname[scheme] has been replaced by @schememodname[typed-scheme].}
 
   @item*[@elem{The Type Annotation}]{We have added a type annotation
-for the @scheme[fib] function, using the @scheme[:] form.}  }
+for the @scheme[fib] function, using the @scheme[:] form.}  ]
 
 In general, these are most of the changes that have to be made to a
 PLT Scheme program to transform it into a Typed Scheme program.
diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/ts-reference.scrbl
index c2982e25..d2911b68 100644
--- a/collects/typed-scheme/ts-reference.scrbl
+++ b/collects/typed-scheme/ts-reference.scrbl
@@ -87,7 +87,7 @@ The following base types are parameteric in their type arguments.
 types @scheme[t ...].  This can only appear as the return type of a
 function.}
 @defform/none[v]{where @scheme[v] is a number, boolean or string, is the singleton type containing only that value}
-@defform/none['sym]{where @scheme[sym] is a symbol, is the singleton type containing only that symbol}
+@defform/none['val]{where @scheme[val] is a Scheme value, is the singleton type containing only that value}
 @defform/none[i]{where @scheme[i] is an identifier can be a reference to a type
 name or a type variable}
 @defform[(Rec n t)]{is a recursive type where @scheme[n] is bound to the
@@ -294,3 +294,18 @@ Other libraries can be used with Typed Scheme via
                [check-version (-> (U Symbol (Listof Any)))])
 (check-version)
 ]
+
+@section{Typed Scheme Syntax Without Type Checking}
+
+@defmodulelang[typed-scheme/no-check]
+
+On occasions where the Typed Scheme syntax is useful, but actual
+typechecking is not desired, the @schememodname[typed-scheme/no-check]
+language is useful.  It provides the same bindings and syntax as Typed
+Scheme, but does no type checking.
+
+Examples:
+
+@schememod[typed-scheme/no-check
+(: x Number)
+(define x "not-a-number")]
\ No newline at end of file
diff --git a/collects/typed-scheme/typecheck/internal-forms.ss b/collects/typed-scheme/typecheck/internal-forms.ss
index b85dd96c..a0ce6e9c 100644
--- a/collects/typed-scheme/typecheck/internal-forms.ss
+++ b/collects/typed-scheme/typecheck/internal-forms.ss
@@ -11,4 +11,6 @@
                 define-typed-struct-internal
                 define-typed-struct/exec-internal
                 assert-predicate-internal
+                declare-refinement-internal
                 :-internal)
+
diff --git a/collects/typed-scheme/typecheck/provide-handling.ss b/collects/typed-scheme/typecheck/provide-handling.ss
index 66b3576a..c2149375 100644
--- a/collects/typed-scheme/typecheck/provide-handling.ss
+++ b/collects/typed-scheme/typecheck/provide-handling.ss
@@ -5,7 +5,7 @@
          syntax/kerncase syntax/boundmap
          (env type-name-env type-alias-env)
          mzlib/trace
-         (private type-contract)
+         (private type-contract typed-renaming)
          (rep type-rep)
 	 (utils tc-utils)
          "def-binding.ss")
@@ -13,7 +13,8 @@
 (require (for-template scheme/base
                        scheme/contract))
 
-(provide remove-provides provide? generate-prov)
+(provide remove-provides provide? generate-prov
+         get-alternate)
 
 (define (provide? form)    
   (kernel-syntax-case form #f
@@ -24,6 +25,12 @@
 (define (remove-provides forms)
   (filter (lambda (e) (not (provide? e))) (syntax->list forms)))
 
+
+(define (renamer id #:alt [alt #f])
+  (if alt
+      (make-typed-renaming (syntax-property id 'not-free-identifier=? #t) alt)
+      (make-rename-transformer (syntax-property id 'not-free-identifier=? #t))))
+
 (define (generate-prov stx-defs val-defs)
   (define mapping (make-free-identifier-mapping))
   (lambda (form)
@@ -54,35 +61,35 @@
                             (define/contract cnt-id #,cnt id)
                             (define-syntax export-id
                               (if (unbox typed-context?)
-                                  (make-rename-transformer (syntax-property #'id 
-                                                                            'not-free-identifier=? #t))
-                                  (make-rename-transformer (syntax-property #'cnt-id
-                                                                            'not-free-identifier=? #t))))
+                                  (renamer #'id #:alt #'cnt-id)
+                                  (renamer #'cnt-id)))
                             (#%provide (rename export-id out-id)))))]
                    [else 
-                    (with-syntax ([(export-id) (generate-temporaries #'(id))])
-                      #`(begin                             
+                    (with-syntax ([(export-id error-id) (generate-temporaries #'(id id))])
+                      #`(begin        
+                          (define-syntax error-id
+                            (lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id))))
                           (define-syntax export-id
                             (if (unbox typed-context?)
-                                (make-rename-transformer (syntax-property #'id 
-                                                                          'not-free-identifier=? #t))
-                                (lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id)))))
+                                (renamer #'id #:alt #'error-id)
+                                (renamer #'error-id)))
                           (provide (rename-out [export-id out-id]))))])))]
         [(mem? internal-id stx-defs) 
          =>
          (lambda (b)
            (with-syntax ([id internal-id]
                          [out-id external-id])
-             (with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))])
-               #`(begin                    
+             (with-syntax ([(export-id error-id) (generate-temporaries #'(id id))])
+               #`(begin  
+                   (define-syntax error-id
+                     (lambda (stx)
+                       (tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id))))
                    (define-syntax export-id
                      (if (unbox typed-context?)
-                         (begin
+                         (begin                           
                            (add-alias #'export-id #'id)
-                           (make-rename-transformer (syntax-property #'id 
-                                                                     'not-free-identifier=? #t)))
-                         (lambda (stx)
-                           (tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id)))))
+                           (renamer #'id #:alt #'error-id))
+                         (renamer #'error-id)))
                    (provide (rename-out [export-id out-id]))))))]
         [(eq? (syntax-e internal-id) (syntax-e external-id))
          #`(provide #,internal-id)]
diff --git a/collects/typed-scheme/typecheck/tc-app-unit.ss b/collects/typed-scheme/typecheck/tc-app-unit.ss
index 61b4f54b..63db7660 100644
--- a/collects/typed-scheme/typecheck/tc-app-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-app-unit.ss
@@ -576,7 +576,7 @@
       [c:lv-clause
        #:with (#%plain-app reverse n:id) #'c.e
        #:with (v) #'(c.v ...) 
-       #:when (free-identifier=? name #'v)
+       #:when (free-identifier=? name #'n)
        (type-annotation #'v)]
       [_ #f]))
   (syntax-parse stx
@@ -757,8 +757,8 @@
      (match (tc-expr #'fn)
        [(tc-result: (Function: arities)) 
         (tc-keywords form arities (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected)]
-       [t (tc-error/expr #:return (ret (Un))
-                         "Cannot apply expression of type ~a, since it is not a function type" t)])]
+       [(tc-result: t) (tc-error/expr #:return (ret (Un))
+                                      "Cannot apply expression of type ~a, since it is not a function type" t)])]
     ;; even more special case for match
     [(#%plain-app (letrec-values ([(lp) (#%plain-lambda args . body)]) lp*) . actuals)
      (and expected (not (andmap type-annotation (syntax->list #'args))) (free-identifier=? #'lp #'lp*))
diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss
index 328e373b..9640ef5a 100644
--- a/collects/typed-scheme/typecheck/tc-expr-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss
@@ -136,7 +136,7 @@
      (ret expected)]
     [((? Type? t1) (? Type? t2))
      (unless (subtype t1 t2)
-       (tc-error/expr"Expected ~a, but got ~a" t2 t1))
+       (tc-error/expr "Expected ~a, but got ~a" t2 t1))
      expected]))
 
 (define (tc-expr/check form expected)
diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss
index 4c6b019b..395a82bd 100644
--- a/collects/typed-scheme/typecheck/tc-structs.ss
+++ b/collects/typed-scheme/typecheck/tc-structs.ss
@@ -86,6 +86,7 @@
 (define (mk/register-sty nm flds parent parent-field-types types 
                          #:wrapper [wrapper values] 
                          #:type-wrapper [type-wrapper values]
+                         #:pred-wrapper [pred-wrapper values]
                          #:mutable [setters? #f]
                          #:proc-ty [proc-ty #f]
                          #:maker [maker* #f]
@@ -104,6 +105,7 @@
         (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters? 
                                #:wrapper wrapper
                                #:type-wrapper type-wrapper
+                               #:pred-wrapper pred-wrapper
                                #:maker (or maker* maker)
                                #:constructor-return cret))))
 
@@ -113,6 +115,7 @@
 (define (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
                                #:wrapper [wrapper values]
                                #:type-wrapper [type-wrapper values]
+                               #:pred-wrapper [pred-wrapper values]
                                #:maker [maker* #f]
                                #:constructor-return [cret #f])
   ;; create the approriate names that define-struct will bind
@@ -125,7 +128,7 @@
      (list (cons (or maker* maker) 
                  (wrapper (->* external-fld-types (if cret cret name))))
            (cons pred
-                 (make-pred-ty (wrapper name))))
+                 (make-pred-ty (pred-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)))) setters external-fld-types/no-parent)
@@ -167,6 +170,7 @@
                    ;; wrap everything in the approriate forall
                    #:wrapper (lambda (t) (make-Poly tvars t))
                    #:type-wrapper (lambda (t) (make-App t new-tvars #f))
+                   #:pred-wrapper (lambda (t) (subst-all (for/list ([t tvars]) (list t Univ)) t))
                    #:poly? #t))
 
 
diff --git a/collects/typed-scheme/typecheck/tc-toplevel.ss b/collects/typed-scheme/typecheck/tc-toplevel.ss
index fce1a1a3..e881e3e4 100644
--- a/collects/typed-scheme/typecheck/tc-toplevel.ss
+++ b/collects/typed-scheme/typecheck/tc-toplevel.ss
@@ -10,7 +10,7 @@
          (rep type-rep)
          (types utils convenience)
          (private parse-type type-annotation type-contract)
-	 (env type-env init-envs type-name-env type-alias-env)
+	 (env type-env init-envs type-name-env type-alias-env lexical-env)
 	 (utils tc-utils mutated-vars)
 	 "provide-handling.ss"
          "def-binding.ss"
@@ -39,6 +39,17 @@
       ;; type aliases have already been handled by an earlier pass
       [(define-values () (begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values)))
        (list)]
+
+      ;; declare-refinement
+      [(define-values () (begin (quote-syntax (declare-refinement-internal pred)) (#%plain-app values)))
+       (match (lookup-type/lexical #'pred)
+              [(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
+               (register-type #'pred 
+                              (make-pred-ty (list dom)
+                                            rng
+                                            (make-Refinement dom #'pred (syntax-local-certifier))))
+               (list)]
+              [t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
       
       ;; require/typed
       [(define-values () (begin (quote-syntax (require/typed-internal nm ty)) (#%plain-app values)))
diff --git a/collects/typed-scheme/typecheck/typechecker.ss b/collects/typed-scheme/typecheck/typechecker.ss
index 2f41a66a..bfa104fe 100644
--- a/collects/typed-scheme/typecheck/typechecker.ss
+++ b/collects/typed-scheme/typecheck/typechecker.ss
@@ -3,8 +3,10 @@
 (require "../utils/utils.ss")
 (require (utils unit-utils)
          mzlib/trace
-         (only-in scheme/unit provide-signature-elements)
-         "signatures.ss" "tc-toplevel.ss"         
+         (only-in scheme/unit
+                  provide-signature-elements
+                  define-values/invoke-unit/infer link)
+         "signatures.ss" "tc-toplevel.ss"
          "tc-new-if.ss" "tc-lambda-unit.ss" "tc-new-app-unit.ss"
          "tc-let-unit.ss" "tc-dots-unit.ss"
          "tc-expr-unit.ss" "check-subforms-unit.ss")
diff --git a/collects/typed/file/tar.ss b/collects/typed/file/tar.ss
new file mode 100644
index 00000000..625a45a8
--- /dev/null
+++ b/collects/typed/file/tar.ss
@@ -0,0 +1,22 @@
+#lang typed-scheme
+;; typed-scheme wrapper on file/tar
+;; yc 2009/2/25
+
+;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; basic type aliases.
+(define-type-alias Path-String (U Path String))
+
+(require/typed file/tar
+               ;; tar appears to return exact-nonenegative-integer? instead of void?
+               [tar (Path-String Path-String * -> Integer)]
+               ;; tar->output appears to take (listof path) instead of (listof path-string?)
+               ;; it also appears to return exact-nonenegative-integer?
+               [tar->output (case-lambda ((Listof Path) -> Integer)
+                                         ((Listof Path) Output-Port -> Integer))]
+               ;; tar->gzip
+               ;; missing from file/tar but available in mzlib/tar
+               ;; actually returns void?
+               [tar-gzip (Path-String Path-String * -> Void)]
+               )
+
+(provide tar tar->output tar-gzip)
\ No newline at end of file
diff --git a/collects/typed/srfi/14.ss b/collects/typed/srfi/14.ss
index 48670078..4c656e91 100644
--- a/collects/typed/srfi/14.ss
+++ b/collects/typed/srfi/14.ss
@@ -91,23 +91,28 @@
  [char-set:ascii Char-Set]
  [char-set:empty Char-Set]
  [char-set:full Char-Set]
+ [char-set-fold (All (A) ((Char A -> A) A Char-Set -> A))]
+ [char-set-unfold
+  (All (A)
+       (case-lambda
+        ((A -> Any) (A -> Char) (A -> A) A -> Char-Set)
+        ((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set)))]
+ [char-set-unfold! 
+  (All (A) ((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set))]
+ [char-set-for-each (All (A) ((Char -> A) Char-Set -> (U A Void)))]
+ [char-set-any (All (A) ((Char -> A) Char-Set -> (U A #f)))]
+ [char-set-every (All (A) ((Char -> A) Char-Set -> (U A Boolean)))]
  ) ; end of require/typed
 
 ;; Definitions provided here for polymorphism
-
-(: char-set-fold (All (A) ((Char A -> A) A Char-Set -> A)))
+#;
 (define (char-set-fold comb base cs)
   (let loop ((c (char-set-cursor cs)) (b base))
     (cond [(end-of-char-set? c) b]
           [else
            (loop (char-set-cursor-next cs c)
                  (comb (char-set-ref cs c) b))])))
-
-(: char-set-unfold
-   (All (A)
-        (case-lambda
-          ((A -> Any) (A -> Char) (A -> A) A -> Char-Set)
-          ((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set))))    
+#;
 (define char-set-unfold
   (pcase-lambda: (A) 
      [([p : (A -> Any)] [f : (A -> Char)] [g : (A -> A)] [seed : A])
@@ -115,29 +120,25 @@
      [([p : (A -> Any)] [f : (A -> Char)] [g : (A -> A)] [seed : A] 
                         [base-cs : Char-Set])
       (char-set-unfold! p f g seed (char-set-copy base-cs))]))
-
-(: char-set-unfold! 
-   (All (A) ((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set)))
+#;
 (define (char-set-unfold! p f g seed base-cs)
   (let lp ((seed seed) (cs base-cs))
         (if (p seed) cs                                 ; P says we are done.
             (lp (g seed)                                ; Loop on (G SEED).
                 (char-set-adjoin! cs (f seed))))))
 
-(: char-set-for-each (All (A) ((Char -> A) Char-Set -> (U A Void))))
+#;
 (define (char-set-for-each f cs)
   (char-set-fold (lambda: ([c : Char] [b : (U A Void)]) (f c)) 
                  (void) 
                  cs))
-
-(: char-set-any (All (A) ((Char -> A) Char-Set -> (U A #f))))
+#;
 (define (char-set-any pred cs)
   (let loop ((c (char-set-cursor cs)))
     (and (not (end-of-char-set? c))
          (or (pred (char-set-ref cs c))
              (loop (char-set-cursor-next cs c))))))
-
-(: char-set-every (All (A) ((Char -> A) Char-Set -> (U A Boolean))))
+#;
 (define (char-set-every pred cs)
   (let loop ((c (char-set-cursor cs)) (b (ann #t (U #t A))))
     (cond [(end-of-char-set? c) b]