# Gradually debugging type errors

*2024-09-01 — idea*


Reasoning about type errors is very difficult, and requires shifting between
static and dynamic types. In OCaml, the type checker asserts ill-typedness but
provides little in the way of understanding why the type checker inferred such
types. These direct error messages are difficult to understand even for
experienced programmers working on larger codebases.

This project will explore how to use gradual types to reason more effectively
about such ill-typed programs, by introducing more dynamic types to help some
users build an intuition about the problem in their code. The intention is to
enable a more exploratory approach to constructing well-typed programs.


Some relevant reading:
- [Refined Criteria for Gradual Typing](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.274)
- [Dynamic Type Inference for Gradual Hindley-Milner Typing](https://arxiv.org/abs/1810.12619)
- [Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong)](https://arxiv.org/abs/1606.07557)

## Links

The project was completed successfully by [Max Carroll](https://maxcarroll0.github.io/blog/), who wrote it up as
(:2025-decomposable-type-highlighting) and presented it at the HATRA workshop
colocated with ICFP 2025, complete with a live demo of type-level debugging in
Hazel. There are more details in my [What I learnt at ICFP/SPLASH 2025 about OCaml, Hazel and FP](https://anil.recoil.org/notes/icfp25-what-i-learnt) writeup from the
conference. [Max Carroll](https://maxcarroll0.github.io/blog/) went on to extend this work in his Part III project on
(:bidirectional-type-slicing).
Status: Completed
Level: PartII
Year: 2024
Project: Planetary Computing
Supervisors: Patrick Ferris, Anil Madhavapeddy
Students: Max Carroll

## Related

- [.plan-26-28: What fun papers piled up while I was out at sea](https://anil.recoil.org/notes/2026w28) (note, 2026-07-12)
- [What I learnt at ICFP/SPLASH 2025 about OCaml, Hazel and FP](https://anil.recoil.org/notes/icfp25-what-i-learnt) (note, 2025-10-09)
- [Bidirectional type slicing](https://anil.recoil.org/ideas/bidirectional-type-slicing) (idea, 2025-10-01)
- [OxCaml Labs](https://anil.recoil.org/projects/oxcaml) (project, 2025-01-01)

---
Canonical: https://anil.recoil.org/ideas/gradual-type-error-debugging
Type: idea
Tags: functional, hazel, ocaml, javascript, types