It is not always easy to correct a type error especially for novice programmers. When a type error occurs, the compiler shows a type error message, but often, it does not show the true cause of the type error. Why? Because it is impossible in general. Without knowing the intention of the programmer, the compiler cannot choose a single cause among multiple possible causes of the type error.

To locate the true cause of a type error, we have built an interactive type debugger for OCaml that incorporates programmer’s intention. When a type error occurs, the type debugger asks a series of questions to the programmer. By correctly answering these questions, we are lead to the true source of the type error.

In this talk, I will first introduce the principle of the type debugger and show how a simple but crucial idea leads to a practicable type debugger. I then describe requirements and challenges for such a tool to be effective in the real use cases, such as in a classroom.