11.2 Failure versus Programming Error

Of course, it is possible to write down a set of equations without solutions. In this case unification fails. There are several interpretations for failure: Either it may be considered as logical information about unsolvability of equations or else as a programming error. In Oz, unsolvable equations should only occur using constructs from constraint programming. Otherwise, failure is considered as programming error. If you feed the following equations for instance, then failure is already recognized statically.

X = f(_ a)
Y = f(_ g(b))
X = Y

The same kind of failure may also raise a programming error at run time:

declare 
proc{Constrain X Y}
   X = f(_ a)
   Y = f(_ g(b))
end 
{Constrain X X}

Only when used in search, failure is considered as logical information and not as programming error.