[mercury-users] problem with existentially quantified higher order argument

[Julien Fischer]

I think that this has come up before.  It should be mentioned
in the BUGS file.

Julien.

On Mon, 2 Jul 2007, Mark Brown wrote:

> Hi Andrea,
>
> On 02-Jul-2007, Andrea Bini <andrea.bini at studenti.unimi.it> wrote:
>> hi all,
>> I have a problem using a discriminated union with a data constructor
>> containing a higher order type with a type variable existentially quatified.
>> I tried solving the problem by myself reading the guide but I didn't
>> succeed. The code is the following:
>>
>> :- pred get_int_range(int::in, int::in, list(int)::in, list(int)::out) is
>> det.
>> get_int_range(A,B,Lin,Lout) :-
>>   ( if
>>       A = B
>>     then
>>       Lout = [B|Lin]
>>     else
>>       B2 = B - 1,
>>       get_int_range(A,B2,[B|Lin],Lout)
>>   ).
>>
>> :- type gen ---> some [T] gen(pred(list(T))).
>> :- inst gen1 == bound(gen(pred(out) is det)).
>
> This *should* be the correct inst to use.
>
>>
>> :- pred try_gen(gen::in(gen1)) is det.
>> try_gen(gen(Gen)) :-
>>   call(Gen,_Dom).
>>
>> main(!IO) :-
>>   My_Int_Gen = get_int_range(1, 5, []),
>>   try_gen('new gen'(My_Int_Gen)).
>>
>>
>> compiling it as it is I get the following compiler error:
>>
>> Uncaught Mercury exception:
>> Software Error: modes.m: Unexpected: modecheck_set_var_inst: unify_inst
>> failed
>> Stack dump not available in this grade.
>
> Unfortunately, the mode analyser gets confused by the extra argument added
> to gen/1 for the typeinfo for T, which causes this exception.  (I've tried
> adding an extra argument to the inst, but that doesn't work either because
> some other part of the compiler gets confused.)
>
> One workaround is to use the inst `ground', but to call an unsafe_inst_cast
> predicate just before the call/N goal.  You can write the unsafe cast
> easily using foreign code.
>
> Another workaround may be to use a function instead of a predicate, because
> then you could use the default forward mode and the inst cast won't be
> needed.
>
>>
>> removing the try_gen invocation in the main predicate I get this cryptic, at
>> least for me, error:
>>
>> prova_errore.m:026: In clause for `try_gen(in((prova_errore.gen1)))':
>> prova_errore.m:026:   in argument 1 (i.e. the predicate term) of
>> higher-order
>> prova_errore.m:026:   predicate call:
>> prova_errore.m:026:   mode error: variable `Gen' has instantiatedness
>> `free',
>> prova_errore.m:026:   expecting higher-order pred inst (of arity 1).
>>
>> I think the problem is in the inst gen1 that is not correct but I cannot
>> understand why. If I use universally quantification, using the same inst,
>> all works correctly
>
> In this case, there will be no extra argument added to gen/1 for the typeinfo.
>
>> and I also have no problem if I use existential
>> quantification on a type variable that is not in an higher-order type (e.g.
>> if gen was declared like this ":- type gen ---> some [T] gen(list(T)).").
>
> In this case, there will be no call/N so the correct higher order inst is
> not needed.
>
> Hope that helps.
>
> Cheers,
> Mark.
>
> --------------------------------------------------------------------------
> mercury-users mailing list
> Post messages to:       mercury-users at csse.unimelb.edu.au
> Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
> Subscriptions:          mercury-users-request at csse.unimelb.edu.au
> --------------------------------------------------------------------------
>
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------