T1473B.hs

-- 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 Model
  ( 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