<div dir="ltr">I agree that unnecessarily chatty error messages are bad, though, from what little I've seen, I think the existing error messages are sometimes already too chatty. For example, I suspect that this error message would be easier to read if it said something like:<div>
<br></div><div><div>In environment</div><div>?292::{?U}</div><div>?293::{?V}</div><div>?294::Type</div><div><br></div><div>Expression: s.#Text</div><div> Have con: string</div><div> Need con: [?292 ~ ?293] => ?294</div>
<div><br></div><div>Incompatible constructors</div><div>Have: string</div><div>Need: [?292 ~ ?293] => ?294</div></div><div><br></div><div>In general, I think it's better to have more lines with a lower information density; that way, I can pick how much I want to consider at once, and don't need to think about the types of unification variables if the shape is already wrong.</div>
<div><br></div><div>I also think that in the case where it's not immediately obvious what the fix is from the type mismatch, it can be helpful to know where the constraints come from (possibly this information should be conditionally enabled with a verbosity flag). For example, </div>
<div><br></div><div>...</div><div><br></div><div>Expression: s.#Text</div><div> Have con: string</div><div> From filename:linenumber:range:</div><div><span style="font-family:arial,sans-serif;font-size:13px"> fun validator (s:{Text:string}) : transaction page =</span><br>
</div><div><span style="font-family:arial,sans-serif;font-size:13px"> ~~~~~~~</span></div><div> Need con: [?292 ~ ?293] => ?294</div><div> From filename:linenumber:range</div><div><span style="font-family:arial,sans-serif;font-size:13px"> case s.Text ! = "" of</span><br>
</div><div><span style="font-family:arial,sans-serif;font-size:13px"> ~~~~~</span></div><div><span style="font-family:arial,sans-serif;font-size:13px"><br></span></div><div>Incompatible constructors</div><div>
Have: string</div><div>Need: [?292 ~ ?293] => ?294</div><div><br></div><div>or something like that, and perhaps have an "even more verbose" option that gives the type of the head of the enclosing expression, as well as all of its arguments and their types?</div>
<div><br></div><div>I seem to recall finding the error messages rather impenetrable when I tried to learn Ur/Web, and they're part of the reason I still haven't gotten around to learning it (the others are: not as many examples around as, e.g., python, javascript, Coq; lack of time).</div>
<div><br></div><div>-Jason</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Jan 5, 2014 at 1:15 PM, Adam Chlipala <span dir="ltr"><<a href="mailto:adamc@csail.mit.edu" target="_blank">adamc@csail.mit.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On 01/04/2014 02:43 PM, Jason Gross wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
As an idea to improve error messages, would it be possible to tag unification hints with where they come from, so that the error message would include something like "... constraint comes from passing 's.Text' as an argument to postfix '!'" or something?<br>
</blockquote>
<br></div>
That's an interesting idea. My first reaction is that the extra information you're suggesting is easy to deduce by inspecting the code. A unification failure for an expression is only triggered in the context of its immediately enclosing parent expression.<br>
<br>
However, I'd never before considered the consequences of parsing misunderstandings like this one! Effectively, shouting out the kind of enclosing parent expression could help the user see how the code is really being parsed.<br>
<br>
At the same time, chattier type inference output can make messages harder to read in the common case, and I've never seen this particular kind of error come up in the wild before. So, for now, I think I'll leave the error messages alone, but I'll keep your suggestion in mind.<div class="HOEnZb">
<div class="h5"><br>
<br>
______________________________<u></u>_________________<br>
Ur mailing list<br>
<a href="mailto:Ur@impredicative.com" target="_blank">Ur@impredicative.com</a><br>
<a href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" target="_blank">http://www.impredicative.com/<u></u>cgi-bin/mailman/listinfo/ur</a><br>
</div></div></blockquote></div><br></div>