{"id":"4e80ec31-87fc-4225-8e36-ca4e964c99d5","arxiv_id":"1908.05294","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"D<: subtyping and typing are undecidable, but removing the bad-bounds rule and restricting comparison of function types yields decidable fragments with complete algorithms.","lead":"Scala 3's core type calculus D<: cannot always decide whether one type is a subtype of another, and the paper proves this. It also identifies two restricted versions that are decidable, with algorithms and machine-checked proofs.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No artifact and only a sketch for Theorem 10; the transitivity/narrowing proof of D<: normal form is the load-bearing step for Theorem 11 and hence for Theorems 13/16.","rationale":"The reader's weakest assumption identifies the same point, and I agree. The normal-form equivalence is the linchpin: all of the paper's undecidability and decidability results are statements about D<: variants, but the technical machinery lives in the normal form. The reduction in Theorem 12 is by induction on normal-form derivations, and the equivalence Theorem 11 is what transfers the result back to D<:. The proof of Theorem 10 is the largest unmechanized-looking step in the text: it has four mutually dependent clauses and a lexicographic induction whose measure is only described informally. The sketch does present the key All-All and Sel2'-any cases, which gives some confidence, but it explicitly omits several cases as symmetric, and the type-declaration-hierarchy machinery in clauses (3) and (4) is intricate. This is exactly the kind of step where a subtle missing subcase can undo a reduction. The claimed Coq/Agda formalization would settle it, and the paper is honest that this is their evidence; without the artifact, the preprint leaves a genuine verification gap. I would keep the reader's CONDITIONAL verdict: the paper is strong, the counterexample to Amin et al. is concrete, and the normal form is a plausible and elegant reformulation, but the central equivalence should not be taken as fully verified until the artifact is available or Theorem 10 is independently formalized. No additional objection beyond the reader's was found.","tokens_in":29153,"tokens_out":10956,"duration_ms":112960,"concrete_test":"Release and run the promised Coq/Agda formalization, or independently formalize Figure 4 and Theorem 10 in a proof assistant, and check in particular the cases the sketch labels symmetric: Sel2'-Sel2', any-Sel1', any-BB, and the non-nil cases of clauses (3) and (4). If the checker accepts all four clauses with the stated lexicographic measure, the concern is settled; if any case is missing or the induction does not go through, Theorem 11, and with it Theorems 13 and 16, must be revised.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The undecidability reductions (Theorems 13 and 16) pass through Theorem 11, which identifies D<: with the normal-form rules of Figure 4. The only-if direction of that equivalence requires Theorem 10: the normal form is transitive, with narrowing and two auxiliary type-declaration-hierarchy clauses, proved by a lexicographic induction on (T,D1,D2). The printed proof is a sequence of representative cases; several cases are dismissed as \"symmetric\", and the mutual dependencies among clauses (1)-(4) are subtle enough that a misplaced or missing case would break the induction. In particular, BB is only a strongly restricted cut (it cuts exactly when the middle type is a path x.A and both bound premises for the same x are available), so it is not syntactically evident that all transitivity through non-path middle types is recovered. If Theorem 10 were false in any case, the normal form would not be equivalent to D<:, and the reduction from F-<: to normal form (Theorem 12) would not establish undecidability of the original D<: subtyping or typing. The paper claims the proofs are mechanized in Coq/Agda, but the preprint provides no artifact, so the load-bearing step is not independently checkable from the text. This is an unverified step, not an identified contradiction.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":29443,"tokens_out":9365,"duration_ms":97214,"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":[{"comment":"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.","section":"§4.6, Theorem 10"},{"comment":"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.","section":"§4.4, Lemmas 7-9"},{"comment":"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.","section":"§5.3 and §6.5, Theorems 25 and 46"},{"comment":"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.","section":"§4.3, Theorem 5"}],"minor_comments":[{"comment":"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.","section":"Global formatting"},{"comment":"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.","section":"Lemma 2"},{"comment":"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.","section":"Theorem 11"},{"comment":"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.","section":"§5.1, item (3)"}],"recommendation":"major_revision","confidential_remarks":"The paper is a strong candidate if the claimed formalization is real and can be supplied. The main concern is verification of Theorem 10 and, to a lesser extent, the completeness theorems for the two algorithms. I recommend asking the authors to provide the Coq/Agda artifact and a short guide mapping each theorem in the paper to the corresponding mechanized statement. If the artifact cannot be provided, the central claims would not be verifiable from the text alone, and the paper should not be accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know. First, this is the first credible proof that D<: subtyping and typing are undecidable, and it also draws a clean boundary with two decidable fragments. Second, the load-bearing step is Theorem 10, the transitivity/narrowing theorem for the normal form, and in this v1 the proof is a sketch with selected cases and no Coq/Agda artifact, so the central claim is not independently checkable from the text. The stress-test note is not manufacturing a flaw; it points at the right spot.\n\nWhat is genuinely new: the counterexample to Amin et al.'s proposed reduction from F<: is simple and convincing, and it explains why the old mapping could not work. The normal form of D<:, with bad bounds isolated as a single BB rule, is a neat idea and does real explanatory work. The reduction from F^-<: to the normal form is clever, and the decision procedures for kernel and strong kernel D<: -- step subtyping and stare-at subtyping -- are real contributions. The equivalence between kernel D<: and the fragment handled by Nieto's step subtyping ties the paper to practice. The citation pattern looks fine: prior undecidability results, the DOT soundness literature, and Nieto's algorithm are all cited appropriately, and the self-cited material is background rather than load-bearing.\n\nThe soft spot is exactly Theorem 10. The lexicographic induction on (T, D1, D2) with four mutually dependent clauses is intricate, and the printed proof dismisses several cases as symmetric. Since Theorem 11 depends on Theorem 10, and Theorems 13 and 16 pass through Theorem 11, any gap there would collapse the undecidability results. I have no evidence of an actual error; the proof outline is coherent and follows the standard Pfenning-style cut-elimination pattern. But for a result this strong, \"trust us, it is mechanized\" is not enough. The paper itself says the formalization is supplementary material and will be submitted as an artifact, yet no artifact is present. That is a correctable issue, not a fatal one.\n\nMinor point: the paper would benefit from stating more explicitly that Theorem 14 -- undecidability without BB -- means the BB rule is not the sole source of undecidability; the decidable fragments require both removing BB and restricting the arrow rule. The paper does say this, but Table 1 and the prose could make it harder to miss.\n\nWho this is for: anyone working on DOT, Scala's type system, or bounded quantification generally. It settles a long-open question and gives useful fragments for compiler implementation.\n\nMy recommendation: send it to serious referees. The result deserves referee time, but artifact release should be a condition of acceptance. If the Coq/Agda proofs check out, this is a major paper.","headline":"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.","tokens_in":29940,"tokens_out":1902,"would_cite":true,"duration_ms":19747,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["D<:","Dependent Object Types","undecidability","subtyping","type checking","bad bounds","kernel subtyping","stare-at subtyping"],"falsifier":"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.","tokens_in":28981,"feed_emoji":"🧩","tokens_out":7304,"duration_ms":68054,"temperature":0.7,"pith_summary":"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.","feed_headline":"D<: subtyping and type checking are undecidable","feed_subtitle":"A normal form isolates bad bounds; removing them yields two decidable fragments with algorithms.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines D<: and supplies the original subtyping relation plus the partial mapping from F<: whose converse this paper repairs.","marker":"[Amin et al. 2016]"},{"why":"Proves F<: subtyping undecidable, the source of the F^-<: reduction and of the observation that function types are unnecessary.","marker":"[Pierce 1992]"},{"why":"Supplies step subtyping, the algorithm later proved to decide exactly kernel D<:.","marker":"[Nieto 2017]"},{"why":"Establishes the F<: normal-form equivalence that motivates and models the D<: normal form.","marker":"[Curien and Ghelli 1990]"},{"why":"Introduces F<: with bounded quantification and the kernel restriction of the function-type rule reused in kernel D<:.","marker":"[Cardelli and Wegner 1985]"},{"why":"Identifies bad bounds as a recurring DOT phenomenon that the BB rule makes explicit.","marker":"[Rompf and Amin 2016]"}],"fun_headline_variants":["Bad-bounds rule makes D<: undecidable","Removing bad-bounds rule gives two decidable D<: fragments","D<: undecidable; two decidable fragments via normal form","D<: typing and subtyping undecidable, with decidable fragments","D<: normal form isolates undecidable bad-bounds rule"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Bad-bounds rule makes D<: undecidable","Removing bad-bounds rule gives two decidable D<: fragments","D<: undecidable; two decidable fragments via normal form","D<: typing and subtyping undecidable, with decidable fragments","D<: normal form isolates undecidable bad-bounds rule"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000804,"raw_usage":{"total_tokens":3512,"prompt_tokens":906,"completion_tokens":2606,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":522,"completion_tokens_details":{"reasoning_tokens":2512}},"tokens_in":522,"tokens_out":2606,"duration_ms":20680,"temperature":1.0,"reasoning_tokens":2512,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:18:18.065635+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}