diff --git a/typed-racket-doc/info.rkt b/typed-racket-doc/info.rkt
index f3133346b..def0c24f7 100644
--- a/typed-racket-doc/info.rkt
+++ b/typed-racket-doc/info.rkt
@@ -27,7 +27,7 @@
 
 (define pkg-authors '(samth stamourv))
 
-(define version "1.15")
+(define version "1.16")
 
 (define license
   '(Apache-2.0 OR MIT))
diff --git a/typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl
index 4c986377f..22d2f3a8f 100644
--- a/typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl
+++ b/typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl
@@ -55,23 +55,27 @@ by logical propositions. These propositions can mention
 certain program terms, allowing a program's types to depend
 on the values of terms.
 
-@defform[#:literals (Refine : Top Bot ! and or when
+@defform[#:literals (Refine : Top Bot ! and or not when
                             unless if < <= = > >= car cdr
                             vector-length + *)
          (Refine [id : type] proposition)
          #:grammar
          ([proposition Top
            Bot
+           type
+           (! type)
            (: symbolic-object type)
            (! symbolic-object type)
            (and proposition ...)
            (or proposition ...)
+           (not proposition)
            (when proposition proposition)
            (unless proposition proposition)
            (if proposition proposition proposition)
            (linear-comp symbolic-object symbolic-object)]
           [linear-comp < <= = >= >]
           [symbolic-object exact-integer
+           (depth arg)
            symbolic-path
            (+ symbolic-object ...)
            (- symbolic-object ...)
@@ -80,7 +84,9 @@ on the values of terms.
            (path-elem symbolic-path)]
           [path-elem car
            cdr
-           vector-length])]{@racket[(Refine [v : t] p)] is a
+           vector-length]
+          [depth exact-nonnegative-integer]
+          [arg exact-nonnegative-integer])]{@racket[(Refine [v : t] p)] is a
  refinement of type @racket[t] with logical proposition
  @racket[p], or in other words it describes any value
  @racket[v] of type @racket[t] for which the logical
@@ -89,7 +95,12 @@ on the values of terms.
  @ex[(ann 42 (Refine [n : Integer] (= n 42)))]
 
  Note: The identifier in a refinement type is in scope
- inside the proposition, but not the type.
+ inside the proposition, but not the type. A bare @racket[type] proposition
+ is shorthand for @racket[(: id type)], and @racket[(! type)] is shorthand
+ for @racket[(! id type)]. The symbolic object @racket[(depth arg)] refers to
+ an argument of an enclosing function type (see @racket[->]); for the purpose
+ of counting @racket[depth], the refinement is itself a scope, but its
+ variable must be referred to by name.
 
 }
 
@@ -185,7 +196,21 @@ A function's range may depend on any of its arguments.
 The grammar of supported propositions and symbolic objects
 (i.e. @racket[prop] and @racket[obj]) is the same as
 the @racket[proposition] and @racket[symbolic-object] grammars
-from @racket[Refine]'s syntax.
+from @racket[Refine]'s syntax. A bare @racket[type] proposition is about the
+only argument in scope, if there is exactly one: for a precondition, the
+arguments in scope are those in its dependency list, and for the range, all of
+the function's arguments. Otherwise, write @racket[(: id type)] or
+@racket[(! id type)] to name the argument explicitly. A single-valued range
+may also be written with the @racket[result] syntax of @racket[->], as in
+@racket[(values (Boolean : #:+ (: x String)))]; propositions given there and
+after the range are combined.
+
+This form can express predicates over an outer argument in a curried function:
+
+@ex[#:label #f
+ (: double-num? (-> ([x : Any])
+                    (-> ([y : Any]) Boolean #:+ (: x Number))))
+ (define ((double-num? x) y) (number? x))]
 
 For example, here is a dependently typed version of
 Racket's @racket[vector-ref] which eliminates vector
diff --git a/typed-racket-doc/typed-racket/scribblings/reference/exploring-types.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/exploring-types.scrbl
index 68990e5a2..1c0caffd2 100644
--- a/typed-racket-doc/typed-racket/scribblings/reference/exploring-types.scrbl
+++ b/typed-racket-doc/typed-racket/scribblings/reference/exploring-types.scrbl
@@ -22,7 +22,7 @@ The following bindings are only available at the Typed Racket REPL.
   will remain unexpanded.
 
   If @racket[#:verbose] is provided, all type aliases are expanded
-  in the printed type.
+  in the printed type and latent propositions and objects are printed.
 
   @examples[#:eval the-top-eval
     ;; I'm not sure why, but the :type examples below don't work
@@ -33,14 +33,29 @@ The following bindings are only available at the Typed Racket REPL.
   ]
 }
 
-@defform[(:print-type e)]{Prints the type of @racket[_e], which must be
-an expression. This prints the whole
-type, which can sometimes be quite large.
+@defform[(:print-type maybe-verbose e)
+         #:grammar ([maybe-verbose (code:line)
+                                   (code:line #:verbose)])]{
+Prints the type of @racket[_e], which must be an expression. This prints the
+whole type, which can sometimes be quite large. If @racket[#:verbose] is
+provided, all type aliases are expanded in the printed type and latent
+propositions and objects are printed.
 
 @examples[#:eval the-top-eval
   (:print-type (+ 1 2))
   (:print-type map)
 ]
+
+When a type error message compares an expected type with the given one, it
+prints the latent propositions and objects of both whenever the expected type
+has some that would otherwise be omitted. To print them in every type that a
+module's error messages show, use the @racket[#:print-propositions] language
+option:
+
+@racketmod[typed/racket #:print-propositions]
+
+@history[#:changed "1.16" @elem{Added the @racket[#:verbose] option and the
+                                @racket[#:print-propositions] language option.}]
 }
 
 @defform[(:query-type/args f t ...)]{Given a function @racket[f] and argument
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 af51fd16d..aa2afd658 100644
--- a/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl
+++ b/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl
@@ -597,7 +597,15 @@ syntax will be disabled.}
 
 @defform[(ann e t)]{Ensure that @racket[e] has type @racket[t], or
 some subtype.  The entire expression has type @racket[t].
-This is legal only in expression contexts.}
+This is legal only in expression contexts.
+
+The type @racket[t] may also describe the propositions and object of
+@racket[e]'s result, using the @racket[result] syntax of function ranges (see
+@racket[->]), as in @racket[(Boolean : #:+ (: x String) #:- (! x String))].
+Outside a function type, such propositions must name their subjects
+explicitly.
+
+@history[#:changed "1.16" @elem{Added propositions and objects in @racket[t].}]}
 
 @defform/none[#{e :: t}]{A reader abbreviation for @racket[(ann e t)].
 
diff --git a/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
index 3dc85dd8d..7bb31cebf 100644
--- a/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
+++ b/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
@@ -646,7 +646,8 @@ delimited continuation functions and continuation mark functions.
 
 @section{Other Type Constructors}
 
-@deftypeconstr*/subs[#:id -> #:literals (|@| * ... ! and or implies car cdr)
+@deftypeconstr*/subs[#:id -> #:literals (* ... ! and or not when unless if
+                                             car cdr vector-length)
                      [(-> dom ... rng opt-proposition)
                       (-> dom ... rest * rng)
                       (-> dom ... rest ooo bound rng)
@@ -659,34 +660,49 @@ delimited continuation functions and continuation mark functions.
                            mandatory-kw
                            opt-kw]
                       [rng type
+                           result
                            (code:line (Some (a ...) type : #:+ proposition))
-                           (Values type ...)]
+                           (Values result ...)
+                           (values result ...)
+                           (AnyValues : proposition)]
+                      [result type
+                              (code:line type : latent-propositions)]
                       [mandatory-kw (code:line keyword type)]
                       [opt-kw [keyword type]]
                       [opt-proposition (code:line)
                                        (code:line : type)
-                                       (code:line : pos-proposition
-				                    neg-proposition
-				      	      object)]
+                                       (code:line : latent-propositions)]
+                      [latent-propositions type
+                                           (code:line pos-proposition
+                                                      neg-proposition
+                                                      object)]
                       [pos-proposition (code:line)
                                        (code:line #:+ proposition ...)]
                       [neg-proposition (code:line)
                                        (code:line #:- proposition ...)]
                       [object (code:line)
-                              (code:line #:object index)]
+                              (code:line #:object symbolic-object)
+                              (code:line #:object arg)]
                       [proposition Top
 		                   Bot
 			           type
                                    (! type)
-                                   (type |@| path-elem ... index)
-                                   (! type |@| path-elem ... index)
+                                   (: symbolic-object type)
+                                   (! symbolic-object type)
                                    (and proposition ...)
                                    (or proposition ...)
-                                   (implies proposition ...)]
-                      [path-elem car cdr]
-                      [index positive-integer
-                             (positive-integer positive-integer)
-                             identifier])]{
+                                   (not proposition)
+                                   (when proposition proposition)
+                                   (unless proposition proposition)
+                                   (if proposition proposition proposition)]
+                      [symbolic-object exact-integer
+                             (depth arg)
+                             identifier
+                             (car symbolic-object)
+                             (cdr symbolic-object)
+                             (vector-length symbolic-object)]
+                      [depth exact-nonnegative-integer]
+                      [arg exact-nonnegative-integer])]{
   The type of functions from the (possibly-empty)
   sequence @racket[dom ....] to the @racket[rng] type.
 
@@ -715,12 +731,12 @@ delimited continuation functions and continuation mark functions.
       (is-zero? 2 #:equality =)
       (is-zero? 2 #:equality eq? #:zero 2.0)]
 
-  When @racket[opt-proposition] is provided, it specifies the
-  @emph{proposition} for the function type (for an introduction to
+  When @racket[opt-proposition] is provided, it specifies latent
+  @emph{propositions} for the function type (for an introduction to
   propositions in Typed Racket, see
-  @tr-guide-secref["propositions-and-predicates"]).  For almost all use
-  cases, only the simplest form of propositions, with a single type after a
-  @racket[:], are necessary:
+  @tr-guide-secref["propositions-and-predicates"]). For almost all use
+  cases, only the simplest form of proposition, with a single type after a
+  @racket[:], is necessary:
 
   @ex[string?]
 
@@ -730,9 +746,13 @@ delimited continuation functions and continuation mark functions.
   expression evaluates to @racket[#f] in a branch, the variable
   @emph{does not} have type @racket[String].
 
-  In some cases, asymmetric type information is useful in the
-  propositions. For example, the @racket[filter] function's first
-  argument is specified with only a positive proposition:
+  The shorthand @racket[(-> Any Boolean : String)] is equivalent to a
+  positive proposition that the argument has type @racket[String] and a
+  negative proposition that the argument does not have type @racket[String].
+
+  In some cases, asymmetric type information is useful. For example, the
+  @racket[filter] function's first argument is specified with only a
+  positive proposition:
 
   @ex[filter]
 
@@ -741,10 +761,52 @@ delimited continuation functions and continuation mark functions.
   the type-checker gains no information in branches in which the result is @racket[#f].
 
   Conversely, @racket[#:-] specifies that a function provides information for the
-  false branch of a conditional.
+  false branch of a conditional. In the propositions of a function's range, a
+  bare @racket[type] proposition is about the function's first argument, and
+  @racket[(! type)] is its negation; a function with no arguments must name the
+  subject of its propositions explicitly:
+
+  @racketblock[(-> Any Boolean : #:+ Number)]
+
+  Use @racket[(: symbolic-object type)] and @racket[(! symbolic-object type)]
+  when the proposition must name a subject explicitly. The symbolic object
+  @racket[(depth arg)] refers to argument @racket[arg] (counting from 0) of an
+  enclosing function type: @racket[(0 0)] is the first argument of the function
+  type whose range contains the proposition, and @racket[(1 0)] is the first
+  argument of the function type whose range contains that function type, as in
+  this curried predicate:
+
+  @racketblock[(-> Any (-> Any Boolean : #:+ (: (1 0) Number)))]
+
+  Only ranges are inside a function type's scope, so a function type that
+  appears as an argument type cannot refer to the arguments of the function
+  that takes it. A @racket[Refine] type's proposition is also inside a scope,
+  so @racket[(1 0)] in the proposition of a @racket[Refine] in a function's
+  range refers to the function's first argument; refer to the refinement's own
+  variable by name. Paths such as @racket[(car (0 0))] are allowed when the
+  argument's type is a pair.
+
+  An identifier symbolic object refers to an immutable variable in scope at the
+  type annotation. The @racket[#:object] form specifies which symbolic object is
+  produced as the result of the function:
+
+  @racketblock[(let ([z : Any 1])
+                 (ann (lambda ([x : Any]) z)
+                      (Any -> Any : #:object z)))]
+
+  As in older code, @racket[#:object arg] with a natural number @racket[arg]
+  refers to the function's argument @racket[arg], i.e. @racket[(0 arg)], rather
+  than to the constant @racket[arg].
 
   The other proposition cases are rarely needed, but the grammar documents them
   for completeness. They correspond to logical operations on the propositions.
+  Older code may use compatibility forms such as
+  @tt{(Number }@racketidfont["@"]@tt{ 0)},
+  @tt{(! Number }@racketidfont["@"]@tt{ car 0)}, and
+  @tt{(Number }@racketidfont["@"]@tt{ 1 0)} for type propositions about
+  arguments, possibly inside the other proposition forms; new code should
+  prefer @racket[(: (0 0) Number)], @racket[(! (car (0 0)) Number)], and
+  @racket[(: (1 0) Number)].
 
   The type of functions can also be specified with an @emph{infix} @racket[->]
   which comes immediately before the @racket[rng] type. The fourth through
@@ -759,10 +821,17 @@ delimited continuation functions and continuation mark functions.
 
   @racket[(Some (a ...) type : #:+ proposition)] for @racket[rng] specifies an
   @deftech[#:key "Some"]{existential type result}, where the type variables @racket[a ...] may appear
-  in @racket[type] and @racket[opt-proposition]. Unpacking the existential type
+  in @racket[type] and @racket[proposition]. Unpacking the existential type
   result is done automatically while checking application of the function.
 
-  @history[#:changed "1.12" @elem{Added @tech[#:key "Some"]{existential type results}}]
+  @history[#:changed "1.12" @elem{Added @tech[#:key "Some"]{existential type results}}
+           #:changed "1.16" @elem{Added the @racket[(: symbolic-object type)],
+                                  @racket[(! symbolic-object type)], @racket[not],
+                                  @racket[when], @racket[unless], and @racket[if]
+                                  propositions, the @racket[(depth arg)] symbolic
+                                  object, and propositions in @racket[Values]
+                                  results and @racket[AnyValues]; the
+                                  @racket[#:object] form is no longer ignored.}]
 }
 
 @;; This is a trick to get a reference to ->* in another manual
@@ -829,8 +898,8 @@ delimited continuation functions and continuation mark functions.
 @deftogether[(
 @deftype[Top]
 @deftype[Bot])]{ These are propositions that can be used with @racket[->].
-  @racket[Top] is the propositions with no information.
-  @racket[Bot] is the propositions which means the result cannot happen.
+  @racket[Top] is the proposition with no information.
+  @racket[Bot] is the proposition which means the result cannot happen.
 }
 
 
@@ -892,7 +961,11 @@ delimited continuation functions and continuation mark functions.
 Returns the type of a sequence of multiple values, with
 types @racket[t ...].  This can only appear as the return type of a
 function.
-@ex[(values 1 2 3)]}
+Each result may also include latent propositions and an object using the same
+@racket[(type : #:+ proposition #:- proposition #:object symbolic-object)]
+syntax as function ranges.
+@ex[(values 1 2 3)]
+@history[#:changed "1.16" @elem{Added latent propositions and objects in results.}]}
 Note that a type variable cannot be instantiated with a @racket[(Values ....)]
 type. For example, the type @racket[(All (A) (-> A))] describes a thunk that
 returns exactly one value.
diff --git a/typed-racket-lib/info.rkt b/typed-racket-lib/info.rkt
index 563944a83..1e53cced6 100644
--- a/typed-racket-lib/info.rkt
+++ b/typed-racket-lib/info.rkt
@@ -12,7 +12,7 @@
 
 (define pkg-authors '(samth stamourv))
 
-(define version "1.15")
+(define version "1.16")
 
 (define license
   '(Apache-2.0 OR MIT))
diff --git a/typed-racket-lib/typed-racket/HISTORY.txt b/typed-racket-lib/typed-racket/HISTORY.txt
index 2c6b078a6..aae3fd3b7 100644
--- a/typed-racket-lib/typed-racket/HISTORY.txt
+++ b/typed-racket-lib/typed-racket/HISTORY.txt
@@ -1,3 +1,21 @@
+9.4
+- Fix unsound erasure of propositions about variables that go out of
+  scope or are substituted away. Propositions in negative positions
+  (function domains), and types whose invariant parameters mention
+  such variables, are now handled soundly, which may cause existing
+  programs not to type check.
+- Fix unsound elimination of type variables during inference for types
+  with invariant parameters, such as `Boxof` and mutable hash tables, and
+  for function types whose propositions mention the variables.
+- Ordinary function types accept the same propositions as dependent
+  function types and `Refine`, such as `(: (0 1) String)`, along with
+  the legacy `@` forms at any depth. `#:object` is no longer ignored.
+- Results in `Values` ranges and in `ann` may have latent propositions
+  and objects.
+- Types print propositions in the syntax that parses them, and type
+  error messages show propositions when they explain a mismatch.
+- Add `:print-type #:verbose` and the `#:print-propositions` language
+  option.
 9.3
 - Bug fixes.
 9.2
diff --git a/typed-racket-lib/typed-racket/base-env/top-interaction.rkt b/typed-racket-lib/typed-racket/base-env/top-interaction.rkt
index 5dbbf3830..cb0f01cf2 100644
--- a/typed-racket-lib/typed-racket/base-env/top-interaction.rkt
+++ b/typed-racket-lib/typed-racket/base-env/top-interaction.rkt
@@ -58,19 +58,28 @@
   (provide
     :type-impl :print-type-impl :query-type/args-impl :query-type/result-impl :kind-impl)
 
+  (define (with-type-printing verbose? type-form? thunk)
+    (parameterize ([current-print-type-fuel
+                    (cond
+                      [verbose? +inf.0]
+                      [type-form? 1]
+                      [else (current-print-type-fuel)])]
+                   ;; This makes sure unions are totally flat for the
+                   ;; infinite fuel case. If fuel that's not 0, 1, or +inf.0
+                   ;; is ever used, more may need to be done.
+                   [current-type-names
+                    (if verbose? '() (current-type-names))]
+                   [current-print-unexpanded (box '())]
+                   [print-complex-props? (or verbose? (print-complex-props?))])
+      (thunk)))
+
   ;; this one doesn't quite fit the pattern of the next three REPL operations, so
   ;; this one isn't defined with a macro as below
   (define (:type-impl stx)
     (syntax-parse stx
       [(_ (~optional (~and #:verbose verbose-kw)) ty:expr)
-       (parameterize ([current-print-type-fuel
-                       (if (attribute verbose-kw) +inf.0 1)]
-                      ;; This makes sure unions are totally flat for the
-                      ;; infinite fuel case. If fuel that's not 0, 1, or +inf.0
-                      ;; is ever used, more may need to be done.
-                      [current-type-names
-                       (if (attribute verbose-kw) '() (current-type-names))]
-                      [current-print-unexpanded (box '())])
+       (with-type-printing (attribute verbose-kw) #t
+        (λ ()
          (define type (pretty-format-rep (match (parse-type #'ty)
                                            [(? App? ty) (resolve ty)]
                                            [ty ty])))
@@ -80,7 +89,7 @@
                          ""
                          (format "[can expand further: ~a]"
                                  (string-join (map ~a unexpanded)))))
-         #`(display #,(format "~a\n~a" type cue)))]
+         #`(display #,(format "~a\n~a" type cue))))]
       [form
        (raise-syntax-error #f "must be applied to exactly one argument" #'form)]))
 
@@ -103,18 +112,22 @@
              [form
               (raise-syntax-error #f err #'form)]))]))
 
-  ;; TODO what should be done with stx
-  ;; Prints the _entire_ type. May be quite large.
-  (define-repl-op :print-type-impl (_ e) #'e
-    (λ (type)
-      #`(displayln
-         #,(pretty-format-rep
-            (match type
-              [(tc-result1: t f o) t]
-              [(tc-results: (list (tc-result: ts) ...) _)
-               (-values ts)]
-              [(tc-any-results: f) (-AnyValues f)]))))
-    "must be applied to exactly one argument")
+  (define (:print-type-impl stx)
+    (syntax-parse stx
+      [(_ (~optional (~and #:verbose verbose-kw)) e:expr)
+       (define result
+         (tc-expr (local-expand #'e 'expression (list #'module*))))
+       (with-type-printing (attribute verbose-kw) #f
+        (λ ()
+          #`(displayln
+             #,(pretty-format-rep
+                (match result
+                  [(tc-result1: t f o) t]
+                  [(tc-results: (list (tc-result: ts) ...) _)
+                   (-values ts)]
+                  [(tc-any-results: f) (-AnyValues f)])))))]
+      [form
+       (raise-syntax-error #f "must be applied to exactly one argument" #'form)]))
 
   ;; given a function and input types, display the result type
   (define-repl-op :query-type/args-impl (_ op arg-type ...)
diff --git a/typed-racket-lib/typed-racket/core.rkt b/typed-racket-lib/typed-racket/core.rkt
index 9e2369137..ea38da960 100644
--- a/typed-racket-lib/typed-racket/core.rkt
+++ b/typed-racket-lib/typed-racket/core.rkt
@@ -9,6 +9,7 @@
          racket/match racket/syntax
          syntax/flatten-begin
          "types/utils.rkt"
+         "types/printer.rkt"
          "types/abbrev.rkt"
          "types/generalize.rkt"
          "typecheck/provide-handling.rkt"
@@ -36,6 +37,8 @@
                     (~and #:no-optimize (~bind [opt? #'#f]))))
               (~optional
                (~and #:with-refinements refinement-reasoning?))
+              (~optional
+               (~and #:print-propositions print-propositions?))
               (~optional
                (~and #:no-delay-errors no-delay-errors?)))
          ...
@@ -51,7 +54,9 @@
                                               (unless (eq? te-mode deep)
                                                 (raise-arguments-error
                                                  (format-symbol "typed/racket/~a" te-attr)
-                                                 "#:with-refinements unsupported")))])
+                                                 "#:with-refinements unsupported")))]
+                      [print-complex-props? (or (attribute print-propositions?)
+                                                (print-complex-props?))])
          (tc-module/full te-mode stx pmb-form
           (λ (new-mod pre-before-code pre-after-code)
             (define ctc-cache (make-hash))
@@ -116,4 +121,3 @@
     ((#:shallow) shallow)
     ((#:optional) optional)
     (else (error (format "Internal Typed Racket Error: unknown type enforcement mode ~s~n" stx)))))
-
diff --git a/typed-racket-lib/typed-racket/infer/promote-demote.rkt b/typed-racket-lib/typed-racket/infer/promote-demote.rkt
index 04af72941..2a6cb4784 100644
--- a/typed-racket-lib/typed-racket/infer/promote-demote.rkt
+++ b/typed-racket-lib/typed-racket/infer/promote-demote.rkt
@@ -3,10 +3,12 @@
 (require "../utils/utils.rkt"
          "../rep/type-rep.rkt"
          "../rep/values-rep.rkt"
+         "../rep/prop-rep.rkt"
          "../rep/rep-utils.rkt"
          "../rep/free-variance.rkt"
          "../types/abbrev.rkt"
          "../types/utils.rkt"
+         "../types/variance.rkt"
          (prefix-in c: (contract-req))
          racket/list racket/match)
 (provide/cond-contract
@@ -17,62 +19,64 @@
   (for/or ([e (in-list (append-map fv ts))])
     (memq e V)))
 
-;; get-propset : SomeValues -> PropSet
-;; extract prop sets out of the range of a function type
-(define (get-propsets rng)
-  (match rng
-    [(AnyValues: p) (list (-PS p p))]
-    [(Values: (list (Result: _ propsets _) ...)) propsets]
-    [(ValuesDots: (list (Result: _ propsets _) ...) _ _) propsets]))
-
-
+;; var-promote : Type (Listof Symbol) -> Type
+;; var-demote : Type (Listof Symbol) -> Type
+;; The least supertype (greatest subtype) of T that does not mention the
+;; type variables V, as in Pierce and Turner's "Local Type Inference".
+;; Variables are replaced by Univ or Bottom according to the variance of
+;; their position. A type that mentions V in an invariant position has no
+;; such supertype (subtype) of the same shape, so it is replaced as a
+;; whole by its top type (Bottom); replacing just the variable, say from
+;; (Boxof X) to (Boxof Any), would give an unrelated type.
 (define (var-promote T V)
   (var-change V T #t))
 (define (var-demote T V)
   (var-change V T #f))
 
-
-
 (define (var-change V cur change)
   (define (co t) (var-change V t change))
   (define (contra t) (var-change V t (not change)))
-  ;; arr? -> (or/c #f arr?)
-  ;; Returns the changed arr or #f if there is no arr above it
-  (define (arr-change arr)
-    (match-define (Arrow: dom rst kws rng rng-T+) arr)
-    (cond
-      [(apply V-in? V (get-propsets rng)) #f]
-      [(and (RestDots? rst) (memq (RestDots-nm rst) V))
-       (make-Arrow (map contra dom) (contra (RestDots-ty rst)) (map contra kws) (co rng) rng-T+)]
-      [else (make-Arrow (map contra dom) (and rst (contra rst)) (map contra kws) (co rng) rng-T+)]))
-  (define (change-elems ts)
-    (for/list ([t (in-list ts)])
-      (if (V-in? V t)
-        (if change Univ -Bottom)
-        t)))
+  (define (mentions-V? t) (V-in? V t))
+  ;; the replacement for all of `cur`, which mentions V invariantly
+  (define (give-up) (if change (top-of cur) -Bottom))
+  ;; changes the parts of `cur` with the given variances
+  (define (change-parts mk parts variances)
+    (if (for/or ([t (in-list parts)]
+                 [v (in-list variances)])
+          (and (not (or (variance:co? v) (variance:contra? v) (variance:const? v)))
+               (mentions-V? t)))
+        (give-up)
+        (apply mk (for/list ([t (in-list parts)]
+                             [v (in-list variances)])
+                    (cond
+                      [(variance:contra? v) (contra t)]
+                      [(variance:co? v) (co t)]
+                      [else t])))))
   (match cur
-    [(app Rep-variances variances) #:when variances 
-     (define mk (Rep-constructor cur))
-     (apply mk (for/list ([t (in-list (Rep-values cur))]
-                          [v (in-list variances)])
-                 (match v
-                   [(? variance:co?) (co t)]
-                   [(? variance:inv?)
-                    (if (V-in? V t)
-                        (if change Univ -Bottom)
-                        t)]
-                   [(? variance:contra?) (contra t)])))]
-    [(Unit: imports exports init-depends t)
-     (make-Unit (map co imports)
-                (map contra imports)
-                (map co init-depends)
-                (co t))]
     [(F: name) (if (memq name V)
                    (if change Univ -Bottom)
                    cur)]
-    [(Fun: arrs) (make-Fun (filter-map arr-change arrs))]
-    [(Immutable-HeterogeneousVector: elems)
-     (make-Immutable-HeterogeneousVector (change-elems elems))]
-    [(Mutable-HeterogeneousVector: elems)
-     (make-Mutable-HeterogeneousVector (change-elems elems))]
+    ;; the domain is contravariant; propositions in the range that
+    ;; mention V are weakened (when promoting) or strengthened (when
+    ;; demoting) like any other type in the range
+    [(Arrow: dom rst kws rng rng-T+)
+     (make-Arrow (map contra dom)
+                 (if (and (RestDots? rst) (memq (RestDots-nm rst) V))
+                     (contra (RestDots-ty rst))
+                     (and rst (contra rst)))
+                 (map contra kws)
+                 (co rng)
+                 rng-T+)]
+    [(DepFun: dom pre rng)
+     (make-DepFun (map contra dom) (contra pre) (co rng))]
+    ;; the type in a NotTypeProp is underneath a negation
+    [(NotTypeProp: obj t) (-not-type obj (contra t))]
+    [(app Rep-variances (? pair? variances))
+     (change-parts (Rep-constructor cur) (Rep-values cur) variances)]
+    [(App: rator rands)
+     (change-parts (λ rands (make-App rator rands))
+                   rands
+                   (or (app-variances rator rands)
+                       (map (λ (_) variance:inv) rands)))]
+    [(? invariant-type?) (if (mentions-V? cur) (give-up) cur)]
     [_ (Rep-fmap cur co)]))
diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt
index 73f575480..471ffcc81 100644
--- a/typed-racket-lib/typed-racket/private/parse-type.rkt
+++ b/typed-racket-lib/typed-racket/private/parse-type.rkt
@@ -111,16 +111,76 @@
      => cdr]
     [else #f]))
 
-;; current-arities : Parameter<(Listof Natural)>
-;; Represents the stack of function arities in the potentially
-;; nested function type being parsed. The stack does not include the
-;; innermost function (since syntax classes can check that locally)
-(define current-arities (make-parameter null))
-
-(define-syntax-rule (with-arity arity e ...)
-  (parameterize ([current-arities (cons arity (current-arities))])
+;; A Binder is one of
+;;  - (binder (Listof (U Type #f)) (U Object #f)): a function type whose
+;;    range (or latent propositions) is being parsed, with the types of
+;;    its arguments (#f where unknown) and the default subject of bare
+;;    type propositions, if any
+;;  - 'refinement: the proposition of a Refine type
+;;  - 'opaque: the argument types of a dependent function, which may or
+;;    may not end up underneath the function's binder
+(struct binder (arg-types default-subject) #:transparent)
+
+;; current-binders : Parameter<(Listof Binder)>
+;; The binders enclosing the position being parsed, innermost first.
+;; These are exactly the binders that increase the De Bruijn level of
+;; objects (see instantiate-obj+simplify), so the object (depth idx)
+;; refers to argument idx of the binder at position depth.
+(define current-binders (make-parameter null))
+
+(define-syntax-rule (with-binder b e ...)
+  (parameterize ([current-binders (cons b (current-binders))])
     e ...))
 
+;; with-function-binder : (Listof Type) e ... -> Any
+;; parses e ... underneath a function type with the given argument types,
+;; whose first argument is the default subject of bare type propositions
+(define-syntax-rule (with-function-binder arg-types e ...)
+  (let ([tys arg-types])
+    (with-binder (binder tys (and (pair? tys) (-arg-path 0)))
+      e ...)))
+
+;; the default subject of a bare type proposition at the current position
+(define (current-default-subject)
+  (match (current-binders)
+    [(cons (binder _ default) _) default]
+    [_ #f]))
+
+;; check-index-object : natural natural -> (U String #f)
+;; Returns an error message if (depth idx) does not refer to an argument
+;; of an enclosing function type
+(define (check-index-object depth idx)
+  (define binders (current-binders))
+  (cond
+    [(for/or ([b (in-list binders)] [_ (in-range (add1 depth))])
+       (eq? b 'opaque))
+     "index objects may not be used in the argument types of a dependent function; refer to arguments by name"]
+    [(>= depth (length binders))
+     (format "index (~a ~a) used in a proposition, but the use is only within ~a enclosing function type~a"
+             depth idx (length binders) (if (= 1 (length binders)) "" "s"))]
+    [else
+     (match (list-ref binders depth)
+       ['refinement
+        (format "index (~a ~a) refers to the variable of a Refine type; refer to it by name"
+                depth idx)]
+       [(binder tys _)
+        (and (>= idx (length tys))
+             (format "index (~a ~a) refers to argument ~a, but the function type has only ~a argument~a"
+                     depth idx idx (length tys) (if (= 1 (length tys)) "" "s")))])]))
+
+;; lookup-symbolic-obj-type : Object -> Type
+;; the type of the value an object denotes, including objects that refer
+;; to arguments of enclosing function types
+(define (lookup-symbolic-obj-type obj)
+  (match obj
+    [(Path: flds (cons depth idx))
+     (define ty
+       (match (list-ref (current-binders) depth)
+         [(binder tys _) (or (list-ref tys idx) Univ)]
+         [_ Univ]))
+     (or (path-type flds ty) Univ)]
+    [_ (lookup-obj-type/lexical obj)]))
+
 
 (define-literal-syntax-class #:for-label car)
 (define-literal-syntax-class #:for-label cdr)
@@ -349,9 +409,12 @@
            #:attr type (do-parse #'t)
            #:attr path '()))
 
-(define (parse-prop stx do-parse mode)
+;; parse-prop : Syntax (Syntax -> Type) Mode (U Object #f) -> Prop
+;; parses a proposition; a bare type `t` stands for (: default-subject t)
+(define (parse-prop stx do-parse mode [default-subject (current-default-subject)])
   (syntax-parse stx
-    [(~var p (proposition do-parse mode)) (attribute p.val)]))
+    [(~var p (proposition do-parse mode default-subject))
+     (attribute p.val)]))
 
 (define int-comps (list (cons '<= -leq)
                         (cons '< -lt)
@@ -359,35 +422,52 @@
                         (cons '> -gt)
                         (cons '= -eq)))
 
-(define-syntax-class (proposition do-parse mode)
+(define-syntax-class (proposition do-parse mode default-subject)
   #:description "proposition"
   #:attributes (val)
   (pattern :Top^ #:attr val -tt)
   (pattern :Bot^ #:attr val -ff)
-  (pattern (:colon^ (~var o (symbolic-object mode)) t:expr)
+  ;; legacy syntax, e.g. (Number @ 0), (! Number @ car 1 0), (Number @ x)
+  (pattern (t:expr :@ ~! pe:legacy-path-elem ... o:legacy-prop-obj)
+           #:attr val (-is-type (-acc-path (attribute pe.val) (attribute o.obj))
+                                (do-parse #'t)))
+  (pattern (:! t:expr :@ ~! pe:legacy-path-elem ... o:legacy-prop-obj)
+           #:attr val (-not-type (-acc-path (attribute pe.val) (attribute o.obj))
+                                 (do-parse #'t)))
+  (pattern (:colon^ ~! (~var o (symbolic-object mode)) t:expr)
            #:attr val (-is-type (attribute o.val) (do-parse #'t)))
-  (pattern (:! (~var o (symbolic-object mode)) t:expr)
+  (pattern (~and (_ _ _) (:! ~! (~var o (symbolic-object mode)) t:expr))
            #:attr val (-not-type (attribute o.val) (do-parse #'t)))
-  (pattern (:and^ (~var p (proposition do-parse mode)) ...)
+  (pattern (:! ~! t:expr)
+           #:fail-unless default-subject
+           "a proposition of the form (! type) needs a default subject; use (! object type)"
+           #:attr val (-not-type default-subject (do-parse #'t)))
+  (pattern (:and^ ~! (~var p (proposition do-parse mode default-subject)) ...)
            #:attr val (apply -and (attribute p.val)))
-  (pattern (:or^ (~var p (proposition do-parse mode)) ...)
+  (pattern (:or^ ~! (~var p (proposition do-parse mode default-subject)) ...)
            #:attr val (apply -or (attribute p.val)))
-  (pattern (:unless^ (~var p1 (proposition do-parse mode)) (~var p2 (proposition do-parse mode)))
+  (pattern (:unless^ ~!
+                     (~var p1 (proposition do-parse mode default-subject))
+                     (~var p2 (proposition do-parse mode default-subject)))
            #:attr val (-or (attribute p1.val) (attribute p2.val)))
-  (pattern (:when^ (~var p1 (proposition do-parse mode)) (~var p2 (proposition do-parse mode)))
+  (pattern (:when^ ~!
+                   (~var p1 (proposition do-parse mode default-subject))
+                   (~var p2 (proposition do-parse mode default-subject)))
            #:attr val (-or (negate-prop (attribute p1.val))
                            (-and (attribute p1.val) (attribute p2.val))))
-  (pattern (:if^ (~var p1 (proposition do-parse mode))
-                 (~var p2 (proposition do-parse mode))
-                 (~var p3 (proposition do-parse mode)))
+  (pattern (:if^ ~!
+                 (~var p1 (proposition do-parse mode default-subject))
+                 (~var p2 (proposition do-parse mode default-subject))
+                 (~var p3 (proposition do-parse mode default-subject)))
            #:attr val (let ([tst (attribute p1.val)]
                             [thn (attribute p2.val)]
                             [els (attribute p3.val)])
                         (-or (-and tst thn)
                              (-and (negate-prop tst) els))))
-  (pattern (:not^ (~var p (proposition do-parse mode)))
+  (pattern (:not^ ~! (~var p (proposition do-parse mode default-subject)))
            #:attr val (negate-prop (attribute p.val)))
   (pattern ((~and comp (~or :<=^ :<^ :>=^ :>^ :=^))
+            ~!
             (~var obj0 (inequality-symbolic-object mode))
             (~var obj1 (inequality-symbolic-object mode))
             (~var objs (inequality-symbolic-object mode))
@@ -403,15 +483,19 @@
                   (loop (cons (mk lhs rhs) ps)
                         rhs
                         os)]
-                 [_ (apply -and ps)])))))
-
+                 [_ (apply -and ps)]))))
+  ;; a bare type is a proposition about the default subject
+  (pattern t:expr
+           #:fail-unless default-subject
+           "a type used as a proposition needs a default subject; use (: object type)"
+           #:attr val (-is-type default-subject (do-parse #'t))))
 
 (define-syntax-class (inequality-symbolic-object mode)
   #:description "symbolic object in an inequality"
   #:attributes (val)
   (pattern (~var o (symbolic-object mode))
            #:do [(define obj (attribute o.val))
-                 (define obj-ty (lookup-obj-type/lexical obj))]
+                 (define obj-ty (lookup-symbolic-obj-type obj))]
            #:fail-when (and (not (side-effect-mode? mode))
                             (not (subtype obj-ty -Int)))
            (format "terms in linear constraints must be integers, got ~a for ~a"
@@ -440,6 +524,11 @@
 (define-syntax-class (symbolic-object-w/o-lexp mode)
   #:description "symbolic object"
   #:attributes (val)
+  ;; argument idx of the enclosing function type depth binders out
+  (pattern (depth:nat idx:nat)
+           #:do [(define msg (check-index-object (syntax-e #'depth) (syntax-e #'idx)))]
+           #:fail-when msg msg
+           #:attr val (-arg-path (syntax-e #'idx) (syntax-e #'depth)))
   (pattern i:id
            #:fail-unless (or (identifier-binding #'i)
                              (local-term-id #'i))
@@ -451,7 +540,7 @@
                         [local-id (lookup-alias/lexical local-id)]))
   (pattern (:car^ ~! (~var o (symbolic-object-w/o-lexp mode)))
            #:do [(define obj (attribute o.val))
-                 (define obj-ty (lookup-obj-type/lexical obj))]
+                 (define obj-ty (lookup-symbolic-obj-type obj))]
            #:fail-when (and (not (side-effect-mode? mode))
                             (not (subtype obj-ty (-pair Univ Univ))))
            (format "car expects a pair, but got ~a for ~a"
@@ -459,7 +548,7 @@
            #:attr val (-car-of (attribute o.val)))
   (pattern (:cdr^ ~! (~var o (symbolic-object-w/o-lexp mode)))
            #:do [(define obj (attribute o.val))
-                 (define obj-ty (lookup-obj-type/lexical obj))]
+                 (define obj-ty (lookup-symbolic-obj-type obj))]
            #:fail-when (and (not (side-effect-mode? mode))
                             (not (subtype obj-ty (-pair Univ Univ))))
            (format "cdr expects a pair, but got ~a for ~a"
@@ -467,7 +556,7 @@
            #:attr val (-cdr-of (attribute o.val)))
   (pattern (:vector-length^ ~! (~var o (symbolic-object-w/o-lexp mode)))
            #:do [(define obj (attribute o.val))
-                 (define obj-ty (lookup-obj-type/lexical obj))]
+                 (define obj-ty (lookup-symbolic-obj-type obj))]
            #:fail-when (and (not (side-effect-mode? mode))
                             (not (subtype obj-ty -VectorTop)))
            (format "vector-length expects a vector, but got ~a for ~a"
@@ -487,7 +576,7 @@
            #:attr val (-lexp (list (syntax->datum #'coeff) (attribute l.val))))
   (pattern (~var o (symbolic-object-w/o-lexp mode))
            #:do [(define obj (attribute o.val))
-                 (define obj-ty (lookup-obj-type/lexical obj))]
+                 (define obj-ty (lookup-symbolic-obj-type obj))]
            #:fail-when (and (not (side-effect-mode? mode))
                             (not (subtype obj-ty -Int)))
            (format "terms in linear expressions must be integers, got ~a for ~a"
@@ -508,30 +597,8 @@
               (scale-obj -1 term)))]))
 
 
-;; old + deprecated
-(define-syntax-class (legacy-prop doms do-parse)
-  #:description "proposition"
-  #:attributes (prop)
-  (pattern :Top^ #:attr prop -tt)
-  (pattern :Bot^ #:attr prop -ff)
-  ;; Here is wrong check
-  (pattern (t:expr :@ ~! pe:legacy-path-elem ... (~var o (legacy-prop-obj doms)))
-           #:attr prop (-is-type (-acc-path (attribute pe.val) (attribute o.obj)) (do-parse #'t)))
-  ;; Here is wrong check
-  (pattern (:! t:expr :@ ~! pe:legacy-path-elem ... (~var o (legacy-prop-obj doms)))
-           #:attr prop (-not-type (-acc-path (attribute pe.val) (attribute o.obj)) (do-parse #'t)))
-  (pattern (:! t:expr)
-           #:attr prop (-not-type 0 (do-parse #'t)))
-  (pattern ((~datum and) (~var p (legacy-prop doms do-parse)) ...)
-           #:attr prop (apply -and (attribute p.prop)))
-  (pattern ((~datum or) (~var p (legacy-prop doms do-parse)) ...)
-           #:attr prop (apply -or (attribute p.prop)))
-  (pattern ((~literal implies) (~var p1 (legacy-prop doms do-parse)) (~var p2 (legacy-prop doms do-parse)))
-           #:attr prop (-or (negate-prop (attribute p1.prop)) (attribute p2.prop)))
-  (pattern t:expr
-           #:attr prop (-is-type 0 (do-parse #'t))))
-
-(define-splicing-syntax-class (legacy-prop-obj doms)
+;; the object of a legacy proposition such as (Number @ 1 0)
+(define-splicing-syntax-class legacy-prop-obj
   #:description "prop object"
   #:attributes (obj)
   (pattern i:id
@@ -540,32 +607,13 @@
            #:fail-when (is-var-mutated? #'i)
            "Propositions for predicates may not reference identifiers that are mutated"
            #:attr obj (-id-path #'i))
-  (pattern idx:nat
-           #:do [(define arg (syntax-e #'idx))]
-           #:fail-unless (< arg (length doms))
-           (format "Proposition's object index ~a is larger than argument length ~a"
-                   arg (length doms))
-           #:attr obj (-arg-path arg 0))
-  (pattern (~seq depth-idx:nat idx:nat)
-           #:do [(define arg (syntax-e #'idx))
-                 (define depth (syntax-e #'depth-idx))]
-           #:fail-unless (<= depth (length (current-arities)))
-           (format "Index ~a used in a proposition, but the use is only within ~a enclosing functions"
-                   depth (length (current-arities)))
-           #:do [(define actual-arg
-                   (if (zero? depth)
-                       (length doms)
-                       (list-ref (current-arities) (sub1 depth))))]
-           #:fail-unless (< arg actual-arg)
-           (format "Proposition's object index ~a is larger than argument length ~a"
-                   depth actual-arg)
-           #:attr obj (-arg-path arg (syntax-e #'depth-idx))))
-
-
-(define-syntax-class legacy-object
-  #:attributes (object)
-  (pattern e:expr
-           #:attr object -empty-obj))
+  (pattern (~or* (~seq depth:nat idx:nat)
+                 (depth:nat idx:nat)
+                 (~seq idx:nat (~peek-not _) (~bind [depth #'0])))
+           #:do [(define msg (check-index-object (syntax-e #'depth) (syntax-e #'idx)))]
+           #:fail-when msg msg
+           #:attr obj (-arg-path (syntax-e #'idx) (syntax-e #'depth))))
+
 
 (define-syntax-class self
   #:attributes (type)
@@ -573,11 +621,11 @@
            #:attr type -Self))
 
 (define-syntax-class existential-type-result
-  #:attributes (vars t prop-type)
+  #:attributes (vars t prop-stx)
   (pattern (:Some^ (x:id ...) t)
-           #:attr prop-type #f
+           #:attr prop-stx #f
            #:attr vars (syntax->list #'(x ...)))
-  (pattern (:Some^ (x:id ...) t :colon^ #:+ prop-type:expr)
+  (pattern (:Some^ (x:id ...) t :colon^ #:+ prop-stx:expr)
            #:attr vars (syntax->list #'(x ...))))
 
 (define-splicing-syntax-class sp-arg
@@ -589,14 +637,35 @@
            #:attr type #'i
            #:attr pred? #'p))
 
-(define-splicing-syntax-class (legacy-full-latent doms do-parse)
+(define-splicing-syntax-class latent-stxes
   #:description "latent propositions and object"
-  (pattern (~seq (~optional (~seq #:+ (~var p+ (legacy-prop doms do-parse)) ...+) #:defaults ([(p+.prop 1) null]))
-                 (~optional (~seq #:- (~var p- (legacy-prop doms do-parse)) ...+) #:defaults ([(p-.prop 1) null]))
-                 (~optional (~seq #:object o:legacy-object)))
-           #:attr positive (apply -and (attribute p+.prop))
-           #:attr negative (apply -and (attribute p-.prop))
-           #:attr object (or (attribute o.object) -empty-obj)))
+  #:attributes ((p+ 1) (p- 1) object-stx)
+  (pattern (~seq (~optional (~seq #:+ p+:expr ...+) #:defaults ([(p+ 1) null]))
+                 (~optional (~seq #:- p-:expr ...+) #:defaults ([(p- 1) null]))
+                 (~optional (~seq #:object o:expr)))
+           #:attr object-stx (attribute o)))
+
+;; parses the latent propositions of a function range at the current
+;; position, which is underneath the function's binder
+(define (latent-stxes->propset p+ p- do-parse mode)
+  (-PS (apply -and
+              (for/list ([p-stx (in-list p+)])
+                (parse-prop p-stx do-parse mode)))
+       (apply -and
+              (for/list ([p-stx (in-list p-)])
+                (parse-prop p-stx do-parse mode)))))
+
+;; parses the object of a function range; a bare natural number n is the
+;; legacy notation for the function's argument n, i.e. (0 n)
+(define (latent-stxes->object object-stx mode)
+  (cond
+    [(not object-stx) -empty-obj]
+    [(exact-nonnegative-integer? (syntax-e object-stx))
+     (define idx (syntax-e object-stx))
+     (define msg (check-index-object 0 idx))
+     (when msg (parse-error #:stx object-stx msg))
+     (-arg-path idx 0)]
+    [else (parse-obj object-stx mode)]))
 
 (define (parse-types stx-list)
   (stx-map parse-type stx-list))
@@ -823,7 +892,8 @@
              [#:identifiers (list x-local)
               #:types (list t)]
              (with-local-term-names (list (cons #'x x-local))
-               (parse-prop #'prop do-parse mode))))
+               (with-binder 'refinement
+                 (parse-prop #'prop do-parse mode (-id-path x-local))))))
          ;; build the refinement type!
          (define refinement-type (-refine x-local t p))
          ;; record the name for printing purposes
@@ -1024,7 +1094,8 @@
                   [#:identifiers dep-local-ids
                    #:types dep-local-types]
                   (with-local-term-names (map cons dep-ids dep-local-ids)
-                    (do-parse (list-ref (attribute args.type-stx) idx)))))
+                    (with-binder 'opaque
+                      (do-parse (list-ref (attribute args.type-stx) idx))))))
               (hash-set! arg-type-dict idx idx-type))
 
             (define (abstract rep)
@@ -1051,7 +1122,16 @@
                   (with-local-term-names (map cons
                                               in-scope-arg-names
                                               in-scope-arg-local-names)
-                    (abstract (parse-prop #'pre-stx do-parse mode))))))
+                    ;; a bare type refers to the only argument in scope, if any
+                    (define default-pre-obj
+                      (and (= 1 (length in-scope-arg-local-names))
+                           (-id-path (car in-scope-arg-local-names))))
+                    (with-binder (binder dom default-pre-obj)
+                      (abstract (parse-prop #'pre-stx do-parse mode)))))))
+            ;; a bare type in the range refers to the only argument, if any
+            (define default-rng-obj
+              (and (= 1 (length arg-local-idents))
+                   (-id-path (car arg-local-idents))))
             ;; now type check the range
             (with-extended-lexical-env
               [#:identifiers arg-local-idents
@@ -1059,18 +1139,25 @@
               (with-local-term-names (map cons
                                           arg-idents
                                           arg-local-idents)
-                (match (parse-values-type #'rng-type do-parse do-parse-multi)
-                  ;; single value'd return type, propositions/objects allowed
-                  [(Values: (list (Result: rng-t _ _)))
-                   (define rng-ps (-PS (or (and (attribute rng-p+)
-                                                (parse-prop #'rng-p+ do-parse mode))
-                                           -tt)
-                                       (or (and (attribute rng-p-)
-                                                (parse-prop #'rng-p- do-parse mode))
-                                           -tt)))
+               (with-binder (binder dom default-rng-obj)
+                (match (parse-values-type #'rng-type do-parse do-parse-multi mode)
+                  ;; single value'd return type, propositions/objects allowed,
+                  ;; either in the result itself or after the range
+                  [(Values: (list (Result: rng-t (PropSet: res-p+ res-p-) res-o)))
+                   (when (and (attribute rng-o) (not (Empty? res-o)))
+                     (parse-error #:stx #'rng-o
+                                  "the range of a dependent function specifies its object twice"))
+                   (define rng-ps (-PS (-and res-p+
+                                             (or (and (attribute rng-p+)
+                                                      (parse-prop #'rng-p+ do-parse mode))
+                                                 -tt))
+                                       (-and res-p-
+                                             (or (and (attribute rng-p-)
+                                                      (parse-prop #'rng-p- do-parse mode))
+                                                 -tt))))
                    (define rng-obj (or (and (attribute rng-o)
                                             (parse-obj #'rng-o mode))
-                                       -empty-obj))
+                                       res-o))
                    (define abstracted-rng-t (abstract rng-t))
                    (define abstracted-rng-ps (abstract rng-ps))
                    (define abstracted-rng-obj (abstract rng-obj))
@@ -1109,58 +1196,63 @@
                       (make-DepFun
                        abstracted-dom
                        abstracted-pre-prop
-                       abstracted-rng-vals)])])))])]
+                       abstracted-rng-vals)])]))))])]
         ;; curried function notation
         [((~and dom:non-keyword-ty (~not :->^)) ...
                                                 :->^
                                                 (~and (~seq rest-dom ...) (~seq (~or _ (~between :->^ 1 +inf.0)) ...)))
-         (define doms (syntax->list #'(dom ...)))
-         (with-arity (length doms)
-           (let ([doms (for/list ([d (in-list doms)])
-                         (do-parse d))])
-             (make-Fun
-              (list (-Arrow doms (do-parse (syntax/loc stx (rest-dom ...))))))))]
+         (define doms (for/list ([d (in-list (syntax->list #'(dom ...)))])
+                        (do-parse d)))
+         (make-Fun
+          (list (-Arrow doms
+                        (with-function-binder doms
+                          (do-parse (syntax/loc stx (rest-dom ...)))))))]
         [(~or (:->^ dom rng :colon^ (~var latent (legacy-simple-latent-prop do-parse)))
               (dom :->^ rng :colon^ (~var latent (legacy-simple-latent-prop do-parse))))
          ;; use do-parse instead of parse-values-type because we need to add the props from the pred-ty
-         (with-arity 1
-           (make-pred-ty (list (do-parse #'dom)) (do-parse #'rng) (attribute latent.type)
-                         (-acc-path (attribute latent.path) (-arg-path 0))))]
+         (define dom-ty (do-parse #'dom))
+         (make-pred-ty (list dom-ty)
+                       (with-function-binder (list dom-ty) (do-parse #'rng))
+                       (attribute latent.type)
+                       (-acc-path (attribute latent.path) (-arg-path 0)))]
         [(~or (:->^ dom:non-keyword-ty ... (~var kws (keyword-tys do-parse)) ... rest:non-keyword-ty ddd:star rng)
               (dom:non-keyword-ty ... (~var kws (keyword-tys do-parse)) ... rest:non-keyword-ty ddd:star :->^ rng))
-         (with-arity (length (syntax->list #'(dom ...)))
-           (make-Fun
-            (list (-Arrow
-                   (do-parse-multi #'(dom ...))
-                   (parse-values-type #'rng do-parse do-parse-multi)
-                   #:rest (do-parse #'rest)
-                   #:kws (map force (attribute kws.Keyword))))))]
+         (define doms (do-parse-multi #'(dom ...)))
+         (make-Fun
+          (list (-Arrow
+                 doms
+                 (with-function-binder doms
+                   (parse-values-type #'rng do-parse do-parse-multi mode))
+                 #:rest (do-parse #'rest)
+                 #:kws (map force (attribute kws.Keyword)))))]
         [(~or (:->^ dom:non-keyword-ty ... rest:non-keyword-ty :ddd/bound rng)
               (dom:non-keyword-ty ... rest:non-keyword-ty :ddd/bound :->^ rng))
-         (with-arity (length (syntax->list #'(dom ...)))
-           (let* ([bnd (syntax-e #'bound)])
-             (unless (bound-index? bnd)
-               (parse-error
-                #:stx #'bound
-                "used a type variable not bound with ... as a bound on a ..."
-                "variable" bnd))
-             (make-Fun
-              (list
-               (make-arr-dots (do-parse-multi #'(dom ...))
-                              (parse-values-type #'rng do-parse do-parse-multi)
-                              (extend-tvars (list bnd)
-                                            (do-parse #'rest))
-                              bnd)))))]
+         (let* ([bnd (syntax-e #'bound)])
+           (unless (bound-index? bnd)
+             (parse-error
+              #:stx #'bound
+              "used a type variable not bound with ... as a bound on a ..."
+              "variable" bnd))
+           (define doms (do-parse-multi #'(dom ...)))
+           (make-Fun
+            (list
+             (make-arr-dots doms
+                            (with-function-binder doms
+                              (parse-values-type #'rng do-parse do-parse-multi mode))
+                            (extend-tvars (list bnd)
+                                          (do-parse #'rest))
+                            bnd))))]
         [(~or (:->^ dom:non-keyword-ty ... rest:non-keyword-ty _:ddd rng)
               (dom:non-keyword-ty ... rest:non-keyword-ty _:ddd :->^ rng))
-         (with-arity (length (syntax->list #'(dom ...)))
-           (let ([var (infer-index stx)])
-             (make-Fun
-              (list
-               (make-arr-dots (do-parse-multi #'(dom ...))
-                              (parse-values-type #'rng do-parse do-parse-multi)
-                              (extend-tvars (list var) (do-parse #'rest))
-                              var)))))]
+         (let ([var (infer-index stx)])
+           (define doms (do-parse-multi #'(dom ...)))
+           (make-Fun
+            (list
+             (make-arr-dots doms
+                            (with-function-binder doms
+                              (parse-values-type #'rng do-parse do-parse-multi mode))
+                            (extend-tvars (list var) (do-parse #'rest))
+                            var))))]
         #| ;; has to be below the previous one
         [(dom:expr ... :->^ rng)
         (->* (do-parse-multi #'(dom ...))
@@ -1172,10 +1264,12 @@
                                      (define syms (map syntax-e (attribute rng.vars)))
                                      (extend-tvars syms
                                                    (cond
-                                                     [(attribute rng.prop-type)
+                                                     [(attribute rng.prop-stx)
                                                       (make-ExitentialResult syms
                                                                              (do-parse (attribute rng.t))
-                                                                             (-PS (-is-type 0 (do-parse (attribute rng.prop-type)))
+                                                                             (-PS (parse-prop (attribute rng.prop-stx)
+                                                                                              do-parse
+                                                                                              mode)
                                                                                   -tt)
                                                                              -empty-obj)]
                                                      [else
@@ -1183,60 +1277,63 @@
         [(~or (:->^ dom:non-keyword-ty ... (~var kws (keyword-tys do-parse)) ... rng)
               (dom:non-keyword-ty ... (~var kws (keyword-tys do-parse)) ... :->^ rng))
 
-         (define doms (syntax->list #'(dom ...)))
-         (with-arity (length doms)
-           (let ([doms (for/list ([d (in-list doms)])
-                         (do-parse d))])
-             (make-Fun
-              (list (-Arrow doms
-                            (parameterize ([parsing-existential-rng? #t])
-                              (parse-values-type #'rng do-parse do-parse-multi))
-                            #:kws (map force (attribute kws.Keyword)))))))]
+         (define doms (for/list ([d (in-list (syntax->list #'(dom ...)))])
+                        (do-parse d)))
+         (make-Fun
+          (list (-Arrow doms
+                        (with-function-binder doms
+                          (parameterize ([parsing-existential-rng? #t])
+                            (parse-values-type #'rng do-parse do-parse-multi mode)))
+                        #:kws (map force (attribute kws.Keyword)))))]
         ;; This case needs to be at the end because it uses cut points to give good error messages.
         [(~or (:->^ ~! dom:non-keyword-ty ... rng:expr
-                    :colon^ (~var latent (legacy-full-latent (syntax->list #'(dom ...)) do-parse)))
+                    :colon^ (~var latent latent-stxes))
               (dom:non-keyword-ty ... :->^ rng:expr
-                                  ~! :colon^ (~var latent (legacy-full-latent (syntax->list #'(dom ...)) do-parse))))
+                                  ~! :colon^ (~var latent latent-stxes)))
          ;; use do-parse instead of parse-values-type because we need to add the props from the pred-ty
-         (with-arity (length (syntax->list #'(dom ...)))
-           (->* (do-parse-multi #'(dom ...) (add1 current-level))
+         (define doms (do-parse-multi #'(dom ...) (add1 current-level)))
+         (with-function-binder doms
+           (->* doms
                 (do-parse #'rng (add1 current-level))
-                : (-PS (attribute latent.positive) (attribute latent.negative))
-                : (attribute latent.object)))]
+                : (latent-stxes->propset (attribute latent.p+) (attribute latent.p-)
+                                         do-parse mode)
+                : (latent-stxes->object (attribute latent.object-stx) mode)))]
         ;; like ->* below but w/ a #:rest-pat present
         [(:->*^ (~var mand (->*-args #t do-parse))
                 (~optional (~var opt (->*-args #f do-parse))
                            #:defaults ([opt.doms null] [opt.kws null]))
                 #:rest-star (rest-types-stx:non-keyword-ty ...)
                 rng)
-         (with-arity (length (attribute mand.doms))
-           (define doms (map do-parse (attribute mand.doms)))
-           (define opt-doms (map do-parse (attribute opt.doms)))
-           (define rest-tys (stx-map do-parse #'(rest-types-stx ...)))
-           (cond
-             [(< (length rest-tys) 1)
-              (opt-fn doms opt-doms (parse-values-type #'rng do-parse do-parse-multi)
-                      #:kws (map force (append (attribute mand.kws)
-                                               (attribute opt.kws))))]
-             [else
-              (opt-fn doms opt-doms (parse-values-type #'rng  do-parse do-parse-multi)
-                      #:rest (make-Rest rest-tys)
-                      #:kws (map force (append (attribute mand.kws)
-                                               (attribute opt.kws))))]))]
+         (define doms (map do-parse (attribute mand.doms)))
+         (define opt-doms (map do-parse (attribute opt.doms)))
+         (define rest-tys (stx-map do-parse #'(rest-types-stx ...)))
+         ;; only the mandatory arguments are present in every arity
+         (define rng-ty (with-function-binder doms
+                          (parse-values-type #'rng do-parse do-parse-multi mode)))
+         (cond
+           [(< (length rest-tys) 1)
+            (opt-fn doms opt-doms rng-ty
+                    #:kws (map force (append (attribute mand.kws)
+                                             (attribute opt.kws))))]
+           [else
+            (opt-fn doms opt-doms rng-ty
+                    #:rest (make-Rest rest-tys)
+                    #:kws (map force (append (attribute mand.kws)
+                                             (attribute opt.kws))))])]
         [(:->*^ (~var mand (->*-args #t do-parse))
                 (~optional (~var opt (->*-args #f do-parse))
                            #:defaults ([opt.doms null] [opt.kws null]))
                 rest:optional->*-rest
                 rng)
-         (with-arity (length (attribute mand.doms))
-           (define doms (map do-parse (attribute mand.doms)))
-           (define opt-doms (map do-parse (attribute opt.doms)))
-           (opt-fn doms opt-doms (parse-values-type #'rng do-parse
-                                                    do-parse-multi)
-                   #:rest (and (attribute rest.type)
-                               (make-Rest (list (do-parse (attribute rest.type)))))
-                   #:kws (map force (append (attribute mand.kws)
-                                            (attribute opt.kws)))))]
+         (define doms (map do-parse (attribute mand.doms)))
+         (define opt-doms (map do-parse (attribute opt.doms)))
+         (opt-fn doms opt-doms (with-function-binder doms
+                                 (parse-values-type #'rng do-parse
+                                                    do-parse-multi))
+                 #:rest (and (attribute rest.type)
+                             (make-Rest (list (do-parse (attribute rest.type)))))
+                 #:kws (map force (append (attribute mand.kws)
+                                          (attribute opt.kws))))]
         [:->^
          (parse-error #:delayed? #t "incorrect use of -> type constructor")
          Err]
@@ -1449,8 +1546,12 @@
                                                  INIT-LEVEL)))))
          #:mode #f))
 
-(define-syntax-rule (define-parse-container-type fname pattern maker maker^ [lhs rhs] ...)
-  (define (fname stx do-parse do-parse-multi)
+;; The generated parser's arguments are the syntax to parse, the parsers
+;; for one type and for a list of types, and the parsing mode. Without
+;; dots, `parse-elems` parses the elements.
+(define-syntax-rule (define-parse-container-type fname pattern maker maker^ parse-elems
+                      [lhs rhs] ...)
+  (define (fname stx do-parse do-parse-multi [mode #f])
     (parameterize ([current-orig-stx stx])
       (syntax-parse stx
         [(pattern tys (... ...) dty :ddd/bound)
@@ -1470,8 +1571,12 @@
                                 (do-parse #'dty))
                   var))]
         [(pattern tys (... ...))
-         (maker^ (do-parse-multi #'(tys (... ...))))]
-        [lhs (rhs do-parse do-parse-multi)] ...))))
+         (maker^ (parse-elems #'(tys (... ...)) do-parse do-parse-multi mode))]
+        [lhs (rhs do-parse do-parse-multi mode)] ...))))
+
+;; the elements of a container type that holds types
+(define (parse-type-elems stxs do-parse do-parse-multi mode)
+  (do-parse-multi stxs))
 
 ;; Syntax -> Type
 ;; Parse a (List ...) type
@@ -1480,21 +1585,44 @@
 (define-parse-container-type parse-list-type :List^
                               (lambda (tys dtys var)
                                 (-Tuple* tys (make-ListDots dtys var)))
-                              -Tuple)
+                              -Tuple
+                              parse-type-elems)
 
 ;; Syntax -> Type
 ;; Parse a (Sequenceof ...) type
 (define-parse-container-type parse-sequence-type :Sequenceof^ -seq-dots (lambda (args)
-                                                                           (apply -seq args)))
+                                                                           (apply -seq args))
+                              parse-type-elems)
+
+;; parse-result-type : Syntax (Syntax -> Type) Mode -> Result
+;; Parses one value of a Values type in a function's range, which may
+;; have latent propositions and an object: (type : #:+ prop #:- prop #:object obj)
+(define (parse-result-type stx do-parse mode)
+  (syntax-parse stx
+    [(t:expr :colon^ (~var latent latent-stxes))
+     (-result (do-parse #'t)
+              (latent-stxes->propset (attribute latent.p+)
+                                     (attribute latent.p-)
+                                     do-parse
+                                     mode)
+              (latent-stxes->object (attribute latent.object-stx) mode))]
+    [t
+     (-result (do-parse #'t))]))
 
 ;; Syntax -> Type
 ;; Parse a (Values ...) or AnyValues type
 (define-parse-container-type parse-values-type (~or :Values^ :values^)
                               -values-dots
                               -values
+                              (lambda (stxs do-parse do-parse-multi mode)
+                                           (for/list ([r-stx (in-list (syntax->list stxs))])
+                                             (parse-result-type r-stx do-parse mode)))
+                              [(:AnyValues^ :colon^ prop:expr)
+                               (lambda (do-parse _ mode)
+                                 (-AnyValues (parse-prop #'prop do-parse mode)))]
                               [:AnyValues^ (lambda _ ManyUniv)]
                               [t
-                               (lambda (do-parse _)
+                               (lambda (do-parse . _)
                                  (-values (list (do-parse #'t))))])
 
 ;;; Utilities for (Class ...) type parsing
@@ -1735,15 +1863,30 @@
     (parse-error "class member conflicts with row variable constraints"
                  "conflicting name" conflicting-name)))
 
+;; parse-tc-results : Syntax -> tc-results
+;; Parses the expected type of an expression. Propositions here are not
+;; underneath any function type, so they have no default subject.
 (define (parse-tc-results stx)
+  (define (parse-tc-result stx)
+    (syntax-parse stx
+      [(_ :colon^ . _)
+       (match-define (Result: t ps o) (parse-result-type stx parse-type #f))
+       (values t ps o)]
+      [t
+       (values (parse-type #'t) #f #f)]))
   (syntax-parse stx
-    [((~or :Values^ :values^) t ...)
-     (define empties (stx-map (λ (x) #f) #'(t ...)))
-     (ret (parse-types #'(t ...))
-          empties
-          empties)]
+    [((~or :Values^ :values^) r ...)
+     (define-values (types props objs)
+       (for/lists (_1 _2 _3)
+                  ([r-stx (in-list (syntax->list #'(r ...)))])
+         (parse-tc-result r-stx)))
+     (ret types props objs)]
+    [(:AnyValues^ :colon^ prop:expr)
+     (-tc-any-results (parse-prop #'prop parse-type #f))]
     [:AnyValues^ (-tc-any-results #f)]
-    [t (ret (parse-type #'t) #f #f)]))
+    [r
+     (define-values (t ps o) (parse-tc-result #'r))
+     (ret t ps o)]))
 
 (define parse-type/id (parse/id parse-type))
 
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index eb0759dba..82a22afc5 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -64,7 +64,6 @@
          instantiate-propset
          instantiate-obj
          abstract-obj
-         substitute-names
          set-struct-property-pred!
          variances-in-type
          DepFun/ids:
@@ -1706,19 +1705,6 @@
                   (transform nm lvl))]
       [_ (Rep-fmap rep rec)])))
 
-;; simple substitution mapping identifiers to
-;; identifiers (or objects)
-;; pre: (= (length names) (length names-or-objs))
-(define (substitute-names rep names names-or-objs)
-  (let subst ([rep rep])
-    (match rep
-      [(Path: flds (? identifier? name))
-       (make-Path (map subst flds)
-                  (match (index-of names name free-identifier=?)
-                    [#f name]
-                    [idx (list-ref names-or-objs idx)]))]
-      [_ (Rep-fmap rep subst)])))
-
 ;;************************************************************
 ;; Smart Constructors/Destructors for Type Binders
 ;;
diff --git a/typed-racket-lib/typed-racket/typecheck/error-message.rkt b/typed-racket-lib/typed-racket/typecheck/error-message.rkt
index 165d672f0..4c7bf430c 100644
--- a/typed-racket-lib/typed-racket/typecheck/error-message.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/error-message.rkt
@@ -14,7 +14,7 @@
          "../types/resolve.rkt"
          "../utils/tc-utils.rkt"
          "../rep/type-rep.rkt"
-         (only-in "../types/printer.rkt" pretty-format-rep))
+         (only-in "../types/printer.rkt" pretty-format-rep call-showing-hidden-props))
 
 (provide/cond-contract [expected-but-got
                         (--> (-or/c Type? string?)
@@ -30,9 +30,14 @@
 ;; Type errors with "type mismatch", arguments may be types or other things
 ;; like the length of a list of types
 (define (type-mismatch t1 t2 [more #f])
-  (define t1* (if (Type? t1) (pretty-format-rep t1 #:indent 12) t1))
-  (define t2* (if (Type? t2) (pretty-format-rep t2 #:indent 9) t2))
-  (tc-error/fields "type mismatch" #:more more "expected" t1* "given" t2* #:delayed? #t))
+  ;; the expected type may demand latent propositions that are not
+  ;; printed by default
+  (call-showing-hidden-props
+   (list t1)
+   (λ ()
+     (define t1* (if (Type? t1) (pretty-format-rep t1 #:indent 12) t1))
+     (define t2* (if (Type? t2) (pretty-format-rep t2 #:indent 9) t2))
+     (tc-error/fields "type mismatch" #:more more "expected" t1* "given" t2* #:delayed? #t))))
 
 ;; expected-but-got : (U Type String) (U Type String) -> Void
 ;;
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
index f2f1a4631..b22753663 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
@@ -16,6 +16,7 @@
          "../types/utils.rkt"
          "../types/subtype.rkt"
          "../types/type-table.rkt"
+         (only-in "../types/printer.rkt" call-showing-hidden-props)
          "../env/lexical-env.rkt"
          "tc-envops.rkt"
          (except-in "../types/abbrev.rkt"
@@ -199,6 +200,16 @@
                            ;; if it's a dependent function, pass the argument identifiers so we
                            ;; can report those in the error message
                            #:arg-names [arg-names '()])
+  ;; the domains may demand latent propositions that are not printed
+  ;; by default
+  (call-showing-hidden-props
+   (apply append doms)
+   (λ ()
+     (domain-mismatches* f-stx args-stx ty doms rests rngs arg-tys tail-ty tail-bound
+                         expected return msg-thunk arg-names))))
+
+(define (domain-mismatches* f-stx args-stx ty doms rests rngs arg-tys tail-ty tail-bound
+                            expected return msg-thunk arg-names)
   (define arguments-str
     (stringify-args arg-tys tail-ty))
   (cond
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt
index cf5273d38..46234d958 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt
@@ -15,6 +15,7 @@
          "../../types/type-table.rkt"
          "../../rep/type-rep.rkt"
          "../../utils/tc-utils.rkt"
+         (only-in "../../types/printer.rkt" call-showing-hidden-props)
          "../../infer/infer.rkt"
          (for-label racket/base)
          ;; adjusted -1 since it's provided for-syntax
@@ -112,9 +113,12 @@
                      (loop kws-rest (cdr actuals) form-rest)
                      ;; failure
                      (and error?
-                          (tc-error/delayed
-                           "Wrong function argument type, expected ~a, got ~a for keyword argument ~a"
-                           t (car actuals) k)
+                          (call-showing-hidden-props
+                           (list t)
+                           (λ ()
+                             (tc-error/delayed
+                              "Wrong function argument type, expected ~a, got ~a for keyword argument ~a"
+                              t (car actuals) k)))
                           (loop kws-rest (cdr actuals) form-rest)))]
                 [req? ;; this keyword argument was required
                  (if error?
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
index ca224528a..c74d146d3 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
@@ -5,6 +5,7 @@
          (prefix-in c: (contract-req))
          (for-syntax syntax/parse racket/base)
          "../utils/tc-utils.rkt"
+         (only-in "../types/printer.rkt" call-showing-hidden-props)
          "../utils/identifier.rkt"
          "../env/tvar-env.rkt"
          "../env/lexical-env.rkt"
@@ -313,10 +314,13 @@
           #:when (subtype t in)
           (ret -Void -true-propset)]
          [(list t)
-          (tc-error/expr #:return (ret -Void -true-propset)
-                         "Wrong argument to parameter - expected ~a and got ~a"
-                         in
-                         t)]
+          (call-showing-hidden-props
+           (list in)
+           (λ ()
+             (tc-error/expr #:return (ret -Void -true-propset)
+                            "Wrong argument to parameter - expected ~a and got ~a"
+                            in
+                            t)))]
          [_
           (tc-error/expr "Wrong number of arguments to parameter - expected 0 or 1, got ~a"
                          (length argtys))])]
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
index 786bdac03..3b7bb9691 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
@@ -805,5 +805,5 @@
     [#:identifiers (cons name formals)
      #:types (cons ft args)]
     (values
-     (erase-identifiers (ret ft) names)
-     (erase-identifiers (tc-body/check body return) names))))
+     (erase-identifiers (ret ft) names (cons ft args))
+     (erase-identifiers (tc-body/check body return) names (cons ft args)))))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
index f30380e25..286ee3190 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
@@ -131,11 +131,13 @@
    tc-results/c)
   (define-values (idents types aliased-objs props)
     (consolidate-bound-ids-info bound-idss bound-resultss))
-  (define ids-to-erase
-    (for/list ([id (in-list idents)]
-               [obj (in-list aliased-objs)]
-               #:when (Empty? obj))
-      id))
+  (define-values (ids-to-erase types-to-erase)
+    (for/lists (_1 _2)
+               ([id (in-list idents)]
+                [type (in-list types)]
+                [obj (in-list aliased-objs)]
+                #:when (Empty? obj))
+      (values id type)))
   (define props^
     (let ([any-res (-tc-any-results #f)])
       (for/fold ([res null])
@@ -165,7 +167,8 @@
        (pre-body-thunk)
        ;; typecheck the body
        (tc-body/check body expected))
-     ids-to-erase)))
+     ids-to-erase
+     types-to-erase)))
 
 (define (tc-expr/maybe-expected/t e names)
   (syntax-parse names
@@ -360,9 +363,10 @@
                                                 (register-ignored! (lr-clause-expr cl)))
                                               (cdr clauses))
                                     (k #t))
-               (substitute-names (loop (cdr clauses))
-                                 names
-                                 os)))])))
+               (substitute-identifiers (loop (cdr clauses))
+                                       names
+                                       os
+                                       ts)))])))
 
 ;; this is so match can provide us with a syntax property to
 ;; say that this binding is only called in tail position
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
index 276ac2f66..45b5595bf 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
@@ -14,6 +14,7 @@
          "../types/path-type.rkt"
          "../types/subtract.rkt"
          "../types/overlap.rkt"
+         "../types/variance.rkt"
          (except-in "../types/abbrev.rkt" -> ->* one-of/c)
          (only-in "../infer/infer.rkt" intersect restrict)
          "../rep/core-rep.rkt"
@@ -21,6 +22,7 @@
          "../rep/object-rep.rkt"
          "../rep/prop-rep.rkt"
          "../rep/rep-utils.rkt"
+         "../rep/free-variance.rkt"
          "../rep/values-rep.rkt")
 
 (provide instantiate-obj+simplify)
@@ -35,9 +37,15 @@
                       (cons/c OptObject?
                               Type?)))
       full-tc-results/c)]
- [erase-identifiers (-> tc-results/c
-                        (listof identifier?)
-                        tc-results/c)])
+ [erase-identifiers (->* (tc-results/c
+                          (listof identifier?))
+                         ((listof Type?))
+                         tc-results/c)]
+ [substitute-identifiers (-> tc-results/c
+                             (listof identifier?)
+                             (listof OptObject?)
+                             (listof Type?)
+                             tc-results/c)])
 
 
 ;; Substitutes the given objects into the values and turns it into a
@@ -67,75 +75,223 @@
     [(ValuesDots: rs dty dbound)
      (-tc-results (map res->tc-res rs) (make-RestDots dty dbound))]))
 
-(define (erase-identifiers res names)
-  (substitute-names res names (for/list ([_ (in-list names)])
-                                -empty-obj)))
+;; erase-identifiers : tc-results (listof identifier) [(listof Type)] -> tc-results
+;; Erases the given identifiers, which are going out of scope, from
+;; `res`. When the identifiers' types are given, props that those types
+;; establish are kept as true rather than erased.
+(define (erase-identifiers res names [types (map (λ (_) Univ) names)])
+  (substitute-identifiers res names (map (λ (_) -empty-obj) names) types))
 
+;; substitute-identifiers : tc-results (listof identifier) (listof OptObject)
+;;                          (listof Type) -> tc-results
+;; Replaces each of `names` in `res` with the corresponding object, which
+;; denotes a value of the corresponding type.
+(define (substitute-identifiers res names objs types)
+  (define entries (map cons objs types))
+  (subst-objs+simplify
+   res
+   (λ (nm _)
+     (and (identifier? nm)
+          (for/first ([name (in-list names)]
+                      [entry (in-list entries)]
+                      #:when (free-identifier=? nm name))
+            entry)))))
+
+;; instantiate-obj+simplify : Rep (listof (list* idx OptObject Type)) -> Rep
+;; Replaces each De Bruijn index (0 . idx), the idx-th argument of the
+;; function whose range is `rep`, with the corresponding object.
 (define (instantiate-obj+simplify rep mapping)
-  ;; lookup: if idx has a mapping,
-  ;; then returns (cons/c OptObject? Type?),
-  ;; else returns #f
-  (define (lookup idx) (match (assv idx mapping)
-                         [(cons _ entry) entry]
-                         [_ #f]))
-  (let subst/lvl ([rep rep] [lvl 0])
-    (define (subst rep) (subst/lvl rep lvl))
+  (subst-objs+simplify
+   rep
+   (λ (nm lvl)
+     (match nm
+       [(cons (== lvl) idx)
+        (match (assv idx mapping)
+          [(cons _ entry) entry]
+          [_ #f])]
+       [_ #f]))))
+
+;; A Polarity describes how a prop at some position is used, and so in
+;; which direction substitution may change it:
+;;  #t -- positive: the prop is a fact the typechecker learns, so it may
+;;        soundly be weakened
+;;  #f -- negative (underneath a function domain, or a negated type): the
+;;        prop is an obligation the context must discharge, so it may
+;;        only be strengthened
+;;  (-> none/c) -- invariant (underneath a mutable container): the prop
+;;        may be neither weakened nor strengthened. Calling the procedure
+;;        gives up on the nearest enclosing type whose polarity is known,
+;;        replacing that type with its top type in a positive position
+;;        or with Bottom in a negative one.
+;;
+;; When a variable is substituted away by the empty object, props
+;; mentioning it can no longer be expressed: they become tt in positive
+;; positions but must become ff in negative ones, since erasing an
+;; obligation to tt would let arguments that never discharge it slip
+;; through. This follows the polarity-indexed substitution of figure 8
+;; of the paper, and object substitution in "Rebuild λTR", where the
+;; polarity is carried by the object (⊤ or ⊥) that replaces the variable
+;; and flips at function domains and underneath ∉. λTR has no mutable
+;; containers; widening an invariant position to its top type (or Bottom)
+;; preserves its subtyping-for-erasure lemma, A⁻ <: A <: A⁺.
+(define (flip pol) (if (procedure? pol) pol (not pol)))
+
+;; the prop that replaces one whose subject is erased
+(define (erased-prop pol)
+  (cond [(procedure? pol) (pol)]
+        [pol -tt]
+        [else -ff]))
+
+;; the props of a result whose object is erased: in a negative position
+;; the object is an obligation that can no longer be stated, so no value
+;; may satisfy the result (λTR uses the bottom object here)
+(define (erased-result-props ps pol)
+  (cond [(procedure? pol) (pol)]
+        [pol ps]
+        [else -ff-propset]))
+
+;; with-widening : Polarity Type ((-> none/c) -> Type) -> Type
+;; Calls `k` with the polarity to use for the invariant parts of a type
+;; at polarity `pol`; if those parts mention an erased object, the whole
+;; type becomes `top` (or Bottom, in a negative position).
+(define (with-widening pol top k)
+  (if (procedure? pol)
+      (k pol)
+      (let/ec esc
+        (k (λ () (esc (if pol top -Bottom)))))))
+
+;; subst-objs+simplify : Rep (name-ref/c natural -> (or/c #f (cons OptObject Type))) -> Rep
+;; Replaces each object whose name `lookup` maps, given the number of
+;; binders the object is underneath, with the object `lookup` returns,
+;; which denotes a value of the type `lookup` returns.
+(define (subst-objs+simplify rep lookup)
+  (let subst/lvl ([rep rep] [lvl 0] [pol #t])
+    (define (subst rep) (subst/lvl rep lvl pol))
+    (define (subst/flip rep) (subst/lvl rep lvl (flip pol)))
+    (define (subst/pol rep pol) (subst/lvl rep lvl pol))
+    (define (lookup* nm) (lookup nm lvl))
+    ;; substitutes a result's object; also returns the type that the
+    ;; substituted object is known to have
+    (define (subst-result-obj o)
+      (match o
+        [(Path: flds (app lookup* (? pair? entry)))
+         (values (make-Path (map subst flds) (car entry))
+                 (or (path-type flds (cdr entry)) Univ))]
+        [_ (values (and o (subst o)) #f)]))
+    ;; substitutes a result's type, props, and object
+    (define (subst-result orig-t orig-ps orig-o)
+      (define-values (o o-ty) (subst-result-obj orig-o))
+      (define t (if (and o-ty (not (Univ? o-ty)))
+                    (intersect (subst orig-t) o-ty)
+                    (subst orig-t)))
+      (define ps (cond
+                   [(not orig-ps) #f]
+                   [(and (Empty? o) (Object? orig-o))
+                    (erased-result-props (subst orig-ps) pol)]
+                   [else (subst orig-ps)]))
+      (values t ps o))
     (match rep
       ;; Functions
-      ;; increment the level of the substituted object
+      ;; increment the level of the substituted object;
+      ;; the domain (incl. rest/keyword args) is a negative position
       [(Arrow: dom rst kws rng rng-T+)
-       (make-Arrow (map subst dom)
-                   (and rst (subst rst))
-                   (map subst kws)
-                   (subst/lvl rng (add1 lvl))
+       (make-Arrow (map subst/flip dom)
+                   (and rst (subst/flip rst))
+                   (map subst/flip kws)
+                   (subst/lvl rng (add1 lvl) pol)
                    rng-T+)]
       [(DepFun: dom pre rng)
        (make-DepFun (for/list ([d (in-list dom)])
-                      (subst/lvl d (add1 lvl)))
-                    (subst/lvl pre (add1 lvl))
-                    (subst/lvl rng (add1 lvl)))]
+                      (subst/lvl d (add1 lvl) (flip pol)))
+                    (subst/lvl pre (add1 lvl) (flip pol))
+                    (subst/lvl rng (add1 lvl) pol))]
       [(Intersection: ts raw-prop)
        (-refine (make-Intersection (map subst ts))
-                (subst/lvl raw-prop (add1 lvl)))]
-      [(Path: flds (cons (== lvl) (app lookup (cons o _))))
+                (subst/lvl raw-prop (add1 lvl) pol))]
+      [(Path: flds (app lookup* (cons o _)))
        (make-Path (map subst flds) o)]
       ;; restrict with the type for results and props
-      [(TypeProp: (Path: flds (cons (== lvl) (app lookup (? pair? entry))))
-                  prop-ty)
+      [(TypeProp: (Path: flds (app lookup* (? pair? entry))) raw-prop-ty)
        (define o (make-Path (map subst flds) (car entry)))
        (define o-ty (or (path-type flds (cdr entry)) Univ))
+       (define prop-ty (subst raw-prop-ty))
        (define new-prop-ty (intersect prop-ty o-ty o))
        (cond
          [(Bottom? new-prop-ty) -ff]
          [(and (not (F? prop-ty))  (subtype o-ty prop-ty)) -tt]
-         [(Empty? o) -tt]
+         [(Empty? o) (erased-prop pol)]
          [else (-is-type o new-prop-ty)])]
-      [(NotTypeProp: (Path: flds (cons (== lvl) (app lookup (? pair? entry))))
-                     prop-ty)
+      [(NotTypeProp: (Path: flds (app lookup* (? pair? entry))) raw-prop-ty)
        (define o (make-Path (map subst flds) (car entry)))
        (define o-ty (or (path-type flds (cdr entry)) Univ))
+       ;; the type in a NotTypeProp is underneath a negation,
+       ;; so polarity flips
+       (define prop-ty (subst/flip raw-prop-ty))
        (define new-o-ty (subtract o-ty prop-ty o))
        (define new-prop-ty (restrict prop-ty o-ty o))
        (cond
          [(or (Bottom? new-o-ty)
               (Univ? new-prop-ty))
           -ff]
-         [(Empty? o) -tt]
+         ;; no overlap between the type of the object and the
+         ;; negated type: the prop is known to hold
+         [(Bottom? new-prop-ty) -tt]
+         [(Empty? o) (erased-prop pol)]
          [else (-not-type o new-prop-ty)])]
-      [(tc-result: orig-t
-                   orig-ps
-                   (Path: flds (cons (== lvl) (app lookup (? pair? entry)))))
-       (define o (make-Path (map subst flds) (car entry)))
-       (define t (intersect orig-t (or (path-type flds (cdr entry)) Univ)))
-       (define ps (subst orig-ps))
-       (-tc-result t ps o)]
-      [(Result: orig-t
-                orig-ps
-                (Path: flds (cons (== lvl) (app lookup (? pair? entry)))))
-       (define o (make-Path (map subst flds) (car entry)))
-       (define t (intersect orig-t (or (path-type flds (cdr entry)) Univ)))
-       (define ps (subst orig-ps))
-       (make-Result t ps o)]
+      ;; other subjects, such as linear expressions, may become empty too
+      [(TypeProp: obj prop-ty)
+       (define new-obj (subst obj))
+       (if (Empty? new-obj)
+           (erased-prop pol)
+           (-is-type new-obj (subst prop-ty)))]
+      [(NotTypeProp: obj prop-ty)
+       (define new-obj (subst obj))
+       (if (Empty? new-obj)
+           (erased-prop pol)
+           (-not-type new-obj (subst/flip prop-ty)))]
+      [(LeqProp: lhs rhs)
+       (define new-lhs (subst lhs))
+       (define new-rhs (subst rhs))
+       (if (or (Empty? new-lhs) (Empty? new-rhs))
+           (erased-prop pol)
+           (make-LeqProp new-lhs new-rhs))]
+      [(tc-result: orig-t orig-ps orig-o exi?)
+       (define-values (t ps o) (subst-result orig-t orig-ps orig-o))
+       (-tc-result t ps o exi?)]
+      [(Result: orig-t orig-ps orig-o n-exi)
+       (define-values (t ps o) (subst-result orig-t orig-ps orig-o))
+       (make-Result t ps o n-exi)]
+      ;; types with contravariant or invariant parameters
+      [(app Rep-variances (? pair? variances))
+       (define (subst-args inv)
+         (apply (Rep-constructor rep)
+                (for/list ([t (in-list (Rep-values rep))]
+                           [v (in-list variances)])
+                  (cond
+                    [(variance:co? v) (subst t)]
+                    [(variance:contra? v) (subst/flip t)]
+                    [else (subst/pol t inv)]))))
+       (if (memq variance:inv variances)
+           (with-widening pol (top-of rep) subst-args)
+           (subst-args pol))]
+      [(App: rator rands)
+       (define variances
+         (or (app-variances rator rands)
+             (map (λ (_) variance:inv) rands)))
+       (define (subst-args inv)
+         (make-App rator
+                   (for/list ([t (in-list rands)]
+                              [v (in-list variances)])
+                     (cond
+                       [(or (variance:co? v) (variance:const? v)) (subst t)]
+                       [(variance:contra? v) (subst/flip t)]
+                       [else (subst/pol t inv)]))))
+       (if (ormap (λ (v) (or (variance:inv? v) (variance:dotted? v))) variances)
+           (with-widening pol Univ subst-args)
+           (subst-args pol))]
+      [(? invariant-type?)
+       (with-widening pol (top-of rep)
+         (λ (inv) (Rep-fmap rep (λ (r) (subst/pol r inv)))))]
       ;; else default fold over subfields
       [_ (Rep-fmap rep subst)])))
 
diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt
index 5a534771d..69aecfbb6 100644
--- a/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/typed-racket-lib/typed-racket/types/printer.rkt
@@ -41,7 +41,7 @@
                  pretty-format-rep print-values print-result)))
 (provide-printer)
 
-(provide print-complex-props? type-output-sexpr-tweaker
+(provide print-complex-props? call-showing-hidden-props type-output-sexpr-tweaker
          current-print-type-fuel current-print-unexpanded)
 
 
@@ -54,6 +54,21 @@
 (define type-output-sexpr-tweaker (make-parameter values))
 (define print-complex-props? (make-parameter #f))
 
+;; call-showing-hidden-props : (Listof Any) (-> A) -> A
+;; Calls `thunk` with latent propositions printed if printing any of `vs`
+;; would otherwise hide some. Error messages pass the expected types, so
+;; that propositions an expected type demands, which can cause a mismatch
+;; by themselves, are shown.
+(define (call-showing-hidden-props vs thunk)
+  (define (hides-props? v)
+    (and (Rep? v)
+         (not (equal? (format "~a" v)
+                      (parameterize ([print-complex-props? #t])
+                        (format "~a" v))))))
+  (parameterize ([print-complex-props? (or (print-complex-props?)
+                                           (ormap hides-props? vs))])
+    (thunk)))
+
 ;; this parameter controls how far down the type to expand type names
 ;; interp. 0 -> don't expand
 ;;         1 -> expand one level, etc.
@@ -409,11 +424,11 @@
          `(,(type->sexp t) : #:+ ,(type->sexp ft))]
         [(Values: (list (Result: t ps (? Empty?))))
          (if (print-complex-props?)
-             `(,(type->sexp t) : ,(propset->sexp ps))
+             `(,(type->sexp t) : ,@(propset->latent-sexps ps))
              (list (type->sexp t)))]
         [(Values: (list (Result: t ps o)))
          (if (print-complex-props?)
-             `(,(type->sexp t) : ,(propset->sexp ps) ,(object->sexp o))
+             `(,(type->sexp t) : ,@(propset->latent-sexps ps) #:object ,(object->sexp o))
              (list (type->sexp t)))]
         [_ (list (values->sexp rng))]))]
     [else `(Unknown Function Type: ,(struct->vector arr))]))
@@ -531,9 +546,10 @@
               (or 'none (PropSet: (? TrueProp?) (? TrueProp?)))
               (or 'none (? Empty?)))
      (type->sexp t)]
-    [(Result: t ps (? Empty?)) `(,(type->sexp t) : ,(propset->sexp ps))]
+    [(Result: t ps (? Empty?)) `(,(type->sexp t) : ,@(propset->latent-sexps ps))]
     [(Result: t ps lo) `(,(type->sexp t) :
-                         ,(propset->sexp ps) :
+                         ,@(propset->latent-sexps ps)
+                         #:object
                          ,(object->sexp lo))]
     [else `(Unknown Result: ,(struct->vector res))]))
 
@@ -541,9 +557,15 @@
 ;; convert a prop set to an s-expression that can be printed
 (define (propset->sexp ps)
   (match ps
-    [(PropSet: thn els) `(,(prop->sexp thn) \| ,(prop->sexp els))]
+    [(? PropSet?) (propset->latent-sexps ps)]
     [else `(Unknown PropSet: ,(struct->vector ps))]))
 
+(define (propset->latent-sexps ps)
+  (match ps
+    [(PropSet: thn els)
+     `(#:+ ,(prop->sexp thn) #:- ,(prop->sexp els))]
+    [else `(#:+ (Unknown PropSet: ,(struct->vector ps)))]))
+
 ;; values->sexp : SomeValues -> S-expression
 ;; convert a values to an s-expression that can be printed
 (define (values->sexp v)
diff --git a/typed-racket-lib/typed-racket/types/variance.rkt b/typed-racket-lib/typed-racket/types/variance.rkt
new file mode 100644
index 000000000..b63dc6fef
--- /dev/null
+++ b/typed-racket-lib/typed-racket/types/variance.rkt
@@ -0,0 +1,64 @@
+#lang racket/base
+
+;; Helpers for operations that follow the variance of type constructors,
+;; such as substituting objects into types (typecheck/tc-subst.rkt) and
+;; eliminating type variables (infer/promote-demote.rkt). When such an
+;; operation cannot change an invariant part of a type, it replaces the
+;; whole type with its top type (in a positive position) or with Bottom
+;; (in a negative one).
+
+(require "../utils/prefab.rkt"
+         racket/match
+         "../env/type-constr-env.rkt"
+         "../rep/type-rep.rkt"
+         "../rep/type-constr.rkt")
+
+(provide top-of
+         invariant-type?
+         app-variances)
+
+;; top-of : Type -> Type
+;; the least supertype of `t` whose invariant parts are not fixed
+(define (top-of t)
+  (match t
+    [(? MPair?) -MPairTop]
+    [(or (? Mutable-Vector?) (? Mutable-HeterogeneousVector?)) -Mutable-VectorTop]
+    [(? Box?) -BoxTop]
+    [(? Channel?) -ChannelTop]
+    [(? Async-Channel?) -Async-ChannelTop]
+    [(? ThreadCell?) -ThreadCellTop]
+    [(? Weak-Box?) -Weak-BoxTop]
+    [(? Mutable-HashTable?) -Mutable-HashTableTop]
+    [(? Weak-HashTable?) -Weak-HashTableTop]
+    [(? Prompt-Tagof?) -Prompt-TagTop]
+    [(? Continuation-Mark-Keyof?) -Continuation-Mark-KeyTop]
+    [(Prefab: key _) (make-PrefabTop key)]
+    [(? Class?) -ClassTop]
+    [(? Unit?) -UnitTop]
+    [(? StructType?) -StructTypeTop]
+    [_ Univ]))
+
+;; invariant-type? : Type -> Boolean
+;; does `t` have invariant parts that its Rep-variances do not describe?
+(define (invariant-type? t)
+  (or (and (Struct? t) (ormap fld-mutable? (Struct-flds t)))
+      (Mutable-HeterogeneousVector? t)
+      (and (Prefab? t) (prefab-key/mutable-fields? (Prefab-key t)))
+      ;; these mix positive, negative, and mutable parts
+      (Class? t)
+      (Instance? t)
+      (Unit? t)
+      (StructType? t)
+      (Struct-Property? t)))
+
+;; app-variances : Type (Listof Type) -> (U (Listof Variance) #f)
+;; the variances of the arguments of an applied type constructor, if known
+(define (app-variances rator rands)
+  (match rator
+    [(Name: id _ _)
+     (match (lookup-type-constructor id)
+       [(struct* TypeConstructor ([variances (? list? variances)]))
+        #:when (= (length variances) (length rands))
+        variances]
+       [_ #f])]
+    [_ #f]))
diff --git a/typed-racket-more/info.rkt b/typed-racket-more/info.rkt
index cc43f9ebf..f605f39f7 100644
--- a/typed-racket-more/info.rkt
+++ b/typed-racket-more/info.rkt
@@ -27,7 +27,7 @@
 
 (define pkg-authors '(samth stamourv))
 
-(define version "1.15")
+(define version "1.16")
 
 (define license
   '(Apache-2.0 OR MIT))
diff --git a/typed-racket-test/fail/demote-arrow-props.rkt b/typed-racket-test/fail/demote-arrow-props.rkt
new file mode 100644
index 000000000..fa699308a
--- /dev/null
+++ b/typed-racket-test/fail/demote-arrow-props.rkt
@@ -0,0 +1,13 @@
+#;
+(exn-pred #rx"could not be applied")
+#lang typed/racket
+
+;; Inferring map's argument type eliminates call's type variable from
+;; (-> Any Boolean : a). Demotion dropped that function type's only case,
+;; leaving a type that every function satisfies, so a function on
+;; integers was accepted and then applied to a string. Demotion must
+;; strengthen the propositions instead.
+
+(: call (All (a) (-> (-> Any Boolean : a) Boolean)))
+(define (call p) (p "hello"))
+(map call (list (λ ([x : Integer]) (= (add1 x) 1))))
diff --git a/typed-racket-test/fail/erase-box-invariant-prop.rkt b/typed-racket-test/fail/erase-box-invariant-prop.rkt
new file mode 100644
index 000000000..23a64ac7d
--- /dev/null
+++ b/typed-racket-test/fail/erase-box-invariant-prop.rkt
@@ -0,0 +1,19 @@
+#;
+(exn-pred #rx"set-box!")
+#lang typed/racket
+
+;; A prop about x underneath Boxof, which is invariant, can be neither
+;; weakened nor strengthened when x goes out of scope. Erasing it to Top
+;; (as a positive position would) let the box escape with type
+;; (Boxof (-> Any Boolean)), so a function that never establishes
+;; (Number @ x) could be stored into it and then trusted by the closure
+;; that still has x in scope. The box's type must widen to BoxTop.
+
+(define p
+  (let ([x : Any ""])
+    (define b : (Boxof (Any -> Boolean : #:+ (Number @ x)))
+      (box (lambda ([w : Any]) (number? x))))
+    (cons b (lambda () (if ((unbox b) 0) (add1 x) 1)))))
+
+(set-box! (car p) (lambda ([w : Any]) #t))
+((cdr p))
diff --git a/typed-racket-test/fail/erase-define-negative-prop.rkt b/typed-racket-test/fail/erase-define-negative-prop.rkt
new file mode 100644
index 000000000..e1a961f4d
--- /dev/null
+++ b/typed-racket-test/fail/erase-define-negative-prop.rkt
@@ -0,0 +1,16 @@
+#;
+(exn-pred #rx"expected: \\(-> Any Boolean : #:\\+ Bot")
+#lang typed/racket
+
+;; Same shape as erase-id-negative-prop.rkt, but x is bound by an
+;; internal definition, which expands to letrec-values, so the erasure
+;; happens when the letrec's clauses go out of scope. The prop
+;; (Number @ x) in the (negative) domain position must erase to Bot.
+
+(define g
+  (let ()
+    (define x : Any "")
+    (lambda ([f : (Any -> Boolean : #:+ (Number @ x))])
+      (if (f x) (add1 x) 1))))
+
+(g (lambda ([w : Any]) #t))
diff --git a/typed-racket-test/fail/erase-depfun-object-negative.rkt b/typed-racket-test/fail/erase-depfun-object-negative.rkt
new file mode 100644
index 000000000..750c9ccfb
--- /dev/null
+++ b/typed-racket-test/fail/erase-depfun-object-negative.rkt
@@ -0,0 +1,16 @@
+#;
+(exn-pred #rx"expected: \\(-> Any Any : #:\\+ Bot #:- Bot")
+#lang typed/racket
+
+;; A function type in a negative position that promises to return x
+;; (#:object x) is an obligation; when x goes out of scope the
+;; obligation can no longer be stated, so no argument may satisfy it.
+;; Dropping the object instead let any function through, after which
+;; (number? (f 0)) wrongly refined x.
+
+(define g
+  (let ([x (ann "" Any)])
+    (lambda ([f : (-> ([w : Any]) Any #:object x)])
+      (if (number? (f 0)) (add1 x) 1))))
+
+(g (lambda ([w : Any]) 3))
diff --git a/typed-racket-test/fail/erase-id-negative-prop.rkt b/typed-racket-test/fail/erase-id-negative-prop.rkt
new file mode 100644
index 000000000..91f73d0a5
--- /dev/null
+++ b/typed-racket-test/fail/erase-id-negative-prop.rkt
@@ -0,0 +1,16 @@
+#;
+(exn-pred #rx"expected: \\(-> Any Boolean : #:\\+ Bot")
+#lang typed/racket
+
+;; Same shape as subst-empty-obj-negative-prop.rkt, but the variable the
+;; latent prop speaks about goes out of scope via let, so the erasure
+;; happens through erase-identifiers rather than object substitution at
+;; an application. The prop (Number @ x) in the (negative) domain
+;; position must erase to Bot, not Top.
+
+(define g
+  (let ([x (ann "" Any)])
+    (lambda ([f : (Any -> Boolean : #:+ (Number @ x))])
+      (if (f x) (add1 x) 1))))
+
+(g (lambda ([w : Any]) #t))
diff --git a/typed-racket-test/fail/erase-kw-negative-prop.rkt b/typed-racket-test/fail/erase-kw-negative-prop.rkt
new file mode 100644
index 000000000..e7f09638d
--- /dev/null
+++ b/typed-racket-test/fail/erase-kw-negative-prop.rkt
@@ -0,0 +1,13 @@
+#;
+(exn-pred #rx"expected \\(-> Any Boolean : #:\\+ Bot")
+#lang typed/racket
+
+;; Keyword argument types are a negative position too: when x goes out
+;; of scope, the prop about it must erase to Bot.
+
+(define g
+  (let ([x (ann "" Any)])
+    (lambda (#:f [f : (-> Any Boolean : #:+ (Number @ x))])
+      (if (f x) (add1 x) 1))))
+
+(g #:f (lambda ([w : Any]) #t))
diff --git a/typed-racket-test/fail/erase-leq-negative-prop.rkt b/typed-racket-test/fail/erase-leq-negative-prop.rkt
new file mode 100644
index 000000000..ad2bfda30
--- /dev/null
+++ b/typed-racket-test/fail/erase-leq-negative-prop.rkt
@@ -0,0 +1,14 @@
+#;
+(exn-pred #rx"expected: \\(-> Any Boolean : #:\\+ Bot")
+#lang typed/racket #:with-refinements
+
+;; A linear inequality about x in a negative position must erase to Bot
+;; when x goes out of scope; erasing it to Top accepted the argument
+;; below and let the body conclude (<= x 0) for x = 5.
+
+(define g
+  (let ([x : Integer 5])
+    (lambda ([f : (-> ([w : Any]) Boolean #:+ (<= x 0))])
+      (if (f 0) (ann x (Refine [n : Integer] (<= n 0))) 0))))
+
+(g (lambda ([w : Any]) #t))
diff --git a/typed-racket-test/fail/erase-param-contravariant-prop.rkt b/typed-racket-test/fail/erase-param-contravariant-prop.rkt
new file mode 100644
index 000000000..8205bc4dc
--- /dev/null
+++ b/typed-racket-test/fail/erase-param-contravariant-prop.rkt
@@ -0,0 +1,16 @@
+#;
+(exn-pred #rx"expected \\(-> Any Boolean : #:\\+ Bot")
+#lang typed/racket
+
+;; The values a parameter accepts are a contravariant (negative)
+;; position, so a prop about x there must erase to Bot, not Top, when x
+;; goes out of scope.
+
+(define p
+  (let ([x : Any ""])
+    (define prm : (Parameterof (Any -> Boolean : #:+ (Number @ x)))
+      (make-parameter (lambda ([w : Any]) (number? x))))
+    (cons prm (lambda () (if ((prm) 0) (add1 x) 1)))))
+
+((car p) (lambda ([w : Any]) #t))
+((cdr p))
diff --git a/typed-racket-test/fail/ordinary-arrow-object-not-produced.rkt b/typed-racket-test/fail/ordinary-arrow-object-not-produced.rkt
new file mode 100644
index 000000000..1b9feb5a7
--- /dev/null
+++ b/typed-racket-test/fail/ordinary-arrow-object-not-produced.rkt
@@ -0,0 +1,10 @@
+#;
+(exn-pred #rx"expected: \\(-> Any Any : #:\\+ Top #:- Top #:object z\\)")
+#lang typed/racket
+
+(let ([z : Any 1])
+  ((lambda ([f : (Any -> Any : #:object z)])
+     (if (number? (f 0))
+         (+ z 1)
+         0))
+   (lambda ([x : Any]) 3)))
diff --git a/typed-racket-test/fail/ordinary-arrow-object-wrong-object.rkt b/typed-racket-test/fail/ordinary-arrow-object-wrong-object.rkt
new file mode 100644
index 000000000..84c018848
--- /dev/null
+++ b/typed-racket-test/fail/ordinary-arrow-object-wrong-object.rkt
@@ -0,0 +1,8 @@
+#;
+(exn-pred #rx"mismatch in object")
+#lang typed/racket
+
+(let ([z : Any 1]
+      [w : Any 2])
+  (ann (lambda ([x : Any]) w)
+       (Any -> Any : #:object z)))
diff --git a/typed-racket-test/fail/print-propositions-option.rkt b/typed-racket-test/fail/print-propositions-option.rkt
new file mode 100644
index 000000000..fa40f983a
--- /dev/null
+++ b/typed-racket-test/fail/print-propositions-option.rkt
@@ -0,0 +1,10 @@
+#;
+(exn-pred #rx"\\(-> Any Boolean : #:\\+ \\(: x String\\) #:- Top\\)")
+#lang typed/racket #:print-propositions
+
+;; With #:print-propositions, types in error messages include their
+;; latent propositions, which are otherwise omitted here.
+
+(define x : Any 1)
+(define f : (U Integer (-> Any Boolean : #:+ (: x String))) 1)
+(f 1)
diff --git a/typed-racket-test/fail/promote-invariant.rkt b/typed-racket-test/fail/promote-invariant.rkt
new file mode 100644
index 000000000..4381fc866
--- /dev/null
+++ b/typed-racket-test/fail/promote-invariant.rkt
@@ -0,0 +1,19 @@
+#;
+(exn-pred #rx"could not be applied")
+#lang typed/racket
+(require racket/flonum)
+
+;; Inferring map's result type eliminates id's type variables. Promoting
+;; (Mutable-HashTable k v) to (Mutable-HashTable Any Any) gave an alias
+;; through which anything could be stored into h, whose values typed
+;; code then trusted to be flonums. A type that mentions an eliminated
+;; variable in an invariant position must widen as a whole, here to
+;; Mutable-HashTableTop, and so inference fails.
+
+(: h (Mutable-HashTable Nothing Nothing))
+(define h (make-hash))
+(: id (All (k v) (-> (Mutable-HashTable k v) (Mutable-HashTable k v))))
+(define (id x) x)
+(hash-set! (car (map id (list h))) 1 "not a flonum")
+(for ([(k v) (in-hash h)])
+  (displayln (fl+ v 1.0)))
diff --git a/typed-racket-test/fail/subst-empty-obj-negative-prop.rkt b/typed-racket-test/fail/subst-empty-obj-negative-prop.rkt
new file mode 100644
index 000000000..3b86ed14d
--- /dev/null
+++ b/typed-racket-test/fail/subst-empty-obj-negative-prop.rkt
@@ -0,0 +1,15 @@
+#;
+(exn-pred #rx"expected: \\(-> Any Boolean : #:\\+ Bot")
+#lang typed/racket
+
+;; Substituting the empty object for x must not erase the latent prop
+;; (Number @ x) to Top when it occurs in a negative position (here, the
+;; domain of the function type for f). Erasing it to Top let this
+;; program typecheck and then crash at runtime with
+;; (add1 ""), since (λ ([w : Any]) true) never establishes (Number @ x).
+
+(((lambda ([x : Any])
+    (lambda ([f : (Any -> Boolean : #:+ (Number @ x))])
+      (if (f x) (add1 x) 1)))
+  (ann "" Any))
+ (λ ([w : Any]) true))
diff --git a/typed-racket-test/fail/subst-vector-invariant-prop.rkt b/typed-racket-test/fail/subst-vector-invariant-prop.rkt
new file mode 100644
index 000000000..986a8d5cd
--- /dev/null
+++ b/typed-racket-test/fail/subst-vector-invariant-prop.rkt
@@ -0,0 +1,17 @@
+#;
+(exn-pred #rx"vector-set!")
+#lang typed/racket
+
+;; Like erase-box-invariant-prop.rkt, but x is substituted away at an
+;; application rather than erased by let. The mutable half of the
+;; Vectorof type must widen to Mutable-VectorTop.
+
+(define p
+  ((lambda ([x : Any])
+     (define v : (Vectorof (Any -> Boolean : #:+ (Number @ x)))
+       (vector (lambda ([w : Any]) (number? x))))
+     (cons v (lambda () (if ((vector-ref v 0) 0) (add1 x) 1))))
+   (ann "" Any)))
+
+(vector-set! (car p) 0 (lambda ([w : Any]) #t))
+((cdr p))
diff --git a/typed-racket-test/fail/user-filter-with-bad-index-object.rkt b/typed-racket-test/fail/user-filter-with-bad-index-object.rkt
index a0f36f930..5bc17e857 100644
--- a/typed-racket-test/fail/user-filter-with-bad-index-object.rkt
+++ b/typed-racket-test/fail/user-filter-with-bad-index-object.rkt
@@ -1,5 +1,5 @@
 #;
-(exn-pred #rx"Proposition's object index 3 is larger than argument length 1")
+(exn-pred #rx"index \\(0 3\\) refers to argument 3, but the function type has only 1 argument")
 #lang typed/racket
 
 ;; This test ensures that a filter object like '3' is
diff --git a/typed-racket-test/succeed/dependent-function-outer-prop.rkt b/typed-racket-test/succeed/dependent-function-outer-prop.rkt
new file mode 100644
index 000000000..6b7047517
--- /dev/null
+++ b/typed-racket-test/succeed/dependent-function-outer-prop.rkt
@@ -0,0 +1,14 @@
+#lang typed/racket
+
+(: double-num? (-> ([x : Any])
+                   (-> ([y : Any]) Boolean #:+ (: x Number))))
+(define ((double-num? x) y) (number? x))
+
+(: double-num?/pos (-> Any (-> Any Boolean : #:+ (: (1 0) Number))))
+(define ((double-num?/pos x) y) (number? x))
+
+(: use-named (-> Any Any Number))
+(define (use-named x y)
+  (if ((double-num? x) y)
+      (+ x 1)
+      0))
diff --git a/typed-racket-test/succeed/ordinary-arrow-named-prop-object.rkt b/typed-racket-test/succeed/ordinary-arrow-named-prop-object.rkt
new file mode 100644
index 000000000..0023d5a57
--- /dev/null
+++ b/typed-racket-test/succeed/ordinary-arrow-named-prop-object.rkt
@@ -0,0 +1,8 @@
+#lang typed/racket
+
+(let ([z : Any 1])
+  ((lambda ([f : (Any -> Boolean : #:+ (: z Number))])
+     (if (f 0)
+         (+ z 1)
+         0))
+   (lambda ([x : Any]) (number? z))))
diff --git a/typed-racket-test/succeed/ordinary-arrow-object-produced.rkt b/typed-racket-test/succeed/ordinary-arrow-object-produced.rkt
new file mode 100644
index 000000000..1323f88d9
--- /dev/null
+++ b/typed-racket-test/succeed/ordinary-arrow-object-produced.rkt
@@ -0,0 +1,8 @@
+#lang typed/racket
+
+(let ([z : Any 1])
+  ((lambda ([f : (Any -> Any : #:object z)])
+     (if (number? (f 0))
+         (+ z 1)
+         0))
+   (lambda ([x : Any]) z)))
diff --git a/typed-racket-test/succeed/polar-subst.rkt b/typed-racket-test/succeed/polar-subst.rkt
new file mode 100644
index 000000000..b79f84643
--- /dev/null
+++ b/typed-racket-test/succeed/polar-subst.rkt
@@ -0,0 +1,49 @@
+#lang typed/racket
+
+;; Companion to fail/subst-empty-obj-negative-prop.rkt and
+;; fail/erase-id-negative-prop.rkt: polarity-aware erasure of the empty
+;; object must not reject these sound uses of latent props.
+
+;; a latent prop about a variable that stays in scope: nothing is
+;; erased, and the argument genuinely establishes (Number @ x)
+(define (f0 [x : Any]) : Number
+  ((lambda ([f : (Any -> Boolean : #:+ (Number @ x))])
+     (if (f x) (add1 x) 1))
+   (lambda ([w : Any]) (number? x))))
+
+;; positive erasure: props about an erased argument in result position
+;; weaken to Top and the application still typechecks
+(define (f1) : Boolean
+  ((lambda ([y : Any]) (number? y)) "hello"))
+
+;; the same, through let
+(define f2
+  (let ([x (ann 5 Any)])
+    (lambda () (number? x))))
+
+;; erasing a variable whose type already establishes the prop keeps the
+;; prop true, even in a negative position
+(define f3
+  (let ([x : Number 5])
+    (lambda ([f : (Any -> Boolean : #:+ (Number @ x))])
+      (if (f x) (add1 x) 1))))
+
+;; a box whose contents mention an erased variable widens to BoxTop,
+;; which can still be read
+(define b
+  (let ([x : Any ""])
+    (ann (box (lambda ([w : Any]) (number? x)))
+         (Boxof (Any -> Boolean : #:+ (Number @ x))))))
+
+;; the values a parameter produces are a positive position
+(define prm
+  (let ([x : Any ""])
+    (ann (make-parameter (lambda ([w : Any]) (number? x)))
+         (Parameterof (Any -> Boolean : #:+ (Number @ x))))))
+
+(f0 1)
+(f1)
+(f2)
+(f3 (lambda ([w : Any]) #t))
+(unbox (ann b BoxTop))
+((prm) 1)
diff --git a/typed-racket-test/unit-tests/infer-tests.rkt b/typed-racket-test/unit-tests/infer-tests.rkt
index 7e82e8387..4b617308f 100644
--- a/typed-racket-test/unit-tests/infer-tests.rkt
+++ b/typed-racket-test/unit-tests/infer-tests.rkt
@@ -14,6 +14,7 @@
   typed-racket/types/substitute
   typed-racket/types/numeric-tower
   typed-racket/types/utils
+  typed-racket/types/subtype
   typed-racket/types/abbrev)
 
 (provide tests)
@@ -91,7 +92,12 @@
          #,(syntax/loc stx
              (check-equal? promoted P "Promoted value doesn't match expected."))
          #,(syntax/loc stx
-             (check-equal? demoted D "Demoted value doesn't match expected.")))))))
+             (check-equal? demoted D "Demoted value doesn't match expected."))
+         ;; demotion and promotion must give a subtype and a supertype
+         #,(syntax/loc stx
+             (check-true (subtype demoted S-v) "Demoted value is not a subtype."))
+         #,(syntax/loc stx
+             (check-true (subtype S-v promoted) "Promoted value is not a supertype.")))))))
 
 (define pd-tests
   (test-suite
@@ -100,27 +106,31 @@
    (pd-t (-v a) () (-v a) (-v a))
    (pd-t (-v a) (a) -Bottom Univ)
    (pd-t (-v a) (b) (-v a) (-v a))
-   (pd-t (-vec (-v a)) (a) (-vec -Bottom) (-vec Univ))
-   (pd-t (-mvec (-lst (-v a))) (a) (-mvec -Bottom) (-mvec Univ))
+   ;; a type that mentions a in an invariant position is replaced as a
+   ;; whole by its top type (or Bottom)
+   (pd-t (-vec (-v a)) (a) (-ivec -Bottom) (Un (-ivec Univ) -Mutable-VectorTop))
+   (pd-t (-mvec (-lst (-v a))) (a) -Bottom -Mutable-VectorTop)
    (pd-t (-ivec (-lst (-v a))) (a) (-ivec (-lst -Bottom)) (-ivec (-lst Univ)))
    (pd-t (-vec (-v a)) (b) (-vec (-v a)) (-vec (-v a)))
 
-   (pd-t (-box (-v a)) (a) (-box -Bottom) (-box Univ))
-   (pd-t (-box (-lst (-v a))) (a) (-box -Bottom) (-box Univ))
+   (pd-t (-box (-v a)) (a) -Bottom -BoxTop)
+   (pd-t (-box (-lst (-v a))) (a) -Bottom -BoxTop)
    (pd-t (-box (-v a)) (b) (-box (-v a)) (-box (-v a)))
 
-   (pd-t (-channel (-v a)) (a) (-channel -Bottom) (-channel Univ))
-   (pd-t (-channel (-lst (-v a))) (a) (-channel -Bottom) (-channel Univ))
+   (pd-t (-channel (-v a)) (a) -Bottom -ChannelTop)
+   (pd-t (-channel (-lst (-v a))) (a) -Bottom -ChannelTop)
    (pd-t (-channel (-v a)) (b) (-channel (-v a)) (-channel (-v a)))
 
-   (pd-t (-thread-cell (-v a)) (a) (-thread-cell -Bottom) (-thread-cell Univ))
-   (pd-t (-thread-cell (-lst (-v a))) (a) (-thread-cell -Bottom) (-thread-cell Univ))
+   (pd-t (-thread-cell (-v a)) (a) -Bottom -ThreadCellTop)
+   (pd-t (-thread-cell (-lst (-v a))) (a) -Bottom -ThreadCellTop)
    (pd-t (-thread-cell (-v a)) (b) (-thread-cell (-v a)) (-thread-cell (-v a)))
 
-   (pd-t (-HT (-v a) (-v a)) (a) (-HT -Bottom -Bottom) (-HT Univ Univ))
+   (pd-t (-HT (-v a) (-v a)) (a)
+         (-Immutable-HT -Bottom -Bottom)
+         (Un (-Immutable-HT Univ Univ) -Mutable-HashTableTop -Weak-HashTableTop))
    (pd-t (-HT (-lst (-v a)) (-lst (-v a))) (a)
-         (Un (-Immutable-HT (-lst -Bottom) (-lst -Bottom)) (-Mutable-HT -Bottom -Bottom) (-Weak-HT -Bottom -Bottom))
-         (Un (-Immutable-HT (-lst Univ) (-lst Univ)) (-Mutable-HT Univ Univ) (-Weak-HT Univ Univ)))
+         (-Immutable-HT (-lst -Bottom) (-lst -Bottom))
+         (Un (-Immutable-HT (-lst Univ) (-lst Univ)) -Mutable-HashTableTop -Weak-HashTableTop))
    (pd-t (-HT (-v a) (-v a)) (b) (-HT (-v a) (-v a)) (-HT (-v a) (-v a)))
 
    (pd-t (-Param (-v a) (-v b)) (a b) (-Param Univ -Bottom) (-Param -Bottom Univ))
@@ -132,6 +142,13 @@
          (->* (list (-lst Univ)) (-lst Univ) (-lst -Bottom))
          (->* (list (-lst -Bottom)) (-lst -Bottom) (-lst Univ)))
 
+   ;; propositions about a are strengthened when demoting and weakened
+   ;; when promoting, rather than dropping the function's case
+   (pd-t (-> Univ -Boolean : (-PS (-is-type 0 (-v a)) (-not-type 0 (-v a)))) (a)
+         (make-Fun (list (-Arrow (list Univ)
+                                 (make-Values (list (make-Result -Boolean -ff-propset -empty-obj))))))
+         (-> Univ -Boolean))
+
    (pd-t (->key #:a (-lst (-v a)) #t #:b (-lst (-v a)) #f -Symbol) (a)
          (->key #:a (-lst Univ) #t #:b (-lst Univ) #f -Symbol)
          (->key #:a (-lst -Bottom) #t #:b (-lst -Bottom) #f -Symbol))
diff --git a/typed-racket-test/unit-tests/interactive-tests.rkt b/typed-racket-test/unit-tests/interactive-tests.rkt
index f1ce1aefb..f4f873ccb 100644
--- a/typed-racket-test/unit-tests/interactive-tests.rkt
+++ b/typed-racket-test/unit-tests/interactive-tests.rkt
@@ -150,6 +150,8 @@
       (:type Byte))
     (test-form (regexp-quote "(U 0 1 Byte-Larger-Than-One")
       (:type #:verbose Byte))
+    (test-form (regexp-quote "#:+ (: (0 1) String)")
+      (:type #:verbose (-> Any Any Boolean : #:+ (: (0 1) String))))
     (test-form-exn #rx":type.*applied to arguments"
       :type)
     (test-form-exn #rx":type.*only valid at the top-level"
@@ -163,6 +165,14 @@
 
     (test-form #rx"Positive-Index"
       (:print-type (+ 1 1)))
+    ;; #:verbose expands type aliases
+    (test-form (regexp-quote "Exact-Complex")
+      (:print-type #:verbose number?))
+    ;; and prints latent propositions and objects
+    (test-form (regexp-quote "#:+ (: (0 0) String) #:- (! (0 0) String)")
+      (:print-type #:verbose (lambda ([x : Any] [y : Any]) (string? x))))
+    (test-form (regexp-quote "#:object (0 1)")
+      (:print-type #:verbose (lambda ([x : Any] [y : Any]) y)))
 
     (test-form #rx"\\*"
       (:kind Number))
@@ -224,6 +234,8 @@
       (:print-type))
     (test-form-exn #rx"exactly one argument"
       (:print-type 1 2))
+    (test-form-exn #rx"exactly one argument"
+      (:print-type #:verbose))
 
     (test-form (regexp-quote "(-> 4 Zero Zero)")
       (:query-type/args * 4 0))
diff --git a/typed-racket-test/unit-tests/parse-type-tests.rkt b/typed-racket-test/unit-tests/parse-type-tests.rkt
index 42bca6950..1a3824c45 100644
--- a/typed-racket-test/unit-tests/parse-type-tests.rkt
+++ b/typed-racket-test/unit-tests/parse-type-tests.rkt
@@ -18,6 +18,7 @@
            typed-racket/types/numeric-tower
            typed-racket/types/resolve
            typed-racket/types/prop-ops
+           typed-racket/types/tc-result
            (submod typed-racket/base-env/base-types initialize)
            (rename-in typed-racket/types/abbrev
                       [Un t:Un] [-> t:->] [->* t:->*]))
@@ -93,7 +94,7 @@
 (define-for-syntax B -Boolean)
 (define-for-syntax Sym -Symbol)
 
-(define tests
+(define type-tests
   (pt-tests
    "parse-type tests"
    [FAIL UNBOUND]
@@ -214,13 +215,34 @@
     (make-pred-ty -Number)]
    [(-> Any Boolean : #:+ (Number @ 0) #:- (! Number @ 0))
     (make-pred-ty -Number)]
+   [(Any -> Boolean : #:+ (: (0 0) Number) #:- (! (0 0) Number))
+    (make-pred-ty -Number)]
+   [(Any -> Boolean : #:+ (and Number (! Integer)) #:- (or Integer (! Number)))
+    (t:->* (list Univ) -Boolean
+           : (-PS (-and (-is-type 0 -Number)
+                        (-not-type 0 -Int))
+                  (-or (-is-type 0 -Int)
+                       (-not-type 0 -Number))))]
    [(Any -> Boolean : #:+ (! Number @ 0) #:- (Number @ 0))
     (t:->* (list Univ) -Boolean : (-PS (-not-type 0 -Number) (-is-type 0 -Number)))]
    [(-> Any Boolean : #:+ (! Number @ 0) #:- (Number @ 0))
     (t:->* (list Univ) -Boolean : (-PS (-not-type 0 -Number) (-is-type 0 -Number)))]
+   [(-> Any Any : #:object not-mutated-var)
+    (t:->* (list Univ) Univ : (-PS -tt -tt) : (-id-path #'not-mutated-var))]
+   [(-> Any Any : #:object (0 0))
+    (t:->* (list Univ) Univ : (-PS -tt -tt) : (-arg-path 0 0))]
    [(-> Any (-> Any Boolean : #:+ (Number @ 1 0) #:- (! Number @ 1 0)))
     (t:-> Univ
           (t:->* (list Univ) -Boolean : (-PS (-is-type (cons 1 0) -Number) (-not-type (cons 1 0) -Number))))]
+   [(-> Any (-> Any Boolean : #:+ (Number @ (1 0)) #:- (! Number @ (1 0))))
+    (t:-> Univ
+          (t:->* (list Univ) -Boolean : (-PS (-is-type (cons 1 0) -Number) (-not-type (cons 1 0) -Number))))]
+   [(-> Any (-> Any Boolean : #:+ (: (1 0) Number) #:- (! (1 0) Number)))
+    (t:-> Univ
+          (t:->* (list Univ) -Boolean : (-PS (-is-type (cons 1 0) -Number) (-not-type (cons 1 0) -Number))))]
+   [(-> Any (-> Any Any : #:object (1 0)))
+    (t:-> Univ
+          (t:->* (list Univ) Univ : (-PS -tt -tt) : (-arg-path 0 1)))]
    [(-> Any Any (-> Any Boolean : #:+ (Number @ 1 1) #:- (! Number @ 1 1)))
     (t:-> Univ Univ
           (t:->* (list Univ) -Boolean : (-PS (-is-type (cons 1 1) -Number) (-not-type (cons 1 1) -Number))))]
@@ -247,13 +269,63 @@
    [FAIL (Any -> Any #:object 0) #:msg "expected the identifier `:'"]
    [FAIL (-> Any Any #:+ (String @ x)) #:msg "expected the identifier `:'"]
    [FAIL (-> Any Boolean : #:+ (Number @ 1 0) #:- (! Number @ 1 0))
-         #:msg "Index 1 used in"]
+         #:msg "index \\(1 0\\) used in a proposition"]
    [FAIL (-> Any (-> Any Boolean : #:+ (Number @ 1 1) #:- (! Number @ 1 1)))
-         #:msg "larger than argument length"]
+         #:msg "has only 1 argument"]
+   ;; legacy propositions nested inside new-style connectives
+   [(-> Any Any Boolean : #:+ (and (Number @ 0) (String @ 1)))
+    (t:-> Univ Univ -Boolean : (-PS (-and (-is-type 0 -Number) (-is-type 1 -String)) -tt))]
+   [(-> Any Boolean : #:+ (or (! Number @ 0) (Integer @ 0)))
+    (t:-> Univ -Boolean : (-PS (-or (-not-type 0 -Number) (-is-type 0 -Int)) -tt))]
+   ;; a bare natural number object is the legacy notation for an argument
+   [(-> Any Any : #:object 0)
+    (t:->* (list Univ) Univ : (-PS -tt -tt) : (-arg-path 0 0))]
+   [FAIL (-> Any Any : #:object 1)
+         #:msg "has only 1 argument"]
+   ;; index objects must refer to an argument of an enclosing function type
+   [FAIL (-> Any Boolean : #:+ (: (3 7) String))
+         #:msg "only within 1 enclosing function type"]
+   [FAIL (-> Any Boolean : #:+ (: (0 5) String))
+         #:msg "has only 1 argument"]
+   [FAIL (-> Any (Refine [n : Any] (: (0 0) String)))
+         #:msg "refers to the variable of a Refine type"]
+   [(-> Any (Refine [n : Any] (: (1 0) String)))
+    (t:-> Univ (-refine/fresh n Univ (-is-type (cons 1 0) -String)))]
+   ;; a function type in a domain is not underneath the enclosing
+   ;; function's binder, so it cannot refer to that function's arguments
+   [FAIL (-> (-> Any Boolean : #:+ (: (1 0) String)) Any)
+         #:msg "only within 1 enclosing function type"]
+   [FAIL (-> ([x : (-> Any Boolean : #:+ (: (1 0) String))]) Any)
+         #:msg "may not be used in the argument types of a dependent function"]
+   ;; paths over index objects use the arguments' types
+   [(-> (Pairof Any Any) Boolean : #:+ (: (car (0 0)) Number))
+    (t:-> (-pair Univ Univ) -Boolean
+          : (-PS (-is-type (-car-of (-arg-path 0 0)) -Number) -tt))]
+   [FAIL (-> Any Boolean : #:+ (: (car (0 0)) Number))
+         #:msg "car expects a pair"]
+   ;; errors inside a recognized proposition are reported as such, not
+   ;; as errors parsing a type
+   [FAIL (-> Any Boolean : #:+ (and (: (car (0 0)) Number)))
+         #:msg "car expects a pair"]
+   [FAIL (-> Boolean : #:+ String)
+         #:msg "needs a default subject"]
+   [FAIL (-> Any Any : #:object mutated-var)
+         #:msg "may not reference identifiers that are mutated"]
+   [FAIL (-> Any Any : #:object unbound)
+         #:msg "may not reference identifiers that are unbound"]
 
 
    [(Any -> Boolean : #:+ (Symbol @ not-mutated-var))
     (t:-> Univ -Boolean : (-PS (-is-type (-id-path #'not-mutated-var) -Symbol) -tt))]
+   [(Any -> Boolean : #:+ (: not-mutated-var Symbol) #:- (! not-mutated-var Symbol))
+    (t:-> Univ -Boolean
+          : (-PS (-is-type (-id-path #'not-mutated-var) -Symbol)
+                 (-not-type (-id-path #'not-mutated-var) -Symbol)))]
+   [(Any -> Boolean : #:+ (and (: not-mutated-var Symbol) (! not-mutated-var String)))
+    (t:-> Univ -Boolean
+          : (-PS (-and (-is-type (-id-path #'not-mutated-var) -Symbol)
+                       (-not-type (-id-path #'not-mutated-var) -String))
+                 -tt))]
    [FAIL (Any -> Boolean : #:+ (Symbol @ mutated-var))
          #:msg "may not reference identifiers that are mutated"]
    [(Any -> Boolean : #:+ (! Symbol @ not-mutated-var))
@@ -307,11 +379,14 @@
     (->optkey -Integer [-String] #:bar -Integer #t #:foo -Integer #f -Void)]
    [(->* (#:bar Integer Integer) (#:foo Integer String) Void)
     (->optkey -Integer [-String] #:bar -Integer #t #:foo -Integer #f -Void)]
-   [(->* (Any (-> Any Boolean : #:+ (String @ 1 0))) Void)
-    (t:-> Univ (t:->* (list Univ) -Boolean : (-PS (-is-type (cons 1 0) -String) -tt))
-          -Void)]
-   [FAIL (->* (Any (-> Any Boolean : #:+ (String @ 2 0))) Void)
-         #:msg "Index 2 used in"]
+   ;; the domains of a function type are not underneath its binder, so a
+   ;; function type in a domain cannot refer to the outer arguments
+   [FAIL (->* (Any (-> Any Boolean : #:+ (String @ 1 0))) Void)
+         #:msg "index \\(1 0\\) used in a proposition"]
+   [(->* (Any) (-> Any Boolean : #:+ (String @ 1 0)))
+    (t:-> Univ (t:->* (list Univ) -Boolean : (-PS (-is-type (cons 1 0) -String) -tt)))]
+   [FAIL (->* (Any) (-> Any Boolean : #:+ (String @ 2 0)))
+         #:msg "index \\(2 0\\) used in a proposition"]
 
    [(Opaque foo?) (make-Opaque #'foo?)]
    ;; PR 14122
@@ -372,6 +447,7 @@
 
    [(Some (X) (-> Number (-> X Number) : X)) (-some (X) (t:-> -Number (t:-> X -Number) : (-PS (-is-type 0 X) (-not-type 0 X))))]
    [(-> Number (Some (X) (-> X Number) : #:+ X)) (t:-> -Number (-some-res (X) (t:-> X -Number) : #:+ X))]
+   [(-> Number (Some (X) (-> X Number) : #:+ (: (0 0) X))) (t:-> -Number (-some-res (X) (t:-> X -Number) : #:+ X))]
 
    ;;; Classes
    [(Class) (-class)]
@@ -520,6 +596,7 @@
    [(Refine [x : Number] Top) -Number]
    [(Refine [x : Number] Bot) -Bottom]
    ;; simplify props about subject
+   [(Refine [x : Any] String) -String]
    [(Refine [x : Any] (: x String)) -String]
    [(Refine [x : Integer] (: x Integer)) -Int]
    [(Refine [x : Integer] (: x Symbol)) -Bottom]
@@ -680,10 +757,24 @@
         Boolean
         #:+ (: x Integer))
     (t:-> Univ -Boolean : (-PS (-is-type (cons 0 0) -Int) -tt))]
+   [(-> ([x : Any])
+        Boolean
+        #:+ Integer)
+    (t:-> Univ -Boolean : (-PS (-is-type (cons 0 0) -Int) -tt))]
+   [(-> ([x : Any])
+        Boolean
+        #:+ (and Number (! Integer)))
+    (t:-> Univ -Boolean : (-PS (-and (-is-type (cons 0 0) -Number)
+                                      (-not-type (cons 0 0) -Int))
+                               -tt))]
    [(-> ([x : Any])
         Boolean
         #:- (! x Integer))
     (t:-> Univ -Boolean : (-PS -tt (-not-type (cons 0 0) -Int)))]
+   [(-> ([x : Any])
+        Boolean
+        #:- Integer)
+    (t:-> Univ -Boolean : (-PS -tt (-is-type (cons 0 0) -Int)))]
    [(-> ([x : Any])
         Boolean
         #:+ (: x Integer)
@@ -700,6 +791,17 @@
           : (-PS (-is-type (cons 0 0) -Int)
                  (-is-type (cons 0 1) -Int))
           : (-id-path (cons 0 0)))]
+   [(-> ([x : Any])
+        #:pre (x) Number
+        Boolean)
+    (make-DepFun (list Univ)
+                 (-is-type (cons 0 0) -Number)
+                 (-values -Boolean))]
+   [FAIL (-> ([x : Any]
+              [y : Any])
+             Boolean
+             #:+ Integer)
+         #:msg "needs a default subject"]
    ;; simple dependencies
    [(-> ([v : (Vectorof Any)]
          [i : (v) (Refine [n : Integer] (<= n (vector-length v)))])
@@ -902,6 +1004,80 @@
              Any)]
    [FAIL (-> ([x : Integer]
               [y : Integer])
-             (Refine [x : Univ] (<= x 42)))]))
+             (Refine [x : Univ] (<= x 42)))]
 
-;; FIXME - add tests for parse-values-type, parse-tc-results
+   ;; Values and AnyValues proposition syntax
+   [(-> Any (AnyValues : (: (0 0) String)))
+    (t:-> Univ (-AnyValues (-is-type (cons 0 0) -String)))]
+   [(-> Any (values (String : #:+ (: (0 0) String) #:- Top)))
+    (t:-> Univ (-values (-result -String (-PS (-is-type (cons 0 0) -String) -tt))))]
+   [(-> Any (values (String : #:+ String #:- Top #:object (0 0))))
+    (t:-> Univ (-values (-result -String (-PS (-is-type 0 -String) -tt) (-arg-path 0 0))))]
+   ;; as elsewhere in a range, a bare type refers to the first argument
+   [(-> Any (AnyValues : String))
+    (t:-> Univ (-AnyValues (-is-type (cons 0 0) -String)))]
+   [FAIL (-> (AnyValues : String))
+         #:msg "needs a default subject"]
+   [(-> Any Any (values (Boolean : #:+ (: (0 1) String)) Any))
+    (t:-> Univ Univ (-values (list (-result -Boolean (-PS (-is-type (cons 0 1) -String) -tt))
+                                   (-result Univ))))]
+   ;; a single-valued range of a dependent function keeps the result's
+   ;; propositions and object
+   [(-> ([x : Any]) (values (Boolean : #:+ (: x String))))
+    (t:-> Univ -Boolean : (-PS (-is-type (cons 0 0) -String) -tt))]
+   [(-> ([x : Any]) (values (Boolean : #:+ (: x String))) #:- (! x Number))
+    (t:-> Univ -Boolean : (-PS (-is-type (cons 0 0) -String) (-not-type (cons 0 0) -Number)))]
+   [(-> ([x : Any]) (values (Any : #:object x)))
+    (t:-> Univ Univ : (-PS -tt -tt) : (-arg-path 0 0))]
+   [FAIL (-> ([x : Any] [y : Any]) (values (Any : #:object x)) #:object y)
+         #:msg "specifies its object twice"]))
+
+(define-syntax (tcr-test stx)
+  (syntax-parse stx
+    [(_ (~datum FAIL) s:expr #:msg msg:expr)
+     (quasisyntax/loc stx
+       (test-case #,(format "~a" (syntax->datum #'s))
+         (define actual-message
+           (phase1-phase0-eval
+             (with-handlers ([exn:fail:syntax? (lambda (exn) #`#,(exn-message exn))])
+               (parameterize ([delay-errors? #f])
+                 (parse-tc-results (quote-syntax s)))
+               #'#f)))
+         (unless (and actual-message (regexp-match? msg actual-message))
+           (with-check-info (['expected msg] ['actual actual-message])
+             (fail-check "parse-tc-results did not raise the expected error")))))]
+    [(_ s:expr val:expr)
+     (quasisyntax/loc stx
+       (test-case #,(format "~a" (syntax->datum #'s))
+         (define-values (expected actual same?)
+           (phase1-phase0-eval
+             (parameterize ([delay-errors? #f])
+               (define expected val)
+               (define actual (parse-tc-results (quote-syntax s)))
+               #`(values #,expected #,actual #,(equal? actual expected)))))
+         (unless same?
+           (with-check-info (['expected expected] ['actual actual])
+             (fail-check "Unequal tc-results")))))]))
+
+;; expected types of expressions, as written in ann
+(define tc-results-tests
+  (test-suite
+   "parse-tc-results tests"
+   (tcr-test String (ret -String #f #f))
+   (tcr-test (values String Symbol) (ret (list -String -Symbol) (list #f #f) (list #f #f)))
+   (tcr-test (Boolean : #:+ (: not-mutated-var String))
+             (ret -Boolean (-PS (-is-type (-id-path #'not-mutated-var) -String) -tt)))
+   (tcr-test (Any : #:object not-mutated-var)
+             (ret Univ -tt-propset (-id-path #'not-mutated-var)))
+   (tcr-test (AnyValues : (: not-mutated-var String))
+             (-tc-any-results (-is-type (-id-path #'not-mutated-var) -String)))
+   ;; outside any function type, there is no default subject and no
+   ;; argument for an index to refer to
+   (tcr-test FAIL (Boolean : #:+ String) #:msg "needs a default subject")
+   (tcr-test FAIL (Any : #:object 0) #:msg "only within 0 enclosing function types")
+   (tcr-test FAIL (Boolean : #:+ (: (0 0) String)) #:msg "only within 0 enclosing function types")))
+
+(define tests
+  (test-suite "parse-type"
+              type-tests
+              tc-results-tests))
diff --git a/typed-racket-test/unit-tests/type-printer-tests.rkt b/typed-racket-test/unit-tests/type-printer-tests.rkt
index 1edcf39e0..d8f200b0c 100644
--- a/typed-racket-test/unit-tests/type-printer-tests.rkt
+++ b/typed-racket-test/unit-tests/type-printer-tests.rkt
@@ -137,7 +137,7 @@
     (check-prints-as? (-poly (a) (-> a -Void)) "(All (a) (-> a Void))")
     (check-prints-as? (-> -Input-Port (make-Values (list (-result -String -true-propset)
                                                          (-result -String -true-propset))))
-                      "(-> Input-Port (values (String : (Top | Bot)) (String : (Top | Bot))))")
+                      "(-> Input-Port (values (String : #:+ Top #:- Bot) (String : #:+ Top #:- Bot)))")
     (check-prints-as? (make-pred-ty -String)
                       "(-> Any Boolean : String)")
     (check-prints-as? (asym-pred Univ -Boolean (-PS (-is-type 0 -String) -tt))
@@ -181,6 +181,8 @@
     (check-prints-as? (-AnyValues -tt) "AnyValues")
     (check-prints-as? (-AnyValues (-is-type '(0 . 0) -String))
                       "(AnyValues : (: (0 0) String))")
+    (check-prints-as? (-values -String (-PS (-is-type '(0 . 0) -String) -tt) -empty-obj)
+                      "(String : #:+ (: (0 0) String) #:- Top)")
 
     (check-prints-as?
      (make-Fun (list (-Arrow (list Univ) #:rest Univ -String)
diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt
index 0e267dab2..cb72c811c 100644
--- a/typed-racket-test/unit-tests/typecheck-tests.rkt
+++ b/typed-racket-test/unit-tests/typecheck-tests.rkt
@@ -2611,6 +2611,22 @@
            (if (f 'dummy) (add1 x) 2))
          (t:-> Univ -Integer : -true-propset)]
 
+        [tc-e
+         (let ([z : Any 1])
+           ((lambda: ([f : (Any -> Any : #:object z)])
+              (if (number? (f 0))
+                  (+ z 1)
+                  0))
+            (lambda: ([x : Any]) z)))
+         -Number]
+
+        [tc-e
+         (let ([z : Any 1])
+           ((lambda: ([f : (Any -> Boolean : #:+ (: z Number))])
+              (if (f 0) (+ z 1) 0))
+            (lambda: ([x : Any]) (number? z))))
+         -Number]
+
         ;; This test ensures that curried predicates have
         ;; the correct props so that they can be used for
         ;; occurrence typing.
@@ -2651,6 +2667,26 @@
         ;; type doesn't really matter, just make sure it typechecks
         -Void]
 
+       [tc-e
+        (let ()
+          (: double-num? (-> ([x : Any])
+                             (-> ([y : Any]) Boolean #:+ (: x Number))))
+          (define ((double-num? x) y) (number? x))
+          (: use (-> Any Any Number))
+          (define (use x y)
+            (if ((double-num? x) y)
+                (+ x 1)
+                0))
+          (void))
+        -Void]
+
+       [tc-e
+        (let ()
+          (: double-num?/pos (-> Any (-> Any Boolean : #:+ (: (1 0) Number))))
+          (define ((double-num?/pos x) y) (number? x))
+          (void))
+        -Void]
+
        ;; Unit test for PR 13298. Should raise an unbound id error
        ;; instead of just allowing `x` to be undefined
        [tc-err (let () (: x Number) 3)]
diff --git a/typed-racket/info.rkt b/typed-racket/info.rkt
index 3cf993f0e..17ab9f784 100644
--- a/typed-racket/info.rkt
+++ b/typed-racket/info.rkt
@@ -11,7 +11,7 @@
 
 (define pkg-authors '(samth stamourv))
 
-(define version "1.15")
+(define version "1.16")
 
 (define license
   '(Apache-2.0 OR MIT))