content: -- https://github.com/ucsd-progsys/liquidhaskell/issues/1473
  
  {-# LANGUAGE GADTs, TypeFamilies, GeneralizedNewtypeDeriving, OverloadedStrings, TemplateHaskell, QuasiQuotes, MultiParamTypeClasses #-}
  
  {-@ LIQUID "--reflection"     @-}
  {-@ LIQUID "--no-adt"         @-}
  {-  LIQUID "--no-termination" @-}
  
  -- | Description of database records.
  module T1473B
    ( User, UserId
    , EntityField(..)
    , Projectable(..)
    ) where
  
  data Entity record = Entity (Key record) record
  
  {-@ reflect entityKey @-}
  entityKey :: Entity record -> Key record
  entityKey (Entity k _) = k
  
  {-@ reflect entityVal @-}
  entityVal :: Entity record -> record
  entityVal (Entity _ v) = v
  
  {-@
  data User = User
    { userName :: String
    , userFriend :: UserId
    , userSsn :: Int
    }
  @-}
  
  {-@ data EntityField User field <q :: Entity User -> Entity User -> Bool> where
          UserId     :: EntityField <{\row v -> entityKey v = entityKey row}>              User {v:_ | True}
          UserName :: EntityField <{\row v -> entityKey v = userFriend (entityVal row)}>   User {v:_ | True}
          UserFriend :: EntityField <{\row v -> entityKey v = userFriend (entityVal row)}> User {v:_ | True}
          UserSsn :: EntityField <{\row v -> entityKey v = entityKey row}>                 User {v:_ | True}
    @-}
  {-@ data variance EntityField covariant covariant contravariant @-}
  
  -- Everything past this point should be generated by TH:
  data User = User
    { userName :: String
    , userFriend :: UserId
    , userSsn :: Int
    }
  
  class PersistEntity record where
    data Key record
    data EntityField record :: * -> *
  
  type UserId = Key User
  
  instance PersistEntity User where
    data Key User = UserKey Int
  
    data EntityField User field where
      UserId :: EntityField User UserId
      UserName :: EntityField User String
      UserFriend :: EntityField User UserId
      UserSsn :: EntityField User Int
  
  class PersistEntity a => Projectable a where
    project :: EntityField a field -> Entity a -> field
  
  instance Projectable User where
    project UserId = entityKey
    project UserName = userName . entityVal
    project UserFriend = userFriend . entityVal
    project UserSsn = userSsn . entityVal
  