{-# OPTIONS_GHC -fno-warn-orphans  #-}
{-# language DataKinds             #-}
{-# language DeriveGeneric         #-}
{-# language FlexibleInstances     #-}
{-# language GADTs                 #-}
{-# language MultiParamTypeClasses #-}
{-# language PolyKinds             #-}
{-# language QuantifiedConstraints #-}
{-# language RankNTypes            #-}
{-# language TypeFamilies          #-}
{-# language TypeOperators         #-}
{-# language UnboxedTuples         #-}
{-# language UndecidableInstances  #-}
module Generics.Kind.Examples where

import           GHC.Generics    (Generic)
import           GHC.TypeLits
import           Type.Reflection (Typeable)

import           Generics.Kind

-- Obtained from Generic

instance GenericK Maybe where
  type RepK Maybe = U1 :+: Field Var0
instance GenericK (Maybe a) where
  type RepK (Maybe a) = SubstRep (RepK Maybe) a
  fromK :: (Maybe a :@@: x) -> RepK (Maybe a) x
fromK = (Maybe a :@@: x) -> RepK (Maybe a) x
forall t k (f :: t -> k) (x :: t) (xs :: LoT k).
(GenericK f, SubstRep' (RepK f) x xs) =>
(f x :@@: xs) -> SubstRep (RepK f) x xs
fromRepK
  toK :: RepK (Maybe a) x -> Maybe a :@@: x
toK   = RepK (Maybe a) x -> Maybe a :@@: x
forall t k (f :: t -> k) (x :: t) (xs :: LoT k).
(GenericK f, SubstRep' (RepK f) x xs) =>
SubstRep (RepK f) x xs -> f x :@@: xs
toRepK

instance GenericK [] where
  type RepK [] = U1 :+: Field Var0 :*: Field ([] :$: Var0)
instance GenericK [a] where
  type RepK [a] = SubstRep (RepK []) a
  fromK :: ([a] :@@: x) -> RepK [a] x
fromK = ([a] :@@: x) -> RepK [a] x
forall t k (f :: t -> k) (x :: t) (xs :: LoT k).
(GenericK f, SubstRep' (RepK f) x xs) =>
(f x :@@: xs) -> SubstRep (RepK f) x xs
fromRepK
  toK :: RepK [a] x -> [a] :@@: x
toK   = RepK [a] x -> [a] :@@: x
forall t k (f :: t -> k) (x :: t) (xs :: LoT k).
(GenericK f, SubstRep' (RepK f) x xs) =>
SubstRep (RepK f) x xs -> f x :@@: xs
toRepK

instance GenericK Either where
  type RepK Either = Field Var0 :+: Field Var1
instance GenericK (Either a) where
  type RepK (Either a) = SubstRep (RepK Either) a
  fromK :: (Either a :@@: x) -> RepK (Either a) x
fromK = (Either a :@@: x) -> RepK (Either a) x
forall t k (f :: t -> k) (x :: t) (xs :: LoT k).
(GenericK f, SubstRep' (RepK f) x xs) =>
(f x :@@: xs) -> SubstRep (RepK f) x xs
fromRepK
  toK :: RepK (Either a) x -> Either a :@@: x
toK   = RepK (Either a) x -> Either a :@@: x
forall t k (f :: t -> k) (x :: t) (xs :: LoT k).
(GenericK f, SubstRep' (RepK f) x xs) =>
SubstRep (RepK f) x xs -> f x :@@: xs
toRepK
instance GenericK (Either a b) where
  type RepK (Either a b) = SubstRep (RepK (Either a)) b
  fromK :: (Either a b :@@: x) -> RepK (Either a b) x
fromK = (Either a b :@@: x) -> RepK (Either a b) x
forall t k (f :: t -> k) (x :: t) (xs :: LoT k).
(GenericK f, SubstRep' (RepK f) x xs) =>
(f x :@@: xs) -> SubstRep (RepK f) x xs
fromRepK
  toK :: RepK (Either a b) x -> Either a b :@@: x
toK   = RepK (Either a b) x -> Either a b :@@: x
forall t k (f :: t -> k) (x :: t) (xs :: LoT k).
(GenericK f, SubstRep' (RepK f) x xs) =>
SubstRep (RepK f) x xs -> f x :@@: xs
toRepK

-- From the docs

data Tree a = Branch (Tree a) (Tree a) | Leaf a
            deriving (forall x. Tree a -> Rep (Tree a) x)
-> (forall x. Rep (Tree a) x -> Tree a) -> Generic (Tree a)
forall x. Rep (Tree a) x -> Tree a
forall x. Tree a -> Rep (Tree a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Tree a) x -> Tree a
forall a x. Tree a -> Rep (Tree a) x
$cto :: forall a x. Rep (Tree a) x -> Tree a
$cfrom :: forall a x. Tree a -> Rep (Tree a) x
Generic

instance GenericK Tree where
  type RepK Tree = Field (Tree :$: Var0) :*: Field (Tree :$: Var0) :+: Field Var0
instance GenericK (Tree a) where
  type RepK (Tree a) = SubstRep (RepK Tree) a
  fromK :: (Tree a :@@: x) -> RepK (Tree a) x
fromK = (Tree a :@@: x) -> RepK (Tree a) x
forall t k (f :: t -> k) (x :: t) (xs :: LoT k).
(GenericK f, SubstRep' (RepK f) x xs) =>
(f x :@@: xs) -> SubstRep (RepK f) x xs
fromRepK
  toK :: RepK (Tree a) x -> Tree a :@@: x
toK   = RepK (Tree a) x -> Tree a :@@: x
forall t k (f :: t -> k) (x :: t) (xs :: LoT k).
(GenericK f, SubstRep' (RepK f) x xs) =>
SubstRep (RepK f) x xs -> f x :@@: xs
toRepK

-- Data family

data family HappyFamily t
data instance HappyFamily (Maybe a) = HFM Bool
data instance HappyFamily [a]       = HFL a

instance GenericK HappyFamily where
  type RepK HappyFamily = TypeError ('Text "Cannot describe this family uniformly")
  fromK :: (HappyFamily :@@: x) -> RepK HappyFamily x
fromK = (HappyFamily :@@: x) -> RepK HappyFamily x
forall a. HasCallStack => a
undefined
  toK :: RepK HappyFamily x -> HappyFamily :@@: x
toK   = RepK HappyFamily x -> HappyFamily :@@: x
forall a. HasCallStack => a
undefined

instance GenericK (HappyFamily (Maybe a)) where
  type RepK (HappyFamily (Maybe a)) = Field ('Kon Bool)
  fromK :: (HappyFamily (Maybe a) :@@: x) -> RepK (HappyFamily (Maybe a)) x
fromK (HFM   x) = Interpret ('Kon Bool) x -> Field ('Kon Bool) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Bool
Interpret ('Kon Bool) x
x
  toK :: RepK (HappyFamily (Maybe a)) x -> HappyFamily (Maybe a) :@@: x
toK   (Field x) = Bool -> HappyFamily (Maybe a)
forall a. Bool -> HappyFamily (Maybe a)
HFM   Bool
Interpret ('Kon Bool) x
x

instance GenericK (HappyFamily [a]) where
  type RepK (HappyFamily [a]) = Field ('Kon a)
  fromK :: (HappyFamily [a] :@@: x) -> RepK (HappyFamily [a]) x
fromK (HFL   x) = Interpret ('Kon a) x -> Field ('Kon a) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field a
Interpret ('Kon a) x
x
  toK :: RepK (HappyFamily [a]) x -> HappyFamily [a] :@@: x
toK   (Field x) = a -> HappyFamily [a]
forall a. a -> HappyFamily [a]
HFL   a
Interpret ('Kon a) x
x

-- Hand-written instance

data SimpleIndex :: * -> * -> * where
  MkSimpleIndex :: [a] -> SimpleIndex [a] b

instance GenericK SimpleIndex where
  type RepK SimpleIndex
    = Exists (*) ((Var1 :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
  fromK :: (SimpleIndex :@@: x) -> RepK SimpleIndex x
fromK (MkSimpleIndex x) = (:=>:) (Var1 :~: ([] :$: Var0)) (Field ([] :$: Var0)) (a ':&&: x)
-> Exists * ((Var1 :~: ([] :$: Var0)) :=>: Field ([] :$: Var0)) x
forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists (Field ([] :$: Var0) (a ':&&: x)
-> (:=>:)
     (Var1 :~: ([] :$: Var0)) (Field ([] :$: Var0)) (a ':&&: x)
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (Interpret ([] :$: Var0) (a ':&&: x)
-> Field ([] :$: Var0) (a ':&&: x)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field [a]
Interpret ([] :$: Var0) (a ':&&: x)
x))
  toK :: RepK SimpleIndex x -> SimpleIndex :@@: x
toK (Exists (SuchThat (Field x))) = [t] -> SimpleIndex [t] (HeadLoT (TailLoT x))
forall a b. [a] -> SimpleIndex [a] b
MkSimpleIndex [t]
Interpret ([] :$: Var0) (t ':&&: x)
x

instance GenericK (SimpleIndex a) where
  type RepK (SimpleIndex a)
    = Exists (*) (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
  fromK :: (SimpleIndex a :@@: x) -> RepK (SimpleIndex a) x
fromK (MkSimpleIndex x) = (:=>:)
  ('Kon [a] :~: ([] :$: Var0)) (Field ([] :$: Var0)) (a ':&&: x)
-> Exists
     * (('Kon [a] :~: ([] :$: Var0)) :=>: Field ([] :$: Var0)) x
forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists (Field ([] :$: Var0) (a ':&&: x)
-> (:=>:)
     ('Kon [a] :~: ([] :$: Var0)) (Field ([] :$: Var0)) (a ':&&: x)
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (Interpret ([] :$: Var0) (a ':&&: x)
-> Field ([] :$: Var0) (a ':&&: x)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field [a]
Interpret ([] :$: Var0) (a ':&&: x)
x))
  toK :: RepK (SimpleIndex a) x -> SimpleIndex a :@@: x
toK (Exists (SuchThat (Field x))) = [t] -> SimpleIndex [t] (HeadLoT x)
forall a b. [a] -> SimpleIndex [a] b
MkSimpleIndex [t]
Interpret ([] :$: Var0) (t ':&&: x)
x

instance GenericK (SimpleIndex a b) where
  type RepK (SimpleIndex a b)
    = Exists (*) (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
  fromK :: (SimpleIndex a b :@@: x) -> RepK (SimpleIndex a b) x
fromK (MkSimpleIndex x) = (:=>:)
  ('Kon [a] :~: ([] :$: Var0)) (Field ([] :$: Var0)) (a ':&&: x)
-> Exists
     * (('Kon [a] :~: ([] :$: Var0)) :=>: Field ([] :$: Var0)) x
forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists (Field ([] :$: Var0) (a ':&&: x)
-> (:=>:)
     ('Kon [a] :~: ([] :$: Var0)) (Field ([] :$: Var0)) (a ':&&: x)
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (Interpret ([] :$: Var0) (a ':&&: x)
-> Field ([] :$: Var0) (a ':&&: x)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field [a]
Interpret ([] :$: Var0) (a ':&&: x)
x))
  toK :: RepK (SimpleIndex a b) x -> SimpleIndex a b :@@: x
toK (Exists (SuchThat (Field x))) = [t] -> SimpleIndex [t] b
forall a b. [a] -> SimpleIndex [a] b
MkSimpleIndex [t]
Interpret ([] :$: Var0) (t ':&&: x)
x

data WeirdTree a where
  WeirdBranch :: WeirdTree a -> WeirdTree a -> WeirdTree a
  WeirdLeaf   :: Show a => t -> a -> WeirdTree a

instance GenericK WeirdTree where
  type RepK WeirdTree
    = Field (WeirdTree :$: Var0) :*: Field (WeirdTree :$: Var0)
      :+: Exists (*) ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1))

  fromK :: (WeirdTree :@@: x) -> RepK WeirdTree x
fromK (WeirdBranch l r) = (:*:) (Field (WeirdTree :$: Var0)) (Field (WeirdTree :$: Var0)) x
-> (:+:)
     (Field (WeirdTree :$: Var0) :*: Field (WeirdTree :$: Var0))
     (Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)))
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 ((:*:) (Field (WeirdTree :$: Var0)) (Field (WeirdTree :$: Var0)) x
 -> (:+:)
      (Field (WeirdTree :$: Var0) :*: Field (WeirdTree :$: Var0))
      (Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)))
      x)
-> (:*:)
     (Field (WeirdTree :$: Var0)) (Field (WeirdTree :$: Var0)) x
-> (:+:)
     (Field (WeirdTree :$: Var0) :*: Field (WeirdTree :$: Var0))
     (Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)))
     x
forall a b. (a -> b) -> a -> b
$                     Interpret (WeirdTree :$: Var0) x -> Field (WeirdTree :$: Var0) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret (WeirdTree :$: Var0) x
WeirdTree (HeadLoT x)
l Field (WeirdTree :$: Var0) x
-> Field (WeirdTree :$: Var0) x
-> (:*:)
     (Field (WeirdTree :$: Var0)) (Field (WeirdTree :$: Var0)) x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Interpret (WeirdTree :$: Var0) x -> Field (WeirdTree :$: Var0) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret (WeirdTree :$: Var0) x
WeirdTree (HeadLoT x)
r
  fromK (WeirdLeaf   a x) = Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)) x
-> (:+:)
     (Field (WeirdTree :$: Var0) :*: Field (WeirdTree :$: Var0))
     (Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)))
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)) x
 -> (:+:)
      (Field (WeirdTree :$: Var0) :*: Field (WeirdTree :$: Var0))
      (Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)))
      x)
-> Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)) x
-> (:+:)
     (Field (WeirdTree :$: Var0) :*: Field (WeirdTree :$: Var0))
     (Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)))
     x
forall a b. (a -> b) -> a -> b
$ (:=>:) (Show :$: Var1) (Field Var0 :*: Field Var1) (t ':&&: x)
-> Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)) x
forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists ((:=>:) (Show :$: Var1) (Field Var0 :*: Field Var1) (t ':&&: x)
 -> Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)) x)
-> (:=>:) (Show :$: Var1) (Field Var0 :*: Field Var1) (t ':&&: x)
-> Exists * ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1)) x
forall a b. (a -> b) -> a -> b
$ (:*:) (Field Var0) (Field Var1) (t ':&&: x)
-> (:=>:) (Show :$: Var1) (Field Var0 :*: Field Var1) (t ':&&: x)
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat ((:*:) (Field Var0) (Field Var1) (t ':&&: x)
 -> (:=>:) (Show :$: Var1) (Field Var0 :*: Field Var1) (t ':&&: x))
-> (:*:) (Field Var0) (Field Var1) (t ':&&: x)
-> (:=>:) (Show :$: Var1) (Field Var0 :*: Field Var1) (t ':&&: x)
forall a b. (a -> b) -> a -> b
$ Interpret Var0 (t ':&&: x) -> Field Var0 (t ':&&: x)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field t
Interpret Var0 (t ':&&: x)
a Field Var0 (t ':&&: x)
-> Field Var1 (t ':&&: x)
-> (:*:) (Field Var0) (Field Var1) (t ':&&: x)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Interpret Var1 (t ':&&: x) -> Field Var1 (t ':&&: x)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret Var1 (t ':&&: x)
HeadLoT x
x

  toK :: RepK WeirdTree x -> WeirdTree :@@: x
toK (L1 (Field l :*: Field r))                     = WeirdTree (HeadLoT x)
-> WeirdTree (HeadLoT x) -> WeirdTree (HeadLoT x)
forall a. WeirdTree a -> WeirdTree a -> WeirdTree a
WeirdBranch Interpret (WeirdTree :$: Var0) x
WeirdTree (HeadLoT x)
l Interpret (WeirdTree :$: Var0) x
WeirdTree (HeadLoT x)
r
  toK (R1 (Exists (SuchThat (Field a :*: Field x)))) = t -> HeadLoT x -> WeirdTree (HeadLoT x)
forall a t. Show a => t -> a -> WeirdTree a
WeirdLeaf t
Interpret Var0 (t ':&&: x)
a Interpret Var1 (t ':&&: x)
HeadLoT x
x

-- Hand-written instance with reflection

data WeirdTreeR a where
  WeirdBranchR :: WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a
  WeirdLeafR   :: (Show a, Eq t, Typeable t) => t -> a -> WeirdTreeR a

instance GenericK WeirdTreeR where
  type RepK WeirdTreeR
    = Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0)
      :+: Exists (*) (((Show :$: Var1) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))
                      :=>: (Field Var0 :*: Field Var1))

  fromK :: (WeirdTreeR :@@: x) -> RepK WeirdTreeR x
fromK (WeirdBranchR l r) = (:*:) (Field (WeirdTreeR :$: Var0)) (Field (WeirdTreeR :$: Var0)) x
-> (:+:)
     (Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0))
     (Exists
        *
        (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
         :=>: (Field Var0 :*: Field Var1)))
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 ((:*:)
   (Field (WeirdTreeR :$: Var0)) (Field (WeirdTreeR :$: Var0)) x
 -> (:+:)
      (Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0))
      (Exists
         *
         (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
          :=>: (Field Var0 :*: Field Var1)))
      x)
-> (:*:)
     (Field (WeirdTreeR :$: Var0)) (Field (WeirdTreeR :$: Var0)) x
-> (:+:)
     (Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0))
     (Exists
        *
        (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
         :=>: (Field Var0 :*: Field Var1)))
     x
forall a b. (a -> b) -> a -> b
$                     Interpret (WeirdTreeR :$: Var0) x -> Field (WeirdTreeR :$: Var0) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret (WeirdTreeR :$: Var0) x
WeirdTreeR (HeadLoT x)
l Field (WeirdTreeR :$: Var0) x
-> Field (WeirdTreeR :$: Var0) x
-> (:*:)
     (Field (WeirdTreeR :$: Var0)) (Field (WeirdTreeR :$: Var0)) x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Interpret (WeirdTreeR :$: Var0) x -> Field (WeirdTreeR :$: Var0) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret (WeirdTreeR :$: Var0) x
WeirdTreeR (HeadLoT x)
r
  fromK (WeirdLeafR   a x) = Exists
  *
  (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
   :=>: (Field Var0 :*: Field Var1))
  x
-> (:+:)
     (Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0))
     (Exists
        *
        (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
         :=>: (Field Var0 :*: Field Var1)))
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Exists
   *
   (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
    :=>: (Field Var0 :*: Field Var1))
   x
 -> (:+:)
      (Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0))
      (Exists
         *
         (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
          :=>: (Field Var0 :*: Field Var1)))
      x)
-> Exists
     *
     (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
      :=>: (Field Var0 :*: Field Var1))
     x
-> (:+:)
     (Field (WeirdTreeR :$: Var0) :*: Field (WeirdTreeR :$: Var0))
     (Exists
        *
        (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
         :=>: (Field Var0 :*: Field Var1)))
     x
forall a b. (a -> b) -> a -> b
$ (:=>:)
  ((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
  (Field Var0 :*: Field Var1)
  (t ':&&: x)
-> Exists
     *
     (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
      :=>: (Field Var0 :*: Field Var1))
     x
forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists ((:=>:)
   ((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
   (Field Var0 :*: Field Var1)
   (t ':&&: x)
 -> Exists
      *
      (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
       :=>: (Field Var0 :*: Field Var1))
      x)
-> (:=>:)
     ((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
     (Field Var0 :*: Field Var1)
     (t ':&&: x)
-> Exists
     *
     (((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
      :=>: (Field Var0 :*: Field Var1))
     x
forall a b. (a -> b) -> a -> b
$ (:*:) (Field Var0) (Field Var1) (t ':&&: x)
-> (:=>:)
     ((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
     (Field Var0 :*: Field Var1)
     (t ':&&: x)
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat ((:*:) (Field Var0) (Field Var1) (t ':&&: x)
 -> (:=>:)
      ((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
      (Field Var0 :*: Field Var1)
      (t ':&&: x))
-> (:*:) (Field Var0) (Field Var1) (t ':&&: x)
-> (:=>:)
     ((Show :$: Var1) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
     (Field Var0 :*: Field Var1)
     (t ':&&: x)
forall a b. (a -> b) -> a -> b
$ Interpret Var0 (t ':&&: x) -> Field Var0 (t ':&&: x)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field t
Interpret Var0 (t ':&&: x)
a Field Var0 (t ':&&: x)
-> Field Var1 (t ':&&: x)
-> (:*:) (Field Var0) (Field Var1) (t ':&&: x)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Interpret Var1 (t ':&&: x) -> Field Var1 (t ':&&: x)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret Var1 (t ':&&: x)
HeadLoT x
x

  toK :: RepK WeirdTreeR x -> WeirdTreeR :@@: x
toK (L1 (Field l :*: Field r))                     = WeirdTreeR (HeadLoT x)
-> WeirdTreeR (HeadLoT x) -> WeirdTreeR (HeadLoT x)
forall a. WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a
WeirdBranchR Interpret (WeirdTreeR :$: Var0) x
WeirdTreeR (HeadLoT x)
l Interpret (WeirdTreeR :$: Var0) x
WeirdTreeR (HeadLoT x)
r
  toK (R1 (Exists (SuchThat (Field a :*: Field x)))) = t -> HeadLoT x -> WeirdTreeR (HeadLoT x)
forall a t. (Show a, Eq t, Typeable t) => t -> a -> WeirdTreeR a
WeirdLeafR t
Interpret Var0 (t ':&&: x)
a Interpret Var1 (t ':&&: x)
HeadLoT x
x

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)))

  fromK :: (WeirdTreeR a :@@: x) -> RepK (WeirdTreeR a) x
fromK (WeirdBranchR l r) = (:*:) (Field ('Kon (WeirdTreeR a))) (Field ('Kon (WeirdTreeR a))) x
-> (:+:)
     (Field ('Kon (WeirdTreeR a)) :*: Field ('Kon (WeirdTreeR a)))
     (Exists
        *
        (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
         :=>: (Field Var0 :*: Field ('Kon a))))
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 ((:*:)
   (Field ('Kon (WeirdTreeR a))) (Field ('Kon (WeirdTreeR a))) x
 -> (:+:)
      (Field ('Kon (WeirdTreeR a)) :*: Field ('Kon (WeirdTreeR a)))
      (Exists
         *
         (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
          :=>: (Field Var0 :*: Field ('Kon a))))
      x)
-> (:*:)
     (Field ('Kon (WeirdTreeR a))) (Field ('Kon (WeirdTreeR a))) x
-> (:+:)
     (Field ('Kon (WeirdTreeR a)) :*: Field ('Kon (WeirdTreeR a)))
     (Exists
        *
        (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
         :=>: (Field Var0 :*: Field ('Kon a))))
     x
forall a b. (a -> b) -> a -> b
$                     Interpret ('Kon (WeirdTreeR a)) x -> Field ('Kon (WeirdTreeR a)) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret ('Kon (WeirdTreeR a)) x
WeirdTreeR a
l Field ('Kon (WeirdTreeR a)) x
-> Field ('Kon (WeirdTreeR a)) x
-> (:*:)
     (Field ('Kon (WeirdTreeR a))) (Field ('Kon (WeirdTreeR a))) x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Interpret ('Kon (WeirdTreeR a)) x -> Field ('Kon (WeirdTreeR a)) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret ('Kon (WeirdTreeR a)) x
WeirdTreeR a
r
  fromK (WeirdLeafR   a x) = Exists
  *
  (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
   :=>: (Field Var0 :*: Field ('Kon a)))
  x
-> (:+:)
     (Field ('Kon (WeirdTreeR a)) :*: Field ('Kon (WeirdTreeR a)))
     (Exists
        *
        (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
         :=>: (Field Var0 :*: Field ('Kon a))))
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Exists
   *
   (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
    :=>: (Field Var0 :*: Field ('Kon a)))
   x
 -> (:+:)
      (Field ('Kon (WeirdTreeR a)) :*: Field ('Kon (WeirdTreeR a)))
      (Exists
         *
         (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
          :=>: (Field Var0 :*: Field ('Kon a))))
      x)
-> Exists
     *
     (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
      :=>: (Field Var0 :*: Field ('Kon a)))
     x
-> (:+:)
     (Field ('Kon (WeirdTreeR a)) :*: Field ('Kon (WeirdTreeR a)))
     (Exists
        *
        (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
         :=>: (Field Var0 :*: Field ('Kon a))))
     x
forall a b. (a -> b) -> a -> b
$ (:=>:)
  ('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
  (Field Var0 :*: Field ('Kon a))
  (t ':&&: x)
-> Exists
     *
     (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
      :=>: (Field Var0 :*: Field ('Kon a)))
     x
forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists ((:=>:)
   ('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
   (Field Var0 :*: Field ('Kon a))
   (t ':&&: x)
 -> Exists
      *
      (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
       :=>: (Field Var0 :*: Field ('Kon a)))
      x)
-> (:=>:)
     ('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
     (Field Var0 :*: Field ('Kon a))
     (t ':&&: x)
-> Exists
     *
     (('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
      :=>: (Field Var0 :*: Field ('Kon a)))
     x
forall a b. (a -> b) -> a -> b
$ (:*:) (Field Var0) (Field ('Kon a)) (t ':&&: x)
-> (:=>:)
     ('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
     (Field Var0 :*: Field ('Kon a))
     (t ':&&: x)
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat ((:*:) (Field Var0) (Field ('Kon a)) (t ':&&: x)
 -> (:=>:)
      ('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
      (Field Var0 :*: Field ('Kon a))
      (t ':&&: x))
-> (:*:) (Field Var0) (Field ('Kon a)) (t ':&&: x)
-> (:=>:)
     ('Kon (Show a) ':&: ((Eq :$: Var0) ':&: (Typeable :$: Var0)))
     (Field Var0 :*: Field ('Kon a))
     (t ':&&: x)
forall a b. (a -> b) -> a -> b
$ Interpret Var0 (t ':&&: x) -> Field Var0 (t ':&&: x)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field t
Interpret Var0 (t ':&&: x)
a Field Var0 (t ':&&: x)
-> Field ('Kon a) (t ':&&: x)
-> (:*:) (Field Var0) (Field ('Kon a)) (t ':&&: x)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Interpret ('Kon a) (t ':&&: x) -> Field ('Kon a) (t ':&&: x)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field a
Interpret ('Kon a) (t ':&&: x)
x

  toK :: RepK (WeirdTreeR a) x -> WeirdTreeR a :@@: x
toK (L1 (Field l :*: Field r))                     = WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a
forall a. WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a
WeirdBranchR Interpret ('Kon (WeirdTreeR a)) x
WeirdTreeR a
l Interpret ('Kon (WeirdTreeR a)) x
WeirdTreeR a
r
  toK (R1 (Exists (SuchThat (Field a :*: Field x)))) = t -> a -> WeirdTreeR a
forall a t. (Show a, Eq t, Typeable t) => t -> a -> WeirdTreeR a
WeirdLeafR t
Interpret Var0 (t ':&&: x)
a a
Interpret ('Kon a) (t ':&&: x)
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 :: (TTY m a :@@: x) -> RepK (TTY m a) x
fromK (WriteTTY s) = (:=>:) ('Kon () :~: 'Kon ()) (Field ('Kon String)) x
-> (:+:)
     (('Kon () :~: 'Kon ()) :=>: Field ('Kon String))
     (('Kon () :~: 'Kon String) :=>: U1)
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (Field ('Kon String) x
-> (:=>:) ('Kon () :~: 'Kon ()) (Field ('Kon String)) x
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (Interpret ('Kon String) x -> Field ('Kon String) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field String
Interpret ('Kon String) x
s))
  fromK TTY m a :@@: x
ReadTTY      = (:=>:) ('Kon String :~: 'Kon String) U1 x
-> (:+:)
     (('Kon String :~: 'Kon ()) :=>: Field ('Kon String))
     (('Kon String :~: 'Kon String) :=>: U1)
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (U1 x -> (:=>:) ('Kon String :~: 'Kon String) U1 x
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat U1 x
forall k (p :: k). U1 p
U1)

  toK :: RepK (TTY m a) x -> TTY m a :@@: x
toK (L1 (SuchThat (Field s))) = String -> TTY m ()
forall k (m :: k). String -> TTY m ()
WriteTTY String
Interpret ('Kon String) x
s
  toK (R1 (SuchThat U1))        = TTY m a :@@: x
forall k (m :: k). TTY m String
ReadTTY

-- Weird-kinded types

data T (a :: k) where
  MkT :: forall (a :: *). 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))
  fromK :: (T :@@: x) -> RepK T x
fromK (MkT x) = (:=>:)
  ('Kon (* ~ *) ':&: (Var0 :~~: Var1))
  (Field ('Kon Maybe ':@: Var0))
  (a ':&&: x)
-> Exists
     *
     (('Kon (* ~ *) ':&: (Var0 :~~: Var1))
      :=>: Field ('Kon Maybe ':@: Var0))
     x
forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Exists (Field ('Kon Maybe ':@: Var0) (a ':&&: x)
-> (:=>:)
     ('Kon (* ~ *) ':&: (Var0 :~~: Var1))
     (Field ('Kon Maybe ':@: Var0))
     (a ':&&: x)
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (Interpret ('Kon Maybe ':@: Var0) (a ':&&: x)
-> Field ('Kon Maybe ':@: Var0) (a ':&&: x)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Maybe a
Interpret ('Kon Maybe ':@: Var0) (a ':&&: x)
x))
  toK :: RepK T x -> T :@@: x
toK (Exists (SuchThat (Field x))) = Maybe t -> T t
forall a. Maybe a -> T a
MkT Maybe t
Interpret ('Kon Maybe ':@: Var0) (t ':&&: x)
x

data P k (a :: k) where
  P :: forall k (a :: k). P k a

instance GenericK (P k) where
  type RepK (P k) = U1
  fromK :: (P k :@@: x) -> RepK (P k) x
fromK P k :@@: x
P  = RepK (P k) x
forall k (p :: k). U1 p
U1
  toK :: RepK (P k) x -> P k :@@: x
toK   RepK (P k) x
U1 = P k :@@: x
forall k (a :: k). P k a
P

{- This does not work
instance GenericK P (k :&&: a :&&: LoT0) where
  type RepK P = KindOf Var1 :~: Var0 :=>: U1
-}

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
  fromK :: (P' j :@@: x) -> RepK (P' j) x
fromK P' j :@@: x
P' = U1 x -> (:=>:) ('Kon k :~: 'Kon k) U1 x
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat U1 x
forall k (p :: k). U1 p
U1
  toK :: RepK (P' j) x -> P' j :@@: x
toK (SuchThat U1) = P' j :@@: x
forall k (a :: k). P' k a
P'

instance GenericK (P' :: * -> k -> *) where
  type RepK (P' :: * -> k -> *) = ('Kon k :~: Var0) :=>: U1
  fromK :: (P' :@@: x) -> RepK P' x
fromK P' :@@: x
P' = U1 x -> (:=>:) ('Kon k :~: Var0) U1 x
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat U1 x
forall k (p :: k). U1 p
U1
  toK :: RepK P' x -> P' :@@: x
toK (SuchThat U1) = P' :@@: x
forall k (a :: k). P' k a
P'

-- Rank-N types

newtype Ranky = MkRanky (forall a. a -> a)

instance GenericK Ranky where
  type RepK Ranky = Field ('ForAll ((->) :$: Var0 ':@: Var0))
  fromK :: (Ranky :@@: x) -> RepK Ranky x
fromK (MkRanky x) = Interpret ('ForAll (((->) :$: Var0) ':@: Var0)) x
-> Field ('ForAll (((->) :$: Var0) ':@: Var0)) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field ((forall t. Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x))
-> ForAllI (((->) :$: Var0) ':@: Var0) x
forall d1 d (f :: Atom (d1 -> d) *) (tys :: LoT d).
(forall (t :: d1). Interpret f (t ':&&: tys)) -> ForAllI f tys
ForAllI forall t. Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x)
forall a. a -> a
x)
  toK :: RepK Ranky x -> Ranky :@@: x
toK (Field (ForAllI x)) = (forall a. a -> a) -> Ranky
MkRanky forall t. Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x)
forall a. a -> a
x

newtype Ranky2 b = MkRanky2 ((forall a. a -> a) -> b)

instance GenericK Ranky2 where
  type RepK Ranky2 = Field ((->) :$: 'ForAll ((->) :$: Var0 ':@: Var0) ':@: Var0)
  fromK :: (Ranky2 :@@: x) -> RepK Ranky2 x
fromK (MkRanky2 f) = Interpret
  (((->) :$: 'ForAll (((->) :$: Var0) ':@: Var0)) ':@: Var0) x
-> Field
     (((->) :$: 'ForAll (((->) :$: Var0) ':@: Var0)) ':@: Var0) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field (\(ForAllI forall t. Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x)
x) -> (forall a. a -> a) -> HeadLoT x
f forall t. Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x)
forall a. a -> a
x)
  toK :: RepK Ranky2 x -> Ranky2 :@@: x
toK (Field f) = ((forall a. a -> a) -> HeadLoT x) -> Ranky2 (HeadLoT x)
forall b. ((forall a. a -> a) -> b) -> Ranky2 b
MkRanky2 (\forall a. a -> a
x -> Interpret
  (((->) :$: 'ForAll (((->) :$: Var0) ':@: Var0)) ':@: Var0) x
ForAllI (((->) :$: Var0) ':@: Var0) x -> HeadLoT x
f ((forall t. Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x))
-> ForAllI (((->) :$: Var0) ':@: Var0) x
forall d1 d (f :: Atom (d1 -> d) *) (tys :: LoT d).
(forall (t :: d1). Interpret f (t ':&&: tys)) -> ForAllI f tys
ForAllI forall t. Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x)
forall a. a -> a
x))

data Shower a where
  MkShower :: (Show a => a -> String) -> Shower a

instance GenericK Shower where
  type RepK Shower = Field ((Show :$: Var0) ':=>>: ((->) :$: Var0 ':@: 'Kon String))
  fromK :: (Shower :@@: x) -> RepK Shower x
fromK (MkShower f) = Interpret
  ((Show :$: Var0) ':=>>: (((->) :$: Var0) ':@: 'Kon String)) x
-> Field
     ((Show :$: Var0) ':=>>: (((->) :$: Var0) ':@: 'Kon String)) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field ((Interpret (Show :$: Var0) x =>
 Interpret (((->) :$: Var0) ':@: 'Kon String) x)
-> SuchThatI (Show :$: Var0) (((->) :$: Var0) ':@: 'Kon String) x
forall d (c :: Atom d Constraint) (tys :: LoT d) (f :: Atom d *).
(Interpret c tys => Interpret f tys) -> SuchThatI c f tys
SuchThatI Show (HeadLoT x) => HeadLoT x -> String
Interpret (Show :$: Var0) x =>
Interpret (((->) :$: Var0) ':@: 'Kon String) x
f)
  toK :: RepK Shower x -> Shower :@@: x
toK (Field (SuchThatI f)) = (Show (HeadLoT x) => HeadLoT x -> String) -> Shower (HeadLoT x)
forall a. (Show a => a -> String) -> Shower a
MkShower Show (HeadLoT x) => HeadLoT x -> String
Interpret (Show :$: Var0) x =>
Interpret (((->) :$: Var0) ':@: 'Kon String) x
f

-- Other representation types

data Unboxed1 = MkUnboxed1 (# Int, Int #)
{- -- We cannot write this
instance GenericK Unboxed1 'LoT0 where
  type RepK Unboxed1 = Field (Kon (# Int, Int #))
  -- fromK (MkUnboxed1 x) = Field x
  -- toK (Field x) = MkUnboxed1 x
  fromK = undefined
  toK   = undefined
-}