diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt
index 5abbc12451..328ace3217 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt
@@ -250,7 +250,7 @@
                (let ((temporaries (generate-temporaries vs-nm)))
                  (define rv (for/fold ((rv recursive-values)) ((temp temporaries)
                                                                (v-nm vs-nm))
-                              (hash-set rv v-nm (same (impersonator/sc temp)))))
+                              (hash-set rv v-nm (same (parametric-var/sc temp)))))
                  (parametric->/sc temporaries
                     (t->sc b #:recursive-values rv)))))]
         [(Mu: n b)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/parametric.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/parametric.rkt
index 3124b229ae..3fd44de174 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/parametric.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/parametric.rkt
@@ -2,17 +2,23 @@
 
 ;; Static contract for parametric->/c.
 
-(require "../structures.rkt" "../constraints.rkt"
-         racket/list racket/match
-         unstable/contract
-         (except-in racket/contract recursive-contract)
-         (for-template racket/base racket/contract/parametric)
-         (for-syntax racket/base syntax/parse))
+(require
+  "../structures.rkt"
+  "../constraints.rkt"
+  "../terminal.rkt"
+  racket/list racket/match
+  unstable/contract
+  (except-in racket/contract recursive-contract)
+  (for-template racket/base racket/contract/parametric)
+  (for-syntax racket/base syntax/parse))
 
 (provide
   (contract-out
-    [parametric->/sc ((listof identifier?) static-contract? . -> . static-contract?)])
-  parametric->/sc:)
+    [parametric->/sc ((listof identifier?) static-contract? . -> . static-contract?)]
+    [parametric-var/sc (identifier? . -> . static-contract?)])
+  parametric->/sc:
+  (rename-out
+    [parametric-var/sc parametric-var/sc:]))
 
 
 (struct parametric-combinator combinator (vars)
@@ -44,3 +50,6 @@
   (syntax-parser
     [(_ vars body)
      #'(parametric-combinator (list body) vars)]))
+
+(define-terminal-sc parametric-var/sc (id) #:impersonator
+   id)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt
index 072bd0291d..7f7db9a562 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt
@@ -9,6 +9,7 @@
   racket/sequence
   (for-template racket/base (prefix-in c: racket/contract))
   "kinds.rkt"
+  "parametric-check.rkt"
   "structures.rkt"
   "constraints.rkt"
   "equations.rkt")
@@ -29,11 +30,13 @@
 ;; kind is the greatest kind of contract that is supported, if a greater kind would be produced the
 ;; fail procedure is called.
 (define (instantiate sc fail [kind 'impersonator])
-  (with-handlers [(exn:fail:constraint-failure?
-                    (lambda (exn) (fail #:reason (exn:fail:constraint-failure-reason exn))))]
-    (instantiate/inner sc
-      (compute-recursive-kinds
-        (contract-restrict-recursive-values (compute-constraints sc kind))))))
+  (if (parametric-check sc)
+      (fail #:reason "multiple parametric contracts are not supported")
+      (with-handlers [(exn:fail:constraint-failure?
+                        (lambda (exn) (fail #:reason (exn:fail:constraint-failure-reason exn))))]
+        (instantiate/inner sc
+          (compute-recursive-kinds
+            (contract-restrict-recursive-values (compute-constraints sc kind)))))))
 
 (define (compute-constraints sc max-kind)
   (define (recur sc)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt
new file mode 100644
index 0000000000..7900dada8a
--- /dev/null
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt
@@ -0,0 +1,26 @@
+#lang racket/base
+
+(require
+  racket/match
+  racket/contract
+  (except-in "structures.rkt" recursive-contract)
+  "combinators/parametric.rkt"
+  "combinators/structural.rkt")
+
+(provide
+  (contract-out
+    [parametric-check (static-contract? . -> . boolean?)]))
+
+(define (parametric-check sc)
+  (let/ec exit
+    (define (recur sc variance)
+      (match sc
+        [(or/sc: elems ...) (=> continue)
+         (match elems
+           [(list-no-order (parametric-var/sc: _) (parametric-var/sc: _) others ...)
+            (exit #t)]
+           [else (continue)])]
+        [else
+          (sc-traverse sc recur)]))
+    (recur sc 'covariant)
+    #f))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt
index 804ffa1945..d1c66bf396 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt
@@ -41,10 +41,8 @@
 
     ;; Polydotted functions should work
     (t/fail (-polydots (a) (->... (list) (a a) -Symbol))
-            "not supported for this type")
+            "not supported for this type")))
 
-    ;; These should fail
-    (t (-> (-poly (a b) (-> (Un a b) (Un a b))) Univ))))
 
 
 
@@ -73,6 +71,10 @@
 
               (t/fail ((-poly (a) (-vec a)) . -> . -Symbol)
                       "cannot generate contract for non-function polymorphic type")
+              (t/fail (-> (-poly (a b) (-> (Un a b) (Un a b))) Univ)
+                      "multiple parametric contracts are not supported")
+
+
               (t/fail
                 (make-Function
                   (list (make-arr* (list) -Boolean #:kws (list (make-Keyword '#:key Univ #f)))