AppM.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module AppM where

import Control.Monad.Reader
import Models.BillingPlan hiding (StorefrontAccess, BackofficeAccess)
import Foundation (Env(..))
import Data.Proxy
import Data.Singletons

newtype AppM (features :: [FeatureFlag]) a = AppM (ReaderT Env IO a) deriving (Functor, Applicative, Monad, MonadReader Env, MonadIO)

type family Feature (f :: FeatureFlag) (fs :: [FeatureFlag]) where
  Feature _ '[] = 'False
  Feature f (f:fs) = 'True
  Feature f (q:fs) = Feature f fs

requireFeature :: (MonadIO (m fs), Feature f fs ~ 'True) => Proxy (f :: FeatureFlag) -> m fs ()
requireFeature _ = pure ()

websiteAction :: (MonadIO (m fs), Feature 'FeatureWebsite fs ~ 'True) => m fs ()
websiteAction = requireFeature (Proxy :: Proxy 'FeatureWebsite)

bookingAction :: (MonadIO (m fs), Feature 'FeatureBookingEngine fs ~ 'True) => m fs ()
bookingAction = requireFeature (Proxy :: Proxy 'FeatureBookingEngine)

action :: (MonadIO (m fs), Feature 'FeatureBookingEngine fs ~ 'True, Feature 'FeatureWebsite fs ~ 'True) => m fs ()
action = websiteAction >> bookingAction

runAction :: forall (fs :: [FeatureFlag]) . (SingI fs) => Proxy fs -> AppM fs () -> IO ()
runAction _ _ = do
  let features :: [FeatureFlag] = fromSing (sing @fs)
  putStrLn (show features)

reply.md

@K.A.Buhr, wow! Thank you for such a detailed reply. You are correct that this is an XY problem, and you've pretty-much nailed the actual problem that I'm trying to solve. Another important piece of context is that, at some point these type-level permissions will have to be "reified" at the value-level. This is because the final check is against the permissions granted to the currently signed-in user, which are stored in the DB.

Taking this into account, I'm planning to have two "general" functions, say:

requiredPermission :: (RequiredPermission p ps) => Proxy p -> AppM ps () 

optionalPermission :: (OptionalPermission p ps) => Proxy p -> AppM ps ()

Here's the difference:

• requiredPermission will simply add the permission to the type-level list and it will be verified when runAppM is called. If the current user does not have ALL the required permissions, then runAppM will immediately throw a 401 error to the UI.
• On the other hand, optionalPermission will extract the user from the Reader environment, check the permission, and return a True / False. runAppM will do nothing with OptionalPermissions. These will be for cases where the absence of a permission should NOT fail the entire action, but skip a specific step in the action.

Given this context, I'm not sure if I would end-up with functions, like grantA or grantB. The "unwrapping" of ALL the RequestPermissions in the AppM constructor will be done by runAppM, which will also ensure that the currently sign-in user actually has these permissions.

Also, are ConstraintKinds something that I should look at, to make writing these type signatures easier? For example:

type HasRequiredPermissions p ps = RequiredPermission p ps ~ True

RequiredPermission.hs

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

module Try2 where


import Control.Monad.Reader
import Data.Singletons
import Data.Singletons.TH

data Permission = PermissionA
                | PermissionB

$(genSingletons [''Permission])

data Env = Env
type AppM (ps :: [Permission]) = ReaderT Env IO

type family RequiredPermission (p :: Permission) ps where
  RequiredPermission p '[] = 'False
  RequiredPermission p (p:ps) = 'True
  RequiredPermission p (q:ps) = RequiredPermission p ps

requiredPermission :: (RequiredPermission p ps ~ 'True) => Proxy p -> AppM ps ()
requiredPermission _ = pure ()

foo = do
  requiredPermission (Proxy :: Proxy 'PermissionA)
  pure (1 :: Int)


-- /Users/saurabhnanda/projects/vl-gitlab/haskell/src/Try2.hs:37:3: error:
--     • Couldn't match type ‘RequiredPermission 'PermissionA ps0’
--                      with ‘'True’
--         arising from a use of ‘requiredPermission’
--       The type variable ‘ps0’ is ambiguous
--     • In a stmt of a 'do' block:
--         requiredPermission (Proxy :: Proxy  'PermissionA)
--       In the expression:
--         do requiredPermission (Proxy :: Proxy  'PermissionA)
--            pure (1 :: Int)
--       In an equation for ‘foo’:
--           foo
--             = do requiredPermission (Proxy :: Proxy  'PermissionA)
--                  pure (1 :: Int)
--    |
-- 37 |   requiredPermission (Proxy :: Proxy 'PermissionA)
--    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Try2.hs

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}

module Try2 where


import Control.Monad.Reader
import Data.Singletons
import Data.Singletons.TH

data Permission = PermissionA
                | PermissionB

$(genSingletons [''Permission])

data Env = Env
type AppM (ps :: [Permission]) = ReaderT Env IO

type family RequiredPermission (p :: Permission) ps where
  RequiredPermission p '[] = 'False
  RequiredPermission p (p:ps) = 'True
  RequiredPermission p (q:ps) = RequiredPermission p ps

requiredPermission :: (RequiredPermission 'PermissionA ps ~ True) => AppM ps ()
requiredPermission = pure ()

requiredPermission' :: (RequiredPermission p ps ~ True) => Proxy p -> AppM ps ()
requiredPermission' = pure ()

-- /Users/saurabhnanda/projects/vl-gitlab/haskell/src/Try2.hs:32:23: error:
--     • Could not deduce: RequiredPermission 'PermissionA ps0 ~ 'True
--       from the context: RequiredPermission 'PermissionA ps ~ 'True
--         bound by the type signature for:
--                    requiredPermission :: forall (ps :: [Permission]).
--                                          (RequiredPermission 'PermissionA ps ~ 'True) =>
--                                          AppM ps ()
--         at /Users/saurabhnanda/projects/vl-gitlab/haskell/src/Try2.hs:32:23-79
--       The type variable ‘ps0’ is ambiguous
--     • In the ambiguity check for ‘requiredPermission’
--       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
--       In the type signature:
--         requiredPermission :: (RequiredPermission  'PermissionA ps
--                                ~ True) =>
--                               AppM ps ()
--    |
-- 32 | requiredPermission :: (RequiredPermission 'PermissionA ps ~ True) => AppM ps ()
--    |                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

-- /Users/saurabhnanda/projects/vl-gitlab/haskell/src/Try2.hs:35:24: error:
--     • Could not deduce: RequiredPermission p ps0 ~ 'True
--       from the context: RequiredPermission p ps ~ 'True
--         bound by the type signature for:
--                    requiredPermission' :: forall (p :: Permission) (ps :: [Permission]).
--                                           (RequiredPermission p ps ~ 'True) =>
--                                           Proxy p -> AppM ps ()
--         at /Users/saurabhnanda/projects/vl-gitlab/haskell/src/Try2.hs:35:24-80
--       The type variable ‘ps0’ is ambiguous
--     • In the ambiguity check for ‘requiredPermission'’
--       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
--       In the type signature:
--         requiredPermission' :: (RequiredPermission p ps ~ True) =>
--                                Proxy p -> AppM ps ()
--    |
-- 35 | requiredPermission' :: (RequiredPermission p ps ~ True) => Proxy p -> AppM ps ()
--    |                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-- Failed, no modules loaded.