Scalable Type Inference for Intrinsically-Typed Binders
summary
Claims that guided type inference using bi-directionality hints plus automation in Ltac2 makes intrinsically-typed binders practical in Rocq: variable contexts are forced top-down, solving missing-scope proofs that bottom-up inference misses. Implementation shows a working strategy: propagate contexts in a first pass then run bottom-up return-type unification, or use a wrapper/pre-type Ltac2 routine to defer unification. Experiments demonstrate previously failing terms now type-check, while some prior-success terms require the two-pass or wrapper workarounds.
AI-written summary · about
chapters (13)
- 0:00Intrinsically typed binders intro
- 0:21Abusing Roc’s type checker
- 1:03DSL with deeply embedded syntax
- 2:08Typing rules in Roc’s dependent types
- 3:11Variable contexts and scoping
- 3:54Type checking examples
- 4:57Proof inference limitations
- 5:59Type checking walkthrough
- 8:07Misalignment in type checking order
- 8:52Bidirectional type checking hints
- 10:58Results and limitations with hints
- 11:42Two-pass type inference
- 12:07Q&A
related talks
15mTaming Type Annotations in Gradual Typing
18mBidirectional Typing for Erlang
33mStatically Typed Interpreters
40mGuarded Impredicativity
45mDepending on Types
19mAbstracting Gradual Typing Moving Forward : Precise and Space-Efficient
33mTyped Clojure: From Optional to Gradual Typing
49mThe Trouble With Types