{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

module T where

data N = Z | S N

type family Dec (n :: N) :: N where
  Dec Z = Z
  Dec (S n) = n

type family OnZ (n :: N) (x :: k) (y :: k) :: k where
  OnZ Z x _ = x
  OnZ (S _) _ y = y

type Next t n a = (OnZ n a (t (Dec n) a))

data T (n :: N) a = T
  (Next T n a)
  (Next T n a)
  (Next T n a)
  (Next T n a)

type TZ = T Z
type T1 = T (S Z)
type T2 = T (S (S Z))
type T3 = T (S (S (S Z)))

instance Functor (T Z) where
  fmap f (T x1 x2 x3 x4) = T (f x1) (f x2) (f x3) (f x4)

instance Functor (T n) => Functor (T (S n)) where
  fmap f (T x1 x2 x3 x4) = T (fmap f x1) (fmap f x2) (fmap f x3) (fmap f x4)