[m-rev.] for review: restrict some typeclass definitions in .int{, 3} files to be abstract

[Zoltan Somogyi]

On 2023-08-02 03:02 +02:00 CEST, "Peter Wang" <novalazy at gmail.com> wrote:
> That looks fine.

Thank you.

>> +% XXX Including the above subtype definitions generates errors like these:
>> +% term_conversion.m:199: In clause for predicate `term_to_univ_special_case'/6:
>> +% term_conversion.m:199:   error: ambiguous overloading causes type ambiguity.
>> +% term_conversion.m:199:   Possible type assignments include:
>> +% term_conversion.m:199:   V_95:
>> +% term_conversion.m:199:     `some [T] (list.list(T))'
>> +% term_conversion.m:199:   or
>> +% term_conversion.m:199:     `some [T] (list.non_empty_list(T))'
>> +% UNDOC_PART_END
> 
> This occurs because [|]/2 is a constructor of both list(T) and
> non_empty_list(T). The fix is to use explicit type qualification,
> as below.

By definition, every constructor of a subtype occurs in its supertype,
and it hasn't caused problems before. However, it does in this case.

The diff you attached works, and fixes the problem in the library directory.
But in the compiler directory, we get over 400 lines of error messages.
For one file, we get

error_type_util.m:214: In clause for function `higher_order_type_pieces'/5:
error_type_util.m:214:   warning: highly ambiguous overloading.
error_type_util.m:214:   The following symbols were overloaded in the following
error_type_util.m:214:   contexts.
error_type_util.m:199:   The function symbol `[]'/0.
error_type_util.m:199:   The possible matches are:
error_type_util.m:199:     the type constructor `list.empty_list'/1,
error_type_util.m:199:     the type constructor `list.list'/1.
error_type_util.m:200:   The function symbol `[]'/0 is also overloaded here.
error_type_util.m:201:   The function symbol `[]'/0 is also overloaded here.
error_type_util.m:206:   The function symbol `[]'/0 is also overloaded here.
error_type_util.m:208:   The function symbol `[]'/0 is also overloaded here.
error_type_util.m:209:   The function symbol `[]'/0 is also overloaded here.
error_type_util.m:210:   The function symbol `[]'/0 is also overloaded here.
error_type_util.m:211:   The function symbol `[]'/0 is also overloaded here.
error_type_util.m:212:   The function symbol `[]'/0 is also overloaded here.
error_type_util.m:200:   The function symbol `[|]'/2.
error_type_util.m:200:   The possible matches are:
error_type_util.m:200:     the type constructor `list.list'/1,
error_type_util.m:200:     the type constructor `list.non_empty_list'/1.
error_type_util.m:201:   The function symbol `[|]'/2 is also overloaded here.
error_type_util.m:197:   The function symbol `higher_order_type'/5.
error_type_util.m:197:   The possible matches are:
error_type_util.m:197:     the type constructor
error_type_util.m:197:     `parse_tree.prog_data.mer_type'/0,
error_type_util.m:197:     the type constructor
error_type_util.m:197:     `parse_tree.prog_type.non_kinded_type'/0.
error_type_util.m:200:   The function symbol `words'/1.
error_type_util.m:200:   The possible matches are:
error_type_util.m:200:     the type constructor
error_type_util.m:200:     `parse_tree.error_spec.format_piece'/0,
error_type_util.m:200:     function `string.words'/1.
error_type_util.m:201:   The function symbol `words'/1 is also overloaded here.
error_type_util.m:205:   The function symbol `list.map'/2.
error_type_util.m:205:   The possible matches are:
error_type_util.m:205:     predicate `list.map'/3,
error_type_util.m:205:     function `list.map'/2.

> Perhaps we can point out which lines the terms with ambiguous types
> occur on.

As shown above, this already happens. (Though if e.g. [] occurs
more than once on a line, you get just one message for that line.)

I am guessing that subtype checking is not treating subtypes of lists
any differently than subtypes of other types, which was my first thought,
and that instead, the factor that distinguishes the errors we get for empty_list
and non_empty_list is that there are clauses that contain a *lot* of occurrences
of [] and [|]. When every such occurrence doubles the number of type
assignments in the type checker, we soon exceed the limit. Do you
agree with this diagnosis?

If yes, then I want to keep the definitions of empy_list and non_empty_list
commented out, but with the comment updated to reflect this diagnosis.
The reason for that is that I don't like the idea of either us, or other Mercury
programmers, having to go around adding explicit type qualifications to lots
of nils and cons just to get the number of type assignments in the type checker
below the ambiguity threshold.

It would be nice if the typechecker could handle subtypes *without*
this kind of doubling. Do you know of  any way, preferably a simple way,
to accomplist that? One idea is that when a var is bound to e.g. [],
then instead of recording its type as list and empty_list in two separate
type assignments, record it as just empty_list, but with a marker that
effectively says "or any supertype". Then, if it ever occurs in a context
that needs it to be list, then just change its type to list in that type assignment,
since list is a supertype of empty_list. This update wouldn't happen without
that marker. Would this be a viable approach, do you think?

Zoltan.