如何编写签名为(Proxy a -> s) -> Proxy (Maybe a) -> Maybe s的函数

核心问题在于：Proxy (Maybe a)本身无法提供KnownSymbol a的类型约束，Haskell静态类型系统无法自动推导a满足该约束，因此需要通过类型反射或显式约束检查来实现函数g。

方案一：借助reflection库实现 #

启用必要的GHC扩展，利用Given类型类传递约束：

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

import GHC.TypeLits (KnownSymbol, symbolVal)
import Data.Proxy (Proxy(..))
import Data.Reflection (reifyGiven, Given(..))

g :: forall a s. (Given (KnownSymbol a) => s) -> Proxy (Maybe a) -> Maybe s
g f _ = reifyGiven (Just f) Nothing

使用时传入symbolVal (Proxy :: Proxy a)作为第一个参数：当a具有KnownSymbol实例时，函数返回Just (symbolVal Proxy)；否则返回Nothing。

方案二：通过Typeable做类型实例检查 #

利用Typeable的类型相等性判断，间接验证a是否存在KnownSymbol实例：

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleContexts #-}

import GHC.TypeLits (KnownSymbol, symbolVal)
import Data.Proxy (Proxy(..))
import Data.Typeable (Typeable, eqT)

g :: forall a s. (Typeable a, s ~ String) => (Proxy a -> s) -> Proxy (Maybe a) -> Maybe s
g f _ = case eqT @(KnownSymbol a) @(KnownSymbol a) of
    Just Refl -> Just $ f (Proxy :: Proxy a)
    Nothing -> Nothing

eqT会在编译时检查KnownSymbol a实例是否存在，存在则返回Just Refl，此时可安全调用f；否则返回Nothing。

关键原因 #

KnownSymbol是约束a的类型类，而非Maybe a的——Maybe a本身没有对应的KnownSymbol实例，也无法自动从a的实例推导而来。因此必须通过反射机制，在编译时验证a的约束是否存在，再决定返回Just或Nothing。

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