Couldn't match kind '*' with 'Nat'

Question

I'm trying to create a type that guarantees that a string is less than N characters long.

{-# 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 the 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 don't understand this error. Why doesn't it work? I've used almost this exact same code to get the natVal of n in other places and it works.

Is there a better way to do this?

Rifleman

Side remark: by turning on the PolyKinds extension, ghc is more lenient with the idea of a poly-kinded Proxy and the error message becomes different and makes it a lot clearer that it's a typical ScopedTypeVariables issue. – Belvia

Answer 1

You need an explicit forall in the signature of textMax, so that ScopedTypeVariables kicks in and the 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

Causation