Without.hs

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

module Data.Without
  ( Without (..)
  ) where

import           Data.Extensible.HList
import           Data.Proxy
import           Data.Type.Equality    (type (==))


class HEq (x :: k) (y :: k) (b :: Bool) | x y -> b
instance ((Proxy x == Proxy y) ~ b) => HEq x y b

class ConsFalse (b :: Bool) (x :: k) (xs :: [k]) (r :: [k]) | b x xs -> r, r b -> xs, x xs r -> b where
  hconsFalse :: Proxy b -> h x -> HList h xs -> HList h r

instance ConsFalse False x xs (x ': xs) where
  hconsFalse _ = HCons

instance ConsFalse True x xs xs where
  hconsFalse _ _ = id


class Without x xs ys | x xs -> ys where
  without :: Proxy x -> HList h xs -> HList h ys

instance Without x '[] '[] where
  without _ HNil = HNil

instance (HEq x y b, ConsFalse b x ys zs, Without y xs ys) => Without y (x ': xs) zs where
  without p (HCons x xs) = hconsFalse (Proxy :: Proxy b) x (without p xs)