module Data.HList ( Has, HasAll, getH, HList (..), singletonH, ReassembleHList, reassemble, ) where import Data.Kind import GHC.TypeLits data HList (xs :: [Type]) where HNil :: HList '[] HCons :: x -> HList xs -> HList (x ': xs) infixr 5 `HCons` type family HasAll xs ys :: Constraint where HasAll '[] _ = () HasAll (x ': xs) ys = (Has x ys, HasAll xs ys) type Has x xs = Has' x xs (HeadEq x xs) type family HeadEq x xs where HeadEq x (x ': _) = 'True HeadEq _ _ = 'False class t ~ HeadEq x xs => Has' (x :: Type) (xs :: [Type]) (t :: Bool) where getH :: HList xs -> x instance Has' x (x ': xs) 'True where getH :: HList (x : xs) -> x getH (HCons x x HList xs _) = x x x {-# INLINE getH #-} instance (Has' x xs t, HeadEq x (y : xs) ~ 'False) => Has' x (y ': xs) 'False where getH :: HList (y : xs) -> x getH (HCons x _ HList xs xs) = HList xs -> x forall x (xs :: [*]) (t :: Bool). Has' x xs t => HList xs -> x getH HList xs xs {-# INLINE getH #-} instance TypeError ( 'ShowType x ':<>: 'Text " is not a part of the list.") => Has' x '[] 'False where getH :: HList '[] -> x getH HList '[] HNil = x forall a. HasCallStack => a undefined {-# INLINE getH #-} singletonH :: a -> HList '[a] singletonH :: a -> HList '[a] singletonH a a = a a a -> HList '[] -> HList '[a] forall x (xs :: [*]). x -> HList xs -> HList (x : xs) `HCons` HList '[] HNil {-# INLINE singletonH #-} instance Eq (HList '[]) where HList '[] HNil == :: HList '[] -> HList '[] -> Bool == HList '[] HNil = Bool True instance (Eq x, Eq (HList xs)) => Eq (HList (x ': xs)) where (HCons x x HList xs xs) == :: HList (x : xs) -> HList (x : xs) -> Bool == (HCons x y HList xs ys) = x x x -> x -> Bool forall a. Eq a => a -> a -> Bool == x x y Bool -> Bool -> Bool && HList xs xs HList xs -> HList xs -> Bool forall a. Eq a => a -> a -> Bool == HList xs HList xs ys type family (==) a b :: Bool where a == a = 'True _ == _ = 'False type ReassembleHList xs ys = ReassembleHList' xs ys (xs == ys) class f ~ (xs == ys) => ReassembleHList' xs ys f where reassemble :: HList xs -> HList ys instance ReassembleHList' xs xs 'True where reassemble :: HList xs -> HList xs reassemble = HList xs -> HList xs forall a. a -> a id {-# INLINE reassemble #-} instance ReassembleHList' (x ': xs) '[] 'False where reassemble :: HList (x : xs) -> HList '[] reassemble HList (x : xs) _ = HList '[] HNil {-# INLINE reassemble #-} instance (Has y xs, ReassembleHList' xs ys f, (xs == (y ': ys)) ~ 'False) => ReassembleHList' xs (y ': ys) 'False where reassemble :: HList xs -> HList (y : ys) reassemble HList xs xs = HList xs -> y forall x (xs :: [*]) (t :: Bool). Has' x xs t => HList xs -> x getH @y HList xs xs y -> HList ys -> HList (y : ys) forall x (xs :: [*]). x -> HList xs -> HList (x : xs) `HCons` HList xs -> HList ys forall (xs :: [*]) (ys :: [*]) (f :: Bool). ReassembleHList' xs ys f => HList xs -> HList ys reassemble HList xs xs {-# INLINE reassemble #-}