Pith. sign in

REVIEW 3 major objections 3 minor 74 references

Bidirectional Typing with Freezing, Skeletons, and Ghosts

T0 review · 3 major / 3 minor · reviewed 2026-08-01 · deepseek-v4-flash

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

Pith's one-line read Fresco claims that mixed-direction information flow can be made declarative: skeletons with ghosts collect information from arguments, tagged subtyping forbids guessing polymorphism, and a simple algorithm is sound and complete.

desk verdict A serious, well-structured FCP inference paper whose central optimality proof rests on missing appendix lemmas — worth a careful referee, not a desk reject. read the letter →

arxiv 2607.16061 v1 pith:W7USCKDM submitted 2026-07-17 cs.PL

Wenhao Tang , Shengyi Jiang , Aghilas Y. Boussaa , Sam Lindley , Bruno C. d. S. Oliveira This is my paper · ORCID
classification cs.PL
keywords first-classpolymorphismbidirectionaltypeinferenceskeletonghosttypesfreezinghigher-rankpolymorphicinstantiationmodaleffect
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

Fresco is a bidirectional type inference system for first-class polymorphism—programs where functions can be instantiated with polymorphic types, not just monomorphic ones. The paper tries to establish that such inference can be made both expressive and predictable: type information should be allowed to flow from arguments to functions and then back, but a polymorphic instantiation should never be guessed 'out of thin air.' Its main claim is a declarative type system plus a simple algorithm that is sound and complete with respect to that declarative system. On the paper's central example, the algorithm types churchMap applied to a Church-encoded list of polymorphic identities, while single id is rejected as ambiguous, showing that mixed information flow can be principled rather than ad hoc.

What carries the argument

The key machinery is skeleton inference, which mirrors the syntax-directed typing rules and produces a skeleton with ordinary ghosts for unknown types and universal ghosts for unknown quantifier sequences; freezing forces a term's skeleton to be exactly its own type, so programmers can decide what information an argument exposes. Skeleton refinement and colouring turn the argument's skeleton into a bidirectional type with inherited and synthesised quantifiers. The second load-bearing piece is tagged subtyping: each guessed instantiation quantifier carries a tag, and a tag is solvable only when a consistency rule like C-ForallInh matches it against an inherited quantifier; at least one occurr

What would settle it

Run the implementation on the two anchor examples from the paper: churchMap $(\lambda f. (f 42, f true))$ churchIds should be accepted, and single id should be rejected. The sharper structural test is to exhibit a program whose only successful derivation instantiates a polytype with no occurrence matched to inherited information—then the 'never guess' principle is violated and the no-best-choice argument collapses.

Watch

Extended reading notes

Core claim

Fresco's central claim is that skeletons and ghosts give a declarative account of how local type information flows between functions and arguments. A skeleton is an argument's type with 'ghost' holes for unknown monotypes and unknown quantifier sequences; skeleton inference collects the known polymorphic shape of an argument, and skeleton refinement fills the holes with information supplied by the function. Colours mark whether a quantifier was inherited from the argument or synthesised by the function. In subtyping, every guessed quantifier is tagged, and the guess is accepted only if at least one occurrence of the tag is determined by an inherited quantifier—this is the formal meaning of '

Load-bearing premise

The load-bearing premise is that a guessed polymorphic instantiation is legitimate exactly when at least one occurrence of its quantifier is anchored to an inherited quantifier, and that the algorithm's look judgement captures precisely this relation; if that correspondence fails, Fresco would either guess polymorphism with no best choice or reject programs it should accept.

Editorial extensions

If this is right

  • If the central claim holds, first-class polymorphism becomes inferable in a bidirectional style: the motivating churchMap program is typable, with the polymorphic identity type flowing from the Church-encoded argument into the function and back into the lambda.
  • The 'determined tag' rule gives a predictable answer to the no-best-choice problem: single id is rejected rather than silently assigned one of several incomparable polymorphic types.
  • Because polytypes are never guessed, unification can remain first-order; only monotypes are solved by global unification, so the algorithm stays simple and local.
  • The same infrastructure—skeleton inference plus ghosts—extends beyond plain polymorphism, as the implementation shows by inferring modal effect types.
  • The syntax-directed declarative system is equivalent to the coloured declarative system, so the specification has a clean algorithmic reading.

Reading between the lines

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

  • The tag-based 'determined by inheritance' test is a candidate general principle for any local inference system that wants to mix directions of information flow without global constraint solving; it could be reused outside this specific system.
  • Named ghosts are the natural next step: connecting occurrences inside a skeleton would let the argument's own shape guide more instantiations, at the cost of more complex skeleton refinement.
  • The single-pass flow restriction is a design trade-off; relaxing it to allow information to flow back and forth repeatedly would increase expressiveness but complicate the optimality story, since the order of solving could start to matter.
  • The extension to modal effect types hints that the mechanism is not tied to System F: any setting where types carry implicit introduction and elimination operations has the same 'don't guess' structure.
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

3 major / 3 minor

Summary. The paper proposes Fresco, a bidirectional type inference system for first-class polymorphism. The key ideas are skeletons with ordinary and universal ghosts, a freezing operator, coloured quantifiers, and a tag-based provenance mechanism that is meant to ensure that polymorphic instantiations are only guessed when they are determined by inherited information. The authors give a declarative type system, a syntax-directed variant equivalent to it (mechanized in Rocq), and an algorithmic type system with a look/constraint-solving judgement. They claim soundness, completeness, and optimality of algorithmic type inference relative to the declarative system, and they report a prototype extended with algebraic data types and modal effect types. The motivating example churchMap (λf.(f 42, f true)) churchIds is claimed to be accepted while QuickLook, HMF, MLF, ATIA, and FCIF reject it.

Significance. If the technical claims hold, Fresco would be a substantial contribution to first-class polymorphism inference: it types a nontrivial motivating example that several established systems cannot, does so with a local algorithm that avoids global impredicative unification, and provides a rule-based specification with optimality theorems. The decorated-skeleton/tag-solving proof infrastructure is novel, and the paper ships two concrete strengths: a Rocq mechanization of the declarative-to-syntax-directed equivalence and a prototype with extensions to modal effect types. However, the central algorithmic theorems are not yet verifiable from the submitted text: the key consistency lemmas are in an appendix that is absent, and the completeness proof in Appendix E is truncated. The significance is therefore conditional on completing that material.

major comments (3)
  1. [§4.5, Appendix E, Appendix F] The proof of soundness and optimality of algorithmic subtyping — and through it Theorem 4.3 — rests on decorative consistency lemmas F.1–F.6 that are cited but not present. For instance, Lemma E.2 (soundness of decorated subtyping) invokes Lemma F.1, Lemma E.10 invokes Lemmas F.3/F.4, and Lemma E.15 invokes Lemma F.6. These are not machine-checked either. Without them, the decorated consistency/tag-solving correspondence is unsubstantiated. In particular, the reader's concern about C-ForallInh/SE-ForallInh (Figs. 2 and 22) discharging a guessed quantifier via a bare inherited quantifier is not refuted: no lemma establishes that every discharged tag corresponds to a unique most-general instantiation. This is load-bearing for the 'never guess polymorphism out of thin air' guarantee and for the optimality theorems.
  2. [Appendix E.3] The completeness proof of algorithmic subtyping (Theorem 4.6) is incomplete in the submitted text. The proof of Lemma E.16 breaks off in the S-Arrow case, and the final induction and the statement's conclusion never appear. Since Theorem 4.6 is in turn used to prove Theorem 4.3 (completeness and optimality of type inference), the central claim of the paper is not fully established. The paper should either include the complete proof or clearly mark it as deferred to a supplementary document.
  3. [§3.4, §4.6, Abstract] The claimed 'declarative specification' is arguably a rule-based presentation of the same tag-solving machinery that the algorithm implements: S-ForallL guesses a decorated polytype and requires its tags to be solved by C-ForallInh, while the algorithmic look/constraint-solving judgement (§4.6) computes exactly those solvable tags. The soundness/completeness theorems are thus partly a coherence result between two presentations of one design. This does not make the paper incorrect, but the authors should clarify what is declarative about the specification beyond being typographically non-algorithmic, and should temper the abstract's phrasing if the specification is not independent of the algorithm.
minor comments (3)
  1. [§5] The Rocq encoding is described as 'a faithful encoding of the declarative type system' and proves Lemmas B.1–B.2. It does not machine-check Theorems 4.2–4.6. This should be stated explicitly early, so that readers do not infer that the algorithmic completeness theorems are mechanized.
  2. [§3.5] The 'precision' order on skeletons is defined as refinement in the other direction from what the word 'precision' might suggest. A short example or a note explaining why a skeleton with more ghosts is considered more precise would reduce confusion.
  3. [§4.6, Fig. 7] The distinction between constraint collection and constraint solving is clear in the text, but the rule names (LS-, LE-, SolS-, SolE-) are easy to confuse. Please consider adding a one-line index or a name table in the appendix.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular derivation: Fresco's soundness/completeness theorems are proven against its own declarative system, not against fitted data or self-cited prior results; the absent Appendix F is a proof gap, not a circular reduction.

full rationale

I walked the derivation chain from D-App/S-ForallL to Theorems 4.2-4.6 and found no step where a claimed output is identical by construction to an input. The algorithmic I-App mirrors the declarative D-App (skeleton-infer argument, split function skeleton, check argument), but this is the standard declarative/algorithmic coherence the paper proves by induction, not a fitted parameter masquerading as a prediction. The tag-based determination principle (C-ForallInh adding a tag, C-ForallSyn not doing so) is the declared design principle, and the look/constraint-solving judgement is a separate algorithmic device; the completeness theorem asserts their equivalence rather than defining one in terms of the other. The motivating churchMap example is not a benchmark fitted by the algorithm: the type of churchIds is an input to the rule, and the polytype ∀c.c→c is produced by the look judgement and then flows back; no parameter was tuned to make the example pass. The only citations that could be called self-citations (FreezeML [12] for the freezing construct, Tang et al. [40] for the Met extension) are used as inspiration/related work, not as load-bearing justification of the central soundness/completeness claims, so they do not create circularity. The genuine concern raised in Section 4.5/Appendix E is that the decorated-subtyping consistency lemmas (F.1-F.6) are cited as being in Appendix F, which is absent from the reviewed text, and the Rocq artifact covers only the syntax-directed/declarative equivalence, not the algorithmic subtyping correspondence. That is an unverified proof obligation and a real risk to the optimality theorem, but it is a completeness gap, not an equivalence of output to input. I therefore score 2, reflecting only the minor non-load-bearing self-citations, not a circular derivation.

Assumptions & free parameters 0 free parameters · 6 assumptions · 5 invented entities

No fitted parameters; this is a formal-system paper. The load-bearing axioms are the tag-based determination principle (§3.4/§4.6), the faithful-skeleton correspondence (§3.6), shallow-subtyping and value-restriction design choices (§2.8), and the unstated adequacy of the Rocq encoding (§5). Invented entities (ghosts, universal ghosts, skeletons, tags) are internal to the type system; their external handle is the prototype's behavior on the published example suite, except tags/modes which are only indirectly observable.

assumptions (6)
  • domain assumption A guessed instantiation quantifier counts as determined iff at least one of its appearances is aligned with an inherited quantifier (C-ForallInh adds the tag; S-ForallL requires every guessed tag to be solved; the algorithmic look must compute exactly this).
    Defines 'never guess polymorphism out of thin air'; the one-appearance relaxation over CLTI/Boxy is the paper's own semantic choice (§2.6, §3.4, §4.6) and is load-bearing for both the declarative system and the algorithm's completeness.
  • domain assumption Skeleton inference against the syntax-directed typing rules (P-rules corresponding one-to-one to SD-rules) yields skeletons whose refinement P ▶ A characterizes exactly the types a term can have after instantiation/generalization.
    §3.5–3.6, §4.4; if skeletons over- or under-approximated possible types, the mixed flow in D-App/P-App could instantiate wrongly; the proof of this correspondence is part of the unmechanized algorithmic metatheory.
  • domain assumption Shallow subtyping: instantiation/type abstraction apply only at top level, with deeper upcasting only when the mode records a real function position.
    §2.8 design choice that makes look local; excluded deeper flows are stated as a limitation.
  • domain assumption Value restriction: type abstraction applies only to syntactic values.
    §2.8; adopted for the modal-effect extension; restricts generalization of non-values (poly(id id) ill-typed).
  • domain assumption The Rocq 'faithful encoding' of the declarative system reflects the paper's rules, and its verified equivalence (B.1–B.2) transfers to the paper's system; no adequacy statement or artifact hash is given.
    §5; a formalization is only as strong as the adequacy of its encoding, which is unstated.
  • standard math Well-scoped System F types, Barendregt convention, alpha-equivalence, and the Gundry–McBride–McKinna metasubstitution/information-increase framework.
    Standard background imported from [2] and [16, 17]; used throughout Section 4 and the appendices.
invented entities (5)
  • Ordinary ghost (unknown-type placeholder in skeletons) independent evidence
    purpose: Represents unknown monomorphic information collected from an argument so the function can fill it back in
    Internal to the type system, but behaviorally checkable through the public prototype on the published example suite (e.g., churchMap accepted, single id rejected).
  • Universal ghost ∀. independent evidence
    purpose: Represents an unknown sequence of universal quantifiers (and modalities in the Met extension), enabling polymorphic/modal instantiation to be inferred from the argument's shape
    Same handle: accept/reject behavior plus the shipped Met tests from the prototype repository.
  • Skeleton + skeleton inference/refinement (P ▶ A) independent evidence
    purpose: The vehicle for mixed information flow: collect argument polytype information before typing the function, then refine
    Falsifiable via the example suite and the claimed one-to-one correspondence with typing rules; which programs are typable is testable with the public prototype.
  • Tags and tag contexts on guessed quantifiers
    purpose: Bookkeeping to enforce the 'only guess determined polymorphism' principle declaratively
    Pure proof machinery; observable only indirectly through accepted programs; no independent handle such as a predicted observable.
  • Function modes (F m) with argument-skeleton triggering
    purpose: Track application structure so deeper subtyping is allowed exactly where a real argument exists
    Adapted from contextual typing counters [45]; internal to the algorithm/spec.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Bidirectional Typing with Freezing, Skeletons, and Ghosts." pith.science (2026). https://pith.science/paper/W7USCKDM

@misc{pith2026260716061,
  author       = {Pith},
  title        = {Pith review of: Bidirectional Typing with Freezing, Skeletons, and Ghosts},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/W7USCKDM}},
  note         = {Machine review of arXiv:2607.16061}
}
read the original abstract

Bidirectional typing makes use of local information flow between functions and arguments. Conventional bidirectional typing only supports unidirectional information flow, typically from functions to arguments, which is insufficient to infer first-class polymorphism. Existing work on improving information flow either has limited support for mixed information flow or requires ad hoc mechanisms that harm predictability. We propose Fresco, a novel bidirectional type inference approach to first-class polymorphism. Fresco enables local type information to flow back and forth between functions and arguments via skeletons, with ghosts representing unknown type information, and allows users to customise the direction of information flow by freezing. The flexible information flow of Fresco enables expressive and predictable inference for first-class polymorphism. We provide a declarative specification for Fresco, a simple type inference algorithm that is sound and complete with respect to the declarative system, and a prototype implementation that further generalises Fresco to infer modal effect types.

Figures

Figures reproduced from arXiv: 2607.16061 by the authors.

Figure 1
Figure 1. gives the declarative typing rules for Fresco. We highlight judgements we have not yet defined in light grey background. The typing judgement has the form Γ ⊢m 𝑀 : 𝐴, which states that under context Γ in mode m the term 𝑀 has type 𝐴. As usual, we require standard well-scopedness of 𝑀 and 𝐴 under Γ as well-formedness conditions for the typing judgement. Moreover, we require compatibility between coloured types and mo… view at source ↗
Figure 2
Figure 2. Subtyping and consistency rules for Fresco. [PITH_FULL_IMAGE:figures/full_fig_p013_2.png] view at source ↗
Figure 3
Figure 3. gives the skeleton inference rules. Skeleton inference has the form Γ ⊢m 𝑀⇒ 𝑃, which means that the term 𝑀 has skeleton 𝑃 under context Γ in mode m. We require well-formedness of 𝑀 and 𝑃 under Γ as well-formedness conditions for the skeleton inference judgement, as well as the compatibility between bidirectional skeletons and modes 𝑃 : sk m. The relation 𝑃 : sk m is defined similarly to 𝐴 : ty m. The only difference… view at source ↗
Figures from the paper (19 more)
Figure 4
Figure 4. Figure 4: Subtyping and consistency rules of skeletons for Fresco. [PITH_FULL_IMAGE:figures/full_fig_p016_4.png]
Figure 5
Figure 5. Figure 5: Selected algorithmic type inference rules and skeleton splitting rules. [PITH_FULL_IMAGE:figures/full_fig_p018_5.png]
Figure 6
Figure 6. Figure 6: Selected algorithmic consistency rules [PITH_FULL_IMAGE:figures/full_fig_p020_6.png]
Figure 7
Figure 7. Figure 7: Look rules, together with selected constraint collection and solving rules. [PITH_FULL_IMAGE:figures/full_fig_p022_7.png]
Figure 8
Figure 8. Figure 8: Comparison for existing examples from Serrano et al [PITH_FULL_IMAGE:figures/full_fig_p029_8.png]
Figure 9
Figure 9. Figure 9: Comparison for the new examples. head : ∀𝑎.List 𝑎 → 𝑎 tail : ∀𝑎.List 𝑎 → List 𝑎 append : ∀𝑎.List 𝑎 → List 𝑎 → List 𝑎 nil : ∀𝑎.List 𝑎 cons : ∀𝑎.𝑎 → List 𝑎 → List 𝑎 map : ∀𝑎 𝑏.(𝑎 → 𝑏) → List 𝑎 → List 𝑏 single : ∀𝑎.𝑎 → List 𝑎 length : ∀𝑎.List 𝑎 → Int compose : ∀𝑎 𝑏 𝑐.(𝑏 →…
Figure 10
Figure 10. Figure 10: Type signatures for functions used in the comparison. For Church encodings, [PITH_FULL_IMAGE:figures/full_fig_p030_10.png]
Figure 11
Figure 11. Figure 11: Declarative subtyping rules for both types and skeletons. [PITH_FULL_IMAGE:figures/full_fig_p031_11.png]
Figure 12
Figure 12. Figure 12: Metasubstitutions (information increase) and equivalence of metasubstitutions. [PITH_FULL_IMAGE:figures/full_fig_p032_12.png]
Figure 13
Figure 13. Figure 13: Declarative rules in algorithmic contexts (only showing changed rules). [PITH_FULL_IMAGE:figures/full_fig_p033_13.png]
Figure 14
Figure 14. Figure 14: Algorithmic type inference and skeleton splitting. [PITH_FULL_IMAGE:figures/full_fig_p034_14.png]
Figure 15
Figure 15. Figure 15: Algorithmic skeleton inference. a solution is optimal if for any other solution (𝜃 :: Θ0 ⊑ Θ;𝑄), there exists a metasubstitution 𝜁 :: Θ1 ⊑ Θ such that 𝜃 ≡ 𝜁 ◦ 𝜃1 :: Θ0 ⊑ Θ and Θ ⊢ 𝜁 𝑃1 ⪯ 𝑄. Theorem C.2 (Soundness of skeleton inference). Given a skeleton inference prob…
Figure 16
Figure 16. Figure 16: Algorithmic subtyping [PITH_FULL_IMAGE:figures/full_fig_p036_16.png]
Figure 17
Figure 17. Figure 17: Constraint collection. Then, look calls the constraint solving algorithm defined in [PITH_FULL_IMAGE:figures/full_fig_p037_17.png]
Figure 18
Figure 18. Figure 18: Constraint solving. C.6 Algorithmic Consistency [PITH_FULL_IMAGE:figures/full_fig_p038_18.png]
Figure 19
Figure 19. Figure 19: Algorithmic consistency [PITH_FULL_IMAGE:figures/full_fig_p040_19.png]
Figure 20
Figure 20. Figure 20: Decorated algorithmic subtyping (only showing non-trivial rules). [PITH_FULL_IMAGE:figures/full_fig_p060_20.png]
Figure 21
Figure 21. Figure 21: Decorated algorithmic consistency. We write C;𝜓 ⇝ Ψ for the tag-solving counterpart of constraint solving. The ordinary judgement C; 𝑃 ⇝ 𝑄 takes an input skeleton 𝑃 and produces an output skeleton 𝑄. In contrast, C;𝜓 ⇝ Ψ takes a decorated candidate 𝜓 and computes the …
Figure 22
Figure 22. Figure 22: Decorated tag solving. E.2 Soundness of Subtyping In this section, we prove soundness of algorithmic subtyping with respect to declarative subtyping. Theorem 4.5 (Soundness of subtyping). Given a subtyping problem (Θ0; n; m; 𝑃0; 𝑃), if Θ0 [𝑃0]-- n m 𝑃 ⩽ 𝑄 ⊣ Θ1, then (…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

74 extracted references · 11 canonical work pages

  1. [1]

    https://github.com/4y8/modal-effect-types/tree/frost

    2026.Metlimplementation. https://github.com/4y8/modal-effect-types/tree/frost

    2026

  2. [2]

    1985.The lambda calculus - its syntax and semantics

    Hendrik Pieter Barendregt. 1985.The lambda calculus - its syntax and semantics. Studies in logic and the foundations of mathematics, Vol. 103. North-Holland

    1985

  3. [3]

    Ishan Bhanuka, Lionel Parreaux, David Binder, and Jonathan Immanuel Brachthäuser. 2023. Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference.Proc. ACM Program. Lang.7, OOPSLA2 (2023), 431–459. doi:10.1145/3622812

    work page doi:10.1145/3622812 2023

  4. [4]

    Didier Le Botlan and Didier Rémy. 2003. MLF: raising ML to the power of system F. InProceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, Colin Runciman and Olin Shivers (Eds.). ACM, 27–38. doi:10.1145/944705.944709

    arXiv 2003

  5. [5]

    Peter Buneman, Sanjeev Khanna, and Wang Chiew Tan. 2001. Why and Where: A Characterization of Data Provenance. InDatabase Theory - ICDT 2001, 8th International Conference, London, UK, January 4-6, 2001, Proceedings (Lecture Notes in Computer Science, Vol. 1973), Jan Van den Bussche and Victor Vianu (Eds.). Springer, 316–330. doi:10.1007/3-540- 44503-X_20

    doi:10.1007/3-540- 2001

  6. [6]

    Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek. 2019. Gradual typing: a new perspective. Proc. ACM Program. Lang.3, POPL (2019), 16:1–16:32. doi:10.1145/3290329

    doi:10.1145/3290329 2019

  7. [7]

    Jacek Chrząszcz. 1998. Polymorphic subtyping without distributivity. InMathematical Foundations of Computer Science 1998, Luboš Brim, Jozef Gruska, and Jiří Zlatuška (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 346–355

    1998

  8. [8]

    Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira. 2023. Greedy Implicit Bounded Quantification.Proc. ACM Program. Lang.7, OOPSLA2 (2023), 2083–2111. doi:10.1145/3622871

    work page doi:10.1145/3622871 2023

Show all 74 references
  1. [9]

    Luis Damas and Robin Milner. 1982. Principal Type-Schemes for Functional Programs. InProceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Albuquerque, New Mexico)(POPL ’82). Association for Computing Machinery, New York, NY, USA, 207–212. ...

    1982

  2. [10]

    Krishnaswami

    Jana Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and easy bidirectional typechecking for higher-rank polymorphism. InACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013, Greg Morrisett and Tarmo Uustal...

    2013

  3. [11]

    Jana Dunfield and Frank Pfenning. 2004. Tridirectional typechecking. InProceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, Neil D. Jones and Xavier Leroy (Eds.). ACM, 281–292. doi:10.1145/9...

    2004

  4. [12]

    Frank Emrich, Sam Lindley, Jan Stolarek, James Cheney, and Jonathan Coates. 2020. FreezeML: complete and easy type inference for first-class polymorphism. InProceedings of the 41st ACM SIGPLAN International Conference on Bidirectional Typing with Freezing, Skeletons, and Ghost...

    2020

  5. [13]

    Frank Emrich, Jan Stolarek, James Cheney, and Sam Lindley. 2022. Constraint-based type inference for FreezeML. Proc. ACM Program. Lang.6, ICFP (2022), 570–595. doi:10.1145/3547642

    2022 doi

  6. [14]

    Jacques Garrigue and Didier Rémy. 1999. Semi-Explicit First-Class Polymorphism for ML.Inf. Comput.155, 1-2 (1999), 134–169. doi:10.1006/INCO.1999.2830

    1999

  7. [15]

    Zhichao Guan, Tailai Yu, Di Wang, and Zhenjiang Hu. 2026. Localizing Type Errors for Syntactic Sugar by Lifting. Proc. ACM Program. Lang.10, OOPSLA1, Article 145 (April 2026), 27 pages. doi:10.1145/3798253

    2026 doi

  8. [16]

    Adam Gundry, Conor McBride, and James McKinna. 2010. Type Inference in Context. InMSFP@ICFP. ACM, 43–54

    2010

  9. [17]

    2013.Type inference, Haskell and dependent types

    Adam Michael Gundry. 2013.Type inference, Haskell and dependent types. Ph. D. Dissertation. University of Strathclyde, Glasgow, UK. http://oleg.lib.strath.ac.uk/R/?func=dbin-jump-full&object_id=22728

    2013

  10. [18]

    Shengyi Jiang, Chen Cui, and Bruno C. d. S. Oliveira. 2025. Bidirectional Higher-Rank Polymorphism with Intersection and Union Types.Proc. ACM Program. Lang.9, POPL (2025), 2118–2148. doi:10.1145/3704907

    2025 doi

  11. [19]

    Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields

    Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical type inference for arbitrary-rank types.J. Funct. Program.17, 1 (2007), 1–82. doi:10.1017/S0956796806006034

    2007 doi

  12. [20]

    András Kovács. 2020. Elaboration with first-class implicit function types.Proc. ACM Program. Lang.4, ICFP (2020), 101:1–101:29. doi:10.1145/3408983

    2020 doi

  13. [21]

    András Kovács. 2026. Elaboration Zoo. https://github.com/AndrasKovacs/elaboration-zoo/ First-class polymorphism with dynamic order elaboration

    2026

  14. [22]

    Daan Leijen. 2008. HMF: simple type inference for first-class polymorphism. InProceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, James Hook and Peter Thiemann (Eds.). ACM, 283–294. doi:...

    2008

  15. [23]

    Daan Leijen. 2009. Flexible types: robust type inference for first-class polymorphism. InProceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). AC...

    2009

  16. [24]

    Daan Leijen and Wenjia Ye. 2025. Principal Type Inference under a Prefix: A Fresh Look at Static Overloading.Proc. ACM Program. Lang.9, PLDI, Article 205 (June 2025), 24 pages. doi:10.1145/3729308

    2025 doi

  17. [25]

    1990.Definition of standard ML

    Robin Milner, Mads Tofte, and Robert Harper. 1990.Definition of standard ML. MIT Press

    1990

  18. [26]

    Garrett Morris

    J. Garrett Morris. 2026. Another Type Inference Algorithm for First-Class Implicit Polymorphism.Proc. ACM Program. Lang.10, ICFP (2026), 304:1–304:29. doi:10.1145/3828702

    2026 doi

  19. [27]

    Alistair O’Brien, Didier Rémy, and Gabriel Scherer. 2025. Omnidirectional type inference for ML: principality any way. arXiv:2511.10343 [cs.PL] https://arxiv.org/abs/2511.10343

    2025 arXiv

  20. [28]

    Martin Odersky, Christoph Zenger, and Matthias Zenger. 2001. Colored local type inference. InConference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, Chris Hankin and Dave Schmidt (Eds.). ACM...

    2001

  21. [29]

    Lionel Parreaux. 2026. Decoupling Resolution from Type Inference. InProceedings of the Workshop on the Implementation of Type Systems (WITS) at the 2026 ACM SIGPLAN International Conference on Principles of Programming Languages (POPL 2026). https://popl26.sigplan.org/details/...

    2026

  22. [30]

    Lionel Parreaux, Aleksander Boruch-Gruszecki, Andong Fan, and Chun Yin Chau. 2024. When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism.Proc. ACM Program. Lang.8, POPL (2024), 1418–1450. doi:10.1145/3632890

    2024 doi

  23. [31]

    Pierce and David N

    Benjamin C. Pierce and David N. Turner. 2000. Local type inference.ACM Trans. Program. Lang. Syst.22, 1 (2000), 1–44. doi:10.1145/345099.345100

    2000

  24. [32]

    Plotkin and John Power

    Gordon D. Plotkin and John Power. 2003. Algebraic Operations and Generic Effects.Appl. Categorical Struct.11, 1 (2003), 69–94. doi:10.1023/A:1023064908962

    2003 doi

  25. [33]

    Plotkin and Matija Pretnar

    Gordon D. Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects.Log. Methods Comput. Sci.9, 4 (2013)

    2013

  26. [34]

    François Pottier and Yann Régis-Gianas. 2006. Stratified type inference for generalized algebraic data types.SIGPLAN Not.41, 1 (Jan. 2006), 232–244. doi:10.1145/1111320.1111058

    2006

  27. [35]

    Russo and Dimitrios Vytiniotis

    Claudio V. Russo and Dimitrios Vytiniotis. 2009. QML: explicit first-class polymorphism for ML. InProceedings of the 2009 ACM SIGPLAN Workshop on ML(Edinburgh, Scotland)(ML ’09). Association for Computing Machinery, New York, NY, USA, 3–14. doi:10.1145/1596627.1596630

    2009

  28. [36]

    Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. 2020. A quick look at impredicativity. Proc. ACM Program. Lang.4, ICFP (2020), 89:1–89:29. doi:10.1145/3408971

    2020 doi

  29. [37]

    Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. 2018. Guarded impredicative polymorphism. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implemen- tation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, J...

    2018

  30. [38]

    Siek and Walid Taha

    Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. InProceedings of the 2006 Scheme and Functional Programming Workshop. University of Chicago, Chicago, IL, USA, 81–92. https://jsiek.github.io/home/ siek06gradual.pdf

    2006

  31. [39]

    Wenhao Tang and Sam Lindley. 2026. Rows and Capabilities as Modal Effects.Proc. ACM Program. Lang.10, POPL (2026), 923–950. doi:10.1145/3776674

    2026 doi

  32. [40]

    Wenhao Tang, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, and Anton Lorenzen. 2025. Modal Effect Types.Proc. ACM Program. Lang.9, OOPSLA1 (2025), 1130–1157. doi:10.1145/3720476

    2025 doi

  33. [41]

    Jerzy Tiuryn and Pawel Urzyczyn. 1996. The subtyping problem for second-order types is undecidable. InProceedings 11th Annual IEEE Symposium on Logic in Computer Science

    1996

  34. [42]

    Peyton Jones

    Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones. 2006. Boxy types: inference for higher-rank types and impredicativity. InProceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-2...

    2006

  35. [43]

    Andrew K. Wright. 1995. Simple Imperative Polymorphism.LISP Symb. Comput.8, 4 (1995), 343–355

    1995

  36. [44]

    Xu Xue, Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira. 2026. Local Contextual Type Inference.Proc. ACM Program. Lang.10, POPL, Article 11 (Jan. 2026), 30 pages. doi:10.1145/3776653

    2026 doi

  37. [45]

    Xu Xue and Bruno C. d. S. Oliveira. 2024. Contextual Typing.Proc. ACM Program. Lang.8, ICFP, Article 266 (Aug. 2024), 29 pages. doi:10.1145/3674655

    2024 doi

  38. [46]

    Eric Zhao, Raef Maroof, Anand Dukkipati, Andrew Blinn, Zhiyi Pan, and Cyrus Omar. 2024. Total Type Error Localization and Recovery with Holes.Proc. ACM Program. Lang.8, POPL (2024), 2041–2068. doi:10.1145/3632910

    2024 doi

  39. [47]

    Jinxu Zhao and Bruno C. d. S. Oliveira. 2022. Elementary Type Inference. In36th European Conference on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany (LIPIcs, Vol. 222), Karim Ali and Jan Vitek (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informati...

    2022 doi

  40. [48]

    A solution to it is a tuple(𝜃1 :: Θ0⊑Θ 1;𝑃1) such that Θ1⊢𝜃 1𝑃∼𝑃 1 where Θ1⊢𝜃 1𝑃0 ▶𝑃1

    A problem of consistency is a tuple(Θ0;𝑃0;𝑃) where𝑃0 and𝑃 are well-formed in Θ0. A solution to it is a tuple(𝜃1 :: Θ0⊑Θ 1;𝑃1) such that Θ1⊢𝜃 1𝑃∼𝑃 1 where Θ1⊢𝜃 1𝑃0 ▶𝑃1. The solution is optimal if for any other solution(𝜃 :: Θ0⊑Θ ;𝑄) , there exists a metasubstitution 𝜁 :: Θ1⊑Θsu...

  41. [49]

    A solution to it is a metasubstitution𝜃1 :: Θ0⊑Θ 1 such that Θ1⊢𝜃 1 ˆ𝛼∼𝜃 1 ˆ𝛽

    A problem of unification of flexible variables is a tuple(Θ0; ˆ𝛼; ˆ𝛽) where ˆ𝛼∈dom(Θ 0) and ˆ𝛽∈dom(Θ 0). A solution to it is a metasubstitution𝜃1 :: Θ0⊑Θ 1 such that Θ1⊢𝜃 1 ˆ𝛼∼𝜃 1 ˆ𝛽. The solution is optimal if for any other solution𝜃 :: Θ0⊑Θ , there exists a metasubstitution ...

  42. [50]

    A solution to it is a metasubstitution𝜃1 :: Θ0,Ξ⊑Θ 1 such that Θ1⊢𝜃 1𝑃∼𝜃 1 ˆ𝛼

    A problem of assignment of a flexible variable is a tuple(Θ0; Ξ; ˆ𝛼;𝑃) where ˆ𝛼∈dom(Θ 0) and𝑃 is well-formed in Θ0,Ξ and𝑃 is not a flexible variable andΞ only contains declarations of flexible variables appearing in𝑃. A solution to it is a metasubstitution𝜃1 :: Θ0,Ξ⊑Θ 1 such t...

  43. [53]

    Lemma C.7 (Completeness and optimality of consistency)

    Given a problem of assignment (Θ0; Ξ; ˆ𝛼;𝑃) , if Θ0|Ξ⊢ ˆ𝛼≔𝑃⊣Θ 1, then Θ0,Ξ⊑Θ 1 is a solution to it. Lemma C.7 (Completeness and optimality of consistency)

  44. [56]

    40 Wenhao Tang, Shengyi Jiang, Aghilas Y

    Given a problem of assignment(Θ0; Ξ; ˆ𝛼;𝑃) , if there exists a solution to it, then Θ0|Ξ⊢ ˆ𝛼≔ 𝑃⊣Θ 1 gives its optimal solutionΘ 0,Ξ⊑Θ 1. 40 Wenhao Tang, Shengyi Jiang, Aghilas Y. Boussaa, Sam Lindley, and Bruno C. d. S. Oliveira Θ0[𝑃0]- -Δ1|Δ 2 𝑃∼𝑄⊣Θ 1 U-Ghost Δ2∩ftv(𝑃 0)=∅ Θ0...

  45. [57]

    The erasure and refinement premises are ⌊𝑆1→𝑆 2⌋=𝑃 10 Θ⊢𝜃(𝑃 ′ 1→𝑃′

  46. [58]

    By 10 , we have𝑃=𝑃 1→𝑃 2

    ▶𝑄1→𝑄 2 11. By 10 , we have𝑃=𝑃 1→𝑃 2. By inversion on 11 , we have Θ⊢𝜃𝑃 ′ 1 ▶𝑄1 3 Θ⊢𝜃𝑃 ′ 2 ▶𝑄2 4 . By 1 and 3 and erasure,(𝜃 :: Θ0 ⊑Θ ;𝑄1) is a solution to the consistency problem (Θ0;𝑃′ 1;𝑃 1). Then by Lemma C.7, we have Θ0[𝑃′ 1]- -𝑃1∼𝑄′ 1⊣Θ 1 5 𝜃1 :: Θ1⊑Θ 6 Θ⊢𝜃 1𝑄′ 1⪯𝑄 1 7 𝜃...

  47. [59]

    ▶𝑄 3 . By IH on 1 with 2 , 3 , and context weakening on the other premises, there areC, Ξ𝑐, 𝑃𝑎, and𝜃𝑎 such that 𝑃′∼ ∀.𝑃′ 0 ☇𝛼 Ξ𝑐 ;C 4 C;𝑃𝑖 ⇝𝑃 𝑎 5 Θ0,𝛽,Ξ 𝑐⊢𝑃 𝑎 6 𝜃𝑎 :: Θ0,𝛽,Ξ 𝑐⊑Θ,𝛽 7 𝜃≡𝜃 𝑎 :: Θ0,𝛽⊑Θ,𝛽 8 Θ,𝛽|Δ⊢𝜃 𝑎𝑃𝑎⪯Ψ𝑖,Ψ𝑎 𝜓𝑎 9 . ByLE-ForallSynon 4 , we have ∀𝛽.𝑃′∼ ∀.𝑃′ 0 ☇𝛼 Ξ𝑐 ;...

  48. [60]

    We proceed by case analysis on𝑃𝑖

    Inversion on the refinement premise gives Θ,𝛽⊢𝜃𝑃 ′ 0 ▶𝑄 2 . We proceed by case analysis on𝑃𝑖. Subcase𝑃 𝑖 =∀𝛽.𝑃 ′ 𝑖 . Inversion on precision gives Θ,𝛽|Δ,𝛽⊢𝜃𝑃 ′ 𝑖⪯Ψ′ 𝑖 𝜓′ 3 Ψ𝑖 =Ψ′ 𝑖,𝜖. IH on 1 , 2 , and 3 gives𝑃𝑏 and𝜃𝑎 with 𝑃′ 𝑖∼𝑃′ 0 ⇝𝑃 𝑏 4 . Our goal follows fromSolE-Forallon 4...

  49. [61]

    Inversion on the refinement premise gives Θ,𝛽⊢𝜃( ∀.𝑃′

  50. [62]

    We proceed by case analysis on𝑃𝑖

    ▶𝑄 2 . We proceed by case analysis on𝑃𝑖. Subcase𝑃 𝑖 =∀𝛽.𝑃 ′ 𝑖 . Inversion on the precision premise gives Θ,𝛽|Δ,𝛽⊢𝜃𝑃 ′ 𝑖⪯Ψ′ 𝑖 𝜓′ 3 Ψ𝑖 =Ψ′ 𝑖,𝜖. IH on 1 , 2 , and 3 gives𝑃𝑏 and𝜃𝑎 with 𝑃′ 𝑖∼ ∀.𝑃′ 0 ⇝𝑃 𝑏 4 . Our goal follows fromSolE-ForallGhoston 4 and choosing𝑃 𝑎 =∀𝛽.𝑃 𝑏. Subcase...

  51. [63]

    We proceed by case analysis on𝑃𝑖

    Inversion on the refinement premise gives Θ⊢𝜃𝑃 ′ 0 ▶𝑄 2 . We proceed by case analysis on𝑃𝑖. Bidirectional Typing with Freezing, Skeletons, and Ghosts 105 Subcase𝑃 𝑖 = . IH on 1 and 2 with input gives𝜃𝑎 with ∼𝑃′ 0 ⇝𝑃′ 0 3 . Our goal follows fromSolE-GhostLand choosing𝑃 𝑎 =∀.𝑃′ ...

  52. [64]

    Given a problem of consistency(Θ0;𝑃0;𝑃) , if Θ0[𝑃0]- -𝑃∼𝑃 1⊣Θ 1, then(Θ0⊑Θ 1;𝑃1) is a solution to it

  53. [65]

    Given a problem of variable unification (Θ0; ˆ𝛼; ˆ𝛽) , if Θ0⊢ ˆ𝛼≃ ˆ𝛽⊣Θ 1, then Θ0⊑Θ 1 is a solution to it

  54. [66]

    Given a problem of assignment (Θ0; Ξ; ˆ𝛼;𝑃) , if Θ0|Ξ⊢ ˆ𝛼≔𝑃⊣Θ 1, then Θ0,Ξ⊑Θ 1 is a solution to it. Proof. We first augment the definition of a consistency problem to(Δ1; Δ2; Θ0;𝑃0;𝑃) where Δ1 and Δ2 are contexts of rigid type variables present in Θ0 that no flexible variables...

  55. [67]

    Case U-Flex-Flex-Id ˆ𝛼∈dom(Θ 0) Θ0⊢ ˆ𝛼≃ ˆ𝛼⊣Θ 0 Trivial

    Unification of flexible variables.We prove that Θ0⊑Θ 1 is a solution by induction on the unification derivation Θ0⊢ ˆ𝛼≃ ˆ𝛽⊣Θ 1. Case U-Flex-Flex-Id ˆ𝛼∈dom(Θ 0) Θ0⊢ ˆ𝛼≃ ˆ𝛼⊣Θ 0 Trivial. 106 Wenhao Tang, Shengyi Jiang, Aghilas Y. Boussaa, Sam Lindley, and Bruno C. d. S. Oliveira ...

  56. [68]

    CaseU-Assign-UnivGhost-Id

    Assignment.We prove that Θ0,Ξ⊑Θ 1 is a solution by induction on the assignment derivation Θ0|Ξ⊢ ˆ𝛼≔𝑃⊣Θ 1. CaseU-Assign-UnivGhost-Id . Our goal follows from reflexivity of information increase, reflexiv- ity of consistency, andC-UnivGhost2. Case U-Assign-SolveM ˆ𝛼∉ftv(𝑃)guess t...

  57. [69]

    Case U-Ghost Δ2∩ftv(𝑃 0)=∅ Θ0[𝑃0]- -Δ1|Δ 2 ∼𝑃 0⊣Θ 0 We haveΘ 0⊑Θ 0 by reflexivity

    Consistency.We prove the augmented statement above by induction on the algorithmic consis- tency derivation. Case U-Ghost Δ2∩ftv(𝑃 0)=∅ Θ0[𝑃0]- -Δ1|Δ 2 ∼𝑃 0⊣Θ 0 We haveΘ 0⊑Θ 0 by reflexivity. ByC-Ghost, we have Θ0⊢ ∼𝑃 0 1 . By reflexivity of refinement and the side condition, ...

  58. [70]

    Given a problem of consistency(Θ0;𝑃0;𝑃) , if there exists a solution to it, then Θ0[𝑃0]- -𝑃∼ 𝑃1⊣Θ 1 gives its optimal solution(Θ 0⊑Θ 1;𝑃 1)

  59. [71]

    Given a problem of variable unification (Θ0; ˆ𝛼; ˆ𝛽) , if there exists a solution to it, then Θ0⊢ ˆ𝛼≃ ˆ𝛽⊣Θ 1 gives its optimal solutionΘ 0⊑Θ 1

  60. [72]

    Given a problem of assignment(Θ0; Ξ; ˆ𝛼;𝑃) , if there exists a solution to it, then Θ0|Ξ⊢ ˆ𝛼≔ 𝑃⊣Θ 1 gives its optimal solutionΘ 0,Ξ⊑Θ 1. Proof. We first augment the definition of a consistency problem to(Δ1; Δ2; Ψ; Θ0;𝑃0;𝑆) where Δ1 and Δ2 are contexts of rigid type variables ...

  61. [73]

    By induction on the context Θ0 and case analysis on which algorithmic unification rule to use

    Unification of flexible variables.It is enough to prove that given a unification problem(Θ0; ˆ𝛼; ˆ𝛽) and a solution 𝜃 :: Θ0⊑Θ 1 Θ⊢𝜃 ˆ𝛼∼𝜃 ˆ𝛽 2 , there exists𝜃 1 andΘ 1 such that Θ0⊢ ˆ𝛼≃ ˆ𝛽⊣Θ 1 𝜃1 :: Θ1⊑Θ𝜃≡𝜃 1 :: Θ0⊑Θ. By induction on the context Θ0 and case analysis on which al...

  62. [74]

    there existΘ 1 and𝜃 1 such that Θ0|Ξ⊢ ˆ𝛼≔𝑃⊣Θ 1 𝜃1 :: Θ1⊑Θ𝜃≡𝜃 1 :: Θ0,Ξ⊑Θ

    Assignment.It is enough to prove that given an assignment problem(Θ0; Ξ; ˆ𝛼;𝑃) and a solution 𝜃 :: Θ0,Ξ⊑Θ 1 Θ⊢𝜃𝑃∼𝜃 ˆ𝛼 2 . there existΘ 1 and𝜃 1 such that Θ0|Ξ⊢ ˆ𝛼≔𝑃⊣Θ 1 𝜃1 :: Θ1⊑Θ𝜃≡𝜃 1 :: Θ0,Ξ⊑Θ. By induction on the pair of contexts Θ0|Ξ and case analysis on which algorithmic ...

  63. [75]

    We prove by induction on the declarative consistency derivation Ψ|Θ⊢𝜃𝑆∼𝑄

    Consistency.We prove for the augmented consistency problem and solution as stated at the beginning of this proof. We prove by induction on the declarative consistency derivation Ψ|Θ⊢𝜃𝑆∼𝑄 . The cases where𝑃 or𝑃0 is a flexible variable are handled by the other two parts of the l...

  64. [76]

    Case C-Ghost ·|Θ⊢ ∼𝑄 In this case𝑆= and𝑃=

    In the induction below, we assume the above three special cases have already been handled. Case C-Ghost ·|Θ⊢ ∼𝑄 In this case𝑆= and𝑃= . The solution gives 𝜃 :: Θ0⊑Θ 1 Θ|Δ 1⊢𝜃𝑃 0 ▶𝑄 2 Θ|Δ 2⊢𝜃 ▶𝑄 3 . By 2 and 3 , the side condition ofU-Ghostholds. Thus byU-Ghost, we have Θ0[𝑃0]- ...

  65. [77]

    Bidirectional Typing with Freezing, Skeletons, and Ghosts 117 By inversion on 4 , we have Θ,𝛼|Δ 2,𝛼⊢𝜃𝑃 ′ ▶𝑄 6

    ▶𝑄 5 . Bidirectional Typing with Freezing, Skeletons, and Ghosts 117 By inversion on 4 , we have Θ,𝛼|Δ 2,𝛼⊢𝜃𝑃 ′ ▶𝑄 6 . By definition of metasubstitution, 2 gives 𝜃 :: Θ0,𝛼⊑Θ,𝛼 7 . IH on 1 , 5 , 6 , and 7 gives Θ0,𝛼[ ∀.𝑃′ 0]- -Δ1|Δ 2,𝛼 𝑃′∼𝑄′⊣Θ 1,𝛼 8 𝜃1 :: Θ1,𝛼⊑Θ,𝛼 9 Θ,𝛼|Δ 1,Δ 2...

  66. [78]

    By guardedness of𝑄, inversion on 4 gives Θ|Δ 2⊢𝜃𝑃 ′ ▶𝑄 6

    Inversion on 3 gives Θ|Δ 1⊢𝜃𝑃 ′ 0 ▶𝑄 5 . By guardedness of𝑄, inversion on 4 gives Θ|Δ 2⊢𝜃𝑃 ′ ▶𝑄 6 . Bidirectional Typing with Freezing, Skeletons, and Ghosts 119 IH on 1 , 5 , 6 , and 2 gives Θ0[𝑃′ 0]- -Δ1|Δ 2 𝑃′∼𝑄′⊣Θ 1 7 𝜃1 :: Θ1⊑Θ 8 Θ|Δ 1,Δ 2⊢𝜃 1𝑄′⪯𝑄 9 𝜃≡𝜃 1 :: Θ0⊑Θ 10 ByU-U...

Pith tools

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