Negation and De Morgan's Law not part of C++20 partial ordering by constraints

The rules for partial ordering by constraints refer to AND and OR, but do not refer to NOT:

13.5.4 Partial ordering by constraints [temp.constr.order]
(1.2) ...
- The constraint A ∧ B subsumes A, but A does not subsume A ∧ B.
- The constraint A subsumes A ∨ B, but A ∨ B does not subsume A.

These rules are based on the definitions of atomic constraints and constraints normalization:

13.5.3 Constraint normalization [temp.constr.normal]
1 The normal form of an expression E is a constraint that is defined
  as follows:
(1.1) The normal form of an expression ( E ) is the normal form of E.
(1.2) The normal form of an expression E1 || E2 is the disjunction
      of the normal forms of E1 and E2.
(1.3) The normal form of an expression E1 && E2 is the conjunction
      of the normal forms of E1 and E2.

Negation (i.e. !E1) is specifically NOT handled.

Thus the following code is using partial ordering correctly:

void foo(auto i) requires std::integral<decltype(i)> {
    std::cout << "integral 1" << std::endl;
}

void foo(auto i) requires std::integral<decltype(i)> && true {
    std::cout << "integral 2" << std::endl;
}

int main() {
    foo(0); // integral 2
}

while this code fails with ambiguity:

template<typename T>
concept not_integral = !std::integral<T>;

template<typename T>
concept not_not_integral = !not_integral<T>;

void foo(auto i) requires not_not_integral<decltype(i)> {
    std::cout << "integral 1" << std::endl;
}

void foo(auto i) requires std::integral<decltype(i)> && true {
    std::cout << "integral 2" << std::endl;
}

int main() {
    foo(0);
}

Code: https://godbolt.org/z/RYjqr2

---

Above causes De Morgan's Law not to work for concepts:

template<class P>
concept has_field_moo_but_not_foo
     = has_field_moo<P> && !has_field_foo<P>;

is not equivalent to:

template<class P>
concept has_field_moo_but_not_foo
     = !(has_field_foo<P> || !has_field_moo<P>);

the first would participate in partial ordering while the latter would not.

Code: https://godbolt.org/z/aRhmyy

---

Was the decision, not to handle negation as part of constraint normalization, taken in order to ease the implementation for compiler vendors? or is there a logical flaw with trying to support it?

Was the decision, not to handle negation as part of constraint normalization, taken in order to ease the implementation for compiler vendors?

Yes. This generalizes to requiring a SAT solver in the compiler.

There was an example added in [temp.constr.op]/5 to demonstrate this, although it does not provide the rationale for the decision:

template <class T> concept sad = false;

template <class T> int f1(T) requires (!sad<T>);
template <class T> int f1(T) requires (!sad<T>) && true;
int i1 = f1(42);        // ambiguous, !sad<T> atomic constraint expressions ([temp.constr.atomic])
                        // are not formed from the same expression

template <class T> concept not_sad = !sad<T>;
template <class T> int f2(T) requires not_sad<T>;
template <class T> int f2(T) requires not_sad<T> && true;
int i2 = f2(42);        // OK, !sad<T> atomic constraint expressions both come from not_­sad

template <class T> int f3(T) requires (!sad<typename T::type>);
int i3 = f3(42);        // error: associated constraints not satisfied due to substitution failure

template <class T> concept sad_nested_type = sad<typename T::type>;
template <class T> int f4(T) requires (!sad_nested_type<T>);
int i4 = f4(42);        // OK, substitution failure contained within sad_­nested_­type

In particular, note the difference between f3 and f4. Does requires !sad<typename T::type> mean that there be no sad nested type, or that there be a nested type that is not sad? It actually means the latter, while the constraint on f4 means the former.