> The job of a compiler error message is to prove to the user that their code is invalid
The job of the compiler error message is to convey why the compiler couldn’t demonstrate the code is correct. The code may be valid but the compiler just can’t prove it (analyses are sound but not complete unless the language is strongly normalizing)
Practically the difficulty of generating error messages is one reason why "we can't have nice things". I ran into this problem while trying to write an adventure game (like Zork) in Drools. Drools sucks in a lot of stuff from a Java compiler and mashes it into a production rules framework and the result is I was getting error messages that made no sense at all and thus gave up on the project.
One approach to compiler development is one of successive transformations and it is possible to cut compilers into very thin slices like the original FORTRAN for the IBM 1401. Similarly you can go beyond the methods taught in Graham's On Lisp to do rather complex metaprogramming in Lisp or some other language, trouble is that an error manifests at stage N+5 but the information required to explain what went wrong was elided at stage N so it is quite difficult to figure out what's going wrong.
Sure, but the goal when designing a compiler and its error messages is to prove to the user that their code in invalid. Most practical type systems are going to be either unsound or incomplete (or both), but the goal should be to make encountering those limitations rare in practice.
I've been working on a type checker for a language with ad-hoc overloading and what I did was have the checker proceed iteratively, making passes over the set of constraints and applying deduction rules. So it never guesses, branches, or has to backtrack. If it can't make progress because there's too much overloading, it gives up and asks the user to add some type annotations. I suspect this will actually work quite well in practice even if it can't type check some valid programs.
Hot take: the primary role of a compiler is to turn malformed code into human readable diagnostics. They are error reporting tools with a codegen is side-gig.
Minor nit:
> The job of a compiler error message is to prove to the user that their code is invalid
The job of the compiler error message is to convey why the compiler couldn’t demonstrate the code is correct. The code may be valid but the compiler just can’t prove it (analyses are sound but not complete unless the language is strongly normalizing)
Practically the difficulty of generating error messages is one reason why "we can't have nice things". I ran into this problem while trying to write an adventure game (like Zork) in Drools. Drools sucks in a lot of stuff from a Java compiler and mashes it into a production rules framework and the result is I was getting error messages that made no sense at all and thus gave up on the project.
One approach to compiler development is one of successive transformations and it is possible to cut compilers into very thin slices like the original FORTRAN for the IBM 1401. Similarly you can go beyond the methods taught in Graham's On Lisp to do rather complex metaprogramming in Lisp or some other language, trouble is that an error manifests at stage N+5 but the information required to explain what went wrong was elided at stage N so it is quite difficult to figure out what's going wrong.
Sure, but the goal when designing a compiler and its error messages is to prove to the user that their code in invalid. Most practical type systems are going to be either unsound or incomplete (or both), but the goal should be to make encountering those limitations rare in practice.
I've been working on a type checker for a language with ad-hoc overloading and what I did was have the checker proceed iteratively, making passes over the set of constraints and applying deduction rules. So it never guesses, branches, or has to backtrack. If it can't make progress because there's too much overloading, it gives up and asks the user to add some type annotations. I suspect this will actually work quite well in practice even if it can't type check some valid programs.
For reporting the expected type on mismatch, I do something similar in RCL to be able to track the source of the expectation: https://ruudvanasseldonk.com/2024/implementing-a-typechecker...
Hot take: the primary role of a compiler is to turn malformed code into human readable diagnostics. They are error reporting tools with a codegen is side-gig.