无法将'*'与'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注释变成相同n的KnownNat 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