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

import GHC.Types

data STPair = forall v. Symbol ::: v

type (r :: Record kvs) :. k = Lookup kvs r k

type Lookup :: forall (kvs :: [STPair]) -> Record kvs -> Symbol -> v
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 -> v -> 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 ReplaceAll fields r kvs where
  ReplaceAll _ r '[] = r
  ReplaceAll fields r (k ::: v : kvs) = Replace fields (ReplaceAll fields r kvs) k v

type family ButWith fr kvs where
  f (r :: Record fields) `ButWith` kvs = f (ReplaceAll fields r kvs)

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

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

type UninitRecord :: forall (kvs :: [STPair]) -> Record kvs
type family UninitRecord kvs where
  UninitRecord '[] = EmptyRecord
  UninitRecord (k ::: _ : kvs) = Undefined :+ UninitRecord kvs

type Undefined :: a
type family Undefined where

type Uninitialized (f :: Record fields -> Type) = f (UninitRecord fields)

type Substitute (r :: Record fields) kvs r' =
  (DoSubstitute fields fields r kvs r', r' ~ ReplaceAll fields r kvs)

type family DoSubstitute fields fields0 r kvs r' where
  DoSubstitute '[] _ _ _ _ = () :: Constraint
  DoSubstitute (field ::: a : fields) fields0 r kvs r' =
    ( ReplaceOrPreserve kvs field a fields0 r r'
    , DoSubstitute fields fields0 r kvs r'
    )

type family ReplaceOrPreserve kvs k a fields r r' where
  ReplaceOrPreserve '[] k a fields r r' = Lookup @a fields r k ~ Lookup @a fields r' k
  ReplaceOrPreserve (k ::: v : _) k a fields _ r' = v ~ Lookup @a fields r' k
  ReplaceOrPreserve (_ ::: _ : kvs) k a fields r r' = ReplaceOrPreserve kvs k a fields r r'


data User'
  (p :: Record
    [ "username" ::: Type
    , "id" ::: 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 = Uninitialized User' `ButWith`
  [ "id" ::: Int
  , "friends" ::: [Int]
  , "username" ::: String
  , "birthday" ::: String
  , "password" ::: String
  ]

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

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

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

assignId :: Substitute r '[ "id" ::: Int ] r' => Int -> User' r -> User' r'
assignId x u = u { userId = x }


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