Transform a functional decision to boolean in/equality

Apart.hs

{-#
LANGUAGE
  GHC2021, GADTs, DataKinds, ExplicitNamespaces, BlockArguments, LambdaCase
#-}

module Apart (apart, equal, boolean) where

import Data.Void (Void)
import Data.Type.Equality ((:~:)(..), type (==))
import Data.Bifunctor
import Unsafe.Coerce (unsafeCoerce)

apart :: (a :~: b -> Void) -> (a == b) :~: False
equal ::  a :~: b          -> (a == b) :~: True
apart f = f axiom `seq` axiom
 where axiom = unsafeCoerce Refl
equal Refl = unsafeCoerce (Refl @True)

boolean
  :: Either (a :~: b -> Void)    (a :~: b)
  -> Either ((a == b) :~: False) ((a == b) :~: True)
boolean = bimap apart equal

_works :: (() == Bool) :~: False
_works = apart @() @Bool \case{}

_explodes :: (() == ()) :~: False
_explodes = apart @() @() \_ -> undefined