[m-rev.] for review: improve typeclass constraints error messages

[Peter Wang]

[the first copy of this seems not to have come through]

Branches: main

Improve two error messages related to typeclass constraints.

1. The "unsatisfied typeclass constraints" error message didn't tell the user
the line numbers of the atomic goals which originated the constraints.

2. The "unsatisfiable typeclass constraints" error message told the user that
a set of constraints couldn't be satisfied, including the constraints it
proved to be satisfiable.  Also, it would list a top-level constraint in the
error message when some of the constraint's descendents could be satisfied.
It is more useful to tell the user about the descendants that couldn't be
satisfied.  Bug #35.

compiler/post_typecheck.m:
        Fix the first problem.

compiler/typeclasses.m:
        Fix the second problem.

tests/invalid/Mmakefile:
tests/invalid/typeclass_test_8.err_exp:
tests/invalid/unsatisfiable_constraint.err_exp:
tests/invalid/unsatisfiable_constraint_msg.err_exp:
tests/invalid/unsatisfiable_constraint_msg.m:
        Add test case and update expected error output.

diff --git a/compiler/post_typecheck.m b/compiler/post_typecheck.m
index 09f39a5..94eac3e 100644
--- a/compiler/post_typecheck.m
+++ b/compiler/post_typecheck.m
@@ -142,6 +142,7 @@
 :- import_module maybe.
 :- import_module pair.
 :- import_module set.
+:- import_module solutions.
 :- import_module string.
 :- import_module svmap.
 :- import_module svvarset.
@@ -367,7 +368,17 @@ report_unsatisfied_constraints(ModuleInfo, PredId, PredInfo, Constraints,
             list.map(constraint_to_error_piece(TVarSet), Constraints), []) ++
         [nl_indent_delta(-1)],
     Msg = simple_msg(Context, [always(Pieces)]),
-    Spec = error_spec(severity_error, phase_type_check, [Msg]),
+
+    DueTo = choose_number(Constraints,
+        "The constraint is due to:",
+        "The constraints are due to:"),
+    ContextMsgStart = error_msg(yes(Context), do_not_treat_as_first, 0,
+        [always([fixed(DueTo)])]),
+    Contexts = find_constraint_contexts(PredInfo, Constraints),
+    ContextMsgs = constraint_contexts_to_error_msgs(Contexts),
+
+    Spec = error_spec(severity_error, phase_type_check,
+        [Msg, ContextMsgStart | ContextMsgs]),
     !:Specs = [Spec | !.Specs].
 
 :- func constraint_to_error_piece(tvarset, prog_constraint)
@@ -376,6 +387,57 @@ report_unsatisfied_constraints(ModuleInfo, PredId, PredInfo, Constraints,
 constraint_to_error_piece(TVarset, Constraint) =
     [quote(mercury_constraint_to_string(TVarset, Constraint))].
 
+    % A prog_constraint cannot contain context information (see the comment on
+    % the type definition). However, a constraint_id happens to contain a
+    % goal_path so we can look up a constraint_id for a prog_constraint, then
+    % use the goal_path to reach the goal to get the context.
+    %
+:- func find_constraint_contexts(pred_info, list(prog_constraint))
+    = list(prog_context).
+
+find_constraint_contexts(PredInfo, Constraints) = Contexts :-
+    pred_info_get_clauses_info(PredInfo, ClausesInfo),
+    clauses_info_clauses_only(ClausesInfo, Clauses),
+
+    pred_info_get_constraint_map(PredInfo, ConstraintMap),
+    ReverseConstraintMap = map.reverse_map(ConstraintMap),
+    map.apply_to_list(Constraints, ReverseConstraintMap, ConstraintIdSets),
+    ConstraintIds = set.union_list(ConstraintIdSets),
+
+    % This could be more efficient.
+    FindContexts = (pred(Context::out) is nondet :-
+        set.member(ConstraintId, ConstraintIds),
+        ConstraintId = constraint_id(_, ConstraintGoalPath, _),
+        promise_equivalent_solutions [Context] (
+            list.member(Clause, Clauses),
+            goal_contains_goal(Clause ^ clause_body, Goal),
+            Goal = hlds_goal(_, GoalInfo),
+            GoalPath = goal_info_get_goal_path(GoalInfo),
+            GoalPath = ConstraintGoalPath,
+            Context = goal_info_get_context(GoalInfo)
+        )
+    ),
+    solutions(FindContexts, Contexts).
+
+:- func constraint_contexts_to_error_msgs(list(prog_context))
+    = list(error_msg).
+
+constraint_contexts_to_error_msgs([]) = [].
+constraint_contexts_to_error_msgs([Context | Contexts]) = [Msg | Msgs] :-
+    (
+        Contexts = [_, _ | _],
+        Words = "a goal here,"
+    ;
+        Contexts = [_],
+        Words = "a goal here, and"
+    ;
+        Contexts = [],
+        Words = "a goal here."
+    ),
+    Msg = error_msg(yes(Context), do_not_treat_as_first, 1,
+        [always([fixed(Words)])]),
+    Msgs = constraint_contexts_to_error_msgs(Contexts).
+
 %-----------------------------------------------------------------------------%
 
     % Report a warning: uninstantiated type parameter.
diff --git a/compiler/typeclasses.m b/compiler/typeclasses.m
index 1528e35..845ad30 100644
--- a/compiler/typeclasses.m
+++ b/compiler/typeclasses.m
@@ -112,16 +112,15 @@ perform_context_reduction(!Info) :-
     ModuleInfo = tc_info_module_info(!.Info),
     module_info_get_class_table(ModuleInfo, ClassTable),
     module_info_get_instance_table(ModuleInfo, InstanceTable),
-    list.filter_map(
-        reduce_type_assign_context(ClassTable, InstanceTable),
-        TypeAssignSet0, TypeAssignSet1),
+    list.foldl2(reduce_type_assign_context(ClassTable, InstanceTable),
+        TypeAssignSet0, [], TypeAssignSet1, [], UnsatTypeAssignSet),
     (
         % Check that this context reduction hasn't eliminated
         % all the type assignments.
         TypeAssignSet0 = [_ | _],
         TypeAssignSet1 = []
     ->
-        Spec = report_unsatisfiable_constraints(!.Info, TypeAssignSet0),
+        Spec = report_unsatisfiable_constraints(!.Info, UnsatTypeAssignSet),
         typecheck_info_add_error(Spec, !Info),
         DeleteConstraints = (pred(TA0::in, TA::out) is det :-
             % Make a new hlds_constraints structure for the type assign,
@@ -140,9 +139,11 @@ perform_context_reduction(!Info) :-
     !:Info = !.Info ^ tc_info_type_assign_set := TypeAssignSet.
 
 :- pred reduce_type_assign_context(class_table::in, instance_table::in,
-    type_assign::in, type_assign::out) is semidet.
+    type_assign::in, list(type_assign)::in, list(type_assign)::out,
+    list(type_assign)::in, list(type_assign)::out) is det.
 
-reduce_type_assign_context(ClassTable, InstanceTable, !TypeAssign) :-
+reduce_type_assign_context(ClassTable, InstanceTable, !.TypeAssign,
+        !TypeAssignSet, !UnsatTypeAssignSet) :-
     type_assign_get_head_type_params(!.TypeAssign, HeadTypeParams),
     type_assign_get_type_bindings(!.TypeAssign, Bindings0),
     type_assign_get_typeclass_constraints(!.TypeAssign, Constraints0),
@@ -154,13 +155,20 @@ reduce_type_assign_context(ClassTable, InstanceTable, !TypeAssign) :-
         HeadTypeParams, Bindings0, Bindings, TVarSet0, TVarSet,
         Proofs0, Proofs, ConstraintMap0, ConstraintMap,
         Constraints0, Constraints),
-    check_satisfiability(Constraints ^ unproven, HeadTypeParams),
 
     type_assign_set_type_bindings(Bindings, !TypeAssign),
     type_assign_set_typeclass_constraints(Constraints, !TypeAssign),
     type_assign_set_typevarset(TVarSet, !TypeAssign),
     type_assign_set_constraint_proofs(Proofs, !TypeAssign),
-    type_assign_set_constraint_map(ConstraintMap, !TypeAssign).
+    type_assign_set_constraint_map(ConstraintMap, !TypeAssign),
+
+    ( check_satisfiability(Constraints ^ unproven, HeadTypeParams) ->
+        !:TypeAssignSet = !.TypeAssignSet ++ [!.TypeAssign]
+    ;
+        % Remember the unsatisfiable type_assign_set so we can produce more
+        % specific error messages.
+        list.cons(!.TypeAssign, !UnsatTypeAssignSet)
+    ).
 
 reduce_context_by_rule_application(ClassTable, InstanceTable, HeadTypeParams,
         !Bindings, !TVarSet, !Proofs, !ConstraintMap, !Constraints) :-
diff --git a/tests/invalid/Mmakefile b/tests/invalid/Mmakefile
index 15f2291..1ccaaa7 100644
--- a/tests/invalid/Mmakefile
+++ b/tests/invalid/Mmakefile
@@ -241,6 +241,7 @@ SINGLEMODULE= \
 	uniq_neg \
 	unsatisfiable_constraint \
 	unsatisfiable_constraint_bug \
+	unsatisfiable_constraint_msg \
 	unsatisfiable_super \
 	user_eq_dummy \
 	uu_type \
diff --git a/tests/invalid/typeclass_test_8.err_exp b/tests/invalid/typeclass_test_8.err_exp
index e4aa1af..d610001 100644
--- a/tests/invalid/typeclass_test_8.err_exp
+++ b/tests/invalid/typeclass_test_8.err_exp
@@ -1,7 +1,4 @@
 typeclass_test_8.m:004: In predicate `main'/2:
-typeclass_test_8.m:004:   type error: unsatisfied typeclass constraint:
-typeclass_test_8.m:004:     `typeclass_test_8.fooable(T)'
-typeclass_test_8.m:004: In predicate `main'/2:
 typeclass_test_8.m:004:   warning: unresolved polymorphism.
 typeclass_test_8.m:004:   The variable with an unbound type was:
 typeclass_test_8.m:004:     X: T
@@ -13,3 +10,9 @@ typeclass_test_8.m:004:   version should be called, because the type variables
 typeclass_test_8.m:004:   listed above didn't get bound. (I ought to tell you
 typeclass_test_8.m:004:   which call caused the problem, but I'm afraid you'll
 typeclass_test_8.m:004:   have to work it out yourself. My apologies.)
+typeclass_test_8.m:004: In predicate `main'/2:
+typeclass_test_8.m:004:   type error: unsatisfied typeclass constraint:
+typeclass_test_8.m:004:     `typeclass_test_8.fooable(T)'
+typeclass_test_8.m:004:   The constraint is due to:
+typeclass_test_8.m:013:     a goal here, and
+typeclass_test_8.m:014:     a goal here.
diff --git a/tests/invalid/unsatisfiable_constraint.err_exp b/tests/invalid/unsatisfiable_constraint.err_exp
index 3083a7e..b752353 100644
--- a/tests/invalid/unsatisfiable_constraint.err_exp
+++ b/tests/invalid/unsatisfiable_constraint.err_exp
@@ -1,9 +1,4 @@
 unsatisfiable_constraint.m:038: In predicate `test'/1:
-unsatisfiable_constraint.m:038:   type error: unsatisfied typeclass constraints:
-unsatisfiable_constraint.m:038:     `unsatisfiable_constraint.a(A, B, A, V_8)',
-unsatisfiable_constraint.m:038:     `unsatisfiable_constraint.a(A, B, C, V_14)',
-unsatisfiable_constraint.m:038:     `unsatisfiable_constraint.b(A, C)'
-unsatisfiable_constraint.m:038: In predicate `test'/1:
 unsatisfiable_constraint.m:038:   warning: unresolved polymorphism.
 unsatisfiable_constraint.m:038:   The variables with unbound types were:
 unsatisfiable_constraint.m:038:     C: C
@@ -17,3 +12,12 @@ unsatisfiable_constraint.m:038:   type variables listed above didn't get bound.
 unsatisfiable_constraint.m:038:   (I ought to tell you which call caused the
 unsatisfiable_constraint.m:038:   problem, but I'm afraid you'll have to work
 unsatisfiable_constraint.m:038:   it out yourself. My apologies.)
+unsatisfiable_constraint.m:038: In predicate `test'/1:
+unsatisfiable_constraint.m:038:   type error: unsatisfied typeclass constraints:
+unsatisfiable_constraint.m:038:     `unsatisfiable_constraint.a(A, B, A, V_8)',
+unsatisfiable_constraint.m:038:     `unsatisfiable_constraint.a(A, B, C, V_14)',
+unsatisfiable_constraint.m:038:     `unsatisfiable_constraint.b(A, C)'
+unsatisfiable_constraint.m:038:   The constraints are due to:
+unsatisfiable_constraint.m:042:     a goal here,
+unsatisfiable_constraint.m:043:     a goal here, and
+unsatisfiable_constraint.m:044:     a goal here.
diff --git a/tests/invalid/unsatisfiable_constraint_msg.err_exp b/tests/invalid/unsatisfiable_constraint_msg.err_exp
new file mode 100644
index 0000000..a77d83d
--- /dev/null
+++ b/tests/invalid/unsatisfiable_constraint_msg.err_exp
@@ -0,0 +1,5 @@
+unsatisfiable_constraint_msg.m:016: In clause for predicate `main'/2:
+unsatisfiable_constraint_msg.m:016:   unsatisfiable typeclass constraints:
+unsatisfiable_constraint_msg.m:016:   `unsatisfiable_constraint_msg.tcb(unsatisfiable_constraint_msg.tb(string))'
+unsatisfiable_constraint_msg.m:016:   and
+unsatisfiable_constraint_msg.m:016:   `unsatisfiable_constraint_msg.tcc(string)'.
diff --git a/tests/invalid/unsatisfiable_constraint_msg.m b/tests/invalid/unsatisfiable_constraint_msg.m
new file mode 100644
index 0000000..35f4378
--- /dev/null
+++ b/tests/invalid/unsatisfiable_constraint_msg.m
@@ -0,0 +1,97 @@
+:- module unsatisfiable_constraint_msg.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module string.
+:- import_module int.
+
+main(!IO) :-
+    io.write_string("typeclass_test", !IO),
+    ( test(ta("a"), tb("b")) ->
+        io.write_string("true", !IO)
+    ;
+        io.write_string("fail", !IO)
+    ).
+
+
+:- pred test(A::in, B::in) is semidet <= (tca(A), tcb(B)).
+
+test(A, B) :-
+    pa(A),
+    pb(B).
+
+
+
+:- typeclass tca(A) where
+[
+    pred pa(A::in) is semidet
+].
+
+:- typeclass tcb(B) where
+[
+    pred pb(B::in) is semidet
+].
+
+:- typeclass tcc(C) where
+[
+    pred pc(C::in) is semidet
+].
+
+:- type ta(A) ---> ta(A).
+:- type tb(B) ---> tb(B).
+
+
+:- instance tca(ta(A)) <= (tca(A), tcc(A))
+where
+[
+    (pa(ta(A)) :-
+        pa(A),
+        pc(A)
+    )
+].
+
+/*
+% missing typeclass instance
+:- instance tcb(tb(B)) <= tcb(B)
+where
+[
+    (pb(tb(A)) :-
+        pb(A)
+    )
+].
+*/
+
+
+:- instance tca(string)
+where
+[
+    (pa(String) :-
+        length(String) > 0
+    )
+].
+
+:- instance tcb(string)
+where
+[
+    (pb(String) :-
+        length(String) > 0
+    )
+].
+
+/*
+% missing typeclass instance
+:- instance c(string)
+where
+[
+    (c(String) :-
+        length(String) > 0
+    )
+].
+*/
+:- end_module unsatisfiable_constraint_msg.

--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------