{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeInType #-} {-# OPTIONS_HADDOCK not-home #-} -- | This module is intended for internal use only, and may change without -- warning in subsequent releases. module Optics.Internal.Optic.TypeLevel where import Data.Kind (Type) import GHC.TypeLits -- | A list of index types, used for indexed optics. -- -- @since 0.2 type IxList = [Type] -- | An alias for an empty index-list type NoIx = ('[] :: IxList) -- | Singleton index list type WithIx i = ('[i] :: IxList) -- | Show a type surrounded by quote marks. type family QuoteType (x :: Type) :: ErrorMessage where QuoteType x = 'Text "‘" ':<>: 'ShowType x ':<>: 'Text "’" -- | Show a symbol surrounded by quote marks. type family QuoteSymbol (x :: Symbol) :: ErrorMessage where QuoteSymbol x = 'Text "‘" ':<>: 'Text x ':<>: 'Text "’" ---------------------------------------- -- Elimination forms in error messages type family ShowSymbolWithOrigin symbol origin :: ErrorMessage where ShowSymbolWithOrigin symbol origin = 'Text " " ':<>: QuoteSymbol symbol ':<>: 'Text " (from " ':<>: 'Text origin ':<>: 'Text ")" type family ShowSymbolsWithOrigin (fs :: [(Symbol, Symbol)]) :: ErrorMessage where ShowSymbolsWithOrigin '[ '(symbol, origin) ] = ShowSymbolWithOrigin symbol origin ShowSymbolsWithOrigin ('(symbol, origin) ': rest) = ShowSymbolWithOrigin symbol origin ':$$: ShowSymbolsWithOrigin rest type family ShowOperators (ops :: [Symbol]) :: ErrorMessage where ShowOperators '[op] = QuoteSymbol op ':<>: 'Text " (from Optics.Operators)" ShowOperators (op ': rest) = QuoteSymbol op ':<>: 'Text " " ':<>: ShowOperators rest type family AppendEliminations a b where AppendEliminations '(fs1, ops1) '(fs2, ops2) = '(Append fs1 fs2, Append ops1 ops2) type family ShowEliminations forms :: ErrorMessage where ShowEliminations '(fs, ops) = ShowSymbolsWithOrigin fs ':$$: 'Text " " ':<>: ShowOperators ops ---------------------------------------- data RepDefined = RepDefined -- | This type family should be called with applications of 'Rep' on both sides, -- and will reduce to 'RepDefined' if at least one of them is defined; otherwise -- it is stuck. type family AnyHasRep (s :: Type -> Type) (t :: Type -> Type) :: RepDefined type instance AnyHasRep (s x) t = 'RepDefined type instance AnyHasRep s (t x) = 'RepDefined -- | Curry a type-level list. -- -- In pseudo (dependent-)Haskell: -- -- @ -- 'Curry' xs y = 'foldr' (->) y xs -- @ type family Curry (xs :: IxList) (y :: Type) :: Type where Curry '[] y = y Curry (x ': xs) y = x -> Curry xs y -- | Append two type-level lists together. type family Append (xs :: [k]) (ys :: [k]) :: [k] where Append '[] ys = ys -- needed for (<%>) and (%>) Append xs '[] = xs -- needed for (<%) Append (x ': xs) ys = x ': Append xs ys -- | Class that is inhabited by all type-level lists @xs@, providing the ability -- to compose a function under @'Curry' xs@. class CurryCompose xs where -- | Compose a function under @'Curry' xs@. This generalises @('.')@ (aka -- 'fmap' for @(->)@) to work for curried functions with one argument for each -- type in the list. composeN :: (i -> j) -> Curry xs i -> Curry xs j instance CurryCompose '[] where composeN = id {-# INLINE composeN #-} instance CurryCompose xs => CurryCompose (x ': xs) where composeN ij f = composeN @xs ij . f {-# INLINE composeN #-}