{-# LANGUAGE DataKinds
           , GADTs
           , PolyKinds
           , RankNTypes
           , ScopedTypeVariables
           , TypeApplications
           , TypeFamilies
           , TypeOperators
           , UndecidableInstances
           , RequiredTypeArguments
  #-}

import GHC.TypeNats
import Data.Kind (Type)
import Numeric.Natural

main :: IO ()
main = putStrLn "This isn't an app."


type family Nth (n :: Natural) (ts :: [k]) where
    Nth 0 (t : ts') = t
    Nth n (t : ts') = Nth (n - 1) ts'

data NatTagged (n :: Natural) a where
    N :: (KnownNat n)=> a -> NatTagged n a

data NS (m :: k -> Type) (ts :: [k]) where
    MkNS :: (Nth n ts ~ t)=> NatTagged n (m t) -> NS m ts

mkNS :: forall k (ts :: [k]) (t :: k) (m :: k -> Type). forall n -> KnownNat n =>
    (Nth n ts ~ t)=> m t -> NS m ts
mkNS n mt = MkNS (N @n mt)