{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
module Servant.OpenApi.Internal.TypeLevel.TMap where

import           Data.Proxy
import           GHC.Exts   (Constraint)

-- $setup
-- >>> :set -XDataKinds
-- >>> :set -XFlexibleContexts
-- >>> :set -XGADTs
-- >>> :set -XRankNTypes
-- >>> :set -XScopedTypeVariables
-- >>> import GHC.TypeLits
-- >>> import Data.List

-- | Map a list of constrained types to a list of values.
--
-- >>> tmap (Proxy :: Proxy KnownSymbol) symbolVal (Proxy :: Proxy ["hello", "world"])
-- ["hello","world"]
class TMap (q :: k -> Constraint) (xs :: [k]) where
  tmap :: p q -> (forall x p'. q x => p' x -> a) -> p'' xs -> [a]

instance TMap q '[] where
  tmap :: forall (p :: (k -> Constraint) -> *) a (p'' :: [k] -> *).
p q
-> (forall (x :: k) (p' :: k -> *). q x => p' x -> a)
-> p'' '[]
-> [a]
tmap p q
_ forall (x :: k) (p' :: k -> *). q x => p' x -> a
_ p'' '[]
_ = []

instance (q x, TMap q xs) => TMap q (x ': xs) where
  tmap :: forall (p :: (a -> Constraint) -> *) a (p'' :: [a] -> *).
p q
-> (forall (x :: a) (p' :: a -> *). q x => p' x -> a)
-> p'' (x : xs)
-> [a]
tmap p q
q forall (x :: a) (p' :: a -> *). q x => p' x -> a
f p'' (x : xs)
_ = forall (x :: a) (p' :: a -> *). q x => p' x -> a
f (forall {k} (t :: k). Proxy t
Proxy :: Proxy x) forall a. a -> [a] -> [a]
: forall k (q :: k -> Constraint) (xs :: [k])
       (p :: (k -> Constraint) -> *) a (p'' :: [k] -> *).
TMap q xs =>
p q
-> (forall (x :: k) (p' :: k -> *). q x => p' x -> a)
-> p'' xs
-> [a]
tmap p q
q forall (x :: a) (p' :: a -> *). q x => p' x -> a
f (forall {k} (t :: k). Proxy t
Proxy :: Proxy xs)