diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss
index 20bbf1f274..e0fdae3a08 100644
--- a/collects/typed-scheme/infer/infer-unit.ss
+++ b/collects/typed-scheme/infer/infer-unit.ss
@@ -454,11 +454,11 @@
     (let ([cs (cgen/list null X S T)])
       (if (not expected)
           (subst-gen cs R must-vars)
-          (cset-meet cs (cgen null X R expected))))))
+          (subst-gen (cset-meet cs (cgen null X R expected)) R must-vars)))))
 
 ;; like infer, but T-var is the vararg type:
 (define (infer/vararg X S T T-var R must-vars [expected #f])
-  (define new-T (extend S T T-var))
+  (define new-T (if T-var (extend S T T-var) T))
   (and ((length S) . >= . (length T))
        (infer X S new-T R must-vars expected)))
 
diff --git a/collects/typed-scheme/infer/signatures.ss b/collects/typed-scheme/infer/signatures.ss
index a3b85665f3..b9b9be1286 100644
--- a/collects/typed-scheme/infer/signatures.ss
+++ b/collects/typed-scheme/infer/signatures.ss
@@ -33,7 +33,8 @@
    [cnt infer/vararg (((listof symbol?) 
                        (listof Type?)
                        (listof Type?)
-                       Type? Type?
+                       (or/c #f Type?)
+                       Type?
                        (listof symbol?))
                       ((or/c #f Type?)) . ->* . any)]
    [cnt infer/dots (((listof symbol?) 
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 7e8b742bf2..398fd0e782 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -14,7 +14,23 @@
 
 [raise (Univ . -> . (Un))]
 
-[car   (-poly (a b) (cl-> [((-pair a b)) a] [((-lst a)) a]))]
+[car   (-poly (a b) 
+              (cl->*
+               (->acc (list (-pair a b)) a (list -car))
+               (->* (list (-lst a)) a)))]
+[cdr   (-poly (a b) 
+              (cl->*
+               (->acc (list (-pair a b)) b (list -cdr))
+               (->* (list (-lst a)) (-lst a))))]
+
+[cadr (-poly (a b c)
+             (cl-> [((-pair a (-pair b c))) b]
+                   [((-lst a)) a]))]
+[caddr  (-poly (a) (-> (-lst a) a))]
+[cadddr (-poly (a) (-> (-lst a) a))]
+[cddr  (-poly (a) (-> (-lst a) (-lst a)))]
+[cdddr (-poly (a) (-> (-lst a) (-lst a)))]
+
 [first (-poly (a b) (cl-> [((-pair a b)) a] [((-lst a)) a]))]
 [second (-poly (a b c)
                (cl-> [((-pair a (-pair b c))) b]
@@ -26,14 +42,7 @@
 [fifth  (-poly (a) ((-lst a) . -> .  a))]
 [sixth  (-poly (a) ((-lst a) . -> .  a))]
 [rest (-poly (a) ((-lst a) . -> .  (-lst a)))]
-[cadr (-poly (a b c)
-             (cl-> [((-pair a (-pair b c))) b]
-                   [((-lst a)) a]))]
-[caddr  (-poly (a) (-> (-lst a) a))]
-[cadddr (-poly (a) (-> (-lst a) a))]
-[cdr   (-poly (a b) (cl-> [((-pair a b)) b] [((-lst a)) (-lst a)]))]
-[cddr  (-poly (a) (-> (-lst a) (-lst a)))]
-[cdddr (-poly (a) (-> (-lst a) (-lst a)))]
+
 [cons (-poly (a b)
              (cl-> [(a (-lst a)) (-lst a)]
                    [(a b) (-pair a b)]))]
diff --git a/collects/typed-scheme/test2.ss b/collects/typed-scheme/test2.ss
index a4305927fb..860a39efa0 100644
--- a/collects/typed-scheme/test2.ss
+++ b/collects/typed-scheme/test2.ss
@@ -19,11 +19,12 @@
 (+)
 (+ 1 2 3)
 (+ 1 2 3.5)
-#|
-(define-struct: (Z) x ([y : Z]))
-(define:  my-x : (x Number) (make-x 1))
-(number? (x-y my-x))
-(if (number? (x-y my-x)) (+ 1 (x-y my-x)) 7)
+
+(define-struct: (Z) X ([y : Z]))
+(define:  my-x : (X Number) (make-X 1))
+#| ; FIXME - doesn't work yet
+(number? (X-y my-x))
+(if (number? (X-y my-x)) (+ 1 (X-y my-x)) 7)
 |#
 
 (define: (f2) : (U) (error 'foo))
@@ -32,5 +33,15 @@
 (: f3 (U (Number -> Number) (Number -> String)))
 (define (f3 x) 7)
 
+(define: x : (List Any Any) (list 1 23 ))
+(car x)
+(if (number? (car x)) (add1 (car #{x :: (Pair Number Any)})) 7)
+(if (number? (car x)) (add1 (car x)) 7)
+
+;; error
 ;(f 12 "hi")
 
+(map + (list 1 2 3))
+(map + (list 1 2 3) (list 1 2 3))
+;; error
+;(map + (list 1 2 3) (list 1 2 "foo"))
\ No newline at end of file
diff --git a/collects/typed-scheme/typecheck/tc-app-helper.ss b/collects/typed-scheme/typecheck/tc-app-helper.ss
index f5f268e9cc..4ea2ff3071 100644
--- a/collects/typed-scheme/typecheck/tc-app-helper.ss
+++ b/collects/typed-scheme/typecheck/tc-app-helper.ss
@@ -1,7 +1,7 @@
 #lang scheme/base
 
-(require "../utils/utils.ss"
-         (utils tc-utils))
+(require "../utils/utils.ss" scheme/match
+         (utils tc-utils) (rep type-rep) (types utils union))
 
 (provide (all-defined-out))
 
@@ -39,3 +39,25 @@
              (if expected
                  (format "Expected result: ~a~n" expected)
                  ""))]))
+
+(define (poly-fail t argtypes #:name [name #f] #:expected [expected #f])
+  (match t
+    [(or (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '()) ...)))
+         (PolyDots-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '()) ...))))
+     (let ([fcn-string (if name
+                           (format "function ~a" (syntax->datum name))
+                           "function")])
+       (if (and (andmap null? msg-doms)
+                (null? argtypes))
+           (tc-error/expr #:return (ret (Un))
+                          (string-append 
+                           "Could not infer types for applying polymorphic "
+                           fcn-string
+                           "\n"))
+           (tc-error/expr #:return (ret (Un))
+                          (string-append
+                           "Polymorphic " fcn-string " could not be applied to arguments:~n"
+                           (domain-mismatches t msg-doms msg-rests msg-drests msg-rngs argtypes #f #f #:expected expected)
+                           (if (not (for/and ([t (apply append (map fv/list msg-doms))]) (memq t msg-vars)))
+                               (string-append "Type Variables: " (stringify msg-vars) "\n")
+                               "")))))]))
\ No newline at end of file
diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss
index 43b4ba8d0b..16e7d2d618 100644
--- a/collects/typed-scheme/typecheck/tc-app.ss
+++ b/collects/typed-scheme/typecheck/tc-app.ss
@@ -4,10 +4,11 @@
          "signatures.ss" "tc-metafunctions.ss"
          "tc-app-helper.ss"
          stxclass scheme/match mzlib/trace
-         (for-syntax stxclass)
+         (for-syntax stxclass scheme/base)
          (types utils abbrev union subtype resolve)
          (utils tc-utils)
          (rep type-rep filter-rep object-rep)
+         (r:infer infer)
          (for-template 
           (only-in '#%kernel [apply k:apply])
           "internal-forms.ss" scheme/base 
@@ -89,6 +90,19 @@
 (define (in-indexes dom)
   (in-range (length dom)))
 
+
+(define-syntax (handle-clauses stx)
+  (syntax-parse stx
+    [(_  (lsts ... arrs) f-stx args-stx pred infer t argtys expected)
+     (with-syntax ([(vars ... a) (generate-temporaries #'(lsts ... arrs))])
+       (syntax/loc stx
+         (or (for/or ([vars lsts] ... [a arrs]
+                      #:when (pred vars ... a))
+               (let ([substitution (infer vars ... a)])
+                 (and substitution
+                      (tc/funapp1 f-stx args-stx (subst-all substitution a) argtys expected #:check #f))))
+             (poly-fail t argtys #:name (and (identifier? f-stx) f-stx) #:expected expected))))]))
+
 (define (tc/funapp f-stx args-stx ftype0 argtys expected)
   (match* (ftype0 argtys)
     ;; we special-case this (no case-lambda) for improved error messages
@@ -109,6 +123,34 @@
        #:return (or expected (ret (Un)))
        (string-append "No function domains matched in function application:\n"
                       (domain-mismatches t doms rests drests rngs argtys-t #f #f))))]
+    ;; polymorphic functions without dotted rest
+    [((tc-result1: (and t
+                      (or (Poly: vars 
+                                 (Function: (list (and arrs (arr: doms rngs rests (and drests #f) '())) ...)))
+                          (PolyDots: vars
+                                     (Function: (list (and arrs (arr: doms rngs rests (and drests #f) '())) ...))))))
+      (list (tc-result1: argtys-t) ...))
+     (handle-clauses (doms rngs rests arrs) f-stx args-stx
+                     ;; only try inference if the argument lengths are appropriate
+                     (lambda (dom _ rest a) ((if rest <= =) (length dom) (length argtys)))
+                     ;; only try to infer the free vars of the rng (which includes the vars in filters/objects)
+                     ;; note that we have to use argtys-t here, since argtys is a list of tc-results
+                     (lambda (dom rng rest a) (infer/vararg vars argtys-t dom rest rng (fv rng) (and expected (tc-results->values expected))))
+                     t argtys expected)]
+    ;; polymorphic ... type
+    [((tc-result1: (and t (PolyDots: 
+                         (and vars (list fixed-vars ... dotted-var))
+                         (Function: (list (and arrs (arr: doms rngs (and #f rests) (cons dtys dbounds) '())) ...)))))
+      (list (tc-result1: argtys-t) ...))
+     (handle-clauses (doms dtys dbounds rngs arrs) f-stx args-stx
+                     (lambda (dom dty dbound rng arr) (and (<= (length dom) (length argtys))
+                                                           (eq? dotted-var dbound)))
+                     (lambda (dom dty dbound rng arr) 
+                       (infer/dots fixed-vars dotted-var argtys-t dom dty rng (fv rng) #:expected (and expected (tc-results->values expected))))
+                     t argtys expected)]
+    ;; procedural structs
+    [(tc-result1: (and sty (Struct: _ _ _ (? Type? proc-ty) _ _ _)))
+     (tc/funapp f-stx (cons (syntax/loc f-stx dummy) args-stx) (ret proc-ty) (cons sty argtys) expected)]
     ;; parameters are functions too
     [((tc-result1: (Param: in out)) (list)) (ret out)]
     [((tc-result1: (Param: in out)) (list (tc-result1: t)))
@@ -167,5 +209,7 @@
                         [_ (make-Empty)])]
                      [_ (make-Empty)]))])
        (ret t-r f-r o-r))]
-    [(_ _)
+    [((arr: _ _ _ drest '()) _)
+     (int-err "funapp with drest args NYI")]
+    [((arr: _ _ _ _ kws) _)
      (int-err "funapp with keyword args NYI")]))
\ No newline at end of file
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index 1a7ca3b9e9..cea9cb4499 100644
--- a/collects/typed-scheme/typecheck/tc-metafunctions.ss
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -11,7 +11,7 @@
          (for-syntax scheme/base))
 
 (provide combine-filter apply-filter abstract-filter abstract-filters
-         split-lfilters merge-filter-sets values->tc-results)
+         split-lfilters merge-filter-sets values->tc-results tc-results->values)
 
 ;; this implements the sequence invariant described on the first page relating to Bot
 (define (lcombine l1 l2)
@@ -172,4 +172,8 @@
                (match lo
                  [(LEmpty:) #f]
                  [(LPath: p (== i)) (make-Path p x)]))
-             (make-Empty))))]))
\ No newline at end of file
+             (make-Empty))))]))
+
+(define (tc-results->values tc)
+  (match tc
+    [(tc-results: ts) (-values ts)]))
\ No newline at end of file
diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss
index 49d1ea97cf..36770a4321 100644
--- a/collects/typed-scheme/typed-scheme.ss
+++ b/collects/typed-scheme/typed-scheme.ss
@@ -119,11 +119,11 @@
           ;; typecheck the body, and produce syntax-time code that registers types
           [let ([type (tc-toplevel-form body2)])])
          (define-syntax-class invis-kw
-           #:literals (define-values define-syntaxes require provide begin)
+           #:literals (define-values define-syntaxes #%require #%provide begin)
            (pattern define-values)
            (pattern define-syntaxes)
-           (pattern require)
-           (pattern provide)
+           (pattern #%require)
+           (pattern #%provide)
            (pattern begin))
        (syntax-parse body2
          [(head:invis-kw . _) 
diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss
index 7ec654ed5e..1b5e2f930d 100644
--- a/collects/typed-scheme/types/abbrev.ss
+++ b/collects/typed-scheme/types/abbrev.ss
@@ -125,6 +125,9 @@
 (define -no-lobj (make-LEmpty))
 (define -no-obj (make-Empty))
 
+(define -car (make-CarPE))
+(define -cdr (make-CdrPE))
+
 ;; convenient syntax
 
 (define-syntax -v 
@@ -177,8 +180,12 @@
      (make-Function (list (make-arr* dom rng #:rest rst)))]
     [(_ dom rng : filters)
      (make-Function (list (make-arr* dom rng #:filters filters)))]
+    [(_ dom rng : filters : object)
+     (make-Function (list (make-arr* dom rng #:filters filters #:object object)))]
     [(_ dom rst rng : filters)
-     (make-Function (list (make-arr* dom rng #:rest rst #:filters filters)))]))
+     (make-Function (list (make-arr* dom rng #:rest rst #:filters filters)))]
+    [(_ dom rst rng : filters : object)
+     (make-Function (list (make-arr* dom rng #:rest rst #:filters filters #:object object)))]))
 
 (define-syntax (-> stx)
   (syntax-parse stx
@@ -201,6 +208,12 @@
     [(_ dom (dty dbound) rng : filters)
      (make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:filters filters)))]))
 
+(define (->acc dom rng path)
+  (make-Function (list (make-arr* dom rng 
+                                  #:filters (-LFS (list (-not-filter (-val #f) path)) 
+                                                  (list (-filter (-val #f) path)))
+                                  #:object (make-LPath path 0)))))
+
 (define (cl->* . args)
   (define (funty-arities f)
     (match f
diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss
index da45eab2f5..35e36327b5 100644
--- a/collects/typed-scheme/types/utils.ss
+++ b/collects/typed-scheme/types/utils.ss
@@ -187,7 +187,11 @@
    [(_ tp fp op) #'(struct tc-results ((list (struct tc-result (tp fp op))) #f))]
    [(_ tp) #'(struct tc-results ((list (struct tc-result (tp _ _))) #f))]))
 
-(provide tc-result: tc-results: tc-result1: tc-result? tc-results?)
+(define (tc-results-t tc)
+  (match tc
+    [(tc-results: t) t]))
+
+(provide tc-result: tc-results: tc-result1: tc-result? tc-results? tc-results-t)
 
 ;; convenience function for returning the result of typechecking an expression
 (define ret