content: {-# LANGUAGE GADTs, TypeFamilies, GeneralizedNewtypeDeriving, OverloadedStrings, TemplateHaskell, QuasiQuotes, MultiParamTypeClasses #-}
  
  {-@ LIQUID "--no-adt"                   @-}
  {-@ LIQUID "--exact-data-cons"           @-}
  {-@ LIQUID "--higherorder"              @-}
  {-@ LIQUID "--no-termination" @-}
  -- | Description of database records.
  module T1476
    ( User, UserId
    , EntityField(..)
    ) 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 -> True}> 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
  
  project :: EntityField User field -> Entity User -> field
  project UserId x = entityKey x
  project UserName x = userName . entityVal $ x
  project UserFriend x = userFriend . entityVal $ x
  project UserSsn x = userSsn . entityVal $ x
  
  