Enquanto escreviasobre como fazer a subtipagem em Haskell, ocorreu-me que seria muito conveniente poder "usar" evidências contraditórias, comoTrue ~ False para informar o compilador sobre ramificações mortas. Com outro tipo vazio padrão,Void, aEmptyCase A extensão permite marcar um ramo morto (ou seja, um que contenha um valor do tipoVoid) deste jeito:

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

Eu gostaria de fazer algo semelhante por insatisfatórioConstraints.

Existe um termo que pode receber o tipoTrue ~ False => a mas não pode receber o tipoa?