{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures, GADTs,  TypeOperators
  #-}

module T6035 where

import Data.Kind (Type)

data Nat = Zero | Succ Nat

type family Sing (a :: k) :: k -> Type

data SNat n where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)

data SList (a :: [k]) where
  SNil :: SList '[]
  SCons :: Sing h h -> SList t -> SList (h ': t)

type instance Sing (a :: Nat) = SNat
type instance Sing (a :: [k]) = SList

nil :: SList '[]
nil = SNil

zero :: SList '[ '[] ]
zero = SCons SNil SNil

term :: SList '[ '[Zero], '[]]
term = SCons (SCons SZero SNil) (SCons SNil SNil)