{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Tools.Laws where

import Data.Data ((:~:) (..), Typeable)
import Data.Kind (Constraint, Type)
import GHC.TypeLits (KnownSymbol, Symbol)
import Prelude (Show)

import Proarrow.Category.Instance.Free (FREE (..), Free, Show2, All)
import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), dimapDefault)

data family Var (cs :: [Kind -> Constraint]) (a :: Symbol) (b :: Symbol)
class Laws (cs :: [Kind -> Constraint]) where
  type EqTypes cs :: [FREE cs (Var cs)]
  laws :: [AssertEq cs]

infix 0 :=:
type AssertEq :: [Kind -> Constraint] -> Type
data AssertEq cs where
  (:=:)
    :: forall {cs} (a :: FREE cs (Var cs)) (b :: FREE cs (Var cs))
     . (a `Elem` EqTypes cs, b `Elem` EqTypes cs) => Free a b -> Free a b -> AssertEq cs
deriving instance (Show2 (Var cs)) => Show (AssertEq cs)

data Place as a where
  Here :: Place (a ': as) a
  There :: (b `Elem` as) => Place (a ': as) b

type Elem :: forall {a}. a -> [a] -> Constraint
class c `Elem` cs where
  place :: Place cs c
instance {-# OVERLAPPABLE #-} (c `Elem` cs) => c `Elem` (d ': cs) where
  place :: Place (d : cs) c
place = Place (d : cs) c
forall (a :: Kind) (c :: a) (cs :: [a]) (d :: a).
Elem c cs =>
Place (d : cs) c
There
instance c `Elem` (c ': cs) where
  place :: Place (c : cs) c
place = Place (c : cs) c
forall (a :: Kind) (c :: a) (cs :: [a]). Place (c : cs) c
Here

data Sym a b where
  Sym :: (KnownSymbol a, KnownSymbol b) => a :~: b -> Sym a b
instance Profunctor (Sym :: CAT Symbol) where
  dimap :: forall (c :: Symbol) (a :: Symbol) (b :: Symbol) (d :: Symbol).
(c ~> a) -> (b ~> d) -> Sym a b -> Sym c d
dimap = (c ~> a) -> (b ~> d) -> Sym a b -> Sym c d
Sym c a -> Sym b d -> Sym a b -> Sym c d
forall {k :: Kind} (p :: k +-> k) (c :: k) (a :: k) (b :: k)
       (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: Symbol) (b :: Symbol) (r :: Kind).
((Ob a, Ob b) => r) -> Sym a b -> r
\\ Sym{} = r
(Ob a, Ob b) => r
r
instance Promonad (Sym :: CAT Symbol) where
  id :: forall (a :: Symbol). Ob a => Sym a a
id = (a :~: a) -> Sym a a
forall (a :: Symbol) (b :: Symbol).
(KnownSymbol a, KnownSymbol b) =>
(a :~: b) -> Sym a b
Sym a :~: a
forall {k :: Kind} (a :: k). a :~: a
Refl
  Sym b :~: c
Refl . :: forall (b :: Symbol) (c :: Symbol) (a :: Symbol).
Sym b c -> Sym a b -> Sym a c
. Sym a :~: b
Refl = (a :~: c) -> Sym a c
forall (a :: Symbol) (b :: Symbol).
(KnownSymbol a, KnownSymbol b) =>
(a :~: b) -> Sym a b
Sym a :~: c
a :~: a
forall {k :: Kind} (a :: k). a :~: a
Refl
instance CategoryOf Symbol where
  type (~>) = Sym
  type Ob a = (KnownSymbol a)

iso :: forall {cs} (a :: FREE cs (Var cs)) (b :: FREE cs (Var cs))
     . (a `Elem` EqTypes cs, b `Elem` EqTypes cs, All cs (FREE cs (Var cs)), Typeable cs)
     => Free a b -> Free b a -> [AssertEq cs]
iso :: forall {cs :: [Kind -> Constraint]} (a :: FREE cs (Var cs))
       (b :: FREE cs (Var cs)).
(Elem a (EqTypes cs), Elem b (EqTypes cs),
 All cs (FREE cs (Var cs)), Typeable cs) =>
Free a b -> Free b a -> [AssertEq cs]
iso Free a b
f Free b a
g = [Free a b
f Free a b -> Free b a -> Free b b
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FREE cs (Var cs)) (c :: FREE cs (Var cs))
       (a :: FREE cs (Var cs)).
Free b c -> Free a b -> Free a c
. Free b a
g Free b b -> Free b b -> AssertEq cs
forall {cs :: [Kind -> Constraint]} (a :: FREE cs (Var cs))
       (b :: FREE cs (Var cs)).
(Elem a (EqTypes cs), Elem b (EqTypes cs)) =>
Free a b -> Free a b -> AssertEq cs
:=: Free b b
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
forall (a :: FREE cs (Var cs)). Ob a => Free a a
id, Free b a
g Free b a -> Free a b -> Free a a
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FREE cs (Var cs)) (c :: FREE cs (Var cs))
       (a :: FREE cs (Var cs)).
Free b c -> Free a b -> Free a c
. Free a b
f Free a a -> Free a a -> AssertEq cs
forall {cs :: [Kind -> Constraint]} (a :: FREE cs (Var cs))
       (b :: FREE cs (Var cs)).
(Elem a (EqTypes cs), Elem b (EqTypes cs)) =>
Free a b -> Free a b -> AssertEq cs
:=: Free a a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
forall (a :: FREE cs (Var cs)). Ob a => Free a a
id] ((Ob a, Ob b) => [AssertEq cs]) -> Free a b -> [AssertEq cs]
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs (Var cs)) (b :: FREE cs (Var cs)) (r :: Kind).
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free a b
f ((Ob b, Ob a) => [AssertEq cs]) -> Free b a -> [AssertEq cs]
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs (Var cs)) (b :: FREE cs (Var cs)) (r :: Kind).
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free b a
g