diff --git a/typed-racket-doc/typed-racket/scribblings/reference/libraries.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/libraries.scrbl
index ff4cb986f..07286204d 100644
--- a/typed-racket-doc/typed-racket/scribblings/reference/libraries.scrbl
+++ b/typed-racket-doc/typed-racket/scribblings/reference/libraries.scrbl
@@ -287,7 +287,7 @@ following steps are required:
   @item{Determine the data manipulated by the library, and how it will
   be represented in Typed Racket.}
   @item{Specify that data in Typed Racket, using @racket[require/typed]
-  and @racket[#:opaque] and/or @racket[#:struct].}
+  and @racket[#:type/predicate] and/or @racket[#:struct].}
   @item{Use the data types to import the various functions and constants
   of the library.}
   @item{Provide all the relevant identifiers from the new adapter module.}
diff --git a/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl
index 6fb1845e2..ff8f62ce5 100644
--- a/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl
+++ b/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl
@@ -487,11 +487,26 @@ the type:
 @defform[(make-predicate t)]{
 
 Evaluates to a predicate for the type @racket[t], with the type
-@racket[(Any -> Boolean : t)]. @racket[t] may not contain function types, or
-types that may refer to mutable data such as @racket[(Vectorof Integer)].}
+@racket[(Any -> Boolean : t)]. @racket[t] may not contain function types,
+@racket[Type/Predicate] types, or types that may refer to mutable data
+such as @racket[(Vectorof Integer)].
+
+If the type @racket[t] includes @racket[Type/Predicate] types,
+@racket[make-positive-predicate] should be used instead.}
 
 @defform[(define-predicate name t)]{
-Equivalent to @racket[(define name (make-predicate t))].
+Equivalent to @racket[(define name (make-predicate t))].}
+
+@defform[(make-positive-predicate t)]{
+
+Evaluates to a predicate for the type @racket[t], with the type
+@racket[(Any -> Boolean : #:+ t)]. @racket[t] may not contain function types, or
+types that may refer to mutable data such as @racket[(Vectorof Integer)].
+
+@racket[make-positive-predicate] does work with @racket[Type/Predicate] types.}
+
+@defform[(define-positive-predicate name t)]{
+Equivalent to @racket[(define name (make-positive-predicate t))].}
 
 @section{Type Annotation and Instantiation}
 
@@ -611,6 +626,7 @@ optionally-renamed identifier.
             [#:struct maybe-tvars (name-id parent) ([f : t] ...)
                  struct-option ...]
             [#:opaque t pred]
+            [#:type/predicate t pred]
 	    [#:signature name ([id : t] ...)]]
  [maybe-renamed id
                 (orig-id new-id)]
@@ -664,6 +680,11 @@ Opaque types must be required lexically before they are used.
     evt?
     (sync (alarm-evt (+ 100 (current-inexact-milliseconds))))]
 
+@index["type/predicate"]{The fifth case} defines a new type @racket[t]
+to represent values which have passed @racket[pred] at any point.
+@racket[pred] is imported from module @racket[m] with type
+@racket[(Any -> Boolean : #:+ t)].
+
 @index["signature"]{The @racket[#:signature] keyword} registers the required
 signature in the signature environment. For more information on the use of
 signatures in Typed Racket see the documentation for
diff --git a/typed-racket-doc/typed-racket/scribblings/reference/typed-units.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/typed-units.scrbl
index 223a85b1a..3f114859a 100644
--- a/typed-racket-doc/typed-racket/scribblings/reference/typed-units.scrbl
+++ b/typed-racket-doc/typed-racket/scribblings/reference/typed-units.scrbl
@@ -255,6 +255,7 @@ The primary use of is for the reflective operation @racket[unit?]}
             [#:struct (name parent) ([f : t] ...)
                  struct-option ...]
             [#:opaque t pred]
+            [#:type/predicate t pred]
 	    [#:signature name ([id : t] ...)]]
  [maybe-renamed id
                 (orig-id new-id)]
diff --git a/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
index 48ccad993..f88278bd9 100644
--- a/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
+++ b/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
@@ -1020,4 +1020,9 @@ prefab types with the (implicitly quoted) prefab-key
 @defform[(Opaque t)]{A type constructed using the @racket[#:opaque]
 clause of @racket[require/typed].}
 
+@defform[(Type/Predicate pred-id)]{
+  A type constructed using the @racket[#:type/predicate] clause of
+  @racket[require/typed].
+}
+
 @(close-eval the-eval)
diff --git a/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt b/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt
index b3587881d..c70d11269 100644
--- a/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt
+++ b/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt
@@ -20,7 +20,7 @@
 ;; special type names that are not bound to particular types
 (define-other-types
   -> ->* case-> U Union ∩ Intersection Rec All Opaque Immutable-Vector Mutable-Vector Vector
-  Parameterof List List* Class Object Row Unit Values AnyValues Instance Refinement
+  Parameterof List List* Class Object Row Unit Values AnyValues Instance Refinement Type/Predicate
   pred Struct Struct-Type Prefab PrefabTop Distinction Sequenceof Refine Self Imp)
 
 (define-other-props
diff --git a/typed-racket-lib/typed-racket/base-env/extra-env-lang.rkt b/typed-racket-lib/typed-racket/base-env/extra-env-lang.rkt
index 571eb6b55..626cb991e 100644
--- a/typed-racket-lib/typed-racket/base-env/extra-env-lang.rkt
+++ b/typed-racket-lib/typed-racket/base-env/extra-env-lang.rkt
@@ -31,6 +31,7 @@
     #:attributes (form outer-form)
     (pattern :simple-clause)
     (pattern :opaque-clause)
+    (pattern :type/predicate-clause)
     (pattern :struct-clause))
 
   (define-syntax-class simple-clause
@@ -52,6 +53,19 @@
                                    (define-syntax type type-name-error)
                                    (provide type pred))))
 
+  (define-syntax-class type/predicate-clause
+    #:description "[#:type/predicate type pred]"
+    (pattern [#:type/predicate type:id pred:id]
+             #:with form
+             #'(begin
+                 (register-type (quote-syntax id)
+                                (asym-pred Univ B (-PS (-is-type 0 (make-Type/Predicate #'pred)) -tt)))
+                 (register-type-name (quote-syntax type)
+                                     (make-Type/Predicate #'pred)))
+             #:with outer-form #'(begin
+                                   (define-syntax type type-name-error)
+                                   (provide type pred))))
+
   (define-syntax-class struct-clause
     #:description "[#:struct name ([field : type] ...)]"
     ;; FIXME: support other struct options
@@ -100,7 +114,8 @@
                              typed-racket/env/global-env typed-racket/env/type-alias-env
                              typed-racket/types/struct-table typed-racket/types/abbrev
                              typed-racket/typecheck/tc-structs
-                             (only-in typed-racket/rep/type-rep make-Name make-Opaque)
+                             (only-in typed-racket/rep/type-rep make-Name make-Opaque
+                                      make-Type/Predicate)
                              (rename-in racket/private/sort [sort raw-sort]))
                     ;; FIXME: add a switch to turn contracts on for testing
                     binding.form ...)))
diff --git a/typed-racket-lib/typed-racket/base-env/prims-contract.rkt b/typed-racket-lib/typed-racket/base-env/prims-contract.rkt
index 4df335ef7..156048b55 100644
--- a/typed-racket-lib/typed-racket/base-env/prims-contract.rkt
+++ b/typed-racket-lib/typed-racket/base-env/prims-contract.rkt
@@ -12,26 +12,30 @@
 ;;
 ;; - their implementations (under the same names) are defined at phase
 ;;   0 using `define` in the main module
-;; 
+;;
 ;; - the `forms` submodule uses `lazy-require` to load the
 ;;   implementations of the forms
 
 
 (provide require/opaque-type require-typed-struct-legacy require-typed-struct
+         require/predicate-type
          require/typed-legacy require/typed require/typed/provide
          require-typed-struct/provide core-cast make-predicate define-predicate
+         make-positive-predicate define-positive-predicate
          require-typed-signature)
 
 (module forms racket/base
   (require (for-syntax racket/lazy-require racket/base))
-  (begin-for-syntax 
+  (begin-for-syntax
     (lazy-require [(submod "..")
                    (require/opaque-type
+                    require/predicate-type
                     require-typed-signature
                     require-typed-struct-legacy
                     require-typed-struct
                     require/typed-legacy require/typed require/typed/provide
-                    require-typed-struct/provide core-cast make-predicate define-predicate)]))
+                    require-typed-struct/provide core-cast make-predicate define-predicate
+                    make-positive-predicate define-positive-predicate)]))
   (define-syntax (def stx)
     (syntax-case stx ()
       [(_ id ...)
@@ -39,11 +43,13 @@
          #'(begin (provide (rename-out [names id] ...))
                   (define-syntax (names stx) (id stx)) ...))]))
   (def require/opaque-type
+        require/predicate-type
         require-typed-signature
         require-typed-struct-legacy
         require-typed-struct
         require/typed-legacy require/typed require/typed/provide
-        require-typed-struct/provide make-predicate define-predicate)
+        require-typed-struct/provide make-predicate define-predicate
+        make-positive-predicate define-positive-predicate)
 
   ;; Expand `cast` to a `core-cast` with an extra `#%expression` in order
   ;; to prevent the contract generation pass from executing too early
@@ -166,10 +172,17 @@
     (pattern [(~or (~datum opaque) #:opaque) opaque ty:id pred:id #:name-exists]
              #:with opt #'(#:name-exists)))
 
+  (define-syntax-class type/predicate-clause
+    #:attributes (ty pred opt)
+    (pattern [#:type/predicate ty:id pred:id]
+             #:with opt #'()))
+
   (define-syntax-class (clause legacy unsafe? lib)
    #:attributes (spec)
    (pattern oc:opaque-clause #:attr spec
      #`(require/opaque-type oc.ty oc.pred #,lib #,@(if unsafe? #'(unsafe-kw) #'()) . oc.opt))
+   (pattern tpc:type/predicate-clause #:attr spec
+     #`(require/predicate-type tpc.ty tpc.pred #,lib #,@(if unsafe? #'(unsafe-kw) #'()) . tpc.opt))
    (pattern (~var strc (struct-clause legacy)) #:attr spec
      #`(require-typed-struct strc.nm (strc.tvar ...)
                              (strc.body ...) strc.constructor-parts ...
@@ -204,7 +217,7 @@
               ;; define `cnt*` to be fixed up later by the module type-checking
               (define cnt*
                 (syntax-local-lift-expression
-                 (make-contract-def-rhs #'ty #f (attribute parent))))
+                 (make-contract-def-rhs #'ty #f #f (attribute parent))))
               (quasisyntax/loc stx
                 (begin
                   ;; register the identifier so that it has a binding (for top-level)
@@ -251,6 +264,11 @@
               (require/typed/provide lib other-clause ...))]
     [(_ lib (~and clause [#:opaque t:id pred:id])
         other-clause ...)
+     #'(begin (require/typed lib clause)
+              (provide t pred)
+              (require/typed/provide lib other-clause ...))]
+    [(_ lib (~and clause [#:type/predicate t:id pred:id])
+        other-clause ...)
      #'(begin (require/typed lib clause)
               (provide t pred)
               (require/typed/provide lib other-clause ...))]))
@@ -269,16 +287,22 @@
 ;; Conversion of types to contracts
 ;;  define-predicate
 ;;  make-predicate
+;;  define-positive-predicate
+;;  make-positive-predicate
 ;;  cast
 
 ;; Helpers to construct syntax for contract definitions
-;; make-contract-def-rhs : Type-Stx Boolean Boolean -> Syntax
-(define (make-contract-def-rhs type flat? maker?)
-  (define contract-def `#s(contract-def ,type ,flat? ,maker? untyped))
+;; make-contract-def-rhs : Type-Stx Boolean Boolean Boolean -> Syntax
+;; The exact? argument determines whether the contract must decide
+;; exactly whether the value has the type.
+;;  - flat? true and exact? true must generate (-> Any Boolean : type)
+;;  - flat? true and exact? false can generate (-> Any Boolean : #:+ type)
+(define (make-contract-def-rhs type flat? exact? maker?)
+  (define contract-def `#s(contract-def ,type ,flat? ,exact? ,maker? untyped))
   (contract-def-property #'#f (λ () contract-def)))
 
-;; make-contract-def-rhs/from-typed : Id Boolean Boolean -> Syntax
-(define (make-contract-def-rhs/from-typed id flat? maker?)
+;; make-contract-def-rhs/from-typed : Id Boolean Boolean Boolean -> Syntax
+(define (make-contract-def-rhs/from-typed id flat? exact? maker?)
   (contract-def-property
    #'#f
    ;; This function should only be called after the type-checking pass has finished.
@@ -291,7 +315,7 @@
          (if types
              #`(U #,@types)
              #f)))
-     `#s(contract-def ,type-stx ,flat? ,maker? typed))))
+     `#s(contract-def ,type-stx ,flat? ,exact? ,maker? typed))))
 
 
 (define (define-predicate stx)
@@ -312,8 +336,9 @@
 (define (make-predicate stx)
   (syntax-parse stx
     [(_ ty:expr)
+     ; passing #t for exact? makes it error on Type/Predicate types
      (define name (syntax-local-lift-expression
-                   (make-contract-def-rhs #'ty #t #f)))
+                   (make-contract-def-rhs #'ty #t #t #f)))
      (define (check-valid-type _)
        (define type (parse-type #'ty))
        (define vars (fv type))
@@ -325,6 +350,40 @@
      #`(#,(external-check-property #'#%expression check-valid-type)
         #,(ignore-some/expr #`(flat-contract-predicate #,name) #'(Any -> Boolean : ty)))]))
 
+
+(define (define-positive-predicate stx)
+  (syntax-parse stx
+    [(_ name:id ty:expr)
+     #`(begin
+         ;; We want the value bound to name to have a nice object name. Using the built in mechanism
+         ;; of define has better performance than procedure-rename.
+         #,(ignore
+            (syntax/loc stx
+              (define name
+                (let ([pred (make-positive-predicate ty)])
+                  (lambda (x) (pred x))))))
+         ;; not a require, this is just the unchecked declaration syntax
+         #,(internal (syntax/loc stx (require/typed-internal name (Any -> Boolean : #:+ ty)))))]))
+
+
+(define (make-positive-predicate stx)
+  (syntax-parse stx
+    [(_ ty:expr)
+     ; passing #f for exact? makes it work with Type/Predicate types
+     (define name (syntax-local-lift-expression
+                   (make-contract-def-rhs #'ty #t #f #f)))
+     (define (check-valid-type _)
+       (define type (parse-type #'ty))
+       (define vars (fv type))
+       ;; If there was an error don't create another one
+       (unless (or (Error? type) (null? vars))
+         (tc-error/delayed
+          "Type ~a could not be converted to a predicate because it contains free variables."
+          type)))
+     #`(#,(external-check-property #'#%expression check-valid-type)
+        #,(ignore-some/expr #`(flat-contract-predicate #,name) #'(Any -> Boolean : #:+ ty)))]))
+
+
 ;; wrapped above in the `forms` submodule
 (define (core-cast stx)
   (syntax-parse stx
@@ -349,10 +408,10 @@
             #'v]
            [else
             (define new-ty-ctc (syntax-local-lift-expression
-                                (make-contract-def-rhs #'ty #f #f)))
+                                (make-contract-def-rhs #'ty #f #f #f)))
             (define existing-ty-id new-ty-ctc)
             (define existing-ty-ctc (syntax-local-lift-expression
-                                     (make-contract-def-rhs/from-typed existing-ty-id #f #f)))
+                                     (make-contract-def-rhs/from-typed existing-ty-id #f #f #f)))
             (define (store-existing-type existing-type)
               (check-no-free-vars existing-type #'v)
               (cast-table-add! existing-ty-id (datum->syntax #f existing-type #'v)))
@@ -408,6 +467,33 @@
                                    (any-wrap-warning/c . c-> . boolean?)))))
            #,(ignore #'(require/contract pred hidden pred-cnt lib)))))]))
 
+(define (require/predicate-type stx)
+  (define-syntax-class unsafe-id
+    (pattern (~literal unsafe-kw)))
+  (syntax-parse stx
+    [_ #:when (eq? 'module-begin (syntax-local-context))
+       ;; it would be inconvenient to find the correct #%module-begin here, so we rely on splicing
+       #`(begin #,stx (begin))]
+    [(_ ty:id pred:id lib (~optional unsafe:unsafe-id))
+     (with-syntax ([hidden (generate-temporary #'pred)])
+       ;; this is needed because this expands to the contract directly without
+       ;; going through the normal `make-contract-def-rhs` function.
+       (set-box! include-extra-requires? #t)
+       (quasisyntax/loc stx
+         (begin
+           ;; register the identifier for the top-level (see require/typed)
+           #,@(if (eq? (syntax-local-context) 'top-level)
+                  (list #'(define-syntaxes (hidden) (values)))
+                  null)
+           #,(internal #'(require/typed-internal hidden (Any -> Boolean : #:+ (Type/Predicate pred))))
+           #,(syntax/loc stx (define-type-alias ty (Type/Predicate pred)))
+           #,(if (attribute unsafe)
+                 (ignore #'(define pred-cnt any/c)) ; unsafe- shouldn't generate contracts
+                 (ignore #'(define pred-cnt
+                             (or/c struct-predicate-procedure?/c
+                                   (any-wrap-warning/c . c-> . boolean?)))))
+           #,(ignore #'(require/contract pred hidden pred-cnt lib)))))]))
+
 
 
 (module self-ctor racket/base
diff --git a/typed-racket-lib/typed-racket/env/init-envs.rkt b/typed-racket-lib/typed-racket/env/init-envs.rkt
index ad84e8161..d34c70a63 100644
--- a/typed-racket-lib/typed-racket/env/init-envs.rkt
+++ b/typed-racket-lib/typed-racket/env/init-envs.rkt
@@ -275,6 +275,8 @@
                 (list ,@(map type->sexp rands)))]
     [(Opaque: pred)
      `(make-Opaque (quote-syntax ,pred))]
+    [(Type/Predicate: pred)
+     `(make-Type/Predicate (quote-syntax ,pred))]
     [(Refinement: parent pred)
      `(make-Refinement ,(type->sexp parent) (quote-syntax ,pred))]
     [(Mu-maybe-name: n (? Type? b))
diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt
index 8a755dd98..bf7e5a8bb 100644
--- a/typed-racket-lib/typed-racket/private/parse-type.rkt
+++ b/typed-racket-lib/typed-racket/private/parse-type.rkt
@@ -139,6 +139,7 @@
 (define-literal-syntax-class #:for-label Union)
 (define-literal-syntax-class #:for-label All)
 (define-literal-syntax-class #:for-label Opaque)
+(define-literal-syntax-class #:for-label Type/Predicate)
 (define-literal-syntax-class #:for-label Parameter)
 (define-literal-syntax-class #:for-label Immutable-Vector)
 (define-literal-syntax-class #:for-label Mutable-Vector)
@@ -789,6 +790,8 @@
        (parse-all-type stx)]
       [(:Opaque^ p?:id)
        (make-Opaque #'p?)]
+      [(:Type/Predicate^ p?:id)
+       (make-Type/Predicate #'p?)]
       [(:Distinction^ name:id unique-id:id rep-ty:expr)
        (-Distinction (syntax-e #'name) (syntax-e #'unique-id) (parse-type #'rep-ty))]
       [(:Parameter^ t)
@@ -1106,6 +1109,8 @@
           Err])]
       [(:Opaque^ . rest)
        (parse-error "bad syntax in Opaque")]
+      [(:Type/Predicate^ . rest)
+       (parse-error "bad syntax in Type/Predicate")]
       [(:U^ . rest)
        (parse-error "bad syntax in Union")]
       [(:Rec^ . rest)
diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt
index 246920711..ca26f599d 100644
--- a/typed-racket-lib/typed-racket/private/type-contract.rkt
+++ b/typed-racket-lib/typed-racket/private/type-contract.rkt
@@ -50,7 +50,11 @@
           #t)]
     [_ #f]))
 
-(struct contract-def (type flat? maker? typed-side) #:prefab)
+;; The exact? field determines whether the contract must decide
+;; exactly whether the value has the type.
+;;  - flat? true and exact? true must generate (-> Any Boolean : type)
+;;  - flat? true and exact? false can generate (-> Any Boolean : #:+ type)
+(struct contract-def (type flat? exact? maker? typed-side) #:prefab)
 
 ;; get-contract-def-property : Syntax -> (U False Contract-Def)
 ;; Checks if the given syntax needs to be fixed up for contract generation
@@ -83,7 +87,8 @@
 ;; (such as mutually recursive class types).
 (define (generate-contract-def stx cache sc-cache)
   (define prop (get-contract-def-property stx))
-  (match-define (contract-def type-stx flat? maker? typed-side) prop)
+  ;; TODO: deal with exact? differently for Type/Predicate and Opaque
+  (match-define (contract-def type-stx flat? exact? maker? typed-side) prop)
   (define *typ (if type-stx (parse-type type-stx) t:-Dead-Code))
   (define kind (if (and type-stx flat?) 'flat 'impersonator))
   (syntax-parse stx #:literals (define-values)
@@ -536,6 +541,11 @@
         (promise/sc (t->sc t))]
        [(Opaque: p?)
         (flat/sc #`(flat-named-contract (quote #,(syntax-e p?)) #,p?))]
+       [(Type/Predicate: p?)
+        ; TODO:
+        ;   make it error on `make-predicate`,
+        ;   but work on `make-positive-predicate`, `cast`, and type-untyped boundaries
+        (flat/sc #`(flat-named-contract (quote #,(syntax-e p?)) #,p?))]
        [(Continuation-Mark-Keyof: t)
         (continuation-mark-key/sc (t->sc t))]
        ;; TODO: this is not quite right for case->
diff --git a/typed-racket-lib/typed-racket/private/with-types.rkt b/typed-racket-lib/typed-racket/private/with-types.rkt
index b3613d7ef..5eb6cd111 100644
--- a/typed-racket-lib/typed-racket/private/with-types.rkt
+++ b/typed-racket-lib/typed-racket/private/with-types.rkt
@@ -154,7 +154,7 @@
 (define (type-stxs->ids+defs type-stxs typed-side)
   (for/lists (_1 _2) ([t (in-list type-stxs)])
     (define ctc-id (generate-temporary))
-    (define contract-def `#s(contract-def ,t #f #f ,typed-side))
+    (define contract-def `#s(contract-def ,t #f #f #f ,typed-side))
     (values ctc-id
             #`(define-values (#,ctc-id)
                 #,(contract-def-property
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 011e8d127..b85dd01f6 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -543,6 +543,10 @@
   #:base
   [#:custom-constructor (make-Opaque (normalize-id pred))])
 
+(def-type Type/Predicate ([pred identifier?])
+  #:base
+  [#:custom-constructor (make-Type/Predicate (normalize-id pred))])
+
 
 
 ;;************************************************************
diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/simple.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/simple.rkt
index 536d95d6a..bfaf43fb5 100644
--- a/typed-racket-lib/typed-racket/static-contracts/combinators/simple.rkt
+++ b/typed-racket-lib/typed-racket/static-contracts/combinators/simple.rkt
@@ -47,7 +47,7 @@
         #:methods gen:equal+hash
          [(define (equal-proc s1 s2 recur)
             (and ;; have to make sure identifiers are compared by free-id=?
-                 ;; because of struct predicates, opaque, etc.
+                 ;; because of struct predicates, opaque, type/predicate, etc.
                  (stx-equal? (simple-contract-syntax s1)
                              (simple-contract-syntax s2))
                  (recur (simple-contract-kind s1)
@@ -75,4 +75,4 @@
 (define (chaperone/sc ctc [name #f])
   (simple-contract ctc 'chaperone name))
 (define (impersonator/sc ctc [name #f])
-  (simple-contract ctc 'impersonator name))
\ No newline at end of file
+  (simple-contract ctc 'impersonator name))
diff --git a/typed-racket-lib/typed-racket/types/overlap.rkt b/typed-racket-lib/typed-racket/types/overlap.rkt
index c3b2ce416..6d2a4f532 100644
--- a/typed-racket-lib/typed-racket/types/overlap.rkt
+++ b/typed-racket-lib/typed-racket/types/overlap.rkt
@@ -50,6 +50,7 @@
    [((Univ:) _) #:no-order #t]
    [((or (B: _) (F: _)) _) #:no-order #t]
    [((Opaque: _) _) #:no-order #t]
+   [((Type/Predicate: _) _) #:no-order #t]
    [((Name/simple: n) (Name/simple: n*)) #:when (free-identifier=? n n*) #t]
    [((Distinction: _ _ t1) t2) #:no-order (overlap? t1 t2)]
    [(t1 (or (? Name? t2)
diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt
index 24ed65f38..90ed88c9a 100644
--- a/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/typed-racket-lib/typed-racket/types/printer.rkt
@@ -655,6 +655,7 @@
     [(? improper-tuple? t)
      `(List* ,@(map type->sexp (improper-tuple-elems t)))]
     [(Opaque: pred) `(Opaque ,(syntax->datum pred))]
+    [(Type/Predicate: pred) `(Type/Predicate ,(syntax->datum pred))]
     [(Struct: nm par (list (fld: t _ _) ...) proc _ _ property-tys)
      `#(,(string->symbol (format "struct:~a" (syntax-e nm)))
         ,(map t->s t)
diff --git a/typed-racket-lib/typed/private/no-check-helper.rkt b/typed-racket-lib/typed/private/no-check-helper.rkt
index e57fc733f..9c1285c20 100644
--- a/typed-racket-lib/typed/private/no-check-helper.rkt
+++ b/typed-racket-lib/typed/private/no-check-helper.rkt
@@ -4,7 +4,8 @@
 
 (require
  (except-in typed-racket/base-env/prims
-            require/typed require/opaque-type require-typed-struct require/typed/provide)
+            require/typed require/opaque-type require-typed-struct require/typed/provide
+            require/predicate-type)
  typed-racket/base-env/base-types-extra
  (for-syntax racket/base syntax/parse syntax/struct
              syntax/parse/experimental/template))
@@ -37,25 +38,32 @@
                #:with opt #'())
       (pattern [(~or #:opaque (~datum opaque)) ty:id pred:id #:name-exists]
                #:with opt #'(#:name-exists)))
+    (define-syntax-class type/predicate-clause
+      #:attributes (ty pred opt)
+      (pattern [#:type/predicate ty:id pred:id]
+               #:with opt #'()))
     (define-splicing-syntax-class struct-option
       (pattern (~seq #:constructor-name cname:id))
       (pattern (~seq #:extra-constructor-name extra-cname:id)))
     (values
-     (syntax-parser 
-       [(_ lib (~or sc:simple-clause strc:struct-clause oc:opaque-clause) ...)
+     (syntax-parser
+       [(_ lib (~or sc:simple-clause strc:struct-clause oc:opaque-clause tpc:type/predicate-clause) ...)
         (template
          (begin
            (require/opaque-type oc.ty oc.pred lib . oc.opt) ...
+           (require/predicate-type tpc.ty tpc.pred lib . tpc.opt) ...
            (require/typed sc.nm sc.ty lib) ...
            (require-typed-struct strc.nm (strc.body ...) (?@ . strc.opts) ... lib) ...))]
        [(_ nm:opt-rename ty lib (~optional [~seq #:struct-maker parent]) ...)
-        #'(require (only-in lib nm.spec))]) 
+        #'(require (only-in lib nm.spec))])
      (syntax-parser
-       [(_ lib (~or sc:simple-clause strc:struct-clause oc:opaque-clause) ...)
+       [(_ lib (~or sc:simple-clause strc:struct-clause oc:opaque-clause tpc:type/predicate-clause) ...)
         (template
          (begin
            (require/opaque-type oc.ty oc.pred lib . oc.opt) ...
            (provide oc.pred) ...
+           (require/predicate-type tpc.ty tpc.pred lib . tpc.opt) ...
+           (provide tpc.pred) ...
            (require/typed sc.nm sc.ty lib) ...
            (provide sc.nm) ...
            (require-typed-struct strc.nm (strc.body ...) (?@ . strc.opts) ... lib) ...
@@ -67,6 +75,9 @@
 (define-syntax-rule (require/opaque-type ty pred lib . _)
   (require (only-in lib pred)))
 
+(define-syntax-rule (require/predicate-type ty pred lib . _)
+  (require (only-in lib pred)))
+
 (define-syntax (require-typed-struct stx)
   (syntax-parse stx #:literals (:)
     [(_ (~or nm:id (nm:id _:id)) ([fld : ty] ...)
diff --git a/typed-racket-lib/typed/racket/unsafe.rkt b/typed-racket-lib/typed/racket/unsafe.rkt
index d3086f45c..1416c88f3 100644
--- a/typed-racket-lib/typed/racket/unsafe.rkt
+++ b/typed-racket-lib/typed/racket/unsafe.rkt
@@ -52,6 +52,11 @@
               (unsafe-require/typed/provide lib other-clause ...))]
     [(_ lib (~and clause [#:opaque t:id pred:id])
         other-clause ...)
+     #'(begin (unsafe-require/typed lib clause)
+              (provide t pred)
+              (unsafe-require/typed/provide lib other-clause ...))]
+    [(_ lib (~and clause [#:type/predicate t:id pred:id])
+        other-clause ...)
      #'(begin (unsafe-require/typed lib clause)
               (provide t pred)
               (unsafe-require/typed/provide lib other-clause ...))]))
diff --git a/typed-racket-test/unit-tests/parse-type-tests.rkt b/typed-racket-test/unit-tests/parse-type-tests.rkt
index 5f4f2a400..27551b2c4 100644
--- a/typed-racket-test/unit-tests/parse-type-tests.rkt
+++ b/typed-racket-test/unit-tests/parse-type-tests.rkt
@@ -291,8 +291,10 @@
          #:msg "Index 2 used in"]
 
    [(Opaque foo?) (make-Opaque #'foo?)]
+   [(Type/Predicate foo?) (make-Type/Predicate #'foo?)]
    ;; PR 14122
    [FAIL (Opaque 3)]
+   [FAIL (Type/Predicate 3)]
 
    ;; struct types
    [(Struct-Type arity-at-least) (make-StructType (resolve -Arity-At-Least))]
diff --git a/typed-racket-test/unit-tests/subtype-tests.rkt b/typed-racket-test/unit-tests/subtype-tests.rkt
index f86d32137..f720204b7 100644
--- a/typed-racket-test/unit-tests/subtype-tests.rkt
+++ b/typed-racket-test/unit-tests/subtype-tests.rkt
@@ -148,6 +148,9 @@
    ;; Opaque
    [(make-Opaque x1) (make-Opaque x2)]
    [FAIL (make-Opaque #'a) (make-Opaque #'b)]
+   ;; Type/Predicate
+   [(make-Type/Predicate x1) (make-Type/Predicate x2)]
+   [FAIL (make-Type/Predicate #'a) (make-Type/Predicate #'b)]
    ;; Refinement
    [(make-Refinement A x1) (make-Refinement A x2)]
    ;[(make-Refinement t1a x1) (make-Refinement t1b x1)]
diff --git a/typed-racket-test/unit-tests/type-printer-tests.rkt b/typed-racket-test/unit-tests/type-printer-tests.rkt
index a0f17b6ae..0d52580f6 100644
--- a/typed-racket-test/unit-tests/type-printer-tests.rkt
+++ b/typed-racket-test/unit-tests/type-printer-tests.rkt
@@ -67,6 +67,7 @@
 
     (check-prints-as? -Custodian "Custodian")
     (check-prints-as? (make-Opaque #'integer?) "(Opaque integer?)")
+    (check-prints-as? (make-Type/Predicate #'integer?) "(Type/Predicate integer?)")
     (check-prints-as? (make-Immutable-Vector -Nat) "(Immutable-Vectorof Nonnegative-Integer)")
     (check-prints-as? (make-Mutable-Vector -Nat) "(Mutable-Vectorof Nonnegative-Integer)")
     (check-prints-as? (make-Vector -Nat) "(Vectorof Nonnegative-Integer)")