{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | NP with optional values -- -- -- Intended for qualified import -- -- > import Ouroboros.Consensus.Util.OptNP (OptNP (..), ViewOptNP (..)) -- > import qualified Ouroboros.Consensus.Util.OptNP as OptNP module Ouroboros.Consensus.Util.OptNP ( NonEmptyOptNP , OptNP (..) , at , empty , fromNP , fromNonEmptyNP , fromSingleton , singleton , toNP -- * View , ViewOptNP (..) , view -- * Combining , combine , combineWith , zipWith ) where import Prelude hiding (zipWith) import Control.Monad (guard) import Data.Functor.These (These1 (..)) import Data.Kind (Type) import Data.Maybe (isJust) import Data.SOP.Strict hiding (And) import Data.Type.Bool (type (&&)) import Data.Type.Equality import GHC.Stack (HasCallStack) import Ouroboros.Consensus.Util.SOP type NonEmptyOptNP = OptNP 'False -- | Like an 'NP', but with optional values data OptNP (empty :: Bool) (f :: k -> Type) (xs :: [k]) where OptNil :: OptNP 'True f '[] OptCons :: !(f x) -> !(OptNP empty f xs) -> OptNP 'False f (x ': xs) OptSkip :: !(OptNP empty f xs) -> OptNP empty f (x ': xs) type instance AllN (OptNP empty) c = All c type instance SListIN (OptNP empty) = SListI type instance Prod (OptNP empty) = NP deriving instance All (Show `Compose` f) xs => Show (OptNP empty f xs) eq :: All (Eq `Compose` f) xs => OptNP empty f xs -> OptNP empty' f xs -> Maybe (empty :~: empty') eq :: OptNP empty f xs -> OptNP empty' f xs -> Maybe (empty :~: empty') eq OptNP empty f xs OptNil OptNP empty' f xs OptNil = (empty :~: empty) -> Maybe (empty :~: empty) forall a. a -> Maybe a Just empty :~: empty forall k (a :: k). a :~: a Refl eq (OptSkip OptNP empty f xs xs) (OptSkip OptNP empty' f xs ys) = OptNP empty f xs -> OptNP empty' f xs -> Maybe (empty :~: empty') forall k (f :: k -> *) (xs :: [k]) (empty :: Bool) (empty' :: Bool). All (Compose Eq f) xs => OptNP empty f xs -> OptNP empty' f xs -> Maybe (empty :~: empty') eq OptNP empty f xs xs OptNP empty' f xs OptNP empty' f xs ys eq (OptCons f x x OptNP empty f xs xs) (OptCons f x y OptNP empty f xs ys) = do Bool -> Maybe () forall (f :: * -> *). Alternative f => Bool -> f () guard (f x x f x -> f x -> Bool forall a. Eq a => a -> a -> Bool == f x f x y) empty :~: empty Refl <- OptNP empty f xs -> OptNP empty f xs -> Maybe (empty :~: empty) forall k (f :: k -> *) (xs :: [k]) (empty :: Bool) (empty' :: Bool). All (Compose Eq f) xs => OptNP empty f xs -> OptNP empty' f xs -> Maybe (empty :~: empty') eq OptNP empty f xs xs OptNP empty f xs OptNP empty f xs ys (empty :~: empty) -> Maybe (empty :~: empty) forall (m :: * -> *) a. Monad m => a -> m a return empty :~: empty forall k (a :: k). a :~: a Refl eq OptNP empty f xs _ OptNP empty' f xs _ = Maybe (empty :~: empty') forall a. Maybe a Nothing instance All (Eq `Compose` f) xs => Eq (OptNP empty f xs) where OptNP empty f xs xs == :: OptNP empty f xs -> OptNP empty f xs -> Bool == OptNP empty f xs ys = Maybe (empty :~: empty) -> Bool forall a. Maybe a -> Bool isJust (OptNP empty f xs -> OptNP empty f xs -> Maybe (empty :~: empty) forall k (f :: k -> *) (xs :: [k]) (empty :: Bool) (empty' :: Bool). All (Compose Eq f) xs => OptNP empty f xs -> OptNP empty' f xs -> Maybe (empty :~: empty') eq OptNP empty f xs xs OptNP empty f xs ys) empty :: forall f xs. SListI xs => OptNP 'True f xs empty :: OptNP 'True f xs empty = case SListI xs => SList xs forall k (xs :: [k]). SListI xs => SList xs sList @xs of SList xs SNil -> OptNP 'True f xs forall k (f :: k -> *). OptNP 'True f '[] OptNil SList xs SCons -> OptNP 'True f xs -> OptNP 'True f (x : xs) forall a (empty :: Bool) (f :: a -> *) (xs :: [a]) (x :: a). OptNP empty f xs -> OptNP empty f (x : xs) OptSkip OptNP 'True f xs forall k (f :: k -> *) (xs :: [k]). SListI xs => OptNP 'True f xs empty fromNonEmptyNP :: forall f xs. IsNonEmpty xs => NP f xs -> NonEmptyOptNP f xs fromNonEmptyNP :: NP f xs -> NonEmptyOptNP f xs fromNonEmptyNP NP f xs xs = case Proxy xs -> ProofNonEmpty xs forall a (xs :: [a]) (proxy :: [a] -> *). IsNonEmpty xs => proxy xs -> ProofNonEmpty xs isNonEmpty (Proxy xs forall k (t :: k). Proxy t Proxy @xs) of ProofNonEmpty {} -> case NP f xs xs of f x x :* NP f xs xs' -> (forall (empty :: Bool). OptNP empty f xs -> NonEmptyOptNP f xs) -> NP f xs -> NonEmptyOptNP f xs forall k (f :: k -> *) (xs :: [k]) r. (forall (empty :: Bool). OptNP empty f xs -> r) -> NP f xs -> r fromNP (f x -> OptNP empty f xs -> OptNP 'False f (x : xs) forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]). f x -> OptNP empty f xs -> OptNP 'False f (x : xs) OptCons f x x) NP f xs xs' fromNP :: (forall empty. OptNP empty f xs -> r) -> NP f xs -> r fromNP :: (forall (empty :: Bool). OptNP empty f xs -> r) -> NP f xs -> r fromNP forall (empty :: Bool). OptNP empty f xs -> r k NP f xs Nil = OptNP 'True f xs -> r forall (empty :: Bool). OptNP empty f xs -> r k OptNP 'True f xs forall k (f :: k -> *). OptNP 'True f '[] OptNil fromNP forall (empty :: Bool). OptNP empty f xs -> r k (f x x :* NP f xs xs) = (forall (empty :: Bool). OptNP empty f xs -> r) -> NP f xs -> r forall k (f :: k -> *) (xs :: [k]) r. (forall (empty :: Bool). OptNP empty f xs -> r) -> NP f xs -> r fromNP (OptNP 'False f xs -> r forall (empty :: Bool). OptNP empty f xs -> r k (OptNP 'False f xs -> r) -> (OptNP empty f xs -> OptNP 'False f xs) -> OptNP empty f xs -> r forall b c a. (b -> c) -> (a -> b) -> a -> c . f x -> OptNP empty f xs -> OptNP 'False f (x : xs) forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]). f x -> OptNP empty f xs -> OptNP 'False f (x : xs) OptCons f x x) NP f xs xs toNP :: OptNP empty f xs -> NP (Maybe :.: f) xs toNP :: OptNP empty f xs -> NP (Maybe :.: f) xs toNP = OptNP empty f xs -> NP (Maybe :.: f) xs forall k (empty :: Bool) (f :: k -> *) (xs :: [k]). OptNP empty f xs -> NP (Maybe :.: f) xs go where go :: OptNP empty f xs -> NP (Maybe :.: f) xs go :: OptNP empty f xs -> NP (Maybe :.: f) xs go OptNP empty f xs OptNil = NP (Maybe :.: f) xs forall k (f :: k -> *). NP f '[] Nil go (OptCons f x x OptNP empty f xs xs) = Maybe (f x) -> (:.:) Maybe f x forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp (f x -> Maybe (f x) forall a. a -> Maybe a Just f x x) (:.:) Maybe f x -> NP (Maybe :.: f) xs -> NP (Maybe :.: f) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* OptNP empty f xs -> NP (Maybe :.: f) xs forall k (empty :: Bool) (f :: k -> *) (xs :: [k]). OptNP empty f xs -> NP (Maybe :.: f) xs go OptNP empty f xs xs go (OptSkip OptNP empty f xs xs) = Maybe (f x) -> (:.:) Maybe f x forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp Maybe (f x) forall a. Maybe a Nothing (:.:) Maybe f x -> NP (Maybe :.: f) xs -> NP (Maybe :.: f) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* OptNP empty f xs -> NP (Maybe :.: f) xs forall k (empty :: Bool) (f :: k -> *) (xs :: [k]). OptNP empty f xs -> NP (Maybe :.: f) xs go OptNP empty f xs xs at :: SListI xs => f x -> Index xs x -> NonEmptyOptNP f xs at :: f x -> Index xs x -> NonEmptyOptNP f xs at f x x Index xs x IZ = f x -> OptNP 'True f xs -> OptNP 'False f (x : xs) forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]). f x -> OptNP empty f xs -> OptNP 'False f (x : xs) OptCons f x x OptNP 'True f xs forall k (f :: k -> *) (xs :: [k]). SListI xs => OptNP 'True f xs empty at f x x (IS Index xs x index) = OptNP 'False f xs -> OptNP 'False f (y : xs) forall a (empty :: Bool) (f :: a -> *) (xs :: [a]) (x :: a). OptNP empty f xs -> OptNP empty f (x : xs) OptSkip (f x -> Index xs x -> OptNP 'False f xs forall k (xs :: [k]) (f :: k -> *) (x :: k). SListI xs => f x -> Index xs x -> NonEmptyOptNP f xs at f x x Index xs x index) singleton :: f x -> NonEmptyOptNP f '[x] singleton :: f x -> NonEmptyOptNP f '[x] singleton f x x = f x -> OptNP 'True f '[] -> NonEmptyOptNP f '[x] forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]). f x -> OptNP empty f xs -> OptNP 'False f (x : xs) OptCons f x x OptNP 'True f '[] forall k (f :: k -> *). OptNP 'True f '[] OptNil -- | If 'OptNP' is not empty, it must contain at least one value fromSingleton :: NonEmptyOptNP f '[x] -> f x fromSingleton :: NonEmptyOptNP f '[x] -> f x fromSingleton (OptCons f x x OptNP empty f xs _) = f x f x x ap :: NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs ap :: NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs ap = NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) (empty :: Bool). NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs go where go :: NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs go :: NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs go ((-.->) f g x f :* NP (f -.-> g) xs fs) (OptCons f x x OptNP empty f xs xs) = g x -> OptNP empty g xs -> OptNP 'False g (x : xs) forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]). f x -> OptNP empty f xs -> OptNP 'False f (x : xs) OptCons ((-.->) f g x -> f x -> g x forall k (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) f g x f f x f x x) (NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) (empty :: Bool). NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs go NP (f -.-> g) xs fs OptNP empty f xs OptNP empty f xs xs) go ((-.->) f g x _ :* NP (f -.-> g) xs fs) (OptSkip OptNP empty f xs xs) = OptNP empty g xs -> OptNP empty g (x : xs) forall a (empty :: Bool) (f :: a -> *) (xs :: [a]) (x :: a). OptNP empty f xs -> OptNP empty f (x : xs) OptSkip (NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) (empty :: Bool). NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs go NP (f -.-> g) xs fs OptNP empty f xs OptNP empty f xs xs) go NP (f -.-> g) xs Nil OptNP empty f xs OptNil = OptNP empty g xs forall k (f :: k -> *). OptNP 'True f '[] OptNil ctraverse' :: forall c proxy empty xs f f' g. (All c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> OptNP empty f xs -> g (OptNP empty f' xs) ctraverse' :: proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> OptNP empty f xs -> g (OptNP empty f' xs) ctraverse' proxy c _ forall (a :: k). c a => f a -> g (f' a) f = OptNP empty f xs -> g (OptNP empty f' xs) forall (ys :: [k]) (empty' :: Bool). All c ys => OptNP empty' f ys -> g (OptNP empty' f' ys) go where go :: All c ys => OptNP empty' f ys -> g (OptNP empty' f' ys) go :: OptNP empty' f ys -> g (OptNP empty' f' ys) go (OptCons f x x OptNP empty f xs xs) = f' x -> OptNP empty f' xs -> OptNP 'False f' (x : xs) forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]). f x -> OptNP empty f xs -> OptNP 'False f (x : xs) OptCons (f' x -> OptNP empty f' xs -> OptNP 'False f' (x : xs)) -> g (f' x) -> g (OptNP empty f' xs -> OptNP 'False f' (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> f x -> g (f' x) forall (a :: k). c a => f a -> g (f' a) f f x x g (OptNP empty f' xs -> OptNP 'False f' (x : xs)) -> g (OptNP empty f' xs) -> g (OptNP 'False f' (x : xs)) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> OptNP empty f xs -> g (OptNP empty f' xs) forall (ys :: [k]) (empty' :: Bool). All c ys => OptNP empty' f ys -> g (OptNP empty' f' ys) go OptNP empty f xs xs go (OptSkip OptNP empty' f xs xs) = OptNP empty' f' xs -> OptNP empty' f' (x : xs) forall a (empty :: Bool) (f :: a -> *) (xs :: [a]) (x :: a). OptNP empty f xs -> OptNP empty f (x : xs) OptSkip (OptNP empty' f' xs -> OptNP empty' f' (x : xs)) -> g (OptNP empty' f' xs) -> g (OptNP empty' f' (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> OptNP empty' f xs -> g (OptNP empty' f' xs) forall (ys :: [k]) (empty' :: Bool). All c ys => OptNP empty' f ys -> g (OptNP empty' f' ys) go OptNP empty' f xs xs go OptNP empty' f ys OptNil = OptNP 'True f' '[] -> g (OptNP 'True f' '[]) forall (f :: * -> *) a. Applicative f => a -> f a pure OptNP 'True f' '[] forall k (f :: k -> *). OptNP 'True f '[] OptNil instance HAp (OptNP empty) where hap :: Prod (OptNP empty) (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs hap = Prod (OptNP empty) (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) (empty :: Bool). NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs ap instance HSequence (OptNP empty) where hctraverse' :: proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> OptNP empty f xs -> g (OptNP empty f' xs) hctraverse' = proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> OptNP empty f xs -> g (OptNP empty f' xs) forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (empty :: Bool) (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *). (All c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> OptNP empty f xs -> g (OptNP empty f' xs) ctraverse' htraverse' :: (forall (a :: k). f a -> g (f' a)) -> OptNP empty f xs -> g (OptNP empty f' xs) htraverse' = Proxy Top -> (forall (a :: k). Top a => f a -> g (f' a)) -> OptNP empty f xs -> g (OptNP empty f' xs) forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (g :: * -> *) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (HSequence h, AllN h c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> h f xs -> g (h f' xs) hctraverse' (Proxy Top forall k (t :: k). Proxy t Proxy @Top) hsequence' :: OptNP empty (f :.: g) xs -> f (OptNP empty g xs) hsequence' = (forall (a :: k). (:.:) f g a -> f (g a)) -> OptNP empty (f :.: g) xs -> f (OptNP empty g xs) forall k l (h :: (k -> *) -> l -> *) (xs :: l) (g :: * -> *) (f :: k -> *) (f' :: k -> *). (HSequence h, SListIN h xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> h f xs -> g (h f' xs) htraverse' forall (a :: k). (:.:) f g a -> f (g a) forall l k (f :: l -> *) (g :: k -> l) (p :: k). (:.:) f g p -> f (g p) unComp {------------------------------------------------------------------------------- View -------------------------------------------------------------------------------} data ViewOptNP f xs where OptNP_ExactlyOne :: f x -> ViewOptNP f '[x] OptNP_AtLeastTwo :: ViewOptNP f (x ': y ': zs) view :: forall f xs. NonEmptyOptNP f xs -> ViewOptNP f xs view :: NonEmptyOptNP f xs -> ViewOptNP f xs view = \case OptCons f x x OptNP empty f xs OptNil -> f x -> ViewOptNP f '[x] forall k (f :: k -> *) (x :: k). f x -> ViewOptNP f '[x] OptNP_ExactlyOne f x x OptCons f x _ (OptCons f x _ OptNP empty f xs _) -> ViewOptNP f xs forall k (f :: k -> *) (x :: k) (y :: k) (zs :: [k]). ViewOptNP f (x : y : zs) OptNP_AtLeastTwo OptCons f x _ (OptSkip OptNP empty f xs _) -> ViewOptNP f xs forall k (f :: k -> *) (x :: k) (y :: k) (zs :: [k]). ViewOptNP f (x : y : zs) OptNP_AtLeastTwo OptSkip (OptCons f x _ OptNP empty f xs _) -> ViewOptNP f xs forall k (f :: k -> *) (x :: k) (y :: k) (zs :: [k]). ViewOptNP f (x : y : zs) OptNP_AtLeastTwo OptSkip (OptSkip OptNP 'False f xs _) -> ViewOptNP f xs forall k (f :: k -> *) (x :: k) (y :: k) (zs :: [k]). ViewOptNP f (x : y : zs) OptNP_AtLeastTwo {------------------------------------------------------------------------------- Combining -------------------------------------------------------------------------------} zipWith :: forall f g h xs. (forall a. These1 f g a -> h a) -> NonEmptyOptNP f xs -> NonEmptyOptNP g xs -> NonEmptyOptNP h xs zipWith :: (forall a. These1 f g a -> h a) -> NonEmptyOptNP f xs -> NonEmptyOptNP g xs -> NonEmptyOptNP h xs zipWith = (forall a. These1 f g a -> h a) -> NonEmptyOptNP f xs -> NonEmptyOptNP g xs -> NonEmptyOptNP h xs forall (f :: * -> *) (g :: * -> *) (h :: * -> *) (empty1 :: Bool) (empty2 :: Bool) (xs :: [*]). (forall a. These1 f g a -> h a) -> OptNP empty1 f xs -> OptNP empty2 g xs -> OptNP (empty1 && empty2) h xs polyZipWith -- | NOT EXPORTED polyZipWith :: forall f g h empty1 empty2 xs. (forall a. These1 f g a -> h a) -> OptNP empty1 f xs -> OptNP empty2 g xs -> OptNP (empty1 && empty2) h xs polyZipWith :: (forall a. These1 f g a -> h a) -> OptNP empty1 f xs -> OptNP empty2 g xs -> OptNP (empty1 && empty2) h xs polyZipWith forall a. These1 f g a -> h a f = OptNP empty1 f xs -> OptNP empty2 g xs -> OptNP (empty1 && empty2) h xs forall (empty1' :: Bool) (xs' :: [*]) (empty2' :: Bool). OptNP empty1' f xs' -> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs' go where go :: OptNP empty1' f xs' -> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs' go :: OptNP empty1' f xs' -> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs' go OptNP empty1' f xs' OptNil OptNP empty2' g xs' OptNil = OptNP (empty1' && empty2') h xs' forall k (f :: k -> *). OptNP 'True f '[] OptNil go (OptCons f x x OptNP empty f xs xs) (OptSkip OptNP empty2' g xs ys) = h x -> OptNP (empty && empty2') h xs -> OptNP 'False h (x : xs) forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]). f x -> OptNP empty f xs -> OptNP 'False f (x : xs) OptCons (These1 f g x -> h x forall a. These1 f g a -> h a f (f x -> These1 f g x forall (f :: * -> *) (g :: * -> *) a. f a -> These1 f g a This1 f x x )) (OptNP empty f xs -> OptNP empty2' g xs -> OptNP (empty && empty2') h xs forall (empty1' :: Bool) (xs' :: [*]) (empty2' :: Bool). OptNP empty1' f xs' -> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs' go OptNP empty f xs xs OptNP empty2' g xs OptNP empty2' g xs ys) go (OptSkip OptNP empty1' f xs xs) (OptCons g x y OptNP empty g xs ys) = h x -> OptNP (empty1' && empty) h xs -> OptNP 'False h (x : xs) forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]). f x -> OptNP empty f xs -> OptNP 'False f (x : xs) OptCons (These1 f g x -> h x forall a. These1 f g a -> h a f (g x -> These1 f g x forall (f :: * -> *) (g :: * -> *) a. g a -> These1 f g a That1 g x y)) (OptNP empty1' f xs -> OptNP empty g xs -> OptNP (empty1' && empty) h xs forall (empty1' :: Bool) (xs' :: [*]) (empty2' :: Bool). OptNP empty1' f xs' -> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs' go OptNP empty1' f xs xs OptNP empty g xs OptNP empty g xs ys) go (OptCons f x x OptNP empty f xs xs) (OptCons g x y OptNP empty g xs ys) = h x -> OptNP (empty && empty) h xs -> OptNP 'False h (x : xs) forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]). f x -> OptNP empty f xs -> OptNP 'False f (x : xs) OptCons (These1 f g x -> h x forall a. These1 f g a -> h a f (f x -> g x -> These1 f g x forall (f :: * -> *) (g :: * -> *) a. f a -> g a -> These1 f g a These1 f x x g x g x y)) (OptNP empty f xs -> OptNP empty g xs -> OptNP (empty && empty) h xs forall (empty1' :: Bool) (xs' :: [*]) (empty2' :: Bool). OptNP empty1' f xs' -> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs' go OptNP empty f xs xs OptNP empty g xs OptNP empty g xs ys) go (OptSkip OptNP empty1' f xs xs) (OptSkip OptNP empty2' g xs ys) = OptNP (empty1' && empty2') h xs -> OptNP (empty1' && empty2') h (x : xs) forall a (empty :: Bool) (f :: a -> *) (xs :: [a]) (x :: a). OptNP empty f xs -> OptNP empty f (x : xs) OptSkip (OptNP empty1' f xs -> OptNP empty2' g xs -> OptNP (empty1' && empty2') h xs forall (empty1' :: Bool) (xs' :: [*]) (empty2' :: Bool). OptNP empty1' f xs' -> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs' go OptNP empty1' f xs xs OptNP empty2' g xs OptNP empty2' g xs ys) combineWith :: SListI xs => (forall a. These1 f g a -> h a) -> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP g xs) -> Maybe (NonEmptyOptNP h xs) combineWith :: (forall a. These1 f g a -> h a) -> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP g xs) -> Maybe (NonEmptyOptNP h xs) combineWith forall a. These1 f g a -> h a _ Maybe (NonEmptyOptNP f xs) Nothing Maybe (NonEmptyOptNP g xs) Nothing = Maybe (NonEmptyOptNP h xs) forall a. Maybe a Nothing combineWith forall a. These1 f g a -> h a f (Just NonEmptyOptNP f xs xs) Maybe (NonEmptyOptNP g xs) Nothing = NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs) forall a. a -> Maybe a Just (NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs)) -> NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs) forall a b. (a -> b) -> a -> b $ (forall a. These1 f g a -> h a) -> NonEmptyOptNP f xs -> OptNP 'True g xs -> OptNP ('False && 'True) h xs forall (f :: * -> *) (g :: * -> *) (h :: * -> *) (empty1 :: Bool) (empty2 :: Bool) (xs :: [*]). (forall a. These1 f g a -> h a) -> OptNP empty1 f xs -> OptNP empty2 g xs -> OptNP (empty1 && empty2) h xs polyZipWith forall a. These1 f g a -> h a f NonEmptyOptNP f xs xs OptNP 'True g xs forall k (f :: k -> *) (xs :: [k]). SListI xs => OptNP 'True f xs empty combineWith forall a. These1 f g a -> h a f Maybe (NonEmptyOptNP f xs) Nothing (Just NonEmptyOptNP g xs ys) = NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs) forall a. a -> Maybe a Just (NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs)) -> NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs) forall a b. (a -> b) -> a -> b $ (forall a. These1 f g a -> h a) -> OptNP 'True f xs -> NonEmptyOptNP g xs -> OptNP ('True && 'False) h xs forall (f :: * -> *) (g :: * -> *) (h :: * -> *) (empty1 :: Bool) (empty2 :: Bool) (xs :: [*]). (forall a. These1 f g a -> h a) -> OptNP empty1 f xs -> OptNP empty2 g xs -> OptNP (empty1 && empty2) h xs polyZipWith forall a. These1 f g a -> h a f OptNP 'True f xs forall k (f :: k -> *) (xs :: [k]). SListI xs => OptNP 'True f xs empty NonEmptyOptNP g xs ys combineWith forall a. These1 f g a -> h a f (Just NonEmptyOptNP f xs xs) (Just NonEmptyOptNP g xs ys) = NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs) forall a. a -> Maybe a Just (NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs)) -> NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs) forall a b. (a -> b) -> a -> b $ (forall a. These1 f g a -> h a) -> NonEmptyOptNP f xs -> NonEmptyOptNP g xs -> OptNP ('False && 'False) h xs forall (f :: * -> *) (g :: * -> *) (h :: * -> *) (empty1 :: Bool) (empty2 :: Bool) (xs :: [*]). (forall a. These1 f g a -> h a) -> OptNP empty1 f xs -> OptNP empty2 g xs -> OptNP (empty1 && empty2) h xs polyZipWith forall a. These1 f g a -> h a f NonEmptyOptNP f xs xs NonEmptyOptNP g xs ys -- | Precondition: there is no overlap between the two given lists: if there is -- a 'Just' at a given position in one, it must be 'Nothing' at the same -- position in the other. combine :: forall (f :: Type -> Type) xs. -- 'These1' is not kind-polymorphic (SListI xs, HasCallStack) => Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP f xs) combine :: Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP f xs) combine = (forall a. These1 f f a -> f a) -> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP f xs) forall (xs :: [*]) (f :: * -> *) (g :: * -> *) (h :: * -> *). SListI xs => (forall a. These1 f g a -> h a) -> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP g xs) -> Maybe (NonEmptyOptNP h xs) combineWith ((forall a. These1 f f a -> f a) -> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP f xs)) -> (forall a. These1 f f a -> f a) -> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP f xs) forall a b. (a -> b) -> a -> b $ \case This1 f a x -> f a x That1 f a y -> f a y These1 {} -> String -> f a forall a. HasCallStack => String -> a error String "combine: precondition violated"