Fix errors discovered during formalization

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))

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

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

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)].
 

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.

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))

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