Мне в итоге подсказали сделать вот так: data N = Z | S N type Index :: k -> [k] -> N type family Index x xs where Index x (x : _) = 'Z Index x (_ : xs) = 'S (Index x xs) type Remove :: N -> (* -> *) -> [* -> *] -> [* -> *] -> Constraint class Remove i f fs gs | i f fs -> gs where remove' :: Union fs x -> Either (f x) (Union gs x) instance Remove 'Z f (f : fs) fs where remove' = union Left Right instance (Remove n f fs gs, n ~ Index f fs) => Remove ('S n) f (g : fs) (g : gs) where remove' = union (Right . Here) (fmap There . remove) remove :: forall f fs gs x. Remove (Index f fs) f fs gs => Union fs x -> Either (f x) (Union gs x) remove = remove' @(Index f fs) handle :: forall f fs gs a x. (Remove (Index f fs) f fs gs) => (f x -> a) -> (Union gs x -> a) -> (Union fs x -> a) А sop я не хочу, зависимость лишняя
pattern Elem :: Member f fs => f a -> Union fs a pattern Elem x <- (project -> Just x) where Elem x = inject x union :: (f x -> c) -> (Union fs x -> c) -> Union (f : fs) x -> c union here there = \case Here fa -> here fa There fa -> there fa
Remove это типа Project?
Не, это "разложить fs на f и всё остальное"
Обсуждают сегодня