Unverified Commit f4ad2bcf authored by Alejandro Serrano's avatar Alejandro Serrano
Browse files

Change * to Type (remove warning in GHC 9)

parent a793e7db
......@@ -18,6 +18,7 @@ module Data.PolyKinded (
, SplitF, Nat(..), TyEnv(..), SplitN
) where
import Data.Kind
import Data.Proxy
infixr 5 :&&:
......@@ -25,7 +26,7 @@ infixr 5 :&&:
-- to a data type of kind @k@.
data LoT k where
-- | Empty list of types.
LoT0 :: LoT (*)
LoT0 :: LoT Type
-- | Cons a type with a list of types.
(:&&:) :: k -> LoT ks -> LoT (k -> ks)
......@@ -35,15 +36,15 @@ type LoT2 a b = a ':&&: b ':&&: 'LoT0
-- | Apply a list of types to a type constructor.
--
-- >>> :kind! Either :@@: (Int :&&: Bool :&&: LoT0)
-- Either Int Bool :: *
type family (f :: k) :@@: (tys :: LoT k) :: * where
-- Either Int Bool :: Type
type family (f :: k) :@@: (tys :: LoT k) :: Type where
f :@@: _ = f
f :@@: as = f (HeadLoT as) :@@: TailLoT as
-- | Head of a non-empty list of types.
--
-- >>> :kind! HeadLoT (Int :&&: LoT0)
-- Int :: *
-- Int :: Type
type family HeadLoT (tys :: LoT (k -> k')) :: k where
HeadLoT (a ':&&: _) = a
......@@ -63,7 +64,7 @@ type family TailLoT (tys :: LoT (k -> k')) :: LoT k' where
-- On concrete lists, this is the identity function.
type family SpineLoT (ts :: LoT k) :: LoT k where
SpineLoT (ts :: LoT (k -> k')) = HeadLoT ts ':&&: SpineLoT (TailLoT ts)
SpineLoT (ts :: LoT (*)) = 'LoT0
SpineLoT (ts :: LoT Type) = 'LoT0
data SLoT (l :: LoT k) where
SLoT0 :: SLoT 'LoT0
......@@ -71,7 +72,7 @@ data SLoT (l :: LoT k) where
class SForLoT (l :: LoT k) where
slot :: SLoT l
instance (l ~ 'LoT0) => SForLoT (l :: LoT (*)) where
instance (l ~ 'LoT0) => SForLoT (l :: LoT Type) where
slot = SLoT0
instance (l ~ (t ':&&: ts), SForLoT ts) => SForLoT (l :: LoT (k -> k')) where
slot = SLoTA Proxy slot
......@@ -79,9 +80,9 @@ instance (l ~ (t ':&&: ts), SForLoT ts) => SForLoT (l :: LoT (k -> k')) where
-- | Split a type @t@ until the constructor @f@ is found.
--
-- >>> :kind! SplitF (Either Int Bool) Either
-- Int :&&: Bool :&&: LoT0 :: LoT (* -> * -> *)
-- Int :&&: Bool :&&: LoT0 :: LoT (Type -> Type -> Type)
-- >>> :kind! SplitF (Either Int Bool) (Either Int)
-- Bool :&&: LoT0 :: LoT (* -> *)
-- Bool :&&: LoT0 :: LoT (Type -> Type)
type SplitF (t :: d) (f :: k) = SplitF' t f 'LoT0
type family SplitF' (t :: d) (f :: k) (p :: LoT l) :: LoT k where
SplitF' f f acc = acc
......
......@@ -16,7 +16,7 @@ import Data.PolyKinded
import Data.Type.Equality
import GHC.Exts
data TyVar (d :: *) (k :: TYPE r) where
data TyVar (d :: Type) (k :: TYPE r) where
VZ :: TyVar (x -> xs) x
VS :: TyVar xs k -> TyVar (x -> xs) k
......@@ -33,13 +33,13 @@ type Var9 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))))
infixr 5 :&:
infixr 5 :=>>:
data Atom (d :: *) (k :: TYPE r) where
data Atom (d :: Type) (k :: TYPE r) where
Var :: TyVar d k -> Atom d k
Kon :: k -> Atom d k
(:@:) :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2
(:&:) :: Atom d Constraint -> Atom d Constraint -> Atom d Constraint
ForAll :: Atom (d1 -> d) (*) -> Atom d (*)
(:=>>:) :: Atom d Constraint -> Atom d (*) -> Atom d (*)
ForAll :: Atom (d1 -> d) Type -> Atom d Type
(:=>>:) :: Atom d Constraint -> Atom d Type -> Atom d Type
type f :$: x = 'Kon f ':@: x
type a :~: b = 'Kon (~) ':@: a ':@: b
......@@ -57,10 +57,10 @@ type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
Interpret ('ForAll f) tys = ForAllI f tys
Interpret (c ':=>>: f) tys = SuchThatI c f tys
newtype ForAllI (f :: Atom (d1 -> d) (*)) (tys :: LoT d) where
newtype ForAllI (f :: Atom (d1 -> d) Type) (tys :: LoT d) where
ForAllI :: (forall t. Interpret f (t ':&&: tys)) -> ForAllI f tys
newtype WrappedI (f :: Atom d (*)) (tys :: LoT d) =
newtype WrappedI (f :: Atom d Type) (tys :: LoT d) =
WrapI { unwrapI :: Interpret f tys }
toWrappedI :: forall f tys t. ForAllI f tys -> WrappedI f (t ':&&: tys)
......@@ -69,7 +69,7 @@ toWrappedI (ForAllI x) = WrapI (x @t)
fromWrappedI :: forall f tys. (forall t. WrappedI f (t ':&&: tys)) -> ForAllI f tys
fromWrappedI = coerce @(forall t. WrappedI f (t ':&&: tys))
newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d (*)) (tys :: LoT d) where
newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d Type) (tys :: LoT d) where
SuchThatI :: (Interpret c tys => Interpret f tys) -> SuchThatI c f tys
type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) :: Constraint where
......
......@@ -17,5 +17,5 @@ import GHC.Generics
-- >
-- > instance Generic (Showable a) where
-- > type Rep (Showable a) = (Show a) :=>: (K1 R a)
data (:=>:) (c :: Constraint) (f :: k -> *) (a :: k) where
data (:=>:) (c :: Constraint) (f :: k -> Type) (a :: k) where
SuchThat :: c => f a -> (c :=>: f) a
......@@ -21,7 +21,7 @@ geq' :: forall t. (GenericK t, GEq (RepK t), ReqsEq (RepK t) 'LoT0)
=> t -> t -> Bool
geq' x y = geq (fromK @_ @t @'LoT0 x) (fromK @_ @t @'LoT0 y)
class GEq (f :: LoT k -> *) where
class GEq (f :: LoT k -> Type) where
type ReqsEq f (tys :: LoT k) :: Constraint
geq :: ReqsEq f tys => f tys -> f tys -> Bool
......
......@@ -12,13 +12,14 @@
{-# language UndecidableInstances #-}
module Generics.Kind.Derive.EqTwoParams where
import Data.Kind
import Generics.Kind
geq2' :: forall t. (GenericK t, GEq2 (RepK t) 'LoT0 'LoT0)
=> t -> t -> Bool
geq2' x y = geq2 (fromK @_ @t @'LoT0 x) (fromK @_ @t @'LoT0 y)
class GEq2 (f :: LoT k -> *) (xs :: LoT k) (ys :: LoT k) where
class GEq2 (f :: LoT k -> Type) (xs :: LoT k) (ys :: LoT k) where
geq2 :: f xs -> f ys -> Bool
instance GEq2 U1 xs ys where
......
......@@ -24,7 +24,7 @@ fmapDefaultOne :: (GenericK f,
=> (a -> b) -> f a -> f b
fmapDefaultOne f = toK . gfmapo f . fromK
class GFunctorOne (f :: LoT (* -> *) -> *) where
class GFunctorOne (f :: LoT (Type -> Type) -> Type) where
type Reqs f a b :: Constraint
gfmapo :: Reqs f a b => (a -> b) -> f (LoT1 a) -> f (LoT1 b)
......@@ -57,7 +57,7 @@ instance GFunctorOne f => GFunctorOne (c :=>: f) where
-- actually you want = Interpret c (LoT1 a) => (Interpret c (LoT1 b), Reqs f a b)
gfmapo v (SuchThat x) = SuchThat (gfmapo v x)
class GFunctorOneArg (t :: Atom (* -> *) (*)) where
class GFunctorOneArg (t :: Atom (Type -> Type) Type) where
gfmapof :: Proxy t -> (a -> b)
-> Interpret t (LoT1 a) -> Interpret t (LoT1 b)
......
......@@ -12,6 +12,7 @@
{-# language UndecidableInstances #-}
module Generics.Kind.Derive.FunctorPosition where
import Data.Kind
import GHC.TypeLits
import Generics.Kind
......@@ -35,7 +36,7 @@ bimapDefault :: forall f a c b d.
bimapDefault f g = fmapDefaultPos @'VZ @f @(LoT2 a d) @(LoT2 c d) f
. fmapDefaultPos @('VS 'VZ) @f @(LoT2 a b) @(LoT2 a d) g
class GFunctorPos (f :: LoT k -> *) (v :: TyVar k *)
class GFunctorPos (f :: LoT k -> Type) (v :: TyVar k Type)
(as :: LoT k) (bs :: LoT k) where
gfmapp :: (Interpret ('Var v) as -> Interpret ('Var v) bs)
-> f as -> f bs
......@@ -71,7 +72,7 @@ instance forall t v as bs. GFunctorArgPos t v as bs (ContainsTyVar v t)
=> GFunctorPos (Field t) v as bs where
gfmapp v (Field x) = Field (gfmappf @_ @t @v @as @bs @(ContainsTyVar v t) v x)
class GFunctorArgPos (t :: Atom d (*)) (v :: TyVar d *)
class GFunctorArgPos (t :: Atom d Type) (v :: TyVar d Type)
(as :: LoT d) (bs :: LoT d)
(p :: Bool) where
gfmappf :: (Interpret ('Var v) as -> Interpret ('Var v) bs)
......@@ -93,7 +94,7 @@ instance ( Functor (Interpret f as), Interpret f as ~ Interpret f bs
instance GFunctorArgPos ('Var 'VZ) 'VZ (a ':&&: as) (b ':&&: bs) 'True where
gfmappf f x = f x
-- We need to keep looking
instance forall d (v :: TyVar d (*)) n r as s bs isthere.
instance forall d (v :: TyVar d Type) n r as s bs isthere.
GFunctorArgPos ('Var v) n as bs isthere
=> GFunctorArgPos ('Var ('VS v)) ('VS n) (r ':&&: as) (s ':&&: bs) isthere where
gfmappf f x = gfmappf @d @('Var v) @n @as @bs @isthere f x
......@@ -107,11 +108,11 @@ instance TypeError ('Text "Should never get here")
-- Alternative implementation
{-
type family EqualTyVar (v :: TyVar d (*)) (w :: TyVar d (*)) :: Bool where
type family EqualTyVar (v :: TyVar d Type) (w :: TyVar d Type) :: Bool where
EqualTyVar v v = True
EqualTyVar v w = False
class GFunctorVarPos (v :: TyVar d *) (w :: TyVar d *)
class GFunctorVarPos (v :: TyVar d Type) (w :: TyVar d Type)
(as :: LoT d) (bs :: LoT d)
(equal :: Bool) where
gfmappv :: (Interpret (Var w) as -> Interpret (Var w) bs)
......
......@@ -17,6 +17,7 @@ import Control.Applicative
import Control.Monad
import Data.Aeson
import Data.Aeson.Types
import Data.Kind
import Data.Proxy
import GHC.Generics (Meta (..))
import GHC.TypeLits
......@@ -30,9 +31,9 @@ gfromJSON' :: forall t. (GenericK t, GFromJSONK (RepK t) 'LoT0)
=> Value -> Parser t
gfromJSON' v = fmap (toK @_ @t @'LoT0) (gfromJSON v)
class GToJSONK (f :: LoT k -> *) (x :: LoT k) where
class GToJSONK (f :: LoT k -> Type) (x :: LoT k) where
gtoJSON :: f x -> Value
class GFromJSONK (f :: LoT k -> *) (x :: LoT k) where
class GFromJSONK (f :: LoT k -> Type) (x :: LoT k) where
gfromJSON :: Value -> Parser (f x)
instance ToJSON (Interpret t x)
......
......@@ -14,6 +14,7 @@
{-# language UndecidableInstances #-}
module Generics.Kind.Derive.KFunctor where
import Data.Kind
import Data.PolyKinded.Functor
import Data.Proxy
......@@ -23,13 +24,13 @@ kfmapDefault :: forall k (f :: k) v as bs. (GenericK f, GenericK f, GFunctor (Re
=> Mappings v as bs -> f :@@: as -> f :@@: bs
kfmapDefault v = toK @k @f @bs . gfmap v . fromK @k @f @as
fmapDefault' :: forall (f :: * -> *) a b.
fmapDefault' :: forall (f :: Type -> Type) a b.
(GenericK f, GenericK f,
GFunctor (RepK f) '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0))
=> (a -> b) -> f a -> f b
fmapDefault' f = kfmapDefault (f :^: M0 :: Mappings '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0))
class GFunctor (f :: LoT k -> *) (v :: Variances) (as :: LoT k) (bs :: LoT k) where
class GFunctor (f :: LoT k -> Type) (v :: Variances) (as :: LoT k) (bs :: LoT k) where
gfmap :: Mappings v as bs -> f as -> f bs
instance GFunctor U1 v as bs where
......@@ -52,12 +53,12 @@ instance (Interpret c as => GFunctor f v as bs, {- Ty c as => -} Interpret c bs)
gfmap v (SuchThat x) = SuchThat (gfmap v x)
instance forall f v as bs.
(forall (t :: *). GFunctor f ('Co ': v) (t ':&&: as) (t ':&&: bs))
=> GFunctor (Exists (*) f) v as bs where
(forall (t :: Type). GFunctor f ('Co ': v) (t ':&&: as) (t ':&&: bs))
=> GFunctor (Exists Type f) v as bs where
gfmap v (Exists (x :: f (t ':&&: x)))
= Exists (gfmap ((id :^: v) :: Mappings ('Co ': v) (t ':&&: as) (t ':&&: bs)) x)
class GFunctorArg (t :: Atom d (*))
class GFunctorArg (t :: Atom d Type)
(v :: Variances) (intended :: Variance)
(as :: LoT d) (bs :: LoT d) where
gfmapf :: Proxy t -> Proxy intended
......@@ -73,13 +74,13 @@ instance GFunctorArg ('Kon t) v 'Co as bs where
instance GFunctorArg ('Kon t) v 'Contra as bs where
gfmapf _ _ _ = id
instance forall d (f :: Atom (* -> d) *) v (as :: LoT d) (bs :: LoT d).
(forall (t :: *). GFunctorArg f ('Co ': v) 'Co (t ':&&: as) (t ':&&: bs))
instance forall d (f :: Atom (Type -> d) Type) v (as :: LoT d) (bs :: LoT d).
(forall (t :: Type). GFunctorArg f ('Co ': v) 'Co (t ':&&: as) (t ':&&: bs))
=> GFunctorArg ('ForAll f) v 'Co as bs where
gfmapf _ _ v x = fromWrappedI $ go $ toWrappedI x
where
go :: forall (t :: *). WrappedI f (t ':&&: as) -> WrappedI f (t ':&&: bs)
go (WrapI p) = WrapI (gfmapf @(* -> d) @f @('Co ': v) @'Co @(t ':&&: as) @(t ':&&: bs)
go :: forall (t :: Type). WrappedI f (t ':&&: as) -> WrappedI f (t ':&&: bs)
go (WrapI p) = WrapI (gfmapf @(Type -> d) @f @('Co ': v) @'Co @(t ':&&: as) @(t ':&&: bs)
Proxy Proxy (id :^: v) p)
instance GFunctorArg ('Var 'VZ) (r ': v) r (a ':&&: as) (b ':&&: bs) where
......
......@@ -12,6 +12,7 @@
{-# language UndecidableInstances #-}
module Generics.Kind.Derive.Traversable where
import Data.Kind
import GHC.TypeLits
import Generics.Kind
......@@ -28,7 +29,7 @@ traverseDefault :: forall f a b g. (GenericK f, GenericK f,
=> (a -> g b) -> f a -> g (f b)
traverseDefault = traverseDefaultPos @'VZ @f @(LoT1 a) @(LoT1 b)
class GTraversable (f :: LoT k -> *) (v :: TyVar k *)
class GTraversable (f :: LoT k -> Type) (v :: TyVar k Type)
(as :: LoT k) (bs :: LoT k) where
gtraverse :: Applicative g
=> (Interpret ('Var v) as -> g (Interpret ('Var v) bs))
......@@ -66,7 +67,7 @@ instance forall t v as bs. GTraversableArg t v as bs (ContainsTyVar v t)
=> GTraversable (Field t) v as bs where
gtraverse v (Field x) = Field <$> gtraversef @_ @t @v @as @bs @(ContainsTyVar v t) v x
class GTraversableArg (t :: Atom d (*)) (v :: TyVar d *)
class GTraversableArg (t :: Atom d Type) (v :: TyVar d Type)
(as :: LoT d) (bs :: LoT d) (p :: Bool) where
gtraversef :: Applicative g
=> (Interpret ('Var v) as -> g (Interpret ('Var v) bs))
......@@ -88,7 +89,7 @@ instance ( Traversable (Interpret f as), Interpret f as ~ Interpret f bs
instance GTraversableArg ('Var 'VZ) 'VZ (a ':&&: as) (b ':&&: bs) 'True where
gtraversef f x = f x
-- We need to keep looking
instance forall d (v :: TyVar d (*)) n r as s bs isthere.
instance forall d (v :: TyVar d Type) n r as s bs isthere.
GTraversableArg ('Var v) n as bs isthere
=> GTraversableArg ('Var ('VS v)) ('VS n) (r ':&&: as) (s ':&&: bs) isthere where
gtraversef f x = gtraversef @d @('Var v) @n @as @bs @isthere f x
......
......@@ -36,7 +36,7 @@ import qualified GHC.Generics.Extra as GG
type DataType d = [ Branch d ]
type Constraints d = [ Atom d Constraint ]
type Fields d = [ Atom d (*) ]
type Fields d = [ Atom d Type ]
data Branch (d :: k) where
E :: Branch (p -> d) -> Branch d
......@@ -44,38 +44,38 @@ data Branch (d :: k) where
-- CONSTRAINTS
type family AllFields (c :: * -> Constraint) (d :: DataType k) (tys :: LoT k) :: Constraint where
type family AllFields (c :: Type -> Constraint) (d :: DataType k) (tys :: LoT k) :: Constraint where
AllFields c '[] tys = ()
AllFields c (b ': bs) tys = (AllFieldsB c b tys, AllFields c bs tys)
type family AllFieldsB (c :: * -> Constraint) (d :: Branch k) (tys :: LoT k) :: Constraint where
type family AllFieldsB (c :: Type -> Constraint) (d :: Branch k) (tys :: LoT k) :: Constraint where
-- AllFieldsB c ('E b) tys = AllFieldsBForAll c b tys
-- AllFieldsB c (cs ':=>: fs) tys = AllFieldsBImplies c cs fs tys
AllFieldsB c (cs ':=>: fs) tys = AllFieldsP c fs tys
{-
class (forall t. AllFieldsB c b (t ':&&: tys))
=> AllFieldsBForAll (c :: * -> Constraint) (b :: Branch (p -> k)) (tys :: LoT k)
=> AllFieldsBForAll (c :: Type -> Constraint) (b :: Branch (p -> k)) (tys :: LoT k)
instance (forall t. AllFieldsB c b (t ':&&: tys)) => AllFieldsBForAll c b tys
class (Satisfies cs tys => AllFieldsP c fs tys)
=> AllFieldsBImplies (c :: * -> Constraint) (cs :: Constraints k) (fs :: Fields k) (tys :: LoT k)
=> AllFieldsBImplies (c :: Type -> Constraint) (cs :: Constraints k) (fs :: Fields k) (tys :: LoT k)
instance (Satisfies cs tys => AllFieldsP c fs tys) => AllFieldsBImplies c cs fs tys
-}
type family AllFieldsP (c :: * -> Constraint) (d :: Fields k) (tys :: LoT k) :: Constraint where
type family AllFieldsP (c :: Type -> Constraint) (d :: Fields k) (tys :: LoT k) :: Constraint where
AllFieldsP c '[] tys = ()
AllFieldsP c (f ': fs) tys = (c (Interpret f tys), AllFieldsP c fs tys)
type family AllAtoms (c :: Atom k (*) -> Constraint) (d :: DataType k) :: Constraint where
type family AllAtoms (c :: Atom k Type -> Constraint) (d :: DataType k) :: Constraint where
AllAtoms c '[] = ()
AllAtoms c (b ': bs) = (AllAtomsB c b, AllAtoms c bs)
type family AllAtomsB (c :: Atom k (*) -> Constraint) (d :: Branch k) :: Constraint where
type family AllAtomsB (c :: Atom k Type -> Constraint) (d :: Branch k) :: Constraint where
-- Existentials and implications should be as above
AllAtomsB c (cs ':=>: fs) = AllAtomsP c fs
type family AllAtomsP (c :: Atom k (*) -> Constraint) (d :: Fields k) :: Constraint where
type family AllAtomsP (c :: Atom k Type -> Constraint) (d :: Fields k) :: Constraint where
AllAtomsP c '[] = ()
AllAtomsP c (f ': fs) = (c f, AllAtomsP c fs)
......@@ -86,7 +86,7 @@ data NB (tys :: LoT d) (b :: Branch d) where
SuchThat_ :: Interpret c tys => NB tys (cs ':=>: fs) -> NB tys ((c ': cs) ':=>: fs)
Fields_ :: NP (NA tys) fs -> NB tys ('[] ':=>: fs)
data NA (tys :: LoT d) (f :: Atom d (*)) where
data NA (tys :: LoT d) (f :: Atom d Type) where
Atom_ :: Interpret f tys -> NA tys f
type RepK (d :: DataType k) (tys :: LoT k) = NS (NB tys) d
......@@ -124,7 +124,7 @@ toN = toK @_ @f
-- Sums
class ConvSum (gg :: * -> *) (kc :: DataType d) (tys :: LoT d) where
class ConvSum (gg :: Type -> Type) (kc :: DataType d) (tys :: LoT d) where
toGhcGenericsS :: RepK kc tys -> gg a
toKindGenericsS :: gg a -> RepK kc tys
......@@ -166,7 +166,7 @@ instance (ConvConstructor f f' tys, ConvSum gs gs' tys)
-- Constructors
class ConvConstructor (gg :: * -> *) (kb :: Branch d) (tys :: LoT d) where
class ConvConstructor (gg :: Type -> Type) (kb :: Branch d) (tys :: LoT d) where
toGhcGenericsC :: NB tys kb -> gg a
toKindGenericsC :: gg a -> NB tys kb
......@@ -197,7 +197,7 @@ instance (c ~ Interpret c' tys, ConvConstructor f (cs ':=>: f') tys)
-- Products
class ConvProduct (gg :: * -> *) (kp :: Fields d) (tys :: LoT d) where
class ConvProduct (gg :: Type -> Type) (kp :: Fields d) (tys :: LoT d) where
toGhcGenericsP :: NP (NA tys) kp -> gg a
toKindGenericsP :: gg a -> NP (NA tys) kp
......@@ -222,7 +222,7 @@ instance (ConvAtom f f' tys, ConvProduct gs gs' tys)
-- Atoms
class ConvAtom (gg :: * -> *) (ka :: Atom d (*)) (tys :: LoT d) where
class ConvAtom (gg :: Type -> Type) (ka :: Atom d Type) (tys :: LoT d) where
toGhcGenericsA :: NA tys ka -> gg a
toKindGenericsA :: gg a -> NA tys ka
......
......@@ -11,6 +11,7 @@
{-# language UndecidableInstances #-}
module Generics.SOP.Kind.Derive.Functor where
import Data.Kind
import Data.PolyKinded.Functor
import Data.Proxy
import Generics.SOP.Kind
......@@ -43,7 +44,7 @@ gfmap v = goS
goP ((Atom_ x :: NA as fl) :* xs) = Atom_ (gfmapf (Proxy @fl) (Proxy @'Co) v x) :* goP xs
class GFunctorArg (v :: Variances) (intended :: Variance)
(as :: LoT d) (bs :: LoT d) (t :: Atom d (*)) where
(as :: LoT d) (bs :: LoT d) (t :: Atom d Type) where
gfmapf :: Proxy t -> Proxy intended
-> Mappings v as bs
-> Mapping intended (Interpret t as) (Interpret t bs)
......
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:
......
......@@ -46,11 +46,11 @@ import qualified GHC.Generics.Extra as GG
--
-- > 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)
......@@ -61,7 +61,7 @@ deriving instance Show (Interpret t x) => Show (Field t x)
-- >
-- > 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)
......@@ -73,9 +73,9 @@ deriving instance (Interpret c x => Show (f x)) => Show ((c :=>: f) x)
-- > 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)
......@@ -89,7 +89,7 @@ deriving instance (forall t. Show (f (t ':&&: x))) => Show (Exists k f x)
-- > 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
......@@ -127,8 +127,8 @@ toRepK :: forall f x xs. (GenericK f, SubstRep' (RepK f) x xs)
=> 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)
......@@ -192,7 +192,7 @@ type family SubstAtom (f :: Atom (t -> k) d) (x :: t) :: Atom k d where
-- 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 @@ instance GenericK (HappyFamily [a]) where
-- 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 @@ data WeirdTree a where
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 @@ data WeirdTreeR a where
instance GenericK WeirdTreeR where
type RepK WeirdTreeR
= Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0)