2024-11-22 00:18 AEDT
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000387mercuryBugpublic2015-07-06 12:502015-07-07 14:58
Reporterpbone 
Assigned To 
PrioritynormalSeveritymajorReproducibilityalways
StatusnewResolutionopen 
Platformx86_64OSDebianOS Versionstretch
Product Version 
Target VersionFixed in Version 
Summary0000387: Polymorphism pass miscompiles some try goals.
DescriptionI get the following error:

polymorphism_try_bug.m:031: In clause for `test(in, di, uo)':
polymorphism_try_bug.m:031: mode mismatch in disjunction.
polymorphism_try_bug.m:031: The variable `TypeInfo_25' has these
polymorphism_try_bug.m:031: instantiation states:
polymorphism_try_bug.m:031: line 26: free
polymorphism_try_bug.m:031: line 26: ground

My predicate contains a try goal with a catch_any block. The TypeInfo in question is the type info for the exception, which passed out of the try goal in a maybe_error type and named-appart.
Steps To Reproducemmc --use-grade-subdirs -O3 --allow-stubs --no-warn-stubs --compile-to-c test_bdd_bug.m
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0000831

mark (administrator)

2015-07-06 17:28

 How do you think this ought to be compiled? What type should MaybeBDD have, for example?

The error message can be improved: you had to figure out what TypeInfo_25 was, and both line numbers refer to the containing disjunction instead of the disjuncts. Also, it's a try goal not a disjunction. But I think the general idea is right, in that the type was bound in one branch and not in another.

This issue applies to an existential type escaping from any form of disjunct. I'll upload a simplified case.

~0000832

pbone (administrator)

2015-07-06 19:28

 I think that this can be compiled correctly, if unintuitive. If MaybeBDD is typed as some [E] maybe_error(bdd(V), {string, E}).

It will become unintuitive if the exception type appears in the head of the clause, that will require the predicate to be existentially typed.

~0000833

mark (administrator)

2015-07-06 23:42

 To put the question another way, what would be the output of calling io.write(type_desc.type_of(MaybeBDD), !IO)? What's in the type_desc for E?

For the error branch, the type_desc is obviously meant to be whatever type_desc the exception value had. But for the ok branch, the type_desc is not provided anywhere. That's more or less what the compiler error message is trying to say.

Note that a similar idiom to those documented in the Existential Types chapter also applies here, namely, wrap ExpPrime in a univ:

catch_any ExpPrime ->
    MaybeBDD = error({"My message", univ(ExpPrime)})

~0000834

pbone (administrator)

2015-07-07 10:29

 I tried breaking the predicate into two parts so that I can put the try goal in a predicate that explicitly returns an existential type. (My idea is that the types should be named apart and the type of the exception should be set when MaybeBDD is unified with error and deconstructed.

    :- some [E] pred test_try(bexpr(V)::in, maybe_error(bdd(V), {string, E})::out)
        is det.

    test_try(BooleanExpression, MaybeBDD) :-
        promise_equivalent_solutions [MaybeBDD] (
        ( try []
            BDDPrime = make_bdd(BooleanExpression)
          then
            MaybeBDD = ok(BDDPrime)
          catch_any ExpPrime ->
            MaybeBDD = error({"My error message", ExpPrime})
        )).

    test2(BooleanExpression, !IO) :-
        test_try(BooleanExpression, MaybeBDD),
        ( MaybeBDD = ok(BDD)
        ; MaybeBDD = error({ErrMessage, _}),
            % This deconstructon should determine the type of the error.
            write_string(ErrMessage, !IO),
            sorry($pred, "Error")
        ),
        io.write(BDD, !IO).

But this doesn't work. and using `new error` doesn't work because error is not existentially typed itself. (I'm learning more about existential types BTW.)

    :- type maybe_error(T)
        ---> ok(T)
        ; some [E] error(string, E).

    test2(BooleanExpression, !IO) :-
        promise_equivalent_solutions [MaybeBDD] (
        ( try []
            BDDPrime = make_bdd(BooleanExpression)
          then
            MaybeBDD = ok(BDDPrime)
          catch_any ExpPrime ->
            MaybeBDD = 'new error'("My error message", ExpPrime)
        )),
        ( MaybeBDD = ok(BDD)
        ; MaybeBDD = error(ErrMessage, _),
            % This deconstructon should determine the type of the error.
            write_string(ErrMessage, !IO),
            sorry($pred, "Error")
        ),
        io.write(BDD, !IO).

This works, it solves the problem in the same way as your use of univ. I've learnt that if I want the type of the error to be determined when error is deconstructed, then I need error to have the existential type applied to it. (Or univ, if I want it a little later).

We can make it a type error for the type of an exception to escape the catch_any branch. Or indeed any branching structure, this will allow us to produce a better error message. Do you agree? is a type error the way to go here? (My reasoning is that the program is incorrectly typed.)

~0000835

pbone (administrator)

2015-07-07 10:29

 Thank you.

~0000836

mark (administrator)

2015-07-07 14:58

 Breaking it into two parts better illustrates why this is a program error, not just a compiler bug. The signature says that there is "some" type, which means that this predicate is responsible for producing that type (see "Semantics of type quantifiers" in the reference manual). But the programmer only provides that type in the catch_any clause, not in the then clause, hence the "mode" mismatch.

The compiler could fill in the type as 'void', like in other circumstances, but this doesn't seem a good idea. If the programmer has provided a type in at least one branch of a branched structure, they ought to do so in all branches. In any case the compiler's use of 'void' would generate a warning.

Which brings us to a different problem: there is no way to give different types in different branches anyway, because that would be a type error. So the following won't work:

    ( X = 1 ; X = "foo" ), io.write(X, !IO)

Instead you must push the polymorphic calls inside the branches:

    ( X = 1, io.write(X, !IO) ; X = "foo", io.write(X, !IO) )

or else you can "box" the existential type:

    ( X = 1, UX = univ(X) ; X = "foo", UX = univ(X) ),
    io.write(univ_value(UX), !IO)

So, regarding your last question, if the programmer does address the "mode" error by providing a type for every branch (or none), then with the current language they will already necessarily receive a "type" error, as the existential type in one branch is opaque and cannot be referred to in the other branches.

I don't think it matters much whether these are called mode errors or type errors. Given that the type quantifier determines where a type is produced, the two concepts amount to the same thing as far as checking the quantifiers is concerned.
+Notes

-Issue History
Date Modified Username Field Change
2015-07-06 12:50 pbone New Issue
2015-07-06 12:50 pbone File Added: polymorphism_try_bug.m
2015-07-06 17:28 mark Note Added: 0000831
2015-07-06 17:30 mark File Added: bug387.m
2015-07-06 19:28 pbone Note Added: 0000832
2015-07-06 23:42 mark Note Added: 0000833
2015-07-07 10:29 pbone Note Added: 0000834
2015-07-07 10:29 pbone Note Added: 0000835
2015-07-07 14:58 mark Note Added: 0000836
+Issue History