diff --git a/collects/tests/typed-scheme/fail/bad-first.ss b/collects/tests/typed-scheme/fail/bad-first.ss
new file mode 100644
index 0000000000..eb0fd623d3
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/bad-first.ss
@@ -0,0 +1,3 @@
+#lang typed-scheme
+(require scheme/list)
+(first (cons 1 2))
diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss
index f551137d01..b123827eee 100644
--- a/collects/typed-scheme/private/base-env-numeric.ss
+++ b/collects/typed-scheme/private/base-env-numeric.ss
@@ -105,8 +105,8 @@
 [imag-part (N . -> . -Real)]
 [magnitude (N . -> . -Real)]
 [angle     (N . -> . -Real)]
-[numerator   (-Real . -> . -Integer)]
-[denominator (-Real . -> . -Integer)]
+[numerator   (-Real . -> . -Real)]
+[denominator (-Real . -> . -Real)]
 [rationalize (-Real -Real . -> . N)]
 [expt (cl->* (-Integer -Integer . -> . -Integer) (N N . -> . N))]
 [sqrt (cl->*
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 31495f596f..a7ca238d94 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -26,34 +26,44 @@
                (->* (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))]
+             (cl->* [->acc (list (-pair a (-pair b c))) b (list -car -cdr)]
+                    [->  (-lst a) a]))]
+[cddr  (-poly (a b c)
+              (cl->* [->acc (list (-pair a (-pair b c))) c (list -cdr -cdr)]
+                     [-> (-lst a) (-lst a)]))]
+
+[caddr  (-poly (a b c d)
+              (cl->* [->acc (list (-pair a (-pair b (-pair c d)))) c (list -car -cdr -cdr)]
+                     [-> (-lst a) a]))]
+[cdddr (-poly (a b c d)
+              (cl->* [->acc (list (-pair a (-pair b (-pair c d)))) d (list -cdr -cdr -cdr)]
+                     [-> (-lst a) a]))]
+
 [cadddr (-poly (a) (-> (-lst a) a))]
-[cddr  (-poly (a) (-> (-lst a) (-lst a)))]
-[cdddr (-poly (a) (-> (-lst a) (-lst a)))]
+[cddddr (-poly (a) (-> (-lst a) (-lst a)))]
+
 
 [first (-poly (a b) 
               (cl->*
-               (->acc (list (-pair a b)) a (list -car))
+               (->acc (list (-pair a (-lst b))) a (list -car))
                (->* (list (-lst a)) a)))]
 [second (-poly (a b c)
-               (cl-> [((-pair a (-pair b c))) b]
-                     [((-lst a)) a]))]
+               (cl->* [->acc (list (-pair a (-pair b (-lst c)))) b (list -car -cdr)]
+                      [->* (list (-lst a)) a]))]
 [third (-poly (a b c d)
-              (cl-> [((-pair a (-pair b (-pair c d)))) c]
-                    [((-lst a)) a]))]
+              (cl->* [->acc (list (-pair a (-pair b (-pair c (-lst d))))) c (list -car -cdr -cdr)]
+                     [->* (list (-lst a)) a]))]
 [fourth (-poly (a) ((-lst a) . -> .  a))]
 [fifth  (-poly (a) ((-lst a) . -> .  a))]
 [sixth  (-poly (a) ((-lst a) . -> .  a))]
 [rest (-poly (a b) 
              (cl->*
-              (->acc (list (-pair a b)) b (list -cdr))
+              (->acc (list (-pair a (-lst b))) (-lst b) (list -cdr))
               (->* (list (-lst a)) (-lst a))))]
 
 [cons (-poly (a b)
-             (cl-> [(a (-lst a)) (-lst a)]
-                   [(a b) (-pair a b)]))]
+             (cl->* [->* (list a (-lst a)) (-lst a)]
+                    [->* (list a b) (-pair a b)]))]
 [*cons (-poly (a b) (cl->
                      [(a b) (-pair a b)]
                      [(a (-lst a)) (-lst a)]))]
@@ -137,14 +147,14 @@
                        . -> .
                        (-lst b))
                       ((a . -> . Univ) (-lst a) . -> . (-lst a))))]
-[filter-not (-poly (a b) (cl->*
-                          ((a . -> . Univ) (-lst a) . -> . (-lst a))))]
+[filter-not (-poly (a) (cl->*
+                        ((a . -> . Univ) (-lst a) . -> . (-lst a))))]
 [remove  (-poly (a) (a (-lst a) . -> . (-lst a)))]
 [remq    (-poly (a) (a (-lst a) . -> . (-lst a)))]
 [remv    (-poly (a) (a (-lst a) . -> . (-lst a)))]
 [remove* (-poly (a b) ((-lst a) (-lst a) [(a b . -> . B)] . ->opt . (-lst b)))]
-[remq*   (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)]))]
-[remv*   (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)]))]
+[remq*   (-poly (a) (cl-> [((-lst a) (-lst a)) (-lst a)]))]
+[remv*   (-poly (a) (cl-> [((-lst a) (-lst a)) (-lst a)]))]
 
 (error 
  (make-Function (list 
diff --git a/collects/typed-scheme/private/base-types-extra.ss b/collects/typed-scheme/private/base-types-extra.ss
index 72c90ef6bd..f76ca4e700 100644
--- a/collects/typed-scheme/private/base-types-extra.ss
+++ b/collects/typed-scheme/private/base-types-extra.ss
@@ -12,12 +12,13 @@
 
 ;; special type names that are not bound to particular types
 (define-other-types
-  -> U mu All Opaque
-  Parameter Tuple Class Values Instance Refinement
+  -> U Rec All Opaque
+  Parameterof List Class Values Instance Refinement
   pred)
 
 (provide (rename-out [All ∀]
                      [U Un]
-                     [Tuple List]
-                     [mu Rec]))
+                     [List Tuple]
+                     [Rec mu]
+                     [Parameterof Parameter]))
 
diff --git a/collects/typed-scheme/private/base-types-new.ss b/collects/typed-scheme/private/base-types-new.ss
index fabc660af6..ffa92162d0 100644
--- a/collects/typed-scheme/private/base-types-new.ss
+++ b/collects/typed-scheme/private/base-types-new.ss
@@ -41,9 +41,11 @@
 [HashTable (-poly (a b) (-HT a b))]
 [Promise (-poly (a) (-Promise a))]
 [Pair (-poly (a b) (-pair a b))]
-[MPair (-poly (a b) (-mpair a b))]
 [Boxof (-poly (a) (make-Box a))]
 [Continuation-Mark-Set -Cont-Mark-Set]
 [False (-val #f)]
 [True (-val #t)]
 [Null (-val null)]
+[Nothing (Un)]
+[Pairof (-poly (a b) (-pair a b))]
+[MPairof (-poly (a b) (-mpair a b))]
diff --git a/collects/typed-scheme/private/base-types.ss b/collects/typed-scheme/private/base-types.ss
index 1d79709269..eb723e41e8 100644
--- a/collects/typed-scheme/private/base-types.ss
+++ b/collects/typed-scheme/private/base-types.ss
@@ -46,3 +46,7 @@
 [False (-val #f)]
 [True (-val #t)]
 [Null (-val null)]
+[Nothing (Un)]
+[Pairof (-poly (a b) (-pair a b))]
+[MPairof (-poly (a b) (-mpair a b))]
+
diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss
index 8d33892f55..fe11cea54b 100644
--- a/collects/typed-scheme/types/printer.ss
+++ b/collects/typed-scheme/types/printer.ss
@@ -185,9 +185,9 @@
                          (fp ")")]))]
     [(arr: _ _ _ _ _) (print-arr c)]
     [(Vector: e) (fp "(Vectorof ~a)" e)]
-    [(Box: e) (fp "(Box ~a)" e)]
+    [(Box: e) (fp "(Boxof ~a)" e)]
     [(Union: elems) (fp "~a" (cons 'U elems))]
-    [(Pair: l r) (fp "(Pair ~a ~a)" l r)]
+    [(Pair: l r) (fp "(Pairof ~a ~a)" l r)]
     [(F: nm) (fp "~a" nm)]   
     ;; FIXME
     [(Values: (list v)) (fp "~a" v)]
@@ -195,8 +195,8 @@
     [(ValuesDots: v dty dbound) (fp "~a" (cons 'values (append v (list dty '... dbound))))]
     [(Param: in out) 
      (if (equal? in out)
-         (fp "(Parameter ~a)" in)           
-         (fp "(Parameter ~a ~a)" in out))]
+         (fp "(Parameterof ~a)" in)           
+         (fp "(Parameterof ~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)]