kind-generics 0.4.1.1 → 0.4.1.2

raw patch · 3 files changed

+47/−32 lines, 3 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• kind-generics.cabal +1/−1
• src/Generics/Kind.hs +28/−14
• src/Generics/Kind/Examples.hs +18/−17

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                kind-generics-version:             0.4.1.1+version:             0.4.1.2 synopsis:            Generic programming in GHC style for arbitrary kinds and GADTs. description:         This package provides functionality to extend the data type generic programming functionality in GHC to classes of arbitrary kind, and constructors featuring constraints and existentials, as usually found in GADTs. -- bug-reports:

@@ -15,6 +15,7 @@ {-# language TypeFamilies              #-} {-# language TypeOperators             #-} {-# language UndecidableInstances      #-}+{-# language UndecidableSuperClasses   #-} -- | Main module of @kind-generics@. Please refer to the @README@ file for documentation on how to use this package. module Generics.Kind (   module Data.PolyKinded@@ -45,11 +46,11 @@ -- -- > instance GenericK [] (a :&&: LoT0) where -- >   type RepK [] = Field Var0 :*: Field ([] :$: Var0)-newtype Field (t :: Atom d (*)) (x :: LoT d) where-  -- Field :: forall (r :: RuntimeRep) (k :: TYPE r) (d :: *). Atom d k -> LoT d -> * where+newtype Field (t :: Atom d Type) (x :: LoT d) where+  -- Field :: forall (r :: RuntimeRep) (k :: TYPE r) (d :: Type). Atom d k -> LoT d -> Type where   -- Until https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0013-unlifted-newtypes.rst   -- and https://ghc.haskell.org/trac/ghc/ticket/14917-  -- are implemented, we are restricted to the (*) kind+  -- are implemented, we are restricted to the Type kind   Field :: { unField :: Interpret t x } -> Field t x deriving instance Show (Interpret t x) => Show (Field t x) @@ -60,7 +61,7 @@ -- > -- > instance GenericK Showable (a :&&: LoT0) where -- >   type RepK Showable = (Show :$: a) :=>: (Field Var0)-data (:=>:) (c :: Atom d Constraint) (f :: LoT d -> *) (x :: LoT d) where+data (:=>:) (c :: Atom d Constraint) (f :: LoT d -> Type) (x :: LoT d) where   SuchThat :: Interpret c x => f x -> (c :=>: f) x deriving instance (Interpret c x => Show (f x)) => Show ((c :=>: f) x) @@ -72,9 +73,9 @@ -- >  E :: t -> Exists -- > -- > instance GenericK E LoT0 where--- >   type RepK E = Exists (*) (Field Var0)-data Exists k (f :: LoT (k -> d) -> *) (x :: LoT d) where-  Exists :: forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d)+-- >   type RepK E = Exists Type (Field Var0)+data Exists k (f :: LoT (k -> d) -> Type) (x :: LoT d) where+  Exists :: forall k (t :: k) d (f :: LoT (k -> d) -> Type) (x :: LoT d)           .{ unExists :: f (t ':&&: x) } -> Exists k f x deriving instance (forall t. Show (f (t ':&&: x))) => Show (Exists k f x) @@ -88,7 +89,7 @@ -- > instance GenericK (Either a) -- > instance GenericK (Either a b) class GenericK (f :: k) where-  type RepK f :: LoT k -> *+  type RepK f :: LoT k -> Type    -- | Convert the data type to its representation.   fromK :: f :@@: x -> RepK f x@@ -126,8 +127,8 @@        => SubstRep (RepK f) x xs -> f x :@@: xs toRepK = toK @_ @f @(x ':&&: xs) . unsubstRep -class SubstRep' (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k) where-  type family SubstRep f x :: LoT k -> *+class SubstRep' (f :: LoT (t -> k) -> Type) (x :: t) (xs :: LoT k) where+  type family SubstRep f x :: LoT k -> Type   substRep   :: f (x ':&&: xs) -> SubstRep f x xs   unsubstRep :: SubstRep f x xs -> f (x ':&&: xs) @@ -153,12 +154,25 @@   substRep   (M1 x) = M1 (substRep   x)   unsubstRep (M1 x) = M1 (unsubstRep x) -instance (Interpret (SubstAtom c x) xs, Interpret c (x ':&&: xs), SubstRep' f x xs)+-- The context says that @Interpret (SubstAtom c x) xs@+-- and @Interpret c (x ':&&: xs)@ are equivalent.+-- But because @Interpret@ is a type family, and the right-hand side of+-- a quantified constraint must be a class, we must use "class synonyms"+-- @InterpretCons@ and @InterpretSubst@.+instance ( Interpret (SubstAtom c x) xs => InterpretCons c x xs+         , Interpret c (x ':&&: xs) => InterpretSubst 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   (SuchThat x) = SuchThat (substRep   x)-  unsubstRep (SuchThat x) = SuchThat (unsubstRep x)+  substRep   (SuchThat x) = SuchThat (substRep   x) :: InterpretSubst c x xs => SubstRep (c :=>: f) x xs+  unsubstRep (SuchThat x) = SuchThat (unsubstRep x) :: InterpretCons  c x xs => (c :=>: f) (x ':&&: xs) +class    Interpret c (x ':&&: xs) => InterpretCons c x xs+instance Interpret c (x ':&&: xs) => InterpretCons c x xs++class    Interpret (SubstAtom c x) xs => InterpretSubst c x xs+instance Interpret (SubstAtom c x) xs => InterpretSubst c x xs+ 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)@@ -178,7 +192,7 @@ -- in "GHC.Generics" with a representation using this module. -- You are never expected to manipulate this type class directly, -- it is part of the deriving mechanism for 'GenericK'.-class Conv (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) where+class Conv (gg :: Type -> Type) (kg :: LoT d -> Type) (tys :: LoT d) where   toGhcGenerics  :: kg tys -> gg a   toKindGenerics :: gg a -> kg tys 

@@ -13,6 +13,7 @@ {-# language UndecidableInstances  #-} module Generics.Kind.Examples where +import           Data.Kind import           GHC.Generics    (Generic) import           GHC.TypeLits import           Type.Reflection (Typeable)@@ -81,24 +82,24 @@  -- Hand-written instance -data SimpleIndex :: * -> * -> * where+data SimpleIndex :: Type -> Type -> Type where   MkSimpleIndex :: [a] -> SimpleIndex [a] b  instance GenericK SimpleIndex where   type RepK SimpleIndex-    = Exists (*) ((Var1 :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))+    = Exists Type ((Var1 :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))   toK (Exists (SuchThat (Field x))) = MkSimpleIndex x  instance GenericK (SimpleIndex a) where   type RepK (SimpleIndex a)-    = Exists (*) (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))+    = Exists Type (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))   toK (Exists (SuchThat (Field x))) = MkSimpleIndex x  instance GenericK (SimpleIndex a b) where   type RepK (SimpleIndex a b)-    = Exists (*) (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))+    = Exists Type (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))   toK (Exists (SuchThat (Field x))) = MkSimpleIndex x @@ -109,7 +110,7 @@ instance GenericK WeirdTree where   type RepK WeirdTree     = Field (WeirdTree :$: Var0) :*: Field (WeirdTree :$: Var0)-      :+: Exists (*) ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1))+      :+: Exists Type ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1))    fromK (WeirdBranch l r) = L1 $                     Field l :*: Field r   fromK (WeirdLeaf   a x) = R1 $ Exists $ SuchThat $ Field a :*: Field x@@ -126,8 +127,8 @@ instance GenericK WeirdTreeR where   type RepK WeirdTreeR     = Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0)-      :+: Exists (*) (((Show :$: Var1) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))-                      :=>: (Field Var0 :*: Field Var1))+      :+: Exists Type (((Show :$: Var1) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))+                       :=>: (Field Var0 :*: Field Var1))    fromK (WeirdBranchR l r) = L1 $                     Field l :*: Field r   fromK (WeirdLeafR   a x) = R1 $ Exists $ SuchThat $ Field a :*: Field x@@ -138,8 +139,8 @@ instance GenericK (WeirdTreeR a) where   type RepK (WeirdTreeR a)     = Field ('Kon (WeirdTreeR a)) :*: Field ('Kon (WeirdTreeR a))-    :+: Exists (*) (('Kon (Show a) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))-                    :=>: (Field Var0 :*: Field ('Kon a)))+    :+: Exists Type (('Kon (Show a) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))+                     :=>: (Field Var0 :*: Field ('Kon a)))    fromK (WeirdBranchR l r) = L1 $                     Field l :*: Field r   fromK (WeirdLeafR   a x) = R1 $ Exists $ SuchThat $ Field a :*: Field x@@ -167,16 +168,16 @@ -- Weird-kinded types  data T (a :: k) where-  MkT :: forall (a :: *). Maybe a -> T a+  MkT :: forall (a :: Type). Maybe a -> T a  {- GHC rewrites this to the following Core data T (a :: k) =   forall (a' :: Type). (k ~ Type, a ~~ a') => MkT (Maybe a') -} -instance GenericK (T :: k -> *) where-  type RepK (T :: k -> *) =-    Exists (*) (('Kon (k ~ (*)) ':&: (Var0 :~~: Var1)) :=>: Field (Maybe :$: Var0))+instance GenericK (T :: k -> Type) where+  type RepK (T :: k -> Type) =+    Exists Type (('Kon (k ~ Type) ':&: (Var0 :~~: Var1)) :=>: Field (Maybe :$: Var0))   fromK (MkT x) = Exists (SuchThat (Field x))   toK (Exists (SuchThat (Field x))) = MkT x @@ -196,13 +197,13 @@ data P' j (a :: k) where   P' :: forall k (a :: k). P' k a -instance GenericK (P' j :: k -> *) where-  type RepK (P' j :: k -> *) = ('Kon k :~: 'Kon j) :=>: U1+instance GenericK (P' j :: k -> Type) where+  type RepK (P' j :: k -> Type) = ('Kon k :~: 'Kon j) :=>: U1   fromK P' = SuchThat U1   toK (SuchThat U1) = P' -instance GenericK (P' :: * -> k -> *) where-  type RepK (P' :: * -> k -> *) = ('Kon k :~: Var0) :=>: U1+instance GenericK (P' :: Type -> k -> Type) where+  type RepK (P' :: Type -> k -> Type) = ('Kon k :~: Var0) :=>: U1   fromK P' = SuchThat U1   toK (SuchThat U1) = P'