# language BlockArguments #
{-# language DefaultSignatures #-}
# language DerivingStrategies #
# language EmptyCase #
{-# language ExplicitNamespaces #-}
# language ImportQualifiedPost #
{-# language FlexibleContexts #-}
# language FlexibleInstances #
# language FunctionalDependencies #
# language GADTs #
# language LambdaCase #
{-# language LinearTypes #-}
# language NoStarIsType #
# language PolyKinds #
# language QuantifiedConstraints #
# language RankNTypes #
# language RoleAnnotations #
{-# language ScopedTypeVariables #-}
# language StandaloneDeriving #
# language StandaloneKindSignatures #
# language StrictData #
{-# language TupleSections #-}
# language TypeApplications #
{-# language TypeFamilies #-}
# language TypeFamilyDependencies #
# language TypeOperators #
{-# language UndecidableInstances #-}
# language UndecidableSuperClasses #

module T19627 where

import Data.Kind
import Prelude hiding ( Functor(..) )

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

class (Prop (Not p), Not (Not p) ~ p) => Prop (p :: Type) where
  type Not p :: Type
  (!=) :: p -> Not p -> r

data Y (a :: Type) (b :: Type) (c :: Type) where
  L :: Y a b a
  R :: Y a b b

newtype a & b = With (forall c. Y a b c -> c)

with :: (forall c. Y a b c -> c) -> a & b
with = With

runWith :: a & b -> Y a b c -> c
runWith (With f) = f

withL' :: a & b -> a
withL' (With f) = f L

withR' :: a & b -> b
withR' (With f) = f R

instance (Prop a, Prop b) => Prop (a & b) where
  type Not (a & b) = Not a `Either` Not b
  w != Left a  = withL' w != a
  w != Right b = withR' w != b

instance (Prop a, Prop b) => Prop (Either a b) where
  type Not (Either a b) = Not a & Not b
  Left a  != w = a != withL' w
  Right a != w = a != withR' w

newtype Yoneda f a = Yoneda
  (forall r. Prop r => (a -> r) -> f r)

data Noneda f a where
  Noneda :: Prop r => !(f r <#- (a ⊸ r)) -> Noneda f a

liftYoneda :: forall f a i. (Functor f, Prop a, Iso i) => i (f a) (Yoneda f a)
liftYoneda = iso \case
  L -> lowerYoneda'
  R -> lol \case
    L -> \(Noneda ((a2r :: a ⊸ r) :-#> nfr)) -> runLol (fmap @f @a @r a2r) L nfr
    R -> \fa -> Yoneda do
      lol \case
        R -> \f -> fmap' f fa
        L -> \nfr -> whyNot \a2r -> fmap a2r fa != nfr


type family NotApart (p :: Type -> Type -> Type) :: Type -> Type -> Type

class
  ( forall a b. (Prop a, Prop b) => Prop (p a b)
  , NotApart (NotIso p) ~ p
  ) => Iso p where
  type NotIso p = (q :: Type -> Type -> Type) | q -> p
  iso :: (forall c. Y (b ⊸ a) (a ⊸ b) c -> c) -> p a b

data b <#- a where (:-#>) :: a -> Not b -> b <#- a
newtype a ⊸ b = Lol (forall c. Y (Not b %1 -> Not a) (a %1 -> b) c -> c)

class
  ( forall a. Prop a => Prop (f a)
  ) => Functor f where
  fmap' :: (Prop a, Prop b, Lol l, Lol l') => l ((a ⊸ b)) (l' (f a) (f b))

fmap :: forall f a b l. (Functor f, Prop a, Prop b, Lol l) => (a ⊸ b) -> l (f a) (f b)
fmap f = fmap' f

class Iso p => Lol (p :: Type -> Type -> Type) where
  lol :: (forall c. Y (Not b -> Not a) (a -> b) c -> c) -> p a b
  apartR :: Not (p a b) -> b <#- a

# language DefaultSignatures #
# language ExplicitNamespaces #
# language FlexibleContexts #
# language LinearTypes #
# language ScopedTypeVariables #
# language TupleSections #
# language TypeFamilies #
# language UndecidableInstances #
------------------
# language BlockArguments #
# language DerivingStrategies #
# language EmptyCase #
# language ImportQualifiedPost #
# language FlexibleInstances #
# language FunctionalDependencies #
# language GADTs #
# language LambdaCase #
# language NoStarIsType #
# language PolyKinds #
# language QuantifiedConstraints #
# language RankNTypes #
# language RoleAnnotations #
# language StandaloneDeriving #
# language StandaloneKindSignatures #
# language StrictData #
# language TypeApplications #
# language TypeFamilyDependencies #
# language TypeOperators #
# language UndecidableSuperClasses #

module T19627 where

import Data.Kind
import Prelude hiding ( Functor(..) )


class (Prop (Not p), Not (Not p) ~ p) => Prop (p :: Type) where
  type Not p :: Type
  (!=) :: p -> Not p -> r

data Y (a :: Type) (b :: Type) (c :: Type) where
  L :: Y a b a
  R :: Y a b b

newtype a & b = With (forall c. Y a b c -> c)

with :: (forall c. Y a b c -> c) -> a & b
with = With

runWith :: a & b -> Y a b c -> c
runWith (With f) = f

withL' :: a & b -> a
withL' (With f) = f L

withR' :: a & b -> b
withR' (With f) = f R

instance (Prop a, Prop b) => Prop (a & b) where
  type Not (a & b) = Not a `Either` Not b
  w != Left a  = withL' w != a
  w != Right b = withR' w != b

instance (Prop a, Prop b) => Prop (Either a b) where
  type Not (Either a b) = Not a & Not b
  Left a  != w = a != withL' w
  Right a != w = a != withR' w

newtype Yoneda f a = Yoneda
  (forall r. Prop r => (a -> r) -> f r)

data Noneda f a where
  Noneda :: Prop r => !(f r <#- (a ⊸ r)) -> Noneda f a

liftYoneda :: forall f a i. (Functor f, Prop a, Iso i) => i (f a) (Yoneda f a)
liftYoneda = iso \case
  L -> lowerYoneda'
  R -> lol \case
    L -> \(Noneda ((a2r :: a ⊸ r) :-#> nfr)) -> runLol (fmap @f @a @r a2r) L nfr
    R -> \fa -> Yoneda do
      lol \case
        R -> \f -> fmap' f fa
        L -> \nfr -> whyNot \a2r -> fmap a2r fa != nfr


type family NotApart (p :: Type -> Type -> Type) :: Type -> Type -> Type

class
  ( forall a b. (Prop a, Prop b) => Prop (p a b)
  , NotApart (NotIso p) ~ p
  ) => Iso p where
  type NotIso p = (q :: Type -> Type -> Type) | q -> p
  iso :: (forall c. Y (b ⊸ a) (a ⊸ b) c -> c) -> p a b

data b <#- a where (:-#>) :: a -> Not b -> b <#- a
newtype a ⊸ b = Lol (forall c. Y (Not b %1 -> Not a) (a %1 -> b) c -> c)

class
  ( forall a. Prop a => Prop (f a)
  ) => Functor f where
  fmap' :: (Prop a, Prop b, Lol l, Lol l') => l ((a ⊸ b)) (l' (f a) (f b))

fmap :: forall f a b l. (Functor f, Prop a, Prop b, Lol l) => (a ⊸ b) -> l (f a) (f b)
fmap f = fmap' f

class Iso p => Lol (p :: Type -> Type -> Type) where
  lol :: (forall c. Y (Not b -> Not a) (a -> b) c -> c) -> p a b
  apartR :: Not (p a b) -> b <#- a
