[SOLVED] Expected a type, but ‘i’ has kind ‘Nat’

Expected a type, but ‘i’ has kind ‘Nat’

I want to implement simple propositional logic with type-bounded size of the interpretation. But somhow I fail to convert type-level numbers to values using natVal. Sample code:

import GHC.TypeLits
import Data.Proxy

newtype PropositionalVariable (interpretationSize) = PropositionalVariable {
  getVariable :: Int
} deriving (Show, Eq)

instance KnownNat i => Enum (PropositionalVariable i) where
  fromEnum = getVariable
  toEnum e | e <= 0 = error "Variable must be positive integer"
           | (toInteger e) > (natVal (Proxy :: Proxy i)) = error "Variable index overflow"
           | otherwise = PropositionalVariable e

Gives me errors like:

• Expected a type, but ‘i’ has kind ‘Nat’
• In the first argument of ‘PropositionalVariable’, namely ‘i’
  In the first argument of ‘Enum’, namely ‘PropositionalVariable i’
  In the instance declaration for ‘Enum (PropositionalVariable i)’

What is the correct way to convert types level integers to values in this case?

Solution

You need to turn on PolyKinds extension or give interpretationSize a kind annotation.