{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-} {-# 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 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) ---------------------------------------- -- 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 ---------------------------------------- -- Lists -- | Reverse a type-level list. type family Reverse (xs :: [k]) (acc :: [k]) :: [k] where Reverse '[] acc = acc Reverse (x : xs) acc = Reverse xs (x : acc) -- | 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 :: (i -> j) -> Curry '[] i -> Curry '[] j composeN = (i -> j) -> Curry '[] i -> Curry '[] j forall a. a -> a id instance CurryCompose xs => CurryCompose (x ': xs) where composeN :: (i -> j) -> Curry (x : xs) i -> Curry (x : xs) j composeN i -> j ij Curry (x : xs) i f = (i -> j) -> Curry xs i -> Curry xs j forall (xs :: IxList) i j. CurryCompose xs => (i -> j) -> Curry xs i -> Curry xs j composeN @xs i -> j ij (Curry xs i -> Curry xs j) -> (x -> Curry xs i) -> x -> Curry xs j forall b c a. (b -> c) -> (a -> b) -> a -> c . Curry (x : xs) i x -> Curry xs i f ---------------------------------------- -- Indices -- | Tagged version of 'Data.Type.Equality.(:~:)' for carrying evidence that two -- index lists in a curried form are equal. data IxEq i is js where IxEq :: IxEq i is is -- | In pseudo (dependent-)Haskell, provide a witness -- -- @ -- foldr f (foldr f init xs) ys = foldr f init (ys ++ xs) -- where f = (->) -- @ -- -- @since 0.4 -- class AppendIndices xs ys ks | xs ys -> ks where appendIndices :: IxEq i (Curry xs (Curry ys i)) (Curry ks i) -- | If the second list is empty, we can shortcircuit and pick the first list -- immediately. instance {-# INCOHERENT #-} AppendIndices xs '[] xs where appendIndices :: IxEq i (Curry xs (Curry '[] i)) (Curry xs i) appendIndices = IxEq i (Curry xs (Curry '[] i)) (Curry xs i) forall k k (i :: k) (is :: k). IxEq i is is IxEq instance AppendIndices '[] ys ys where appendIndices :: IxEq i (Curry '[] (Curry ys i)) (Curry ys i) appendIndices = IxEq i (Curry '[] (Curry ys i)) (Curry ys i) forall k k (i :: k) (is :: k). IxEq i is is IxEq instance AppendIndices xs ys ks => AppendIndices (x ': xs) ys (x ': ks) where appendIndices :: forall i. IxEq i (Curry (x ': xs) (Curry ys i)) (Curry (x ': ks) i) appendIndices :: IxEq i (Curry (x : xs) (Curry ys i)) (Curry (x : ks) i) appendIndices | IxEq i (Curry xs (Curry ys i)) (Curry ks i) IxEq <- IxEq i (Curry xs (Curry ys i)) (Curry ks i) forall (xs :: IxList) (ys :: IxList) (ks :: IxList) i. AppendIndices xs ys ks => IxEq i (Curry xs (Curry ys i)) (Curry ks i) appendIndices @xs @ys @ks @i = IxEq i (Curry (x : xs) (Curry ys i)) (Curry (x : ks) i) forall k k (i :: k) (is :: k). IxEq i is is IxEq ---------------------------------------- -- Either -- | If lhs is 'Right', return it. Otherwise check rhs. type family FirstRight (m1 :: Either e a) (m2 :: Either e a) :: Either e a where FirstRight ('Right a) _ = 'Right a FirstRight _ b = b type family FromRight (def :: b) (e :: Either a b) :: b where FromRight _ ('Right b) = b FromRight def ('Left _) = def type family IsLeft (e :: Either a b) :: Bool where IsLeft ('Left _) = 'True IsLeft ('Right _) = 'False ---------------------------------------- -- Errors -- | Show a custom type error if @p@ is true. type family When (p :: Bool) (err :: Constraint) :: Constraint where When 'True err = err When 'False _ = () -- | Show a custom type error if @p@ is false (or stuck). type family Unless (p :: Bool) (err :: Constraint) :: Constraint where Unless 'True _ = () Unless 'False err = err -- | Use with 'Unless' to detect stuck (undefined) type families. type family Defined (f :: k) :: Bool where Defined (f _) = Defined f Defined _ = 'True -- | Show a type surrounded by quote marks. type family QuoteType (x :: t) :: 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 "’" type family ToOrdinal (n :: Nat) :: ErrorMessage where ToOrdinal 1 = 'Text "1st" ToOrdinal 2 = 'Text "2nd" ToOrdinal 3 = 'Text "3rd" ToOrdinal n = 'ShowType n ':<>: 'Text "th" ---------------------------------------- -- Misc -- | Derive the shape of @a@ from the shape of @b@. class HasShapeOf (a :: k) (b :: k) instance {-# OVERLAPPING #-} (fa ~ f a, HasShapeOf f g) => HasShapeOf fa (g b) instance (a ~ b) => HasShapeOf a b