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

I see TypeApplications is enabled, but it looks like you don’t use the extension at all, and instead use Proxy. Did you start by using @ and then determine it didn’t work, or is Proxy less obscure, or am I just confused, or what?

I see TypeApplications is enabled, but it looks like you don’t use the extension at all, and instead use Proxy. Did you start by using @ and then determine it didn’t work, or is Proxy less obscure, or am I just confused, or what?

I did. I was going to write it TypeApplications style, then forgot. =)

I did. I was going to write it TypeApplications style, then forgot. =)

I mentioned it in the tweet that originally linked here, but the technique that I used here is originally due to aarvar.

I mentioned it in the tweet that originally linked here, but the technique that I used here is originally due to aarvar.

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

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