{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoNamedWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Data.Functor.Const.Singletons (
Sing, SConst(..), GetConst, sGetConst,
ConstSym0, ConstSym1,
GetConstSym0, GetConstSym1
) where
import Control.Applicative
import Control.Monad.Singletons.Internal
import Data.Eq.Singletons
import Data.Foldable.Singletons
import Data.Kind (Type)
import Data.Monoid.Singletons
import Data.Ord.Singletons
import Data.Semigroup.Singletons.Internal.Classes
import Data.Singletons
import Data.Singletons.Base.Instances hiding (FoldlSym0, sFoldl)
import Data.Singletons.Base.Enum
import Data.Singletons.TH
import GHC.Base.Singletons
hiding ( Const, ConstSym0, ConstSym1
, Foldr, FoldrSym0, sFoldr )
import GHC.Num.Singletons
import Text.Show.Singletons
type SConst :: Const a b -> Type
data SConst :: Const a b -> Type where
SConst :: forall {k} a (b :: k) (x :: a).
Sing x -> SConst ('Const @a @b x)
type instance Sing = SConst
instance SingKind a => SingKind (Const a b) where
type Demote (Const a b) = Const (Demote a) b
fromSing :: forall (a :: Const a b). Sing a -> Demote (Const a b)
fromSing (SConst Sing x
sa) = Demote a -> Const (Demote a) b
forall {k} a (b :: k). a -> Const a b
Const (Sing x -> Demote a
forall (a :: a). Sing a -> Demote a
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sa)
toSing :: Demote (Const a b) -> SomeSing (Const a b)
toSing (Const Demote a
a) = Demote a
-> (forall {a :: a}. Sing a -> SomeSing (Const a b))
-> SomeSing (Const a b)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote a
a ((forall {a :: a}. Sing a -> SomeSing (Const a b))
-> SomeSing (Const a b))
-> (forall {a :: a}. Sing a -> SomeSing (Const a b))
-> SomeSing (Const a b)
forall a b. (a -> b) -> a -> b
$ Sing ('Const a) -> SomeSing (Const a b)
SConst ('Const a) -> SomeSing (Const a b)
forall k (a :: k). Sing a -> SomeSing k
SomeSing (SConst ('Const a) -> SomeSing (Const a b))
-> (Sing a -> SConst ('Const a)) -> Sing a -> SomeSing (Const a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> SConst ('Const a)
forall {k} a (b :: k) (arg :: a). Sing arg -> SConst ('Const arg)
SConst
instance SingI a => SingI ('Const a) where
sing :: Sing ('Const a)
sing = Sing a -> SConst ('Const a)
forall {k} a (b :: k) (arg :: a). Sing arg -> SConst ('Const arg)
SConst Sing a
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI1 'Const where
liftSing :: forall (x :: k1). Sing x -> Sing ('Const x)
liftSing = Sing x -> Sing ('Const x)
Sing x -> SConst ('Const x)
forall {k} a (b :: k) (arg :: a). Sing arg -> SConst ('Const arg)
SConst
type ConstSym0 :: a ~> Const a b
data ConstSym0 z
type instance Apply ConstSym0 x = 'Const x
instance SingI ConstSym0 where
sing :: Sing ConstSym0
sing = SingFunction1 ConstSym0 -> Sing ConstSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 Sing t -> Sing (Apply ConstSym0 t)
Sing t -> SConst ('Const t)
SingFunction1 ConstSym0
forall {k} a (b :: k) (arg :: a). Sing arg -> SConst ('Const arg)
SConst
type ConstSym1 :: a -> Const a b
type family ConstSym1 x where
ConstSym1 x = 'Const x
$