Пока пишуо том, как сделать подтип в Хаскелемне пришло в голову, что было бы очень удобно иметь возможность "использовать" противоречивые доказательства, такие какTrue ~ False сообщить компилятору о мертвых ветках. С другим стандартным пустым типом,Void,EmptyCase Расширение позволяет пометить мертвую ветвь (то есть ту, которая содержит значение типаVoid) сюда:

use :: Void -> a
use x = case x of

Я хотел бы сделать что-то подобное для неудовлетворенныхConstraints.

Есть ли термин, который может быть дан типTrue ~ False => a но нельзя дать типa?