[m-rev.] for review: do occurs checks on the parse tree

[Julien Fischer]

Hi Zoltan,

On Tue, 1 Oct 2019, Zoltan Somogyi wrote:

> For review by anyone. I am particularly looking for feedback on the
> issue of warnings for ok code, such as worst_purity(P1, P2) \= P2.
> Can people think of a better way to handle them? All the ways I can
> think of to avoid warning about such cases are far too expensive
> in compiler execution time compared to the rarity of the misleading
> warnings they would avoid.

The two cases you detected could have been avoided if we knew that
worst_purity/2 was a function.  Is gathering together all the visible
function names and arities really going to be that expensive.  (We
could delay doing so until a situation like the above is detected.)

(Basing the decision on whether to emit the warning on whether a
symbol does not correspond to a visible function is obviously not
perfect but it should suffice for most cases except where some
fairly inadvisable overloading has taken place -- and that's likely
to cause its own problems.)

OTOH, since it's only two instances out of the entire Mercury system
I'm inclined to simply say issuing warnings for such ok code is fine.

(Actually, the test that got the warning in library/term_to_xml.m looks
a bit questionable anyway, we iterate over the string once to check it
is alphabetic, then again to convert into lower case, and then again to
compare it with the orgiginal; that test could just be
string.all_match(is_lower, Head)).

> Warn about occurs check violations in parse trees.
> 
> Until now, we have generated warnings about occurs check violations
> in the HLDS. Since the HLDS is in superhomogeneous form, this means
> we warn for X = f(X), but not for Xs = [X1, X2 | Xs]. The reason is
> that the latter expands to Xs = [X1 | Xs1], Xs1 = [X2 | Xs],
> and neither of those two unifications fails the occurs check.

> compiler/superhomogeneous.m:
>     While expanding terms into superhomogeneous form, keep track
>     of which variables have been unified with a term *or an ancestor
>     of that term*. In the case above, we know that Xs1 is *part of* Xs,
>     so unifying it with [X2 | Xs] is an occurs check violation.
>
>     Generate a warning for such violations. This is only a warning,
>     because in the parse tree, function symbols can be not just
>     data constructors but also function applications, and we can't
>     say which is which. While X = f(X) is a real problem if f is
>     a data constructor, it may be perfectly ok code (a test for a
>     fixpoint) if f is a function.
> 
> compiler/modecheck_unify.m:
>     Disable the HLDS version of this warning, to avoid warning
>     about the problem twice. (This diff leaves the infrastructure
>     supporting the HLDS warning remains in place, in case we want
>     to enable it again.)
> 
> compiler/prog_data.m:
> library/term_to_xml.m:
>     Change code to avoid the new warning.
> 
> tests/invalid/ambiguous_overloading_error.err_exp:
> tests/invalid/max_error_line_width.err_exp:
> tests/invalid/occurs.err_exp:
> tests/warnings/unify_x_f_x.exp:
>     Update these expected outputs to expect the new warning,
>     and (in some cases) not to expect its HLDS version.

There should be a command line option for disabling this warning.

The diff looks fine otherwise.

Julien.