{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.HeteroParList.Constrained where

import Data.Kind

data PL c (t :: k -> Type) (ss :: [k]) where
	Nil :: PL c t '[]
	(:^*) :: c s => t s -> PL c t ss -> PL c t (s ': ss)

instance Show (PL c t '[]) where show :: PL c t '[] -> String
show PL c t '[]
Nil = String
"Nil"

instance (Show (t s), Show (PL c t ss)) =>
	Show (PL c t (s ': ss)) where
	show :: PL c t (s : ss) -> String
show (t s
x :^* PL c t ss
xs) = t s -> String
forall a. Show a => a -> String
show t s
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :^* " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PL c t ss -> String
forall a. Show a => a -> String
show PL c t ss
xs

null :: PL c t ss -> Bool
null :: forall {k} (c :: k -> Constraint) (t :: k -> *) (ss :: [k]).
PL c t ss -> Bool
null = \case PL c t ss
Nil -> Bool
True; t s
_ :^* PL c t ss
_ -> Bool
False