Для программирования в ограничениях (constraint programming) характерно отсутствие объяснений, почему же система не имеет решений: то ли это программист перестарался, сделав систему сверхограниченной, то ли задача сама по себе не имеет решений.

Страничка на LtU со ссылками на диссертацию про улучшение ошибок при выводе типов и на сайт, посвящённый алгоритмам решения систем ограничений на основе объяснений (explanation).

(Системы программирования в ограничениях используются для проверок и вывода типов.)