diff --git a/collects/tests/typed-scheme/succeed/with-syntax.rkt b/collects/tests/typed-scheme/succeed/with-syntax.rkt
new file mode 100644
index 0000000000..07108e457c
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/with-syntax.rkt
@@ -0,0 +1,7 @@
+#lang typed/racket
+(require racket/syntax)
+
+(: f : -> Syntax)
+(define (f)
+  (with-syntax* ([(x ...) (list 1 2 3)])
+    #`(#,(syntax +) x ...)))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/base-env.rkt b/collects/typed-scheme/private/base-env.rkt
index 49f7cd8411..2d5d294161 100644
--- a/collects/typed-scheme/private/base-env.rkt
+++ b/collects/typed-scheme/private/base-env.rkt
@@ -19,6 +19,7 @@
   racket/mpair
   racket/base
   racket/set
+  syntax/stx racket/private/stx
   (only-in string-constants/private/only-once maybe-print-message)
   (only-in mzscheme make-namespace)
   (only-in racket/match/runtime match:error matchable? match-equality-test))
@@ -1058,3 +1059,6 @@
 [ephemeron? (make-pred-ty (make-Ephemeron Univ))]
 [ephemeron-value (-poly (v) (-> (make-Ephemeron v) (Un (-val #f) v)))]
 
+; syntax/stx (needed for `with-syntax')
+[stx->list (-> (-Syntax Univ) (-lst (-Syntax Univ)))]
+[stx-list? (-> (-Syntax Univ) -Boolean)]
\ No newline at end of file
diff --git a/collects/typed-scheme/private/base-special-env.rkt b/collects/typed-scheme/private/base-special-env.rkt
index 1927d1ac49..455dc32f22 100644
--- a/collects/typed-scheme/private/base-special-env.rkt
+++ b/collects/typed-scheme/private/base-special-env.rkt
@@ -138,5 +138,26 @@
   [(syntax-parse (local-expand #'(in-bytes-lines) 'expression #f)
      [(i-n _ ...)
       #'i-n])
-   (->opt [-Input-Port -Symbol] (-seq -Bytes))])
+   (->opt [-Input-Port -Symbol] (-seq -Bytes))]
+  
+  ;; from the expansion of `with-syntax'
+  [(syntax-parse (local-expand #'(with-syntax ([x 1]) #'(x)) 'expression null)
+     #:literals (let-values #%plain-app #%plain-lambda if letrec-syntaxes+values)
+     [(let-values _
+        (let-values _
+          (let-values _
+            (if _
+                (let-values _ (letrec-syntaxes+values _ _ (#%plain-app (#%plain-lambda _ (#%plain-app apply-pattern-substitute _ _ _)) _)))
+                _))))
+      #'apply-pattern-substitute])
+   (->* (list (-Syntax Univ) Univ) Univ Any-Syntax)]
+  
+  [(syntax-parse (local-expand #'(with-syntax ([x 1]) #'(x)) 'expression null)
+     #:literals (let-values #%plain-app #%plain-lambda if letrec-syntaxes+values)
+    [(let-values _ (let-values _ 
+                     (let-values _ (if _ _ (let-values _ 
+                                             (if _ (let-values _ (letrec-syntaxes+values _ _ (#%plain-app with-syntax-fail _))) _))))))
+      #'with-syntax-fail])
+   (-> (-Syntax Univ) (Un))]
+  )