[m-rev.] for review: Fix bug with typechecking of coercions.

[Peter Wang]

On Tue, 02 Jul 2024 14:51:47 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> On 2024-07-01 16:52 +10:00 AEST, "Peter Wang" <novalazy at gmail.com> wrote:
> > Fix a problem where the order that the coercions are typechecked
> > can cause type variables to be bound differently.
> > 
> > For example, assuming citrus =< fruit:
> > 
> >     X = [] : list(T),
> >     coerce(X) = _ : list(fruit),
> >     coerce(X) = _ : list(citrus)
> > 
> > T could end up bound to either 'fruit' or 'citrus' depending on which
> > coercion is checked first, due to unification of the type variable in
> > the coerce argument type, and the target type of the coercion.
> 
> That seems like a *very* rare situation. Did you come across it "in the wild",
> or did you construct it when you found something that made you go "hang on ..."?
> 

The latter.

> > --- a/compiler/typecheck_clauses.m
> > +++ b/compiler/typecheck_clauses.m
> 
> > @@ -2503,8 +2502,8 @@ compare_types_corresponding(TypeTable, TVarSet, Comparison,
> >  
> >  %---------------------------------------------------------------------------%
> >  
> > -    % Remove satisfied coerce constraints from each type assignment,
> > -    % then drop any type assignments with unsatisfied coerce constraints
> > +    % Check coerce constraints in each type assignment to see if they can be
> > +    % satisfied. Drop any type assignments with unsatisfied coerce constraints
> >      % if there is at least one type assignment that does satisfy coerce
> >      % constraints.
> >      %
> 
> "that DOES satisfy" or "that CAN satisfy"? Either way, that comment should
> explain *why* you answer that question the way you do.
> 

I've reworded the comment.

> > +report_unresolved_coerce_from_to(ClauseContext, Context, TVarSet,
> > +        FromType, ToType) = Spec :-
> > +    InClauseForPieces = in_clause_for_pieces(ClauseContext),
> > +    FromTypeStr = mercury_type_to_string(TVarSet, print_num_only, FromType),
> > +    ToTypeStr = mercury_type_to_string(TVarSet, print_num_only, ToType),
> > +    ErrorPieces = [words("error: cannot coerce from")] ++
> > +        [quote(FromTypeStr), words("to"), quote(ToTypeStr), suffix("."), nl] ++
> > +        [words("The type of the coerced argument is")] ++
> > +        color_as_incorrect([words("unresolved.")]) ++ [nl],
> > +    Spec = spec($pred, severity_error, phase_type_check, Context,
> > +        InClauseForPieces ++ ErrorPieces).
> 
> I think this error message text very much embodies your view as the
> compiler implementor. From a user's point of view, the "cannot coerce" part
> is just the consequence; the actual *error* is a type being unresolved.
> That being so, I would (a) put that part first in the message, and, more important,
> I would (b) name the variable whose type is unresolved (at least if it actually
> *has* a name).

Done. This required adding a prog_var to the coerce_constraint type.
I'll see about making the other coerce type error messages include the
variable name as well, in a separate change.

I've followed your other suggestions. Thanks.

Peter