Skip to content

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?

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information