Open SimonJF opened 5 years ago
jstolarek
commented
5 years ago whether this would be a sensible thing to add.
From a user perspective I think this would be useful. In OCaml, whenever dealing with polymorphic variant errors, the compiler would report two enormous types and then add "Types of tag X mismatch" pointing out how the types of one specific tag differ, which was a great help in pinning down the actual problem.
jamescheney
commented
5 years ago This reminds me of something I've been wondering about, incidentally. There's been a line of work on something called "type error slicing", for polymorphic languages, which mostly aims to provide error messages that highlight the parts of the program that you should look at to understand a type error.
However, it seems like something similar could be useful for variant type errors: specifically, what I'd think would be most useful would be something like this:
examples/sessions/chatserver/chatServer.links:91: Type error: The cases of an offer should match the type of its patterns, but the pattern
`s'
has type
`Supervisor'
while the subsequent patterns have type of the form
`[&||...,NewTopic:End|&]'
which does not match the expected type of the form
`[&||...,NewTopic:?(ChatSessions.Topic).End|&]'
Specifically, could not match ?(ChatSessions.Topic).End against Endi.e. where we elide all of the stuff that does match, and just show the context needed to understand where something doesn't match. This is not a realistic proposal yet but might be an interesting research problem.
jamescheney
commented
4 years ago All gripers take a Unify.error as an argument. Unify.error is a variant with two cases: Msg and PresentAbsentError. Most gripers ignore this argument. The only exception is record_pattern which pattern matches on error to see wiether it is PresentAbsentClash.
The only place PresentAbsentClash is mentioned in code is in a comment in unify.ml, where instead an ordinary Msg is returned.
So: the infrastructure for doing something better here seems to be present, btu is not being used. An easy thing to do would be to print the unification error associated with each griper by default, as it typically gives a somewhat more relevant reason for the unification failure. (cf. #186 and #447). A more ambitious thing to do could be to enumerate the different kinds of unification failures in the error variant type and perhaps different gripers coudl use this information in different ways. Also, the unification errors seem to use internal variable numbers which ought to be related back to the source syntax / variable names.
It also seems like it would be sensible to remove the PresentAbsentClash error kind and the associated dead code.
jamescheney
commented
4 years ago The main problem with externalizing unification errors is that they are printing variables as integers as illustrated in #447. The refresh_tyvar_names mechanism needs to be used in unify.ml to avoid this (or perhaps, the printing of types/variables delayed to the handling griper which already does this to refresh the names of type variables used in the expressions whose unification failed).
Nowadays, when writing applications, I tend to have
debug=trueset primarily in order to get the unification errors displayed. Take the following error message for example:In the more recent branch without recursive type inlining, we have the more minimal:
Nevertheless, the exact unification error is:
which is far more descriptive.
Ideally, I'd like something such as:
My question, therefore, is whether this would be a sensible thing to add. Would there be any places where adding the unification error would be more difficult to understand than the remainder of the error, or expose internal state not present in the rest of the error message? If so, would there be any simple way of rectifying this, or is this a non-starter?