module Generics.Kind.Unexported where import Generics.Kind hiding (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 = SubstRep U1 x xs forall k (p :: k). U1 p U1 unsubstRep :: SubstRep U1 x xs -> U1 (x ':&&: xs) unsubstRep 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 x :: 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 x :: 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 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 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 (x :: f (x ':&&: xs) x :*: y :: 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 (x :*: 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 x :: 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 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 x :: 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 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 x :: 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 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 type family SubstAtom (f :: Atom (t -> k) d) (x :: t) :: Atom k d where SubstAtom ('Var 'VZ) x = 'Kon x SubstAtom ('Var ('VS v)) x = 'Var v SubstAtom ('Kon t) x = 'Kon t SubstAtom (t1 ':@: t2) x = (SubstAtom t1 x) ':@: (SubstAtom t2 x) SubstAtom (t1 ':&: t2) x = (SubstAtom t1 x) ':&: (SubstAtom t2 x)