On 06/02/15 11:08, Richard Eisenberg wrote:
Two scattered thoughts on this issue:
- I don't think snagging all of the errors from TcErrors is quite enough. For example, the errors generated in TcHsType might also be relevant, and maybe those in TcTyClsDecls. But, getting TcErrors would be 80% of the way, I think.
Good point. Ultimately it might be nice if plugins could manipulate any error messages at all, but unsolved constraints (in TcErrors) seem like a good starting point.
- It has been suggested (I forget by whom, sorry) that sometimes this approach grabs info at the wrong level of abstraction, even for a plugin. As a case in point, I'll think about my `units` package, which implements a domain-specific type system for dimensional analysis. (I know this will be close to Adam's heart!) The errors generated by tiny misuses of this package are disastrous. But, figuring out what went wrong from an error message would still be hard, even as a plugin. Instead, it would be much better if extra checks were put in place during typechecking; if these checks fail, then the errors are easier to diagnose. I'm thinking, in particular of what's done in Helium, as presented at Haskell Implementors' Workshop 2014: http://foswiki.cs.uu.nl/foswiki/pub/Hage/ResearchTalks/hiw-helium.pdf I'm not familiar at all with Idris's approach here, but it would be interesting to compare and contrast the two to see what we can learn from others' experience.
I agree that working backwards from error messages is not necessarily the best approach, but at least it's one that we can see how to implement easily and will allow us to make some progress. Idris is a great example here - I should have credited it for the inspiration in my earlier message. Doing something Helium-like might well be useful, but it's something of a research project (Alejandro's, to be precise!) and would require rather substantial changes to the typechecker in order to control the order in which constraints are solved. For units, I would argue that the right approach is to use a typechecker plugin to implement custom constraint solving behaviour for the equational theory you want... but then I am doing exactly that, so I'm biased. ;-) Adam -- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/