Unification is not the right logic for assertion resolution

[Thierry Delisle]

Currently assertion resolution uses unification. This means that to check if a function can satisfy an assertion we use the same rules as to obtain the type of ternary if expression.

The leads to problems where an expression that would resolve normally doesn't necessarily resolve assertions.
For example:

forall( dtype T | sized(T) | { void ^?{}( T & ); } ) void delete( T * ptr );

monitor a {};
void ^?{}( T mutex & this );

int main() {
    a * p = ...;
    delete(a); // destructor does not unify because of mutex
}

To fix this we need to use check assertion satisfaction using resolution rather than unification.