Coercing an existential subtype constructor in the same clause produces mode error

[C4Cypher]

I am finding that I get a mode error if I attempt to construct a subtype with an existentially typed subterm and then coerce it to the supertype in the same clause. If I move the constructor to it's own call, the problem does not exhibit. Is this intended behavior and am I missing something about how a constructed existentially typed data type is instantiated?

Unit test example:

:- module test.

:- interface.
:- import_module io.

:- pred main(io::di, io::uo) is det.

:- implementation.

:- import_module string.

:- type foobar 
    --->    some [T] foo(T)
    ;       bar.

:- type foo =< foobar
    --->    some [T] foo(T).

:- pred printfoobar(foobar::in, io::di, io::uo) is det.

printfoobar(Foobar, !IO) :- 
    write_string("Foobar: " ++ string(Foobar) ++ "\n", !IO).

:- func newfoo(T) = foo.

newfoo(T) = 'new foo'(T).

main(!IO) :-  % Compiles and executes properly
    Foo = newfoo(5),
    Foobar = coerce(Foo),
    printfoobar(Foobar, !IO).

/*  
main(!IO) :- 
    Foo = 'new foo'(5):foo,
    Foobar = coerce(Foo),
    printfoobar(Foobar, !IO).

$ mmc -E --make test.exe
Making Mercury\int3s\test.int3
Making Mercury\ints\test.int
Making Mercury\cs\test.c
test.m:045: In clause for `main(di, uo)':
test.m:045:   mode error in conjunction. The next 2 error messages indicate
test.m:045:   possible causes of this error.
test.m:045:
test.m:044:   In clause for `main(di, uo)':
test.m:044:   in coerce expression:
test.m:044:   mode error: the instantiatedness of the argument term
test.m:044:     unique(
test.m:044:       foo(
test.m:044:         unique(
test.m:044:           <type_ctor_info for builtin.int/0>
test.m:044:         ),
test.m:044:         unique(
test.m:044:           5
test.m:044:         )
test.m:044:       )
test.m:044:     )
test.m:044:   is invalid for the type of the argument term `test.foo'.
test.m:045:
test.m:045:   In clause for `main(di, uo)':
test.m:045:   in argument 1 of call to predicate `test.printfoobar'/3:
test.m:045:   mode error: variable `Foobar' has instantiatedness `free',
test.m:045:   expected instantiatedness was `ground'.

*/

I understand the second part of the error message, given that mode analysis cannot ground Foobar if there is a mode error with the coerce expression. What I do not understand is the mode requirements for the coerce expression. Is it the uniqueness of the constructed data term that is causing the error?

[wangp]

Thanks for the test case. It shows an oversight in the modechecker, which cannot coerce terms that include existential types.

Under the hood, each existentially quantified argument adds a hidden type_info argument, which aren't being accounted for when modechecking coerce. But there is likely to be more to it.

[juliensf]

It's likely the same set of issues (or very closely related) that occur with Mantis bug #89 for inst subtyping.

[C4Cypher]

My pleasure. I want to help in any way I can, and while I haven't dug into the source enough to really grok the compiler yet, I hope, in the future, to help tackle things like fixing unique modes and run-time typeclass introspection. That and I know my way around a bug report. Please let me know if there's anything I can provide that can help further.

[C4Cypher]

Interesting, I'm running into this issue again when passing existentially boxed values to modes that are sub-insts of, but not strictly 'ground'.

:- pragma promise_equivalent_clauses(value_term/1).

value_term(V::in) = ('new mr_value'(V)::out(mercury_value)).
value_term(V2::out) = (mr_value(V1)::in) :- dynamic_cast(V1, V2).

/*
$ mmc --make libmh_term
Making Mercury\int3s\mh_term.int3
Making Mercury\ints\mh_term.int
Making Mercury\cs\mh_term.c
mh_term.m:155: In clause for `value_term(in) = out((mh_term.mercury_value))':
mh_term.m:155:   mode error: argument 3 had the wrong instantiatedness.
mh_term.m:155:   Final instantiatedness of `HeadVar__2' was
mh_term.m:155:   `unique(mr_value(ground, ground))', 
mh_term.m:155:   expected final instantiatedness was
mh_term.m:155:     named inst mercury_value
mh_term.m:155:     which expands to
mh_term.m:155:       bound(
mh_term.m:155:         mr_value(ground)
mh_term.m:155:       ).
** Error making `Mercury\cs\mh_term.c'.
*/

I'm assuming that the mode checker is tripping up on the second argument in the inst of 'HeadVar_2', not the uniqueness

P.S. Moving the unification of the headvar and the existential constructor into the body of the clause results in the same error.

value_term(V::in) = (T::out(mercury_value)) :- T = 'new mr_value'(V).

[wangp]

Fixed in rotd-2024-07-11.