diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index 6f258618..7501a64c 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -718,7 +718,7 @@
                 (-poly (a) (a . -> . a))]
         [tc-e (apply values (list 1 2 3)) #:ret (ret (list -Integer -Integer -Integer))]
         
-        [tc-e (ann (if #t 3 "foo") Integer) -Integer]
+        [tc-e/t (ann (if #t 3 "foo") Integer) -Integer]
         
         [tc-e/t (plambda: (a ...) ([x : Number] . [y : a ... a])
                           (andmap null? (map list y)))
@@ -730,7 +730,7 @@
         #;[tc-err (let: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))])
                         (fact 20))]
         
-        #;[tc-err ]
+        [tc-err (ann (lambda: ([x : Any]) #f) (Any -> Boolean : String))]
         )
   (test-suite
    "check-type tests"
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index ad172a1d..c54e302f 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -576,8 +576,10 @@
   (syntax-parse stx
     [(values t ...)
      #:when (eq? 'values (syntax-e #'values))
-     (ret (map parse-type (syntax->list #'(t ...))))]
-    [t (ret (parse-type #'t))]))
+     (ret (map parse-type (syntax->list #'(t ...))) 
+          (map (lambda (x) (make-NoFilter)) (syntax->list #'(t ...)))
+          (map (lambda (x) (make-NoObject)) (syntax->list #'(t ...))))]
+    [t (ret (parse-type #'t) (make-NoFilter) (make-NoObject))]))
 
 (define parse-tc-results/id (parse/id parse-tc-results))
 
diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index 097d6d68..04524bd0 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -63,9 +63,25 @@ This file defines two sorts of primitives. All of them are provided into any mod
     (pattern (orig-nm:id internal-nm:id)
 	     #:with spec #'(orig-nm internal-nm)
 	     #:with nm #'internal-nm))
+  (define-syntax-class simple-clause
+    #:attributes (nm ty)
+    (pattern [nm:opt-rename ty]))
+  (define-syntax-class struct-clause
+    #:literals (struct)
+    #:attributes (nm (body 1))
+    (pattern [struct nm:opt-rename (body ...)]))
+  (define-syntax-class opaque-clause
+    #:literals (opaque)
+    #:attributes (ty pred opt)
+    (pattern [opaque ty:id pred:id]
+             #:with opt #'())
+    (pattern [opaque ty:id pred:id #:name-exists]
+             #:with opt #'(#:name-exists)))
   (syntax-parse stx
-    [(_ lib [nm:opt-rename ty] ...)
-     #'(begin (require/typed nm ty lib) ...)]
+    [(_ lib (~or [sc:simple-clause] [strc:struct-clause] [oc:opaque-clause]) ...)
+     #'(begin (require/typed sc.nm sc.ty lib) ... 
+              (require-typed-struct strc.nm (strc.body ...) lib) ...
+              (require/opaque-type oc.ty oc.pred lib . oc.opt) ...)]
     [(_ nm:opt-rename ty lib (~or [#:struct-maker parent] #:opt) ...)
      (with-syntax ([cnt* (generate-temporary #'nm.nm)]
 		   [sm (if #'parent
diff --git a/collects/typed-scheme/rep/filter-rep.ss b/collects/typed-scheme/rep/filter-rep.ss
index 33d09553..3d32f2c0 100644
--- a/collects/typed-scheme/rep/filter-rep.ss
+++ b/collects/typed-scheme/rep/filter-rep.ss
@@ -48,6 +48,10 @@
                       ()
                       [result FilterSet?])])
 
+;; represents no info about the filters of this expression
+;; should only be used for parsing type annotations and expected types
+(df NoFilter () [#:fold-rhs #:base])
+
 (define index/c (or/c natural-number/c keyword?))
 
 (dlf LBot () [#:fold-rhs #:base])
diff --git a/collects/typed-scheme/rep/object-rep.ss b/collects/typed-scheme/rep/object-rep.ss
index afd87e32..9c7f93b5 100644
--- a/collects/typed-scheme/rep/object-rep.ss
+++ b/collects/typed-scheme/rep/object-rep.ss
@@ -15,6 +15,10 @@
   [#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))]
   [#:fold-rhs (*Path (map pathelem-rec-id p) v)])
 
+;; represents no info about the filters of this expression
+;; should only be used for parsing type annotations and expected types
+(do NoObject () [#:fold-rhs #:base])
+
 (dlo LEmpty () [#:fold-rhs #:base])
 
 (dlo LPath ([p (listof PathElem?)] [idx index/c])
diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/ts-reference.scrbl
index 32adc2d7..c5d03a0b 100644
--- a/collects/typed-scheme/ts-reference.scrbl
+++ b/collects/typed-scheme/ts-reference.scrbl
@@ -149,6 +149,18 @@ different arity.}
 @defform[(pcase-lambda: (a ...) [formals body] ...)]{
 A polymorphic function of multiple arities.}
 
+@subsection{Loops}
+
+@defform/subs[(do: : u ([id : t init-expr step-expr-maybe] ...)
+                       (stop?-expr finish-expr ...)
+                expr ...+)
+              ([step-expr-maybe code:blank
+                                step-expr])]{
+Like @scheme[do], but each @scheme[id] having the associated type @scheme[t], and 
+the final body @scheme[expr] having the type @scheme[u].
+}
+
+
 @subsection{Definitions}
 
 @defform*[[(define: v : t e)
@@ -212,48 +224,39 @@ contexts.}
 Here, @scheme[_m] is a module spec, @scheme[_pred] is an identifier
 naming a predicate, and @scheme[_r] is an optionally-renamed identifier.
 
-@defform*[[
-(require/typed r t m)
-(require/typed m [r t] ...)
-]]{The first form requires @scheme[r] from module @scheme[m], giving
-it type @scheme[t].  The second form generalizes this to multiple
-identifiers.
+@defform/subs[#:literals (struct opaque)
+(require/typed m rt-clause ...)
+([rt-clause [r t]
+	    [struct name ([f : t] ...)]
+	    [struct (name parent) ([f : t] ...)]
+	    [opaque t pred]])
+]{This form requires identifiers from the module @scheme[m], giving
+them the specified types.   
 
-In both cases, the identifiers are protected with @rtech{contracts} which
-enforce the type @scheme[t].  If this contract fails, the module
+The first form requires @scheme[r], giving it type @scheme[t].
+
+The second and third forms require the struct with name @scheme[name]
+with fields @scheme[f ...], where each field has type @scheme[t].  The
+third form allows a @scheme[parent] structure type to be specified.
+The parent type must already be a structure type known to Typed
+Scheme, either built-in or via @scheme[require/typed].  The
+structure predicate has the appropriate Typed Scheme filter type so
+that it may be used as a predicate in @scheme[if] expressions in Typed
+Scheme.
+
+The fourth case defines a new type @scheme[t].  @scheme[pred], imported from
+module @scheme[m], is a predicate for this type.  The type is defined
+as precisely those values to which @scheme[pred] produces
+@scheme[#t].  @scheme[pred] must have type @scheme[(Any -> Boolean)].
+
+In all cases, the identifiers are protected with @rtech{contracts} which
+enforce the specified types.  If this contract fails, the module
 @scheme[m] is blamed. 
 
 Some types, notably polymorphic types constructed with @scheme[All],
 cannot be converted to contracts and raise a static error when used in
 a @scheme[require/typed] form.}
 
-@defform[(require/opaque-type t pred m)]{
-This defines a new type @scheme[t].  @scheme[pred], imported from
-module @scheme[m], is a predicate for this type.  The type is defined
-as precisely those values to which @scheme[pred] produces
-@scheme[#t].  @scheme[pred] must have type @scheme[(Any -> Boolean)].}
-
-@defform*[[(require-typed-struct name ([f : t] ...) m)
-           (require-typed-struct (name parent) ([f : t] ...) m)]]{
-Requires all the functions associated with the structure @scheme[name] from the module @scheme[m],
-with the appropriate types.  The structure predicate has the
-appropriate Typed Scheme filter type so that it may be used as a
-predicate in @scheme[if] expressions in Typed Scheme.  
-
-In the second form, @scheme[parent] must already be a structure type
-known to Typed Scheme, either via @scheme[define-struct:] or
-@scheme[require-typed-struct].  
-}
-
-@defform/subs[(do: : u ([id : t init-expr step-expr-maybe] ...)
-                       (stop?-expr finish-expr ...)
-                expr ...+)
-              ([step-expr-maybe code:blank
-                                step-expr])]{
-Like @scheme[do], but each @scheme[id] having the associated type @scheme[t], and 
-the final body @scheme[expr] having the type @scheme[u].
-}
-
 @section{Libraries Provided With Typed Scheme}
 
 The @schememodname[typed-scheme] language corresponds to the
diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss
index 341f2ae4..f2c37f07 100644
--- a/collects/typed-scheme/typecheck/tc-app.ss
+++ b/collects/typed-scheme/typecheck/tc-app.ss
@@ -501,8 +501,7 @@
 ;; syntax tc-results? -> tc-results?
 (define (tc/app/check form expected)
     (define t (tc/app/internal form expected))
-    (check-below t expected)
-    expected)
+    (check-below t expected))
 
 (define (object-index os i)
   (unless (number? i)
@@ -638,4 +637,5 @@
     [((arr: _ _ _ drest '()) _)
      (int-err "funapp with drest args NYI")]
     [((arr: _ _ _ _ kws) _)
-     (int-err "funapp with keyword args NYI")]))
\ No newline at end of file
+     (int-err "funapp with keyword args NYI")]))
+
diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss
index 3fac7230..f4d867e1 100644
--- a/collects/typed-scheme/typecheck/tc-expr-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss
@@ -2,7 +2,7 @@
 
 
 (require (rename-in "../utils/utils.ss" [private private-in]))
-(require syntax/kerncase
+(require syntax/kerncase mzlib/trace
          scheme/match (prefix-in - scheme/contract)
          "signatures.ss"
          (types utils convenience union subtype)
@@ -133,18 +133,42 @@
 ;;                   (Type Type -> Type))
 (define (check-below tr1 expected)
   (match* (tr1 expected)
+    ;; these two have to be first so that errors can be allowed in cases where multiple values are expected
+    [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:)))
+     (ret ts2)]
     [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
      expected]
-    [((tc-results: t1) (tc-results: t2))
-     (unless (= (length t1) (length t2))
-       (tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1)))
-     (unless (for/and ([t t1] [s t2]) (subtype t s))
-       (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
+    
+    [((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:)))
+     (unless (= (length ts) (length ts2))
+       (tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts)))
+     (unless (for/and ([t ts] [s ts2]) (subtype t s))
+       (tc-error/expr "Expected ~a, but got ~a" (stringify ts2) (stringify ts)))
+     (if (= (length ts) (length ts2))
+         (ret ts2 fs os)
+         (ret ts2))]
+    [((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:)))
+     (cond 
+       [(not (subtype t1 t2))
+        (tc-error/expr "Expected ~a, but got ~a" t2 t1)])
+     expected]
+    [((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
+     (cond 
+       [(not (subtype t1 t2))
+        (tc-error/expr "Expected ~a, but got ~a" t2 t1)]
+       [(not (and (equal? f1 f2) (equal? o1 o2)))
+        (tc-error/expr "Expected result with filter ~a and object ~a, got filter ~a and object ~a" f2 o2 f1 o1)])
      expected]
     [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
      (unless (andmap subtype t1 t2)
        (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
      expected]
+    [((tc-results: t1 fs os) (tc-results: t2 fs os))
+     (unless (= (length t1) (length t2))
+       (tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1)))
+     (unless (for/and ([t t1] [s t2]) (subtype t s))
+       (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
+     expected]
     [((tc-result1: t1 f o) (? Type? t2))
      (unless (subtype t1 t2)
        (tc-error/expr "Expected ~a, but got ~a" t2 t1))
diff --git a/collects/typed-scheme/typecheck/tc-if.ss b/collects/typed-scheme/typecheck/tc-if.ss
index 6ebe28c2..b4658981 100644
--- a/collects/typed-scheme/typecheck/tc-if.ss
+++ b/collects/typed-scheme/typecheck/tc-if.ss
@@ -18,6 +18,11 @@
 (import tc-expr^)
 (export tc-if^)
 
+(define (erase-filter tc)
+  (match tc
+    [(tc-results: ts _ _)
+     (ret ts (for/list ([f ts]) (make-NoFilter)) (for/list ([f ts]) (make-NoObject)))]))
+
 (define (tc/if-twoarm tst thn els [expected #f])
   (define (tc expr reachable?)
     (unless reachable? (warn-unreachable expr))
@@ -25,7 +30,7 @@
       ;; if reachable? is #f, then we don't want to verify that this branch has the appropriate type
       ;; in particular, it might be (void)
       [(and expected reachable?)
-       (tc-expr/check expr expected)]
+       (tc-expr/check expr (erase-filter expected))]
       ;; this code is reachable, but we have no expected type
       [reachable? (tc-expr expr)]
       ;; otherwise, this code is unreachable
@@ -41,11 +46,15 @@
                    [(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs- flag-) (tc els (unbox flag-)))])
          ;; if we have the same number of values in both cases
          (cond [(= (length ts) (length us))
-                (combine-results
-                 (for/list ([t ts] [u us] [o2 os2] [o3 os3] [f2 fs2] [f3 fs3])
-                   (combine-filter f1 f2 f3 t u o2 o3)))]
+                (let ([r
+                       (combine-results
+                        (for/list ([t ts] [u us] [o2 os2] [o3 os3] [f2 fs2] [f3 fs3])
+                          (combine-filter f1 f2 f3 t u o2 o3)))])
+                  (if expected
+                      (check-below r expected)
+                      r))]
                [else
-                (tc-error/expr #:return (ret Err)
+                (tc-error/expr #:return (ret (or expected Err))
                                "Expected the same number of values from both branches of if expression, but got ~a and ~a"
                                (length ts) (length us))])))]
     [(tc-results: t _ _)
diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss
index ced31998..f2588981 100644
--- a/collects/typed-scheme/types/printer.ss
+++ b/collects/typed-scheme/types/printer.ss
@@ -45,6 +45,7 @@
                           (for ([i thn]) (fp "~a " i)) (fp "|")
                           (for ([i els]) (fp " ~a" i))
                           (fp")")]
+    [(NoFilter:) (fp "-")]
     [(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path (syntax-e id))]
     [(TypeFilter: type path id) (fp "(~a @ ~a ~a)" type path (syntax-e id))]
     [(Bot:) (fp "Bot")]))
@@ -65,6 +66,7 @@
 (define (print-object c port write?)
   (define (fp . args) (apply fprintf port args))
   (match c
+    [(NoObject:) (fp "-")]
     [(Empty:) (fp "")]
     [(Path: pes i) (fp "~a" (append pes (list (syntax-e i))))]))
 
diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss
index 6f4504c3..225b8a95 100644
--- a/collects/typed-scheme/types/utils.ss
+++ b/collects/typed-scheme/types/utils.ss
@@ -240,7 +240,7 @@
  [ret    
   (->d ([t (or/c Type/c (listof Type/c))])
        ([f (if (list? t)
-               (listof FilterSet?)
+               (listof (or/c FilterSet? NoFilter?))
                FilterSet?)]
         [o (if (list? t)
                (listof Object?)