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

-- | Strict variant of NP
--
-- See [@sop-core@'s
-- NP](https://hackage.haskell.org/package/sop-core/docs/Data-SOP-NP.html).
module Data.SOP.Strict.NP (
    -- * NP
    NP (..)
  , hd
  , map_NP'
  , npToSListI
  , singletonNP
  , tl
  ) where

import           Data.Coerce
import           Data.Kind (Type)
import           Data.SOP hiding (NP (..), hd, tl)
import           Data.SOP.Classes
import           Data.SOP.Constraint
import           NoThunks.Class

type NP :: (k -> Type) -> [k] -> Type
data NP f xs where
  Nil  :: NP f '[]
  (:*) :: !(f x) -> !(NP f xs) -> NP f (x ': xs)

infixr 5 :*

type instance CollapseTo NP a = [a]
type instance AllN       NP c = All c
type instance AllZipN    NP c = AllZip c
type instance Prod       NP   = NP
type instance SListIN    NP   = SListI
type instance Same       NP   = NP

singletonNP :: f x -> NP f '[x]
singletonNP :: forall {k} (f :: k -> *) (x :: k). f x -> NP f '[x]
singletonNP f x
fx = f x
fx f x -> NP f '[] -> NP f '[x]
forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP f xs -> NP f (x : xs)
:* NP f '[]
forall {k} (f :: k -> *). NP f '[]
Nil

hd :: NP f (x ': xs) -> f x
hd :: forall {k} (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x
hd (f x
x :* NP f xs
_) = f x
f x
x

tl :: NP f (x ': xs) -> NP f xs
tl :: forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
NP f (x : xs) -> NP f xs
tl (f x
_ :* NP f xs
xs) = NP f xs
NP f xs
xs

ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP NP (f -.-> g) xs
Nil          NP f xs
Nil       = NP g xs
NP g '[]
forall {k} (f :: k -> *). NP f '[]
Nil
ap_NP (Fn f x -> g x
f :* NP (f -.-> g) xs
fs) (f x
x :* NP f xs
xs) = f x -> g x
f f x
f x
x g x -> NP g xs -> NP g (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP f xs -> NP f (x : xs)
:* NP (f -.-> g) xs -> NP f xs -> NP g xs
forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP NP (f -.-> g) xs
fs NP f xs
NP f xs
xs

pure_NP :: SListI xs => (forall a. f a) -> NP f xs
pure_NP :: forall {k} (xs :: [k]) (f :: k -> *).
SListI xs =>
(forall (a :: k). f a) -> NP f xs
pure_NP = Proxy Top -> (forall (a :: k). Top a => f a) -> NP f xs
forall {k} (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP (forall {k} (t :: k). Proxy t
forall (t :: k -> Constraint). Proxy t
Proxy @Top)

cpure_NP :: forall c xs proxy f. All c xs
         => proxy c -> (forall a. c a => f a) -> NP f xs
cpure_NP :: forall {k} (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP proxy c
_ forall (a :: k). c a => f a
f = SList xs -> NP f xs
forall (xs' :: [k]). All c xs' => SList xs' -> NP f xs'
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: All c xs' => SList xs' -> NP f xs'
    go :: forall (xs' :: [k]). All c xs' => SList xs' -> NP f xs'
go SList xs'
SNil  = NP f xs'
NP f '[]
forall {k} (f :: k -> *). NP f '[]
Nil
    go SList xs'
SCons = f x
forall (a :: k). c a => f a
f f x -> NP f xs -> NP f (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP f xs -> NP f (x : xs)
:* SList xs -> NP f xs
forall (xs' :: [k]). All c xs' => SList xs' -> NP f xs'
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList

collapse_NP :: NP (K a) xs -> [a]
collapse_NP :: forall {k} a (xs :: [k]). NP (K a) xs -> [a]
collapse_NP = NP (K a) xs -> [a]
forall {k} a (xs :: [k]). NP (K a) xs -> [a]
go
  where
    go :: NP (K a) xs -> [a]
    go :: forall {k} a (xs :: [k]). NP (K a) xs -> [a]
go NP (K a) xs
Nil         = []
    go (K a
x :* NP (K a) xs
xs) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: NP (K a) xs -> [a]
forall {k} a (xs :: [k]). NP (K a) xs -> [a]
go NP (K a) xs
xs

ctraverse'_NP  ::
     forall c proxy xs f f' g. (All c xs,  Applicative g)
  => proxy c -> (forall a. c a => f a -> g (f' a)) -> NP f xs  -> g (NP f' xs)
ctraverse'_NP :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
ctraverse'_NP proxy c
_ forall (a :: k). c a => f a -> g (f' a)
f = NP f xs -> g (NP f' xs)
forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys)
go
  where
    go :: All c ys => NP f ys -> g (NP f' ys)
    go :: forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys)
go NP f ys
Nil       = NP f' ys -> g (NP f' ys)
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NP f' ys
NP f' '[]
forall {k} (f :: k -> *). NP f '[]
Nil
    go (f x
x :* NP f xs
xs) = f' x -> NP f' xs -> NP f' ys
f' x -> NP f' xs -> NP f' (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP f xs -> NP f (x : xs)
(:*) (f' x -> NP f' xs -> NP f' ys)
-> g (f' x) -> g (NP f' xs -> NP 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 (NP f' xs -> NP f' ys) -> g (NP f' xs) -> g (NP 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
<*> NP f xs -> g (NP f' xs)
forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys)
go NP f xs
xs

ctraverse__NP ::
     forall c proxy xs f g. (All c xs, Applicative g)
  => proxy c -> (forall a. c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP proxy c
_ forall (a :: k). c a => f a -> g ()
f = NP f xs -> g ()
forall (ys :: [k]). All c ys => NP f ys -> g ()
go
  where
    go :: All c ys => NP f ys -> g ()
    go :: forall (ys :: [k]). All c ys => NP f ys -> g ()
go NP f ys
Nil       = () -> g ()
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    go (f x
x :* NP f xs
xs) = f x -> g ()
forall (a :: k). c a => f a -> g ()
f f x
x g () -> g () -> g ()
forall a b. g a -> g b -> g b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> NP f xs -> g ()
forall (ys :: [k]). All c ys => NP f ys -> g ()
go NP f xs
xs

traverse__NP ::
     forall xs f g. (SListI xs, Applicative g)
  => (forall a. f a -> g ()) -> NP f xs -> g ()
traverse__NP :: forall {k} (xs :: [k]) (f :: k -> *) (g :: * -> *).
(SListI xs, Applicative g) =>
(forall (a :: k). f a -> g ()) -> NP f xs -> g ()
traverse__NP = Proxy Top
-> (forall (a :: k). Top a => f a -> g ()) -> NP f xs -> g ()
forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP (forall {k} (t :: k). Proxy t
forall (t :: k -> Constraint). Proxy t
Proxy @Top)

trans_NP ::
     AllZip c xs ys
  => proxy c
  -> (forall x y . c x y => f x -> g y)
  -> NP f xs -> NP g ys
trans_NP :: forall {k} {k} (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP proxy c
_ forall (x :: k) (y :: k). c x y => f x -> g y
_t NP f xs
Nil       = NP g ys
NP g '[]
forall {k} (f :: k -> *). NP f '[]
Nil
trans_NP proxy c
p  forall (x :: k) (y :: k). c x y => f x -> g y
t (f x
x :* NP f xs
xs) = f x -> g (Head ys)
forall (x :: k) (y :: k). c x y => f x -> g y
t f x
x g (Head ys) -> NP g (Tail ys) -> NP g (Head ys : Tail ys)
forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP f xs -> NP f (x : xs)
:* proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g (Tail ys)
forall {k} {k} (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP proxy c
p f x -> g y
forall (x :: k) (y :: k). c x y => f x -> g y
t NP f xs
xs

coerce_NP ::
     forall f g xs ys .
     AllZip (LiftedCoercible f g) xs ys
  => NP f xs -> NP g ys
coerce_NP :: forall {k} {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
AllZip (LiftedCoercible f g) xs ys =>
NP f xs -> NP g ys
coerce_NP = Proxy (LiftedCoercible f g)
-> (forall (x :: k) (y :: k).
    LiftedCoercible f g x y =>
    f x -> g y)
-> NP f xs
-> NP g ys
forall {k} {k} (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP (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

-- | Version of 'map_NP' that does not require a singleton
map_NP' :: forall f g xs. (forall a. f a -> g a) -> NP f xs -> NP g xs
map_NP' :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
(forall (a :: k). f a -> g a) -> NP f xs -> NP g xs
map_NP' forall (a :: k). f a -> g a
f = NP f xs -> NP g xs
forall (xs' :: [k]). NP f xs' -> NP g xs'
go
  where
    go :: NP f xs' -> NP g xs'
    go :: forall (xs' :: [k]). NP f xs' -> NP g xs'
go NP f xs'
Nil       = NP g xs'
NP g '[]
forall {k} (f :: k -> *). NP f '[]
Nil
    go (f x
x :* NP f xs
xs) = f x -> g x
forall (a :: k). f a -> g a
f f x
x g x -> NP g xs -> NP g (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP f xs -> NP f (x : xs)
:* NP f xs -> NP g xs
forall (xs' :: [k]). NP f xs' -> NP g xs'
go NP f xs
xs

-- | Conjure up an 'SListI' constraint from an 'NP'
npToSListI :: NP a xs -> (SListI xs => r) -> r
npToSListI :: forall {k} (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP a xs
np = SList xs -> (SListI xs => r) -> r
forall {k} (xs :: [k]) r. SList xs -> (SListI xs => r) -> r
sListToSListI (SList xs -> (SListI xs => r) -> r)
-> SList xs -> (SListI xs => r) -> r
forall a b. (a -> b) -> a -> b
$ NP a xs -> SList xs
forall {k} (a :: k -> *) (xs :: [k]). NP a xs -> SList xs
npToSList NP a xs
np
  where
    sListToSListI :: SList xs -> (SListI xs => r) -> r
    sListToSListI :: forall {k} (xs :: [k]) r. SList xs -> (SListI xs => r) -> r
sListToSListI SList xs
SNil  SListI xs => r
k = r
SListI xs => r
k
    sListToSListI SList xs
SCons SListI xs => r
k = r
SListI xs => r
k

    npToSList :: NP a xs -> SList xs
    npToSList :: forall {k} (a :: k -> *) (xs :: [k]). NP a xs -> SList xs
npToSList NP a xs
Nil       = SList xs
SList '[]
forall {k}. SList '[]
SNil
    npToSList (a x
_ :* NP a xs
xs) = SList xs -> (SListI xs => SList xs) -> SList xs
forall {k} (xs :: [k]) r. SList xs -> (SListI xs => r) -> r
sListToSListI (NP a xs -> SList xs
forall {k} (a :: k -> *) (xs :: [k]). NP a xs -> SList xs
npToSList NP a xs
xs) SList xs
SList (x : xs)
SListI xs => SList xs
forall {k} (xs :: [k]) (x :: k). SListI xs => SList (x : xs)
SCons

instance HPure NP where
  hpure :: forall (xs :: [k]) (f :: k -> *).
SListIN NP xs =>
(forall (a :: k). f a) -> NP f xs
hpure  = (forall (a :: k). f a) -> NP f xs
forall {k} (xs :: [k]) (f :: k -> *).
SListI xs =>
(forall (a :: k). f a) -> NP f xs
pure_NP
  hcpure :: forall (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
AllN NP c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
hcpure = proxy c -> (forall (a :: k). c a => f a) -> NP f xs
forall {k} (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP

instance HAp NP where
  hap :: forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
hap = Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
NP (f -.-> g) xs -> NP f xs -> NP g xs
forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP

instance HCollapse NP where
  hcollapse :: forall (xs :: [k]) a.
SListIN NP xs =>
NP (K a) xs -> CollapseTo NP a
hcollapse = NP (K a) xs -> [a]
NP (K a) xs -> CollapseTo NP a
forall {k} a (xs :: [k]). NP (K a) xs -> [a]
collapse_NP

instance HSequence NP where
  hctraverse' :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *)
       (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
(AllN NP c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
hctraverse' = proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
ctraverse'_NP
  htraverse' :: forall (xs :: [k]) (g :: * -> *) (f :: k -> *) (f' :: k -> *).
(SListIN NP xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs)
htraverse'  = Proxy Top
-> (forall (a :: k). Top a => f a -> g (f' a))
-> NP f xs
-> g (NP 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 NP c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP 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 NP xs, Applicative f) =>
NP (f :.: g) xs -> f (NP g xs)
hsequence'  = (forall (a :: k). (:.:) f g a -> f (g a))
-> NP (f :.: g) xs -> f (NP g xs)
forall (xs :: [k]) (g :: * -> *) (f :: k -> *) (f' :: k -> *).
(SListIN NP xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP 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

instance HTraverse_ NP where
  hctraverse_ :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *)
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(AllN NP c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
hctraverse_ = proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP
  htraverse_ :: forall (xs :: [k]) (g :: * -> *) (f :: k -> *).
(SListIN NP xs, Applicative g) =>
(forall (a :: k). f a -> g ()) -> NP f xs -> g ()
htraverse_  = (forall (a :: k). f a -> g ()) -> NP f xs -> g ()
forall {k} (xs :: [k]) (f :: k -> *) (g :: * -> *).
(SListI xs, Applicative g) =>
(forall (a :: k). f a -> g ()) -> NP f xs -> g ()
traverse__NP

instance HTrans NP NP where
  htrans :: forall (c :: k1 -> k2 -> Constraint) (xs :: [k1]) (ys :: [k2])
       (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *)
       (g :: k2 -> *).
AllZipN (Prod NP) c xs ys =>
proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> NP f xs
-> NP g ys
htrans = proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> NP f xs
-> NP g ys
forall {k} {k} (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP
  hcoerce :: forall (f :: k1 -> *) (g :: k2 -> *) (xs :: [k1]) (ys :: [k2]).
AllZipN (Prod NP) (LiftedCoercible f g) xs ys =>
NP f xs -> NP g ys
hcoerce = NP f xs -> NP g ys
forall {k} {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
AllZip (LiftedCoercible f g) xs ys =>
NP f xs -> NP g ys
coerce_NP

-- | Copied from sop-core
--
-- Not derived, since derived instance ignores associativity info
instance All (Show `Compose` f) xs => Show (NP f xs) where
  showsPrec :: Int -> NP f xs -> ShowS
showsPrec Int
_ NP f xs
Nil       = String -> ShowS
showString String
"Nil"
  showsPrec Int
d (f x
f :* NP f xs
fs) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5)
                        (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> f x -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
5 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) f x
f
                        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :* "
                        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NP f xs -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
5 NP f xs
fs

deriving instance  All (Eq `Compose` f) xs                            => Eq  (NP f xs)
deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NP f xs)

instance All (Compose NoThunks f) xs
      => NoThunks (NP (f :: k -> Type) (xs :: [k])) where
  showTypeOf :: Proxy (NP f xs) -> String
showTypeOf Proxy (NP f xs)
_ = String
"NP"
  wNoThunks :: Context -> NP f xs -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt = \case
      NP f xs
Nil     -> Maybe ThunkInfo -> IO (Maybe ThunkInfo)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ThunkInfo
forall a. Maybe a
Nothing
      f x
x :* NP f xs
xs -> [IO (Maybe ThunkInfo)] -> IO (Maybe ThunkInfo)
allNoThunks [
                     Context -> f x -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
noThunks (String
"fst" String -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctxt) f x
x
                   , Context -> NP f xs -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
noThunks (String
"snd" String -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctxt) NP f xs
xs
                   ]