Для программирования в ограничениях (constraint programming) характерно отсутствие объяснений, почему же система не имеет решений: то ли это программист перестарался, сделав систему сверхограниченной, то ли задача сама по себе не имеет решений.
Страничка на LtU со ссылками на
диссертацию про улучшение ошибок при выводе типов и на
сайт, посвящённый алгоритмам решения систем ограничений на основе объяснений (explanation).
(Системы программирования в ограничениях используются для проверок и вывода типов.)