{-# 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"