haskell - 约束 Haskell 中类型级列表的元素

Question

我正在尝试编写一个类型族，我可以用它来约束类型级别列表的元素。我有这段代码:

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, TypeFamilies #-}

import GHC.TypeLits (KnownSymbol, symbolVal)
import GHC.Exts (Constraint)
import Data.Proxy (Proxy(..))

type family AllHave (c :: k -> Constraint) (xs :: [k]) :: Constraint
type instance AllHave c '[] = ()
type instance AllHave c (x ': xs) = (c x, AllHave c xs)

type family Head (xs :: [k]) :: k where
    Head (x ': xs) = x

headProxy :: proxy xs -> Proxy (Head xs)
headProxy _ = Proxy

test :: AllHave KnownSymbol xs => proxy xs -> String
test p = symbolVal (headProxy p)

main :: IO ()
main = putStrLn $ test (Proxy :: Proxy '["a", "b"])

根据我的理解，这应该可行，但是当我编译 ghc 时会吐出这个:

Test.hs:18:10:
    Could not deduce (KnownSymbol (Head xs))
      arising from a use of ‘symbolVal’
    from the context (AllHave KnownSymbol xs)
      bound by the type signature for
                 test :: AllHave KnownSymbol xs => proxy xs -> String
      at Test.hs:17:9-52
    In the expression: symbolVal (headProxy p)
    In an equation for ‘test’: test p = symbolVal (headProxy p)

Answer 1

这里的问题是当在 test 中输入 xs 时 Head 不会减少，因此 Haskell 无法推断出 KnownSymbol ( Head xs) 来自 AllHave KnownSymbol xs。它不应该:如果 xs 为空应该怎么办？

要解决这个问题，你可以像这样显式地声明xs不为空:

test :: AllHave KnownSymbol (x ': xs) => proxy (x ': xs) -> String