{-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Fcf.Data.Vinyl (rappend) where import qualified Data.Vinyl as V import Fcf rappend :: V.Rec f as -> V.Rec f bs -> V.Rec f (Eval (as ++ bs)) rappend :: Rec f as -> Rec f bs -> Rec f (Eval (as ++ bs)) rappend Rec f as V.RNil Rec f bs ys = Rec f bs Rec f (Eval (as ++ bs)) ys rappend (f r x V.:& Rec f rs xs) Rec f bs ys = f r x f r -> Rec f (rs <> bs) -> Rec f (r : (rs <> bs)) forall u (a :: u -> *) (r :: u) (rs :: [u]). a r -> Rec a rs -> Rec a (r : rs) V.:& (Rec f rs xs Rec f rs -> Rec f bs -> Rec f (Eval (rs ++ bs)) forall a (f :: a -> *) (as :: [a]) (bs :: [a]). Rec f as -> Rec f bs -> Rec f (Eval (as ++ bs)) `rappend` Rec f bs ys)