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

[Mark Brown]

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
--------------------------------------------------------------------------