Catch and throw exceptions without Typeable constraints

ID.hs

{-# LANGUAGE GHC2021, RoleAnnotations #-}

module ID (
  ID, newID,
  sameID,
) where

-- base
import Unsafe.Coerce (unsafeCoerce)
import Data.Coerce (coerce)
import Data.Type.Equality ((:~~:)(..))
import Data.Unique (Unique, newUnique, hashUnique)

type role ID nominal
newtype   ID (a :: k) = ID Unique

instance Show (ID a) where
  show (ID u) = "<ID:" ++ show (hashUnique u) ++ ">"

newID :: IO (ID a)
newID = coerce newUnique

-- | 'ID' cannot lawfully be 'TestEquality', though it could be 'GEq' & 'GOrd'.
sameID :: forall a b. ID a -> ID b -> Maybe (a :~~: b)
sameID (ID id1) (ID id2)
  | id1 == id2 = Just (unsafeCoerce (HRefl @a))
  | otherwise  = Nothing

Parametrically.hs

{-# LANGUAGE GHC2021, GADTs #-}

module Parametrically (parametrically) where

-- base
import Data.Type.Equality ((:~~:)(..))
import Data.Functor ((<&>))
import Control.Exception (Exception, throwIO, handleJust)

import ID

-- | Catch and throw exceptions without 'Typeable' constraints.
--
-- > parametrically (\throw -> ... ) \exn -> ...
--
parametrically :: ((forall x. e -> IO x) -> IO a) -> (e -> IO a) -> IO a
parametrically scope handleEx = do
  ident <- newID
  handleJust
    (check ident)
    handleEx
    (scope (throwIdentified ident))


data Identified = forall a. Identified (ID a) a

instance Show Identified where
  showsPrec d (Identified id_ _)
    = showParen (d >= 11)
    $ showString "Identified " . showsPrec 11 id_ . showString " _"

instance Exception Identified

check :: ID a -> Identified -> Maybe a
check id1 (Identified id2 r) = id1 `sameID` id2 <&> \HRefl -> r

throwIdentified :: ID a -> a -> IO b
throwIdentified ident = throwIO . Identified ident