{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
module T24 where
import GHC.TypeNats (type (-))
data Proxy a = Stop | Next (Proxy a)

type family LongP n a where
  LongP 0 a = a
  LongP n a = Next (LongP (n - 1) a)

-- >>> :kind! ((LongP 10 Stop) :: Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy Double)))))))))))))