2024-12-14 09:18 AEDT

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000191mercuryBugpublic2015-11-02 11:10
Reportercolanderman 
Assigned Tojuliensf 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
Product Version 
Target VersionFixed in Version 
Summary0000191: indirect instance implementations ignore special insts
DescriptionIf a typeclass requires a predicate of a specific inst, but an instance indirectly defines that predicate (using "is"), the inst is not properly checked and an implementation with a more general inst (e.g. in or out) can be used. Result is a software error during compile, below.
Additional InformationSoftware Error: code_gen.m: Unexpected: semidet model in det context
TagsNo tags attached.
Attached Files
  • ? file icon instbug.m (507 bytes) 2011-03-22 13:52
  • patch file icon inst_match.patch (526 bytes) 2011-04-05 12:21 -
    --- compiler/inst_match.m~	2011-04-04 22:03:49.489592747 -0400
    +++ compiler/inst_match.m	2011-04-04 22:03:49.489592747 -0400
    @@ -1048,7 +1048,7 @@
             % We can only do this check if the type is known.
             bound_inst_list_is_complete_for_type(set.init, ModuleInfo, ListB, Type)
         ;
    -        true
    +        MaybeType = no
             % XXX enabling the check for bound_inst_list_is_complete
             % for type makes the mode checker too conservative in
             % the absence of alias tracking, so we currently always
    
    patch file icon inst_match.patch (526 bytes) 2011-04-05 12:21 +
  • patch file icon inst_match2.patch (14,424 bytes) 2011-04-07 13:37 -
    --- compiler/inst_match.m~	2011-04-04 22:03:49.489592747 -0400
    +++ compiler/inst_match.m	2011-04-04 22:03:49.489592747 -0400
    @@ -1048,7 +1048,7 @@
             % We can only do this check if the type is known.
             bound_inst_list_is_complete_for_type(set.init, ModuleInfo, ListB, Type)
         ;
    -        true
    +        MaybeType = no
             % XXX enabling the check for bound_inst_list_is_complete
             % for type makes the mode checker too conservative in
             % the absence of alias tracking, so we currently always
    --- library/builtin.m~	2011-04-06 21:55:19.844856577 -0400
    +++ library/builtin.m	2011-04-06 22:16:34.098488142 -0400
    @@ -388,7 +388,7 @@
         %
     :- pred cc_multi_equal(T, T).
     :- mode cc_multi_equal(di, uo) is cc_multi.
    -:- mode cc_multi_equal(in, out) is cc_multi.
    +:- mode cc_multi_equal(in(I =< ground), out(I =< ground)) is cc_multi.
     
         % `impure_true' is like `true' except that it is impure.
         %
    @@ -1184,7 +1184,7 @@
     % Any changes here may need to be reflected there.
     
     :- pragma foreign_proc("C",
    -    cc_multi_equal(X::in, Y::out),
    +    cc_multi_equal(X::in(I =< ground), Y::out(I =< ground)),
         [will_not_call_mercury, thread_safe, promise_pure,
             does_not_affect_liveness],
     "
    @@ -1199,7 +1199,7 @@
     ").
     
     :- pragma foreign_proc("C#",
    -    cc_multi_equal(X::in, Y::out),
    +    cc_multi_equal(X::in(I =< ground), Y::out(I =< ground)),
         [will_not_call_mercury, thread_safe, promise_pure],
     "
         Y = X;
    @@ -1212,7 +1212,7 @@
     ").
     
     :- pragma foreign_proc("Java",
    -    cc_multi_equal(X::in, Y::out),
    +    cc_multi_equal(X::in(I =< ground), Y::out(I =< ground)),
         [will_not_call_mercury, thread_safe, promise_pure],
     "
         Y = X;
    @@ -1225,7 +1225,7 @@
     ").
     
     :- pragma foreign_proc("Erlang",
    -    cc_multi_equal(X::in, Y::out),
    +    cc_multi_equal(X::in(I =< ground), Y::out(I =< ground)),
         [will_not_call_mercury, thread_safe, promise_pure],
     "
         Y = X
    --- library/exception.m~	2011-04-06 22:07:33.804376595 -0400
    +++ library/exception.m	2011-04-06 23:16:13.911887652 -0400
    @@ -350,34 +350,39 @@
     :- pragma no_inline(get_determinism/2).
     :- pragma promise_equivalent_clauses(get_determinism/2).
     
    +% Trick Mercury into using the correct mode.
    +% The real fix is to make check_hlds.modecheck_call.choose_best_match nondet.
    +:- pred ccme(A::in(I =< ground), A::out(I =< ground)) is cc_multi.
    +ccme(A, B) :- cc_multi_equal(A, B).
    +
     get_determinism(_Pred::(pred(out) is det),
             Det::out(bound(exp_detism_det))) :-
    -    ( cc_multi_equal(exp_detism_det, Det)
    +    ( ccme(exp_detism_det, Det)
         ; throw(software_error("get_determinism"))
         ).
     get_determinism(_Pred::(pred(out) is semidet),
             Det::out(bound(exp_detism_semidet))) :-
    -    ( cc_multi_equal(exp_detism_semidet, Det)
    +    ( ccme(exp_detism_semidet, Det)
         ; throw(software_error("get_determinism"))
         ).
     get_determinism(_Pred::(pred(out) is cc_multi),
             Det::out(bound(exp_detism_cc_multi))) :-
    -    ( cc_multi_equal(exp_detism_cc_multi, Det)
    +    ( ccme(exp_detism_cc_multi, Det)
         ; throw(software_error("get_determinism"))
         ).
     get_determinism(_Pred::(pred(out) is cc_nondet),
             Det::out(bound(exp_detism_cc_nondet))) :-
    -    ( cc_multi_equal(exp_detism_cc_nondet, Det)
    +    ( ccme(exp_detism_cc_nondet, Det)
         ; throw(software_error("get_determinism"))
         ).
     get_determinism(_Pred::(pred(out) is multi),
             Det::out(bound(exp_detism_multi))) :-
    -    ( cc_multi_equal(exp_detism_multi, Det)
    +    ( ccme(exp_detism_multi, Det)
         ; throw(software_error("get_determinism"))
         ).
     get_determinism(_Pred::(pred(out) is nondet),
             Det::out(bound(exp_detism_nondet))) :-
    -    ( cc_multi_equal(exp_detism_nondet, Det)
    +    ( ccme(exp_detism_nondet, Det)
         ; throw(software_error("get_determinism"))
         ).
     
    @@ -386,12 +391,12 @@
     
     get_determinism_2(_Pred::pred(out, di, uo) is det,
             Det::out(bound(exp_detism_det))) :-
    -    ( cc_multi_equal(exp_detism_det, Det)
    +    ( ccme(exp_detism_det, Det)
         ; throw(software_error("get_determinism_2"))
         ).
     get_determinism_2(_Pred::pred(out, di, uo) is cc_multi,
             Det::out(bound(exp_detism_cc_multi))) :-
    -    ( cc_multi_equal(exp_detism_cc_multi, Det)
    +    ( ccme(exp_detism_cc_multi, Det)
         ; throw(software_error("get_determinism_2"))
         ).
     
    @@ -492,14 +497,23 @@
     wrap_success(Goal, succeeded(R)) :- Goal(R).
     
     :- pred wrap_success_or_failure(pred(T), exception_result(T)) is det.
    -:- mode wrap_success_or_failure(pred(out) is det, out) is det.
    +:- mode wrap_success_or_failure(pred(out) is det, out(cannot_fail)) is det.
     :- mode wrap_success_or_failure(pred(out) is semidet, out) is det.
     %:- mode wrap_success_or_failure(pred(out) is multi, out) is multi. (unused)
     %:- mode wrap_success_or_failure(pred(out) is nondet, out) is multi. (unused)
    -:- mode wrap_success_or_failure(pred(out) is cc_multi, out) is cc_multi.
    +:- mode wrap_success_or_failure(pred(out) is cc_multi, out(cannot_fail)) is cc_multi.
     :- mode wrap_success_or_failure(pred(out) is cc_nondet, out) is cc_multi.
    +:- pragma promise_equivalent_clauses(wrap_success_or_failure/2).
     
    -wrap_success_or_failure(Goal, Result) :-
    +% We need multiple clauses because Mercury seems to decide the
    +% inst of Result before pruning the else branch.
    +wrap_success_or_failure(Goal::pred(out) is det, Result::out(cannot_fail)) :-
    +    Goal(R), Result = succeeded(R).
    +wrap_success_or_failure(Goal::pred(out) is semidet, Result::out) :-
    +    (if Goal(R) then Result = succeeded(R) else Result = failed).
    +wrap_success_or_failure(Goal::pred(out) is cc_multi, Result::out(cannot_fail)) :-
    +    Goal(R), Result = succeeded(R).
    +wrap_success_or_failure(Goal::pred(out) is cc_nondet, Result::out) :-
         (if Goal(R) then Result = succeeded(R) else Result = failed).
     
     /*********************
    @@ -518,19 +532,19 @@
         try_det(Detism, Goal, Result).
     
     try_det(exp_detism_det, Goal, Result) :-
    -    WrappedGoal = (pred(R::out) is det :-
    +    WrappedGoal = (pred(R::out(cannot_fail)) is det :-
             wrap_success_or_failure(Goal, R)
         ),
         catch_impl(WrappedGoal, wrap_exception, Result0),
    -    cc_multi_equal(Result0, Result).
    +    ccme(Result0, Result).
     try_det(exp_detism_semidet, Goal, Result) :-
         WrappedGoal = (pred(R::out) is det :-
             wrap_success_or_failure(Goal, R)
         ),
         catch_impl(WrappedGoal, wrap_exception, Result0),
    -    cc_multi_equal(Result0, Result).
    +    ccme(Result0, Result).
     try_det(exp_detism_cc_multi, Goal, Result) :-
    -    WrappedGoal = (pred(R::out) is cc_multi :-
    +    WrappedGoal = (pred(R::out(cannot_fail)) is cc_multi :-
             wrap_success_or_failure(Goal, R)
         ),
         catch_impl(WrappedGoal, wrap_exception, Result).
    @@ -832,12 +846,18 @@
     :- pragma promise_pure(catch_impl/3).
     :- /* impure */
        pred catch_impl(pred(T), handler(T), T).
    -:- mode catch_impl(pred(out) is det,       in(handler), out) is det.
    -:- mode catch_impl(pred(out) is semidet,   in(handler), out) is semidet.
    -:- mode catch_impl(pred(out) is cc_multi,  in(handler), out) is cc_multi.
    -:- mode catch_impl(pred(out) is cc_nondet, in(handler), out) is cc_nondet.
    -:- mode catch_impl(pred(out) is multi,     in(handler), out) is multi.
    -:- mode catch_impl(pred(out) is nondet,    in(handler), out) is nondet.
    +:- mode catch_impl(pred(out(I =< ground)) is det,       in(handler),
    +    out(I =< ground)) is det.
    +:- mode catch_impl(pred(out(I =< ground)) is semidet,   in(handler),
    +    out(I =< ground)) is semidet.
    +:- mode catch_impl(pred(out(I =< ground)) is cc_multi,  in(handler),
    +    out(I =< ground)) is cc_multi.
    +:- mode catch_impl(pred(out(I =< ground)) is cc_nondet, in(handler),
    +    out(I =< ground)) is cc_nondet.
    +:- mode catch_impl(pred(out(I =< ground)) is multi,     in(handler),
    +    out(I =< ground)) is multi.
    +:- mode catch_impl(pred(out(I =< ground)) is nondet,    in(handler),
    +    out(I =< ground)) is nondet.
     
     %
     % By default we call the external implementation, but specific backends
    @@ -852,17 +872,23 @@
     throw_impl(Univ::in) :-
         builtin_throw(Univ).
     
    -catch_impl(Pred::(pred(out) is det), Handler::in(handler), T::out) :-
    +catch_impl(Pred::(pred(out(I =< ground)) is det), Handler::in(handler),
    +           T::out(I =< ground)) :-
         builtin_catch(Pred, Handler, T).
    -catch_impl(Pred::(pred(out) is semidet), Handler::in(handler), T::out) :-
    +catch_impl(Pred::(pred(out(I =< ground)) is semidet), Handler::in(handler),
    +           T::out(I =< ground)) :-
         builtin_catch(Pred, Handler, T).
    -catch_impl(Pred::(pred(out) is cc_multi), Handler::in(handler), T::out) :-
    +catch_impl(Pred::(pred(out(I =< ground)) is cc_multi), Handler::in(handler),
    +           T::out(I =< ground)) :-
         builtin_catch(Pred, Handler, T).
    -catch_impl(Pred::(pred(out) is cc_nondet), Handler::in(handler), T::out) :-
    +catch_impl(Pred::(pred(out(I =< ground)) is cc_nondet), Handler::in(handler),
    +           T::out(I =< ground)) :-
         builtin_catch(Pred, Handler, T).
    -catch_impl(Pred::(pred(out) is multi), Handler::in(handler), T::out) :-
    +catch_impl(Pred::(pred(out(I =< ground)) is multi), Handler::in(handler),
    +           T::out(I =< ground)) :-
         builtin_catch(Pred, Handler, T).
    -catch_impl(Pred::(pred(out) is nondet), Handler::in(handler), T::out) :-
    +catch_impl(Pred::(pred(out(I =< ground)) is nondet), Handler::in(handler),
    +           T::out(I =< ground)) :-
         builtin_catch(Pred, Handler, T).
     
     % builtin_throw and builtin_catch are implemented below using
    @@ -873,12 +899,18 @@
     
     :- /* impure */
        pred builtin_catch(pred(T), handler(T), T).
    -:- mode builtin_catch(pred(out) is det, in(handler), out) is det.
    -:- mode builtin_catch(pred(out) is semidet, in(handler), out) is semidet.
    -:- mode builtin_catch(pred(out) is cc_multi, in(handler), out) is cc_multi.
    -:- mode builtin_catch(pred(out) is cc_nondet, in(handler), out) is cc_nondet.
    -:- mode builtin_catch(pred(out) is multi, in(handler), out) is multi.
    -:- mode builtin_catch(pred(out) is nondet, in(handler), out) is nondet.
    +:- mode builtin_catch(pred(out(I =< ground)) is det, in(handler),
    +    out(I =< ground)) is det.
    +:- mode builtin_catch(pred(out(I =< ground)) is semidet, in(handler),
    +    out(I =< ground)) is semidet.
    +:- mode builtin_catch(pred(out(I =< ground)) is cc_multi, in(handler),
    +    out(I =< ground)) is cc_multi.
    +:- mode builtin_catch(pred(out(I =< ground)) is cc_nondet, in(handler),
    +    out(I =< ground)) is cc_nondet.
    +:- mode builtin_catch(pred(out(I =< ground)) is multi, in(handler),
    +    out(I =< ground)) is multi.
    +:- mode builtin_catch(pred(out(I =< ground)) is nondet, in(handler),
    +    out(I =< ground)) is nondet.
     
     %
     % IMPORTANT: any changes or additions to external predicates should be
    --- library/list.m~	2011-04-06 22:38:34.127522212 -0400
    +++ library/list.m	2011-04-06 22:40:37.672093399 -0400
    @@ -126,8 +126,10 @@
         % and eliminating any duplicates. L1 and L2 must be sorted and must each
         % not contain any duplicates.
         %
    -:- pred list.merge_and_remove_dups(list(T)::in, list(T)::in, list(T)::out)
    -    is det.
    +:- pred list.merge_and_remove_dups(list(T), list(T), list(T)) is det.
    +:- mode list.merge_and_remove_dups(in, in, out) is det.
    +:- mode list.merge_and_remove_dups(in(non_empty_list), in, out(non_empty_list)) is det.
    +:- mode list.merge_and_remove_dups(in, in(non_empty_list), out(non_empty_list)) is det.
     :- func list.merge_and_remove_dups(list(T), list(T)) = list(T).
     
         % list.remove_adjacent_dups(L0, L):
    @@ -343,7 +345,10 @@
         % List is List0 sorted with the second and subsequent occurrence of
         % any duplicates removed.
         %
    -:- pred list.sort_and_remove_dups(list(T)::in, list(T)::out) is det.
    +:- pred list.sort_and_remove_dups(list(T), list(T)) is det.
    +:- mode list.sort_and_remove_dups(in, out) is det.
    +:- mode list.sort_and_remove_dups(in(non_empty_list), out(non_empty_list))
    +    is det.
     :- func list.sort_and_remove_dups(list(T)) = list(T).
     
         % list.sort(List0, List):
    @@ -1891,17 +1896,18 @@
     
     %-----------------------------------------------------------------------------%
     
    -:- pred list.merge_sort_and_remove_dups_2(int::in, list(T)::in, list(T)::out)
    -    is det.
    +:- pred list.merge_sort_and_remove_dups_2(int, list(T), list(T)).
    +:- mode list.merge_sort_and_remove_dups_2(in, in, out) is det.
    +:- mode list.merge_sort_and_remove_dups_2(in, in(non_empty_list), out(non_empty_list)) is det.
     :- pragma type_spec(list.merge_sort_and_remove_dups_2(in, in, out),
         T = var(_)).
     
     list.merge_sort_and_remove_dups_2(Length, List, SortedList) :-
    -    ( Length > 1 ->
    +    ( List = [A, B | Rest] ->
             HalfLength = Length // 2,
    -        ( list.split_list(HalfLength, List, Front, Back) ->
    +        ( list.split_list(HalfLength - 2, Rest, Front, Back) ->
                 list.merge_sort_and_remove_dups_2(HalfLength,
    -                Front, SortedFront),
    +                [A, B | Front], SortedFront),
                 list.merge_sort_and_remove_dups_2(Length - HalfLength,
                     Back, SortedBack),
                 list.merge_and_remove_dups(SortedFront, SortedBack, SortedList)
    --- library/solutions.m~	2011-04-06 22:26:52.724677229 -0400
    +++ library/solutions.m	2011-04-06 22:27:35.684254515 -0400
    @@ -196,7 +196,7 @@
     
     :- implementation.
     
    -:- import_module mutvar.
    +:- import_module exception, mutvar.
     
     %-----------------------------------------------------------------------------%
     
    @@ -248,10 +248,19 @@
     %-----------------------------------------------------------------------------%
     
     :- pred builtin_solutions(pred(T), list(T)).
    -:- mode builtin_solutions(pred(out) is multi, out) is det.  % really cc_multi
    +:- mode builtin_solutions(pred(out) is multi, out(non_empty_list)) is det.  % really cc_multi
     :- mode builtin_solutions(pred(out) is nondet, out) is det. % really cc_multi
    +:- pragma promise_equivalent_clauses(builtin_solutions/2).
     
    -builtin_solutions(Generator, UnsortedList) :-
    +builtin_solutions(Generator::pred(out) is multi, UnsortedList::out(non_empty_list)) :-
    +    builtin_aggregate(Generator, list.cons, [], UnsortedList0),
    +    (
    +        UnsortedList0 = [_|_], UnsortedList = UnsortedList0
    +    ;
    +        UnsortedList0 = [], throw(software_error("builtin_solutions"))
    +    ).
    +
    +builtin_solutions(Generator::pred(out) is nondet, UnsortedList::out) :-
         builtin_aggregate(Generator, list.cons, [], UnsortedList).
     
     %-----------------------------------------------------------------------------%
    
    patch file icon inst_match2.patch (14,424 bytes) 2011-04-07 13:37 +

-Relationships
+Relationships

-Notes

~0000321

colanderman (reporter)

Last edited: 2011-03-22 14:25

This seems to be part of a more general problem of complex insts not being propagated through predicate calls. Am I misunderstanding the semantics of the language?

Edit: seems to be related to bugs # 86 and 117.

~0000322

colanderman (reporter)

Squashed it, was a one-line fix in compiler/inst_match.m. Also fixes bugs 86 and 117. See attached patch.

~0000323

juliensf (administrator)

The above patch breaks compilation of the stage 2 standard library. (That doesn't necessarily
mean it is incorrect, since at least some the library code that breaks looks suspicious -- we
will need to look into this further before applying the above patch.)

~0000326

colanderman (reporter)

That's what I get for being sneaky and skipping the install phase :)

Attached is a (much larger) patch that fixes *most* of the library issues. It involved some mode additions to the list module (there really should be lots more), generalizing the mode of cc_multi_equal, and specializing cc_multi_equal in exception.m (this is due to the fact that the compiler chooses the di/uo mode of cc_multi_equal as "best" and doesn't try the other mode when it fails).

term_to_xml.m still doesn't compile, and I believe it is due to a possible bug I mentioned on the users mailing list, concerning predicates which refine nested insts. The error I'm getting is:

term_to_xml.m:1348: In clause for `'__Unify__'(in, (unique(list.'[|]'(free,
term_to_xml.m:1348: unique((list.[])))) >> bound(list.'[|]'(ground,
term_to_xml.m:1348: bound((list.[]))))), (ground >>
bound(list.'[|]'(ground,
term_to_xml.m:1348: bound((list.[]))))))':
term_to_xml.m:1348: mode error: argument 3 did not get sufficiently
term_to_xml.m:1348: instantiated.
term_to_xml.m:1348: Final instantiatedness of `HeadVar__2' was
term_to_xml.m:1348: `bound(list.'[|]'(ground, ground))',
term_to_xml.m:1348: expected final instantiatedness was
term_to_xml.m:1348: `bound(list.'[|]'(ground, bound((list.[]))))'.

which looks suspiciously similar to the issue I mentioned. I will focus my efforts on trying to track down that bug, and will hope that it's as simple as this one was to fix.

~0000859

juliensf (administrator)

This was fixed in commit 491bb0a.
+Notes

-Issue History
Date Modified Username Field Change
2011-03-22 13:52 colanderman New Issue
2011-03-22 13:52 colanderman File Added: instbug.m
2011-03-22 14:18 colanderman Note Added: 0000321
2011-03-22 14:25 colanderman Note Edited: 0000321
2011-04-05 12:21 colanderman File Added: inst_match.patch
2011-04-05 12:22 colanderman Note Added: 0000322
2011-04-07 03:22 juliensf Note Added: 0000323
2011-04-07 13:37 colanderman File Added: inst_match2.patch
2011-04-07 13:41 colanderman Note Added: 0000326
2015-11-02 11:10 juliensf Note Added: 0000859
2015-11-02 11:10 juliensf Status new => resolved
2015-11-02 11:10 juliensf Resolution open => fixed
2015-11-02 11:10 juliensf Assigned To => juliensf
+Issue History