無法與'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。

有沒有更好的方法來做到這一點？

來源

2016-11-21 Sean Clark Hess

方備註：通過打開' PolyKinds'的擴展，ghc比poly-kinded'Proxy'更加寬鬆，並且錯誤信息變得不同，並且使得它更加清晰，它是一個典型的'ScopedTypeVariables'問題。 – gallais

您在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

來源

2016-11-21 23:30:28 duplode

無法與'Nat'匹配'Nat'

回答

相關問題