无法与'Nat'匹配'Nat'
问题描述:
我试图创建一个类型来保证字符串的长度小于N个字符。无法与'Nat'匹配'Nat'
{-# 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))’
我不明白这个错误。为什么它不起作用? I've used almost this exact same code to get the natVal of n in other places and it works。
有没有更好的方法来做到这一点?
答
您在textMax
签名需要一个明确的forall
,使ScopedTypeVariables
踢和在Proxy n
注释的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
方备注:通过打开' PolyKinds'的扩展,ghc比poly-kinded'Proxy'更加宽松,并且错误信息变得不同,并且使得它更加清晰,它是一个典型的'ScopedTypeVariables'问题。 – gallais