[m-rev.] for post-commit review: add workarounds for bugs #184 and #214
Julien Fischer
jfischer at opturion.com
Wed Jun 29 16:23:31 AEST 2016
For post-commit review by Mark or Zoltan.
The diff below addresses the symptoms rather than the cause, which I suspect is
either a bug in the type checker or the type checker not keeping track of
enough information to produce an error message in the first place. I am
committing this now since, for bug #184 at least, it is an improvement over the
status quo. The request for a review concerns the XXXs below, in particular,
do you now of there are some invariants on the structure of constraint_maps
that are not documented?
-----------------------------------------------
Add workarounds for bugs #184 and #214.
Bug #184 is a compiler abort due to the code that generates an error message
for an unsatisfied type class constraint. That code is either making an
incorrect assumption about the constraint_map type or the there is a bug in the
type checker. Bug #214 is also concerned with the error message for
unsatisfied type class constraints: in that case we attempt to list which goals
that are causing the unsatisfied constraints, but that list of goals is empty
and we end up with an incomplete looking error message. (This is related to
bug #184 as once the the workaround for the abort is in place, the same thing
occurs there.)
compiler/post_typecheck.m:
Do not assume that all unproven constraints will appears as values
in the constraint map: that isn't true for the program in bug #184.
If the list of goals that are causing unsatisfied type class constraints
is empty, then omit the prefix "The unsatisfied constraints are
due to:" from the error message.
tests/invalid/Mmakefile:
tests/invalid/Mercury.options.m:
tests/invalid/bug184.{m,err_exp}:
tests/invalid/bug214.{m,err_exp}:
Add the test cases for the above bugs.
Julien.
diff --git a/compiler/post_typecheck.m b/compiler/post_typecheck.m
index 4b88d31..c4b3f30 100644
--- a/compiler/post_typecheck.m
+++ b/compiler/post_typecheck.m
@@ -215,17 +215,26 @@ report_unsatisfied_constraints(ModuleInfo, PredId, PredInfo, Constraints,
[nl_indent_delta(-1)],
Msg = simple_msg(Context, [always(Pieces)]),
- 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([words(DueTo)])]),
ConstrainedGoals = find_constrained_goals(PredInfo, Constraints),
- ContextMsgs = constrained_goals_to_error_msgs(ModuleInfo,
- ConstrainedGoals),
-
- Spec = error_spec(severity_error, phase_type_check,
- [Msg, ContextMsgStart | ContextMsgs]),
+ (
+ % XXX this happens for bugs #184 and #214. Should it?
+ % If we performed this check after checking for unresolved polymorphism
+ % we could at least report the problem is due to unbound type variables
+ % occurring in Constraints.
+ ConstrainedGoals = [],
+ ContextMsgs = []
+ ;
+ ConstrainedGoals = [_ | _],
+ DueTo = choose_number(Constraints,
+ "The constraint is due to:",
+ "The constraints are due to:"),
+ ContextMsgsPrefix = error_msg(yes(Context), do_not_treat_as_first, 0,
+ [always([words(DueTo)])]),
+ ContextMsgsList = constrained_goals_to_error_msgs(ModuleInfo,
+ ConstrainedGoals),
+ ContextMsgs = [ContextMsgsPrefix | ContextMsgsList]
+ ),
+ Spec = error_spec(severity_error, phase_type_check, [Msg | ContextMsgs]),
!:Specs = [Spec | !.Specs].
:- func constraint_to_error_piece(tvarset, prog_constraint)
@@ -249,7 +258,16 @@ find_constrained_goals(PredInfo, Constraints) = Goals :-
pred_info_get_constraint_map(PredInfo, ConstraintMap),
ReverseConstraintMap = map.reverse_map(ConstraintMap),
- map.apply_to_list(Constraints, ReverseConstraintMap, ConstraintIdSets),
+
+ % XXX Workaround for bug #184 -- we used to use the commented out line
+ % below, but for some programs Constraints has elements that are *not* in
+ % the key set of ReverseConstraintMap. Either the assumption that every
+ % element of Constraints is a value of ConstraintMap is wrong, or the there
+ % is a bug somewhere in the type checker.
+ %
+ % map.apply_to_list(Constraints, ReverseConstraintMap, ConstraintIdSets),
+ list.foldl(gather_constraint_ids(ReverseConstraintMap), Constraints,
+ [], ConstraintIdSets),
ConstraintIds = set.union_list(ConstraintIdSets),
% This could be more efficient.
@@ -267,6 +285,15 @@ find_constrained_goals(PredInfo, Constraints) = Goals :-
A),
solutions(FindGoals, Goals).
+:- pred gather_constraint_ids(map(prog_constraint, set(constraint_id))::in,
+ prog_constraint::in, list(set(constraint_id))::in, list(set(constraint_id))::out) is det.
+
+gather_constraint_ids(ReverseConstraintMap, Constraint, !ConstraintIdSets) :-
+ ( if map.search(ReverseConstraintMap, Constraint, ConstraintIdSet)
+ then !:ConstraintIdSets = [ConstraintIdSet | !.ConstraintIdSets]
+ else true
+ ).
+
:- func constrained_goals_to_error_msgs(module_info, list(hlds_goal))
= list(error_msg).
diff --git a/tests/invalid/Mercury.options b/tests/invalid/Mercury.options
index dfb0b5c..5b83bb9 100644
--- a/tests/invalid/Mercury.options
+++ b/tests/invalid/Mercury.options
@@ -15,6 +15,7 @@ MCFLAGS-assert_in_interface = --no-intermodule-optimization \
MCFLAGS-actual_expected = --no-intermodule-optimization
MCFLAGS-any_to_ground_in_ite_cond_nomax = --no-max-error-line-width
+MCFLAGS-bug214 = --allow-stubs --no-warn-stubs
# Mantis bug 238 shows up in bug238.m only with --constraint-propagation.
MCFLAGS-bug238 = --constraint-propagation
MCFLAGS-children = --no-intermodule-optimization
diff --git a/tests/invalid/Mmakefile b/tests/invalid/Mmakefile
index f802d20..a8c0657 100644
--- a/tests/invalid/Mmakefile
+++ b/tests/invalid/Mmakefile
@@ -76,8 +76,10 @@ SINGLEMODULE= \
bug117 \
bug150 \
bug17 \
+ bug184 \
bug191 \
bug197 \
+ bug214 \
bug238 \
bug257 \
bug278 \
diff --git a/tests/invalid/bug184.err_exp b/tests/invalid/bug184.err_exp
new file mode 100644
index 0000000..89b7755
--- /dev/null
+++ b/tests/invalid/bug184.err_exp
@@ -0,0 +1,10 @@
+bug184.m:019: In function `test'/0:
+bug184.m:019: type error: unsatisfied typeclass constraint:
+bug184.m:019: `bug184.myclass(T)'
+bug184.m:019: In function `test'/0:
+bug184.m:019: warning: unresolved polymorphism.
+bug184.m:019: The variable with an unbound type was:
+bug184.m:019: V_2: list.list(T)
+bug184.m:019: The unbound type variable will be implicitly bound to the
+bug184.m:019: builtin type `void'.
+For more information, recompile with `-E'.
diff --git a/tests/invalid/bug184.m b/tests/invalid/bug184.m
new file mode 100644
index 0000000..e39e797
--- /dev/null
+++ b/tests/invalid/bug184.m
@@ -0,0 +1,34 @@
+%---------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
+%---------------------------------------------------------------------------%
+% Regression test for bug #184.
+% This program caused the compiler to abort with:
+%
+% Uncaught Mercury exception:
+% Software Error: map.lookup: key not found
+% Key Type: parse_tree.prog_data.prog_constraint
+% Key Value: constraint(qualified(unqualified("bug184"), "myclass"),
+% [type_variable(var(1), kind_star)])
+% Value Type: set_ordlist.set_ordlist(hlds.hlds_data.constraint_id)
+%
+%---------------------------------------------------------------------------%
+
+:- module bug184.
+:- interface.
+
+:- func test = int.
+
+:- implementation.
+
+:- import_module list.
+
+test = f([]).
+
+:- typeclass myclass(T) where [
+ func f(T) = int
+].
+
+:- instance myclass(list(T)) <= myclass(T) where [
+ f(_) = 4
+].
+
diff --git a/tests/invalid/bug214.err_exp b/tests/invalid/bug214.err_exp
new file mode 100644
index 0000000..48df666
--- /dev/null
+++ b/tests/invalid/bug214.err_exp
@@ -0,0 +1,3 @@
+bug214.m:043: In predicate `solve_mip_cg'/2:
+bug214.m:043: type error: unsatisfied typeclass constraint:
+bug214.m:043: `bug214.linear_expr(int, V_15, int)'
diff --git a/tests/invalid/bug214.m b/tests/invalid/bug214.m
new file mode 100644
index 0000000..c996952
--- /dev/null
+++ b/tests/invalid/bug214.m
@@ -0,0 +1,151 @@
+%---------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
+%---------------------------------------------------------------------------%
+% Regression test for bug #214.
+% The error message produced for this program is:
+%
+% bug.m:026: In predicate `solve_mip_cg'/2:
+% bug.m:026: type error: unsatisfied typeclass constraint:
+% bug.m:026: `bug.linear_expr(int, V_15, int)'
+% bug.m:026: The constraint is due to:
+%
+% But no constraints are listed.
+% The actual problem here is that the type of the 4th argument of the
+% closure mip_search is incorrect.
+% (XXX as of rotd-2016-06-29, the compiler doesn't print the last
+% line of the error message -- ideally it would produce something that
+% would allow the user to localise the cause of the unsatisfied constraint.)
+%
+% Compile with: mmc --allow-stubs --no-warn-stubs --make bug
+
+:- module bug214.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module array.
+:- import_module array2d.
+:- import_module float.
+:- import_module int.
+:- import_module list.
+
+%-----------------------------------------------------------------------------%
+
+main(!IO).
+
+:- pred solve_mip_cg(ss::mdi, ss::muo) is semidet.
+
+solve_mip_cg(!SS) :-
+ invoke(create_colgen_dw_solver, {CgSolver, _K, OrigVars}, !SS),
+
+ % The next two lines are incorrect.
+ OrigVarsL = condense(lists(OrigVars)),
+ list.map((func(E) = v(E)), OrigVarsL) = OrigVarsV,
+
+ % They should actually be replaced by ...
+ % OrigVarsV = condense(lists(OrigVars)),
+
+ new_assertion_ref(0, NodeCounter, !SS),
+ Search = mip_search(CgSolver, most_frac, std_split, OrigVarsV, NodeCounter),
+ Check = mip_check_cutoff(CgSolver, integer_granularity),
+ branch_and_bound(Search, Check, _Optimal, !SS).
+
+:- pred create_colgen_dw_solver
+ : propagate({colgen_dw_solver, int, array2d(int)})
+ `with_inst` propagate_semidet.
+
+%-----------------------------------------------------------------------------%
+
+:- type ss ---> ss.
+
+:- type solve(T) == pred(T, ss, ss).
+:- inst solve_det == (pred(out, mdi, muo) is det).
+:- inst solve_semidet == (pred(out, mdi, muo) is semidet).
+:- inst solve_nondet == (pred(out, mdi, muo) is nondet).
+
+:- type solve0 == pred(ss, ss).
+:- inst solve0_nondet == (pred(mdi, muo) is nondet).
+
+:- type ps ---> ps.
+
+:- type propagate(T) == pred(T, ps, ps).
+:- inst propagate_det == (pred(out, di, uo) is det).
+:- inst propagate_semidet == (pred(out, di, uo) is semidet).
+
+:- type propagate0 == pred(ps, ps).
+:- inst propagate0_det == (pred(di, uo) is det).
+:- inst propagate0_semidet == (pred(di, uo) is semidet).
+
+%-----------------------------------------------------------------------------%
+
+:- pred invoke(propagate(T)) : solve(T).
+:- mode invoke(in(propagate_det)) `with_inst` solve_semidet.
+:- mode invoke(in(propagate_semidet)) `with_inst` solve_semidet.
+
+%-----------------------------------------------------------------------------%
+
+:- type assertion_ref(T) ---> assertion_ref(T).
+
+:- pred new_assertion_ref(T::in, assertion_ref(T)::out, ss::mdi, ss::uo) is det.
+
+:- typeclass linear_expr(Expr, Coeff, Var) <= ((Expr -> Var), (Expr -> Coeff))
+where [
+ func v(Var) = Expr
+].
+
+:- typeclass lp_solver(S) where [].
+
+:- type colgen_dw_solver ---> colgen_dw_solver.
+
+:- instance lp_solver(colgen_dw_solver) where [].
+
+:- type col_num == int.
+
+%-----------------------------------------------------------------------------%
+
+:- pred branch_and_bound(bb_search(T)::in(bb_search),
+ bb_check(T)::in(bb_check), T::out, ss::mdi, ss::muo) is semidet.
+
+:- type bb_search(T) == solve(T).
+:- inst bb_search == solve_nondet.
+
+:- type bb_check(T) == (pred(T, ps, ps)).
+:- inst bb_check == (pred(in, di, uo) is semidet).
+
+:- func integer_granularity = float.
+
+:- type lp_nodes_ref == assertion_ref(int).
+
+:- type lp_split(S) == (pred(lp_nodes_ref, S, col_num, ss, ss)).
+:- inst lp_split == (pred(in, in, in, mdi, muo) is nondet).
+
+:- type lp_choose_var(S) == (pred(S, list(col_num), col_num, ss, ss)).
+:- inst lp_choose_var == (pred(in, in, out, mdi, muo) is semidet).
+
+:- type ip_solution
+ ---> ip_solution(
+ ip_objective :: float,
+ ip_var_values :: list(float)
+ ).
+
+:- pred mip_search(S::in, lp_choose_var(S)::in(lp_choose_var),
+ lp_split(S)::in(lp_split), list(col_num)::in, assertion_ref(int)::in)
+ : bb_search(ip_solution) `with_inst` bb_search <= lp_solver(S).
+
+:- pred mip_check_cutoff(S::in, float::in, ip_solution::in)
+ : propagate0 `with_inst` propagate0_semidet <= lp_solver(S).
+
+:- pred std_split(assertion_ref(int)::in, S::in, col_num::in)
+ : solve0 `with_inst` solve0_nondet <= lp_solver(S).
+
+:- pred most_frac(S::in, list(col_num)::in)
+ : solve(col_num) `with_inst` solve_semidet <= lp_solver(S).
+
+%-----------------------------------------------------------------------------%
More information about the reviews
mailing list