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

[Peter Wang]

On Wed, 02 Aug 2023 11:53:41 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> 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 ambiguity can be resolved usually, but not in this case.

I think where this problem will arise most in practice is when you try
to print out a term:

    print([1, 2, 3], !IO)

Is that a list(int) or non_empty_list(int)? The end result is the same,
but the compiler doesn't know that.

> 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.
> 

These ambiguities can be resolved, but the compiler warns about the
predicate using a lot of overloaded symbols. Maybe we should raise the
default value of --typecheck-ambiguity-warn-limit.

> > 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.)
> 

In term_conversion.m, it took me some trial and error to find the
location where I should place the type qualifiers.

> 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?

Yes.

> 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?

That does seem worth investigating.

Some initial thoughts:

- At the end, we must remember to check that all program variables are
  assigned a proper type, so there are no more "or any supertype" left.

- The "marker" would probably be placed in the type bindings map of the
  type_assign structure.

- When a variable is to be assigned a subtype-or-any-supertype,
  we should introduce a type variable, then bind the type variable to
  that subtype-or-any-supertype.

  This should deal with the problem of var-var unifications.
  If X = Y, then X and Y should always end up with the same type.

Peter