Category.hs

{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE NoStarIsType #-}

{-# OPTIONS_GHC -Wall #-}

-- {-# OPTIONS_GHC -fno-warn-unused-imports #-}  -- TEMP
{-# OPTIONS_GHC -fconstraint-solver-iterations=10 #-} -- for Oks

-- For ConCat.Inline.ClassOp
{-# OPTIONS_GHC -fplugin=ConCat.Inline.Plugin #-}

-- {-# OPTIONS_GHC -ddump-simpl #-}

-- | Another go at constrained categories. This time without Prod, Coprod, Exp.

module ConCat.Category where

import Prelude hiding (id,(.),curry,uncurry,const,zip,unzip,zipWith,minimum,maximum)
import qualified Prelude as P
import Control.Arrow (Kleisli(..),arr)
import qualified Control.Arrow as A
import Control.Monad ((<=<))
import Data.Typeable (Typeable)
import GHC.Exts (Coercible,coerce)
import qualified GHC.Exts as X
import Data.Type.Equality ((:~:)(..))
import qualified Data.Type.Equality as Eq
import Data.Type.Coercion (Coercion(..))
import qualified Data.Type.Coercion as Co
import GHC.Types (Type)
import Data.Constraint hiding ((&&&),(***),(:=>))
-- import Debug.Trace
import Data.Monoid
import GHC.Generics (U1(..),Par1(..),(:*:)(..),(:.:)(..))
import GHC.TypeLits
import Control.Monad.Fix (MonadFix)
-- import Data.Proxy (Proxy)

import Data.Pointed
import Data.Key (Zip(..))
import Data.Distributive (Distributive(..))
import Data.Functor.Rep (Representable(..))
import Control.Newtype.Generics (Newtype(..))
import Data.Vector.Sized (Vector)
import Data.Finite.Internal (Finite(..))

import ConCat.Misc hiding ((<~),(~>),type (&&))
import ConCat.Rep hiding (Rep)
import ConCat.MinMax
import qualified ConCat.Rep as R
import ConCat.Additive
import qualified ConCat.Inline.ClassOp as IC

#define PINLINER(nm) {-# INLINE nm #-}
-- #define PINLINER(nm)

-- Prevents some subtle non-termination errors. See 2017-12-27 journal notes.
-- #define OPINLINE INLINE [0]

-- Changed to NOINLINE [0]. See 2017-12-29 journal notes.
#define OPINLINE NOINLINE [0]

{--------------------------------------------------------------------
    Unit and pairing for binary type constructors
--------------------------------------------------------------------}

-- Unit for binary type constructors
data U2 a b = U2 deriving (Show)

infixr 7 :**:
-- | Product for binary type constructors
data (p :**: q) a b = p a b :**: q a b

prod :: p a b :* q a b -> (p :**: q) a b
prod (p,q) = (p :**: q)

unProd :: (p :**: q) a b -> p a b :* q a b
unProd (p :**: q) = (p,q)

exl2 :: (p :**: q) a b -> p a b
exl2 = exl . unProd

exr2 :: (p :**: q) a b -> q a b
exr2 = exr . unProd

instance HasRep ((k :**: k') a b) where
  type Rep ((k :**: k') a b) = k a b :* k' a b
  abst (f,g) = f :**: g
  repr (f :**: g) = (f,g)

{--------------------------------------------------------------------
    Monoid wrapper
--------------------------------------------------------------------}

newtype Monoid2 m a b = Monoid2 m

{--------------------------------------------------------------------
    Constraints
--------------------------------------------------------------------}

class HasCon a where
  type Con a :: Constraint
  toDict :: a -> Dict (Con a)
  unDict :: Con a => a

newtype Sat kon a = Sat (Dict (kon a))

instance HasCon (Sat kon a) where
  type Con (Sat kon a) = kon a
  toDict (Sat d) = d
  unDict = Sat Dict

instance HasCon () where
  type Con () = ()
  toDict () = Dict
  unDict = ()

instance (HasCon a, HasCon b) => HasCon (a :* b) where
  type Con (a :* b) = (Con a,Con b)
  toDict (toDict -> Dict, toDict -> Dict) = Dict
  unDict = (unDict,unDict)

infixr 1 |-
newtype a |- b = Entail (Con a :- Con b)

instance Newtype (a |- b) where
  type O (a |- b) = Con a :- Con b
  pack e = Entail e
  unpack (Entail e) = e

instance Category (|-) where
  -- type Ok (|-) = HasCon
  id = pack refl
  (.) = inNew2 (\ g f -> Sub $ Dict \\ g \\ f)

instance OpCon (:*) (Sat HasCon) where
  inOp = Entail (Sub Dict)
  {-# INLINE inOp #-}

instance AssociativePCat (|-) where
  lassocP = pack (Sub Dict)
  rassocP = pack (Sub Dict)

instance MonoidalPCat (|-) where
  (***) = inNew2 $ \ f g -> Sub $ Dict \\ f \\ g

instance BraidedPCat (|-) where
  swapP = pack (Sub Dict)

instance ProductCat (|-) where
  -- type Prod (|-) = (:*)
  exl = pack (Sub Dict)
  exr = pack (Sub Dict)
  dup = pack (Sub Dict)
  -- (&&&) = inNew2 $ \ f g -> Sub $ Dict \\ f \\ g

infixl 1 <+

-- | Wrapper
(<+) :: Con a => (Con b => r) -> (a |- b) -> r
r <+ Entail (Sub Dict) = r
-- f <+ Entail e = f \\ e
{-# INLINE (<+) #-}

infixr 3 &&
-- (&&) = Prod (|-)
type (&&) = (:*)

class OpCon op con where
  inOp :: con a && con b |- con (a `op` b)
  -- default inOp :: (forall a b. (Con (con a), Con (con b)) => Con (con (a `op` b)))
  --              => con a && con b |- con (a `op` b)
  -- inOp = Entail (Sub Dict)

-- TODO: Look for a working type for this default inOp definition

-- class    OpCon op (Dict (kon a)) => OpCon' op kon a
-- instance OpCon op (Dict (kon a)) => OpCon' op kon a

-- class    kon a => Sat kon a
-- instance kon a => Sat kon a

yes1 :: c |- Sat Yes1 a
yes1 = Entail (Sub Dict)  -- Move to AltCat

forkCon :: forall con con' a. Sat (con &+& con') a |- Sat con a :* Sat con' a
forkCon = Entail (Sub Dict)

joinCon :: forall con con' a. Sat con a :* Sat con' a |- Sat (con &+& con') a
joinCon = Entail (Sub Dict)

inForkCon :: (Sat con1 a :* Sat con2 a |- Sat con1' b :* Sat con2' b)
          -> (Sat (con1 &+& con2) a |- Sat (con1' &+& con2') b)
inForkCon h = joinCon . h . forkCon

-- We might want forkCon, joinCon, and inForkCon elsewhere as well.
-- Consider renaming.

type Yes1' = Sat Yes1

type Ok' k = Sat (Ok k)

type OpSat op kon = OpCon op (Sat kon)

inSat :: OpCon op (Sat con) => Sat con a && Sat con b |- Sat con (a `op` b)
inSat = inOp

inOpL :: OpCon op con => (con a && con b) && con c |- con ((a `op` b) `op` c)
inOpL = inOp . first  inOp

inOpR :: OpCon op con => con a && (con b && con c) |- con (a `op` (b `op` c))
inOpR = inOp . second inOp

inOpL' :: OpCon op con
       => (con a && con b) && con c |- con (a `op` b) && con ((a `op` b) `op` c)
inOpL' = inOp . exl &&& inOpL
-- inOpL' = second inOp . rassocP . first (dup . inOp)

-- (con a && con b) && con c
-- con (a `op` b) && con c
-- (con (a `op` b) && con (a `op` b)) && con c
-- con (a `op` b) && (con (a `op` b) && con c)
-- con (a `op` b) && con ((a `op` b) `op` c)

inOpR' :: OpCon op con => con a && (con b && con c) |- con (a `op` (b `op` c)) &&  con (b `op` c)
inOpR' = inOpR &&& inOp . exr
-- inOpR' = first inOp . lassocP . second (dup . inOp)

-- There were mutual recursions between (a) inOpL' & rassocP, and (b) inOpR' & lassocP

inOpLR :: forall op con a b c. OpCon op con =>
  ((con a && con b) && con c) && (con a && (con b && con c))
  |- con ((a `op` b) `op` c) && con (a `op` (b `op` c))
inOpLR = inOpL *** inOpR

instance OpCon op Yes1' where
  inOp = Entail (Sub Dict)
  {-# INLINE inOp #-}

instance Typeable op => OpCon op (Sat Typeable) where
  inOp = Entail (Sub Dict)
  {-# INLINE inOp #-}

instance OpCon (:*) (Sat Eq) where
  inOp = Entail (Sub Dict)
  {-# INLINE inOp #-}

instance OpCon (:*) (Sat Ord) where
  inOp = Entail (Sub Dict)
  {-# INLINE inOp #-}

-- TODO: more OpCon instances for standard type classes

instance OpCon (:*) (Sat Additive) where
  inOp = Entail (Sub Dict)
  {-# INLINE inOp #-}

instance OpCon (:+) (Sat Eq) where
  inOp = Entail (Sub Dict)
  {-# INLINE inOp #-}

instance OpCon (:+) (Sat Ord) where
  inOp = Entail (Sub Dict)
  {-# INLINE inOp #-}

instance OpCon (->) (Sat Additive) where
  inOp = Entail (Sub Dict)
  {-# INLINE inOp #-}

class OkAdd k where okAdd :: Ok' k a |- Sat Additive a

type Ok2 k a b         = C2 (Ok k) a b
type Ok3 k a b c       = C3 (Ok k) a b c
type Ok4 k a b c d     = C4 (Ok k) a b c d
type Ok5 k a b c d e   = C5 (Ok k) a b c d e
type Ok6 k a b c d e f = C6 (Ok k) a b c d e f

type Oks k as = AllC (Ok k) as

-- I like the elegance of Oks, but it leads to complex dictionary expressions.
-- For now, use Okn for the operations introduced by lambda-to-ccc conversion.

class Show2 k where show2 :: a `k` b -> String

{--------------------------------------------------------------------
    Categories
--------------------------------------------------------------------}

class Category k where
  type Ok k :: Type -> Constraint
  type Ok k = Yes1
  id  :: Ok k a => a `k` a
  infixr 9 .
  (.) :: forall b c a. Ok3 k a b c => (b `k` c) -> (a `k` b) -> (a `k` c)

infixl 1 <~
infixr 1 ~>
-- | Add post- and pre-processing
(<~) :: (Category k, Oks k [a,b,a',b'])
     => (b `k` b') -> (a' `k` a) -> ((a `k` b) -> (a' `k` b'))
(h <~ f) g = h . g . f

-- | Add pre- and post-processing
(~>) :: (Category k, Oks k [a,b,a',b'])
     => (a' `k` a) -> (b `k` b') -> ((a `k` b) -> (a' `k` b'))
f ~> h = h <~ f

instance Category (->) where
  id  = P.id
  (.) = (P..)

instance Monad m => Category (Kleisli m) where
  id  = pack return
  (.) = inNew2 (<=<)

instance Category (:~:) where
  id  = Refl
  (.) = flip Eq.trans

instance Category Coercion where
  id  = Coercion
  (.) = flip Co.trans

instance Category U2 where
  id = U2
  U2 . U2 = U2

instance Monoid m => Category (Monoid2 m) where
  id = Monoid2 mempty
  Monoid2 m . Monoid2 n = Monoid2 (m `mappend` n)

instance (Category k, Category k') => Category (k :**: k') where
  type Ok (k :**: k') = Ok k &+& Ok k'
  id = id :**: id
  (g :**: g') . (f :**: f') = g.f :**: g'.f'
  PINLINER(id)
  PINLINER((.))

{--------------------------------------------------------------------
    Products
--------------------------------------------------------------------}

type Prod k = (:*)

infixr 3 ***, &&&

type OkProd k = OpCon (Prod k) (Ok' k)

okProd :: forall k a b. OkProd k
       => Ok' k a && Ok' k b |- Ok' k (Prod k a b)
okProd = inOp
{-# INLINE okProd #-}

class (Category k, OkProd k) => AssociativePCat k where
  lassocP :: forall a b c. Ok3 k a b c
          => Prod k a (Prod k b c) `k` Prod k (Prod k a b) c
  default lassocP :: forall a b c. (MProductCat k, Ok3 k a b c)
                  => Prod k a (Prod k b c) `k` Prod k (Prod k a b) c
  lassocP = second exl &&& (exr . exr)
            <+ okProd @k @a @b
            <+ inOpR' @(Prod k) @(Ok' k) @a @b @c
  {-# INLINE lassocP #-}
  rassocP :: forall a b c. Ok3 k a b c
          => Prod k (Prod k a b) c `k` Prod k a (Prod k b c)
  default rassocP :: forall a b c. (MProductCat k, Ok3 k a b c)
                  => Prod k (Prod k a b) c `k` Prod k a (Prod k b c)
  rassocP = (exl . exl) &&& first  exr
            <+ okProd @k    @b @c
            <+ inOpL' @(Prod k) @(Ok' k) @a @b @c
  {-# INLINE rassocP #-}

-- | Category with monoidal product.
class (Category k, OkProd k) => MonoidalPCat k where
  (***) :: forall a b c d. Ok4 k a b c d
        => (a `k` c) -> (b `k` d) -> (Prod k a b `k` Prod k c d)
  first :: forall a a' b. Ok3 k a b a'
        => (a `k` a') -> (Prod k a b `k` Prod k a' b)
  first = (*** id)
  {-# INLINE first #-}
  second :: forall a b b'. Ok3 k a b b'
         => (b `k` b') -> (Prod k a b `k` Prod k a b')
  second = (id ***)
  {-# INLINE second #-}

-- | Braided monoidal category
class (Category k, OkProd k {- , MonoidalPCat k -}) => BraidedPCat k where
  swapP :: forall a b. Ok2 k a b => Prod k a b `k` Prod k b a
  default swapP :: forall a b. (ProductCat k, MonoidalPCat k, Ok2 k a b)
                => Prod k a b `k` Prod k b a
  swapP = exr &&& exl
          <+ okProd @k @a @b
  {-# INLINE swapP #-}

type MBraidedPCat k = (BraidedPCat k, MonoidalPCat k)

-- | Category with product.
class (Category k, OkProd k) => ProductCat k where
  exl :: Ok2 k a b => Prod k a b `k` a
  exr :: Ok2 k a b => Prod k a b `k` b
  dup :: Ok  k a => a `k` Prod k a a

(&&&) :: forall k a c d. (MProductCat k, Ok3 k a c d)
      => (a `k` c) -> (a `k` d) -> (a `k` Prod k c d)
f &&& g = (f *** g) . dup
  <+ okProd @k @a @a
  <+ okProd @k @c @d
{-# INLINE (&&&) #-}

type MProductCat k = (ProductCat k, MonoidalPCat k)

instance AssociativePCat (->) where
  lassocP = \ (a,(b,c)) -> ((a,b),c)
  rassocP = \ ((a,b),c) -> (a,(b,c))
  
instance MonoidalPCat (->) where
  (***)  = (A.***)
  first  = A.first
  second = A.second

instance BraidedPCat (->) where
  swapP = \ (a,b) -> (b,a)

instance ProductCat (->) where
  -- type Prod (->) = (:*)
  exl = fst
  exr = snd
  dup = \ a -> (a,a)

-- TODO: do we want inline for (&&&), (***), first, and second?

instance MonoidalPCat U2 where
  U2 *** U2 = U2
  PINLINER((***))

instance BraidedPCat U2 where
  swapP = U2
  PINLINER(swapP)

instance ProductCat U2 where
  exl = U2
  exr = U2
  dup = U2
  -- U2 &&& U2 = U2
  PINLINER(exl)
  PINLINER(exr)
  PINLINER(dup)
  -- PINLINER((&&&))

instance (AssociativePCat k, AssociativePCat k') => AssociativePCat (k :**: k') where
  lassocP = lassocP :**: lassocP
  rassocP = rassocP :**: rassocP
  PINLINER(lassocP)
  PINLINER(rassocP)

instance (MonoidalPCat k, MonoidalPCat k') => MonoidalPCat (k :**: k') where
  (f :**: f') *** (g :**: g') = (f *** g) :**: (f' *** g')
  first (f :**: f') = first f :**: first f'
  second (f :**: f') = second f :**: second f'
  PINLINER((***))
  PINLINER(first)
  PINLINER(second)

instance (BraidedPCat k, BraidedPCat k') => BraidedPCat (k :**: k') where
  swapP = swapP :**: swapP
  PINLINER(swapP)

instance (ProductCat k, ProductCat k') => ProductCat (k :**: k') where
  exl = exl :**: exl
  exr = exr :**: exr
  dup = dup :**: dup
  PINLINER(exl)
  PINLINER(exr)
  PINLINER(dup)

instance Monad m => MonoidalPCat (Kleisli m) where
  (***) = (A.***)
  PINLINER((***))

instance Monad m => BraidedPCat (Kleisli m) where
  swapP = arr swapP

instance Monad m => ProductCat (Kleisli m) where
  -- type Prod (Kleisli m) = (:*)
  exl   = arr exl
  exr   = arr exr
  dup   = arr dup
  PINLINER(exl)
  PINLINER(exr)
  PINLINER(dup)

{--------------------------------------------------------------------
    Coproducts
--------------------------------------------------------------------}

type Coprod k = (:+)

type OkCoprod k = OpCon (Coprod k) (Ok' k)

okCoprod :: forall k a b. OkCoprod k
         => Ok' k a && Ok' k b |- Ok' k (Coprod k a b)
okCoprod = inOp
{-# INLINE okCoprod #-}

infixr 2 +++, |||

class (Category k, OkCoprod k) => AssociativeSCat k where
  lassocS :: forall a b c. Oks k [a,b,c]
          => Coprod k a (Coprod k b c) `k` Coprod k (Coprod k a b) c
  default lassocS :: forall a b c. (MCoproductCat k, Oks k [a,b,c])
                  => Coprod k a (Coprod k b c) `k` Coprod k (Coprod k a b) c
  lassocS = inl.inl ||| (inl.inr ||| inr)
            <+ inOpL' @(Coprod k) @(Ok' k) @a @b @c
            <+ okCoprod @k    @b @c
  {-# INLINE lassocS #-}
  rassocS :: forall a b c. Oks k [a,b,c]
          => Coprod k (Coprod k a b) c `k` Coprod k a (Coprod k b c)
  default rassocS :: forall a b c. (MCoproductCat k, Oks k [a,b,c])
                  => Coprod k (Coprod k a b) c `k` Coprod k a (Coprod k b c)
  rassocS = (inl ||| inr.inl) ||| inr.inr
            <+ inOpR' @(Coprod k) @(Ok' k) @a @b @c
            <+ okCoprod @k @a @b
  {-# INLINE rassocS #-}

class (Category k, OkCoprod k) => BraidedSCat k where
  swapS :: forall a b. Ok2 k a b => Coprod k a b `k` Coprod k b a
  default swapS :: forall a b. (MCoproductCat k, Ok2 k a b) => Coprod k a b `k` Coprod k b a
  swapS = inr ||| inl <+ okCoprod @k @b @a
  {-# INLINE swapS #-}

-- Monoidal category over sums
class (OkCoprod k, Category k) => MonoidalSCat k where
  (+++) :: forall a b c d. Ok4 k a b c d
        => (c `k` a) -> (d `k` b) -> (Coprod k c d `k` Coprod k a b)
  left  :: forall a a' b. Oks k [a,b,a']
        => (a `k` a') -> (Coprod k a b `k` Coprod k a' b)
  left  = (+++ id)
  {-# INLINE left #-}
  right :: forall a b b'. Oks k [a,b,b']
        => (b `k` b') -> (Coprod k a b `k` Coprod k a b')
  right = (id +++)
  {-# INLINE right #-}

-- | Category with coproduct.
class (Category k, OkCoprod k) => CoproductCat k where
  -- type Coprod k :: u -> u -> u
  -- type Coprod k = (:+)
  inl :: Ok2 k a b => a `k` Coprod k a b
  inr :: Ok2 k a b => b `k` Coprod k a b
  jam :: Ok k a => Coprod k a a `k` a

type MCoproductCat k = (CoproductCat k, MonoidalSCat k)

(|||) :: forall k a c d. (MCoproductCat k, Ok3 k a c d)
      => (c `k` a) -> (d `k` a) -> (Coprod k c d `k` a)
f ||| g = jam . (f +++ g)
        <+ okCoprod @k @a @a
        <+ okCoprod @k @c @d
{-# INLINE (|||) #-}

instance AssociativeSCat (->)

instance MonoidalSCat (->) where
  (+++) = (A.+++)
  left  = A.left
  right = A.right

instance BraidedSCat (->) where
  swapS = Right ||| Left

instance CoproductCat (->) where
  -- type Coprod (->) = (:+)
  inl = Left
  inr = Right
  jam = id `either` id

-- TODO: do we want inline for (|||), (+++), left, and right?

instance Monad m => MonoidalSCat (Kleisli m) where
  (+++) = inNew2 (\ f g -> (fmap Left ||| fmap Right) . (f +++ g))

-- f :: a -> m c
-- g :: b -> m d
-- f +++ g :: a :+ b -> m c :+ m d
-- fmap Left ||| fmap Right :: m c :+ m d -> m (c :+ d)

instance Monad m => BraidedSCat (Kleisli m) where
  swapS = arr swapS

instance Monad m => CoproductCat (Kleisli m) where
  inl = arr inl
  inr = arr inr
  jam = arr jam

-- f :: a -> m c
-- g :: b -> m c
-- h :: a :+ b -> m c

--   want :: a -> m (a :+ b)

instance MonoidalSCat U2 where
  U2 +++ U2 = U2

instance BraidedSCat U2 where swapS = U2

instance (BraidedSCat k, BraidedSCat k') => BraidedSCat (k :**: k') where
  swapS = swapS :**: swapS
  PINLINER(swapS)

instance CoproductCat U2 where
  inl = U2
  inr = U2
  jam = U2

instance (AssociativeSCat k, AssociativeSCat k') => AssociativeSCat (k :**: k') where
  lassocS = lassocS :**: lassocS
  rassocS = rassocS :**: rassocS
  PINLINER(lassocS)
  PINLINER(rassocS)

instance (MonoidalSCat k, MonoidalSCat k') => MonoidalSCat (k :**: k') where
  (f :**: f') +++ (g :**: g') = (f +++ g) :**: (f' +++ g')
  left (f :**: f') = left f :**: left f'
  right (f :**: f') = right f :**: right f'
  PINLINER((+++))
  PINLINER(left)
  PINLINER(right)

instance (CoproductCat k, CoproductCat k') => CoproductCat (k :**: k') where
  inl = inl :**: inl
  inr = inr :**: inr
  jam = jam :**: jam
  PINLINER(inl)
  PINLINER(inr)
  PINLINER(jam)

{--------------------------------------------------------------------
    Abelian categories
--------------------------------------------------------------------}

#if 1

type AbelianCat k =
  (MProductCat k, CoproductPCat k, TerminalCat k, CoterminalCat k, OkAdd k)

zeroC :: (AbelianCat k, Ok2 k a b) => a `k` b
zeroC = ti . it

plusC :: forall k a b. (AbelianCat k, Ok2 k a b) => Binop (a `k` b)
f `plusC` g = jamP . (f *** g) . dup
  <+ okProd @k @b @b
  <+ okProd @k @a @a
  <+ okAdd  @k @b

#else

class AbelianCat k where
  zeroC :: forall a b. (Ok2 k a b, Additive b) => a `k` b
  plusC :: forall a b. (Ok2 k a b, Additive b) => Binop (a `k` b)
  default plusC :: forall a b. (Ok2 k a b, Additive b, ProductCat k, CoproductPCat k)
                => Binop (a `k` b)
  -- Two reasonable defaults
#if 1
  f `plusC` g = (f |||| g) . dup <+ okProd @k @a @a
#else
  f `plusC` g = jamP . (f &&& g) <+ okProd @k @b @b
#endif

-- TODO: probably remove the Additive constraints here, but use OkAdd k in the
-- plusC default.

instance AbelianCat U2 where
  zeroC = U2
  U2 `plusC` U2 = U2

instance (AbelianCat k, AbelianCat k') => AbelianCat (k :**: k') where
  zeroC = zeroC :**: zeroC
  (f :**: f') `plusC` (g :**: g') = (f `plusC` g) :**: (f' `plusC` g')
  PINLINER(zeroC)
  PINLINER(plusC)

-- TODO: relate AbelianCat to ProductCat and CoproductPCat.
-- Also to IxProductCat and IxCoproductPCat.

#endif

{--------------------------------------------------------------------
    A dual to ProductCat. Temporary workaround.
--------------------------------------------------------------------}

-- TODO: eliminate CoproductPCat in favor of when we have associated products,
-- coproducts, etc.

type CoprodP k = Prod k

type OkCoprodP k = OkProd k

okCoprodP :: forall k a b. OkCoprodP k
           => Ok' k a && Ok' k b |- Ok' k (CoprodP k a b)
okCoprodP = inOp
{-# INLINE okCoprodP #-}

-- | Category with coproduct as Cartesian product.
class BraidedPCat k => CoproductPCat k where
  inlP :: Ok2 k a b => a `k` CoprodP k a b
  inrP :: Ok2 k a b => b `k` CoprodP k a b
  jamP :: Ok k a => CoprodP k a a `k` a

type MCoproductPCat k = (CoproductPCat k, MonoidalPCat k)

infixr 2 ||||

(||||) :: forall k a c d. (MCoproductPCat k, Ok3 k a c d)
       => (c `k` a) -> (d `k` a) -> (CoprodP k c d `k` a)
f |||| g = jamP . (f *** g)
         <+ okCoprodP @k @a @a
         <+ okCoprodP @k @c @d
{-# INLINE (||||) #-}


-- Don't bother with left, right, lassocS, rassocS, and misc helpers.

instance CoproductPCat U2 where
  inlP = U2
  inrP = U2
  jamP = U2

instance (CoproductPCat k, CoproductPCat k') => CoproductPCat (k :**: k') where
  inlP = inlP :**: inlP
  inrP = inrP :**: inrP
  jamP = jamP :**: jamP
  PINLINER(inlP)
  PINLINER(inrP)
  PINLINER(jamP)

-- Scalar multiplication

class ScalarCat k a where
  scale :: a -> (a `k` a)

instance Num a => ScalarCat (->) a where
  scale = (*)  -- I don't think I want to inline (*)
  PINLINER(scale)

instance ScalarCat U2 a where
  scale = const U2

instance (ScalarCat k a, ScalarCat k' a) => ScalarCat (k :**: k') a where
  scale s = scale s :**: scale s
  PINLINER(scale)

type LinearCat k a = (MProductCat k, CoproductPCat k, ScalarCat k a, Ok k a)

{--------------------------------------------------------------------
    Distributive
--------------------------------------------------------------------}

class DistribCat k where
  distl :: forall a u v. Ok3 k a u v
        => Prod k a (Coprod k u v) `k` Coprod k (Prod k a u) (Prod k a v)
  distr :: forall u v b. Ok3 k u v b
        => Prod k (Coprod k u v) b `k` Coprod k (Prod k u b) (Prod k v b)
  default distl :: forall a u v. (MonoidalSCat k, BraidedPCat k, Ok3 k a u v)
                => Prod k a (Coprod k u v) `k` Coprod k (Prod k a u) (Prod k a v)
  distl = (swapP +++ swapP) . distr . swapP
    <+ okProd   @k @(Coprod k u v) @a
    <+ okCoprod @k @(Prod k u a) @(Prod k v a)
    <+ okProd   @k @u @a
    <+ okProd   @k @v @a
    <+ okCoprod @k @(Prod k a u) @(Prod k a v)
    <+ okProd   @k @a @u
    <+ okProd   @k @a @v
    <+ okProd   @k @a @(Coprod k u v)
    <+ okCoprod @k @u @v
  {-# INLINE distl #-}
  default distr :: forall u v b. (MonoidalSCat k, BraidedPCat k, Ok3 k u v b)
                => Prod k (Coprod k u v) b `k` Coprod k (Prod k u b) (Prod k v b)
  distr = (swapP +++ swapP) . distl . swapP
    <+ okProd   @k @b @(Coprod k u v)
    <+ okCoprod @k @(Prod k b u) @(Prod k b v)
    <+ okProd   @k @b @u
    <+ okProd   @k @b @v
    <+ okCoprod @k @(Prod k u b) @(Prod k v b)
    <+ okProd   @k @u @b
    <+ okProd   @k @v @b
    <+ okProd   @k @(Coprod k u v) @b
    <+ okCoprod @k @u @v
  {-# INLINE distr #-}
  {-# MINIMAL distl | distr #-}

-- instance DistribCat (->) where
--   distl (a,uv) = ((a,) +++ (a,)) uv
--   distr (uv,b) = ((,b) +++ (,b)) uv

instance DistribCat (->) where
  distl (a,Left  u) = Left  (a,u)
  distl (a,Right v) = Right (a,v)
  distr (Left  u,b) = Left  (u,b)
  distr (Right v,b) = Right (v,b)

instance DistribCat U2 where
  distl = U2
  distr = U2

instance (DistribCat k, DistribCat k') => DistribCat (k :**: k') where
  distl = distl :**: distl
  distr = distr :**: distr
  PINLINER(distl)
  PINLINER(distr)

{--------------------------------------------------------------------
    Exponentials
--------------------------------------------------------------------}

type OkExp k = OpCon (Exp k) (Ok' k)

okExp :: forall k a b. OkExp k
      => Ok' k a && Ok' k b |- Ok' k (Exp k a b)
okExp = inOp
{-# INLINE okExp #-}

-- #define ExpAsCat

#ifdef ExpAsCat
type Exp k = k
#else
type Exp k = (->)
#endif

class (OkExp k, ProductCat k) => ClosedCat k where
  -- type Exp k :: u -> u -> u
  apply   :: forall a b. Ok2 k a b => Prod k (Exp k a b) a `k` b
  apply = uncurry id
          <+ okExp @k @a @b
  {-# INLINE apply #-}
  curry   :: Ok3 k a b c => (Prod k a b `k` c) -> (a `k` Exp k b c)
  uncurry :: forall a b c. Ok3 k a b c
          => (a `k` Exp k b c)  -> (Prod k a b `k` c)
  default uncurry :: forall a b c. (MonoidalPCat k, Ok3 k a b c)
                  => (a `k` Exp k b c)  -> (Prod k a b `k` c)
  uncurry g = apply . first g
              <+ okProd @k @(Exp k b c) @b
              <+ okProd @k @a @b
              <+ okExp  @k @b @c
  {-# INLINE uncurry #-}
  {-# MINIMAL curry, (apply | uncurry) #-}

--   apply   :: (Ok2 k a b, p ~ Prod k, e ~ Exp k) => ((a `e` b) `p` a) `k` b

instance ClosedCat (->) where
  -- type Exp (->) = (->)
  apply   = P.uncurry ($)
  curry   = P.curry
  uncurry = P.uncurry

-- TODO: do we want inline for apply, curry, and uncurry?

applyK   ::            Kleisli m (Kleisli m a b :* a) b
curryK   :: Monad m => Kleisli m (a :* b) c -> Kleisli m a (Kleisli m b c)
uncurryK :: Monad m => Kleisli m a (Kleisli m b c) -> Kleisli m (a :* b) c

applyK   = pack (apply . first unpack)
curryK   = inNew $ \ h -> return . pack . curry h
uncurryK = inNew $ \ f -> \ (a,b) -> f a >>= ($ b) . unpack

#if 0
instance Monad m => ClosedCat (Kleisli m) where
  -- type Exp (Kleisli m) = Kleisli m
  apply   = applyK
  curry   = curryK
  uncurry = uncurryK
#endif

instance ClosedCat U2 where
  apply = U2
  curry U2 = U2
  uncurry U2 = U2

#ifdef ExpAsCat
instance (ClosedCat k, ClosedCat k') => ClosedCat (k :**: k') where
  apply = (apply . first exl) :**: undefined
  -- apply = (apply . first exl) :**: (apply . first exr)

  -- apply = (apply . exl) :**: (apply . exr)
  -- apply :: forall a b. (Ok2 k a b, Ok2 k' a b)
  --       => (k :**: k') ((k :**: k') a b :* a) b
  -- apply = undefined -- (apply . exl) :**: _
  curry (f :**: f') = curry f :**: curry f'
  uncurry (g :**: g') = uncurry g :**: uncurry g'
  PINLINER(apply)
  PINLINER(curry)
  PINLINER(uncurry)
#else
instance (ClosedCat k, ClosedCat k') => ClosedCat (k :**: k') where
  apply = apply :**: apply
  -- apply = (apply . exl) :**: (apply . exr)
  -- apply :: forall a b. (Ok2 k a b, Ok2 k' a b)
  --       => (k :**: k') ((k :**: k') a b :* a) b
  -- apply = undefined -- (apply . exl) :**: _
  curry (f :**: f') = curry f :**: curry f'
  uncurry (g :**: g') = uncurry g :**: uncurry g'
  PINLINER(apply)
  PINLINER(curry)
  PINLINER(uncurry)
#endif

-- An alternative to ClosedCat
class OkExp k => FlipCat k where
  flipC  :: Ok3 k a b c => (a `k` (b -> c)) -> (b -> (a `k` c))
  flipC' :: Ok3 k a b c => (b -> (a `k` c)) -> (a `k` (b -> c))

instance FlipCat (->) where
  flipC  = flip
  flipC' = flip

-- TODO: inline?

instance FlipCat U2 where
  flipC  U2 = const U2
  flipC' _ = U2

instance (FlipCat k, FlipCat k') => FlipCat (k :**: k') where
  flipC (f :**: f') b = flipC f b :**: flipC f' b
  flipC' h = flipC' (exl2 . h) :**: flipC' (exr2 . h)

-- Hm. The use of exl2 and exr2 here suggest replication of effort

--                h  :: b -> (k :**: k') a c
--         exl2 . h  :: b -> a `k` c
-- flipC' (exl2 . h) :: b -> a `k` c

type Unit k = ()

type OkUnit k = Ok k (Unit k)

class OkUnit k => TerminalCat k where
  -- type Unit k :: u
  it :: Ok k a => a `k` Unit k
  default it :: (ConstCat k (Unit k), Ok k a) => a `k` Unit k
  it = const ()
  {-# INLINE it #-}

-- TODO: add default it = const () when ConstCat k, and then remove instances
-- that were using this definition explicitly.

instance TerminalCat (->) where
  -- type Unit (->) = ()
  it = const ()

instance Monad m => TerminalCat (Kleisli m) where
  -- type Unit (Kleisli m) = ()
  it = arr it

instance TerminalCat U2 where
  it = U2

instance (TerminalCat k, TerminalCat k') => TerminalCat (k :**: k') where
  it = it :**: it
  PINLINER(it)

class OkUnit k => UnitCat k where
  lunit :: Ok k a => a `k` Prod k (Unit k) a
  default lunit :: (MProductCat k, TerminalCat k, Ok k a) => a `k` Prod k (Unit k) a
  lunit = it &&& id
  lcounit :: Ok k a => Prod k (Unit k) a `k` a
  default lcounit :: (ProductCat k, Ok k a) => Prod k (Unit k) a `k` a
  lcounit = exr
  runit :: Ok k a => a `k` Prod k a (Unit k)
  default runit :: (MProductCat k, TerminalCat k, Ok k a) => a `k` Prod k a (Unit k)
  runit = id &&& it
  rcounit :: Ok k a => Prod k a (Unit k) `k` a
  default rcounit :: (ProductCat k, TerminalCat k, Ok k a) => Prod k a (Unit k) `k` a
  rcounit = exl
  PINLINER(lunit)
  PINLINER(runit)
  PINLINER(lcounit)
  PINLINER(rcounit)

instance UnitCat (->)
instance Monad m => UnitCat (Kleisli m)
instance UnitCat U2

instance (UnitCat k, UnitCat k') => UnitCat (k :**: k') where
  lunit   = lunit   :**: lunit
  runit   = runit   :**: runit
  lcounit = lcounit :**: lcounit
  rcounit = rcounit :**: rcounit
  PINLINER(lunit)
  PINLINER(runit)
  PINLINER(lcounit)
  PINLINER(rcounit)

-- lunit :: (ProductCat k, TerminalCat k, Ok k a) => a `k` Prod k (Unit k) a
-- lunit = it &&& id

-- runit :: (ProductCat k, TerminalCat k, Ok k a) => a `k` Prod k a (Unit k)
-- runit = id &&& it

type Counit k = ()  -- for now

class Ok k (Counit k) => CoterminalCat k where
  ti :: Ok k a => Counit k `k` a

instance CoterminalCat U2 where
  ti = U2

instance (CoterminalCat k, CoterminalCat k') => CoterminalCat (k :**: k') where
  ti = ti :**: ti
  PINLINER(ti)

#if 0

class Category k => UnsafeArr k where
  unsafeArr :: Ok2 k a b => (a -> b) -> a `k` b

instance UnsafeArr (->) where
  unsafeArr = A.arr

instance Monad m => UnsafeArr (Kleisli m) where
  unsafeArr = A.arr

#endif

constFun :: forall k p a b. (ClosedCat k, Ok3 k p a b)
         => (a `k` b) -> (p `k` Exp k a b)
constFun f = curry (f . exr) <+ okProd @k @p @a
{-# INLINE constFun #-}

--        f        :: a `k` b
--        f . exl  :: Prod k p a `k` b
-- curry (f . exl) :: p `k` (Exp k a b)

-- Combine with currying:

constFun2 :: forall k p a b c. (ClosedCat k, Oks k [p,a,b,c])
          => (Prod k a b `k` c) -> (p `k` (Exp k a (Exp k b c)))
constFun2 = constFun . curry
            <+ okExp @k @b @c

unitFun :: forall k a b. (ClosedCat k, TerminalCat k, Ok2 k a b)
        => (a `k` b) -> (Unit k `k` (Exp k a b))
unitFun = constFun

unUnitFun :: forall k p a. (ClosedCat k, MonoidalPCat k, TerminalCat k, Oks k [p,a]) =>
             (Unit k `k` Exp k p a) -> (p `k` a)
unUnitFun g = uncurry g . (it &&& id)
              <+ okProd @k @(Unit k) @p

{--------------------------------------------------------------------
    Constant arrows
--------------------------------------------------------------------}

-- Drop ConstObj for now

type ConstObj k b = b

#if 0

class (TerminalCat k, Ok k (ConstObj k b)) => ConstCat k b where
--   type ConstObj k b
--   type ConstObj k b = b
  unitArrow  :: b -> (Unit k `k` ConstObj k b)
  const :: Ok k a => b -> (a `k` ConstObj k b)
  const b = unitArrow b . it
  unitArrow = const
  {-# MINIMAL unitArrow | const #-}

#else

-- TODO: If I keep this version, remove TerminalCat parent
class (Category k, Ok k (ConstObj k b)) => ConstCat k b where
  -- type ConstObj k b
  -- type ConstObj k b = b
  const :: Ok k a => b -> (a `k` ConstObj k b)
  -- default const :: (HasRep (ConstObj k b), ConstCat k (Rep b), RepCat k, Ok k a)
  --               => b -> (a `k` ConstObj k b)
  -- const = repConst
  unitArrow :: OkUnit k => b -> (Unit k `k` ConstObj k b)
  unitArrow = const
  -- default const :: (TerminalCat k, OkUnit k)
  --               => b -> (Unit k `k` ConstObj k b)
  default const :: (TerminalCat k, Ok k a)
                => b -> (a `k` ConstObj k b)
  const b = unitArrow b . it

#endif

#if 0

instance (ProductCat k, ConstCat k b, ConstCat k c, Ok k a)
      => ConstCat k (b :* c) where
  const = pairConst

instance {-# OVERLAPPABLE #-}
  ( Category k, ConstCat k (R.Rep b), RepCat k, HasRep (ConstObj k b)
  , Ok k (ConstObj k b) ) => ConstCat k b where
  const = repConst

#endif

repConst :: (HasRep b, r ~ R.Rep b, RepCat k b (ConstObj k r), ConstCat k r, Ok k a, Ok k (ConstObj k b))
         => b -> (a `k` ConstObj k b)
repConst b = abstC . const (repr b)

--                      b  :: b
--                reprC b  :: r
--         const (reprC b) :: a `k` ConstObj k r
-- abstC . const (reprC b) :: a `k` ConstObj k r

pairConst :: (MProductCat k, ConstCat k b, ConstCat k c, Ok k a)
          => b :* c -> (a `k` (b :* c))
pairConst (b,c) = const b &&& const c

-- | Inject a constant on the left
lconst :: forall k a b. (MProductCat k, ConstCat k a, Ok2 k a b)
       => a -> (b `k` (a :* b))
lconst a = first  (const a) . dup
           <+ okProd @k @b @b
           <+ okProd @k @(ConstObj k a) @b

-- | Inject a constant on the right
rconst :: forall k a b. (MProductCat k, ConstCat k b, Ok2 k a b)
       => b -> (a `k` (a :* b))
rconst b = second (const b) . dup
           <+ okProd @k @a @a
           <+ okProd @k @a @(ConstObj k b)

#if 1
instance ConstCat (->) b where const = P.const
#else

-- Temp cheat. No longer needed, since I fix transCatOp in Plugin to fail
-- gracefully when the target category doesn't inhabit the needed class.

#define LitConst(ty) \
instance ConstCat (->) (ty) where { const = P.const ; {-# INLINE const #-} }

LitConst(())
LitConst(Bool)
LitConst(Int)
LitConst(Float)
LitConst(Double)

#endif

-- instance Monad m => ConstCat (Kleisli m) b where const b = arr (const b)

instance (Monad m, ConstCat (->) b) => ConstCat (Kleisli m) b where const b = arr (const b)

-- For prims, use constFun instead.

instance ConstCat U2 a where
  const _ = U2
  -- unitArrow b = unitArrow b :**: unitArrow b

instance (ConstCat k a, ConstCat k' a) => ConstCat (k :**: k') a where
  const b = const b :**: const b
  -- unitArrow b = unitArrow b :**: unitArrow b
  PINLINER(const)
  -- PINLINER(unitArrow)

-- Note that `ConstCat` is *not* poly-kinded. Since the codomain `b` is an
-- argument to `unitArrow` and `const`, `k :: * -> * -> *`. I'm uneasy
-- about this kind restriction, which would preclude some useful categories,
-- including linear maps and entailment. Revisit this issue later.

class DelayCat k where
  delay :: Ok k a => a -> (a `k` a)

instance DelayCat (->) where
  delay = error "delay: not really defined for functions"
  -- Will I need to use oops instead?

class ProductCat k => LoopCat k where
  loop :: Ok3 k s a b => ((a :* s) `k` (b :* s)) -> (a `k` b)

instance LoopCat (->) where
  loop = error "loop: not really defined for functions"
  -- Will I need to use oops instead?

{--------------------------------------------------------------------
    Traced monoidal categories
--------------------------------------------------------------------}

class ProductCat k => TracedCat k where
  trace :: Ok3 k a b c => ((a :* c) `k` (b :* c)) -> (a `k` b)

instance TracedCat (->) where
  trace h a = b where (b,c) = h (a,c)

instance TracedCat U2 where trace U2 = U2

instance (TracedCat k, TracedCat k') => TracedCat (k :**: k') where
  trace (f :**: g) = trace f :**: trace g
  PINLINER(trace)

instance MonadFix m => TracedCat (Kleisli m) where
  trace (Kleisli h) = Kleisli (\ a -> do rec (b,c) <- h (a,c)
                                         return b)
  PINLINER(trace)

{--------------------------------------------------------------------
    Class aggregates
--------------------------------------------------------------------}

-- | Bi-cartesion (cartesian & co-cartesian) closed categories. Also lumps in
-- terminal and distributive, though should probably be moved out.
type BiCCC k = (ClosedCat k, CoproductCat k, TerminalCat k, DistribCat k)

-- -- | 'BiCCC' with constant arrows.
-- type BiCCCC k p = (BiCCC k, ConstCat k p {-, RepCat k, LoopCat k, DelayCat k-})


{--------------------------------------------------------------------
    Add constraints to a category
--------------------------------------------------------------------}

-- infixr 3 &+&
-- class    (con a, con' a) => (con &+& con') a
-- instance (con a, con' a) => (con &+& con') a

-- instance (HasCon (f a), HasCon (g a)) => HasCon ((f &+& g) a) where
--   type Con ((f &+& g) a) = (Con (f a),Con (g a))
--   toDict (And1 (toDict -> Dict) (toDict -> Dict)) = Dict
--   unDict = And1 unDict unDict

data Constrained (con :: Type -> Constraint) k a b = Constrained (a `k` b)

instance (OpSat op con, OpSat op con') => OpCon op (Sat (con &+& con')) where
  inOp :: forall a b. Sat (con &+& con') a && Sat (con &+& con') b |- Sat (con &+& con') (a `op` b)
  inOp = Entail (Sub $ Dict <+ inSat @op @con @a @b <+ inSat @op @con' @a @b)

-- TODO: define inSat, combining inOp and Sat

instance Category k => Category (Constrained con k) where
  type Ok (Constrained con k) = Ok k &+& con
  id = Constrained id
  Constrained g . Constrained f = Constrained (g . f)

instance (AssociativePCat k, OpSat (Prod k) con)
      => AssociativePCat (Constrained con k) where
  lassocP = Constrained lassocP
  rassocP = Constrained rassocP

instance (MonoidalPCat k, OpSat (Prod k) con)
      => MonoidalPCat (Constrained con k) where
  Constrained f *** Constrained g = Constrained (f *** g)

instance (BraidedPCat k, OpSat (Prod k) con) => BraidedPCat (Constrained con k) where
  swapP = Constrained swapP

instance (ProductCat k, OpSat (Prod k) con) => ProductCat (Constrained con k) where
  -- type Prod (Constrained con k) = Prod k
  exl = Constrained exl
  exr = Constrained exr
  dup = Constrained dup
  -- Constrained f &&& Constrained g = Constrained (f &&& g)

instance (AssociativeSCat k, OpSat (Coprod k) con)
      => AssociativeSCat (Constrained con k) where
  lassocS = Constrained lassocS
  rassocS = Constrained rassocS

instance (BraidedSCat k, OpSat (Coprod k) con)
      => BraidedSCat (Constrained con k) where
  swapS = Constrained swapS

instance (MonoidalSCat k, OpSat (Coprod k) con)
      => MonoidalSCat (Constrained con k) where
  Constrained f +++ Constrained g = Constrained (f +++ g)

instance (CoproductCat k, OpSat (Coprod k) con)
      => CoproductCat (Constrained con k) where
  -- type Coprod (Constrained con k) = Coprod k
  inl = Constrained inl
  inr = Constrained inr
  jam = Constrained jam
  -- Constrained a ||| Constrained b = Constrained (a ||| b)

instance (ClosedCat k, OpSat (Prod k) con, OpSat (Exp k) con) => ClosedCat (Constrained con k) where
  -- type Exp (Constrained con k) = Exp k
  apply = Constrained apply
  curry   (Constrained f) = Constrained (curry f)
  uncurry (Constrained g) = Constrained (uncurry g)

instance (BoolCat k, con Bool, OpCon (Prod k) (Sat con))
      => BoolCat (Constrained con k) where
  notC = Constrained notC
  andC = Constrained andC
  orC = Constrained orC
  xorC = Constrained xorC

instance (EqCat k a, con a, con Bool, OpSat (Prod k) con) => EqCat (Constrained con k) a where
  equal = Constrained equal
  notEqual = Constrained notEqual

instance (OrdCat k a, con a, con Bool, OpSat (Prod k) con) => OrdCat (Constrained con k) a where
  lessThan = Constrained lessThan
  greaterThan = Constrained greaterThan
  lessThanOrEqual = Constrained lessThanOrEqual
  greaterThanOrEqual = Constrained greaterThanOrEqual

instance (CoerceCat k a b, con a, con b) => CoerceCat (Constrained con k) a b where
  coerceC = Constrained coerceC

instance (ConstCat k b, con b) => ConstCat (Constrained con k) b where
  const = Constrained . const

instance (TracedCat k, OpSat (Prod k) con) => TracedCat (Constrained con k) where
  trace (Constrained fn) = Constrained $ trace fn

instance OkFunctor (Constrained con k) f where
  okFunctor = okFunctor @(Constrained con k)

instance FunctorCat k f => FunctorCat (Constrained con k) f where
  fmapC (Constrained fn) = Constrained $ fmapC fn
  unzipC = Constrained unzipC

instance (Applicative m, con a) => PointedCat (Constrained con (->)) m a where
  pointC = Constrained pure

instance (NumCat k a, con a) => NumCat (Constrained con k) a where
  negateC = Constrained negateC
  addC = Constrained addC
  subC = Constrained subC
  mulC = Constrained mulC
  powIC = Constrained powIC

instance (IntegralCat k a, con a) => IntegralCat (Constrained con k) a where
  divC = Constrained divC
  modC = Constrained modC

instance (FractionalCat k a, con a) => FractionalCat (Constrained con k) a where
  recipC  = Constrained recipC
  divideC = Constrained divideC

instance (FloatingCat k a, con a) => FloatingCat (Constrained con k) a where
  expC = Constrained expC
  logC = Constrained logC
  cosC = Constrained cosC
  sinC = Constrained sinC
  sqrtC = Constrained sqrtC
  tanhC = Constrained tanhC

instance (RealFracCat k a b, con a, con b) => RealFracCat (Constrained con k) a b where
  floorC = Constrained floorC
  ceilingC = Constrained ceilingC
  truncateC = Constrained truncateC

instance (FromIntegralCat k a b, con a, con b)
      => FromIntegralCat (Constrained con k) a b where
  fromIntegralC = Constrained fromIntegralC

instance (BottomCat k a b, con a, con b) => BottomCat (Constrained con k) a b where
  bottomC = Constrained bottomC

instance (IfCat k a, OpCon (Prod k) (Sat con), con Bool, con a)
      => IfCat (Constrained con k) a where
  ifC = Constrained ifC

instance (RepCat k a r, con a, con r) => RepCat (Constrained con k) a r where
  abstC = Constrained abstC
  reprC = Constrained reprC

instance RepresentableCat k f => RepresentableCat (Constrained con k) f where
  tabulateC = Constrained tabulateC
  indexC = Constrained indexC

{--------------------------------------------------------------------
    Other category subclasses, perhaps to move elsewhere
--------------------------------------------------------------------}

-- I don't think I want the general Kleisli instances for the rest.
-- For instance, for circuits, type BoolOf (:>) = Source Bool.

#define KleisliInstances

-- Adapted from Circat.Classes

type BoolOf k = Bool

class (ProductCat k, Ok k (BoolOf k)) => BoolCat k where
  -- type BoolOf k
  notC :: BoolOf k `k` BoolOf k
  andC, orC, xorC :: Prod k (BoolOf k) (BoolOf k) `k` BoolOf k

--     • Potential superclass cycle for ‘BoolCat’
--         one of whose superclass constraints is headed by a type family:
--           ‘Ok k bool’
--       Use UndecidableSuperClasses to accept this
--     • In the class declaration for ‘BoolCat’

instance BoolCat (->) where
  -- type BoolOf (->) = Bool
  notC = not
  andC = P.uncurry (&&)
  orC  = P.uncurry (||)
  xorC = P.uncurry (/=)

-- No inline, since not, (&&), (||) are not class-ops, and (/=) is
-- specialized to Bool here (and hence appears as $fEqBool_$c/=)

#ifdef KleisliInstances
instance Monad m => BoolCat (Kleisli m) where
  -- type BoolOf (Kleisli m) = Bool
  notC = arr notC
  andC = arr andC
  orC  = arr orC
  xorC = arr xorC
#endif

instance BoolCat U2 where
  notC = U2
  andC = U2
  orC  = U2
  xorC = U2

instance (BoolCat k, BoolCat k') => BoolCat (k :**: k') where
  notC = notC :**: notC
  andC = andC :**: andC
  orC  = orC  :**: orC
  xorC = xorC :**: xorC
  PINLINER(notC)
  PINLINER(andC)
  PINLINER(orC)
  PINLINER(xorC)

okTT :: forall k a. OkProd k => Ok' k a |- Ok' k (Prod k a a)
okTT = okProd @k @a @a . dup

class (BoolCat k, Ok k a) => EqCat k a where
  equal, notEqual :: Prod k a a `k` BoolOf k
  notEqual = notC . equal    <+ okTT @k @a
  equal    = notC . notEqual <+ okTT @k @a
  {-# MINIMAL equal | notEqual #-}

instance Eq a => EqCat (->) a where
  equal    = uncurry (IC.inline (==))
  notEqual = uncurry (IC.inline (/=))
  {-# OPINLINE equal #-}
  {-# OPINLINE notEqual #-}

#ifdef KleisliInstances
instance (Monad m, Eq a) => EqCat (Kleisli m) a where
  equal    = arr equal
  notEqual = arr notEqual
#endif

instance EqCat U2 a where
  equal = U2
  notEqual = U2

instance (EqCat k a, EqCat k' a) => EqCat (k :**: k') a where
  equal = equal :**: equal
  notEqual = notEqual :**: notEqual
  PINLINER(equal)
  PINLINER(notEqual)

class (EqCat k a, Ord a) => OrdCat k a where
  lessThan, greaterThan, lessThanOrEqual, greaterThanOrEqual :: Prod k a a `k` BoolOf k
  default lessThan    :: BraidedPCat k => Prod k a a `k` BoolOf k
  default greaterThan :: BraidedPCat k => Prod k a a `k` BoolOf k
  greaterThan        = lessThan . swapP    <+ okTT @k @a
  lessThan           = greaterThan . swapP <+ okTT @k @a
  lessThanOrEqual    = notC . greaterThan  <+ okTT @k @a
  greaterThanOrEqual = notC . lessThan     <+ okTT @k @a
  {-# MINIMAL lessThan | greaterThan #-}

class Ok k a => MinMaxCat k a where
  minC, maxC :: Prod k a a `k` a
#if 0
  default minC :: (OrdCat k a, IfCat k a, Ok k a) => Prod k a a `k` a
  default maxC :: (OrdCat k a, IfCat k a, Ok k a) => Prod k a a `k` a
  minC = ifC . (lessThanOrEqual &&& id)
           <+ okProd @k @Bool @(a :* a)
           <+ okProd @k @a @a
  maxC = ifC . (greaterThan     &&& id)
           <+ okProd @k @Bool @(a :* a)
           <+ okProd @k @a @a
#endif

-- TODO: maybe replace minC and maxC with sortP :: (a :* b) `k` (a :* b). Or add
-- a sortP method and defaults for all three. Would be groovy for parallel
-- sorting.

instance Ord a => MinMaxCat (->) a where
  minC = uncurry (IC.inline min)
  maxC = uncurry (IC.inline max)
  {-# OPINLINE minC #-}
  {-# OPINLINE maxC #-}

instance Ord a => OrdCat (->) a where
  lessThan           = uncurry (IC.inline (<))
  greaterThan        = uncurry (IC.inline (>))
  lessThanOrEqual    = uncurry (IC.inline (<=))
  greaterThanOrEqual = uncurry (IC.inline (>=))
  {-# OPINLINE lessThan #-}
  {-# OPINLINE greaterThan #-}
  {-# OPINLINE lessThanOrEqual #-}
  {-# OPINLINE greaterThanOrEqual #-}

#ifdef KleisliInstances
instance (Monad m, Ord a) => OrdCat (Kleisli m) a where
  lessThan           = arr lessThan
  greaterThan        = arr greaterThan
  lessThanOrEqual    = arr lessThanOrEqual
  greaterThanOrEqual = arr greaterThanOrEqual
#endif

instance Ord a => OrdCat U2 a where
  lessThan           = U2
  greaterThan        = U2
  lessThanOrEqual    = U2
  greaterThanOrEqual = U2

instance MinMaxCat U2 a where
  minC = U2
  maxC = U2

instance (OrdCat k a, OrdCat k' a) => OrdCat (k :**: k') a where
  lessThan = lessThan :**: lessThan
  greaterThan = greaterThan :**: greaterThan
  lessThanOrEqual = lessThanOrEqual :**: lessThanOrEqual
  greaterThanOrEqual = greaterThanOrEqual :**: greaterThanOrEqual
  PINLINER(lessThan)
  PINLINER(greaterThan)
  PINLINER(lessThanOrEqual)
  PINLINER(greaterThanOrEqual)

instance (MinMaxCat k a, MinMaxCat k' a) => MinMaxCat (k :**: k') a where
  minC = minC :**: minC
  maxC = maxC :**: maxC
  PINLINER(minC)
  PINLINER(maxC)

class (Category k, Ok k a) => EnumCat k a where
  succC, predC :: a `k` a
  default succC :: (MProductCat k, NumCat k a, ConstCat k a, Num a) => a `k` a
  default predC :: (MProductCat k, NumCat k a, ConstCat k a, Num a) => a `k` a
  succC = addC . rconst 1 <+ okProd @k @a @a
  predC = subC . rconst 1 <+ okProd @k @a @a

instance Enum a => EnumCat (->) a where
  succC = IC.inline succ
  predC = IC.inline pred
  {-# OPINLINE succC #-}
  {-# OPINLINE predC #-}

instance EnumCat U2 a where
  succC = U2
  predC = U2

instance (EnumCat k a, EnumCat k' a) => EnumCat (k :**: k') a where
  succC = succC :**: succC
  predC = predC :**: predC
  PINLINER(succC)
  PINLINER(predC)

class Ok k a => NumCat k a where
  negateC :: a `k` a
  addC, subC, mulC :: Prod k a a `k` a
  powIC :: Ok k Int => Prod k a Int `k` a
  default subC :: MProductCat k => Prod k a a `k` a
  subC = addC . second negateC <+ okProd @k @a @a
  {-# INLINE subC #-}

instance Num a => NumCat (->) a where
  negateC = IC.inline negate
  -- mysterious bug workaround, but leads to different error. see 2017-12-27 notes.
  -- addC (x,y) = IC.inline (+) x y
  addC    = uncurry (IC.inline (+))
  subC    = uncurry (IC.inline (-))
  mulC    = uncurry (IC.inline (*))
  powIC   = uncurry (^) -- (^) is not a class-op
  {-# OPINLINE negateC #-}
  {-# OPINLINE addC #-}
  {-# OPINLINE subC #-}
  {-# OPINLINE mulC #-}
  {-# OPINLINE powIC #-}

#ifdef KleisliInstances
instance (Monad m, Num a) => NumCat (Kleisli m) a where
  negateC = arr negateC
  addC    = arr addC
  subC    = arr subC
  mulC    = arr mulC
  powIC   = arr powIC
#endif

instance NumCat U2 a where
  negateC = U2
  addC    = U2
  subC    = U2
  mulC    = U2
  powIC   = U2

instance (NumCat k a, NumCat k' a) => NumCat (k :**: k') a where
  negateC = negateC :**: negateC
  addC    = addC    :**: addC
  subC    = subC    :**: subC
  mulC    = mulC    :**: mulC
  powIC   = powIC   :**: powIC
  PINLINER(negateC)
  PINLINER(addC)
  PINLINER(subC)
  PINLINER(mulC)
  PINLINER(powIC)

class Ok k a => IntegralCat k a where
  -- For now
  divC :: Prod k a a `k` a
  modC :: Prod k a a `k` a

divModC :: forall k a. (MProductCat k, IntegralCat k a, Ok k a)
        => Prod k a a `k` Prod k a a
divModC = divC &&& modC  <+ okProd @k @a @a

instance Integral a => IntegralCat (->) a where
  divC = uncurry (IC.inline div)
  modC = uncurry (IC.inline mod)
  {-# OPINLINE divC #-}
  {-# OPINLINE modC #-}

#ifdef KleisliInstances
instance (Monad m, Integral a) => IntegralCat (Kleisli m) a where
  divC = arr divC
  modC = arr modC
#endif

instance IntegralCat U2 a where
  divC = U2
  modC = U2

instance (IntegralCat k a, IntegralCat k' a) => IntegralCat (k :**: k') a where
  divC = divC :**: divC
  modC = modC :**: modC
  PINLINER(divC)
  PINLINER(modC)

class Ok k a => FractionalCat k a where
  recipC :: a `k` a
  divideC :: Prod k a a `k` a
  default recipC :: (MProductCat k, ConstCat k a, Num a) => a `k` a
  recipC = divideC . lconst 1 <+ okProd @k @a @a
  {-# INLINE recipC #-}
  default divideC :: (MProductCat k, NumCat k a) => Prod k a a `k` a
  divideC = mulC . second recipC <+ okProd @k @a @a
  {-# INLINE divideC #-}
  {-# MINIMAL recipC | divideC #-}

instance Fractional a => FractionalCat (->) a where
  recipC  = IC.inline recip
  divideC = uncurry (IC.inline (/))
  {-# OPINLINE recipC #-}
  {-# OPINLINE divideC #-}

#ifdef KleisliInstances
instance (Monad m, Fractional a) => FractionalCat (Kleisli m) a where
  recipC  = arr recipC
  divideC = arr divideC
#endif

instance FractionalCat U2 a where
  recipC  = U2
  divideC = U2

instance (FractionalCat k a, FractionalCat k' a) => FractionalCat (k :**: k') a where
  recipC  = recipC  :**: recipC
  divideC = divideC :**: divideC
  PINLINER(recipC)
  PINLINER(divideC)

class Ok k a => FloatingCat k a where
  expC, logC, cosC, sinC, sqrtC, tanhC :: a `k` a
  -- powC :: (a :* a) `k` a

-- ln :: Floating a => a -> a
-- ln = logBase (exp 1)

instance Floating a => FloatingCat (->) a where
  expC = IC.inline exp
  logC = IC.inline log
  cosC = IC.inline cos
  sinC = IC.inline sin
  sqrtC = IC.inline sqrt
  tanhC = IC.inline tanh
  -- powC = IC.inline (**)
  {-# OPINLINE expC #-}
  {-# OPINLINE logC #-}
  {-# OPINLINE cosC #-}
  {-# OPINLINE sinC #-}
  {-# OPINLINE sqrtC #-}
  {-# OPINLINE tanhC #-}

#ifdef KleisliInstances
instance (Monad m, Floating a) => FloatingCat (Kleisli m) a where
  expC = arr expC
  logC = arr logC
  cosC = arr cosC
  sinC = arr sinC
  sqrtC = arr sqrtC
  tanhC = arr tanh
  -- powC = arr powC
#endif

instance FloatingCat U2 a where
  expC = U2
  logC = U2
  cosC = U2
  sinC = U2
  sqrtC = U2
  tanhC = U2
  -- powC = U2

instance (FloatingCat k a, FloatingCat k' a) => FloatingCat (k :**: k') a where
  expC = expC :**: expC
  logC = logC :**: logC
  cosC = cosC :**: cosC
  sinC = sinC :**: sinC
  sqrtC = sqrtC :**: sqrtC
  tanhC = tanhC :**: tanhC
  PINLINER(expC)
  PINLINER(logC)
  PINLINER(cosC)
  PINLINER(sinC)
  PINLINER(sqrtC)
  PINLINER(tanhC)
  -- powC = powC :**: powC
  -- PINLINER(powC)

class Ok k a => RealFracCat k a b where
  floorC, ceilingC :: a `k` b
  truncateC :: a `k` b

instance (RealFrac a, Integral b) => RealFracCat (->) a b where
  floorC    = IC.inline floor
  ceilingC  = IC.inline ceiling
  truncateC = IC.inline truncate
  {-# OPINLINE floorC #-}
  {-# OPINLINE ceilingC #-}
  {-# OPINLINE truncateC #-}

#ifdef KleisliInstances
instance (Monad m, RealFrac a, Integral b) => RealFracCat (Kleisli m) a b where
  floorC    = arr floorC
  ceilingC  = arr ceilingC
  truncateC = arr truncateC
#endif

instance Integral b => RealFracCat U2 a b where
  floorC    = U2
  ceilingC  = U2
  truncateC = U2

instance (RealFracCat k a b, RealFracCat k' a b) => RealFracCat (k :**: k') a b where
  floorC    = floorC    :**: floorC
  ceilingC  = ceilingC  :**: ceilingC
  truncateC = truncateC :**: truncateC
  PINLINER(floorC)
  PINLINER(ceilingC)
  PINLINER(truncateC)

-- Stand-in for fromIntegral, avoiding the intermediate Integer in the Prelude
-- definition.
class FromIntegralCat k a b where
  fromIntegralC :: a `k` b
  foo_FromIntegralCat :: ()  -- experiment
  foo_FromIntegralCat = ()

instance (Integral a, Num b) => FromIntegralCat (->) a b where
  fromIntegralC = X.inline fromIntegral -- non-class-op
  {-# OPINLINE fromIntegralC #-}

#ifdef KleisliInstances
instance (Monad m, Integral a, Num b) => FromIntegralCat (Kleisli m) a b where
  fromIntegralC = arr fromIntegral
#endif

instance FromIntegralCat U2 a b where
  fromIntegralC = U2

instance (FromIntegralCat k a b, FromIntegralCat k' a b) => FromIntegralCat (k :**: k') a b where
  fromIntegralC = fromIntegralC :**: fromIntegralC
  PINLINER(fromIntegralC)

#if 1

-- Revisit later. I used BottomCat for an encoding of sums via products.

class BottomCat k a b where
  bottomC :: a `k` b

-- instance (BottomCat k a b, BottomCat k a c, ProductCat k, Ok3 k a b c) => BottomCat k a (b :* c) where
--   bottomC = bottomC &&& bottomC

instance (BottomCat k a b, ClosedCat k, Ok4 k z b a (z -> b)) => BottomCat k a (z -> b) where
  bottomC = curry (bottomC . exl) <+ okProd @k @a @z

instance BottomCat (->) a b where bottomC = error "bottomC for (->) evaluated"

instance BottomCat U2 a b where
  bottomC = U2

instance (BottomCat k a b, BottomCat k' a b) => BottomCat (k :**: k') a b where
  bottomC = bottomC :**: bottomC
  PINLINER(bottomC)

#endif

type IfT k a = Prod k (BoolOf k) (Prod k a a) `k` a

class (BoolCat k, Ok k a) => IfCat k a where
  ifC :: IfT k a

instance IfCat (->) a where
  ifC (i,(t,e)) = if i then t else e

#ifdef KleisliInstances
instance Monad m => IfCat (Kleisli m) a where
  ifC = arr ifC
#endif

instance IfCat U2 a where
  ifC = U2

instance (IfCat k a, IfCat k' a) => IfCat (k :**: k') a where
  ifC = ifC :**: ifC
  PINLINER(ifC)

class UnknownCat k a b where
  unknownC :: a `k` b

instance UnknownCat (->) a b where
  unknownC = error "unknown"

instance UnknownCat U2 a b where
  unknownC = U2

instance (UnknownCat k a b, UnknownCat k' a b) => UnknownCat (k :**: k') a b where
  unknownC = unknownC :**: unknownC
  PINLINER(unknownC)

class RepCat k a r where
  reprC :: a `k` r
  abstC :: r `k` a

-- 2018-02-08 (notes): I removed the "| a -> r" functional dependency.

instance (HasRep a, r ~ R.Rep a) => RepCat (->) a r where
  reprC = repr
  abstC = abst

instance (r ~ R.Rep a) => RepCat U2 a r where
  reprC = U2
  abstC = U2

instance (RepCat k a b, RepCat k' a b) => RepCat (k :**: k') a b where
  reprC = reprC :**: reprC
  abstC = abstC :**: abstC
  PINLINER(reprC)
  PINLINER(abstC)

class TransitiveCon con where
  trans :: (con a b, con b c) :- con a c

instance TransitiveCon Coercible where
  trans = Sub Dict

-- instance TransitiveCon (CoerceCat (->)) where
--   trans = Sub Dict

class (
      -- TransitiveCon (CoerceCat k)
      ) => CoerceCat k a b where
  coerceC :: a `k` b

instance Coercible a b => CoerceCat (->) a b where
  coerceC = coerce

instance CoerceCat U2 a b where
  coerceC = U2

instance (CoerceCat k a b, CoerceCat k' a b) => CoerceCat (k :**: k') a b where
  coerceC = coerceC :**: coerceC
  PINLINER(coerceC)

#if 0

#ifdef VectorSized
-- TODO: drop "Arr" alias if these definitions work out
type Arr = Vector

class (ClosedCat k, {-KnownNat n, -}Ok3 k b (Finite n) (Arr n b))
   => ArrayCat k n b where
  array :: Exp k (Finite n) b `k` Arr n b
  arrAt :: Prod k (Arr n b) (Finite n) `k` b

instance KnownNat n => ArrayCat (->) n b where
  array = arrayFun
  arrAt = arrAtFun
  PINLINER(array)
  PINLINER(arrAt)

arrayFun :: KnownNat n => (Finite n -> b) -> Arr n b
arrayFun = VS.generate_
{-# NOINLINE arrayFun #-}

arrAtFun :: KnownNat n => Arr n b :* Finite n -> b
arrAtFun = uncurry VS.index
{-# NOINLINE arrAtFun #-}

-- TODO: working definitions for arrayFun and arrAtFun

instance {- KnownNat n => -} ArrayCat U2 n b where
  array = U2
  arrAt = U2

instance (ArrayCat k n b, ArrayCat k' n b) => ArrayCat (k :**: k') n b where
  array = array :**: array
  arrAt = arrAt :**: arrAt
  PINLINER(array)
  PINLINER(arrAt)

-- #ifdef KleisliInstances
-- instance (Monad m, Enum n) => ArrayCat (Kleisli m) n b where
--   array = arr array
--   arrAt = arr arrAt
-- #endif

#else
-- Arrays
data Arr i a = MkArr (Array i a) deriving Show

-- I'm using "data" instead of "newtype" here to avoid the coercion.

class (ClosedCat k, Ok3 k a b (Arr a b)) => ArrayCat k a b where
  array :: Exp k a b `k` Arr a b
  arrAt :: Prod k (Arr a b) a `k` b
  -- at    :: Arr a b `k` Exp k a b
  -- {-# MINIMAL array, (arrAt | at) #-}
  -- arrAt = uncurry at
  -- at = curry arrAt

instance {- Enum a => -} ArrayCat (->) a b where
  array = arrayFun
  arrAt = arrAtFun
  PINLINER(array)
  PINLINER(arrAt)

arrayFun :: {- Enum a => -} (a -> b) -> Arr a b
arrayFun = oops "arrayFun not yet defined"
{-# NOINLINE arrayFun #-}

arrAtFun :: {- Enum a => -} Arr a b :* a -> b
arrAtFun = oops "arrAtFun not yet defined"
{-# NOINLINE arrAtFun #-}

-- TODO: working definitions for arrayFun and arrAtFun

instance ArrayCat U2 a b where
  array = U2
  -- array _ = U2
  arrAt = U2

instance (ArrayCat k a b, ArrayCat k' a b) => ArrayCat (k :**: k') a b where
  array = array :**: array
  arrAt = arrAt :**: arrAt
  PINLINER(array)
  PINLINER(arrAt)
  -- at = at :**: at
  -- PINLINER(at)

-- #ifdef KleisliInstances
-- instance (Monad m, Enum a) => ArrayCat (Kleisli m) a b where
--   array = arr array
--   arrAt = arr arrAt
-- #endif

#endif

#endif

{--------------------------------------------------------------------
    Functors
--------------------------------------------------------------------}

-- -- These functors change categories but not objects

-- -- | Functors map objects and arrows.
-- class (Category k, Category k'{-, OkTarget f k k'-})
--    => FunctorC f k k' {-  | f -> k k'-} where
--   -- | @fmapC@ maps arrows.
--   fmapC :: (Ok2 k a b, Oks k' [a,b]) => (a `k` b) -> (a `k'` b)
--   -- Laws:
--   -- fmapC id == id
--   -- fmapC (q . p) == fmapC q . fmapC p

{--------------------------------------------------------------------
    Functor-level operations
--------------------------------------------------------------------}

class OkFunctor k h where
  okFunctor :: Ok' k a |- Ok' k (h a)

instance OkFunctor (->) h where okFunctor = Entail (Sub Dict)

instance (OkFunctor k h, OkFunctor k' h)
      => OkFunctor (k :**: k') h where
  okFunctor = inForkCon (okFunctor @k *** okFunctor @k')

class OkFunctor k h => FunctorCat k h where
  fmapC :: Ok2 k a b => (a `k` b) -> (h a `k` h b)
  unzipC :: forall a b. Ok2 k a b => h (a :* b) `k` (h a :* h b)
#if 0
  default unzipC :: forall a b.
          (FunctorCat k h, TerminalCat k, ClosedCat k, Ok2 k a b)
       => h (a :* b) `k` (h a :* h b)
  unzipC = fmapC exl &&& fmapC exr
             <+ okFunctor @k @h @(a :* b)
             <+ okFunctor @k @h @a
             <+ okFunctor @k @h @b
             <+ okProd    @k @a @b
#endif

-- TODO: Maybe rename FunctorCat to avoid confusion.

class (Zip h, OkFunctor k h) => ZipCat k h where
  zipC :: Ok2 k a b => (h a :* h b) `k` h (a :* b)
  -- zipWithC :: Ok3 k a b c => (a :* b -> c) `k` (h a :* h b -> h c)

class OkFunctor k h => ZapCat k h where
  zapC :: Ok2 k a b => h (a `k` b) -> (h a `k` h b)

class ({- Pointed h, -} OkFunctor k h, Ok k a) => PointedCat k h a where
  pointC :: a `k` h a

-- TODO: remove superclasses like Pointed from other classes, and then review
-- instances for unnecessary parent constraints. I've removed them the
-- PointedCat instances in Syntactic and Circuit.

-- TODO: eliminate pointC in favor of using tabulate

-- TODO: Try removing Representable h and maybe OkFunctor k h from the
-- superclasses.

-- TODO: Try removing OkFunctor superclass constraint.
-- When I first triec, I ran into trouble with a rule in AltCat.

-- class DiagCat k h where
--   diagC  :: Ok k a => (a :* a) `k` h (h a)

-- TODO: do I want SumCat, AddCat, or both?

-- class (Ok k a, Num a) => SumCat k h a where
--   sumC :: h a `k` a

class Ok k a => AddCat k h a where
  sumAC :: h a `k` a

-- class IxSummable n => IxSummableCat k n where
--   ixSumC ::  (Ok k a, Additive a) => (a :^ n) `k` a

-- TODO: Keep only one of AddCat and IxSummableCat, depending on whether I go
-- with functions or functors for indexed products and coproducts.
-- Nope. Use jamPF instead of ixSumC.

instance Functor h => FunctorCat (->) h where
  fmapC  = IC.inline fmap
  unzipC = X.inline unzip
  {-# OPINLINE fmapC #-}
  {-# OPINLINE unzipC #-}

#if 0
instance (Zip h, Representable h) => ZipCat (->) h where
  zipC (as,bs) = tabulate (index as &&& index bs)
instance (Pointed h, Representable h) => PointedCat (->) h where
  pointC a = tabulate (const a)

-- Overlapping instances for ConCat.Misc.Yes1 (Rep h)
--   arising from a use of ‘&&&’
-- Matching instances:
--   instance [safe] forall k (a :: k). ConCat.Misc.Yes1 a
--     -- Defined at /Users/conal/Haskell/concat/classes/src/ConCat/Misc.hs:123:10
-- There exists a (perhaps superclass) match:
--   from the context: Representable h
--     bound by the instance declaration
--   or from: Ok2 (->) a b
--     bound by the type signature for:
--                zipC :: Ok2 (->) a b => h a :* h b -> h (a :* b)

-- TODO: inline for tabulate and index?

#else

instance Zip h => ZipCat (->) h where
  zipC = uncurry (IC.inline zip)
  -- zipWithC :: (a :* b -> c) -> (h a :* h b -> h c)
  -- zipWithC f = uncurry (inline zipWith (curry f))
  {-# OPINLINE zipC #-}

instance Zip h => ZapCat (->) h where
  -- zapC = IC.inline zap
  -- zapC = zap
  zapC = zipWith id  -- as in the default; 2017-12-27 notes
  {-# OPINLINE zapC #-}

instance Pointed h => PointedCat (->) h a where
  pointC = IC.inline point
  {-# OPINLINE pointC #-}

#endif

-- instance (Foldable h, Num a) => SumCat (->) h a where
--   sumC = IC.inline sum
--   {-# OPINLINE sumC #-}

instance (Foldable h, Additive a) => AddCat (->) h a where
  sumAC = sumA  -- not a method, so no IC.inline
  {-# OPINLINE sumAC #-}

-- instance (OkFunctor k h, OkFunctor k' h) => OkFunctor (k :**: k') h where
--   okFunctor = inForkCon (okFunctor @k *** okFunctor @k')

instance (FunctorCat k h, FunctorCat k' h) => FunctorCat (k :**: k') h where
  fmapC (f :**: g) = fmapC f :**: fmapC g
  unzipC = unzipC :**: unzipC
  {-# INLINE fmapC #-}
  {-# INLINE unzipC #-}

instance (ZipCat k h, ZipCat k' h) => ZipCat (k :**: k') h where
  zipC = zipC :**: zipC
  {-# INLINE zipC #-}
  -- zipWithC = zipWithC :**: zipWithC
  -- {-# INLINE zipWithC #-}

instance (ZapCat k h, ZapCat k' h, Functor h) => ZapCat (k :**: k') h where
  zapC = uncurry (:**:) . (zapC *** zapC) . unzip . fmap unProd
  {-# INLINE zapC #-}

--             unProd  :: (p :**: q) a b -> p a b :* q a b
--        fmap unProd  :: h ((p :**: q) a b) -> h (p a b :* q a b)
-- unzip (fmap unProd) :: h (p a b :* q a b) -> h (p a b) :* h (q a b)
-- (zapC *** zapC)     :: h (p a b) :* h (q a b) -> p (h a) (h b) :* q (h a) (h b)
-- uncurry (:**:)      :: p (h a) (h b) :* q (h a) (h b) -> (p :**: q) (h a) (h b)

instance (PointedCat k h a, PointedCat k' h a) => PointedCat (k :**: k') h a where
  pointC = pointC :**: pointC
  {-# INLINE pointC #-}

-- instance (DiagCat k h, DiagCat k' h) => DiagCat (k :**: k') h where
--   diagC  = diagC :**: diagC
--   {-# INLINE diagC #-}

-- instance (SumCat k h a, SumCat k' h a) => SumCat (k :**: k') h a where
--   sumC = sumC :**: sumC
--   {-# INLINE sumC #-}

instance (AddCat k h a, AddCat k' h a) => AddCat (k :**: k') h a where
  sumAC = sumAC :**: sumAC
  {-# INLINE sumAC #-}

-- instance (IxSummableCat k h a, IxSummableCat k' h a) => IxSummableCat (k :**: k') h a where
--   ixSumC = ixSumC :**: ixSumC
--   {-# INLINE ixSumC #-}

class TraversableCat k t f where
  sequenceAC :: Ok k a => t (f a) `k` f (t a)

-- TODO: perhaps remove the f parameter:
--
-- class TraversableCat k g where
--   sequenceAC :: (OkFunctor k f, Ok k a) => t (f a) `k` f (t a)

instance (Traversable t, Applicative f) => TraversableCat (->) t f where
  sequenceAC = IC.inline sequenceA
  {-# OPINLINE sequenceAC #-}

instance (TraversableCat k t f, TraversableCat k' t f)
      => TraversableCat (k :**: k') t f where
  sequenceAC = sequenceAC :**: sequenceAC
  {-# INLINE sequenceAC #-}

class DistributiveCat k g f where
  distributeC :: Ok k a => f (g a) `k` g (f a)

-- TODO: perhaps remove the f parameter:
--
-- class DistributiveCat k g where
--   distributeC :: (OkFunctor k f, Ok k a) => f (g a) `k` g (f a)

instance (Distributive g, Functor f) => DistributiveCat (->) g f where
  distributeC = IC.inline distribute
  {-# OPINLINE distributeC #-}

instance (DistributiveCat k g f, DistributiveCat k' g f)
      => DistributiveCat (k :**: k') g f where
  distributeC = distributeC :**: distributeC
  {-# INLINE distributeC #-}

class RepresentableCat k f where
  tabulateC :: Ok k a => (Rep f -> a) `k` f a
  indexC    :: Ok k a => f a `k` (Rep f -> a)

instance Representable f => RepresentableCat (->) f where
  tabulateC = IC.inline tabulate
  indexC    = IC.inline index
  {-# OPINLINE tabulateC #-}
  {-# OPINLINE indexC #-}

instance (RepresentableCat k h, RepresentableCat k' h)
      => RepresentableCat (k :**: k') h where
  tabulateC = tabulateC :**: tabulateC
  indexC    = indexC    :**: indexC
  {-# INLINE tabulateC #-}
  {-# INLINE indexC #-}

---- Experiment

-- fmap' and liftA2' are class-op-inlining synonyms for fmap and liftA2. Look
-- for a better alternative. See 2017-10-20 notes.

fmap' :: Functor f => (a -> b) -> f a -> f b
fmap' = IC.inline fmap

liftA2' :: Applicative f => (a -> b -> c) -> f a -> f b -> f c
liftA2' f as bs = fmap' f as <*> bs

-- dbanas 2018-01-08
zipWith' :: Zip f => (a -> b -> c) -> f a -> f b -> f c
zipWith' = IC.inline zipWith

class FunctorCat k h => Strong k h where
  strength :: Ok2 k a b => (a :* h b) `k` h (a :* b)

instance Functor h => Strong (->) h where
  strength (a,bs) = (a,) <$> bs

instance (Strong k h, Strong k' h) => Strong (k :**: k') h where
  strength = strength :**: strength

{--------------------------------------------------------------------
    Indexed products and coproducts
--------------------------------------------------------------------}

-- I intend to replace all of the functor-level vocabulary with indexed products
-- and coproducts.

class OkIxProd k h where
  okIxProd :: Ok' k a |- Ok' k (h a)
-- TODO: Now same as OkFunctor, so drop one.

class (Category k, OkIxProd k h) => IxMonoidalPCat k h where
  crossF :: forall a b. Ok2 k a b => h (a `k` b) -> (h a `k` h b)

class IxMonoidalPCat k h => IxProductCat k h where
  exF    :: forall a  . Ok  k a   => h (h a `k` a)
  forkF  :: forall a b. Ok2 k a b => h (a `k` b) -> (a `k` h b)
  replF  :: forall a  . Ok  k a   => a `k` h a
  -- Defaults
  forkF fs = crossF fs . replF <+ okIxProd @k @h @a <+ okIxProd @k @h @b
  default replF :: forall a . (Pointed h, Ok k a) => a `k` h a
  replF     = forkF (point id)
  {-# INLINE forkF #-}
  {-# INLINE replF #-}
  {-# MINIMAL exF, (forkF | replF) #-}

  -- default crossF :: forall a b. (Zip h, Ok2 k a b) => h (a `k` b) -> (h a `k` h b)
  -- crossF fs = forkF (zipWith (.) fs exF) <+ okIxProd @k @h @a
  -- {-# INLINE crossF #-}

#if 0
-- Types for forkF

fs                :: h (a `k` b)
crossF fs         :: h a `k` h b
crossF fs . replF :: a `k` h b

-- Types for crossF

                      exF  :: h (h a `k` a)
                   fs      :: h (a `k` b)
       zipWith (.) fs exF  :: h (h a `k` b)
forkF (zipWith (.) fs exF) :: h a `k` h b

-- Types for `replF` via `forkF`:

       const id  :: h (a `k` a)
forkF (const id) :: a `k` h a

-- Laws:

forkF exF == id
(. forkF fs) <$> exF == fs

-- Types:

      exF :: h (h b `k` b)
forkF exF :: h b `k` h b

         fs          :: h (a `k` b)
   forkF fs          :: a `k` h b
(. forkF fs)         :: (h b `k` b) -> (a `k` b)
             <$> exF :: h (h b `k` b)
(. forkF fs) <$> exF :: h (a `k` b)

#endif

instance OkIxProd (->) h where okIxProd = Entail (Sub Dict)

instance Zip h => IxMonoidalPCat (->) h where
  crossF = zipWith id -- 2018-02-07 notes
  {-# INLINE crossF #-}

instance (Representable h, Zip h, Pointed h) => IxProductCat (->) h where
  exF    = tabulate (flip index)
  replF  = point
           -- zap
  forkF = \ fs x -> ($ x) <$> fs
  {-# OPINLINE exF    #-}
  {-# OPINLINE replF  #-}
  {-# OPINLINE forkF #-}

--           flip index :: Rep h -> h a -> a
-- tabulate (flip index) :: h (h a -> a)
-- 
-- point :: a -> h a
-- zap   :: h (a -> b) -> h a -> h b

instance OkIxProd U2 h where
  okIxProd = Entail (Sub Dict)

instance IxMonoidalPCat U2 h where
  crossF = const U2

instance Pointed h => IxProductCat U2 h where
  exF    = point U2
  forkF  = const U2
  replF  = U2

instance (OkIxProd k h, OkIxProd k' h) => OkIxProd (k :**: k') h where
  okIxProd :: forall a. Ok' (k :**: k') a |- Ok' (k :**: k') (h a)
  okIxProd = Entail (Sub (Dict <+ okIxProd @k  @h @a
                               <+ okIxProd @k' @h @a))

instance (IxMonoidalPCat k h, IxMonoidalPCat k' h, Zip h) => IxMonoidalPCat (k :**: k') h where
  crossF = prod . (crossF *** crossF) . unzip . fmap unProd

instance (IxProductCat k h, IxProductCat k' h, Zip h) => IxProductCat (k :**: k') h where
  exF    = zipWith (:**:) exF exF
  forkF  = prod . (forkF  *** forkF ) . unzip . fmap unProd
  replF  = replF :**: replF

class (OkFunctor k h, Ok k a) => MinMaxFunctorCat k h a where
  minimumC :: h a `k` a
  maximumC :: h a `k` a

instance (MinMaxFunctorCat k h a, MinMaxFunctorCat k' h a) => MinMaxFunctorCat (k :**: k') h a where
  minimumC = minimumC :**: minimumC
  maximumC = maximumC :**: maximumC
  
instance MinMax h a => MinMaxFunctorCat (->) h a where
  minimumC = minimum
  maximumC = maximum
  {-# OPINLINE minimumC #-}
  {-# OPINLINE maximumC #-}

-- needed to construct the typeclass hierarchy for MinMaxFunctorCat
class (OkFunctor k h, Ok k a) => MinMaxFFunctorCat k h a where
  minimumCF :: h a -> (a :* (h a `k` a))
  maximumCF :: h a -> (a :* (h a `k` a))

instance MinMaxRep h a => MinMaxFFunctorCat (->) h a where
  minimumCF h =
    let (i, v) = minimumRep h
    in (v, flip index i)

  maximumCF h =
    let (i, v) = maximumRep h
    in (v, flip index i)
  {-# OPINLINE minimumCF #-}
  {-# OPINLINE maximumCF #-}

instance (MinMaxFFunctorCat k h a, MinMaxFFunctorCat k' h a, Ord a) => MinMaxFFunctorCat (k :**: k') h a where
  minimumCF h =
    let (a, f) = minimumCF h
        (a', f') = minimumCF h
    in (min a a', f :**: f') -- min is fishy here: they should both agree
  maximumCF h =
    let (a, f) = maximumCF h
        (a', f') = maximumCF h
    in (max a a', f :**: f') -- ditto is fishy here: they should both agree

#if 0
-- forkF:
fmap unProd     :: h ((k :**: k') a b) -> h ((a `k` b) :* (a `k'` b))
unzip           :: ... -> h (a `k` b) :* h (a `k'` b)
forkF *** forkF :: ... -> (a `k` h b) :* (a `k'` h b)
prod            :: ... -> (k :**: k') a (h b)
#endif

#if 0

class OkIxCoprod k n where
  okIxCoprod :: Ok' k a |- Ok' k (n , a)

-- TODO: is there a functor-style equivalent/dual for (n , a), say some kind of
-- co-representable thingy?

-- | Indexed monoidal coproducts
class (Category k, OkIxCoprod k h) => IxMonoidalSCat k n where
  plusF :: forall a b . Ok2 k a b => h (b `k` a) -> ((n , b) `k` (n , a))

  -- -- Defaults
  -- plusF fs = joinF (zipWith (.) inF fs) <+ okIxCoprod @k @n @a
  -- {-# INLINE plusF #-}

-- | Indexed cocartesian
class IxMonoidalSCat k h => IxCoproductCat k n where
  inF   :: forall a   . Ok  k a   => h (a `k` (n , a))
  joinF :: forall a b . Ok2 k a b => h (b `k` a) -> ((n , b) `k` a)
  jamF  :: forall a   . Ok  k a   => (n , a) `k` a
  joinF fs = jamF . plusF fs <+ okIxCoprod @k @n @a <+ okIxCoprod @k @n @b
  jamF     = joinF (const id)  -- or exr if we assumed products.
  {-# INLINE joinF #-}
  {-# INLINE jamF #-}
  {-# MINIMAL inF, (joinF | jamF) #-}

instance OkIxCoprod (->) n where okIxCoprod = Entail (Sub Dict)

instance IxCoproductCat (->) n where
  inF   = (,)
  joinF = uncurry
  jamF  = snd
  {-# OPINLINE inF   #-}
  {-# OPINLINE joinF #-}
  {-# OPINLINE jamF  #-}

#if 0

-- Types for plusF default:

                   inF     :: h (a `k` (n , a))
                       fs  :: h (b `k` a)
       zipWith (.) inF fs  :: h (b `k` (n , a))
joinF (zipWith (.) inF fs) :: (n , b) `k` (n , a)

-- Types for `joinPF` default:

               fs :: h (b `k` a)
        plusPF fs :: (n , b) `k` (n , a)
jamPF . plusPF fs :: (n , b) `k` a

-- Types for `jamF` default:

       const id  :: h (a `k` a)
joinF (const id) :: (n , a) `k` a

-- Laws:

joinF inF == id
(joinF fs .) <$> inF == fs

-- Types:

       inF :: h (b `k` h b)
joinF inF :: h b `k` h b

          fs         :: h (b `k` a)
   joinF fs          :: h b `k` a
(. joinF fs)         :: (b `k` h b) -> (b `k` a)
             <$> inF :: h (b `k` h b)
(. joinF fs) <$> inF :: h (b `k` a)

#endif

instance OkIxCoprod U2 n where
  okIxCoprod = Entail (Sub Dict)

instance IxMonoidalSCat U2 n where
  plusF = const U2

instance IxCoproductCat U2 n where
  inF   = pure U2
  joinF = const U2
  jamF  = U2

instance (OkIxCoprod k n, OkIxCoprod k' n) => OkIxCoprod (k :**: k') n where
  okIxCoprod :: forall a. Ok' (k :**: k') a |- Ok' (k :**: k') (n , a)
  okIxCoprod = Entail (Sub (Dict <+ okIxCoprod @k  @n @a
                                 <+ okIxCoprod @k' @n @a))

instance (IxMonoidalSCat k n, IxMonoidalSCat k' n) => IxMonoidalSCat (k :**: k) n where
  plusF = prod . (plusF *** plusF) . unzip . fmap unProd

instance (IxCoproductCat k n, IxCoproductCat k' n) => IxCoproductCat (k :**: k') n where
  inF   = zipWith (:**:) inF inF
  joinF = prod . (joinF *** joinF) . unzip . fmap unProd
  jamF  = jamF :**: jamF

#endif

-- Functor additivity
class Additive1 h where additive1 :: Sat Additive a |- Sat Additive (h a)

instance Additive1 ((->) a) where additive1 = Entail (Sub Dict)
instance Additive1 Sum      where additive1 = Entail (Sub Dict)
instance Additive1 Product  where additive1 = Entail (Sub Dict)
instance Additive1 U1       where additive1 = Entail (Sub Dict)
instance Additive1 Par1     where additive1 = Entail (Sub Dict)
instance (AddF f, AddF g) => Additive1 (f :*: g)  where additive1 = Entail (Sub Dict)
instance (AddF f, AddF g) => Additive1 (g :.: f)  where additive1 = Entail (Sub Dict)
instance KnownNat n       => Additive1 (Vector n) where additive1 = Entail (Sub Dict)

-- TODO: move Additive1 elsewhere

-- | Indexed coproducts as indexed products.
class (IxMonoidalPCat k h, OkIxProd k h) => IxCoproductPCat k h where
  inPF   :: forall a   . Ok  k a   => h (a `k` h a)
  joinPF :: forall a b . Ok2 k a b => h (b `k` a) -> (h b `k` a)
  -- plusPF :: forall a b . Ok2 k a b => h (b `k` a) -> (h b `k` h a)  -- same as crossPF
  jamPF  :: forall a   . Ok  k a   => h a `k` a
  -- Defaults
  -- default plusPF :: forall a b . (Zip h, Ok2 k a b) => h (b `k` a) -> (h b `k` h a)
  -- plusPF fs = joinPF (zipWith (.) inPF fs)
  --     <+ okIxProd @k @h @a
  default joinPF :: forall a b . (IxMonoidalPCat k h, Ok2 k a b) => h (b `k` a) -> (h b `k` a)
  joinPF fs = jamPF . crossF fs <+ okIxProd @k @h @a <+ okIxProd @k @h @b
  default jamPF :: forall a . (Pointed h, Ok k a) => h a `k` a
  jamPF     = joinPF (point id)
  {-# INLINE joinPF #-}
  -- {-# INLINE plusPF #-}
  {-# INLINE jamPF #-}
  -- {-# MINIMAL inPF, (joinPF | (plusPF, jamPF)) #-}
  {-# MINIMAL inPF, (joinPF | jamPF) #-}

#if 0

-- Types for `joinPF` default:

               fs :: h (b `k` a)
        plusPF fs :: h b `k` h a
jamPF . plusPF fs :: h b `k` a

-- Types for `plusPF` default:

                    inPF     :: h (a `k` h a)
                         fs  :: h (b `k` a)
        zipWith (.) inPF fs  :: h (b `k` h a)
joinPF (zipWith (.) inPF fs) :: h b `k` h a

-- Types for `jamPF` via `joinPF`:

        const id  :: h (a `k` a)
joinPF (const id) :: h a `k` a

-- Laws:

joinPF inPF == id
(joinPF fs .) <$> inPF == fs

-- Types:

       inPF :: h (b `k` h b)
joinPF inPF :: h b `k` h b

          fs           :: h (b `k` a)
   joinPF fs           :: h b `k` a
(. joinPF fs)          :: (b `k` h b) -> (b `k` a)
              <$> inPF :: h (b `k` h b)
(. joinPF fs) <$> inPF :: h (b `k` a)

#endif

-- instance Summable h => IxCoproductPCat (->) h where
--   inPF      = tabulate (\ i a -> tabulate (\ j -> if i == j then a else zero))
--   plusPF    = crossF
--   jamPF     = sumA
--   {-# OPINLINE inPF #-}
--   {-# OPINLINE plusPF #-}
--   {-# OPINLINE jamPF #-}

  -- joinPF fs = jamPF . plusPF fs  -- default, so remove
  -- {-# OPINLINE joinPF #-}

-- inPF :: h (a -> h a)

-- Rep h -> a -> h a
-- Rep h -> a -> Rep h -> a

-- jamPF :: h a -> a

instance Pointed h => IxCoproductPCat U2 h where
  inPF   = point U2
  joinPF = const U2
  jamPF  = U2
  -- plusPF = const U2

instance (IxCoproductPCat k h, IxCoproductPCat k' h, Zip h)
      => IxCoproductPCat (k :**: k') h where
  inPF   = zipWith (:**:) inPF inPF
  joinPF = prod . (joinPF *** joinPF) . unzip . fmap unProd
  jamPF  = jamPF :**: jamPF
  -- plusPF = prod . (plusPF *** plusPF) . unzip . fmap unProd

{--------------------------------------------------------------------
    Finite
--------------------------------------------------------------------}

class FiniteCat k where
  unFinite     :: KnownNat n => Finite n `k` Int
  unsafeFinite :: KnownNat n => Int `k` Finite n

instance FiniteCat (->) where
  unsafeFinite :: KnownNat n => Int -> Finite n
  unsafeFinite n = Finite (fromIntegral n)
  unFinite :: Finite n -> Int
  unFinite (Finite n) = fromInteger n
  {-# OPINLINE unsafeFinite #-}
  {-# OPINLINE unFinite #-}

instance (FiniteCat k,FiniteCat k') => FiniteCat (k :**: k') where
  unFinite     = unFinite     :**: unFinite
  unsafeFinite = unsafeFinite :**: unsafeFinite

#if 0
{--------------------------------------------------------------------
    Obsolete
--------------------------------------------------------------------}

-- | Alias for '(***)'
(++++) :: (MonoidalPCat k, Ok4 k a b c d) =>
          (c `k` a) -> (d `k` b) -> (CoprodP k c d `k` CoprodP k a b)
(++++) = (***)
{-# INLINE (++++) #-}

-- Alias for 'crossF'
plusPF :: (IxMonoidalPCat k h, Ok2 k a b) => h (b `k` a) -> (h b `k` h a)
plusPF = crossF
{-# INLINE plusPF #-}
#endif

#if 0

{--------------------------------------------------------------------
    Experimental
--------------------------------------------------------------------}

-- Experimentally moved from ConCat.AltCat
crossSecondFirst :: forall k a b c d. (MonoidalPCat k, Ok4 k a b c d)
                 => a `k` c -> b `k` d -> (a :* b) `k` (c :* d)
f `crossSecondFirst` g = second g . first f
                         <+ okProd @k @a @b
                         <+ okProd @k @c @b
                         <+ okProd @k @c @d
{-# INLINE crossSecondFirst #-}

#endif