Indexed Monad for uniquely consumed values

Unique.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DeriveFunctor #-}
module Unique ( 
  Unique(),
  Value(),

  return,
  (>>=),
  (>>),

  run,
  produce,
  consume,

  Delete,
  type (++),
  type (\\) 
) where 
import Prelude ((.), Functor, const)

data Unique :: [*] -> [*] -> * -> * where {
  Unique :: a -> Unique consumed produced a
} deriving Functor

data Value uid a = Value a deriving Functor

produce :: a -> Unique '[] '[uid] (Value uid a)
produce = Unique . Value

consume :: Value uid a -> Unique '[uid] '[] a
consume (Value a) = Unique a

(>>=) :: Unique cs ps a -> (a -> Unique cs' ps' b) -> Unique (cs ++ (cs' \\ ps)) ((ps \\ cs') ++ ps') b
(>>=) (Unique a) f = let Unique b = f a in Unique b

(>>) m m' = m >>= const m'

return :: a -> Unique '[] '[] a
return = Unique

run :: Unique '[] '[] a -> a
run (Unique a) = a

type family (m :: [*]) ++ (n :: [*]) :: [*] where
  '[]       ++ ys = ys
  xs        ++ '[] = xs
  (x ': xs) ++ ys = x ': (xs ++ ys)

type family (m :: [*]) \\ (n :: [*]) :: [*] where
  xs \\ '[] = xs
  '[] \\ ys = '[]
  xs \\ (y ': ys) = Delete y xs \\ ys

type family Delete (x :: *) (xs :: [*]) :: [*] where
  Delete x '[] = '[]
  Delete x (x ': xs) = xs
  Delete x (y ': xs) = y ': Delete x xs