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