能否用不同Kind的环境定义ReaderT？类型级权限追踪遇阻

Let's walk through each of your questions step by step to unpack what's happening with Haskell's kind system and type-level programming here.

Why Your Initial AppM Definition Failed #

Your first attempt:

type AppM (perms :: [*]) = ReaderT (perms :: [*]) IO

failed because ReaderT expects its first type argument to have kind * (a concrete, runtime-representable type).

Here, perms is a type-level list of types (kind [*]), not a concrete type itself. ReaderT r m a requires r to be a type that describes a value you can read (like Int, String, or a custom record)—something with kind *. Since [*] doesn't match that requirement, the compiler throws an error.

Why Wrapping with HList Works #

Your revised definition:

data HList (l :: [*]) where
  HNil :: HList '[]
  HCons :: e -> HList l -> HList (e ': l)
type AppM (perms :: [*]) = ReaderT (HList perms) IO

works because HList is a type constructor that takes a type-level list (kind [*]) and returns a concrete type (kind *).

For example, HList '[Int, String] is a valid concrete type (you can create values like HCons 42 (HCons "hello" HNil)), which fits perfectly as the r argument to ReaderT. The perms parameter is still kind [*], but we're passing HList perms (kind *) to ReaderT—that's the key difference that fixes the kind mismatch.

Fixing the PList Definition Issues #

Your goal here is to create a type-level list of Permission values, but you're running into kind mismatches because of confusion between value-level and type-level constructs. Let's fix this:

First, recall that with DataKinds, we lift the value-level Permission type to a kind Permission, and its constructors become type-level constants ('PermissionA, 'PermissionB) of kind Permission.

Your PList is meant to hold type-level lists of these lifted permissions (kind [Permission]). To connect the value level to the type level, we need to use singletons (which genSingletons generates for us):

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}

data Permission = PermissionA | PermissionB
$(genSingletons [''Permission])

data PList (perms :: [Permission]) where
  PNil :: PList '[]
  PCons :: Sing (p :: Permission) -> PList perms -> PList (p ': perms)

Why This Works: #

• Sing (p :: Permission) is a concrete type (kind *) that represents the type-level p :: Permission at the value level. For example, SPermissionA (generated by genSingletons) has type Sing 'PermissionA, which corresponds to the type-level 'PermissionA :: Permission.
• When we write p ': perms, p is a type-level constant of kind Permission, so the resulting list has kind [Permission]—exactly what PList expects as its type parameter.

Why Your Previous Attempts Failed: #

1. First PList variant: You used p as a value-level argument (type Permission, kind *), so p ': perms tried to create a list of kind [*] instead of [Permission]—mismatching PList's expected kind.
2. Second PList variant: You wrote (p :: Permission) as the argument type, but p here is a type-level entity of kind Permission, not a concrete value type (kind *). The compiler expects a value type in that position, hence the error.

If you don't need to carry value-level information (just track types), you could also use Proxy instead of singletons:

data PList (perms :: [Permission]) where
  PNil :: PList '[]
  PCons :: Proxy (p :: Permission) -> PList perms -> PList (p ': perms)

But singletons are more flexible if you need to use the permission value later in your code.

内容的提问来源于stack exchange，提问作者Saurabh Nanda