diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss
index 3a2fb91735..5f425efc7b 100644
--- a/collects/typed-scheme/private/type-contract.ss
+++ b/collects/typed-scheme/private/type-contract.ss
@@ -122,18 +122,14 @@
          #`(cons/c #,(t->c t1) #,(t->c t2))]
         [(Opaque: p? cert)
          #`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))]
-        [(F: v) (cond [(assoc v (vars)) => (if pos? second third)]
+        [(F: v) (cond [(assoc v (vars)) => second]
                       [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]) (format-symbol "~a+" v)))]
-			 [(vs- ...) (generate-temporaries (for/list ([v vs-nm]) (format-symbol "~a-" v)))])
-             (parameterize ([vars (append (map list
-					       vs
-					       (syntax->list #'(vs+ ...))
-					       (syntax->list #'(vs- ...)))
+           (with-syntax ([(v ...) (generate-temporaries vs-nm)])
+             (parameterize ([vars (append (map list vs (syntax->list #'(v ...)))
 					  (vars))])
-               #`(poly/c ([vs- vs+] ...) #,(t->c b)))))]
+               #`(poly/c (v ...) #,(t->c b)))))]
         [(Mu: n b)
          (match-let ([(Mu-name: n-nm _) ty])
            (with-syntax ([(n*) (generate-temporaries (list n-nm))])
diff --git a/collects/unstable/poly-c.ss b/collects/unstable/poly-c.ss
index 2d307171ef..d85c4ecb29 100644
--- a/collects/unstable/poly-c.ss
+++ b/collects/unstable/poly-c.ss
@@ -1,73 +1,87 @@
 #lang scheme/base
 
-(require scheme/contract (for-syntax scheme/base))
+(require scheme/bool scheme/contract)
 
-(provide memory/c apply/c poly/c)
+(provide poly/c parametric/c opaque/c memory/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-syntax-rule (poly/c [x ...] c)
+  (make-polymorphic-contract 'poly/c
+                             memory/c
+                             '(x ...)
+                             (lambda (x ...) c)))
 
- (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-syntax-rule (parametric/c [x ...] c)
+  (make-polymorphic-contract 'parametric/c
+                             opaque/c
+                             '(x ...)
+                             (lambda (x ...) c)))
 
- (define (apply/c c
-                  #:name [name (build-compound-type-name 'apply/c c)])
-   (simple-contract
-    #:name name
-    #:projection
-    (lambda (blame)
-      (lambda (p)
-        (let* ([ctc (coerce-contract 'apply/c c)]
-               [thunk
-                (lambda ()
-                  (((contract-projection ctc) blame) 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)])))))
-    #:first-order procedure?)))
+(define-struct polymorphic-contract [title barrier vars body]
+  #:property prop:contract
+  (build-contract-property
+   #:name
+   (lambda (c)
+     (list (polymorphic-contract-title c)
+           (polymorphic-contract-vars c)
+           '...))
+   #:projection
+   (lambda (c)
+     (lambda (b)
 
-(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))))]))
+       (define (wrap p)
+         ;; values in polymorphic types come in from negative position,
+         ;; relative to the poly/c contract
+         (define negative? (blame-swapped? b))
+         (define barrier/c (polymorphic-contract-barrier c))
+         (define instances
+           (for/list ([var (in-list (polymorphic-contract-vars c))])
+             (barrier/c negative? var)))
+         (define protector
+           (apply (polymorphic-contract-body c) instances))
+         (((contract-projection protector) b) p))
+
+       (lambda (p)
+         (unless (procedure? p)
+           (raise-blame-error b p "expected a procedure; got: ~e" p))
+         (make-keyword-procedure
+          (lambda (keys vals . args) (keyword-apply (wrap p) keys vals args))
+          (case-lambda
+            [() ((wrap p))]
+            [(a) ((wrap p) a)]
+            [(a b) ((wrap p) a b)]
+            [(a b c) ((wrap p) a b c)]
+            [(a b c d) ((wrap p) a b c d)]
+            [(a b c d e) ((wrap p) a b c d e)]
+            [(a b c d e f) ((wrap p) a b c d e f)]
+            [(a b c d e f g) ((wrap p) a b c d e f g)]
+            [(a b c d e f g h) ((wrap p) a b c d e f g h)]
+            [args (apply (wrap p) args)])))))))
+
+(define (memory/c positive? name)
+  (define memory (make-weak-hasheq))
+  (define (make x) (hash-set! memory x #t) x)
+  (define (pred x) (hash-has-key? memory x))
+  (define (get x) x)
+  (make-barrier-contract name positive? make pred get))
+
+(define (opaque/c positive? name)
+  (define-values [ type make pred getter setter ]
+    (make-struct-type name #f 1 0))
+  (define (get x) (getter x 0))
+  (make-barrier-contract name positive? make pred get))
+
+(define-struct barrier-contract [name positive? make pred get]
+  #:property prop:contract
+  (build-contract-property
+   #:name (lambda (c) (barrier-contract-name c))
+   #:projection
+   (lambda (c)
+     (lambda (b)
+       (if (boolean=? (blame-original? b) (barrier-contract-positive? c))
+         (lambda (x)
+           ((barrier-contract-make c) x))
+         (lambda (x)
+           (if ((barrier-contract-pred c) x)
+             ((barrier-contract-get c) x)
+             (raise-blame-error b x "expected a(n) ~a; got: ~e"
+                                (barrier-contract-name c) x))))))))
diff --git a/collects/unstable/scribblings/poly-c.scrbl b/collects/unstable/scribblings/poly-c.scrbl
index d5b0ff230b..422b243046 100644
--- a/collects/unstable/scribblings/poly-c.scrbl
+++ b/collects/unstable/scribblings/poly-c.scrbl
@@ -5,60 +5,91 @@
                      scheme/contract
                      scheme/base))
 
-@title[#:tag "poly-c"]{Anaphoric Contracts}
+@title[#:tag "poly-c"]{Polymorphic Contracts}
 
-@(define the-eval (make-base-eval))
-@(the-eval '(require unstable/poly-c scheme/contract))
+@(define (build-eval)
+   (let* ([e (make-base-eval)])
+     (e '(require unstable/poly-c scheme/contract))
+     e))
 
 @defmodule[unstable/poly-c]
 
 @unstable[@author+email["Sam Tobin-Hochstadt" "samth@ccs.neu.edu"]
           @author+email["Carl Eastlund" "cce@ccs.neu.edu"]]
 
+@defform[(poly/c (x ...) c)]{
 
-@defform[(poly/c ([id+ id-] ...) cnt)]{
-Creates an ``anaphoric'' contract, using the @scheme[id+ ...] as the
-positive positions, and the @scheme[id- ...] as the negative positions.  
+Creates a contract for polymorphic functions that may inspect their arguments.
+Each function is protected by @scheme[c], where each @scheme[x] is bound in
+@scheme[c] and refers to a polymorphic type that is instantiated each time the
+function is applied.
 
-Anaphoric contracts verify that only values provided to a given
-positive position flow out of the corresponding negative position.
+At each application of a function, the @scheme[poly/c] contract constructs a new
+weak, @scheme[eq?]-based hash table for each @scheme[x].  Values flowing into
+the polymorphic function (i.e. values protected by some @scheme[x] in negative
+position with respect to @scheme[poly/c]) are stored in the hash table.  Values
+flowing out of the polymorphic function (i.e. protected by some @scheme[x] in
+positive position with respect to @scheme[poly/c]) are checked for their
+presence in the hash table.  If they are present, they are returned; otherwise,
+a contract violation is signalled.
 
-@examples[#:eval the-eval
-(define/contract (f x) (poly/c ([in out]) (in . -> . out)) 
-  (if (equal? x 17) 18 x))
-(f 1)
-(f #f)
-(f 17)
+@examples[#:eval (build-eval)
+(define/contract (check x y) (poly/c [X] (boolean? X . -> . X))
+  (if (or (not x) (equal? y 'surprise))
+      'invalid
+      y))
+(check #t 'ok)
+(check #f 'ignored)
+(check #t 'surprise)
 ]
+
 }
 
-@defproc[(apply/c [cnt any/c] 
-		  [#:name name any/c 
-		  (build-compound-type-name 'apply/c c)]) contract?]{
-Produces a procedure contract that is like @scheme[cnt], but any delayed
-evalutation in @scheme[cnt] is re-done on every
-application of the contracted function.
+@defform[(parametric/c (x ...) c)]{
+
+Creates a contract for parametric polymorphic functions.  Each function is
+protected by @scheme[c], where each @scheme[x] is bound in @scheme[c] and refers
+to a polymorphic type that is instantiated each time the function is applied.
+
+At each application of a function, the @scheme[parametric/c] contract constructs
+a new opaque wrapper for each @scheme[x]; values flowing into the polymorphic
+function (i.e. values protected by some @scheme[x] in negative position with
+respect to @scheme[parametric/c]) are wrapped in the corresponding opaque
+wrapper.  Values flowing out of the polymorphic function (i.e. values protected
+by some @scheme[x] in positive position with respect to @scheme[parametric/c])
+are checked for the appropriate wrapper.  If they have it, they are unwrapped;
+if they do not, a contract violation is signalled.
+
+@examples[#:eval (build-eval)
+(define/contract (check x y) (parametric/c [X] (boolean? X . -> . X))
+  (if (or (not x) (equal? y 'surprise))
+      'invalid
+      y))
+(check #t 'ok)
+(check #f 'ignored)
+(check #t 'surprise)
+]
+
 }
 
-@defproc[(memory/c [#:name name any/c "memory/c"]
-		   [#:from from any/c (format "~a:from" name)]
-		   [#:to to any/c (format "~a:to" name)]
-		   [#:weak weak? any/c #t]
-		   [#:equal equal (or/c 'eq 'eqv 'equal) 'eq]
-		   [#:table make-table  (-> hash?)
-		   (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)])]
-		   )
-		    (values flat-contract? flat-contract?)]{
+@defproc[(memory/c [positive? boolean?] [name any/c]) contract?]{
 
-Produces a pair of contracts.  The first contract remembers all values
-that flow into it, and rejects nothing.  The second accepts only
-values that have previously been passed to the first contract.  
+This function constructs a contract that records values flowing in one direction
+in a fresh, weak hash table, and looks up values flowing in the other direction,
+signalling a contract violation if those values are not in the table.
 
-If @scheme[weak?] is not @scheme[#f], the first contract holds onto
-the values only weakly.  @scheme[from] and @scheme[to] are the names
-of the of the two contracts. }
+If @scheme[positive?] is true, values in positive position get stored and values
+in negative position are checked.  Otherwise, the reverse happens.
 
+}
 
+@defproc[(opaque/c [positive? boolean?] [name any/c]) contract?]{
+
+This function constructs a contract that wraps values flowing in one direction
+in a unique, opaque wrapper, and unwraps values flowing in the other direction,
+signalling a contract violation if those values are not wrapped.
+
+If @scheme[positive?] is true, values in positive position get wrapped and
+values in negative position get unwrapped.  Otherwise, the reverse happens.
+
+}