Implement Unsatisfiable as an alternative to TypeError
This proposal has been accepted: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst
Implementing this will require extending GHC.TypeError
with the following definitions, and adding special-purpose behaviour to Unsatisfiable
constraints as described in the proposal. This will provide an alternative to TypeError
that is more clearly specified.
class Unsatisfiable (e :: ErrorMessage) where
unsatisfiableLifted :: a
unsatisfiable :: forall (e :: ErrorMessage) {rep} (a :: TYPE rep). Unsatisfiable e => a
unsatisfiable = unsatisfiableLifted @e @((# #) -> a) (# #)
Would anyone be interested in implementing this?