{-# LANGUAGE DataKinds #-}
{-# 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)