kind-generics 0.3.0.0 → 0.4.0.0

raw patch · 5 files changed

+243/−63 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +13/−0
• README.md +165/−22
• kind-generics.cabal +3/−3
• src/Generics/Kind.hs +15/−15
• src/Generics/Kind/Examples.hs +47/−23

@@ -0,0 +1,13 @@+# Revision history for `kind-generics`++## 0.4++* Removed second parameter from `GenericK`. Thanks to Li-yao Xia who submitted a [merge request](https://gitlab.com/trupill/kind-generics/merge_requests/5).++## 0.3++* Renamed `F` and `E` to more descriptive names `Field` and `Exists`.++## 0.2++* Split functionality between `kind-apply`, `kind-generics`, and `kind-generics-deriving`.

@@ -26,8 +26,8 @@ By doing so, two instances are generated:  ```haskell-instance GenericK Tree     (a :&&: LoT0) where ...-instance GenericK (Tree a) LoT0          where ...+instance GenericK Tree     where ...+instance GenericK (Tree a) where ... ```  ### Derivation from `GHC.Generics`@@ -46,10 +46,10 @@ Let us look at the `GenericK` instance for `Tree`:  ```haskell-instance GenericK Tree (a :&&: LoT0) where+instance GenericK Tree where   type RepK Tree = (Field (Tree :$: Var0) :*: Field (Tree :$: Var0))                    :+: (Field Var0)-instance GenericK (Tree a) LoT0 where+instance GenericK (Tree a) where   type RepK (Tree a) = SubstRep (RepK Tree) a   fromK = fromRepK   toK   = toRepK@@ -76,7 +76,7 @@ Let us have a closer look at the definition of the `GenericK` type class. If you have been using other data type-generic programming libraries you might recognize `RepK` as the generalized version of `Rep`, which ties a data type with its description, and the pair of functions `fromK` and `toK` to go back and forth the original values and their generic counterparts.  ```haskell-class GenericK (f :: k) (x :: LoT k) where+class GenericK (f :: k) where   type RepK f :: LoT k -> *   fromK :: f :@@: x -> RepK f x   toK   :: RepK f x -> f :@@: x@@ -121,9 +121,9 @@ For a productive usage of `kind-generics`, you should provide as many views of your data type as you can. In the case of `Either` this entails writing the following instances:  ```haskell-instance GenericK Either (a :&&: b :&&: LoT0) where ...-instance GenericK (Either a)    (b :&&: LoT0) where ...-instance GenericK (Either a b)          LoT0  where ...+instance GenericK Either       where ...+instance GenericK (Either a)   where ...+instance GenericK (Either a b) where ... ```  Sometimes it is not possible to write all of these instances, due to restrictions in GHC's type system. The most common case is a data type making use of a type family -- we cannot write something like `Fam :$: Var0` because type families cannot be partially applied. The `kind-generics-th` package contains a thorough description of these limitations.@@ -139,7 +139,7 @@ For example, suppose the `a` is the name of the first type variable and `b` the name of the second. Here are the corresponding atoms:  ```haskell-a            ->  V0+a            ->  Var0 Maybe a      ->  Kon Maybe :@: Var0 Either b a   ->  Kon Either :@: Var1 :@: Var0 b (Maybe a)  ->  Var1 :@: (Kon Maybe :@: Var0)@@ -147,7 +147,7 @@  Since the `Kon f :@: x` pattern is very common, `kind-generics` also allows you to write it as simply `f :$: x`. The names `(:$:)` and `(:@:)` are supposed to resemble `(<$>)` and `(<*>)` from the `Applicative` type class. -The kind of an atom is described by two pieces of information, `Atom d k`. The first argument `d` specifies the amount of variables that it uses. The second argument `k` tells you the kind of the type you obtain if you replace the variable markers `V0`, `V1`, ... by actual types. For example:+The kind of an atom is described by two pieces of information, `Atom d k`. The first argument `d` specifies the amount of variables that it uses. The second argument `k` tells you the kind of the type you obtain if you replace the variable markers `Var0`, `Var1`, ... by actual types. For example:  ```haskell Var0                       ->  Atom (k -> ks)             k@@ -174,7 +174,7 @@ At the term level there is almost no difference in the usage, except for the fact that fields are wrapped in the `Field` constructor instead of `K1`.  ```haskell-instance GenericK Tree (a :&&: LoT0) where+instance GenericK Tree where   type RepK Tree = (Field (Tree :$: Var0) :*: Field (Tree :$: Var0))                    :+: (Field Var0) @@ -190,14 +190,14 @@  ```haskell data WeirdTree a where-  WeirdBranch :: WeirdTree a -> WeirdTree a -> WeirdTree a +  WeirdBranch :: WeirdTree a -> WeirdTree a -> WeirdTree a   WeirdLeaf   :: Show a => t -> a -> WeirdTree a ```  The family of pattern functors `V1`, `U1`, `Field`, `(:+:)`, and `(:*:)` is not enough. Let us see what other things we use in the representation of `WeirdTree`:  ```haskell-instance GenericK WeirdTree (a :&&: LoT0) where+instance GenericK WeirdTree where   type RepK WeirdTree     = Field (WeirdTree :$: Var0) :*: Field (WeirdTree :$: Var0)       :+: Exists (*) ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1))@@ -210,7 +210,7 @@ In most cases, `GenericK` instances for GADTs can be derived by `kind-generics-th`. Just for the record, here is how one of such `GenericK` instances looks like:  ```haskell-instance GenericK WeirdTree (a :&&: LoT0) where+instance GenericK WeirdTree where   type RepK WeirdTree = ...    fromK (WeirdBranch l r) = L1 $                     Field l :*: Field r@@ -279,7 +279,7 @@  ```haskell instance GShow (Field t) where-  type ReqsShow (Field t) x = Interpret t x+  type ReqsShow (Field t) x = Show (Interpret t x)   gshow = ... ``` @@ -312,7 +312,7 @@  ### Using an explicit list of types -A more powerful approach to using `kind-generics` is to imitate the separation done in `GenericK` between a head and its type arguments. That means extending the class with a new parameter, and reworking the basic cases to include that argument.+A more powerful approach to using `kind-generics` is to separate the head of a type from its type arguments. That means extending the class with a new parameter, and reworking the basic cases to include that argument.  ```haskell class GShow (f :: LoT k -> *) (x :: LoT k) where@@ -356,7 +356,7 @@  ```haskell class GFunctor f where-  gmap :: (a -> b) -> f a -> f b +  gmap :: (a -> b) -> f a -> f b ```  Following the approach outlined above, we need to reify the arguments to `f` as additional parameters to the type class. Since `f` appears applied to two different arguments, we get not one but two parameters in the type class.@@ -365,12 +365,11 @@ class GFunctor (f :: LoT k -> *) (as :: LoT k) (bs :: LoT k) where ... ``` -The problem now is that `as` and `bs` are *lists* of types. But the functor action only works over the *last* one (in general, only over *one* position). So how do we express the type of `gmap`? We can use a `TyVar` to specify that position, and the interpret it over the list of types. Since the new variable `v` appears only as argument to a type family, we need some kind of `Proxy` type to make GHC happy.+The problem now is that `as` and `bs` are *lists* of types. But the functor action only works over the *last* one (in general, only over *one* position). So how do we express the type of `gmap`? We can use a `TyVar` to specify that position, and the interpret it over the list of types. Since the new variable `v` appears only as argument to a type family, we need some kind of `Proxy` type to make GHC happy, or to enable the `AllowAmbiguousTypes` extension and work around the lack of inference with type applications.  ```haskell class GFunctor (f :: LoT k -> *) (v :: TyVar d *) (as :: LoT k) (bs :: LoT k) where-  gmap :: Proxy v-       -> (Interpret (Var v) as -> Interpret (Var v) bs)+  gmap :: (Interpret (Var v) as -> Interpret (Var v) bs)        -> f as -> f bs ``` @@ -381,13 +380,157 @@          => GFunctor (Exists k f) v as bs where ... ``` -The rest of the implementation of `GFunctor` can be found in `kind-generics-deriving`. The most complex part is to detect whether a field mentions the specific variable we are mapping over, because otherwise the data has to remain constant. Luckily, the very strong types guarantee that we don't make a mistake.- We have seen three ways of handling generic operations in `kind-generics`:  * *Introducing a requirements constraint*. This is the simpler one, and code stays almost verbatim from a `GHC.Generics` implementation. However, we cannot support existentials or constraints. * *Using an explicit list of types*. In this case the code can also be copied almost verbatim from a `GHC.Generics` implementations. The type class implementing the generic operation is enlarged with additional parameters to account for the lists of types which are applied in the operations. With this approach we can handle almost any operation which consumes a value of a GADT. * *Explicit list of types + position*. When defining generic operations over higher-rank types -- like `Functor` -- it is usually required to have an additional parameter in the type class to account for the *position* (or positions) which are affected by the operation. We need to do so because going under the `Exists` constructor shifts the indices of the variables.++### Inspecting atoms++The implementation of `GFunctor` follows the general pattern of calling `gmap` recursively when you find sums, products, constraints, or existentials. The complex part comes in the handling of fields: at that point we need to figure out whether the atom in that field mentions the specific variable we are mapping over, so we can apply the corresponding function. Take for example the representation of `Either`:++```haskell+type RepK Either = Field Var0 :+: Field Var1+```++If we want to implement the usual `fmap`, we need to map over `Var1`, but not over `Var0`. This section shows the technique required to do so. Luckily, the very strong types guarantee that we don't make a mistake.++In order to distinguish the shape of the atoms we need to introduce another type class, `GFunctorField`. It looks pretty much like `GFunctor`, with the difference that its first argument is an *atom* instead of a *pattern functor*. In turn, this means that in the type signature of its methods we need to interpret the atom to turn it into a type. Here are the two type classes side by side:++```haskell+class GFunctorField (t :: Atom k (*)) (v :: TyVar d *) (as :: LoT k) (bs :: LoT k) where+  gmapf :: (Interpret (Var v) as -> Interpret (Var v) bs)+        -> Interpret t as -> Interpret t bs+-- compare with+class GFunctor      (f :: LoT k -> *) (v :: TyVar d *) (as :: LoT k) (bs :: LoT k) where+  gmap  :: (Interpret (Var v) as -> Interpret (Var v) bs)+        -> f as -> f bs+```++If we assume that we satisfy the `GFunctorField` constraint for a given atom, we can write the `GFunctor` instance for the field constructor. Note that we have used explicit type applications because many of these types are ambiguous and cannot be resolved otherwise:++```haskell+instance forall t v as bs. GFunctorField t v as bs+         => GFunctorPos (Field t) v as bs where+  gmap f (Field x) = Field (gmapf @_ @t @v @as @bs f x)+```++This pattern is very common when dealing with generic derivation of operations for types which are not of kind `*`: introduce first a type class for the pattern functors, and then another one with each specific shape of `Field` you may have. Now the question turns into how to write each of the instances of `GFunctorField`.++Let's begin with the simplest one. If we have a constant, we know we don't need to apply any function to it. So `gmapf` is effectively just the identity function:++```haskell+instance GFunctorField (Kon t) v as bs where+  gfmappf _ = id+```++Another case we can handle is an type application of the form `f x`, provided that `f` is a functor and we recursively know how to map over `x`. Think of a data type similar to rose trees:++```haskell+data Rose a = a :<: [Rose a]+```++If we would write the functor instance by hand, in the case of the field of type `[Rose a]`, we would `fmap` over the list, using as argument the recursive `fmap` over `Rose`. The same pattern is captured with the following instance:++```haskell+instance forall f x v as bs.+         ( Functor (Interpret f as), Interpret f as ~ Interpret f bs+         , GFunctorField x v as bs )+         => GFunctorField (f :@: x) v as bs where+  gmapf f x = fmap (gmapf @_ @x @v @as @bs f) x+```++Ok, a bit more is happening than we I have just stated. The additional requirement `Interpret f as ~ Interpret f bs` forces the type constructor being applied to remain constant. This covers the case of `[Rose a]` being mapped to `[Rose b]`, since the type constructor is `[]` regardless of the type of its elements. However, `kind-generics` makes it possible to express more exotic types such as `Var1 :@: Var0`; in that case we are only able to construct the generic mapping operation if the argument to `Var1` is the same in both the input and output lists of kinds.++We come to the most important case: how to handle variables. The idea is quite simple: we want to apply the function only if the atom is the same variable as the one we intended to map over. Otherwise, the `gmap` function should keep the field as it was. A first approach would be to use the following two instances:++```haskell+instance {-# OVERLAPS     #-} GFunctorField (Var v) v as bs where ...+instance {-# OVERLAPPABLE #-} GFunctorField (Var v) w as bs where ...+```++The problem is that we require overlapping instances, which lead to brittle type checking, and are commonly regarded as a construct to avoid if possible. Fortunately, we can work around this problem in two different ways:++#### Preventing overlapping with more instances++Let us think for a moment how we would compare two type variables if we were writing the function in usual term-level Haskell. Usually the two final equations would be written with a catch-all pattern, but here it's important to have non-overlapping equations.++```haskell+compareTyVar :: TyVar d k -> TyVar d k -> Bool+compareTyVar VZ     VZ     = True+compareTyVar (VS v) (VS w) = compareTyVar v w+compareTyVar (VS v) VZ     = False+compareTyVar VZ     (VS w) = False+```++Each of these branches can be translated into an instance of `GFunctorField`. Note that the shape of the second argument limits the shape of the lists of types given afterwards, and this is reflected in the instances:++```haskell+-- case VZ / VZ -> apply the function+instance GFunctorField (Var VZ) VZ (a :&&: as) (b :&&: bs) where+  gmapf f x = f x+-- case VS v / VS w -> recur+instance forall v w r as s bs. GFunctorField (Var v) w as bs+         => GFunctorField (Var (VS v)) (VS w) (r :&&: as) (s :&&: bs) where+  gmapf f x = gmapf @d @(Var v) @w @as @bs f x+-- cases for different head constructors+instance GFunctorField (Var VZ) (VS w) (r :&&: as)   (r :&&: bs) where+  gmapf _ = id+instance GFunctorField (Var (VS v)) VZ (r :&&: LoT0) (r :&&: LoT0) where+  gmapf _ = id+```++#### Preventing overlapping using a type family++If you are not afraid of throwing more machinery at the problem, there's another approach to solve this problem. Checking for equality of types is brittle when used in the head of a type class. However, *closed* type families provide this ability in a well-behaved way:++```haskell+type family EqualTyVar (v :: TyVar d (*)) (w :: TyVar d (*)) :: Bool where+  EqualTyVar v v = True+  EqualTyVar v w = False+```++So what we can do is to introduce (yet) another type class which dispatches based on the result of applying `EqualTyVar` to the two involved type variables.++```haskell+class GFunctorVar (v :: TyVar d *) (w :: TyVar d *)+                  (as :: LoT d) (bs :: LoT d)+                  (equal :: Bool) where+  gmapv :: (Interpret (Var w) as -> Interpret (Var w) bs)+        ->  Interpret (Var v) as -> Interpret (Var v) bs+```++We have two cases: if the `equal` parameter is `True`, we know by construction that `v` and `w` are equal. Haskell's type system is not strong enough to carry this evidence, but we can force this to happen using a type equality constraint. So the following instance corresponds (finally) to the case in which we need to apply the function to the argument:++```haskell+instance v ~ w => GFunctorVar v w as bs True where+  gmapv f x = f x+```++In the other case we know by construction that interpreting `Var v` should result in the same type, since we are not mapping over it. Once again, we cannot bring the evidence from `EqualTyVar` to this point, but we can force GHC to check that it is the case using a type equality constraint:++```haskell+instance (Interpret (Var v) as ~ Interpret (Var v) bs)+        => GFunctorVar v w as bs False where+  gmapv _ = id+```++The last question is: how do we tell `GFunctorField` to use the result of `EqualTyVar` to choose an instance? We simply call the type family in the `instance` declaration:++```haskell+instance forall v w as bs. GFunctorVar v w as bs (EqualTyVar v w)+         => GFunctorField (Var v) w as bs where+  gmapf = gmapv @_ @v @w @as @bs @(EqualTyVar v w)+```++Adding this instance requires the `UndecidableInstances` extension, because GHC cannot guarantee resolution will terminate (as far as the compiler knows, `EqualTyVar` could be doing arbitrary computation). For that reason, I personally prefer to use the previous approach.++### More tricks for `Functor`++The implementation of `GFunctor` outlined above is correct, but could be more expensive that a hand-written one. For example, if you have a field of type `[[Int]]`, the implementation you get is equivalent to `fmap (fmap id)`: two levels of `fmap` corresponding to the two nested lists, and `id` because `Int` is a constant. But a programmer would just notice that the entire field never mentions a type variable, and would write `id` directly.++If you look at the implementation of `GFunctor` in `kind-generics-deriving` (called [`GFunctorPosition`](https://gitlab.com/trupill/kind-generics/blob/master/kind-generics-deriving/src/Generics/Kind/Derive/FunctorPosition.hs) in that library), you will notice a call to `ContainsTyVar` in the instance for `Field`. The role of this parameter is to short-cut evaluation in those cases. So before going into the `GFunctorField` recursive structure, we check whether the field mentions the type variable we are interested in.  ## Conclusion and limitations 

@@ -1,8 +1,8 @@ cabal-version:       >=1.10 name:                kind-generics-version:             0.3.0.0+version:             0.4.0.0 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 gound in 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: license:             BSD3 license-file:        LICENSE@@ -11,7 +11,7 @@ -- copyright: category:            Data build-type:          Simple-extra-source-files:  README.md+extra-source-files:  README.md, CHANGELOG.md  source-repository head   type:     git

@@ -38,7 +38,7 @@ import Data.Kind import GHC.Generics.Extra hiding ((:=>:), SuchThat) import qualified GHC.Generics.Extra as GG-import GHC.Exts+-- import GHC.Exts  -- | Fields: used to represent each of the (visible) arguments to a constructor. -- Replaces the 'K1' type from "GHC.Generics". The type of the field is@@ -60,14 +60,14 @@ -- > data Showable a = Show a => a -> X a -- > -- > instance GenericK Showable (a :&&: LoT0) where--- >   type RepK Showable = (Show :$: a) :=>: (Field V0)+-- >   type RepK Showable = (Show :$: a) :=>: (Field Var0) data (:=>:) (c :: Atom d Constraint) (f :: LoT d -> *) (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)  -- | Existentials: a representation of the form @E f@ describes -- a constructor whose inner type is represented by @f@, and where--- the type variable at index 0, @V0@, is existentially quantified.+-- the type variable at index 0, @Var0@, is existentially quantified. -- -- > data E where -- >  E :: t -> Exists@@ -81,16 +81,16 @@  -- THE TYPE CLASS --- | Representable types of any kind. The definition of an instance must--- mention the type constructor along with a list of types of the corresponding--- length. For example:+-- | Representable types of any kind. Examples: ----- > instance GenericK Int    LoT0--- > instance GenericK []     (a :&&: LoT0)--- > instance GenericK Either (a :&&: b :&&: LoT0)-class GenericK (f :: k) (x :: LoT k) where+-- > instance GenericK Int+-- > instance GenericK []+-- > instance GenericK Either+-- > instance GenericK (Either a)+-- > instance GenericK (Either a b)+class GenericK (f :: k) where   type RepK f :: LoT k -> *-  +   -- | Convert the data type to its representation.   fromK :: f :@@: x -> RepK f x   default@@ -105,13 +105,13 @@         => RepK f x -> f :@@: x   toK = to . toGhcGenerics -type GenericF t f x = (GenericK f x, x ~ (SplitF t f), t ~ (f :@@: x))+type GenericF t f x = (GenericK f, x ~ (SplitF t f), t ~ (f :@@: x)) fromF :: forall f t x. GenericF t f x => t -> RepK f x fromF = fromK @_ @f toF :: forall f t x. GenericF t f x => RepK f x -> t toF = toK @_ @f -type GenericN n t f x = (GenericK f x, 'TyEnv f x ~ (SplitN n t), t ~ (f :@@: x))+type GenericN n t f x = (GenericK f, 'TyEnv f x ~ (SplitN n t), t ~ (f :@@: x)) fromN :: forall n t f x. GenericN n t f x => t -> RepK f x fromN = fromK @_ @f toN :: forall n t f x. GenericN n t f x => RepK f x -> t@@ -119,11 +119,11 @@  -- CONVERSION BETWEEN FEWER AND MORE ARGUMENTS -fromRepK :: forall f x xs. (GenericK f (x ':&&: xs), SubstRep' (RepK f) x xs)+fromRepK :: forall f x xs. (GenericK f, SubstRep' (RepK f) x xs)          => f x :@@: xs -> SubstRep (RepK f) x xs fromRepK = substRep . fromK @_ @f @(x ':&&: xs) -toRepK :: forall f x xs. (GenericK f (x ':&&: xs), SubstRep' (RepK f) x xs)+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 

@@ -23,20 +23,27 @@  -- Obtained from Generic -instance GenericK Maybe (a ':&&: 'LoT0) where+instance GenericK Maybe where   type RepK Maybe = U1 :+: Field Var0-instance GenericK (Maybe a) LoT0 where+instance GenericK (Maybe a) where   type RepK (Maybe a) = SubstRep (RepK Maybe) a   fromK = fromRepK   toK   = toRepK -instance GenericK Either (a ':&&: b ':&&: LoT0) where+instance GenericK [] where+  type RepK [] = U1 :+: Field Var0 :*: Field ([] :$: Var0)+instance GenericK [a] where+  type RepK [a] = SubstRep (RepK []) a+  fromK = fromRepK+  toK   = toRepK++instance GenericK Either where   type RepK Either = Field Var0 :+: Field Var1-instance GenericK (Either a) (b ':&&: LoT0) where+instance GenericK (Either a) where   type RepK (Either a) = SubstRep (RepK Either) a   fromK = fromRepK   toK   = toRepK-instance GenericK (Either a b) LoT0 where+instance GenericK (Either a b) where   type RepK (Either a b) = SubstRep (RepK (Either a)) b   fromK = fromRepK   toK   = toRepK@@ -46,9 +53,9 @@ data Tree a = Branch (Tree a) (Tree a) | Leaf a             deriving Generic -instance GenericK Tree (a ':&&: 'LoT0) where+instance GenericK Tree where   type RepK Tree = Field (Tree :$: Var0) :*: Field (Tree :$: Var0) :+: Field Var0-instance GenericK (Tree a) LoT0 where+instance GenericK (Tree a) where   type RepK (Tree a) = SubstRep (RepK Tree) a   fromK = fromRepK   toK   = toRepK@@ -59,17 +66,17 @@ data instance HappyFamily (Maybe a) = HFM Bool data instance HappyFamily [a]       = HFL a -instance GenericK HappyFamily (a ':&&: 'LoT0) where+instance GenericK HappyFamily where   type RepK HappyFamily = TypeError (Text "Cannot describe this family uniformly")   fromK = undefined   toK   = undefined -instance GenericK (HappyFamily (Maybe a)) 'LoT0 where+instance GenericK (HappyFamily (Maybe a)) where   type RepK (HappyFamily (Maybe a)) = Field (Kon Bool)   fromK (HFM   x) = Field x   toK   (Field x) = HFM   x -instance GenericK (HappyFamily [a]) 'LoT0 where+instance GenericK (HappyFamily [a]) where   type RepK (HappyFamily [a]) = Field (Kon a)   fromK (HFL   x) = Field x   toK   (Field x) = HFL   x@@ -79,19 +86,19 @@ data SimpleIndex :: * -> * -> * where   MkSimpleIndex :: [a] -> SimpleIndex [a] b -instance GenericK SimpleIndex (a :&&: b :&&: LoT0) where+instance GenericK SimpleIndex where   type RepK SimpleIndex     = Exists (*) ((Var1 :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))   toK (Exists (SuchThat (Field x))) = (MkSimpleIndex x) -instance GenericK (SimpleIndex a) (b :&&: LoT0) where+instance GenericK (SimpleIndex a) where   type RepK (SimpleIndex a)     = Exists (*) ((Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))   toK (Exists (SuchThat (Field x))) = (MkSimpleIndex x) -instance GenericK (SimpleIndex a b) LoT0 where+instance GenericK (SimpleIndex a b) where   type RepK (SimpleIndex a b)     = Exists (*) ((Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))   fromK (MkSimpleIndex x) = Exists (SuchThat (Field x))@@ -101,7 +108,7 @@   WeirdBranch :: WeirdTree a -> WeirdTree a -> WeirdTree a    WeirdLeaf   :: Show a => t -> a -> WeirdTree a -instance GenericK WeirdTree (a ':&&: 'LoT0) where+instance GenericK WeirdTree where   type RepK WeirdTree     = Field (WeirdTree :$: Var0) :*: Field (WeirdTree :$: Var0)       :+: Exists (*) ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1))@@ -118,7 +125,7 @@   WeirdBranchR :: WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a    WeirdLeafR   :: (Show a, Eq t, Typeable t) => t -> a -> WeirdTreeR a -instance GenericK WeirdTreeR (a ':&&: 'LoT0) where+instance GenericK WeirdTreeR where   type RepK WeirdTreeR     = Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0)       :+: Exists (*) (((Show :$: Var1) :&: (Eq :$: Var0) :&: (Typeable :$: Var0))@@ -130,7 +137,7 @@   toK (L1 (Field l :*: Field r)) = WeirdBranchR l r   toK (R1 (Exists (SuchThat (Field a :*: Field x)))) = WeirdLeafR a x -instance GenericK (WeirdTreeR a) 'LoT0 where+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))@@ -142,6 +149,23 @@   toK (L1 (Field l :*: Field r)) = WeirdBranchR l r   toK (R1 (Exists (SuchThat (Field a :*: Field x)))) = WeirdLeafR a x +-- From https://gitlab.com/trupill/kind-generics/issues/3++data TTY m a where+  WriteTTY :: String -> TTY m ()+  ReadTTY  :: TTY m String++instance GenericK (TTY m a) where+  type RepK (TTY m a)+    =     ((Kon a :~: Kon ()) :=>: Field (Kon String))+      :+: ((Kon a :~: Kon String) :=>: U1)++  fromK (WriteTTY s) = L1 (SuchThat (Field s))+  fromK ReadTTY      = R1 (SuchThat U1)++  toK (L1 (SuchThat (Field s))) = WriteTTY s+  toK (R1 (SuchThat U1))        = ReadTTY+ -- Weird-kinded types  data T (a :: k) where@@ -152,7 +176,7 @@   forall (a' :: Type). (k ~ Type, a ~~ a') => MkT (Maybe a')  -} -instance GenericK (T :: k -> *) (a :&&: LoT0) where+instance GenericK (T :: k -> *) where   type RepK (T :: k -> *) =     Exists (*) ((Kon (k ~ (*)) :&: (Var0 :~~: Var1)) :=>: Field (Maybe :$: Var0))   fromK (MkT x) = Exists (SuchThat (Field x))@@ -161,7 +185,7 @@ data P k (a :: k) where   P :: forall k (a :: k). P k a -instance GenericK (P k) ((a :: k) :&&: LoT0) where+instance GenericK (P k) where   type RepK (P k) = U1   fromK P  = U1   toK   U1 = P@@ -174,12 +198,12 @@ data P' j (a :: k) where   P' :: forall k (a :: k). P' k a -instance GenericK (P' j :: k -> *) (a :&&: LoT0) where+instance GenericK (P' j :: k -> *) where   type RepK (P' j :: k -> *) = (Kon k :~: Kon j) :=>: U1   fromK P' = SuchThat U1   toK (SuchThat U1) = P' -instance GenericK (P' :: * -> k -> *) (j :&&: a :&&: LoT0) where+instance GenericK (P' :: * -> k -> *) where   type RepK (P' :: * -> k -> *) = (Kon k :~: Var0) :=>: U1   fromK P' = SuchThat U1   toK (SuchThat U1) = P'@@ -188,14 +212,14 @@  data Ranky = MkRanky (forall a. a -> a) -instance GenericK Ranky LoT0 where+instance GenericK Ranky where   type RepK Ranky = Field (ForAll ((->) :$: Var0 :@: Var0))   fromK (MkRanky x) = Field (ForAllI x)   toK (Field (ForAllI x)) = MkRanky x  newtype Ranky2 b = MkRanky2 ((forall a. a -> a) -> b) -instance GenericK Ranky2 (b ':&&: LoT0) where+instance GenericK Ranky2 where   type RepK Ranky2 = Field ((->) :$: ForAll ((->) :$: Var0 :@: Var0) :@: Var0)   fromK (MkRanky2 f) = Field (\(ForAllI x) -> f x)   toK (Field f) = MkRanky2 (\x -> f (ForAllI x))@@ -203,7 +227,7 @@ data Shower a where   MkShower :: (Show a => a -> String) -> Shower a -instance GenericK Shower (a ':&&: LoT0) where+instance GenericK Shower where   type RepK Shower = Field ((Show :$: Var0) :=>>: ((->) :$: Var0 :@: Kon String))   fromK (MkShower f) = Field (SuchThatI f)   toK (Field (SuchThatI f)) = MkShower f