Невозможно преобразовать список на уровне типов обратно в уровень значений с помощью библиотеки синглетонов.

Я пытаюсь написать разумно систему авторизации со статической проверкой [1], и в настоящее время пытаюсь написать функцию, которая будет извлекать необходимые разрешения из аннотации/фантома на уровне типа для значения -уровень.

{-# LANGUAGE DataKinds, GADTs, ScopedTypeVariables #-}

module Try5 where

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


data Permission = PermA
                | PermB
                deriving (Eq, Show)
$(genSingletons [''Permission])

data Env = Env

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

-- other functions for constructing an action in `AppM perms`
-- have been removed for brevity

runAction :: AppM (perms :: [Permission]) () -> IO ()
runAction _ = do
  let permissions :: [Permission] = fromSing $ singByProxy (Proxy :: Proxy (perms :: [Permission]))
  putStrLn $ "Huzzah, I freed the permissions from the type-level cage: " <> (show permissions)
  pure ()

Ошибка:

    • Ambiguous type variable ‘a0’ arising from a use of ‘singByProxy’
      prevents the constraint ‘(SingI a0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instances exist:
        instance forall a (n1 :: a) (n2 :: [a]).
                 (SingI n1, SingI n2) =>
                 SingI (n1 : n2)
          -- Defined in ‘singletons-2.4.1:Data.Singletons.Prelude.Instances’
        instance SingI '[]
          -- Defined in ‘singletons-2.4.1:Data.Singletons.Prelude.Instances’
    • In the second argument of ‘($)’, namely
        ‘singByProxy (Proxy :: Proxy (perms :: [Permission]))’
      In the expression:
        fromSing $ singByProxy (Proxy :: Proxy (perms :: [Permission]))
      In a pattern binding:
        permissions :: [Permission]
          = fromSing $ singByProxy (Proxy :: Proxy (perms :: [Permission]))
   |
24 |   let permissions :: [Permission] = fromSing $ singByProxy (Proxy :: Proxy (perms :: [Permission]))
   |                                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[1] Дополнительный контекст можно найти по адресу https://stackoverflow.com/a/56828016/534481.