Failed to combine the good '*' with 'Nat'

Question

I am trying to create a type that ensures that the string is less than N characters.

{-# 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 

This gives an error:

 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 do not understand this error. Why is this not working? I used almost this exact code to get natVal n elsewhere and it works .

Is there a better way to do this?

Answer 1

You will need an explicit forall in the textMax signature, so that ScopedTypeVariables starts, and n in the Proxy n annotation becomes the same n in the KnownNat n constraint:

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