While writing about how to do subtyping in Haskell, it occurred to me that it would be very convenient to be able to "use" contradictory evidence such as True ~ False
to inform the compiler about dead branches. With another standard empty type, Void
, the EmptyCase
extension allows you to mark a dead branch (i.e. one that contains a value of type Void
) this way:
use :: Void -> a
use x = case x of
I'd like to do something similar for unsatisfiable Constraint
s.
Is there a term which can be given the type True ~ False => a
but cannot be given the type a
?