With this definition:
member _ [] = False
member x (h:t) = if x == h then True else member x t
PAKCS 2.0.1 (from Ubuntu 18.04) gives no answers, warnings or errors:
Top-level binding with no type signature:
member :: Prelude.Eq a => a -> [a] -> Prelude.Bool
member> member x [1, 2, 3] =:= True where x free
member>
I expected to see 3 values. What am I doing wrong here?
The program <smap.informatik.uni-kiel.de/smap.cgi?75> gives only one solution since the rule
member x (h:t) = if x =:= h then True else member x t
unifies x with the first element of the list and yields True and nothing else.
Note that (=:=) is a unification constraint rather than a Boolean test. This means that x =:= 1 binds x to 1 (in order to satisfy the constraint) and yields True but never False. Hence, 2 =:= 1 simply fails rather than yielding False. On the other hand, 2 == 1 yields False. Thus, you might expect that x == 1 binds x to 1 yielding True or binds x to 2, 3, 4,... yielding False. Actually, this is the case in the Curry implementation KiCS2 but PAKCS is for some reason more restricted so that it suspends on this expression.
One further remark: one can view (=:=) as an optimization of (==) which can be used in case where only the result True is required, e.g., in conditions of rules. Therefore, newer PAKCS implementation automatically transform (==) into (=:=) in such cases so that only (==) might be used in source programs. Further details can be found in this paper.