-- | Work in Progress.
module Kindly.Rank2 where

--------------------------------------------------------------------------------

import Data.Bool (Bool (..))
import Kindly.Class

--------------------------------------------------------------------------------

data MyHKD f = MyHKD {forall (f :: * -> *). MyHKD f -> f Bool
one :: f Bool, forall (f :: * -> *). MyHKD f -> f ()
two :: f ()}

instance CategoricalFunctor MyHKD where
  type Dom MyHKD = (->) ~> (->)
  type Cod MyHKD = (->)

  map :: (Nat (->) (->)) f g -> MyHKD f -> MyHKD g
  map :: forall (f :: * -> *) (g :: * -> *).
Nat (->) (->) f g -> MyHKD f -> MyHKD g
map (Nat forall x. f x -> g x
nat) MyHKD {f Bool
f ()
one :: forall (f :: * -> *). MyHKD f -> f Bool
two :: forall (f :: * -> *). MyHKD f -> f ()
one :: f Bool
two :: f ()
..} = g Bool -> g () -> MyHKD g
forall (f :: * -> *). f Bool -> f () -> MyHKD f
MyHKD (f Bool -> g Bool
forall x. f x -> g x
nat f Bool
one) (f () -> g ()
forall x. f x -> g x
nat f ()
two)

newtype MyHKD2 p = MyHKD2 {forall (p :: * -> * -> *). MyHKD2 p -> p () Bool
field :: p () Bool}

instance CategoricalFunctor MyHKD2 where
  type Dom MyHKD2 = (->) ~> ((->) ~> (->))
  type Cod MyHKD2 = (->)

  map :: Dom MyHKD2 p q -> MyHKD2 p -> MyHKD2 q
  map :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Dom MyHKD2 p q -> MyHKD2 p -> MyHKD2 q
map (Nat (Nat forall x. p () x -> q () x
nat)) MyHKD2 {p () Bool
field :: forall (p :: * -> * -> *). MyHKD2 p -> p () Bool
field :: p () Bool
..} = q () Bool -> MyHKD2 q
forall (p :: * -> * -> *). p () Bool -> MyHKD2 p
MyHKD2 (p () Bool -> q () Bool
forall x. p () x -> q () x
nat p () Bool
field)