Function Returns “No Solution” Instead Of “Nothing”

Question

I have a standard datatype representing formulae of predicate logic. A function representing a natural deduction elimination rule for disjunction might look like:

d_el p q =
  if p =: (Dis r s) && q =: (Neg r) then Just s else
  if q =: (Dis r s) && p =: (Neg r) then Just s else
     Nothing where r,s free

x =: y = (x =:= y) == success

Instead of evaluating to Nothing when unification fails, the function returns no solutions in PACKS:

logic> d_el (Dis Bot Top) (Not Bot)
Result: Just Top
More Solutions? [Y(es)/n(o)/a(ll)] n
logic> d_el (Dis Bot Top) (Not Top)
No more solutions.

What am I missing, and why doesn't el evaluate to Nothing when unification fails?

Answer 1

It seems that this is not the best way to use equational constraints. When a =:= b fails then complete function clause fails also.
E.g.:

xx x = if (x =:= 5) == success then 1 else x
xx x = 3

Evaluating xx 7 results in 3 (not 7) because 7 =:= 5 completely terminates first clause of the xx function.

I think the code should look like this:

d_el p q = case (p,q) of
   (Dis a s, Neg b) -> if a == b then Just s else Nothing
   (Neg a, Dis b s) -> if a == b then Just s else Nothing
   _ -> Nothing