diff --git a/pkgs/racket-pkgs/racket-doc/scribblings/reference/contracts.scrbl b/pkgs/racket-pkgs/racket-doc/scribblings/reference/contracts.scrbl
index b6ea60caee..3dd64f231c 100644
--- a/pkgs/racket-pkgs/racket-doc/scribblings/reference/contracts.scrbl
+++ b/pkgs/racket-pkgs/racket-doc/scribblings/reference/contracts.scrbl
@@ -1157,7 +1157,7 @@ if they do not, a contract violation is signaled.
 ]
 }
 
-@defproc[(new-∀/c [name symbol?]) contract?]{
+@defproc[(new-∀/c [name (or/c symbol? #f) #f]) contract?]{
   Constructs a new universal contract.
 
   Universal contracts accept all values when in negative positions (e.g., function
@@ -1166,22 +1166,22 @@ if they do not, a contract violation is signaled.
   a universal contract accepts only values that were previously accepted
   in negative positions (by checking for the wrappers).
 
-  The name is used to identify the contract in error messages.
+  The name is used to identify the contract in error messages and defaults
+  to a name based on the lexical context of @racket[new-∀/c].
 
   For example, this contract:
   @racketblock[(let ([a (new-∀/c 'a)])
                  (-> a a))]
-  describes the identity function (or a non-terminating function)
+  describes the identity function (or a non-terminating function).
   That is, the first use of the @racket[a] appears in a
   negative position and thus inputs to that function are wrapped with an opaque struct.
   Then, when the function returns, it is checked to determine whether the result is wrapped, since
   the second @racket[a] appears in a positive position.
 
   The @racket[new-∀/c] construct constructor is dual to @racket[new-∃/c].
-
 }
 
-@defproc[(new-∃/c [name symbol?]) contract?]{
+@defproc[(new-∃/c [name (or/c symbol? #f) #f]) contract?]{
   Constructs a new existential contract.
 
   Existential contracts accept all values when in positive positions (e.g., function
@@ -1190,7 +1190,8 @@ if they do not, a contract violation is signaled.
   they accepts only values that were previously accepted in positive positions (by checking
   for the wrappers).
 
-  The name is used to identify the contract in error messages.
+  The name is used to identify the contract in error messages and defaults
+  to a name based on the lexical context of @racket[new-∀/c].
 
   For example, this contract:
   @racketblock[(let ([a (new-∃/c 'a)])
diff --git a/pkgs/racket-pkgs/racket-test/tests/racket/contract/name.rkt b/pkgs/racket-pkgs/racket-test/tests/racket/contract/name.rkt
index 68d5f4be61..861d24f481 100644
--- a/pkgs/racket-pkgs/racket-test/tests/racket/contract/name.rkt
+++ b/pkgs/racket-pkgs/racket-test/tests/racket/contract/name.rkt
@@ -326,6 +326,12 @@
   (test-name '(set/c (set/c char?) #:cmp 'eqv) (set/c (set/c char? #:cmp 'dont-care) #:cmp 'eqv))
   (test-name '(set/c (-> char? char?) #:cmp 'equal) (set/c (-> char? char?) #:cmp 'equal))
 
+  (test-name 'α (let ([α (new-∀/c)]) α))
+  (test-name 'α (let ([α (new-∀/c #f)]) α))
+  (test-name 'β (let ([α (new-∀/c 'β)]) α))
+  (test-name '∀∃-unknown ((values new-∀/c)))
+  (test-name '∀∃-unknown ((values new-∀/c) #f))
+  
   (test-name '(class/c [m (->m integer? integer?)]) (class/c [m (->m integer? integer?)]))
   (test-name '(class/c [m (->*m (integer?) (integer?) integer?)])
               (class/c [m (->*m (integer?) (integer?) integer?)]))
diff --git a/racket/collects/racket/contract/private/exists.rkt b/racket/collects/racket/contract/private/exists.rkt
index 636c298ccd..c58e7e46c2 100644
--- a/racket/collects/racket/contract/private/exists.rkt
+++ b/racket/collects/racket/contract/private/exists.rkt
@@ -1,10 +1,12 @@
 #lang racket/base
 
 (require "prop.rkt"
-         "blame.rkt")
+         "blame.rkt"
+         "guts.rkt"
+         (for-syntax racket/base syntax/name))
 
-(provide new-∃/c
-         new-∀/c
+(provide (rename-out [_new-∃/c new-∃/c]
+                     [_new-∀/c new-∀/c])
          ∀∃?)
 
 (define (∀∃-proj ctc)
@@ -22,6 +24,7 @@
 
 (define-struct ∀∃/c (in out pred? name neg?)
   #:omit-define-syntaxes
+  #:property prop:custom-write custom-write-property-proc  
   #:property prop:contract
   (build-contract-property
    #:name (λ (ctc) (∀∃/c-name ctc))
@@ -30,6 +33,27 @@
 
 (define-struct ∀∃ ())
 
+(define-for-syntax (∀∃/trans which stx)
+  (define name (or (syntax-local-name)
+                   (let ([n (syntax-local-infer-name stx)])
+                     (string->symbol
+                      (format "∀∃-~a" (or n "unknown"))))))
+  (syntax-case stx ()
+    [x 
+     (identifier? #'x) 
+     #`(let ([which (case-lambda
+                      [() (#,which '#,name)]
+                      [(x) (#,which (or x '#,name))])])
+         which)]
+    [(f) #`(#,which '#,name)]
+    [(f x) #`(#,which (or x '#,name))]
+    [(f . x)
+     (with-syntax ([app (datum->syntax stx '#%app stx stx)])
+       #`(app #,which . x))]))
+
+(define-syntax (_new-∀/c stx) (∀∃/trans #'new-∀/c stx))
+(define-syntax (_new-∃/c stx) (∀∃/trans #'new-∃/c stx))
+
 (define (new-∃/c raw-name) (mk raw-name #t))
 (define (new-∀/c raw-name) (mk raw-name #f))
 
@@ -38,4 +62,3 @@
   (define-values (struct-type constructor predicate accessor mutator)
     (make-struct-type name struct:∀∃ 1 0))
   (make-∀∃/c constructor (λ (x) (accessor x 0)) predicate raw-name neg?))
-