{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances #-}

import GHC.Records
import GHC.Types

data STPair = Symbol ::: Type

type (:.) :: Record kvs -> Symbol -> Type
type (r :: Record kvs) :. (k :: Symbol) = Lookup kvs r k

type Lookup :: forall (kvs :: [STPair]) -> Record kvs -> Symbol -> Type
type family Lookup kvs r k where
  Lookup (k ::: _ : _) (x :+ _) k = x
  Lookup (_ : kvs) (_ :+ r) k = Lookup kvs r k

type Replace :: forall (kvs :: [STPair]) -> Record kvs -> Symbol -> Type -> Record kvs'
type family Replace kvs r k v where
  Replace (k ::: _ : _) (_ :+ vs) k v = v :+ vs
  Replace (_ : kvs) (x :+ vs) k v = x :+ Replace kvs vs k v

type family ButWith fr kvs where
  f r `ButWith` '[] = f r
  f (r :: Record kvs) `ButWith` (k ::: v : kvs') = f (Replace kvs r k v) `ButWith` kvs'

infix 9 :.
infixr 7 :::, :+

data Record (r :: [STPair]) where
  EmptyRecord :: Record '[]
  (:+) :: v -> Record kvs -> Record (k ::: v : kvs)


data User'
  (p :: Record
    [ "id" ::: Type
    , "username" ::: Type
    , "password" ::: Type
    , "birthday" ::: Type
    , "friends" ::: Type
    ]
  ) = MkUser
  { userId :: p:."id"
  , userUserName :: p:."username"
  , userPassword :: p:."password"
  , userBirthday :: p:."birthday"
  , userFriends :: p:."friends"
  }

deriving instance
  ( Show (p:."id")
  , Show (p:."username")
  , Show (p:."password")
  , Show (p:."birthday")
  , Show (p:."friends")
  ) => Show (User' p)

type User = User' (Int :+ String :+ String :+ String :+ [Int] :+ EmptyRecord)

type UserCreate = User `ButWith` '["id" ::: ()]

createUser :: UserCreate
createUser = MkUser
  { userId = ()
  , userUserName = "Bob"
  , userPassword = "secret123"
  , userBirthday = "01-01"
  , userFriends = []
  }

countUserFriends :: User `ButWith` '["friends" ::: [a]] -> Int
countUserFriends = length . userFriends

assignId :: Int -> UserCreate -> User
assignId x u = u { userId = x }

main :: IO ()
main = do
  let u0 = createUser
  let u = assignId 50 u0
  print u
  print $ countUserFriends u