{-#GADTs,KindSignatures,ScopedTypeVariables,TypeOperators,PolyKinds,RankNTypes#-}


data Tuple :: [Type] -> Type where
  TNil :: Tuple '[]
  TCons :: a -> Tuple l -> Tuple (a:l)

data EncodingType' = FinType'|ConstrType'

data EncodingType :: EncodingType' -> Type where
  ConstrType :: [Type] ->EncodingType ConstrType'
  ConstrSumType :: EncodingType ConstrType' -> EncodingType ConstrType' -> EncodingType ConstrType'
  FinType :: EncodingType ConstrType' -> EncodingType FinType'

data Encoding :: forall (p :: EncodingType').(EncodingType p) -> (Type -> Type -> Type) -> Type -> Type where
  Constr :: a (Tuple l) t -> Encoding (ConstrType l) a t
  ConstrSum :: Encoding (ConstrType c1) a t-> Encoding (ConstrType c2) a t-> Encoding (ConstrSumType (ConstrType c1) (ConstrType c2)) a t
  Fin :: forall (a :: Type -> Type -> Type) (t :: Type) (l :: EncodingType ConstrType').a (Encoding l a t) t -> Encoding (FinType l) a t



{-examples-}
type ArrId a b = forall id.Encoding (FinType (ConstrType '[b])) a id
type ArrPair a b c = forall pair.Encoding (FinType (ConstrType '[b,c])) a pair
type ArrEither a e b = forall either.Encoding (FinType (ConstrSumType (ConstrType '[e]) (ConstrType '[b]))) a either