{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | NP with optional values -- -- Intended for qualified import -- -- > import Data.SOP.OptNP (OptNP (..), ViewOptNP (..)) -- > import qualified Data.SOP.OptNP as OptNP module Data.SOP.OptNP ( NonEmptyOptNP , OptNP (..) , at , empty , fromNP , fromNonEmptyNP , fromSingleton , singleton , toNP -- * View , ViewOptNP (..) , view -- * Combining , combine , combineWith , zipWith ) where import Control.Monad (guard) import Data.Coerce (coerce) import Data.Functor.These (These1 (..)) import Data.Kind (Type) import Data.Maybe (isJust) import Data.Proxy import Data.SOP.BasicFunctors import Data.SOP.Constraint import Data.SOP.Index import Data.SOP.NonEmpty import Data.SOP.Sing import Data.SOP.Strict import Data.Type.Bool (type (&&)) import Data.Type.Equality import GHC.Stack (HasCallStack) import Prelude hiding (zipWith) type NonEmptyOptNP = OptNP 'False -- | Like an 'NP', but with optional values type OptNP :: Bool -> (k -> Type) -> [k] -> Type data OptNP empty f xs 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 :: 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 OptNil OptNP empty' f xs OptNil = (empty :~: empty') -> Maybe (empty :~: empty') forall a. a -> Maybe a Just empty :~: empty 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 a. a -> Maybe a forall (m :: * -> *) a. Monad m => a -> m a return empty :~: empty 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 :: forall {k} (f :: k -> *) (xs :: [k]). SListI xs => OptNP 'True f xs empty = case forall (xs :: [k]). SListI xs => SList xs forall {k} (xs :: [k]). SListI xs => SList xs sList @xs of SList xs SNil -> OptNP 'True f xs OptNP 'True f '[] forall {k} (f :: k -> *). OptNP 'True f '[] OptNil SList xs SCons -> OptNP 'True f xs -> OptNP 'True f (x : xs) forall {k} (empty :: Bool) (f :: k -> *) (x :: [k]) (y :: k). OptNP empty f x -> OptNP empty f (y : x) 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 :: forall {k} (f :: k -> *) (xs :: [k]). IsNonEmpty xs => 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 forall (proxy :: [k] -> *). proxy xs -> ProofNonEmpty xs isNonEmpty (forall (t :: [k]). Proxy t forall {k} (t :: k). Proxy t Proxy @xs) of ProofNonEmpty {} -> case NP f xs xs of f x x :* NP f xs1 xs' -> (forall (empty :: Bool). OptNP empty f xs1 -> NonEmptyOptNP f xs) -> NP f xs1 -> 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 xs1 -> OptNP 'False f (x : xs1) forall {k} (f :: k -> *) (x :: k) (y :: Bool) (zs :: [k]). f x -> OptNP y f zs -> OptNP 'False f (x : zs) OptCons f x f x x) NP f xs1 xs' fromNP :: (forall empty. OptNP empty f xs -> r) -> NP f xs -> r fromNP :: forall {k} (f :: k -> *) (xs :: [k]) r. (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 OptNP 'True f '[] forall {k} (f :: k -> *). OptNP 'True f '[] OptNil fromNP forall (empty :: Bool). OptNP empty f xs -> r k (f x x :* NP f xs1 xs) = (forall (empty :: Bool). OptNP empty f xs1 -> r) -> NP f xs1 -> 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 xs1 -> OptNP 'False f xs) -> OptNP empty f xs1 -> r forall b c a. (b -> c) -> (a -> b) -> a -> c . f x -> OptNP empty f xs1 -> OptNP 'False f (x : xs1) forall {k} (f :: k -> *) (x :: k) (y :: Bool) (zs :: [k]). f x -> OptNP y f zs -> OptNP 'False f (x : zs) OptCons f x x) NP f xs1 xs toNP :: OptNP empty f xs -> NP (Maybe :.: f) xs toNP :: forall {k} (empty :: Bool) (f :: k -> *) (xs :: [k]). 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 :: forall {k} (empty :: Bool) (f :: k -> *) (xs :: [k]). OptNP empty f xs -> NP (Maybe :.: f) xs go OptNP empty f xs OptNil = NP (Maybe :.: f) xs NP (Maybe :.: f) '[] 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 {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NP f xs1 -> NP f (x : xs1) :* 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 {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NP f xs1 -> NP f (x : xs1) :* 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 :: 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 IZ = f x -> OptNP 'True f xs1 -> OptNP 'False f (x : xs1) forall {k} (f :: k -> *) (x :: k) (y :: Bool) (zs :: [k]). f x -> OptNP y f zs -> OptNP 'False f (x : zs) OptCons f x x OptNP 'True f xs1 forall {k} (f :: k -> *) (xs :: [k]). SListI xs => OptNP 'True f xs empty at f x x (IS Index xs1 x index) = OptNP 'False f xs1 -> OptNP 'False f (y : xs1) forall {k} (empty :: Bool) (f :: k -> *) (x :: [k]) (y :: k). OptNP empty f x -> OptNP empty f (y : x) OptSkip (f x -> Index xs1 x -> OptNP 'False f xs1 forall {k} (xs :: [k]) (f :: k -> *) (x :: k). SListI xs => f x -> Index xs x -> NonEmptyOptNP f xs at f x x Index xs1 x index) singleton :: f x -> NonEmptyOptNP f '[x] singleton :: forall {k} (f :: k -> *) (x :: k). f x -> NonEmptyOptNP f '[x] singleton f x x = f x -> OptNP 'True f '[] -> OptNP 'False f '[x] forall {k} (f :: k -> *) (x :: k) (y :: Bool) (zs :: [k]). f x -> OptNP y f zs -> OptNP 'False f (x : zs) 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 :: forall {k} (f :: k -> *) (x :: k). 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 :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (empty :: Bool). 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 :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (empty :: Bool). NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs go ((-.->) f g x f :* NP (f -.-> g) xs1 fs) (OptCons f x x OptNP empty f xs xs) = g x -> OptNP empty g xs1 -> OptNP 'False g (x : xs1) forall {k} (f :: k -> *) (x :: k) (y :: Bool) (zs :: [k]). f x -> OptNP y f zs -> OptNP 'False f (x : zs) 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) xs1 -> OptNP empty f xs1 -> OptNP empty g xs1 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) xs1 fs OptNP empty f xs1 OptNP empty f xs xs) go ((-.->) f g x _ :* NP (f -.-> g) xs1 fs) (OptSkip OptNP empty f xs xs) = OptNP empty g xs1 -> OptNP empty g (x : xs1) forall {k} (empty :: Bool) (f :: k -> *) (x :: [k]) (y :: k). OptNP empty f x -> OptNP empty f (y : x) OptSkip (NP (f -.-> g) xs1 -> OptNP empty f xs1 -> OptNP empty g xs1 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) xs1 fs OptNP empty f xs1 OptNP empty f xs xs) go NP (f -.-> g) xs Nil OptNP empty f xs OptNil = OptNP empty g xs OptNP 'True g '[] 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' :: 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' 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 :: forall (ys :: [k]) (empty' :: Bool). All c ys => 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 empty' f' ys f' x -> OptNP empty f' xs -> OptNP 'False f' (x : xs) forall {k} (f :: k -> *) (x :: k) (y :: Bool) (zs :: [k]). f x -> OptNP y f zs -> OptNP 'False f (x : zs) OptCons (f' x -> OptNP empty f' xs -> OptNP empty' f' ys) -> g (f' x) -> g (OptNP empty f' xs -> OptNP empty' f' ys) 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 empty' f' ys) -> g (OptNP empty f' xs) -> g (OptNP empty' f' ys) forall a b. g (a -> b) -> g a -> g b 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' ys OptNP empty' f' xs -> OptNP empty' f' (x : xs) forall {k} (empty :: Bool) (f :: k -> *) (x :: [k]) (y :: k). OptNP empty f x -> OptNP empty f (y : x) OptSkip (OptNP empty' f' xs -> OptNP empty' f' ys) -> g (OptNP empty' f' xs) -> g (OptNP empty' f' ys) 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 empty' f' ys -> g (OptNP empty' f' ys) forall a. a -> g a forall (f :: * -> *) a. Applicative f => a -> f a pure OptNP empty' f' ys OptNP 'True f' '[] forall {k} (f :: k -> *). OptNP 'True f '[] OptNil instance HAp (OptNP empty) where hap :: forall (f :: k -> *) (g :: k -> *) (xs :: [k]). 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 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 ap instance HSequence (OptNP empty) where hctraverse' :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (OptNP empty) 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) 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 (xs :: [k]) (g :: * -> *) (f :: k -> *) (f' :: k -> *). (SListIN (OptNP empty) xs, Applicative g) => (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) forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (OptNP empty) 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) hctraverse' (forall {k} (t :: k). Proxy t forall (t :: k -> Constraint). Proxy t Proxy @Top) hsequence' :: forall (xs :: [k]) (f :: * -> *) (g :: k -> *). (SListIN (OptNP empty) xs, Applicative f) => 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 (xs :: [k]) (g :: * -> *) (f :: k -> *) (f' :: k -> *). (SListIN (OptNP empty) xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> OptNP empty f xs -> g (OptNP empty f' 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' (:.:) f g a -> f (g a) 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 type instance Same (OptNP empty) = OptNP empty instance HTrans (OptNP empty) (OptNP empty) where htrans :: forall (c :: k1 -> k2 -> Constraint) (xs :: [k1]) (ys :: [k2]) (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *) (g :: k2 -> *). AllZipN (Prod (OptNP empty)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> OptNP empty f xs -> OptNP empty g ys htrans = proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> OptNP empty f xs -> OptNP empty g ys forall {k1} {k2} {k} (empty :: Bool) (c :: k1 -> k2 -> Constraint) (xs :: [k1]) (ys :: [k2]) (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *) (g :: k2 -> *). AllZipN (Prod (OptNP empty)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> OptNP empty f xs -> OptNP empty g ys trans_OptNP -- NOTE(jdral): this code could be replaced by 'unsafeCoerce' (see 'trans_NP' -- or 'trans_NS' for examples), but this would technically sacrifice type -- safety. For now, this version should be sufficient. hcoerce :: forall (f :: k1 -> *) (g :: k2 -> *) (xs :: [k1]) (ys :: [k2]). AllZipN (Prod (OptNP empty)) (LiftedCoercible f g) xs ys => OptNP empty f xs -> OptNP empty g ys hcoerce = OptNP empty f xs -> OptNP empty g ys forall {k} {k} {k} (empty :: Bool) (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]). AllZipN (Prod (OptNP empty)) (LiftedCoercible f g) xs ys => OptNP empty f xs -> OptNP empty g ys coerce_OptNP trans_OptNP :: AllZipN (Prod (OptNP empty)) c xs ys => proxy c -> (forall x y. c x y => f x -> g y) -> OptNP empty f xs -> OptNP empty g ys trans_OptNP :: forall {k1} {k2} {k} (empty :: Bool) (c :: k1 -> k2 -> Constraint) (xs :: [k1]) (ys :: [k2]) (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *) (g :: k2 -> *). AllZipN (Prod (OptNP empty)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> OptNP empty f xs -> OptNP empty g ys trans_OptNP proxy c p forall (x :: k1) (y :: k2). c x y => f x -> g y t = \case OptNP empty f xs OptNil -> OptNP empty g ys OptNP 'True g '[] forall {k} (f :: k -> *). OptNP 'True f '[] OptNil OptCons f x fx OptNP empty f xs fxs -> g (Head ys) -> OptNP empty g (Tail ys) -> OptNP 'False g (Head ys : Tail ys) forall {k} (f :: k -> *) (x :: k) (y :: Bool) (zs :: [k]). f x -> OptNP y f zs -> OptNP 'False f (x : zs) OptCons (f x -> g (Head ys) forall (x :: k1) (y :: k2). c x y => f x -> g y t f x fx) (proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> OptNP empty f xs -> OptNP empty g (Tail ys) forall {k1} {k2} {k} (empty :: Bool) (c :: k1 -> k2 -> Constraint) (xs :: [k1]) (ys :: [k2]) (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *) (g :: k2 -> *). AllZipN (Prod (OptNP empty)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> OptNP empty f xs -> OptNP empty g ys trans_OptNP proxy c p f x -> g y forall (x :: k1) (y :: k2). c x y => f x -> g y t OptNP empty f xs fxs) OptSkip OptNP empty f xs fxs -> OptNP empty g (Tail ys) -> OptNP empty g (Head ys : Tail ys) forall {k} (empty :: Bool) (f :: k -> *) (x :: [k]) (y :: k). OptNP empty f x -> OptNP empty f (y : x) OptSkip (proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> OptNP empty f xs -> OptNP empty g (Tail ys) forall {k1} {k2} {k} (empty :: Bool) (c :: k1 -> k2 -> Constraint) (xs :: [k1]) (ys :: [k2]) (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *) (g :: k2 -> *). AllZipN (Prod (OptNP empty)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> OptNP empty f xs -> OptNP empty g ys trans_OptNP proxy c p f x -> g y forall (x :: k1) (y :: k2). c x y => f x -> g y t OptNP empty f xs fxs) coerce_OptNP :: forall empty f g xs ys. AllZipN (Prod (OptNP empty)) (LiftedCoercible f g) xs ys => OptNP empty f xs -> OptNP empty g ys coerce_OptNP :: forall {k} {k} {k} (empty :: Bool) (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]). AllZipN (Prod (OptNP empty)) (LiftedCoercible f g) xs ys => OptNP empty f xs -> OptNP empty g ys coerce_OptNP = Proxy (LiftedCoercible f g) -> (forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y) -> OptNP empty f xs -> OptNP empty g ys forall {k1} {k2} {k} (empty :: Bool) (c :: k1 -> k2 -> Constraint) (xs :: [k1]) (ys :: [k2]) (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *) (g :: k2 -> *). AllZipN (Prod (OptNP empty)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> OptNP empty f xs -> OptNP empty g ys trans_OptNP (forall {k} (t :: k). Proxy t forall (t :: k -> k -> Constraint). Proxy t Proxy @(LiftedCoercible f g)) f x -> g y forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y forall a b. Coercible a b => a -> b coerce {------------------------------------------------------------------------------- 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 :: forall {k} (f :: k -> *) (xs :: [k]). 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 ViewOptNP f (x : x : 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 ViewOptNP f (x : x : 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 ViewOptNP f (x : x : 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 ViewOptNP f (x : x : 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 (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) -> OptNP 'False f xs -> OptNP 'False g xs -> OptNP 'False h xs (forall a. These1 f g a -> h a) -> OptNP 'False f xs -> OptNP 'False 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 -- | 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 (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 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 :: forall (empty1' :: Bool) (xs' :: [*]) (empty2' :: Bool). 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 'True h '[] 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 {k} (f :: k -> *) (x :: k) (y :: Bool) (zs :: [k]). f x -> OptNP y f zs -> OptNP 'False f (x : zs) 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 {k} (f :: k -> *) (x :: k) (y :: Bool) (zs :: [k]). f x -> OptNP y f zs -> OptNP 'False f (x : zs) 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 {k} (f :: k -> *) (x :: k) (y :: Bool) (zs :: [k]). f x -> OptNP y f zs -> OptNP 'False f (x : zs) 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 {k} (empty :: Bool) (f :: k -> *) (x :: [k]) (y :: k). OptNP empty f x -> OptNP empty f (y : x) 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 (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 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 These1 f g a -> h a 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 These1 f g a -> h a 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 These1 f g a -> h a 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 :: forall (f :: * -> *) (xs :: [*]). (SListI xs, HasCallStack) => 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"