{-# 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 = 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   = 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 = 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   = 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 = 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   = 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 = 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   = 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 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 :: forall (x :: LoT (*)). (Tree a :@@: x) -> RepK (Tree a) x
fromK = 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   = 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 = forall a. HasCallStack => a
undefined
  toK :: forall (x :: LoT (* -> *)).
RepK HappyFamily x -> HappyFamily :@@: x
toK   = 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) = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Bool
x
  toK :: forall (x :: LoT (*)).
RepK (HappyFamily (Maybe a)) x -> HappyFamily (Maybe a) :@@: x
toK   (Field Interpret ('Kon Bool) x
x) = forall a. Bool -> HappyFamily (Maybe a)
HFM   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) = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field a
x
  toK :: forall (x :: LoT (*)).
RepK (HappyFamily [a]) x -> HappyFamily [a] :@@: x
toK   (Field Interpret ('Kon a) x
x) = forall a. a -> HappyFamily [a]
HFL   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) = forall k (a :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (a ':&&: x) -> Exists k f x
Exists (forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field [a]
x))
  toK :: forall (x :: LoT (* -> * -> *)).
RepK SimpleIndex x -> SimpleIndex :@@: x
toK (Exists (SuchThat (Field Interpret ([] :$: Var0) (t ':&&: x)
x))) = forall a b. [a] -> SimpleIndex [a] b
MkSimpleIndex 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) = forall k (a :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (a ':&&: x) -> Exists k f x
Exists (forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field [a]
x))
  toK :: forall (x :: LoT (* -> *)).
RepK (SimpleIndex a) x -> SimpleIndex a :@@: x
toK (Exists (SuchThat (Field Interpret ([] :$: Var0) (t ':&&: x)
x))) = forall a b. [a] -> SimpleIndex [a] b
MkSimpleIndex 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) = forall k (a :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (a ':&&: x) -> Exists k f x
Exists (forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field [a]
x))
  toK :: forall (x :: LoT (*)).
RepK (SimpleIndex a b) x -> SimpleIndex a b :@@: x
toK (Exists (SuchThat (Field Interpret ([] :$: Var0) (t ':&&: x)
x))) = forall a b. [a] -> SimpleIndex [a] b
MkSimpleIndex 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) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall a b. (a -> b) -> a -> b
$                     forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field WeirdTree (HeadLoT x)
l forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field WeirdTree (HeadLoT x)
r
  fromK (WeirdLeaf   t
a HeadLoT x
x) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ forall k (a :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (a ':&&: x) -> Exists k f x
Exists forall a b. (a -> b) -> a -> b
$ forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat forall a b. (a -> b) -> a -> b
$ forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field t
a forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field HeadLoT 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))                     = forall a. WeirdTree a -> WeirdTree a -> WeirdTree a
WeirdBranch Interpret (WeirdTree :$: Var0) x
l Interpret (WeirdTree :$: Var0) x
r
  toK (R1 (Exists (SuchThat (Field Interpret Var0 (t ':&&: x)
a :*: Field Interpret Var1 (t ':&&: x)
x)))) = forall a a. Show a => a -> a -> WeirdTree a
WeirdLeaf Interpret Var0 (t ':&&: x)
a 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) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall a b. (a -> b) -> a -> b
$                     forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field WeirdTreeR (HeadLoT x)
l forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field WeirdTreeR (HeadLoT x)
r
  fromK (WeirdLeafR   t
a HeadLoT x
x) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ forall k (a :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (a ':&&: x) -> Exists k f x
Exists forall a b. (a -> b) -> a -> b
$ forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat forall a b. (a -> b) -> a -> b
$ forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field t
a forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field HeadLoT 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))                     = forall a. WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a
WeirdBranchR Interpret (WeirdTreeR :$: Var0) x
l Interpret (WeirdTreeR :$: Var0) x
r
  toK (R1 (Exists (SuchThat (Field Interpret Var0 (t ':&&: x)
a :*: Field Interpret Var1 (t ':&&: x)
x)))) = forall a a. (Show a, Eq a, Typeable a) => a -> a -> WeirdTreeR a
WeirdLeafR Interpret Var0 (t ':&&: x)
a 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) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall a b. (a -> b) -> a -> b
$                     forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field WeirdTreeR a
l forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field WeirdTreeR a
r
  fromK (WeirdLeafR   t
a a
x) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ forall k (a :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (a ':&&: x) -> Exists k f x
Exists forall a b. (a -> b) -> a -> b
$ forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat forall a b. (a -> b) -> a -> b
$ forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field t
a forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field a
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))                     = forall a. WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a
WeirdBranchR Interpret ('Kon (WeirdTreeR a)) x
l Interpret ('Kon (WeirdTreeR a)) x
r
  toK (R1 (Exists (SuchThat (Field Interpret Var0 (t ':&&: x)
a :*: Field Interpret ('Kon a) (t ':&&: x)
x)))) = forall a a. (Show a, Eq a, Typeable a) => a -> a -> WeirdTreeR a
WeirdLeafR Interpret Var0 (t ':&&: x)
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) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field String
s))
  fromK TTY m a :@@: x
TTY m a
ReadTTY      = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat 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))) = forall {k} (m :: k). String -> TTY m ()
WriteTTY Interpret ('Kon String) x
s
  toK (R1 (SuchThat U1 x
U1))        = 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) = forall k (a :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (a ':&&: x) -> Exists k f x
Exists (forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Maybe a
x))
  toK :: forall (x :: LoT (k -> *)). RepK T x -> T :@@: x
toK (Exists (SuchThat (Field Interpret (Maybe :$: Var0) (t ':&&: x)
x))) = forall a. Maybe a -> T a
MkT Interpret (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  = 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 = 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' = forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat forall k (p :: k). U1 p
U1
  toK :: forall (x :: LoT (k -> *)). RepK (P' j) x -> P' j :@@: x
toK (SuchThat U1 x
U1) = 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' = forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat forall k (p :: k). U1 p
U1
  toK :: forall (x :: LoT (* -> k -> *)). RepK P' x -> P' :@@: x
toK (SuchThat U1 x
U1) = 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) = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field (forall {d1} {d} (f :: Atom (d1 -> d) (*)) (tys :: LoT d).
(forall (t :: d1). Interpret f (t ':&&: tys)) -> ForAllI f tys
ForAllI 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 forall t. Interpret (((->) :$: Var0) ':@: Var0) (t ':&&: x)
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) = 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)
x)
  toK :: forall (x :: LoT (* -> *)). RepK Ranky2 x -> Ranky2 :@@: x
toK (Field Interpret
  (((->) :$: 'ForAll (((->) :$: Var0) ':@: Var0)) ':@: Var0) x
f) = forall b. ((forall a. a -> a) -> b) -> Ranky2 b
MkRanky2 (\forall a. a -> a
x -> Interpret
  (((->) :$: 'ForAll (((->) :$: Var0) ':@: Var0)) ':@: Var0) x
f (forall {d1} {d} (f :: Atom (d1 -> d) (*)) (tys :: LoT d).
(forall (t :: d1). Interpret f (t ':&&: tys)) -> ForAllI f tys
ForAllI 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) = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field (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
f)
  toK :: forall (x :: LoT (* -> *)). RepK Shower x -> Shower :@@: x
toK (Field (SuchThatI Interpret ('Kon Show ':@: Var0) x =>
Interpret (((->) :$: Var0) ':@: 'Kon String) x
f)) = forall a. (Show a => a -> String) -> Shower a
MkShower Interpret ('Kon 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) = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Eval (HeadLoT x (HeadLoT (TailLoT x)))
x
  toK :: forall (x :: LoT ((k -> * -> *) -> k -> *)).
RepK Hkd x -> Hkd :@@: x
toK (Field Interpret ('Eval (Var0 ':@: Var1)) x
x) = forall {k} (f :: k -> * -> *) (a :: k). Eval (f a) -> Hkd f a
Hkd 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) = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Eval (f (HeadLoT x))
x
  toK :: forall (x :: LoT (k -> *)). RepK (Hkd f) x -> Hkd f :@@: x
toK (Field Interpret ('Eval ('Kon f ':@: Var0)) x
x) = forall {k} (f :: k -> * -> *) (a :: k). Eval (f a) -> Hkd f a
Hkd 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) = forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Eval (f a)
x
  toK :: forall (x :: LoT (*)). RepK (Hkd f a) x -> Hkd f a :@@: x
toK (Field Interpret ('Kon (Eval (f a))) x
x) = forall {k} (f :: k -> * -> *) (a :: k). Eval (f a) -> Hkd f a
Hkd Interpret ('Kon (Eval (f a))) x
x