[m-dev.] mmc bug

[Ralph Becket]

Peter Schachte, Tuesday,  7 March 2006:
> Hi,
> 
> It seems that Mark's concern about mmc handling any>>ground modes was
> justified.  The attached test program gives this error:
> 
>     ground.m:049: In predicate `ground.eq/4':
>     ground.m:049:   warning: declared impure but actually pure.
>     ground.m:057: In clause for `label((any >> ground))':
>     ground.m:057:  mode error: argument 1 did not get sufficiently
>     instantiated.
>     ground.m:057:  Final instantiatedness of `HeadVar__1' was
>     `bound((list.[]) ;
>     ground.m:057:   list.'[|]'(any, any))',
>     ground.m:057:   expected final instantiatedness was `ground'.
>     ground.m:023: In `label1((any >> ground))':
>     ground.m:023:   warning: determinism declaration could be tighter.
>     ground.m:023:   Declared `nondet', inferred `det'.
> 
> Ignore the warnings at the beginning and end.  The error in the middle
> suggests to me that mmc doesn't think an any can ever become ground.

> :- pred label(list(fdvar)::(any>>ground)) is nondet.
>
> label([]).
> label([X | Xs]):-
>         label1(X),
>         label(Xs).
> 
> :- pred label1(fdvar::(any>>ground)) is nondet.
>
> label1(X) :-
> 	promise_pure
> 	(   unsafe_cast_to_ground(X)
> 	).

The problem here is that the compiler hasn't inferred that since the
spine of the list argument to label/1 must be ground (list/1 isn't a
solver type) and the argument has become ground, then the whole
thing must be ground afterwards.

This is probably a bug, but I won't have time to look into it for a
while (it isn't serious since you can just call unsafe_cast_to_ground
on the list as a whole).

I should point out that {solver type, inst any}, {non-solver type, inst
ground} are natural companions, but {solver type, inst ground} is going
to lead you into a world of pain.  We need someone to do a PhD on the
mode system...

-- Ralph
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------