{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoNamedWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# 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.Monoid.Singletons
import Data.Ord.Singletons
import Data.Semigroup.Singletons.Internal.Classes
import Data.Singletons.Base.Instances hiding (FoldlSym0, sFoldl)
import Data.Singletons.Base.Enum
import Data.Singletons.TH
import Data.Singletons.TH.Options
import GHC.Base.Singletons
hiding ( Const, ConstSym0, ConstSym1
, Foldr, FoldrSym0, sFoldr )
import GHC.Num.Singletons
import Text.Show.Singletons
$(withOptions defaultOptions{genSingKindInsts = False}
(genSingletons [''Const]))
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 n
sa) = Demote a -> Const (Demote a) b
forall {k} a (b :: k). a -> Const a b
Const (Sing n -> Demote a
forall (a :: a). Sing a -> Demote a
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
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) (k :: a). Sing k -> SConst ('Const k)
SConst
$