Repository navigation
Conversation
Substituting the empty object for a variable (because the actual
argument has no object, or because a local variable goes out of scope)
erased props mentioning that variable to TrueProp everywhere: the
TypeProp/NotTypeProp/LeqProp constructors collapse any prop over an
Empty object to tt. That is only sound in positive positions, where the
prop is a fact the typechecker learns. In negative positions --
underneath a function type's domain, or a negated type -- the prop is
an obligation the context must discharge, and erasing it to tt removes
the obligation. This program typechecked and then crashed at runtime,
because (lambda ([w : Any]) true) never establishes (Number @ x):
(((lambda ([x : Any])
(lambda ([f : (Any -> Boolean : #:+ (Number @ x))])
(if (f x) (add1 x) 1)))
(ann "" Any))
(lambda ([w : Any]) true))
The substitution in figure 8 of "Logical Types for Untyped Languages"
(ICFP 2010) is polarity-indexed for exactly this reason, as is object
substitution in the Rebuild λTR formalization, but
instantiate-obj+simplify did not implement the polarity.
One traversal, subst-objs+simplify, now performs every such
substitution: instantiating a function's range at an application,
erasing let- and named-let-bound variables, and substituting the
variables of letrec clauses (and so of internal definitions), which
previously went through substitute-names. It carries the polarity,
which flips at Arrow and DepFun domains (including rest and keyword
arguments and preconditions) and underneath the type of a NotTypeProp.
Props over an erased object become ff rather than tt in negative
positions, including props over linear expressions and LeqProps, and a
result whose object is erased in a negative position gets ff props,
since its object requirement can no longer be stated (λTR uses the
bottom object here).
Underneath an invariant type parameter, as in Boxof or Vectorof,
neither weakening nor strengthening is sound: erasing to tt let a box
escape with type (Boxof (-> Any Boolean)), so a function that never
establishes (Number @ x) could be stored into it and then trusted by a
closure that still had x in scope. The traversal follows the variances
of structural types and of user-defined type constructors, flipping at
contravariant parameters such as a Parameterof's input. When an erased
object occurs underneath an invariant parameter, it widens the
enclosing type to its top type (BoxTop, Mutable-VectorTop, ...) in a
positive position, or to Bottom in a negative one, which preserves
λTR's subtyping-for-erasure lemma A⁻ <: A <: A⁺. Mutable struct and
prefab fields, classes, objects, units, and applications of type
constructors with unknown variance are treated as invariant.
Erasure now also uses the erased variables' types, as application
already used the arguments' types, so a prop that a variable's type
establishes stays true: erasing x : Number from (Number @ x) gives tt
even in a negative position. NotTypeProps whose negated type cannot
overlap the substituted value's type simplify to tt for the same
reason.
Inferring the instantiation of a polymorphic function whose argument is
itself polymorphic, as in (map f xs) where f has an All type, eliminates
f's type variables by promoting the types they occur in to supertypes,
or demoting them to subtypes, that do not mention them (Pierce and
Turner's local type inference). Both directions had holes.
Promotion replaced a variable in an invariant position with Any, so
(Mutable-HashTable k v) became (Mutable-HashTable Any Any), which is
not a supertype. This program typechecked, stored a string into h
through the resulting alias, and then handed it to fl+ as a flonum:
(: 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)))
A type that mentions an eliminated variable in an invariant position now
becomes its top type (Mutable-HashTableTop here) when promoted and
Bottom when demoted, which also covers mutable structs and prefabs,
classes, units, and applications of type constructors with invariant or
unknown variance; these used to be treated as covariant.
Demotion dropped any case of a function type whose propositions
mentioned an eliminated variable, which yields a supertype, not a
subtype: with no cases left, every function satisfied it. This program
passed a function on integers where (-> Any Boolean : a) was expected,
and call then applied it to a string:
(: call (All (a) (-> (-> Any Boolean : a) Boolean)))
(define (call p) (p "hello"))
(map call (list (λ ([x : Integer]) (= (add1 x) 1))))
Propositions are now changed like any other type in the range, so a
proposition about an eliminated variable is weakened when promoting and
strengthened when demoting, with the polarity flipped underneath a
NotTypeProp. Dependent function types now get contravariant domains as
well. As a result, inference rejects some programs it accepted only by
dropping such a case, such as (map call (list string?) (list "s")) for a
call of type (All (a) (-> (-> Any Boolean : a) Any (U a #f))); no
subtype of (-> Any Boolean : a) without a admits string?, so such a
program needs an explicit instantiation.
Like object substitution, elimination finds a type's top type and the
variances of its parameters with the helpers in types/variance.rkt.
Ordinary function types, dependent function types, and Refine types each parsed propositions with their own syntax: -> accepted only the legacy forms such as (Number @ 0), while the others accepted (: obj type), (! obj type), and the logical connectives. One syntax class now parses propositions everywhere, accepting the legacy forms at any depth, so (and (Number @ 0) (String @ 1)) still works, and new code can write (-> Any Any Boolean : #:+ (: (0 1) String)). A bare type proposition is about the default subject: the first argument of an ordinary function type, the only argument in scope of a dependent function type, or the variable of a Refine. Without a default subject, as in a function type with no arguments, the parser reports an error instead of producing a proposition about a nonexistent argument. The symbolic object (depth arg) refers to argument arg of the function type depth scopes out, which matches how the printer writes these objects, so printed types can be read back. The parser now tracks the scopes that actually shift these De Bruijn indices: a function type's range and latent propositions, but not its domains, and a Refine's proposition. Previously it counted a function type while parsing its domains, so a function type in a domain could refer to arguments that its propositions would never see. Index objects outside any scope, or naming a Refine's variable, are rejected, and paths such as (car (0 0)) check the argument's type. #:object is now honored in ordinary function types; it was silently ignored. As the old documentation promised, a natural number there refers to an argument, so #:object 0 means (0 0). Values results in function ranges, and the expected types of ann, may carry latent propositions and an object, written as in function ranges: (Boolean : #:+ (: x String)). A single-valued range of a dependent function keeps such propositions rather than dropping them. Propositions in a recognized form report errors in that form; before, a mistake inside (: obj type) fell through to the bare-type case and was reported as a malformed type.
The printer wrote latent propositions as (p+ | p-) followed by an
object, which no parser accepts. It now writes them as function ranges
are written, #:+ p+ #:- p- #:object o, so printed types can be read
back.
Type error messages hid the propositions of the types they compared,
so a mismatch caused by propositions alone read as nonsense, such as
expected: (-> Any Boolean)
given: (-> Any True)
Messages that compare an expected type with a given one now print the
propositions of both whenever the expected type has some that would
otherwise be omitted; only those can cause a mismatch by themselves:
expected: (-> Any Boolean : #:+ Bot #:- Top)
given: (-> Any True)
The #:print-propositions language option prints propositions in every
type a module's error messages show, and :print-type accepts #:verbose,
as :type does, to print them at the REPL.
Record the proposition and inference changes in HISTORY and in the documentation's history notes.
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
Resyntax analyzed 41 files in this pull request and found no issues.
capfredf
reviewed
Oct 5, 2026
| (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))) |
Member
There was a problem hiding this comment.
-empty-obj x pol is fine, but using top and bottom obj seems to make the code a bit clearer to me(FWIW, I chose the latter in typed/rhombus)
capfredf
approved these changes
Oct 5, 2026
Member
|
Can we split the parser fix and soundness fix? |
capfredf
self-requested a review
October 6, 2026 12:14
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
During the course of writing https://arxiv.org/abs/2609.16299 we discovered several soundness and other bugs in Typed Racket,
These commits resolve them. This is an initial PR and I expect changes during review.