{-# OPTIONS_GHC -Wno-orphans #-}
module Proarrow.Tools.Laws where

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

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

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 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]

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)