without function for Record in extensible package

without.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}


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


main :: IO ()
main = do
  let
    p1 :: Record '["n" ':> String, "a" ':> Int]
    p1 = #n @= "hoge" <: #a @= 0x20 <: nil
  out "p1" p1
  out "without #n p1" $ without #n p1
  out "without #a p1" $ without #a p1
  out "without all p1" $ without #n $ without #a p1


out :: Show a => String -> a -> IO ()
out hd x = putStrLn $ hd ++ ": " ++ show x

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 HWithout (x :: k) (xs :: [k]) (ys :: [k]) | x xs -> ys where
  hwithout :: Proxy x -> HList h xs -> HList h ys

instance HWithout x '[] '[] where
  hwithout _ HNil = HNil

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


without
  :: forall k v xs ys h.
    (HWithout (k ':> v) xs ys, Associate k v xs)
  => FieldName k -> RecordOf h xs -> RecordOf h ys
without _ =
  fromHList . hwithout (Proxy :: Proxy (k ':> v)) . toHList