[m-rev.] for review: better error messages for lambda exprs

[Julien Fischer]

Hi,

On Sun, 8 May 2016, Zoltan Somogyi wrote:

> On Sun, 8 May 2016 15:11:16 +1000, Peter Wang <novalazy at gmail.com> wrote:
>> Let me try to summarise it.  The compiler will reject the use of these
>> names as data-functors and compound data-terms:
>>
>>     :           (still allowed as a data-functor)
>>     with_type
>>     @           (still allowed as a data-functor)
>>     ^           (still allowed as a data-functor)
>>     :=
>>     :-
>>     -->
>>     is
>
> After this change, one-character names above are still allowed
> to be used with arity 0 because the lexer generates the same output
> when it sees e.g. @ as when it sees '@'. Programs must be able to
> use every character as a character constant. If it weren't for this,
> I would also want to disallow their use with arity 0 as well.
>
>> Those names are not rejected as part of type definitions.  It is
>> possible to construct/deconstruct terms with those names through the
>> standard library, just not directly in Mercury code.
>
> I would be happy to change that, and reject any attempt to use
> any operator or word that has a meaning in Mercury syntax as the
> name of a data constructor, or as the name of any other user-defined
> entity, such as type name, mode name, predicate name etc. This includes
> @, ^ and :.
>
> Can people please vote: would you support or oppose such a change?

I support such a change.

...

>> Can we improve error messages another way, like generating special error
>> messages if there is a type failure involving the names above?
>
> Mistakes in the uses of these names usually lead to more than one type error;
> have a look at the old version of lambda_syntax_error.err_exp. Some of
> these involve the badly-used keywords, but some do not: instead, they
> report errors for the terms below them, such as the ones whose function
> symbols are "::", "in" and "semidet".
>
> If I understand you correctly, you are asking whether we can modify
> the typechecker to replace the several type errors that currently result
> from e.g. a malformed lambda expression with a single error message
> that says in effect "these type errors result from a malformed lambda
> expression". My answer is that while that is theoretically possible,
> the resulting code would *not* be just a type checker: it would be a
> combination of type checker and forensic parser. I say "forensic"
> because its task would be even harder than the task of the parser:
> it would have to parse not a single term that is intended to be
> a lambda expression but isn't, but a *sequence* of the superhomogeneous
> unifications that result from the flattening of the original malformed term.
> To know which type errors it should include in the above umbrella
> message and which it shouldn't, it would have to find out exactly which
> unifications are part of the original malformed-lambda-expression term,
> which is conceptually equivalent to reconstructing that term.
>
> I would much rather directly generate an error message that says
> "you shot this term" than indirectly a message that says "the blood
> spatter seems to indicate that you shot this term". And I would
> much rather generate error messages about syntax errors in
> the parser, rather than the type checker.

Agreed.

Julien.