Closed kinds aren't as closed as you'd think

Closed.hs

{-# language PolyKinds, DataKinds, RankNTypes, TypeApplications, ScopedTypeVariables, TypeFamilies, FlexibleInstances #-}

import Data.Proxy

class KnownUnit (k :: ()) where
   reflect :: Proxy k -> Int

instance KnownUnit '() where
  reflect _ = 0

instance KnownUnit x => KnownUnit (f x) where
  reflect _ = 1 + reflect (Proxy :: Proxy x)

type family Succ :: k -> k

reify :: Int -> (forall k. KnownUnit k => Proxy k -> r) -> r
reify 0 f = f (Proxy :: Proxy '())
reify n f = reify (n - 1) $ \(Proxy :: Proxy k) -> f (Proxy :: Proxy (Succ k))

-- ghci> reify 23 reflect
-- 23

Here's a reexposition of Edwad's example using type applications.