{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_HADDOCK not-home #-}
module Optics.Internal.Optic.TypeLevel where
import Data.Kind
import GHC.TypeLits
type IxList = [Type]
type NoIx = ('[] :: IxList)
type WithIx i = ('[i] :: IxList)
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
type family Reverse (xs :: [k]) (acc :: [k]) :: [k] where
Reverse '[] acc = acc
Reverse (x : xs) acc = Reverse xs (x : acc)
type family Curry (xs :: IxList) (y :: Type) :: Type where
Curry '[] y = y
Curry (x ': xs) y = x -> Curry xs y
type family Append (xs :: [k]) (ys :: [k]) :: [k] where
Append '[] ys = ys
Append xs '[] = xs
Append (x ': xs) ys = x ': Append xs ys
class CurryCompose xs where
composeN :: (i -> j) -> Curry xs i -> Curry xs j
instance CurryCompose '[] where
composeN :: forall i j. (i -> j) -> Curry '[] i -> Curry '[] j
composeN = forall a. a -> a
id
instance CurryCompose xs => CurryCompose (x ': xs) where
composeN :: forall i j. (i -> j) -> Curry (x : xs) i -> Curry (x : xs) j
composeN i -> j
ij Curry (x : xs) i
f = forall (xs :: IxList) i j.
CurryCompose xs =>
(i -> j) -> Curry xs i -> Curry xs j
composeN @xs i -> j
ij forall b c a. (b -> c) -> (a -> b) -> a -> c
. Curry (x : xs) i
f
data IxEq i is js where
IxEq :: IxEq i is is
class AppendIndices xs ys ks | xs ys -> ks where
appendIndices :: IxEq i (Curry xs (Curry ys i)) (Curry ks i)
instance {-# INCOHERENT #-} xs ~ zs => AppendIndices xs '[] zs where
appendIndices :: forall i. IxEq i (Curry xs (Curry '[] i)) (Curry zs i)
appendIndices = forall {k} {k} (i :: k) (is :: k). IxEq i is is
IxEq
instance ys ~ zs => AppendIndices '[] ys zs where
appendIndices :: forall i. IxEq i (Curry '[] (Curry ys i)) (Curry zs i)
appendIndices = 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 :: forall i. IxEq i (Curry (x : xs) (Curry ys i)) (Curry (x : ks) i)
appendIndices | IxEq i (Curry xs (Curry ys i)) (Curry ks i)
IxEq <- 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 = forall {k} {k} (i :: k) (is :: k). IxEq i is is
IxEq
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
type family When (p :: Bool) (err :: Constraint) :: Constraint where
When 'True err = err
When 'False _ = ()
type family Unless (p :: Bool) (err :: Constraint) :: Constraint where
Unless 'True _ = ()
Unless 'False err = err
type family Defined (f :: k) :: Bool where
Defined (f _) = Defined f
Defined _ = 'True
type family QuoteType (x :: t) :: ErrorMessage where
QuoteType x = 'Text "‘" ':<>: 'ShowType x ':<>: 'Text "’"
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"
class HasShapeOf (a :: k) (b :: k)
instance {-# OVERLAPPING #-} (fa ~ f a, HasShapeOf f g) => HasShapeOf fa (g b)
instance (a ~ b) => HasShapeOf a b