association list with type-level keys which prevents duplicates by construction

TSL.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Data.Promotion.Prelude
import Data.Singletons.Prelude
import Data.Singletons.TypeLits

data TSL (a :: [k]) v where
  TNil :: TSL '[] v
  TCons :: NotElem a as ~ 'True
        => Sing (a :: k) -> v -> TSL (as :: [k]) v -> TSL (a ': as) v

-- tCons specialised to Symbol kinds
tCons' :: forall a v (as :: [Symbol]). SingI as
       => SSymbol a -> v -> TSL as v -> Maybe (TSL (a ': as) v)
tCons' p v l = case sNotElem p (sing :: Sing as) of
                STrue -> Just $ TCons p v l
                SFalse -> Nothing

tCons :: forall kparam (a :: k) v (as :: [k]). (kparam ~ ('KProxy :: KProxy k), SingI as, SEq kparam)
      => Sing a -> v -> TSL as v -> Maybe (TSL (a ': as) v)
tCons p v l = case sNotElem p (sing :: Sing as) of
                STrue -> Just $ TCons p v l
                SFalse -> Nothing

toList :: forall kparam (a :: [k]) v.
          (kparam ~ 'KProxy, SingKind (kparam :: KProxy k))
       => TSL a v -> [(DemoteRep kparam, v)]
toList TNil = []
toList (TCons p v r) = (fromSing p, v) : toList r

-- fromList specialised to Strings / Symbol kinds
fromList' :: [(String, v)] -> (forall (a :: [Symbol]). SingI a => TSL a v -> r) -> r -> r
fromList' []        k _ = k TNil
fromList' ((s,v):r) k f = withSomeSing s $ \ss -> withKnownSymbol ss $ fromList' r (\(t :: TSL (a' :: [Symbol]) v) -> case sNotElem ss (sing :: Sing a') of
                                                                                                                        SFalse -> f
                                                                                                                        STrue -> k $ TCons ss v t) f

fromList :: forall kparam v r. (kparam ~ ('KProxy :: KProxy k), SEq kparam, SingKind kparam)
         => [(DemoteRep kparam, v)] -> (forall (a :: [k]). SingI a => TSL a v -> r) -> r -> r
fromList []         k _ = k TNil
fromList ((s, v):r) k f = withSomeSing s $ \ss -> withSingI ss $ fromList r (\(t :: TSL (a' :: [k]) v) -> case sNotElem ss (sing :: Sing a') of
                                                                                                            SFalse -> f
                                                                                                            STrue  -> k $ TCons ss v t) f