Nats.hs

{-# LANGUAGE
    ExistentialQuantification,
    RankNTypes,
    KindSignatures,
    TypeApplications,
    TypeInType,
    ScopedTypeVariables,
    TypeFamilyDependencies,
    AllowAmbiguousTypes
#-}
module Main where

import Data.Kind

data N = Z | S N

class KnownN (n :: N) where
    knownN :: Int

instance KnownN 'Z where
    knownN = 0

instance KnownN n => KnownN ('S n) where
    knownN = knownN @n + 1

type family Pow1 (n :: N) = (p :: Type) | p -> n where
  Pow1 'Z = ()
  Pow1 ('S n) = ((), Pow1 n)

data Ser1 = forall (n :: N). KnownN n => Ser1 (Pow1 n)

p0 :: Pow1 'Z
p0 = ()

ser :: Ser1
ser = Ser1 p0

withPow :: forall r. Int -> (forall n. KnownN n => Pow1 n -> r) -> r
withPow 0 f = f ()
withPow k f  = withPow (k - 1) (\p -> f ((), p))

intToSer1 :: Int -> Ser1
intToSer1 i = withPow i Ser1

powLevels :: forall n. KnownN n => Pow1 n -> Int
powLevels _ = knownN @n

ser1ToInt :: Ser1 -> Int
ser1ToInt (Ser1 p) = powLevels p

main :: IO ()
main = do
    putStrLn $ show $ withPow 5 powLevels

Have you tried passing powLevels to withPow?

Yup, it works. I've updated it so you can compile and run it with GHC.