{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module LocationTF where
import Data.Proxy
import GHC.TypeLits
data Location (area :: Area) (section :: Section) where
    Area :: KnownSymbol area => Proxy area -> Location area Nothing
    Location :: (KnownSymbol area, KnownSymbol n) => Proxy area -> Proxy n -> Location area (Just n)
type Area = Symbol
type Section = Maybe Symbol
area :: forall a b. (KnownSymbol a) => Location a b -> String
area _ = symbolVal $ Proxy @a
section :: forall a b. (KnownSymbol a, KnownSymbol b) => Location a (Just b) -> String
section _ = symbolVal $ Proxy @b
location :: forall a b. KnownSymbol (ToLocation a b) => Location a b -> String
location x = symbolVal $ Proxy @(ToLocation a b)
type family ToLocation (a :: Area) (b :: Section) :: Symbol where
    ToLocation x 'Nothing = x
    ToLocation x ('Just y) = AppendSymbol x (AppendSymbol " - " y)