{-# 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           Data.Kind
import           GHC.Generics    (Generic)
import           GHC.TypeLits
import           Type.Reflection (Typeable)

import qualified Fcf.Core as Fcf
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 :: forall (x :: LoT (*)). (Maybe a :@@: x) -> RepK (Maybe a) x
fromK = (Maybe a :@@: x) -> SubstRep (RepK Maybe) a x
(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 :: forall (x :: LoT (*)). RepK (Maybe a) x -> Maybe a :@@: x
toK   = SubstRep (RepK Maybe) a x -> Maybe a :@@: x
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 :: forall (x :: LoT (*)). ([a] :@@: x) -> RepK [a] x
fromK = ([a] :@@: x) -> SubstRep (RepK []) a x
([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 :: forall (x :: LoT (*)). RepK [a] x -> [a] :@@: x
toK   = SubstRep (RepK []) a x -> [a] :@@: x
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 :: forall (x :: LoT (* -> *)). (Either a :@@: x) -> RepK (Either a) x
fromK = (Either a :@@: x) -> SubstRep (RepK Either) a x
(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 :: forall (x :: LoT (* -> *)). RepK (Either a) x -> Either a :@@: x
toK   = SubstRep (RepK Either) a x -> Either a :@@: x
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 :: forall (x :: LoT (*)). (Either a b :@@: x) -> RepK (Either a b) x
fromK = (Either a b :@@: x) -> SubstRep (RepK (Either a)) b x
(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 :: forall (x :: LoT (*)). RepK (Either a b) x -> Either a b :@@: x
toK   = SubstRep (RepK (Either a)) b x -> Either a b :@@: x
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
$cfrom :: forall a x. Tree a -> Rep (Tree a) x
from :: forall x. Tree a -> Rep (Tree a) x
$cto :: forall a x. Rep (Tree a) x -> Tree a
to :: forall x. Rep (Tree a) x -> Tree a
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 :: forall (x :: LoT (*)). (Tree a :@@: x) -> RepK (Tree a) x
fromK = (Tree a :@@: x) -> SubstRep (RepK Tree) a x
(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 :: forall (x :: LoT (*)). RepK (Tree a) x -> Tree a :@@: x
toK   = SubstRep (RepK Tree) a x -> Tree a :@@: x
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 :: forall (x :: LoT (* -> *)).
(HappyFamily :@@: x) -> RepK HappyFamily x
fromK = (HappyFamily :@@: x) -> RepK HappyFamily x
HappyFamily (HeadLoT x) -> (TypeError ...)
forall a. HasCallStack => a
undefined
  toK :: forall (x :: LoT (* -> *)).
RepK HappyFamily x -> HappyFamily :@@: x
toK   = (TypeError ...) -> HappyFamily (HeadLoT x)
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 :: forall (x :: LoT (*)).
(HappyFamily (Maybe a) :@@: x) -> RepK (HappyFamily (Maybe a)) x
fromK (HFM   Bool
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 :: forall (x :: LoT (*)).
RepK (HappyFamily (Maybe a)) x -> HappyFamily (Maybe a) :@@: x
toK   (Field Interpret ('Kon Bool) x
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 :: forall (x :: LoT (*)).
(HappyFamily [a] :@@: x) -> RepK (HappyFamily [a]) x
fromK (HFL   a
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 :: forall (x :: LoT (*)).
RepK (HappyFamily [a]) x -> HappyFamily [a] :@@: x
toK   (Field Interpret ('Kon a) x
x) = a -> HappyFamily [a]
forall a. a -> HappyFamily [a]
HFL   a
Interpret ('Kon a) x
x

-- Hand-written instance

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

instance GenericK SimpleIndex where
  type RepK SimpleIndex
    = Exists Type ((Var1 :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
  fromK :: forall (x :: LoT (* -> * -> *)).
(SimpleIndex :@@: x) -> RepK SimpleIndex x
fromK (MkSimpleIndex [a]
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 :: forall (x :: LoT (* -> * -> *)).
RepK SimpleIndex x -> SimpleIndex :@@: x
toK (Exists (SuchThat (Field Interpret ([] :$: Var0) (t ':&&: x)
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 Type (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
  fromK :: forall (x :: LoT (* -> *)).
(SimpleIndex a :@@: x) -> RepK (SimpleIndex a) x
fromK (MkSimpleIndex [a]
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 :: forall (x :: LoT (* -> *)).
RepK (SimpleIndex a) x -> SimpleIndex a :@@: x
toK (Exists (SuchThat (Field Interpret ([] :$: Var0) (t ':&&: x)
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 Type (('Kon a :~: ([] :$: Var0)) :=>: Field ([] :$: Var0))
  fromK :: forall (x :: LoT (*)).
(SimpleIndex a b :@@: x) -> RepK (SimpleIndex a b) x
fromK (MkSimpleIndex [a]
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 :: forall (x :: LoT (*)).
RepK (SimpleIndex a b) x -> SimpleIndex a b :@@: x
toK (Exists (SuchThat (Field Interpret ([] :$: Var0) (t ':&&: x)
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 Type ((Show :$: Var1) :=>: (Field Var0 :*: Field Var1))

  fromK :: forall (x :: LoT (* -> *)). (WeirdTree :@@: x) -> RepK WeirdTree x
fromK (WeirdBranch WeirdTree (HeadLoT x)
l WeirdTree (HeadLoT x)
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   t
a HeadLoT x
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 HeadLoT x
Interpret Var1 (t ':&&: x)
x

  toK :: forall (x :: LoT (* -> *)). RepK WeirdTree x -> WeirdTree :@@: x
toK (L1 (Field Interpret (WeirdTree :$: Var0) x
l :*: Field Interpret (WeirdTree :$: Var0) x
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 Interpret Var0 (t ':&&: x)
a :*: Field Interpret Var1 (t ':&&: x)
x)))) = t -> HeadLoT x -> WeirdTree (HeadLoT x)
forall a a. Show a => a -> a -> WeirdTree a
WeirdLeaf t
Interpret Var0 (t ':&&: x)
a HeadLoT x
Interpret Var1 (t ':&&: 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 Type (((Show :$: Var1) ':&: (Eq :$: Var0) ':&: (Typeable :$: Var0))
                       :=>: (Field Var0 :*: Field Var1))

  fromK :: forall (x :: LoT (* -> *)).
(WeirdTreeR :@@: x) -> RepK WeirdTreeR x
fromK (WeirdBranchR WeirdTreeR (HeadLoT x)
l WeirdTreeR (HeadLoT x)
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   t
a HeadLoT x
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 HeadLoT x
Interpret Var1 (t ':&&: x)
x

  toK :: forall (x :: LoT (* -> *)). RepK WeirdTreeR x -> WeirdTreeR :@@: x
toK (L1 (Field Interpret (WeirdTreeR :$: Var0) x
l :*: Field Interpret (WeirdTreeR :$: Var0) x
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 Interpret Var0 (t ':&&: x)
a :*: Field Interpret Var1 (t ':&&: x)
x)))) = t -> HeadLoT x -> WeirdTreeR (HeadLoT x)
forall a a. (Show a, Eq a, Typeable a) => a -> a -> WeirdTreeR a
WeirdLeafR t
Interpret Var0 (t ':&&: x)
a HeadLoT x
Interpret Var1 (t ':&&: x)
x

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

  fromK :: forall (x :: LoT (*)).
(WeirdTreeR a :@@: x) -> RepK (WeirdTreeR a) x
fromK (WeirdBranchR WeirdTreeR a
l WeirdTreeR a
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   t
a 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 :: forall (x :: LoT (*)). RepK (WeirdTreeR a) x -> WeirdTreeR a :@@: x
toK (L1 (Field Interpret ('Kon (WeirdTreeR a)) x
l :*: Field Interpret ('Kon (WeirdTreeR a)) x
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 Interpret Var0 (t ':&&: x)
a :*: Field Interpret ('Kon a) (t ':&&: x)
x)))) = t -> a -> WeirdTreeR a
forall a a. (Show a, Eq a, Typeable a) => a -> 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 :: forall (x :: LoT (*)). (TTY m a :@@: x) -> RepK (TTY m a) x
fromK (WriteTTY String
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
TTY m a
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 :: forall (x :: LoT (*)). RepK (TTY m a) x -> TTY m a :@@: x
toK (L1 (SuchThat (Field Interpret ('Kon String) x
s))) = String -> TTY m ()
forall {k} (m :: k). String -> TTY m ()
WriteTTY String
Interpret ('Kon String) x
s
  toK (R1 (SuchThat U1 x
U1))        = TTY m a :@@: x
TTY m String
forall {k} (m :: k). TTY m String
ReadTTY

-- Weird-kinded types

data T (a :: k) where
  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 -> Type) where
  type RepK (T :: k -> Type) =
    Exists Type (('Kon (k ~ Type) ':&: (Var0 :~~: Var1)) :=>: Field (Maybe :$: Var0))
  fromK :: forall (x :: LoT (k -> *)). (T :@@: x) -> RepK T x
fromK (MkT Maybe a
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 :: forall (x :: LoT (k -> *)). RepK T x -> T :@@: x
toK (Exists (SuchThat (Field Interpret ('Kon Maybe ':@: Var0) (t ':&&: x)
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 :: forall (x :: LoT (k -> *)). (P k :@@: x) -> RepK (P k) x
fromK P k :@@: x
P k (HeadLoT x)
P  = U1 x
RepK (P k) x
forall k (p :: k). U1 p
U1
  toK :: forall (x :: LoT (k -> *)). RepK (P k) x -> P k :@@: x
toK   U1 x
RepK (P k) x
U1 = P k :@@: x
P k (HeadLoT 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 -> Type) where
  type RepK (P' j :: k -> Type) = ('Kon k :~: 'Kon j) :=>: U1
  fromK :: forall (x :: LoT (k -> *)). (P' j :@@: x) -> RepK (P' j) x
fromK P' j :@@: x
P' j (HeadLoT 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 :: forall (x :: LoT (k -> *)). RepK (P' j) x -> P' j :@@: x
toK (SuchThat U1 x
U1) = P' j :@@: x
P' j (HeadLoT x)
forall k (a :: k). P' k a
P'

instance GenericK (P' :: Type -> k -> Type) where
  type RepK (P' :: Type -> k -> Type) = ('Kon k :~: Var0) :=>: U1
  fromK :: forall (x :: LoT (* -> k -> *)). (P' :@@: x) -> RepK P' x
fromK P' :@@: x
P' (HeadLoT x) (HeadLoT (TailLoT 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 :: forall (x :: LoT (* -> k -> *)). RepK P' x -> P' :@@: x
toK (SuchThat U1 x
U1) = P' :@@: x
P' k (HeadLoT (TailLoT 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 :: forall (x :: LoT (*)). (Ranky :@@: x) -> RepK Ranky x
fromK (MkRanky forall a. a -> a
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 Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x)
t -> t
forall t. Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x)
forall a. a -> a
x)
  toK :: forall (x :: LoT (*)). RepK Ranky x -> Ranky :@@: x
toK (Field (ForAllI forall t. Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x)
x)) = (forall a. a -> a) -> Ranky
MkRanky Interpret (((->) :$: Var0) ':@: Var0) (a ':&&: x)
a -> a
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 :: forall (x :: LoT (* -> *)). (Ranky2 :@@: x) -> RepK Ranky2 x
fromK (MkRanky2 (forall a. a -> a) -> HeadLoT x
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 Interpret (((->) :$: Var0) ':@: Var0) (a ':&&: x)
a -> a
forall t. Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x)
forall a. a -> a
x)
  toK :: forall (x :: LoT (* -> *)). RepK Ranky2 x -> Ranky2 :@@: x
toK (Field Interpret
  (((->) :$: 'ForAll (((->) :$: Var0) ':@: Var0)) ':@: Var0) x
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 Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x)
t -> t
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 :: forall (x :: LoT (* -> *)). (Shower :@@: x) -> RepK Shower x
fromK (MkShower Show (HeadLoT x) => HeadLoT x -> String
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 Interpret (((->) :$: Var0) ':@: 'Kon String) x
Show (HeadLoT x) => HeadLoT x -> String
HeadLoT x -> String
Interpret (Show :$: Var0) x =>
Interpret (((->) :$: Var0) ':@: 'Kon String) x
f)
  toK :: forall (x :: LoT (* -> *)). RepK Shower x -> Shower :@@: x
toK (Field (SuchThatI Interpret (Show :$: Var0) x =>
Interpret (((->) :$: Var0) ':@: 'Kon String) x
f)) = (Show (HeadLoT x) => HeadLoT x -> String) -> Shower (HeadLoT x)
forall a. (Show a => a -> String) -> Shower a
MkShower Interpret (((->) :$: Var0) ':@: 'Kon String) x
Show (HeadLoT x) => HeadLoT x -> String
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
-}

-- Type families

-- HKD pattern, defunctionalized variant
newtype Hkd f a = Hkd (Fcf.Eval (f a))

-- Simplified encoding compared to kind-generics-th.
-- Fcf.Eval in Hkd could be any other type family, so a general
-- implementation would have to defunctionalize it.
instance GenericK Hkd where
  type RepK Hkd = Field (Eval (Var0 :@: Var1))
  fromK :: forall (x :: LoT ((k -> * -> *) -> k -> *)).
(Hkd :@@: x) -> RepK Hkd x
fromK (Hkd Eval (HeadLoT x (HeadLoT (TailLoT x)))
x) = Interpret ('Eval (Var0 ':@: Var1)) x
-> Field ('Eval (Var0 ':@: Var1)) x
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Eval (HeadLoT x (HeadLoT (TailLoT x)))
Interpret ('Eval (Var0 ':@: Var1)) x
x
  toK :: forall (x :: LoT ((k -> * -> *) -> k -> *)).
RepK Hkd x -> Hkd :@@: x
toK (Field Interpret ('Eval (Var0 ':@: Var1)) x
x) = Eval (HeadLoT x (HeadLoT (TailLoT x)))
-> Hkd (HeadLoT x) (HeadLoT (TailLoT x))
forall {k} (f :: k -> * -> *) (a :: k). Eval (f a) -> Hkd f a
Hkd Eval (HeadLoT x (HeadLoT (TailLoT x)))
Interpret ('Eval (Var0 ':@: Var1)) x
x

instance GenericK (Hkd f) where
  type RepK (Hkd f) = Field (Eval (Kon f :@: Var0))
  fromK :: forall (x :: LoT (k -> *)). (Hkd f :@@: x) -> RepK (Hkd f) x
fromK (Hkd Eval (f (HeadLoT x))
x) = Interpret ('Eval ('Kon f ':@: Var0)) x
-> Field ('Eval ('Kon f ':@: Var0)) x
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Eval (f (HeadLoT x))
Interpret ('Eval ('Kon f ':@: Var0)) x
x
  toK :: forall (x :: LoT (k -> *)). RepK (Hkd f) x -> Hkd f :@@: x
toK (Field Interpret ('Eval ('Kon f ':@: Var0)) x
x) = Eval (f (HeadLoT x)) -> Hkd f (HeadLoT x)
forall {k} (f :: k -> * -> *) (a :: k). Eval (f a) -> Hkd f a
Hkd Eval (f (HeadLoT x))
Interpret ('Eval ('Kon f ':@: Var0)) x
x

instance GenericK (Hkd f a) where
  type RepK (Hkd f a) = Field (Kon (Fcf.Eval (f a)))
  fromK :: forall (x :: LoT (*)). (Hkd f a :@@: x) -> RepK (Hkd f a) x
fromK (Hkd Eval (f a)
x) = Interpret ('Kon (Eval (f a))) x -> Field ('Kon (Eval (f a))) x
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Eval (f a)
Interpret ('Kon (Eval (f a))) x
x
  toK :: forall (x :: LoT (*)). RepK (Hkd f a) x -> Hkd f a :@@: x
toK (Field Interpret ('Kon (Eval (f a))) x
x) = Eval (f a) -> Hkd f a
forall {k} (f :: k -> * -> *) (a :: k). Eval (f a) -> Hkd f a
Hkd Eval (f a)
Interpret ('Kon (Eval (f a))) x
x