-----------------------------------------------------------------------------
-- |
-- Module      :  Generics.OneLiner.Internal
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
{-# LANGUAGE
    GADTs
  , DataKinds
  , PolyKinds
  , RankNTypes
  , LinearTypes
  , TypeFamilies
  , TypeOperators
  , ConstraintKinds
  , TypeApplications
  , FlexibleContexts
  , FlexibleInstances
  , AllowAmbiguousTypes
  , ScopedTypeVariables
  , UndecidableInstances
  , MultiParamTypeClasses
  #-}
module Generics.OneLiner.Internal where

import GHC.Generics hiding (from, to, from1, to1)
import qualified GHC.Generics as G
import GHC.Types (Constraint)
import Data.Functor.Identity
import Data.Kind (Type)
import Data.Profunctor.Linear (Profunctor(..))
import Data.Proxy
import Prelude (Functor(..), Applicative(..), ($), (.), (+))
import Prelude.Linear hiding (zero, ($), (.), (+))
import qualified Unsafe.Linear as Unsafe

import Generics.OneLiner.Classes

to :: Generic a => Rep a x %1-> a
to :: forall a x. Generic a => Rep a x %1 -> a
to = (Rep a x -> a) %1 -> Rep a x %1 -> a
forall a b (p :: Multiplicity). (a %p -> b) %1 -> a %1 -> b
Unsafe.toLinear Rep a x -> a
forall a x. Generic a => Rep a x -> a
G.to
from :: Generic a => a %1-> Rep a x
from :: forall a x. Generic a => a %1 -> Rep a x
from = (a -> Rep a x) %1 -> a %1 -> Rep a x
forall a b (p :: Multiplicity). (a %p -> b) %1 -> a %1 -> b
Unsafe.toLinear a -> Rep a x
forall a x. Generic a => a -> Rep a x
G.from
to1 :: Generic1 f => Rep1 f x %1-> f x
to1 :: forall {k} (f :: k -> *) (x :: k). Generic1 f => Rep1 f x %1 -> f x
to1 = (Rep1 f x -> f x) %1 -> Rep1 f x %1 -> f x
forall a b (p :: Multiplicity). (a %p -> b) %1 -> a %1 -> b
Unsafe.toLinear Rep1 f x -> f x
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
G.to1
from1 :: Generic1 f => f x %1-> Rep1 f x
from1 :: forall {k} (f :: k -> *) (x :: k). Generic1 f => f x %1 -> Rep1 f x
from1 = (f x -> Rep1 f x) %1 -> f x %1 -> Rep1 f x
forall a b (p :: Multiplicity). (a %p -> b) %1 -> a %1 -> b
Unsafe.toLinear f x -> Rep1 f x
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
G.from1

type family Constraints' (t :: Type -> Type) (t' :: Type -> Type) (c :: Type -> Type -> Constraint) (c1 :: (Type -> Type) -> (Type -> Type) -> Constraint) :: Constraint
type instance Constraints' V1 V1 c c1 = ()
type instance Constraints' U1 U1 c c1 = ()
type instance Constraints' (f :+: g) (f' :+: g') c c1 = (Constraints' f f' c c1, Constraints' g g' c c1)
type instance Constraints' (f :*: g) (f' :*: g') c c1 = (Constraints' f f' c c1, Constraints' g g' c c1)
type instance Constraints' (f :.: g) (f' :.: g') c c1 = (c1 f f', Constraints' g g' c c1)
type instance Constraints' Par1 Par1 c c1 = ()
type instance Constraints' (Rec1 f) (Rec1 g) c c1 = c1 f g
type instance Constraints' (K1 i a) (K1 i' b) c c1 = c a b
type instance Constraints' (M1 i t f) (M1 i' t' f') c c1 = Constraints' f f' c c1

type ADT' = ADT_ Identity Proxy ADTProfunctor
type ADTNonEmpty' = ADT_ Identity Proxy NonEmptyProfunctor
type ADTRecord' = ADT_ Identity Proxy RecordProfunctor

type ADT1' t t' = (ADT_ Identity Identity ADTProfunctor t t', ADT_ Proxy Identity ADT1Profunctor t t')
type ADTNonEmpty1' t t' = (ADT_ Identity Identity NonEmptyProfunctor t t', ADT_ Proxy Identity NonEmptyProfunctor t t')
type ADTRecord1' t t' = (ADT_ Identity Identity RecordProfunctor t t', ADT_ Proxy Identity RecordProfunctor t t')

type ADTProfunctor = GenericEmptyProfunctor ': NonEmptyProfunctor
type ADT1Profunctor = GenericConstantProfunctor ': ADTProfunctor
type NonEmptyProfunctor = GenericSumProfunctor ': RecordProfunctor
type RecordProfunctor = '[GenericProductProfunctor, GenericUnitProfunctor, Profunctor]

type family Satisfies (p :: Type -> Type -> Type) (ks :: [(Type -> Type -> Type) -> Constraint]) :: Constraint
type instance Satisfies p (k ': ks) = (k p, Satisfies p ks)
type instance Satisfies p '[] = ()

class (ks :: [(Type -> Type -> Type) -> Constraint]) |- (k :: (Type -> Type -> Type) -> Constraint) where
  implies :: Satisfies p ks => (k p => p a b) -> p a b

instance {-# OVERLAPPABLE #-} ks |- k => (_k ': ks) |- k where
  implies :: forall (p :: * -> * -> *) a b.
Satisfies p (_k : ks) =>
(k p => p a b) -> p a b
implies = forall (ks :: [(* -> * -> *) -> Constraint])
       (k :: (* -> * -> *) -> Constraint) (p :: * -> * -> *) a b.
(ks |- k, Satisfies p ks) =>
(k p => p a b) -> p a b
implies @ks @k
  {-# INLINE implies #-}

instance (k ': _ks) |- k where
  implies :: forall (p :: * -> * -> *) a b.
Satisfies p (k : _ks) =>
(k p => p a b) -> p a b
implies k p => p a b
p = p a b
k p => p a b
p
  {-# INLINE implies #-}

generic' :: forall ks c p t t' a b. (ADT_ Identity Proxy ks t t', Constraints' t t' c AnyType, Satisfies p ks)
         => (forall s s'. c s s' => p s s')
         -> p (t a) (t' b)
generic' :: forall (ks :: [(* -> * -> *) -> Constraint])
       (c :: * -> * -> Constraint) (p :: * -> * -> *) (t :: * -> *)
       (t' :: * -> *) a b.
(ADT_ Identity Proxy ks t t', Constraints' t t' c AnyType,
 Satisfies p ks) =>
(forall s s'. c s s' => p s s') -> p (t a) (t' b)
generic' forall s s'. c s s' => p s s'
f = forall (nullary :: * -> *) (unary :: * -> *)
       (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) (t' :: * -> *)
       (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(ADT_ nullary unary ks t t', Constraints' t t' c c1,
 Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (t a) (t' b)
generic_ @Identity @Proxy @ks (forall {k} (t :: k). Proxy t
forall {t :: * -> * -> Constraint}. Proxy t
Proxy @c) (p s s' -> Identity (p s s')
forall a. a -> Identity a
Identity p s s'
forall s s'. c s s' => p s s'
f) (forall {k} (t :: k). Proxy t
forall {t :: (* -> *) -> (* -> *) -> Constraint}. Proxy t
Proxy @AnyType) forall {k} (t :: k). Proxy t
forall (r1 :: * -> *) (s1 :: * -> *) d e.
AnyType r1 s1 =>
Proxy (p d e -> p (r1 d) (s1 e))
Proxy Proxy (p a b)
forall {k} (t :: k). Proxy t
Proxy
{-# INLINE generic' #-}

generic1' :: forall ks c1 p t t' a b. (ADT_ Proxy Identity ks t t', Constraints' t t' AnyType c1, Satisfies p ks)
           => (forall s s' d e. c1 s s' => p d e -> p (s d) (s' e))
           -> p a b
           -> p (t a) (t' b)
generic1' :: forall (ks :: [(* -> * -> *) -> Constraint])
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADT_ Proxy Identity ks t t', Constraints' t t' AnyType c1,
 Satisfies p ks) =>
(forall (s :: * -> *) (s' :: * -> *) d e.
 c1 s s' =>
 p d e -> p (s d) (s' e))
-> p a b -> p (t a) (t' b)
generic1' forall (s :: * -> *) (s' :: * -> *) d e.
c1 s s' =>
p d e -> p (s d) (s' e)
f p a b
p = forall (nullary :: * -> *) (unary :: * -> *)
       (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) (t' :: * -> *)
       (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(ADT_ nullary unary ks t t', Constraints' t t' c c1,
 Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (t a) (t' b)
generic_ @Proxy @Identity @ks (forall {k} (t :: k). Proxy t
forall {t :: * -> * -> Constraint}. Proxy t
Proxy @AnyType) forall {k} (t :: k). Proxy t
forall s s'. AnyType s s' => Proxy (p s s')
Proxy (forall {k} (t :: k). Proxy t
forall {t :: (* -> *) -> (* -> *) -> Constraint}. Proxy t
Proxy @c1) ((p d e -> p (r1 d) (s1 e)) -> Identity (p d e -> p (r1 d) (s1 e))
forall a. a -> Identity a
Identity p d e -> p (r1 d) (s1 e)
forall (s :: * -> *) (s' :: * -> *) d e.
c1 s s' =>
p d e -> p (s d) (s' e)
f) (p a b -> Identity (p a b)
forall a. a -> Identity a
Identity p a b
p)
{-# INLINE generic1' #-}

generic01' :: forall ks c0 c1 p t t' a b. (ADT_ Identity Identity ks t t', Constraints' t t' c0 c1, Satisfies p ks)
          => (forall s s'. c0 s s' => p s s')
          -> (forall s s' d e. c1 s s' => p d e -> p (s d) (s' e))
          -> p a b
          -> p (t a) (t' b)
generic01' :: forall (ks :: [(* -> * -> *) -> Constraint])
       (c0 :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADT_ Identity Identity ks t t', Constraints' t t' c0 c1,
 Satisfies p ks) =>
(forall s s'. c0 s s' => p s s')
-> (forall (s :: * -> *) (s' :: * -> *) d e.
    c1 s s' =>
    p d e -> p (s d) (s' e))
-> p a b
-> p (t a) (t' b)
generic01' forall s s'. c0 s s' => p s s'
k forall (s :: * -> *) (s' :: * -> *) d e.
c1 s s' =>
p d e -> p (s d) (s' e)
f p a b
p = forall (nullary :: * -> *) (unary :: * -> *)
       (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) (t' :: * -> *)
       (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(ADT_ nullary unary ks t t', Constraints' t t' c c1,
 Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (t a) (t' b)
generic_ @Identity @Identity @ks (forall {k} (t :: k). Proxy t
forall {t :: * -> * -> Constraint}. Proxy t
Proxy @c0) (p s s' -> Identity (p s s')
forall a. a -> Identity a
Identity p s s'
forall s s'. c0 s s' => p s s'
k) (forall {k} (t :: k). Proxy t
forall {t :: (* -> *) -> (* -> *) -> Constraint}. Proxy t
Proxy @c1) ((p d e -> p (r1 d) (s1 e)) -> Identity (p d e -> p (r1 d) (s1 e))
forall a. a -> Identity a
Identity p d e -> p (r1 d) (s1 e)
forall (s :: * -> *) (s' :: * -> *) d e.
c1 s s' =>
p d e -> p (s d) (s' e)
f) (p a b -> Identity (p a b)
forall a. a -> Identity a
Identity p a b
p)
{-# INLINE generic01' #-}

class ADT_ (nullary :: Type -> Type) (unary :: Type -> Type) (ks :: [(Type -> Type -> Type) -> Constraint]) (t :: Type -> Type) (t' :: Type -> Type) where
  generic_ :: forall c c1 p a b. (Constraints' t t' c c1, Satisfies p ks)
           => Proxy c
           -> (forall s s'. c s s' => nullary (p s s'))
           -> Proxy c1
           -> (forall r1 s1 d e. c1 r1 s1 => unary (p d e -> p (r1 d) (s1 e)))
           -> unary (p a b)
           -> p (t a) (t' b)

instance ks |- GenericEmptyProfunctor => ADT_ nullary unary ks V1 V1 where
  generic_ :: forall (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(Constraints' V1 V1 c c1, Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (V1 a) (V1 b)
generic_ Proxy c
_ forall s s'. c s s' => nullary (p s s')
_ Proxy c1
_ forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
_ unary (p a b)
_ = forall (ks :: [(* -> * -> *) -> Constraint])
       (k :: (* -> * -> *) -> Constraint) (p :: * -> * -> *) a b.
(ks |- k, Satisfies p ks) =>
(k p => p a b) -> p a b
implies @ks @GenericEmptyProfunctor GenericEmptyProfunctor p => p (V1 a) (V1 b)
forall (p :: * -> * -> *) a a'.
GenericEmptyProfunctor p =>
p (V1 a) (V1 a')
zero
  {-# INLINE generic_ #-}

instance ks |- GenericUnitProfunctor => ADT_ nullary unary ks U1 U1 where
  generic_ :: forall (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(Constraints' U1 U1 c c1, Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (U1 a) (U1 b)
generic_ Proxy c
_ forall s s'. c s s' => nullary (p s s')
_ Proxy c1
_ forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
_ unary (p a b)
_ = forall (ks :: [(* -> * -> *) -> Constraint])
       (k :: (* -> * -> *) -> Constraint) (p :: * -> * -> *) a b.
(ks |- k, Satisfies p ks) =>
(k p => p a b) -> p a b
implies @ks @GenericUnitProfunctor GenericUnitProfunctor p => p (U1 a) (U1 b)
forall (p :: * -> * -> *) a a'.
GenericUnitProfunctor p =>
p (U1 a) (U1 a')
unit
  {-# INLINE generic_ #-}

instance (ks |- GenericSumProfunctor, ADT_ nullary unary ks f f', ADT_ nullary unary ks g g') => ADT_ nullary unary ks (f :+: g) (f' :+: g') where
  generic_ :: forall (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(Constraints' (f :+: g) (f' :+: g') c c1, Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p ((:+:) f g a) ((:+:) f' g' b)
generic_ Proxy c
for forall s s'. c s s' => nullary (p s s')
f Proxy c1
for1 forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
f1 unary (p a b)
p1 = forall (ks :: [(* -> * -> *) -> Constraint])
       (k :: (* -> * -> *) -> Constraint) (p :: * -> * -> *) a b.
(ks |- k, Satisfies p ks) =>
(k p => p a b) -> p a b
implies @ks @GenericSumProfunctor
    (p (f a) (f' b) -> p (g a) (g' b) -> p ((:+:) f g a) ((:+:) f' g' b)
forall (p :: * -> * -> *) (f :: * -> *) a (f' :: * -> *) a'
       (g :: * -> *) (g' :: * -> *).
GenericSumProfunctor p =>
p (f a) (f' a')
-> p (g a) (g' a') -> p ((:+:) f g a) ((:+:) f' g' a')
plus (forall (nullary :: * -> *) (unary :: * -> *)
       (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) (t' :: * -> *)
       (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(ADT_ nullary unary ks t t', Constraints' t t' c c1,
 Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (t a) (t' b)
generic_ @nullary @unary @ks Proxy c
for forall s s'. c s s' => nullary (p s s')
f Proxy c1
for1 forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
f1 unary (p a b)
p1) (forall (nullary :: * -> *) (unary :: * -> *)
       (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) (t' :: * -> *)
       (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(ADT_ nullary unary ks t t', Constraints' t t' c c1,
 Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (t a) (t' b)
generic_ @nullary @unary @ks Proxy c
for forall s s'. c s s' => nullary (p s s')
f Proxy c1
for1 forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
f1 unary (p a b)
p1))
  {-# INLINE generic_ #-}

instance (ks |- GenericProductProfunctor, ADT_ nullary unary ks f f', ADT_ nullary unary ks g g') => ADT_ nullary unary ks (f :*: g) (f' :*: g') where
  generic_ :: forall (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(Constraints' (f :*: g) (f' :*: g') c c1, Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p ((:*:) f g a) ((:*:) f' g' b)
generic_ Proxy c
for forall s s'. c s s' => nullary (p s s')
f Proxy c1
for1 forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
f1 unary (p a b)
p1 = forall (ks :: [(* -> * -> *) -> Constraint])
       (k :: (* -> * -> *) -> Constraint) (p :: * -> * -> *) a b.
(ks |- k, Satisfies p ks) =>
(k p => p a b) -> p a b
implies @ks @GenericProductProfunctor
    (p (f a) (f' b) -> p (g a) (g' b) -> p ((:*:) f g a) ((:*:) f' g' b)
forall (p :: * -> * -> *) (f :: * -> *) a (f' :: * -> *) a'
       (g :: * -> *) (g' :: * -> *).
GenericProductProfunctor p =>
p (f a) (f' a')
-> p (g a) (g' a') -> p ((:*:) f g a) ((:*:) f' g' a')
mult (forall (nullary :: * -> *) (unary :: * -> *)
       (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) (t' :: * -> *)
       (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(ADT_ nullary unary ks t t', Constraints' t t' c c1,
 Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (t a) (t' b)
generic_ @nullary @unary @ks Proxy c
for forall s s'. c s s' => nullary (p s s')
f Proxy c1
for1 forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
f1 unary (p a b)
p1) (forall (nullary :: * -> *) (unary :: * -> *)
       (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) (t' :: * -> *)
       (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(ADT_ nullary unary ks t t', Constraints' t t' c c1,
 Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (t a) (t' b)
generic_ @nullary @unary @ks Proxy c
for forall s s'. c s s' => nullary (p s s')
f Proxy c1
for1 forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
f1 unary (p a b)
p1))
  {-# INLINE generic_ #-}

instance ks |- Profunctor => ADT_ Identity unary ks (K1 i v) (K1 i' v') where
  generic_ :: forall (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(Constraints' (K1 i v) (K1 i' v') c c1, Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => Identity (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (K1 i v a) (K1 i' v' b)
generic_ Proxy c
_ forall s s'. c s s' => Identity (p s s')
f Proxy c1
_ forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
_ unary (p a b)
_ = forall (ks :: [(* -> * -> *) -> Constraint])
       (k :: (* -> * -> *) -> Constraint) (p :: * -> * -> *) a b.
(ks |- k, Satisfies p ks) =>
(k p => p a b) -> p a b
implies @ks @Profunctor ((K1 i v a %1 -> v)
-> (v' %1 -> K1 i' v' b) -> p v v' -> p (K1 i v a) (K1 i' v' b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap (\(K1 v
x) -> v
x) v' %1 -> K1 i' v' b
forall k i c (p :: k). c -> K1 i c p
K1 (Identity (p v v') -> p v v'
forall a. Identity a -> a
runIdentity Identity (p v v')
forall s s'. c s s' => Identity (p s s')
f))
  {-# INLINE generic_ #-}

instance ks |- GenericConstantProfunctor => ADT_ Proxy unary ks (K1 i v) (K1 i' v) where
  generic_ :: forall (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(Constraints' (K1 i v) (K1 i' v) c c1, Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => Proxy (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (K1 i v a) (K1 i' v b)
generic_ Proxy c
_ forall s s'. c s s' => Proxy (p s s')
_ Proxy c1
_ forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
_ unary (p a b)
_ = forall (ks :: [(* -> * -> *) -> Constraint])
       (k :: (* -> * -> *) -> Constraint) (p :: * -> * -> *) a b.
(ks |- k, Satisfies p ks) =>
(k p => p a b) -> p a b
implies @ks @GenericConstantProfunctor ((K1 i v a %1 -> v)
-> (v %1 -> K1 i' v b) -> p v v -> p (K1 i v a) (K1 i' v b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap (\(K1 v
x) -> v
x) v %1 -> K1 i' v b
forall k i c (p :: k). c -> K1 i c p
K1 p v v
forall (p :: * -> * -> *) c. GenericConstantProfunctor p => p c c
identity)
  {-# INLINE generic_ #-}

instance (ks |- Profunctor, ADT_ nullary unary ks f f') => ADT_ nullary unary ks (M1 i c f) (M1 i' c' f') where
  generic_ :: forall (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(Constraints' (M1 i c f) (M1 i' c' f') c c1, Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (M1 i c f a) (M1 i' c' f' b)
generic_ Proxy c
for forall s s'. c s s' => nullary (p s s')
f Proxy c1
for1 forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
f1 unary (p a b)
p1 = forall (ks :: [(* -> * -> *) -> Constraint])
       (k :: (* -> * -> *) -> Constraint) (p :: * -> * -> *) a b.
(ks |- k, Satisfies p ks) =>
(k p => p a b) -> p a b
implies @ks @Profunctor
    ((M1 i c f a %1 -> f a)
-> (f' b %1 -> M1 i' c' f' b)
-> p (f a) (f' b)
-> p (M1 i c f a) (M1 i' c' f' b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap (\(M1 f a
x) -> f a
x) f' b %1 -> M1 i' c' f' b
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (nullary :: * -> *) (unary :: * -> *)
       (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) (t' :: * -> *)
       (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(ADT_ nullary unary ks t t', Constraints' t t' c c1,
 Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (t a) (t' b)
generic_ @nullary @unary @ks Proxy c
for forall s s'. c s s' => nullary (p s s')
f Proxy c1
for1 forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
unary (p d e -> p (r1 d) (s1 e))
f1 unary (p a b)
p1))
  {-# INLINE generic_ #-}

instance (ks |- Profunctor, ADT_ nullary Identity ks g g') => ADT_ nullary Identity ks (f :.: g) (f' :.: g') where
  generic_ :: forall (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(Constraints' (f :.: g) (f' :.: g') c c1, Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    Identity (p d e -> p (r1 d) (s1 e)))
-> Identity (p a b)
-> p ((:.:) f g a) ((:.:) f' g' b)
generic_ Proxy c
for forall s s'. c s s' => nullary (p s s')
f Proxy c1
for1 forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
Identity (p d e -> p (r1 d) (s1 e))
f1 Identity (p a b)
p1 = forall (ks :: [(* -> * -> *) -> Constraint])
       (k :: (* -> * -> *) -> Constraint) (p :: * -> * -> *) a b.
(ks |- k, Satisfies p ks) =>
(k p => p a b) -> p a b
implies @ks @Profunctor
    (((:.:) f g a %1 -> f (g a))
-> (f' (g' b) %1 -> (:.:) f' g' b)
-> p (f (g a)) (f' (g' b))
-> p ((:.:) f g a) ((:.:) f' g' b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap (\(Comp1 f (g a)
x) -> f (g a)
x) f' (g' b) %1 -> (:.:) f' g' b
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (p (f (g a)) (f' (g' b)) -> p ((:.:) f g a) ((:.:) f' g' b))
-> p (f (g a)) (f' (g' b)) -> p ((:.:) f g a) ((:.:) f' g' b)
forall a b. (a -> b) -> a -> b
$ Identity (p (g a) (g' b) -> p (f (g a)) (f' (g' b)))
-> p (g a) (g' b) -> p (f (g a)) (f' (g' b))
forall a. Identity a -> a
runIdentity Identity (p (g a) (g' b) -> p (f (g a)) (f' (g' b)))
forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
Identity (p d e -> p (r1 d) (s1 e))
f1 (forall (nullary :: * -> *) (unary :: * -> *)
       (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) (t' :: * -> *)
       (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(ADT_ nullary unary ks t t', Constraints' t t' c c1,
 Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    unary (p d e -> p (r1 d) (s1 e)))
-> unary (p a b)
-> p (t a) (t' b)
generic_ @nullary @Identity @ks Proxy c
for forall s s'. c s s' => nullary (p s s')
f Proxy c1
for1 forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
Identity (p d e -> p (r1 d) (s1 e))
f1 Identity (p a b)
p1))
  {-# INLINE generic_ #-}

instance ks |- Profunctor => ADT_ nullary Identity ks Par1 Par1 where
  generic_ :: forall (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(Constraints' Par1 Par1 c c1, Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    Identity (p d e -> p (r1 d) (s1 e)))
-> Identity (p a b)
-> p (Par1 a) (Par1 b)
generic_ Proxy c
_ forall s s'. c s s' => nullary (p s s')
_ Proxy c1
_ forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
Identity (p d e -> p (r1 d) (s1 e))
_ Identity (p a b)
p = forall (ks :: [(* -> * -> *) -> Constraint])
       (k :: (* -> * -> *) -> Constraint) (p :: * -> * -> *) a b.
(ks |- k, Satisfies p ks) =>
(k p => p a b) -> p a b
implies @ks @Profunctor
    ((Par1 a %1 -> a)
-> (b %1 -> Par1 b) -> p a b -> p (Par1 a) (Par1 b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap (\(Par1 a
x) -> a
x) b %1 -> Par1 b
forall p. p -> Par1 p
Par1 (Identity (p a b) -> p a b
forall a. Identity a -> a
runIdentity Identity (p a b)
p))
  {-# INLINE generic_ #-}

instance ks |- Profunctor => ADT_ nullary Identity ks (Rec1 f) (Rec1 f') where
  generic_ :: forall (c :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *) a b.
(Constraints' (Rec1 f) (Rec1 f') c c1, Satisfies p ks) =>
Proxy c
-> (forall s s'. c s s' => nullary (p s s'))
-> Proxy c1
-> (forall (r1 :: * -> *) (s1 :: * -> *) d e.
    c1 r1 s1 =>
    Identity (p d e -> p (r1 d) (s1 e)))
-> Identity (p a b)
-> p (Rec1 f a) (Rec1 f' b)
generic_ Proxy c
_ forall s s'. c s s' => nullary (p s s')
_ Proxy c1
_ forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
Identity (p d e -> p (r1 d) (s1 e))
f Identity (p a b)
p = forall (ks :: [(* -> * -> *) -> Constraint])
       (k :: (* -> * -> *) -> Constraint) (p :: * -> * -> *) a b.
(ks |- k, Satisfies p ks) =>
(k p => p a b) -> p a b
implies @ks @Profunctor
    ((Rec1 f a %1 -> f a)
-> (f' b %1 -> Rec1 f' b)
-> p (f a) (f' b)
-> p (Rec1 f a) (Rec1 f' b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap (\(Rec1 f a
x) -> f a
x) f' b %1 -> Rec1 f' b
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (Identity (p (f a) (f' b)) -> p (f a) (f' b)
forall a. Identity a -> a
runIdentity (Identity (p a b -> p (f a) (f' b))
forall (r1 :: * -> *) (s1 :: * -> *) d e.
c1 r1 s1 =>
Identity (p d e -> p (r1 d) (s1 e))
f Identity (p a b -> p (f a) (f' b))
-> Identity (p a b) -> Identity (p (f a) (f' b))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Identity (p a b)
p)))
  {-# INLINE generic_ #-}


data Ctor a b = Ctor { forall {k} a (b :: k). Ctor a b -> a -> Int
index :: a -> Int, forall {k} a (b :: k). Ctor a b -> Int
count :: Int }
instance Profunctor Ctor where
  dimap :: forall s a b t. (s %1 -> a) -> (b %1 -> t) -> Ctor a b -> Ctor s t
dimap s %1 -> a
l b %1 -> t
_ (Ctor a -> Int
i Int
c) = (s -> Int) -> Int -> Ctor s t
forall {k} a (b :: k). (a -> Int) -> Int -> Ctor a b
Ctor (a -> Int
i (a -> Int) -> (s -> a) -> s -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s %1 -> a) %1 -> s -> a
forall a b. (a %1 -> b) %1 -> a -> b
forget s %1 -> a
l) Int
c
  {-# INLINE dimap #-}
instance GenericUnitProfunctor Ctor where
  unit :: forall a a'. Ctor (U1 a) (U1 a')
unit = (U1 a -> Int) -> Int -> Ctor (U1 a) (U1 a')
forall {k} a (b :: k). (a -> Int) -> Int -> Ctor a b
Ctor (Int %1 -> U1 a -> Int
forall a b. a %1 -> b -> a
const Int
0) Int
1
  {-# INLINE unit #-}
instance GenericProductProfunctor Ctor where
  mult :: forall (f :: * -> *) a (f' :: * -> *) a' (g :: * -> *)
       (g' :: * -> *).
Ctor (f a) (f' a')
-> Ctor (g a) (g' a') -> Ctor ((:*:) f g a) ((:*:) f' g' a')
mult Ctor (f a) (f' a')
_ Ctor (g a) (g' a')
_ = ((:*:) f g a -> Int) -> Int -> Ctor ((:*:) f g a) ((:*:) f' g' a')
forall {k} a (b :: k). (a -> Int) -> Int -> Ctor a b
Ctor (Int %1 -> (:*:) f g a -> Int
forall a b. a %1 -> b -> a
const Int
0) Int
1
  {-# INLINE mult #-}
instance GenericSumProfunctor Ctor where
  plus :: forall (f :: * -> *) a (f' :: * -> *) a' (g :: * -> *)
       (g' :: * -> *).
Ctor (f a) (f' a')
-> Ctor (g a) (g' a') -> Ctor ((:+:) f g a) ((:+:) f' g' a')
plus Ctor (f a) (f' a')
l Ctor (g a) (g' a')
r = ((:+:) f g a -> Int) -> Int -> Ctor ((:+:) f g a) ((:+:) f' g' a')
forall {k} a (b :: k). (a -> Int) -> Int -> Ctor a b
Ctor ((f a -> Int) -> (g a -> Int) -> (:+:) f g a -> Int
forall (f :: * -> *) a b (m :: Multiplicity) (g :: * -> *).
(f a %m -> b) -> (g a %m -> b) -> (:+:) f g a %m -> b
e1 (Ctor (f a) (f' a') -> f a -> Int
forall {k} a (b :: k). Ctor a b -> a -> Int
index Ctor (f a) (f' a')
l) ((Ctor (f a) (f' a') -> Int
forall {k} a (b :: k). Ctor a b -> Int
count Ctor (f a) (f' a')
l Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ) (Int -> Int) -> (g a -> Int) -> g a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctor (g a) (g' a') -> g a -> Int
forall {k} a (b :: k). Ctor a b -> a -> Int
index Ctor (g a) (g' a')
r)) (Ctor (f a) (f' a') -> Int
forall {k} a (b :: k). Ctor a b -> Int
count Ctor (f a) (f' a')
l Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Ctor (g a) (g' a') -> Int
forall {k} a (b :: k). Ctor a b -> Int
count Ctor (g a) (g' a')
r)
  {-# INLINE plus #-}
instance GenericEmptyProfunctor Ctor where
  zero :: forall a a'. Ctor (V1 a) (V1 a')
zero = (V1 a -> Int) -> Int -> Ctor (V1 a) (V1 a')
forall {k} a (b :: k). (a -> Int) -> Int -> Ctor a b
Ctor (Int %1 -> V1 a -> Int
forall a b. a %1 -> b -> a
const Int
0) Int
0
  {-# INLINE zero #-}
instance GenericConstantProfunctor Ctor where
  identity :: forall c. Ctor c c
identity = (c -> Int) -> Int -> Ctor c c
forall {k} a (b :: k). (a -> Int) -> Int -> Ctor a b
Ctor (Int %1 -> c -> Int
forall a b. a %1 -> b -> a
const Int
0) Int
1
  {-# INLINE identity #-}

record :: forall c p t t'. (ADTRecord t t', Constraints t t' c, GenericRecordProfunctor p)
       => (forall s s'. c s s' => p s s') -> p t t'
record :: forall (c :: * -> * -> Constraint) (p :: * -> * -> *) t t'.
(ADTRecord t t', Constraints t t' c, GenericRecordProfunctor p) =>
(forall s s'. c s s' => p s s') -> p t t'
record forall s s'. c s s' => p s s'
f = (t %1 -> Rep t Any)
-> (Rep t' Any %1 -> t') -> p (Rep t Any) (Rep t' Any) -> p t t'
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap t %1 -> Rep t Any
forall a x. Generic a => a %1 -> Rep a x
from Rep t' Any %1 -> t'
forall a x. Generic a => Rep a x %1 -> a
to (p (Rep t Any) (Rep t' Any) -> p t t')
-> p (Rep t Any) (Rep t' Any) -> p t t'
forall a b. (a -> b) -> a -> b
$ forall (ks :: [(* -> * -> *) -> Constraint])
       (c :: * -> * -> Constraint) (p :: * -> * -> *) (t :: * -> *)
       (t' :: * -> *) a b.
(ADT_ Identity Proxy ks t t', Constraints' t t' c AnyType,
 Satisfies p ks) =>
(forall s s'. c s s' => p s s') -> p (t a) (t' b)
generic' @RecordProfunctor @c forall s s'. c s s' => p s s'
f
{-# INLINE record #-}

record1 :: forall c p t t' a b. (ADTRecord1 t t', Constraints1 t t' c, GenericRecordProfunctor p)
        => (forall d e s s'. c s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
record1 :: forall (c :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADTRecord1 t t', Constraints1 t t' c,
 GenericRecordProfunctor p) =>
(forall d e (s :: * -> *) (s' :: * -> *).
 c s s' =>
 p d e -> p (s d) (s' e))
-> p a b -> p (t a) (t' b)
record1 forall d e (s :: * -> *) (s' :: * -> *).
c s s' =>
p d e -> p (s d) (s' e)
f p a b
p = (t a %1 -> Rep1 t a)
-> (Rep1 t' b %1 -> t' b)
-> p (Rep1 t a) (Rep1 t' b)
-> p (t a) (t' b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap t a %1 -> Rep1 t a
forall {k} (f :: k -> *) (x :: k). Generic1 f => f x %1 -> Rep1 f x
from1 Rep1 t' b %1 -> t' b
forall {k} (f :: k -> *) (x :: k). Generic1 f => Rep1 f x %1 -> f x
to1 (p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b))
-> p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b)
forall a b. (a -> b) -> a -> b
$ forall (ks :: [(* -> * -> *) -> Constraint])
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADT_ Proxy Identity ks t t', Constraints' t t' AnyType c1,
 Satisfies p ks) =>
(forall (s :: * -> *) (s' :: * -> *) d e.
 c1 s s' =>
 p d e -> p (s d) (s' e))
-> p a b -> p (t a) (t' b)
generic1' @RecordProfunctor @c forall d e (s :: * -> *) (s' :: * -> *).
c s s' =>
p d e -> p (s d) (s' e)
forall (s :: * -> *) (s' :: * -> *) d e.
c s s' =>
p d e -> p (s d) (s' e)
f p a b
p
{-# INLINE record1 #-}

record01 :: forall c0 c1 p t t' a b. (ADTRecord1 t t', Constraints01 t t' c0 c1, GenericRecordProfunctor p)
         => (forall s s'. c0 s s' => p s s') -> (forall d e s s'. c1 s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
record01 :: forall (c0 :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADTRecord1 t t', Constraints01 t t' c0 c1,
 GenericRecordProfunctor p) =>
(forall s s'. c0 s s' => p s s')
-> (forall d e (s :: * -> *) (s' :: * -> *).
    c1 s s' =>
    p d e -> p (s d) (s' e))
-> p a b
-> p (t a) (t' b)
record01 forall s s'. c0 s s' => p s s'
k forall d e (s :: * -> *) (s' :: * -> *).
c1 s s' =>
p d e -> p (s d) (s' e)
f p a b
p = (t a %1 -> Rep1 t a)
-> (Rep1 t' b %1 -> t' b)
-> p (Rep1 t a) (Rep1 t' b)
-> p (t a) (t' b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap t a %1 -> Rep1 t a
forall {k} (f :: k -> *) (x :: k). Generic1 f => f x %1 -> Rep1 f x
from1 Rep1 t' b %1 -> t' b
forall {k} (f :: k -> *) (x :: k). Generic1 f => Rep1 f x %1 -> f x
to1 (p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b))
-> p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b)
forall a b. (a -> b) -> a -> b
$ forall (ks :: [(* -> * -> *) -> Constraint])
       (c0 :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADT_ Identity Identity ks t t', Constraints' t t' c0 c1,
 Satisfies p ks) =>
(forall s s'. c0 s s' => p s s')
-> (forall (s :: * -> *) (s' :: * -> *) d e.
    c1 s s' =>
    p d e -> p (s d) (s' e))
-> p a b
-> p (t a) (t' b)
generic01' @RecordProfunctor @c0 @c1 forall s s'. c0 s s' => p s s'
k forall d e (s :: * -> *) (s' :: * -> *).
c1 s s' =>
p d e -> p (s d) (s' e)
forall (s :: * -> *) (s' :: * -> *) d e.
c1 s s' =>
p d e -> p (s d) (s' e)
f p a b
p
{-# INLINE record01 #-}

nonEmpty :: forall c p t t'. (ADTNonEmpty t t', Constraints t t' c, GenericNonEmptyProfunctor p)
         => (forall s s'. c s s' => p s s') -> p t t'
nonEmpty :: forall (c :: * -> * -> Constraint) (p :: * -> * -> *) t t'.
(ADTNonEmpty t t', Constraints t t' c,
 GenericNonEmptyProfunctor p) =>
(forall s s'. c s s' => p s s') -> p t t'
nonEmpty forall s s'. c s s' => p s s'
f = (t %1 -> Rep t Any)
-> (Rep t' Any %1 -> t') -> p (Rep t Any) (Rep t' Any) -> p t t'
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap t %1 -> Rep t Any
forall a x. Generic a => a %1 -> Rep a x
from Rep t' Any %1 -> t'
forall a x. Generic a => Rep a x %1 -> a
to (p (Rep t Any) (Rep t' Any) -> p t t')
-> p (Rep t Any) (Rep t' Any) -> p t t'
forall a b. (a -> b) -> a -> b
$ forall (ks :: [(* -> * -> *) -> Constraint])
       (c :: * -> * -> Constraint) (p :: * -> * -> *) (t :: * -> *)
       (t' :: * -> *) a b.
(ADT_ Identity Proxy ks t t', Constraints' t t' c AnyType,
 Satisfies p ks) =>
(forall s s'. c s s' => p s s') -> p (t a) (t' b)
generic' @NonEmptyProfunctor @c forall s s'. c s s' => p s s'
f
{-# INLINE nonEmpty #-}

nonEmpty1 :: forall c p t t' a b. (ADTNonEmpty1 t t', Constraints1 t t' c, GenericNonEmptyProfunctor p)
          => (forall d e s s'. c s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
nonEmpty1 :: forall (c :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADTNonEmpty1 t t', Constraints1 t t' c,
 GenericNonEmptyProfunctor p) =>
(forall d e (s :: * -> *) (s' :: * -> *).
 c s s' =>
 p d e -> p (s d) (s' e))
-> p a b -> p (t a) (t' b)
nonEmpty1 forall d e (s :: * -> *) (s' :: * -> *).
c s s' =>
p d e -> p (s d) (s' e)
f p a b
p = (t a %1 -> Rep1 t a)
-> (Rep1 t' b %1 -> t' b)
-> p (Rep1 t a) (Rep1 t' b)
-> p (t a) (t' b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap t a %1 -> Rep1 t a
forall {k} (f :: k -> *) (x :: k). Generic1 f => f x %1 -> Rep1 f x
from1 Rep1 t' b %1 -> t' b
forall {k} (f :: k -> *) (x :: k). Generic1 f => Rep1 f x %1 -> f x
to1 (p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b))
-> p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b)
forall a b. (a -> b) -> a -> b
$ forall (ks :: [(* -> * -> *) -> Constraint])
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADT_ Proxy Identity ks t t', Constraints' t t' AnyType c1,
 Satisfies p ks) =>
(forall (s :: * -> *) (s' :: * -> *) d e.
 c1 s s' =>
 p d e -> p (s d) (s' e))
-> p a b -> p (t a) (t' b)
generic1' @NonEmptyProfunctor @c forall d e (s :: * -> *) (s' :: * -> *).
c s s' =>
p d e -> p (s d) (s' e)
forall (s :: * -> *) (s' :: * -> *) d e.
c s s' =>
p d e -> p (s d) (s' e)
f p a b
p
{-# INLINE nonEmpty1 #-}

nonEmpty01 :: forall c0 c1 p t t' a b. (ADTNonEmpty1 t t', Constraints01 t t' c0 c1, GenericNonEmptyProfunctor p)
           => (forall s s'. c0 s s' => p s s') -> (forall d e s s'. c1 s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
nonEmpty01 :: forall (c0 :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADTNonEmpty1 t t', Constraints01 t t' c0 c1,
 GenericNonEmptyProfunctor p) =>
(forall s s'. c0 s s' => p s s')
-> (forall d e (s :: * -> *) (s' :: * -> *).
    c1 s s' =>
    p d e -> p (s d) (s' e))
-> p a b
-> p (t a) (t' b)
nonEmpty01 forall s s'. c0 s s' => p s s'
k forall d e (s :: * -> *) (s' :: * -> *).
c1 s s' =>
p d e -> p (s d) (s' e)
f p a b
p = (t a %1 -> Rep1 t a)
-> (Rep1 t' b %1 -> t' b)
-> p (Rep1 t a) (Rep1 t' b)
-> p (t a) (t' b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap t a %1 -> Rep1 t a
forall {k} (f :: k -> *) (x :: k). Generic1 f => f x %1 -> Rep1 f x
from1 Rep1 t' b %1 -> t' b
forall {k} (f :: k -> *) (x :: k). Generic1 f => Rep1 f x %1 -> f x
to1 (p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b))
-> p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b)
forall a b. (a -> b) -> a -> b
$ forall (ks :: [(* -> * -> *) -> Constraint])
       (c0 :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADT_ Identity Identity ks t t', Constraints' t t' c0 c1,
 Satisfies p ks) =>
(forall s s'. c0 s s' => p s s')
-> (forall (s :: * -> *) (s' :: * -> *) d e.
    c1 s s' =>
    p d e -> p (s d) (s' e))
-> p a b
-> p (t a) (t' b)
generic01' @NonEmptyProfunctor @c0 @c1 forall s s'. c0 s s' => p s s'
k forall d e (s :: * -> *) (s' :: * -> *).
c1 s s' =>
p d e -> p (s d) (s' e)
forall (s :: * -> *) (s' :: * -> *) d e.
c1 s s' =>
p d e -> p (s d) (s' e)
f p a b
p
{-# INLINE nonEmpty01 #-}

generic :: forall c p t t'. (ADT t t', Constraints t t' c, GenericProfunctor p)
        => (forall s s'. c s s' => p s s') -> p t t'
generic :: forall (c :: * -> * -> Constraint) (p :: * -> * -> *) t t'.
(ADT t t', Constraints t t' c, GenericProfunctor p) =>
(forall s s'. c s s' => p s s') -> p t t'
generic forall s s'. c s s' => p s s'
f = (t %1 -> Rep t Any)
-> (Rep t' Any %1 -> t') -> p (Rep t Any) (Rep t' Any) -> p t t'
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap t %1 -> Rep t Any
forall a x. Generic a => a %1 -> Rep a x
from Rep t' Any %1 -> t'
forall a x. Generic a => Rep a x %1 -> a
to (p (Rep t Any) (Rep t' Any) -> p t t')
-> p (Rep t Any) (Rep t' Any) -> p t t'
forall a b. (a -> b) -> a -> b
$ forall (ks :: [(* -> * -> *) -> Constraint])
       (c :: * -> * -> Constraint) (p :: * -> * -> *) (t :: * -> *)
       (t' :: * -> *) a b.
(ADT_ Identity Proxy ks t t', Constraints' t t' c AnyType,
 Satisfies p ks) =>
(forall s s'. c s s' => p s s') -> p (t a) (t' b)
generic' @ADTProfunctor @c forall s s'. c s s' => p s s'
f
{-# INLINE generic #-}

generic1 :: forall c p t t' a b. (ADT1 t t', Constraints1 t t' c, Generic1Profunctor p)
         => (forall d e s s'. c s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
generic1 :: forall (c :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADT1 t t', Constraints1 t t' c, Generic1Profunctor p) =>
(forall d e (s :: * -> *) (s' :: * -> *).
 c s s' =>
 p d e -> p (s d) (s' e))
-> p a b -> p (t a) (t' b)
generic1 forall d e (s :: * -> *) (s' :: * -> *).
c s s' =>
p d e -> p (s d) (s' e)
f p a b
p = (t a %1 -> Rep1 t a)
-> (Rep1 t' b %1 -> t' b)
-> p (Rep1 t a) (Rep1 t' b)
-> p (t a) (t' b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap t a %1 -> Rep1 t a
forall {k} (f :: k -> *) (x :: k). Generic1 f => f x %1 -> Rep1 f x
from1 Rep1 t' b %1 -> t' b
forall {k} (f :: k -> *) (x :: k). Generic1 f => Rep1 f x %1 -> f x
to1 (p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b))
-> p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b)
forall a b. (a -> b) -> a -> b
$ forall (ks :: [(* -> * -> *) -> Constraint])
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADT_ Proxy Identity ks t t', Constraints' t t' AnyType c1,
 Satisfies p ks) =>
(forall (s :: * -> *) (s' :: * -> *) d e.
 c1 s s' =>
 p d e -> p (s d) (s' e))
-> p a b -> p (t a) (t' b)
generic1' @ADT1Profunctor @c forall d e (s :: * -> *) (s' :: * -> *).
c s s' =>
p d e -> p (s d) (s' e)
forall (s :: * -> *) (s' :: * -> *) d e.
c s s' =>
p d e -> p (s d) (s' e)
f p a b
p
{-# INLINE generic1 #-}

generic01 :: forall c0 c1 p t t' a b. (ADT1 t t', Constraints01 t t' c0 c1, GenericProfunctor p)
          => (forall s s'. c0 s s' => p s s') -> (forall d e s s'. c1 s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
generic01 :: forall (c0 :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADT1 t t', Constraints01 t t' c0 c1, GenericProfunctor p) =>
(forall s s'. c0 s s' => p s s')
-> (forall d e (s :: * -> *) (s' :: * -> *).
    c1 s s' =>
    p d e -> p (s d) (s' e))
-> p a b
-> p (t a) (t' b)
generic01 forall s s'. c0 s s' => p s s'
k forall d e (s :: * -> *) (s' :: * -> *).
c1 s s' =>
p d e -> p (s d) (s' e)
f p a b
p = (t a %1 -> Rep1 t a)
-> (Rep1 t' b %1 -> t' b)
-> p (Rep1 t a) (Rep1 t' b)
-> p (t a) (t' b)
forall (arr :: * -> * -> *) s a b t.
Profunctor arr =>
(s %1 -> a) -> (b %1 -> t) -> arr a b -> arr s t
dimap t a %1 -> Rep1 t a
forall {k} (f :: k -> *) (x :: k). Generic1 f => f x %1 -> Rep1 f x
from1 Rep1 t' b %1 -> t' b
forall {k} (f :: k -> *) (x :: k). Generic1 f => Rep1 f x %1 -> f x
to1 (p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b))
-> p (Rep1 t a) (Rep1 t' b) -> p (t a) (t' b)
forall a b. (a -> b) -> a -> b
$ forall (ks :: [(* -> * -> *) -> Constraint])
       (c0 :: * -> * -> Constraint)
       (c1 :: (* -> *) -> (* -> *) -> Constraint) (p :: * -> * -> *)
       (t :: * -> *) (t' :: * -> *) a b.
(ADT_ Identity Identity ks t t', Constraints' t t' c0 c1,
 Satisfies p ks) =>
(forall s s'. c0 s s' => p s s')
-> (forall (s :: * -> *) (s' :: * -> *) d e.
    c1 s s' =>
    p d e -> p (s d) (s' e))
-> p a b
-> p (t a) (t' b)
generic01' @ADTProfunctor @c0 @c1 forall s s'. c0 s s' => p s s'
k forall d e (s :: * -> *) (s' :: * -> *).
c1 s s' =>
p d e -> p (s d) (s' e)
forall (s :: * -> *) (s' :: * -> *) d e.
c1 s s' =>
p d e -> p (s d) (s' e)
f p a b
p
{-# INLINE generic01 #-}

-- | `Constraints` is a constraint type synonym, containing the constraint
-- requirements for an instance for `t` of class `c`.
-- It requires an instance of class `c` for each component of `t`.
type Constraints t t' c = Constraints' (Rep t) (Rep t') c AnyType

type Constraints1 t t' c = Constraints' (Rep1 t) (Rep1 t') AnyType c

type Constraints01 t t' c0 c1 = Constraints' (Rep1 t) (Rep1 t') c0 c1

-- | `ADTRecord` is a constraint type synonym. An instance is an `ADT` with *exactly* one constructor.
type ADTRecord t t' = (Generic t, Generic t', ADTRecord' (Rep t) (Rep t'), Constraints t t' AnyType)

type ADTRecord1 t t' = (Generic1 t, Generic1 t', ADTRecord1' (Rep1 t) (Rep1 t'), Constraints1 t t' AnyType)

-- | `ADTNonEmpty` is a constraint type synonym. An instance is an `ADT` with *at least* one constructor.
type ADTNonEmpty t t' = (Generic t, Generic t', ADTNonEmpty' (Rep t) (Rep t'), Constraints t t' AnyType)

type ADTNonEmpty1 t t' = (Generic1 t, Generic1 t', ADTNonEmpty1' (Rep1 t) (Rep1 t'), Constraints1 t t' AnyType)

-- | `ADT` is a constraint type synonym. The `Generic` instance can be derived,
-- and any generic representation will be an instance of `ADT'` and `AnyType`.
type ADT t t' = (Generic t, Generic t', ADT' (Rep t) (Rep t'), Constraints t t' AnyType)

type ADT1 t t' = (Generic1 t, Generic1 t', ADT1' (Rep1 t) (Rep1 t'), Constraints1 t t' AnyType)

class AnyType a b
instance AnyType a b

-- | The result type of a curried function.
--
-- If @r@ is not a function type (i.e., does not unify with `_ -> _`):
--
-- @
-- `FunResult` (a -> r) ~ r
-- `FunResult` (a -> b -> r) ~ r
-- `FunResult` (a -> b -> c -> r) ~ r
-- @
type family FunResult t where
  FunResult (a -> b) = FunResult b
  FunResult r = r

-- | Automatically apply a lifted function to a polymorphic argument as
-- many times as possible.
--
-- A constraint `FunConstraint c t` is equivalent to the conjunction of
-- constraints `c s` for every argument type of `t`.
--
-- If @r@ is not a function type:
--
-- @
-- c a :- FunConstraints c (a -> r)
-- (c a, c b) :- FunConstraints c (a -> b -> r)
-- (c a, c b, c d) :- FunConstraints c (a -> b -> d -> r)
-- @
class FunConstraints c t where
  autoApply :: Applicative f => (forall s. c s => f s) -> f t -> f (FunResult t)

instance {-# OVERLAPPING #-} (c a, FunConstraints c b) => FunConstraints c (a -> b) where
  autoApply :: forall (f :: * -> *).
Applicative f =>
(forall s. c s => f s) -> f (a -> b) -> f (FunResult (a -> b))
autoApply forall s. c s => f s
run f (a -> b)
f = forall (c :: * -> Constraint) t (f :: * -> *).
(FunConstraints c t, Applicative f) =>
(forall s. c s => f s) -> f t -> f (FunResult t)
autoApply @c forall s. c s => f s
run (f (a -> b)
f f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f a
forall s. c s => f s
run)
  {-# INLINE autoApply #-}

instance FunResult r ~ r => FunConstraints c r where
  autoApply :: forall (f :: * -> *).
Applicative f =>
(forall s. c s => f s) -> f r -> f (FunResult r)
autoApply forall s. c s => f s
_run f r
r = f r
f (FunResult r)
r
  {-# INLINE autoApply #-}


data Pair a = Pair a a
instance Functor Pair where
  fmap :: forall a b. (a -> b) -> Pair a -> Pair b
fmap a -> b
f (Pair a
a a
b) = b -> b -> Pair b
forall a. a -> a -> Pair a
Pair (a -> b
f a
a) (a -> b
f a
b)
  {-# INLINE fmap #-}

infixr 9 .:
(.:) :: (c -> d) -> (a -> b -> c) -> (a -> b -> d)
.: :: forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
(.:) = ((b -> c) -> b -> d) -> (a -> b -> c) -> a -> b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) (((b -> c) -> b -> d) -> (a -> b -> c) -> a -> b -> d)
-> ((c -> d) -> (b -> c) -> b -> d)
-> (c -> d)
-> (a -> b -> c)
-> a
-> b
-> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> d) -> (b -> c) -> b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)
{-# INLINE (.:) #-}