haskell - 无法将种类 '*' 与 'Nat' 匹配

Question

我正在尝试创建一种保证字符串长度小于 N 个字符的类型。

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DataKinds #-}

import GHC.TypeLits (Symbol, Nat, KnownNat, natVal, KnownSymbol, symbolVal)
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Proxy (Proxy(..))

data TextMax (n :: Nat) = TextMax Text
  deriving (Show)

textMax :: KnownNat n => Text -> Maybe (TextMax n)
textMax t
  | Text.length t <= (fromIntegral $ natVal (Proxy :: Proxy n)) = Just (TextMax t)
  | otherwise = Nothing

这给出了错误：

src/Simple/Reporting/Metro2/TextMax.hs:18:50: error:
• Couldn't match kind ‘*’ with ‘Nat’
  When matching the kind of ‘Proxy’
• In the first argument of ‘natVal’, namely ‘(Proxy :: Proxy n)’
  In the second argument of ‘($)’, namely ‘natVal (Proxy :: Proxy n)’
  In the second argument of ‘(<=)’, namely
    ‘(fromIntegral $ natVal (Proxy :: Proxy n))’

我不明白这个错误。为什么它不起作用？我已经使用几乎完全相同的代码在其他地方获取 n 的 natVal 并且它可以工作。

有一个更好的方法吗？

Answer 1

您需要forall在 的签名中显式textMax，以便ScopedTypeVariables启动并且注释中的 约束在约束n中Proxy n变得相同：nKnownNat n

textMax :: forall n. KnownNat n => Text -> Maybe (TextMax n)
textMax t
  | Text.length t <= (fromIntegral $ natVal (Proxy :: Proxy n)) = Just (TextMax t)
  | otherwise = Nothing