{-# LANGUAGE PolyKinds #-}
module Servant.Util.Common.PolyKinds
( TyNamedParam (..)
, type (?:)
, TyNamedParamType
, TyNamedParamsNames
, ReifyParamsNames (..)
, reifyParamsNames
, LookupParam
, reifyParamsNamesSet
, ParamsContainNoName
, Elem
, If
, type (==)
, type (&&)
, type (||)
, type (++)
, type (//)
, InsSorted
, UnionSorted
, Demote (..)
, Demoted
, tyBoolCase
) where
import Universum
import Data.Constraint (Dict (..))
import qualified Data.Set as S
import GHC.TypeLits (AppendSymbol, CmpSymbol, ErrorMessage (..), KnownSymbol, Symbol, TypeError,
symbolVal)
import Servant (If)
import Unsafe.Coerce (unsafeCoerce)
data TyNamedParam a = TyNamedParam Symbol a
type (?:) = 'TyNamedParam
type family TyNamedParamType p where
TyNamedParamType ('TyNamedParam _ a) = a
type family TyNamedParamsNames (params :: [TyNamedParam k]) :: [Symbol] where
TyNamedParamsNames '[] = '[]
TyNamedParamsNames ('TyNamedParam name _ ': params) = name ': TyNamedParamsNames params
class ReifyParamsNames (params :: [TyNamedParam k]) where
reifyParamsNames' :: [Text]
instance ReifyParamsNames '[] where
reifyParamsNames' :: [Text]
reifyParamsNames' = [Text]
forall a. Monoid a => a
mempty
instance (KnownSymbol name, ReifyParamsNames params, ParamsContainNoName params name) =>
ReifyParamsNames ('TyNamedParam name (p :: k) ': params) where
reifyParamsNames' :: [Text]
reifyParamsNames' =
String -> Text
forall a. ToText a => a -> Text
toText (Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal @name Proxy name
forall k (t :: k). Proxy t
Proxy) Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: ReifyParamsNames params => [Text]
forall k (params :: [TyNamedParam k]).
ReifyParamsNames params =>
[Text]
reifyParamsNames' @k @params
reifyParamsNames :: forall params. ReifyParamsNames params => [Text]
reifyParamsNames :: [Text]
reifyParamsNames = ReifyParamsNames params => [Text]
forall k (params :: [TyNamedParam k]).
ReifyParamsNames params =>
[Text]
reifyParamsNames' @_ @params
reifyParamsNamesSet :: forall params. ReifyParamsNames params => Set Text
reifyParamsNamesSet :: Set Text
reifyParamsNamesSet = [Text] -> Set Text
forall a. Ord a => [a] -> Set a
S.fromList ([Text] -> Set Text) -> [Text] -> Set Text
forall a b. (a -> b) -> a -> b
$ ReifyParamsNames params => [Text]
forall k (params :: [TyNamedParam k]).
ReifyParamsNames params =>
[Text]
reifyParamsNames @params
type family LookupParam (desc :: Symbol) (name :: Symbol)
(params :: [TyNamedParam k]) :: k where
LookupParam desc name '[] =
TypeError ('Text ("No " `AppendSymbol` desc `AppendSymbol` " with name ")
':<>: 'ShowType name ':<>: 'Text " found")
LookupParam desc name ('TyNamedParam name a ': params) = a
LookupParam desc name ('TyNamedParam name0 a ': params) =
LookupParam desc name params
type family ParamsContainNoName (params :: [TyNamedParam k]) name :: Constraint where
ParamsContainNoName '[] name = ()
ParamsContainNoName ('TyNamedParam name p ': params) name =
TypeError ('Text "Duplicate name in parameters: " ':<>: 'ShowType name)
ParamsContainNoName ('TyNamedParam name p ': params) name' =
ParamsContainNoName params name'
type family Elem (a :: k) (l :: [k]) :: Bool where
Elem a '[] = 'False
Elem a (a ': l) = 'True
Elem a (_ ': l) = Elem a l
type family (==) (a :: k) (b :: k) :: Bool where
a == a = 'True
_ == _ = 'False
infix 4 ==
type family (&&) (a :: Bool) (b :: Bool) :: Bool where
'False && _ = 'False
_ && 'False = 'False
'True && 'True = 'True
infix 3 &&
type family (||) (a :: Bool) (b :: Bool) :: Bool where
'True || _ = 'True
_ || 'True = 'True
'False || 'False = 'False
infix 2 ||
type family (++) (as :: [k]) (bs :: [k]) :: [k] where
'[] ++ bs = bs
(a ': as) ++ bs = a ': (as ++ bs)
type family (//) (as :: [k]) (bs :: [k]) :: [k] where
'[] // bs = '[]
(a ': as) // bs = If (a `Elem` bs) (as // bs) (a ': (as // bs))
type family InsSorted (s :: Symbol) (ss :: [Symbol]) :: [Symbol] where
InsSorted s '[] = '[s]
InsSorted s0 (s ': ss) =
If (CmpSymbol s0 s == 'GT) (s ': InsSorted s0 ss)
( If (s0 == s) (s ': ss) (s0 ': s ': ss)
)
type family UnionSorted (ss1 :: [Symbol]) (ss2 :: [Symbol]) :: [Symbol] where
UnionSorted ss1 '[] = ss1
UnionSorted '[] ss2 = ss2
UnionSorted (s1 ': ss1) (s2 ': ss2) =
If (s1 == s2) (s1 ': UnionSorted ss1 ss2)
( If (CmpSymbol s1 s2 == 'LT)
(s1 ': UnionSorted ss1 (s2 ': ss2))
(s2 ': UnionSorted (s1 ': ss1) ss2)
)
class Demote (ty :: k) where
demote :: Proxy ty -> Demoted k
type family Demoted k :: Type
type instance Demoted Bool = Bool
instance Demote 'True where
demote :: Proxy 'True -> Demoted Bool
demote Proxy 'True
_ = Bool
Demoted Bool
True
instance Demote 'False where
demote :: Proxy 'False -> Demoted Bool
demote Proxy 'False
_ = Bool
Demoted Bool
False
tyBoolCase
:: Demote b
=> Proxy (b :: Bool)
-> Either (Dict (b ~ 'False)) (Dict (b ~ 'True))
tyBoolCase :: Proxy b -> Either (Dict (b ~ 'False)) (Dict (b ~ 'True))
tyBoolCase Proxy b
p = case Proxy b -> Demoted Bool
forall k (ty :: k). Demote ty => Proxy ty -> Demoted k
demote Proxy b
p of
Demoted Bool
False -> Dict (b ~ 'False) -> Either (Dict (b ~ 'False)) (Dict (b ~ 'True))
forall a b. a -> Either a b
Left (Dict (b ~ 'False)
-> Either (Dict (b ~ 'False)) (Dict (b ~ 'True)))
-> Dict (b ~ 'False)
-> Either (Dict (b ~ 'False)) (Dict (b ~ 'True))
forall a b. (a -> b) -> a -> b
$ Dict (() ~ ()) -> Dict (b ~ 'False)
forall a b. a -> b
unsafeCoerce (Dict (() ~ ()) -> Dict (b ~ 'False))
-> Dict (() ~ ()) -> Dict (b ~ 'False)
forall a b. (a -> b) -> a -> b
$ (() ~ ()) => Dict (() ~ ())
forall (a :: Constraint). a => Dict a
Dict @(() ~ ())
Demoted Bool
True -> Dict (b ~ 'True) -> Either (Dict (b ~ 'False)) (Dict (b ~ 'True))
forall a b. b -> Either a b
Right (Dict (b ~ 'True) -> Either (Dict (b ~ 'False)) (Dict (b ~ 'True)))
-> Dict (b ~ 'True)
-> Either (Dict (b ~ 'False)) (Dict (b ~ 'True))
forall a b. (a -> b) -> a -> b
$ Dict (() ~ ()) -> Dict (b ~ 'True)
forall a b. a -> b
unsafeCoerce (Dict (() ~ ()) -> Dict (b ~ 'True))
-> Dict (() ~ ()) -> Dict (b ~ 'True)
forall a b. (a -> b) -> a -> b
$ (() ~ ()) => Dict (() ~ ())
forall (a :: Constraint). a => Dict a
Dict @(() ~ ())
type instance Demoted (Maybe k) = Maybe (Demoted k)
instance Demote 'Nothing where
demote :: Proxy 'Nothing -> Demoted (Maybe a)
demote Proxy 'Nothing
_ = Demoted (Maybe a)
forall a. Maybe a
Nothing
instance Demote a => Demote ('Just (a :: k)) where
demote :: Proxy ('Just a) -> Demoted (Maybe k)
demote Proxy ('Just a)
_ = Demoted k -> Maybe (Demoted k)
forall a. a -> Maybe a
Just (Demoted k -> Maybe (Demoted k)) -> Demoted k -> Maybe (Demoted k)
forall a b. (a -> b) -> a -> b
$ Proxy a -> Demoted k
forall k (ty :: k). Demote ty => Proxy ty -> Demoted k
demote (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
type instance Demoted Nat = Natural
instance KnownNat a => Demote a where
demote :: Proxy a -> Demoted Nat
demote = Proxy a -> Demoted Nat
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal