-- Like Key from vault:
--
-- https://github.com/HeinrichApfelmus/vault/blob/master/src/Data/Vault/ST/backends/GHC.h#L19C29-L20C1

{-# LANGUAGE RoleAnnotations #-}

module Bluefin.Internal.Key
  ( Key,
    newKey,
    eqKey,
  )
where

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

type role Key nominal

newtype Key (a :: k) = MkKey Unique

newKey :: IO (Key a)
newKey :: forall {k} (a :: k). IO (Key a)
newKey = IO Unique -> IO (Key a)
forall a b. Coercible a b => a -> b
coerce IO Unique
newUnique

-- 'Key' cannot lawfully be 'TestEquality', though it could be 'GEq'
-- and 'GOrd'.
eqKey :: forall a b. Key a -> Key b -> Maybe (a :~~: b)
eqKey :: forall {k1} {k2} (a :: k1) (b :: k2).
Key a -> Key b -> Maybe (a :~~: b)
eqKey (MkKey Unique
id1) (MkKey Unique
id2) =
  if Unique
id1 Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
id2
    then (a :~~: b) -> Maybe (a :~~: b)
forall a. a -> Maybe a
Just ((a :~~: a) -> a :~~: b
forall a b. a -> b
unsafeCoerce (forall (a :: k1). a :~~: a
forall {k1} (a :: k1). a :~~: a
HRefl @a))
    else Maybe (a :~~: b)
forall a. Maybe a
Nothing