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 0000000000..280bd9bc54
--- /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/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss
index da0990418e..b74c331316 100644
--- a/collects/typed-scheme/private/type-contract.ss
+++ b/collects/typed-scheme/private/type-contract.ss
@@ -20,7 +20,7 @@
  mzlib/trace
  scheme/list
  (only-in scheme/contract -> ->* case-> cons/c flat-rec-contract provide/contract any/c)
- (for-template scheme/base scheme/contract (only-in scheme/class object% is-a?/c subclass?/c)))
+ (for-template scheme/base scheme/contract (utils poly-c) (only-in scheme/class object% is-a?/c subclass?/c)))
 
 (define (define/fixup-contract? stx)
   (or (syntax-property stx 'typechecker:contract-def)
@@ -54,7 +54,9 @@
 (define (type->contract ty fail)
   (define vars (make-parameter '()))
   (let/cc exit
-    (let t->c ([ty ty])
+    (let loop ([ty ty] [pos? #t])
+      (define (t->c t) (loop t pos?))
+      (define (t->c/neg t) (loop t (not pos?)))
       (match ty
         [(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
         [(Univ:) #'any/c]
@@ -74,13 +76,13 @@
              (define-values (dom* rngs* rst)
                (match a
                  [(arr: dom (Values: rngs) #f #f '() _ _)
-                  (values (map t->c dom) (map t->c rngs) #f)]
+                  (values (map t->c/neg dom) (map t->c rngs) #f)]
                  [(arr: dom rng #f #f '() _ _)
-                  (values (map t->c dom) (list (t->c rng)) #f)]
+                  (values (map t->c/neg dom) (list (t->c rng)) #f)]
                  [(arr: dom (Values: rngs) rst #f '() _ _)
-                  (values (map t->c dom) (map t->c rngs) (t->c rst))]
+                  (values (map t->c/neg dom) (map t->c rngs) (t->c/neg rst))]
                  [(arr: dom rng rst #f '() _ _)
-                  (values (map t->c dom) (list (t->c rng)) (t->c rst))]))
+                  (values (map t->c/neg dom) (list (t->c rng)) (t->c/neg rst))]))
              (with-syntax 
                  ([(dom* ...) dom*]
                   [rng* (match rngs*
@@ -102,12 +104,22 @@
          #`(cons/c #,(t->c t1) #,(t->c t2))]
         [(Opaque: p? cert)
          #`(flat-contract #,(cert p?))]
-        [(F: v) (cond [(assoc v (vars)) => cadr]
+        [(F: v) (cond [(assoc v (vars)) => (if pos? second third)]
                       [else (int-err "unknown var: ~a" v)])]
+	[(Poly: vs (and b (Function: _)))
+         (match-let ([(Poly-names: vs-nm _) ty])
+           (with-syntax ([(vs+ ...) (generate-temporaries (for/list ([v vs-nm]) (symbol-append v '+)))]
+			 [(vs- ...) (generate-temporaries (for/list ([v vs-nm]) (symbol-append v '-)))])
+             (parameterize ([vars (append (map list
+					       vs
+					       (syntax->list #'(vs+ ...))
+					       (syntax->list #'(vs- ...)))
+					  (vars))])
+               #`(poly/c ([vs- vs+] ...) #,(t->c b)))))]
         [(Mu: n b)
          (match-let ([(Mu-name: n-nm _) ty])
            (with-syntax ([(n*) (generate-temporaries (list n-nm))])
-             (parameterize ([vars (cons (list n #'n*) (vars))])
+             (parameterize ([vars (cons (list n #'n* #'n*) (vars))])
                #`(flat-rec-contract n* #,(t->c b)))))]
         [(Value: #f) #'false/c]    
         [(Instance: _) #'(is-a?/c object%)]
@@ -115,10 +127,7 @@
         [(Value: '()) #'null?]
         [(Struct: _ _ _ _ #f pred? cert) (cert pred?)]
         [(Syntax: (Base: 'Symbol _)) #'identifier?]
-        [(Syntax: t)
-         (if (equal? ty Any-Syntax)
-             #`syntax?
-             #`(syntax/c #,(t->c t)))]
+        [(Syntax: t) #`(syntax/c #,(t->c t))]
         [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
         [(Param: in out) #`(parameter/c #,(t->c out))]
 	[(Hashtable: k v) #`hash?]
diff --git a/collects/typed-scheme/utils/poly-c.ss b/collects/typed-scheme/utils/poly-c.ss
new file mode 100644
index 0000000000..695a85dc50
--- /dev/null
+++ b/collects/typed-scheme/utils/poly-c.ss
@@ -0,0 +1,70 @@
+#lang scheme/base
+
+(require scheme/contract (for-syntax scheme/base))
+
+(provide memory/c apply/c poly/c)
+
+(with-contract
+ poly-internals
+ ([memory/c
+   (->*
+    []
+    [ #:name any/c
+      #:to any/c
+      #:from any/c
+      #:weak boolean?
+      #:equal (or/c 'eq 'eqv 'equal)
+      #:table (-> (and/c hash? (not/c immutable?))) ]
+    (values flat-contract? flat-contract?))]
+  [apply/c (->* [any/c] [#:name any/c] contract?)])
+
+ (define (memory/c
+          #:name [name "memory/c"]
+          #:to [to (format "~a:to" name)]
+          #:from [from (format "~a:from" name)]
+          #:weak [weak? #t]
+          #:equal [equal 'eq]
+          #:table [make-table
+                   (case equal
+                     [(eq) (if weak? make-weak-hasheq make-hasheq)]
+                     [(eqv) (if weak? make-weak-hasheqv make-hasheqv)]
+                     [(equal) (if weak? make-weak-hash make-hash)])])
+   (let* ([table (make-table)])
+     (values
+      (flat-named-contract from
+        (lambda (v) (hash-set! table v #t) #t))
+      (flat-named-contract to
+        (lambda (v) (hash-ref table v #f))))))
+
+ (define (apply/c c
+                  #:name [name (build-compound-type-name 'apply/c c)])
+   (make-proj-contract
+    name
+    (lambda (pos neg src name2)
+      (lambda (p)
+        (let* ([ctc (coerce-contract 'apply/c c)]
+               [thunk (lambda () ((((proj-get ctc) ctc) pos neg src name2) p))])
+          (make-keyword-procedure
+           (lambda (keys vals . args) (keyword-apply (thunk) keys vals args))
+           (case-lambda
+             [() ((thunk))]
+             [(a) ((thunk) a)]
+             [(a b) ((thunk) a b)]
+             [(a b c) ((thunk) a b c)]
+             [(a b c d) ((thunk) a b c d)]
+             [(a b c d e) ((thunk) a b c d e)]
+             [(a b c d e f) ((thunk) a b c d e f)]
+             [(a b c d e f g) ((thunk) a b c d e f g)]
+             [(a b c d e f g h) ((thunk) a b c d e f g h)]
+             [args (apply (thunk) args)])))))
+    procedure?)))
+
+(define-syntax (poly/c stx)
+  (syntax-case stx ()
+    [(_ opts ... ([c- c+] ...) c)
+     (quasisyntax/loc stx
+       (apply/c
+        #:name (quote #,stx)
+        (recursive-contract
+         (let-values ([(c- c+) (memory/c #:from 'c- #:to 'c+ opts ...)] ...)
+           c))))]))
diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss
index 485bc20b7f..d90e27ee33 100644
--- a/collects/typed-scheme/utils/utils.ss
+++ b/collects/typed-scheme/utils/utils.ss
@@ -19,6 +19,7 @@
          extend
          debug
          in-syntax
+	 symbol-append
 	 ;; require macros
 	 rep utils typecheck infer env private)
 
diff --git a/collects/typed/srfi/14.ss b/collects/typed/srfi/14.ss
index 4867007896..4c656e913a 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]