Pith. sign in

REVIEW 4 major objections 4 minor 21 references

Undecidability of $D_{<:}$ and Its Decidable Fragments

T0 review · 4 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper proves that subtyping and type checking in D<: are undecidable, and that two fragments obtained by removing the bad-bounds rule are decidable, coinciding exactly with the fragments decided by step and stare-at subtyping.

desk verdict First credible undecidability proof for D<: with a clean decidable-fragment boundary, but the central transitivity theorem is only sketched and the promised Coq/Agda artifact is absent in v1. read the letter →

arxiv 1908.05294 v1 pith:YCQ7MYKV submitted 2019-08-14 cs.PL

Jason Hu , Ondřej Lhoták This is my paper · ORCID
classification cs.PL
keywords D<:DependentObjectTypesundecidabilitysubtypingtypecheckingbadboundskernelstare-at
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

D<: is a syntactic core of DOT, the calculus behind Scala 3, and whether its type system can be mechanized has been open. This paper proves that both subtyping and type checking in D<: are undecidable, by reducing an undecidable fragment of F<: subtyping to D<: through a newly discovered normal form. The normal form replaces the transitivity rule by an explicit bad-bounds rule, making the source of undecidability crisp. Once that rule is removed, two decidable fragments, kernel and strong kernel D<:, are identified, and the paper exhibits terminating algorithms that decide exactly those fragments.

What carries the argument

The load-bearing object is the D<: normal form, a reformulation of D<: subtyping whose premises mention only subterms of the conclusion but which defines the same relation as the original system. It makes bad bounds explicit as a single rule, BB: when a context variable x is declared with both {A:S..⊤} and {A:⊥..U}, the rule concludes S<:U, capturing exactly the transitivity through the path type x.A that otherwise lets arbitrary lower bounds leak above arbitrary upper bounds. Equivalence with the original rules is obtained through a lexicographic induction that proves transitivity and narrowing together, using type declaration hierarchies for nested declarations. The undecidability reduction maps every type variable X of F^-<: to a path x_X.A with declaration {A:⊥..[T]}, so that D<: derivations in the image can be inverted back to F^-<: derivations.

What would settle it

Search restrictively over small well-formed contexts and types for a subtyping judgment provable in the original D<: rules via transitivity through an arbitrary middle type but not derivable in the normal-form rules with BB; any such judgment would refute the equivalence theorem on which the undecidability proof rests.

Watch

Extended reading notes

Core claim

The central claim is that D<: subtyping has an equivalent normal form in which the transitivity rule is replaced by a single bad-bounds rule, and through that normal form both subtyping and typing in D<: reduce from an undecidable fragment of F<: and are therefore undecidable. The same normal form shows that deleting the bad-bounds rule and restricting the function-type rule to identical parameter types gives kernel D<:, which is decidable and is exactly the fragment decided by step subtyping; allowing parameter types to differ by comparing two contexts gives strong kernel D<:, which is decidable by stare-at subtyping and strictly between kernel and full D<: in expressiveness. The authors report that the supporting lemmas are mechanized in proof assistants.

Load-bearing premise

The undecidability reduction depends on the equivalence between D<: and its normal form, and that equivalence depends on an intricate theorem proving transitivity and narrowing for the normal form by lexicographic induction; the theorem is only sketched in the text, and a gap there would break the reduction.

Editorial extensions

If this is right

  • Full D<: subtyping and D<: typing have no sound and complete decision procedure; implementations must work with semi-algorithms or a decidable fragment.
  • Kernel D<: is decidable and is exactly the fragment of D<: subtyping handled by step subtyping, giving a precise characterization of that algorithm's power.
  • Strong kernel D<: is decidable, strictly between kernel and full D<: in expressiveness, and is decided by stare-at subtyping, including comparisons between parameter types that are aliases.
  • D<: without the bad-bounds rule is still undecidable, so bad bounds are not the only source of undecidability.
  • The Scala compiler's omission of the bad-bounds rule aligns with a decidable fragment of D<: rather than being an arbitrary implementation shortcoming.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the same normal-form strategy carries over to full DOT, one would expect the bad-bounds rule to make full DOT subtyping undecidable as well, with kernel-style restrictions yielding decidable fragments.
  • The soundness of stare-at subtyping's context truncation depends on removing the BB rule; recovering any useful fragment of bad bounds would likely require controlling transitivity through type declaration hierarchies.
  • A proof of the paper's conjecture that kernel D<: plus the BB rule is undecidable would pin undecidability on bad bounds alone, and would probably need a deterministic subfragment of D<: that can encode a counter machine.
  • Strong kernel D<:'s two-context comparison suggests a general principle for alias-heavy type systems: keep a context for each side of a subtype judgment so that aliases can be resolved symmetrically without full transitivity.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper addresses the decidability of subtyping and typing in D<:, a syntactic subset of Dependent Object Types (DOT). It first shows that a previously proposed embedding of F<: into D<: cannot prove undecidability because it lacks the only-if direction, and gives an explicit counterexample (§4.2). It then defines F^-<:, a function-free fragment of F<: that is still undecidable, and develops a normal form for D<: subtyping in which transitivity is replaced by the BB (bad bounds) rule. The paper claims that this normal form is equivalent to the original D<: subtyping relation (Theorem 10 and Theorem 11) and uses it to reduce F^-<: subtyping to D<: subtyping (Theorem 12 and Theorem 13) and to D<: typing (Theorem 15 and Theorem 16). The second half of the paper defines two decidable fragments: kernel D<:, which is shown to be exactly the fragment decided by Nieto's step subtyping, and strong kernel D<:, which is decided by the new stare-at subtyping algorithm. The authors state that the proofs are mechanized in Coq and Agda, but no artifact is provided in this arXiv version.

Significance. If correct, the paper settles a long-open question: subtyping and typing in D<: are undecidable, and the bad-bounds rule is identified as a crisp source of the undecidability. The decidable fragments and the two algorithms are of real practical interest for Scala/DOT-like type systems, and the paper gives a clear account of how the normal form makes the bad-bounds phenomenon explicit. The reduction strategy is well motivated and does not appear circular: it reduces from prior undecidability of F^-<: and uses a mapping due to Amin et al. The paper also contains an instructive counterexample to the earlier claimed reduction. However, the central verification is incomplete: the load-bearing transitivity/narrowing theorem (Theorem 10) is only sketched, several inversion lemmas are stated without proof, and the claimed machine-checked formalization is not available. These gaps are fixable in principle, but they currently prevent the contributions from being fully checked.

major comments (4)
  1. [§4.6, Theorem 10] The proof of the transitivity/narrowing theorem is the load-bearing step for the equivalence of D<: with its normal form (Theorem 11) and therefore for the undecidability reductions (Theorems 13 and 16). The text gives the lexicographic induction and works through three cases for transitivity, but several cases are dismissed as symmetric or dual, narrowing is dispatched in one sentence, and clauses (3) and (4) involving type declaration hierarchies are only partially analyzed. The BB rule cuts only when the middle type is a path x.A, so the unrestricted transitivity of the normal form is exactly what needs to be established; a missing or incorrect case in clauses (3)-(4) would invalidate the equivalence. The claimed Coq/Agda mechanization is not supplied in this version, so this step cannot be independently verified from the manuscript.
  2. [§4.4, Lemmas 7-9] The inversion lemmas in invertible contexts are stated without proofs, yet they are used essentially in Theorem 12 (the Sel1' and BB cases) and in Theorem 15. Lemma 8(4), in particular, is a nontrivial statement about reachability between path types, and Lemma 9 is exactly what transfers subtyping inversion from D<: back to F^-<:. Their absence, together with the absence of the formalization, leaves the only-if direction of the undecidability reduction unverified. The authors should provide proofs of these lemmas or point to the mechanized proofs.
  3. [§5.3 and §6.5, Theorems 25 and 46] The completeness theorems for step subtyping with respect to kernel D<: and for stare-at subtyping with respect to strong kernel D<: are central to the paper's decidable-fragment claims. Both proofs are presented only as strengthened induction hypotheses plus a discussion of one or two cases; Theorem 46 states that the proof is similar to Theorem 25, but it additionally depends on Theorem 45, whose proof is also only described in a sentence. As with Theorem 10, no machine-checked artifact is available, so the exactness of the algorithms and the characterization of the fragments cannot currently be verified from the text.
  4. [§4.3, Theorem 5] Undecidability of F^-<: is asserted by saying that Pierce's proof does not depend on function types. Since undecidability of a larger calculus does not automatically transfer to a fragment, the paper should reconstruct or formally cite the specific reduction showing that function types are not needed. This is likely true, but the one-sentence proof is too thin for a result on which all subsequent undecidability claims rest.
minor comments (4)
  1. [Global formatting] The review copy contains pervasive symbol corruption in rule names, e.g. 'A/l.sc/l.sc', 'F/hyphen.scA/l.sc/l.sc', and 'K/hyphen.scA/l.sc/l.sc' instead of readable rule identifiers. If this reflects the actual submission rather than a text-extraction artifact, the PDF should be regenerated so that rule names are legible.
  2. [Lemma 2] The proof of Lemma 2, which replaces Sel1/Sel2 with Sel1'/Sel2', is extremely compressed. Since this equivalence is used to justify the normal form, a slightly more detailed argument (or a reference to the corresponding mechanized proof) would help the reader.
  3. [Theorem 11] The if direction of Theorem 11 is described as immediate, but it relies on simultaneously simulating BB using Sel1', Sel2', and transitivity. A brief sentence explaining this simulation would improve readability.
  4. [§5.1, item (3)] The conjecture 'a calculus with bad bounds will be undecidable' is vague in light of Table 1, which lists kernel and strong kernel variants with the BB rule as 'unknown'. Please state precisely which calculus is conjectured undecidable.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the undecidability result reduces from the external F^-<: problem through an independently defined mapping and a proved normal-form equivalence.

full rationale

The paper's central derivation is self-contained in the relevant sense: it does not fit any parameter, rename an input as a prediction, or import a load-bearing uniqueness premise from the authors' own prior work. Theorem 13 reduces D<: subtyping to F^-<: subtyping via the mapping of Definition 7. F^-<: undecidability is cited to Pierce [1992], an external source, and the mapping originates in Amin et al. [2016], also external. The only self-authored citation, Rapoport et al. [2017], appears as background on the bad-bounds phenomenon, but the paper constructs its own bad-bounds derivation and its theorems do not depend on that citation. The normal-form reformulation of Figure 4 is justified by Theorem 10, which proves transitivity and narrowing for the normal form by a lexicographic induction. Although the printed proof is a sketch and the claimed Coq/Agda mechanization is not supplied as an artifact, a missing artifact is a verification and evidence concern, not a circularity: the proof does not assume what it proves. The BB rule is a restricted transitivity case, but it is included as an explicit rule in the normal form and Theorem 10 proves the resulting relation transitive; this is not circular. No step in the derivation chain reduces by construction to its own inputs, and no fitted values or empirical predictions are involved. Therefore the correct finding is no significant circularity, with score 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

This is a formal calculus paper; no numerical parameters are fitted. The central claims rest on prior undecidability results and on the authors' own normal-form equivalence, which is proven in the text and claimed mechanized. The formal artifacts (normal form, kernel, strong kernel) are definitions rather than independently testable entities.

assumptions (4)
  • domain assumption F^-<: subtyping is undecidable, as cited to Pierce 1992 (Theorem 5).
    The paper asserts this in one sentence without reproducing the reduction; it is load-bearing for the reduction to D<:.
  • domain assumption F<: normal form is equivalent to F<: (Theorem 1, from Curien and Ghelli).
    Used to justify working with normal forms; cited from prior literature.
  • domain assumption Amin et al.'s mapping preserves F<: subtyping (Theorem 3).
    Used for the 'if' direction of the reductions; taken from Amin et al. 2016.
  • standard math Types are considered up to alpha-conversion and contexts are well-formed (Section 2).
    Standard framework for the paper; not proven independently.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Undecidability of $D_{<:}$ and Its Decidable Fragments." pith.science (2026). https://pith.science/paper/YCQ7MYKV

@misc{pith2026190805294,
  author       = {Pith},
  title        = {Pith review of: Undecidability of $D_<:$ and Its Decidable Fragments},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YCQ7MYKV}},
  note         = {Machine review of arXiv:1908.05294}
}
abstract

Dependent Object Types (DOT) is a calculus with path dependent types, intersection types, and object self-references, which serves as the core calculus of Scala 3. Although the calculus has been proven sound, it remains open whether type checking in DOT is decidable. In this paper, we establish undecidability proofs of type checking and subtyping of $D_{<:}$, a syntactic subset of DOT. It turns out that even for $D_{<:}$, undecidability is surprisingly difficult to show, as evidenced by counterexamples for past attempts. To prove undecidability, we discover an equivalent definition of the $D_{<:}$ subtyping rules in normal form. Besides being easier to reason about, this definition makes the phenomenon of bad bounds explicit as a single inference rule. After removing this rule, we discover two decidable fragments of $D_{<:}$ subtyping and identify algorithms to decide them. We prove soundness and completeness of the algorithms with respect to the fragments, and we prove that the algorithms terminate. Our proofs are mechanized in a combination of Coq and Agda.

Figures

Figures reproduced from arXiv: 1908.05294 by the authors.

Figure 1
Figure 1. Definition of subtyping in F<: [Pierce 2002, [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Definition of F<: normal form Definition 3. F<: is defined in [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Definition of D<: [Amin et al. 2016] Proof. This follows directly from the fact that the only typing rules that apply to variables are the Var and Sub rules. This new definition of subtyping with the Sel1’ and Sel2’ rules no longer depends on typing. We will use this definition in the rest of the paper. 4 UNDECIDABILITY OF D<: (SUB)TYPING 4.1 Definition of Undecidability A common method for proving a decision proble… view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: Definition of subtyping of D<: normal form Proving transitivity of D<: normal form is quite tricky. First, transitivity is interdependent with narrowing, so we will need to prove the two together. Second, the proof of transitivity requires reasoning about types of the …
Figure 5
Figure 5. Figure 5: Definition of kernel D<: The second adjustment is to remove the BB rule. There are several reasons for that: (1) Bad bounds are consequences of unintended interactions between the Sel1’, Sel2’ and Trans rules. (2) Nieto [2017] observed that the implementation of subtyp…
Figure 6
Figure 6. Figure 6: Definition of step subtyping operation [ [PITH_FULL_IMAGE:figures/full_fig_p015_6.png]
Figure 7
Figure 7. Figure 7: Definitions of Exposure and Upcast / Downcast operations [Nieto 2017] to look up x in the typing context to a type member declaration {A : S..U } and read off the upper bound U (lower bound S, respectively). A complication, however, is that the typing context could ass…
Figure 8
Figure 8. Figure 8: Definition of strong kernel D<: Let us write the contexts twice for this rule: Γ ⊢D<: S ′ <: S ⊣ Γ Γ; x : S ′ ⊢D<: Ux <: U ′ x ⊣ Γ; x : S ′ Γ ⊢D<: ∀(x : S)U <: ∀(x : S ′ )U ′ ⊣ Γ All-TwoContexts Now do the same for the kernel version too: Γ; x : S ⊢D<: Ux <: U ′ x ⊣ Γ;…
Figure 9
Figure 9. Figure 9: Definition of OPE<: Lemma 26. Strong kernel D<: is reflexive. Γ1 ⊢D<:SK T <: T ⊣ Γ2 Proof. By induction on T. In the next two theorems, we wish to show that strong kernel D<: is in between kernel D<: and full D<: in terms of expressiveness: Theorem 27. If Γ ⊢D<:K S <: …
Figure 10
Figure 10. Figure 10: Definition of stare-at subtyping Even if we remove the BB rule from full D<: , the Sk-All rule is strictly weaker than the full All rule. For example, the following is a derivation in full D<: : straightforward ⊢D<: {A : ⊥..⊥} <: {A : ⊥..⊤} Bnd straightforward x : {A …
Figure 11
Figure 11. Figure 11: Definition of Revealing and new definitions of Upcast and Downcast for the context and type to the left of <: or >:, while Bob is responsible for the other side. In partic￾ular, Alice and Bob are completely independent and do not need to see the contexts or types held…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

21 extracted references · 14 canonical work pages

  1. [1]

    Publicatio n date: January 2018

    work page 2018

  2. [11]

    SIGPLAN Not

    Getting F-bo unded Polymorphism into Shape. SIGPLAN Not. 49, 6 (June 2014), 89–99. https://doi.org/10.1145/2666356.2594308 Radu Grigore

    arXiv 2014

  3. [12]

    https://doi.org/10.1145/3009837.3009871 Andrew J

    ACM, New York, NY, USA, 73–85. https://doi.org/10.1145/3009837.3009871 Andrew J. Kennedy and Benjamin C. Pierce

    arXiv

  4. [13]

    https://doi.org/10.1145/3136000.3136003 Martin Odersky, Vincent Cremet, Christine Röckl, and Matthias Zenger

    ACM, New York, NY, USA, 2–7. https://doi.org/10.1145/3136000.3136003 Martin Odersky, Vincent Cremet, Christine Röckl, and Matthias Zenger

    work page arXiv

  5. [17]

    A S imple Soundness Proof for Dependent Object Types. Proc. ACM Program. Lang. 1, OOPSLA, Article 46 (Oct. 2017), 27 pages. https://doi.org/10.1145/3133870 Tiark Rompf and Nada Amin

    work page doi:10.1145/3133870 2017

  6. [18]

    In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016)

    Type Soundness for Dependent Object T ypes (DOT). In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016). ACM, New York, NY, USA, 624–641. https://doi.org/10.1145/2983990.2984008 Agda Team

    arXiv 2016

  7. [19]

    https://doi.org/10.5281/zenodo.1219885 Stefan Wehr and Peter Thiemann

    The Coq Proof Assistant, version 8.8.0. https://doi.org/10.5281/zenodo.1219885 Stefan Wehr and Peter Thiemann

    work page doi:10.5281/zenodo.1219885

  8. [56]

    https://doi.org/10.1006/inco.1994.1013 Luca Cardelli and Peter Wegner

    arXiv 1994

Show all 21 references
  1. [141]

    https://doi.org/10.1006/inco.1999.2832 Benjamin C. Pierce

    1999

  2. [309]

    Barendregt

    https://doi.org/10.1016/S0304-3975(00)00175-4 H.P. Barendregt

    doi

  3. [1985]

    ACM Comput

    On Understanding Types, Data Abstraction, and Polymorphism. ACM Comput. Surv. 17, 4 (Dec. 1985), 471–523. https://doi.org/10.1145/6041.6042 Adam Chlipala

    1985

  4. [1992]

    In Proceedings of the 19th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (P OPL ’92)

    Bounded Quantification is Undecidable. In Proceedings of the 19th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (P OPL ’92) . ACM, New York, NY, USA, 305–315. https://doi.org/10.1145/143165.143228 Benjamin C. Pierce

  5. [1994]

    Information and Computation 109, 1 (1994), 4 –

    An Ext ension of System F with Subtyping. Information and Computation 109, 1 (1994), 4 –

    1994

  6. [2000]

    Intuitionistic and Class ical Logic

    Structural Cut Elimination: I. Intuitionistic and Class ical Logic. Information and Computation 157, 1 (2000), 84 –

    2000

  7. [2001]

    Theoretical Computer Science 266, 1 (2001), 273 –

    Subtyping dependent types. Theoretical Computer Science 266, 1 (2001), 273 –

    2001

  8. [2009]

    In Proceedings of the 7th Asian Symposium on Programming Languages and Syst ems (APLAS ’09)

    On the Decidability of Subtyping with Bounded Existential Types. In Proceedings of the 7th Asian Symposium on Programming Languages and Syst ems (APLAS ’09) . Springer-Verlag, Berlin, Heidelberg, 111–127. https://doi.org/10.1007/978-3-642-10672-9_10 Proc. ACM Program. Lang., V...

    doi

  9. [2014]

    In Proceedings of the 2014 ACM International Conference on Object Oriented Programming S ystems Languages & Applications (OOPSLA ’14)

    Foundations of Path-dependent Types. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming S ystems Languages & Applications (OOPSLA ’14) . ACM, New York, NY, USA, 233–249. https://doi.org/10.1145/2660193.2660216 David Aspinall and Adriana Compagnoni

    2014

  10. [2016]

    Springer International Publishing, Cham, 249–272

    The Essence of Dependent Object Types. Springer International Publishing, Cham, 249–272. https://doi.org/10.1007/978-3-319-30936-1_14 Nada Amin, Adriaan Moors, and Martin Odersky

    doi

  11. [2017]

    In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017

    Type soundness proofs with definitional interpreters. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 . ACM, 666–

    2017

  12. [2018]

    In Interactive Theorem Proving - 9th International Conferenc e, ITP 2018, Oxford, UK, July 9-12, 2018 (LNCS 10895)

    Verification of PCP-Related Computational Reductions in Coq. In Interactive Theorem Proving - 9th International Conferenc e, ITP 2018, Oxford, UK, July 9-12, 2018 (LNCS 10895) . Springer, 253–269. Preliminary version appeared as arXiv:1711.07023. Yannick Forster and Dominique L...

    2018 arXiv

  13. [2019]

    https://doi.org/10.1145/3293880.3294096 Yannick Forster and Gert Smolka

    ACM, New York, NY, USA, 104–117. https://doi.org/10.1145/3293880.3294096 Yannick Forster and Gert Smolka

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.