module Generics.Kind.Unexported where import Generics.Kind hiding (SubstRep, SubstRep') class SubstRep' (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k) where type family SubstRep f x :: LoT k -> * substRep :: f (x ':&&: xs) -> SubstRep f x xs unsubstRep :: SubstRep f x xs -> f (x ':&&: xs) instance SubstRep' U1 x xs where type SubstRep U1 x = U1 substRep :: U1 (x ':&&: xs) -> SubstRep U1 x xs substRep U1 (x ':&&: xs) U1 = U1 xs SubstRep U1 x xs forall k (p :: k). U1 p U1 unsubstRep :: SubstRep U1 x xs -> U1 (x ':&&: xs) unsubstRep U1 xs SubstRep U1 x xs U1 = U1 (x ':&&: xs) forall k (p :: k). U1 p U1 instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :+: g) x xs where type SubstRep (f :+: g) x = (SubstRep f x) :+: (SubstRep g x) substRep :: (:+:) f g (x ':&&: xs) -> SubstRep (f :+: g) x xs substRep (L1 f (x ':&&: xs) x) = SubstRep f x xs -> (:+:) (SubstRep f x) (SubstRep g x) xs forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p L1 (f (x ':&&: xs) -> SubstRep f x xs forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => f (x ':&&: xs) -> SubstRep f x xs substRep f (x ':&&: xs) x) substRep (R1 g (x ':&&: xs) x) = SubstRep g x xs -> (:+:) (SubstRep f x) (SubstRep g x) xs forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p R1 (g (x ':&&: xs) -> SubstRep g x xs forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => f (x ':&&: xs) -> SubstRep f x xs substRep g (x ':&&: xs) x) unsubstRep :: SubstRep (f :+: g) x xs -> (:+:) f g (x ':&&: xs) unsubstRep (L1 SubstRep f x xs x) = f (x ':&&: xs) -> (:+:) f g (x ':&&: xs) forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p L1 (SubstRep f x xs -> f (x ':&&: xs) forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => SubstRep f x xs -> f (x ':&&: xs) unsubstRep SubstRep f x xs x) unsubstRep (R1 SubstRep g x xs x) = g (x ':&&: xs) -> (:+:) f g (x ':&&: xs) forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p R1 (SubstRep g x xs -> g (x ':&&: xs) forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => SubstRep f x xs -> f (x ':&&: xs) unsubstRep SubstRep g x xs x) instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :*: g) x xs where type SubstRep (f :*: g) x = (SubstRep f x) :*: (SubstRep g x) substRep :: (:*:) f g (x ':&&: xs) -> SubstRep (f :*: g) x xs substRep (f (x ':&&: xs) x :*: g (x ':&&: xs) y) = f (x ':&&: xs) -> SubstRep f x xs forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => f (x ':&&: xs) -> SubstRep f x xs substRep f (x ':&&: xs) x SubstRep f x xs -> SubstRep g x xs -> (:*:) (SubstRep f x) (SubstRep g x) xs forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> g p -> (:*:) f g p :*: g (x ':&&: xs) -> SubstRep g x xs forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => f (x ':&&: xs) -> SubstRep f x xs substRep g (x ':&&: xs) y unsubstRep :: SubstRep (f :*: g) x xs -> (:*:) f g (x ':&&: xs) unsubstRep (SubstRep f x xs x :*: SubstRep g x xs y) = SubstRep f x xs -> f (x ':&&: xs) forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => SubstRep f x xs -> f (x ':&&: xs) unsubstRep SubstRep f x xs x f (x ':&&: xs) -> g (x ':&&: xs) -> (:*:) f g (x ':&&: xs) forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> g p -> (:*:) f g p :*: SubstRep g x xs -> g (x ':&&: xs) forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => SubstRep f x xs -> f (x ':&&: xs) unsubstRep SubstRep g x xs y instance SubstRep' f x xs => SubstRep' (M1 i c f) x xs where type SubstRep (M1 i c f) x = M1 i c (SubstRep f x) substRep :: M1 i c f (x ':&&: xs) -> SubstRep (M1 i c f) x xs substRep (M1 f (x ':&&: xs) x) = SubstRep f x xs -> M1 i c (SubstRep f x) xs forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 (f (x ':&&: xs) -> SubstRep f x xs forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => f (x ':&&: xs) -> SubstRep f x xs substRep f (x ':&&: xs) x) unsubstRep :: SubstRep (M1 i c f) x xs -> M1 i c f (x ':&&: xs) unsubstRep (M1 SubstRep f x xs x) = f (x ':&&: xs) -> M1 i c f (x ':&&: xs) forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 (SubstRep f x xs -> f (x ':&&: xs) forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => SubstRep f x xs -> f (x ':&&: xs) unsubstRep SubstRep f x xs x) instance (Interpret (SubstAtom c x) xs, Interpret c (x ':&&: xs), SubstRep' f x xs) => SubstRep' (c :=>: f) x xs where type SubstRep (c :=>: f) x = (SubstAtom c x) :=>: (SubstRep f x) substRep :: (:=>:) c f (x ':&&: xs) -> SubstRep (c :=>: f) x xs substRep (SuchThat f (x ':&&: xs) x) = SubstRep f x xs -> (:=>:) (SubstAtom c x) (SubstRep f x) xs forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *). Interpret c x => f x -> (:=>:) c f x SuchThat (f (x ':&&: xs) -> SubstRep f x xs forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => f (x ':&&: xs) -> SubstRep f x xs substRep f (x ':&&: xs) x) unsubstRep :: SubstRep (c :=>: f) x xs -> (:=>:) c f (x ':&&: xs) unsubstRep (SuchThat SubstRep f x xs x) = f (x ':&&: xs) -> (:=>:) c f (x ':&&: xs) forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *). Interpret c x => f x -> (:=>:) c f x SuchThat (SubstRep f x xs -> f (x ':&&: xs) forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k). SubstRep' f x xs => SubstRep f x xs -> f (x ':&&: xs) unsubstRep SubstRep f x xs x) instance (Interpret (SubstAtom t x) xs ~ Interpret t (x ':&&: xs)) => SubstRep' (Field t) x xs where type SubstRep (Field t) x = Field (SubstAtom t x) substRep :: Field t (x ':&&: xs) -> SubstRep (Field t) x xs substRep (Field Interpret t (x ':&&: xs) x) = Interpret (SubstAtom t x) xs -> Field (SubstAtom t x) xs forall {d} (t :: Atom d (*)) (x :: LoT d). Interpret t x -> Field t x Field Interpret (SubstAtom t x) xs Interpret t (x ':&&: xs) x unsubstRep :: SubstRep (Field t) x xs -> Field t (x ':&&: xs) unsubstRep (Field Interpret (SubstAtom t x) xs x) = Interpret t (x ':&&: xs) -> Field t (x ':&&: xs) forall {d} (t :: Atom d (*)) (x :: LoT d). Interpret t x -> Field t x Field Interpret (SubstAtom t x) xs Interpret t (x ':&&: xs) x