{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Data.Functor.Product.Singletons (
Sing, SProduct(..),
PairSym0, PairSym1, PairSym2
) where
import Control.Applicative
import Control.Applicative.Singletons
import Control.Monad
import Control.Monad.Singletons
import Control.Monad.Zip
import Control.Monad.Zip.Singletons
import Data.Foldable.Singletons hiding (Product)
import Data.Function.Singletons
import Data.Functor.Product
import Data.Kind
import Data.Monoid.Singletons hiding (SProduct(..))
import Data.Singletons
import Data.Singletons.TH
import Data.Traversable.Singletons
type SProduct :: Product f g a -> Type
data SProduct :: Product f g a -> Type where
SPair :: forall f g a (x :: f a) (y :: g a).
Sing x -> Sing y -> SProduct ('Pair @f @g @a x y)
type instance Sing = SProduct
instance (SingI x, SingI y) => SingI ('Pair x y) where
sing :: Sing ('Pair x y)
sing = Sing x -> Sing y -> SProduct ('Pair x y)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
(arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair Sing x
forall {k} (a :: k). SingI a => Sing a
sing Sing y
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI x => SingI1 ('Pair x) where
liftSing :: forall (x :: g a). Sing x -> Sing ('Pair x x)
liftSing = Sing x -> Sing x -> SProduct ('Pair x x)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
(arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair Sing x
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI2 'Pair where
liftSing2 :: forall (x :: f a) (y :: g a). Sing x -> Sing y -> Sing ('Pair x y)
liftSing2 = Sing x -> Sing y -> Sing ('Pair x y)
Sing x -> Sing y -> SProduct ('Pair x y)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
(arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair
type PairSym0 :: forall f g a. f a ~> g a ~> Product f g a
data PairSym0 z
type instance Apply PairSym0 x = PairSym1 x
instance SingI PairSym0 where
sing :: Sing PairSym0
sing = SingFunction2 PairSym0 -> Sing PairSym0
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 Sing t1 -> Sing t2 -> Sing (Apply (Apply PairSym0 t1) t2)
Sing t1 -> Sing t2 -> SProduct ('Pair t1 t2)
SingFunction2 PairSym0
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
(arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair
type PairSym1 :: forall f g a. f a -> g a ~> Product f g a
data PairSym1 fa z
type instance Apply (PairSym1 x) y = 'Pair x y
instance SingI x => SingI (PairSym1 x) where
sing :: Sing (PairSym1 x)
sing = SingFunction1 (PairSym1 x) -> Sing (PairSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (PairSym1 x) -> Sing (PairSym1 x))
-> SingFunction1 (PairSym1 x) -> Sing (PairSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> SProduct ('Pair x t)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
(arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair (forall (a :: f a). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x)
instance SingI1 PairSym1 where
liftSing :: forall (x :: f a). Sing x -> Sing (PairSym1 x)
liftSing Sing x
s = SingFunction1 (PairSym1 x) -> Sing (PairSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (PairSym1 x) -> Sing (PairSym1 x))
-> SingFunction1 (PairSym1 x) -> Sing (PairSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> SProduct ('Pair x t)
forall {k} (f :: k -> *) (g :: k -> *) (a :: k) (arg :: f a)
(arg :: g a).
Sing arg -> Sing arg -> SProduct ('Pair arg arg)
SPair Sing x
s
type PairSym2 :: forall f g a. f a -> g a -> Product f g a
type family PairSym2 x y where
PairSym2 x y = 'Pair x y
$