{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

{- | This module provides a way to represent \"tag\" of various polynomial data types. For example,
a GADT 'TagMaybe' represents a functor of the same shape of 'Maybe'.

> data TagMaybe n where
>    TagNothing :: TagMaybe Void -- ^ Nothing takes 0 parameter
>    TagJust    :: TagMaybe ()   -- ^ Just takes 1 paramerer

-}
module Data.Functor.Polynomial.Tag(
  -- * The type class for tags
  HasFinitary(..),

  -- * Tags
  TagMaybe(..),
  TagList(..),

  TagFn, TagV(), TagK(..), TagSum, TagMul(..),
  TagPow(..), geqPow, gcomparePow,
  TagComp(..),
  TagDay(..),

  -- * Reexports

  GShow(..), GEq(..), GCompare(..), GOrdering(..)
) where

import Data.Kind (Type)

import Data.Type.Equality ((:~:)(..))
import GHC.Generics ( type (:+:)(..) )

import GHC.TypeNats hiding (pattern SNat)
import GHC.TypeNats.Extra (SNat(SNat))
import Data.Void
import Data.Finitary (Finitary(..))
import Data.Finite (Finite)
import Data.Functor.Classes (showsUnaryWith)

import Data.GADT.HasFinitary
import Data.GADT.Show
import Data.GADT.Compare
    ( defaultCompare, defaultEq, GCompare(..), GEq(..), GOrdering(..) )
import Data.GADT.Compare.Extra ( fromOrdering, (>>?) )


import Data.Functor.Pow

-- | Tag of 'Maybe'.
data TagMaybe n where
    TagNothing :: TagMaybe Void
    TagJust    :: TagMaybe ()

deriving instance Eq (TagMaybe n)
deriving instance Ord (TagMaybe n)
deriving instance Show (TagMaybe n)

instance HasFinitary TagMaybe where
    withFinitary :: forall n r. TagMaybe n -> (Finitary n => r) -> r
withFinitary TagMaybe n
TagNothing Finitary n => r
body = r
Finitary n => r
body
    withFinitary TagMaybe n
TagJust Finitary n => r
body = r
Finitary n => r
body

instance GEq TagMaybe where
    geq :: forall a b. TagMaybe a -> TagMaybe b -> Maybe (a :~: b)
geq TagMaybe a
TagNothing TagMaybe b
TagNothing = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    geq TagMaybe a
TagJust TagMaybe b
TagJust = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    geq TagMaybe a
_ TagMaybe b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance GCompare TagMaybe where
    gcompare :: forall a b. TagMaybe a -> TagMaybe b -> GOrdering a b
gcompare TagMaybe a
TagNothing TagMaybe b
TagNothing = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
    gcompare TagMaybe a
TagNothing TagMaybe b
TagJust = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    gcompare TagMaybe a
TagJust TagMaybe b
TagNothing = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
    gcompare TagMaybe a
TagJust TagMaybe b
TagJust = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ

instance GShow TagMaybe where
    gshowsPrec :: forall n. Int -> TagMaybe n -> ShowS
gshowsPrec = Int -> TagMaybe a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

data TagList a where
  TagList :: KnownNat n => TagList (Finite n)

deriving instance Eq (TagList a)
deriving instance Ord (TagList a)

instance Show (TagList a) where
  showsPrec :: Int -> TagList a -> ShowS
showsPrec = Int -> TagList a -> ShowS
forall a. Int -> TagList a -> ShowS
forall k (t :: k -> Type) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec

instance HasFinitary TagList where
  withFinitary :: forall n r. TagList n -> (Finitary n => r) -> r
withFinitary TagList n
TagList Finitary n => r
body = r
Finitary n => r
body

instance GEq TagList where
  geq :: forall a b. TagList a -> TagList b -> Maybe (a :~: b)
geq (TagList @n) (TagList @m) =
    let sn :: SNat n
sn = SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat :: SNat n
        sm :: SNat n
sm = SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat :: SNat m
    in case SNat n -> SNat n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq SNat n
sn SNat n
sm of
          Maybe (n :~: n)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
          Just n :~: n
Refl -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

instance GCompare TagList where
  gcompare :: forall a b. TagList a -> TagList b -> GOrdering a b
gcompare (TagList @n) (TagList @m) =
    let sn :: SNat n
sn = SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat :: SNat n
        sm :: SNat n
sm = SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat :: SNat m
    in case SNat n -> SNat n -> GOrdering n n
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> GOrdering a b
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare SNat n
sn SNat n
sm of
          GOrdering n n
GLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
          GOrdering n n
GEQ -> GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
          GOrdering n n
GGT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT

instance GShow TagList where
  gshowsPrec :: forall a. Int -> TagList a -> ShowS
gshowsPrec Int
p (TagList @n) = (Int -> String -> ShowS) -> String -> Int -> String -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith ((String -> ShowS) -> Int -> String -> ShowS
forall a b. a -> b -> a
const String -> ShowS
forall a. [a] -> [a] -> [a]
(++)) String
"TagList" Int
p (String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @n SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat))

-- | @TagFn n@ represents @((), const n :: () -> Type)@.
--
--   This is the tag of @(->) r@ functor.
--
--   It's also the tag of 'Data.Proxy.Proxy' and 'Data.Functor.Identity',
--   by being isomorphic to @(->) Void@ and @(->) ()@ respectively.
--
--   > TagFn Void   -- Tag of Proxy
--   > TagFn ()     -- Tag of Identity
type TagFn = (:~:)

-- | @TagV n@ is an empty type for any @n@. It represents @(∅, α = absurd :: ∅ -> Nat)@. 
--
--   This is the tag of 'GHC.Generics.V1'.
type TagV :: Type -> Type
data TagV n
  deriving (TagV n -> TagV n -> Bool
(TagV n -> TagV n -> Bool)
-> (TagV n -> TagV n -> Bool) -> Eq (TagV n)
forall n. TagV n -> TagV n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall n. TagV n -> TagV n -> Bool
== :: TagV n -> TagV n -> Bool
$c/= :: forall n. TagV n -> TagV n -> Bool
/= :: TagV n -> TagV n -> Bool
Eq, Eq (TagV n)
Eq (TagV n) =>
(TagV n -> TagV n -> Ordering)
-> (TagV n -> TagV n -> Bool)
-> (TagV n -> TagV n -> Bool)
-> (TagV n -> TagV n -> Bool)
-> (TagV n -> TagV n -> Bool)
-> (TagV n -> TagV n -> TagV n)
-> (TagV n -> TagV n -> TagV n)
-> Ord (TagV n)
TagV n -> TagV n -> Bool
TagV n -> TagV n -> Ordering
TagV n -> TagV n -> TagV n
forall n. Eq (TagV n)
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall n. TagV n -> TagV n -> Bool
forall n. TagV n -> TagV n -> Ordering
forall n. TagV n -> TagV n -> TagV n
$ccompare :: forall n. TagV n -> TagV n -> Ordering
compare :: TagV n -> TagV n -> Ordering
$c< :: forall n. TagV n -> TagV n -> Bool
< :: TagV n -> TagV n -> Bool
$c<= :: forall n. TagV n -> TagV n -> Bool
<= :: TagV n -> TagV n -> Bool
$c> :: forall n. TagV n -> TagV n -> Bool
> :: TagV n -> TagV n -> Bool
$c>= :: forall n. TagV n -> TagV n -> Bool
>= :: TagV n -> TagV n -> Bool
$cmax :: forall n. TagV n -> TagV n -> TagV n
max :: TagV n -> TagV n -> TagV n
$cmin :: forall n. TagV n -> TagV n -> TagV n
min :: TagV n -> TagV n -> TagV n
Ord, Int -> TagV n -> ShowS
[TagV n] -> ShowS
TagV n -> String
(Int -> TagV n -> ShowS)
-> (TagV n -> String) -> ([TagV n] -> ShowS) -> Show (TagV n)
forall n. Int -> TagV n -> ShowS
forall n. [TagV n] -> ShowS
forall n. TagV n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall n. Int -> TagV n -> ShowS
showsPrec :: Int -> TagV n -> ShowS
$cshow :: forall n. TagV n -> String
show :: TagV n -> String
$cshowList :: forall n. [TagV n] -> ShowS
showList :: [TagV n] -> ShowS
Show)

absurdTagV :: TagV n -> any
absurdTagV :: forall n any. TagV n -> any
absurdTagV TagV n
v = case TagV n
v of { }

instance HasFinitary TagV where
  withFinitary :: forall n r. TagV n -> (Finitary n => r) -> r
withFinitary TagV n
v Finitary n => r
_ = TagV n -> r
forall n any. TagV n -> any
absurdTagV TagV n
v

instance GEq TagV where
  geq :: forall a b. TagV a -> TagV b -> Maybe (a :~: b)
geq = TagV a -> TagV b -> Maybe (a :~: b)
forall n any. TagV n -> any
absurdTagV

instance GCompare TagV where
  gcompare :: forall a b. TagV a -> TagV b -> GOrdering a b
gcompare = TagV a -> TagV b -> GOrdering a b
forall n any. TagV n -> any
absurdTagV

instance GShow TagV where
  gshowsPrec :: forall n. Int -> TagV n -> ShowS
gshowsPrec = Int -> TagV a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

-- | @TagK c n@ represents @(c, α)@, where @α@ is a constant function to @Void@:
--   
--   > α = const Void :: c -> Type
--   
--   This is the tag of 'Data.Functor.Const'.
type TagK :: Type -> Type -> Type
data TagK c n where
  TagK :: c -> TagK c Void

deriving instance Eq c => Eq (TagK c n)
deriving instance Ord c => Ord (TagK c n)
deriving instance Show c => Show (TagK c n)

instance HasFinitary (TagK c) where
  withFinitary :: forall n r. TagK c n -> (Finitary n => r) -> r
withFinitary (TagK c
_) Finitary n => r
body = r
Finitary n => r
body

instance Eq c => GEq (TagK c) where
  geq :: forall a b. TagK c a -> TagK c b -> Maybe (a :~: b)
geq (TagK c
c) (TagK c
c')
      | c
c c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
c' = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      | Bool
otherwise = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance Ord c => GCompare (TagK c) where
  gcompare :: forall a b. TagK c a -> TagK c b -> GOrdering a b
gcompare (TagK c
c) (TagK c
c') = Ordering -> GOrdering a a
forall {k} (a :: k). Ordering -> GOrdering a a
fromOrdering (c -> c -> Ordering
forall a. Ord a => a -> a -> Ordering
compare c
c c
c')

instance Show c => GShow (TagK c) where
  gshowsPrec :: forall a. Int -> TagK c a -> ShowS
gshowsPrec = Int -> TagK c a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

-- | When @t1, t2@ represents @(U, α1)@ and @(V,α2)@ respectively,
--   
--   > α1 :: U -> Nat
--   > α2 :: V -> Nat
--   
--   @TagSum t1 t2@ represents @(Either U V, β = either α1 α2)@.
--
--   > β :: Either U V -> Nat
--   > β (Left u)  = α1(u)
--   > β (Right v) = α2(v)
--
--   This is the tag of @f :+: g@, when @t1, t2@ is the tag of @f, g@ respectively.
type TagSum = (:+:)

-- |  When @t1, t2@ represents @(U, α1)@ and @(V,α2)@ respectively,
--   
--   > α1 :: U -> Nat
--   > α2 :: V -> Nat
--   
--   @TagMul t1 t2@ represents the direct product @(U,V)@ and the function @β@ on it:
--   
--   > β :: (U,V) -> Nat
--   > β(u,v) = α1 u + α2 v
--   
--   This is the tag of @f :*: g@ when @t1, t2@ is the tag of @f, g@ respectively.
data TagMul f g x where
  TagMul :: !(f x) -> !(g y) -> TagMul f g (Either x y)

instance (HasFinitary t1, HasFinitary t2) => HasFinitary (TagMul t1 t2) where
  withFinitary :: forall n r. TagMul t1 t2 n -> (Finitary n => r) -> r
withFinitary (TagMul t1 x
t1 t2 y
t2) Finitary n => r
body =
    t1 x -> (Finitary x => r) -> r
forall n r. t1 n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary t1 x
t1 ((Finitary x => r) -> r) -> (Finitary x => r) -> r
forall a b. (a -> b) -> a -> b
$ t2 y -> (Finitary y => r) -> r
forall n r. t2 n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary t2 y
t2 r
Finitary n => r
Finitary y => r
body

deriving instance (forall n. Show (t1 n), forall n. Show (t2 n)) => Show (TagMul t1 t2 m)
instance (forall n. Show (t1 n), forall n. Show (t2 n)) => GShow (TagMul t1 t2) where
  gshowsPrec :: forall a. Int -> TagMul t1 t2 a -> ShowS
gshowsPrec = Int -> TagMul t1 t2 a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

instance (GEq t1, GEq t2) => Eq (TagMul t1 t2 n) where
  == :: TagMul t1 t2 n -> TagMul t1 t2 n -> Bool
(==) = TagMul t1 t2 n -> TagMul t1 t2 n -> Bool
forall {k} (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq

instance (GEq t1, GEq t2) => GEq (TagMul t1 t2) where
  geq :: forall a b. TagMul t1 t2 a -> TagMul t1 t2 b -> Maybe (a :~: b)
geq (TagMul t1 x
t1 t2 y
t2) (TagMul t1 x
t1' t2 y
t2') =
    do x :~: x
Refl <- t1 x -> t1 x -> Maybe (x :~: x)
forall a b. t1 a -> t1 b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq t1 x
t1 t1 x
t1'
       y :~: y
Refl <- t2 y -> t2 y -> Maybe (y :~: y)
forall a b. t2 a -> t2 b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq t2 y
t2 t2 y
t2'
       (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

instance (GCompare t1, GCompare t2) => Ord (TagMul t1 t2 n) where
  compare :: TagMul t1 t2 n -> TagMul t1 t2 n -> Ordering
compare = TagMul t1 t2 n -> TagMul t1 t2 n -> Ordering
forall {k} (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare

instance (GCompare t1, GCompare t2) => GCompare (TagMul t1 t2) where
  gcompare :: forall a b. TagMul t1 t2 a -> TagMul t1 t2 b -> GOrdering a b
gcompare (TagMul t1 x
t1 t2 y
t2) (TagMul t1 x
t1' t2 y
t2') = t1 x -> t1 x -> GOrdering x x
forall a b. t1 a -> t1 b -> GOrdering a b
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare t1 x
t1 t1 x
t1' GOrdering x x -> ((x ~ x) => GOrdering a b) -> GOrdering a b
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? t2 y -> t2 y -> GOrdering y y
forall a b. t2 a -> t2 b -> GOrdering a b
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare t2 y
t2 t2 y
t2' GOrdering y y -> ((y ~ y) => GOrdering a b) -> GOrdering a b
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? GOrdering a a
GOrdering a b
(y ~ y) => GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ

-- | When @t, u@ is the tag of @f, g@ respectively,
--   @TagComp t u@ is the tag of @f :.: g@.
data TagComp t u n where
  TagComp :: t a -> TagPow (Cardinality a) u n -> TagComp t u n

instance (HasFinitary u) => HasFinitary (TagComp t u) where
  withFinitary :: forall n r. TagComp t u n -> (Finitary n => r) -> r
withFinitary (TagComp t a
_ TagPow (Cardinality a) u n
pu) Finitary n => r
body = TagPow (Cardinality a) u n -> (Finitary n => r) -> r
forall n r. TagPow (Cardinality a) u n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary TagPow (Cardinality a) u n
pu r
Finitary n => r
body

deriving instance (forall n. Show (t n), forall n. Show (u n)) => Show (TagComp t u m)
instance (forall n. Show (t n), forall n. Show (u n)) => GShow (TagComp t u) where
  gshowsPrec :: forall a. Int -> TagComp t u a -> ShowS
gshowsPrec = Int -> TagComp t u a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

instance (GEq t, GEq u) => GEq (TagComp t u) where
  geq :: forall a b. TagComp t u a -> TagComp t u b -> Maybe (a :~: b)
geq (TagComp t a
t TagPow (Cardinality a) u a
pu) (TagComp t a
t' TagPow (Cardinality a) u b
pu') =
    do a :~: a
Refl <- t a -> t a -> Maybe (a :~: a)
forall a b. t a -> t b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq t a
t t a
t'
       a :~: b
Refl <- TagPow (Cardinality a) u a
-> TagPow (Cardinality a) u b -> Maybe (a :~: b)
forall a b.
TagPow (Cardinality a) u a
-> TagPow (Cardinality a) u b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq TagPow (Cardinality a) u a
pu TagPow (Cardinality a) u b
TagPow (Cardinality a) u b
pu'
       (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

instance (GEq t, GEq u) => Eq (TagComp t u n) where
  == :: TagComp t u n -> TagComp t u n -> Bool
(==) = TagComp t u n -> TagComp t u n -> Bool
forall {k} (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq

instance (GCompare t, GCompare u) => GCompare (TagComp t u) where
  gcompare :: forall a b. TagComp t u a -> TagComp t u b -> GOrdering a b
gcompare (TagComp t a
t TagPow (Cardinality a) u a
pu) (TagComp t a
t' TagPow (Cardinality a) u b
pu') = t a -> t a -> GOrdering a a
forall a b. t a -> t b -> GOrdering a b
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare t a
t t a
t' GOrdering a a -> ((a ~ a) => GOrdering a b) -> GOrdering a b
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? TagPow (Cardinality a) u a
-> TagPow (Cardinality a) u b -> GOrdering a b
forall a b.
TagPow (Cardinality a) u a
-> TagPow (Cardinality a) u b -> GOrdering a b
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare TagPow (Cardinality a) u a
pu TagPow (Cardinality a) u b
TagPow (Cardinality a) u b
pu' GOrdering a b -> ((a ~ b) => GOrdering a b) -> GOrdering a b
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? GOrdering a a
GOrdering a b
(a ~ b) => GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ

instance (GCompare t, GCompare u) => Ord (TagComp t u n) where
  compare :: TagComp t u n -> TagComp t u n -> Ordering
compare = TagComp t u n -> TagComp t u n -> Ordering
forall {k} (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare

type TagDay :: (Type -> Type) -> (Type -> Type) -> Type -> Type
data TagDay t u n where
  TagDay :: t n -> u m -> TagDay t u (n, m)

instance (HasFinitary t, HasFinitary u) => HasFinitary (TagDay t u) where
  withFinitary :: forall n r. TagDay t u n -> (Finitary n => r) -> r
withFinitary (TagDay t n
t u m
u) Finitary n => r
body = t n -> (Finitary n => r) -> r
forall n r. t n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary t n
t (u m -> (Finitary m => r) -> r
forall n r. u n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary u m
u r
Finitary n => r
Finitary m => r
body)

deriving instance (forall n. Show (t n), forall n. Show (u n)) => Show (TagDay t u m)

instance (forall n. Show (t n), forall n. Show (u n)) => GShow (TagDay t u) where
  gshowsPrec :: forall a. Int -> TagDay t u a -> ShowS
gshowsPrec = Int -> TagDay t u a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

instance (GEq t, GEq u) => GEq (TagDay t u) where
  TagDay t n
t u m
u geq :: forall a b. TagDay t u a -> TagDay t u b -> Maybe (a :~: b)
`geq` TagDay t n
t' u m
u' =
    do n :~: n
Refl <- t n -> t n -> Maybe (n :~: n)
forall a b. t a -> t b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq t n
t t n
t'
       m :~: m
Refl <- u m -> u m -> Maybe (m :~: m)
forall a b. u a -> u b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq u m
u u m
u'
       (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

instance (GEq t, GEq u) => Eq (TagDay t u n) where
  == :: TagDay t u n -> TagDay t u n -> Bool
(==) = TagDay t u n -> TagDay t u n -> Bool
forall {k} (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq

instance (GCompare t, GCompare u) => GCompare (TagDay t u) where
  gcompare :: forall a b. TagDay t u a -> TagDay t u b -> GOrdering a b
gcompare (TagDay t n
t u m
u) (TagDay t n
t' u m
u') = t n -> t n -> GOrdering n n
forall a b. t a -> t b -> GOrdering a b
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare t n
t t n
t' GOrdering n n -> ((n ~ n) => GOrdering a b) -> GOrdering a b
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? u m -> u m -> GOrdering m m
forall a b. u a -> u b -> GOrdering a b
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare u m
u u m
u' GOrdering m m -> ((m ~ m) => GOrdering a b) -> GOrdering a b
forall {k1} k2 (a :: k2) (b :: k2) (a' :: k1) (b' :: k1).
GOrdering a b -> ((a ~ b) => GOrdering a' b') -> GOrdering a' b'
>>? GOrdering a a
GOrdering a b
(m ~ m) => GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ

instance (GCompare t, GCompare u) => Ord (TagDay t u m) where
  compare :: TagDay t u m -> TagDay t u m -> Ordering
compare = TagDay t u m -> TagDay t u m -> Ordering
forall {k} (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare