Permissions.hs

{-# LANGUAGE TypeApplications, UndecidableInstances, ConstraintKinds, ExistentialQuantification, DataKinds, ScopedTypeVariables, TypeFamilies, TypeOperators #-}

module Rights where

import Data.Kind
import Data.List
import Data.Coerce
import Data.Proxy
import GHC.TypeLits

data Right =
    CreatePortal
  | InviteUser
  | EditArticle
  deriving (Eq)

newtype SRight (right :: Right) = SRight Right

class KnownRight (a :: Right) where
  rightSing :: SRight a

instance KnownRight CreatePortal where
  rightSing = SRight CreatePortal

instance KnownRight InviteUser where
  rightSing = SRight InviteUser

instance KnownRight EditArticle where
  rightSing = SRight EditArticle

knownRight :: forall right proxy. KnownRight right => proxy right -> Right
knownRight _ =
  case rightSing :: SRight right of
    SRight x -> x

type family HasRight (right :: Right) (rights :: [Right]) :: Constraint where
  HasRight r '[] = TypeError (Text "Insufficient permission: " :<>: ShowType r)
  HasRight r (r ': rx) = ()
  HasRight r (x ': rx) = HasRight r rx

data User (rights :: [Right]) = User [Right]

data SomeUser = forall rights. SomeUser (User rights)

newtype SRights (rights :: [Right]) =
  SRights [Right]

class KnownRights (rights :: [Right]) where
  rightsSing :: SRights rights

instance KnownRights '[] where
  rightsSing = SRights []

instance
  ( KnownRight right
  , KnownRights rights
  ) => KnownRights (right ': rights) where
  rightsSing =
    case rightSing :: SRight right of
      SRight right ->
        case rightsSing :: SRights rights of
          SRights rights -> SRights (right:rights)

authenticate
  :: forall
      (desiredRights :: [Right])
      (assignedRights :: [Right])
  . KnownRights desiredRights
  => User assignedRights
  -> Maybe (User desiredRights)
authenticate user@(User userRights)
  | null (expectedRights \\ userRights) = Just (coerce user)
  | otherwise = Nothing
  where
    expectedRights =
      case rightsSing :: SRights desiredRights of
        SRights rights -> rights

type PermittedToDoAdminStuff rights =
  ( HasRight 'CreatePortal rights
  , HasRight 'InviteUser rights
  )

someVeryImportantAction
  :: ( HasRight 'CreatePortal rights
     , HasRight 'InviteUser rights
     )
  => User rights
  -> IO ()
someVeryImportantAction _ = putStrLn "admin stuff"

someOtherImportantAction
  :: (HasRight 'EditArticle rights)
  => User rights
  -> IO ()
someOtherImportantAction _ = putStrLn "some other admin stuff"

someLogic :: User rights -> IO ()
someLogic uncheckedUser = do
  -- will result in a compile error
  -- someVeryImportantAction uncheckedUser
  -- someVeryImportantAction user
  let
    mauthenticatedUser =
      authenticate @'[CreatePortal, InviteUser] uncheckedUser

  case mauthenticatedUser of
    Just user -> do
      someVeryImportantAction user
      --someOtherImportantAction user
    Nothing   -> print "Not authenticated"
  return ()