diff --git a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
index f6cde47a..79281c32 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
@@ -238,11 +238,9 @@
       [(null? (syntax-e s)) (formals (reverse acc) #f stx)]
       [else (formals (reverse acc) s stx)])))
 
+;; Currently no support for objects representing the rest argument
 (define (formals->objects formals)
-  (for/list ([i (in-list (append (formals-positional formals)
-                                 (if (formals-rest formals)
-                                     (list (formals-rest formals))
-                                     empty)))])
+  (for/list ([i (in-list (formals-positional formals))])
     (make-Path null i)))
 
 
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
index 3ad139b9..6e6c44da 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
@@ -13,16 +13,18 @@
          merge-tc-results
          tc-results->values)
 
-
+;; Objects representing the rest argument are currently not supported
 (define/cond-contract (abstract-results results arg-names #:rest-id [rest-id #f])
   ((tc-results/c (listof identifier?)) (#:rest-id (or/c #f identifier?))
    . ->* . SomeValues/c)
-  (define arg-names* (append arg-names (if rest-id (list rest-id) null)))
-  (tc-results->values
-    (replace-names
-      (for/list ([(nm k) (in-indexed (in-list arg-names*))])
-        (list nm (make-Path null (list 0 k))))
-      results)))
+  (define positional-arg-objects
+    (for/list ([(nm k) (in-indexed (in-list arg-names))])
+      (list nm (make-Path null (list 0 k)))))
+  (define arg-objects
+    (if rest-id
+        (cons (list rest-id -empty-obj) positional-arg-objects)
+        positional-arg-objects))
+  (tc-results->values (replace-names arg-objects results)))
 
 (define (tc-results->values tc)
   (match (fix-results tc)
diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt
index fd353046..03120851 100644
--- a/typed-racket-test/unit-tests/typecheck-tests.rkt
+++ b/typed-racket-test/unit-tests/typecheck-tests.rkt
@@ -1104,9 +1104,9 @@
                         (apply (plambda: (b ...) ([x : Number] . [y : Number ... b]) x)
                                1 w))
               (-polydots (a) ((list -String) (-Number a) . ->... . -Number))]
-        [tc-e/t (let ([f (plambda: (a ...) [w : a ... a] w)])
-                  (f 1 "hello" #\c))
-                (-lst* -One -String -Char)]
+        [tc-e (let ([f (plambda: (a ...) [w : a ... a] w)])
+                (f 1 "hello" #\c))
+              (-lst* -One -String -Char)]
         ;; instantiating non-dotted terms
         [tc-e/t (inst (plambda: (a) ([x : a]) x) Integer)
                 (make-Function (list (make-arr* (list -Integer) -Integer
@@ -2615,7 +2615,7 @@
        [tc-e ((inst (tr:lambda #:∀ (A) (x [y : A]) y) String) 'a "foo")
              #:ret (ret -String -true-filter)]
        [tc-e ((inst (tr:lambda #:forall (A ...) (x . [rst : A ... A]) rst) String) 'a "foo")
-             #:ret (ret (-lst* -String) -true-filter)]
+             (-lst* -String)]
        #| FIXME: does not work yet, TR thinks the type variable is unbound
        [tc-e (inst (tr:lambda #:forall (A) (x [y : A] [z : String "z"]) y) String)
              #:ret (ret (->opt Univ -String [-String] -String) -true-filter)]
@@ -2634,7 +2634,7 @@
              -String]
        [tc-e (let () (tr:define #:forall (A ...) (f x . [rst : A ... A]) rst)
                      (f 'a "b" "c"))
-             #:ret (ret (-lst* -String -String) -true-filter)]
+             (-lst* -String -String)]
 
        ;; test new :-less forms that allow fewer annotations
        [tc-e/t (let ([x "foo"]) x) -String]
@@ -3605,6 +3605,16 @@
        [tc-e/t
          (lambda: ([x : Flonum]) (if (= x (ann 1.0 Positive-Flonum)) x 'other))
          (t:-> -Flonum (t:Un -PosFlonum (-val 'other)) : -true-filter)]
+
+       [tc-e/t (lambda: ([x : One])
+                 (let ([f (lambda: [w : Any *] w)])
+                   (f x "hello" #\c)))
+        (t:-> -One (-lst Univ) : -true-filter)]
+
+       [tc-e/t (lambda: ([x : One])
+                 (let ([f (plambda: (a ...) [w : a ... a] w)])
+                   (f x "hello" #\c)))
+        (t:-> -One (-lst* -One -String -Char))]
        )
 
   (test-suite