Unique type generation via linearity

Fresh.hs

{-# OPTIONS_GHC -Wno-unused-foralls #-}
{-#
LANGUAGE
  UnliftedNewtypes, UnboxedTuples, DataKinds, LinearTypes, TypeFamilies,
  RoleAnnotations, RequiredTypeArguments, LiberalTypeSynonyms
#-}

module Fresh (
  Source, create, destroy,
  type ( # ), fresh,
  runExists,
) where

-- GHC/base
import GHC.Exts (TYPE, ZeroBitType, Multiplicity(One))
import GHC.TypeNats (Nat, type (+))

-- base
import Data.Kind (Type, FUN)

type role Source    nominal nominal
type      Source :: Type -> Nat  -> ZeroBitType
newtype   Source    x       n     = MkSource (# #)

{-# NOINLINE create #-}
create :: (forall x. Source x 0 ―○ Ur r) ―○ r
create k = case k (MkSource (# #)) of
  Ur r -> r

{-# INLINE destroy #-}
destroy :: Source x n ―○ (# #)
destroy (MkSource t) = t

newtype x # n = MkFresh (Source x n)

{-# INLINE fresh #-}
fresh :: Source x n ―○ (Source x (n + 1) ―○ x # n ―○ r) ―○ r
fresh src k = k (MkSource (# #)) (MkFresh src)

type family (x :: Type) ## (n :: Nat) :: k where {}

{-# INLINE runExists #-}
runExists :: forall x n r k. x # n ―○ (forall (t :: k) -> r) ―○ r
runExists (MkFresh src) k = k (x ## n)
 where
  !(# #) = destroy src


type (―○) :: forall rr1 rr2. TYPE rr1 -> TYPE rr2 -> Type
type (―○) = FUN One
infixr 0 ―○

data Ur a where
  Ur :: a -> Ur a