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 #-}