determinism question

[Don Smith]

Hello,

For the following code, the Mercury compiler is able to verify
the determinism declaration.

  :- pred p(int::out, list(int)::in,list(int)::out) is semidet.
  p(0) --> [0].
  p(N) --> [1],p(Tmp), {N is Tmp+1}.
  p(N) --> [2],p(Tmp), {N is Tmp+2}.
  p(N) --> [3],p(Tmp), {N is Tmp+3}.

But for the following logically equivalent code, the compiler says
test.m:022: In `p(out, in, out)':
test.m:022:   error: determinism declaration not satisfied.
test.m:022:   Declared `semidet', inferred `nondet'.
test.m:023:   Disjunction has multiple clauses with solutions.

  :- pred p(int::out, list(int)::in,list(int)::out) is semidet.
  p(X) --> p0(X) ; p1(X) ; p2(X) ; p3(X).
  
  :- pred p0(int::out, list(int)::in,list(int)::out) is semidet.
  :- pred p1(int::out, list(int)::in,list(int)::out) is semidet.
  :- pred p2(int::out, list(int)::in,list(int)::out) is semidet.
  :- pred p3(int::out, list(int)::in,list(int)::out) is semidet.
  p0(0) --> [0].
  p1(N) --> [1],p(Tmp), {N is Tmp+1}.
  p2(N) --> [2],p(Tmp), {N is Tmp+2}.
  p3(N) --> [3],p(Tmp), {N is Tmp+3}.

Couldn't the compiler unfold the definitions of p0, p1, p2, and p3 and
thereby infer that the disjuncts in the rule for p/1 are mutually exclusive?  
You'd need to make sure that you didn't unfold so much that it looped at
compile time.

  Don