Generate fresh Typeable types.

Fresh.hs

module Fresh
  ( Fresh, runFresh, withFresh
  ) where

import Data.Typeable

import Control.Monad.State (StateT, evalStateT, get, put)
import Control.Monad.Trans (MonadTrans)


data Z
data S n

data SomeTypeable where
  SomeTypeable :: (Typeable k, Typeable x) => Proxy (x :: k) -> SomeTypeable


newtype Fresh m a = Fresh (StateT SomeTypeable m a)
  deriving (Functor, Applicative, Monad, MonadTrans)

runFresh :: Monad m => Fresh m a -> m a
runFresh (Fresh s) = evalStateT s (SomeTypeable (Proxy :: Proxy Z))

withFresh
  :: Monad m
  => (forall k (x :: k). Typeable x => Proxy x -> Fresh m r)
  -> Fresh m r
withFresh f = do
  SomeTypeable (p :: Proxy n) <- Fresh get
  Fresh (put (SomeTypeable (Proxy :: Proxy (S n))))
  f p