Are there any rows which can satisfy the ct's CHECK constraint? If not, why we allow creating table when check constraint itself is contradicted?
I'd bet on it being a combination of complexity and insufficient expected benefit. Time is better spent elsewhere. Mathmatically proving a contradiction in software is harder than reasoning about it mentally.
I've actually used that as a feature, in postgresql and other databases, where assertions were unavailable, or procedural code was unavailable or against policy.
Consider the following:
CREATE TABLE wanted_values ( x integer );
INSERT INTO wanted_values VALUES (1), (2), (3);
CREATE TABLE found_values ( x integer );
INSERT INTO found_values VALUES (1), (3);
CREATE TABLE missing_values (
x integer,
CONSTRAINT contradiction CHECK (false)
);
INSERT INTO missing_values
SELECT x FROM wanted_values
EXCEPT
SELECT x FROM found_values;
gives the error
ERROR:new row for relation "missing_values" violates check constraint "contradiction"
DETAIL:Failing row contains (2).
Which can be handy when you need to fail a transaction because of bad data and don't have branching logic available.
