[m-users.] Compiler cannot infer determinism det when exhaustively pattern matching on a constant?

[Volker Wysk]

Am Mittwoch, dem 31.07.2024 um 19:56 +0200 schrieb Anders Lundstedt:
> Dear all,

Hi.

> 
> I try to define a predicate by exhaustive pattern matching on a
> constant. The compiler complains:
> 
> “determinism declaration not satisfied. Declared `det', inferred `nondet'.”
> 
> Why?
> 
> 
> Example code below, showing what fails (the predicate p3) and also
> showing a workaround (the predicate p2, using helper predicate p1):
> 
> :- module test.
> :- interface.
> :- type t ---> c1; c2.
> :- pred p1(t::in, t::out) is det.
> :- pred p2(t::out) is det.
> :- pred p3(t::out) is det.
> :- implementation.
> :- func c = t.
> c = c1.
> % accepted by compiler
> p1(A, B) :- (A = c1, B = c2) ; (A = c2, B = c1).
> % accepted by compiler
> p2(A) :- p1(c, A).
> % compiler error
> p3(A) :- (c = c1, A = c2) ; (c = c2, A = c1).

I'm not entirely sure, but I think it's a limitation in the reasoning that
the compiler can do. It looks like it isn't a switch when you don't test a
variable but a constant. In order to see that there's always one solution,
the compiler would have to optimize away the second one of the two disjuncts
of p3 and optimize away the "c = c1" part of the first disjunct. Looks like
it doesn't do that.

I find the error message hard to follow.

Cheers,
Volker