{-# language AllowAmbiguousTypes       #-}
{-# language ConstraintKinds           #-}
{-# language DataKinds                 #-}
{-# language DefaultSignatures         #-}
{-# language ExistentialQuantification #-}
{-# language FlexibleContexts          #-}
{-# language FlexibleInstances         #-}
{-# language GADTs                     #-}
{-# language MultiParamTypeClasses     #-}
{-# language PolyKinds                 #-}
{-# language QuantifiedConstraints     #-}
{-# language ScopedTypeVariables       #-}
{-# language StandaloneDeriving        #-}
{-# language TypeApplications          #-}
{-# language TypeFamilies              #-}
{-# language TypeOperators             #-}
{-# language UndecidableInstances      #-}
-- | Main module of @kind-generics@. Please refer to the @README@ file for documentation on how to use this package.
module Generics.Kind (
  module Data.PolyKinded
, module Data.PolyKinded.Atom
  -- * Generic representation types
, (:+:)(..), (:*:)(..), V1, U1(..), M1(..)
, Field(..), (:=>:)(..), Exists(..)
  -- * Generic type classes
, GenericK(..)
, GenericF, fromF, toF
, GenericN, fromN, toN
  -- * Getting more instances almost for free
, fromRepK, toRepK, SubstRep, SubstRep', SubstAtom
  -- * Bridging with "GHC.Generics"
, Conv(..)
) where

import           Data.Kind
import           Data.PolyKinded
import           Data.PolyKinded.Atom
import           GHC.Generics.Extra   hiding (SuchThat, (:=>:))
import qualified GHC.Generics.Extra   as GG
-- import GHC.Exts

-- | Fields: used to represent each of the (visible) arguments to a constructor.
-- Replaces the 'K1' type from "GHC.Generics". The type of the field is
-- represented by an 'Atom' from "Data.PolyKinded.Atom".
--
-- > instance GenericK [] (a :&&: LoT0) where
-- >   type RepK [] = Field Var0 :*: Field ([] :$: Var0)
newtype Field (t :: Atom d (*)) (x :: LoT d) where
  -- Field :: forall (r :: RuntimeRep) (k :: TYPE r) (d :: *). Atom d k -> LoT d -> * where
  -- Until https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0013-unlifted-newtypes.rst
  -- and https://ghc.haskell.org/trac/ghc/ticket/14917
  -- are implemented, we are restricted to the (*) kind
  Field :: { Field t x -> Interpret t x
unField :: Interpret t x } -> Field t x
deriving instance Show (Interpret t x) => Show (Field t x)

-- | Constraints: used to represent constraints in a constructor.
-- Replaces the '(:=>:)' type from "GHC.Generics.Extra".
--
-- > data Showable a = Show a => a -> X a
-- >
-- > instance GenericK Showable (a :&&: LoT0) where
-- >   type RepK Showable = (Show :$: a) :=>: (Field Var0)
data (:=>:) (c :: Atom d Constraint) (f :: LoT d -> *) (x :: LoT d) where
  SuchThat :: Interpret c x => f x -> (c :=>: f) x
deriving instance (Interpret c x => Show (f x)) => Show ((c :=>: f) x)

-- | Existentials: a representation of the form @E f@ describes
-- a constructor whose inner type is represented by @f@, and where
-- the type variable at index 0, @Var0@, is existentially quantified.
--
-- > data E where
-- >  E :: t -> Exists
-- >
-- > instance GenericK E LoT0 where
-- >   type RepK E = Exists (*) (Field Var0)
data Exists k (f :: LoT (k -> d) -> *) (x :: LoT d) where
  Exists :: forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d)
          .{ ()
unExists :: f (t ':&&: x) } -> Exists k f x
deriving instance (forall t. Show (f (t ':&&: x))) => Show (Exists k f x)

-- THE TYPE CLASS

-- | Representable types of any kind. Examples:
--
-- > instance GenericK Int
-- > instance GenericK []
-- > instance GenericK Either
-- > instance GenericK (Either a)
-- > instance GenericK (Either a b)
class GenericK (f :: k) where
  type RepK f :: LoT k -> *

  -- | Convert the data type to its representation.
  fromK :: f :@@: x -> RepK f x
  default
    fromK :: (Generic (f :@@: x), Conv (Rep (f :@@: x)) (RepK f) x)
          => f :@@: x -> RepK f x
  fromK = Rep (f :@@: x) Any -> RepK f x
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
gg a -> kg tys
toKindGenerics (Rep (f :@@: x) Any -> RepK f x)
-> ((f :@@: x) -> Rep (f :@@: x) Any) -> (f :@@: x) -> RepK f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f :@@: x) -> Rep (f :@@: x) Any
forall a x. Generic a => a -> Rep a x
from

  -- | Convert from a representation to its corresponding data type.
  toK   :: RepK f x -> f :@@: x
  default
    toK :: (Generic (f :@@: x), Conv (Rep (f :@@: x)) (RepK f) x)
        => RepK f x -> f :@@: x
  toK = Rep (f :@@: x) Any -> f :@@: x
forall a x. Generic a => Rep a x -> a
to (Rep (f :@@: x) Any -> f :@@: x)
-> (RepK f x -> Rep (f :@@: x) Any) -> RepK f x -> f :@@: x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RepK f x -> Rep (f :@@: x) Any
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
kg tys -> gg a
toGhcGenerics

type GenericF t f x = (GenericK f, x ~ SplitF t f, t ~ (f :@@: x))
fromF :: forall f t x. GenericF t f x => t -> RepK f x
fromF :: t -> RepK f x
fromF = forall (x :: LoT k). GenericK f => (f :@@: x) -> RepK f x
forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @f
toF :: forall f t x. GenericF t f x => RepK f x -> t
toF :: RepK f x -> t
toF = forall (x :: LoT k). GenericK f => RepK f x -> f :@@: x
forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @f

type GenericN n t f x = (GenericK f, 'TyEnv f x ~ SplitN n t, t ~ (f :@@: x))
fromN :: forall n t f x. GenericN n t f x => t -> RepK f x
fromN :: t -> RepK f x
fromN = forall (x :: LoT k). GenericK f => (f :@@: x) -> RepK f x
forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @f
toN :: forall n t f x. GenericN n t f x => RepK f x -> t
toN :: RepK f x -> t
toN = forall (x :: LoT k). GenericK f => RepK f x -> f :@@: x
forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @f

-- CONVERSION BETWEEN FEWER AND MORE ARGUMENTS

fromRepK :: forall f x xs. (GenericK f, SubstRep' (RepK f) x xs)
         => f x :@@: xs -> SubstRep (RepK f) x xs
fromRepK :: (f x :@@: xs) -> SubstRep (RepK f) x xs
fromRepK = RepK f (x ':&&: xs) -> SubstRep (RepK f) x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep (RepK f (x ':&&: xs) -> SubstRep (RepK f) x xs)
-> ((f x :@@: xs) -> RepK f (x ':&&: xs))
-> (f x :@@: xs)
-> SubstRep (RepK f) x xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f :@@: (x ':&&: xs)) -> RepK f (x ':&&: xs)
forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @f @(x ':&&: xs)

toRepK :: forall f x xs. (GenericK f, SubstRep' (RepK f) x xs)
       => SubstRep (RepK f) x xs -> f x :@@: xs
toRepK :: SubstRep (RepK f) x xs -> f x :@@: xs
toRepK = RepK f (x ':&&: xs) -> f :@@: (x ':&&: xs)
forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @f @(x ':&&: xs) (RepK f (x ':&&: xs) -> f x :@@: xs)
-> (SubstRep (RepK f) x xs -> RepK f (x ':&&: xs))
-> SubstRep (RepK f) x xs
-> f x :@@: xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubstRep (RepK f) x xs -> RepK f (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep

class SubstRep' (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k) where
  type family SubstRep f x :: LoT k -> *
  substRep   :: f (x ':&&: xs) -> SubstRep f x xs
  unsubstRep :: SubstRep f x xs -> f (x ':&&: xs)

instance SubstRep' U1 x xs where
  type SubstRep U1 x = U1
  substRep :: U1 (x ':&&: xs) -> SubstRep U1 x xs
substRep   U1 (x ':&&: xs)
U1 = SubstRep U1 x xs
forall k (p :: k). U1 p
U1
  unsubstRep :: SubstRep U1 x xs -> U1 (x ':&&: xs)
unsubstRep SubstRep U1 x xs
U1 = U1 (x ':&&: xs)
forall k (p :: k). U1 p
U1

instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :+: g) x xs where
  type SubstRep (f :+: g)  x = SubstRep f x :+: SubstRep g x
  substRep :: (:+:) f g (x ':&&: xs) -> SubstRep (f :+: g) x xs
substRep   (L1 f (x ':&&: xs)
x) = SubstRep f x xs -> (:+:) (SubstRep f x) (SubstRep g x) xs
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f (x ':&&: xs) -> SubstRep f x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   f (x ':&&: xs)
x)
  substRep   (R1 g (x ':&&: xs)
x) = SubstRep g x xs -> (:+:) (SubstRep f x) (SubstRep g x) xs
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g (x ':&&: xs) -> SubstRep g x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   g (x ':&&: xs)
x)
  unsubstRep :: SubstRep (f :+: g) x xs -> (:+:) f g (x ':&&: xs)
unsubstRep (L1 x) = f (x ':&&: xs) -> (:+:) f g (x ':&&: xs)
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (SubstRep f x xs -> f (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep f x xs
x)
  unsubstRep (R1 x) = g (x ':&&: xs) -> (:+:) f g (x ':&&: xs)
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (SubstRep g x xs -> g (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep g x xs
x)

instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :*: g) x xs where
  type SubstRep (f :*: g) x = SubstRep f x :*: SubstRep g x
  substRep :: (:*:) f g (x ':&&: xs) -> SubstRep (f :*: g) x xs
substRep   (f (x ':&&: xs)
x :*: g (x ':&&: xs)
y) = f (x ':&&: xs) -> SubstRep f x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   f (x ':&&: xs)
x SubstRep f x xs
-> SubstRep g x xs -> (:*:) (SubstRep f x) (SubstRep g x) xs
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g (x ':&&: xs) -> SubstRep g x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   g (x ':&&: xs)
y
  unsubstRep :: SubstRep (f :*: g) x xs -> (:*:) f g (x ':&&: xs)
unsubstRep (x :*: y) = SubstRep f x xs -> f (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep f x xs
x f (x ':&&: xs) -> g (x ':&&: xs) -> (:*:) f g (x ':&&: xs)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: SubstRep g x xs -> g (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep g x xs
y

instance SubstRep' f x xs => SubstRep' (M1 i c f) x xs where
  type SubstRep (M1 i c f) x = M1 i c (SubstRep f x)
  substRep :: M1 i c f (x ':&&: xs) -> SubstRep (M1 i c f) x xs
substRep   (M1 f (x ':&&: xs)
x) = SubstRep f x xs -> M1 i c (SubstRep f x) xs
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f (x ':&&: xs) -> SubstRep f x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   f (x ':&&: xs)
x)
  unsubstRep :: SubstRep (M1 i c f) x xs -> M1 i c f (x ':&&: xs)
unsubstRep (M1 x) = f (x ':&&: xs) -> M1 i c f (x ':&&: xs)
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (SubstRep f x xs -> f (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep f x xs
x)

instance (Interpret (SubstAtom c x) xs, Interpret c (x ':&&: xs), SubstRep' f x xs)
         => SubstRep' (c :=>: f) x xs where
  type SubstRep (c :=>: f) x = SubstAtom c x :=>: SubstRep f x
  substRep :: (:=>:) c f (x ':&&: xs) -> SubstRep (c :=>: f) x xs
substRep   (SuchThat f (x ':&&: xs)
x) = SubstRep f x xs -> (:=>:) (SubstAtom c x) (SubstRep f x) xs
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (f (x ':&&: xs) -> SubstRep f x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   f (x ':&&: xs)
x)
  unsubstRep :: SubstRep (c :=>: f) x xs -> (:=>:) c f (x ':&&: xs)
unsubstRep (SuchThat x) = f (x ':&&: xs) -> (:=>:) c f (x ':&&: xs)
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (SubstRep f x xs -> f (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep f x xs
x)

instance (Interpret (SubstAtom t x) xs ~ Interpret t (x ':&&: xs))
         => SubstRep' (Field t) x xs where
  type SubstRep (Field t) x = Field (SubstAtom t x)
  substRep :: Field t (x ':&&: xs) -> SubstRep (Field t) x xs
substRep   (Field Interpret t (x ':&&: xs)
x) = Interpret (SubstAtom t x) xs -> Field (SubstAtom t x) xs
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret (SubstAtom t x) xs
Interpret t (x ':&&: xs)
x
  unsubstRep :: SubstRep (Field t) x xs -> Field t (x ':&&: xs)
unsubstRep (Field x) = Interpret t (x ':&&: xs) -> Field t (x ':&&: xs)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret (SubstAtom t x) xs
Interpret t (x ':&&: xs)
x

type family SubstAtom (f :: Atom (t -> k) d) (x :: t) :: Atom k d where
  SubstAtom ('Var 'VZ)     x = 'Kon x
  SubstAtom ('Var ('VS v)) x = 'Var v
  SubstAtom ('Kon t)       x = 'Kon t
  SubstAtom (t1 ':@: t2)   x = SubstAtom t1 x ':@: SubstAtom t2 x
  SubstAtom (t1 ':&: t2)   x = SubstAtom t1 x ':&: SubstAtom t2 x

-- CONVERSION BETWEEN GHC.GENERICS AND KIND-GENERICS

-- | Bridges a representation of a data type using the combinators
-- in "GHC.Generics" with a representation using this module.
-- You are never expected to manipulate this type class directly,
-- it is part of the deriving mechanism for 'GenericK'.
class Conv (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) where
  toGhcGenerics  :: kg tys -> gg a
  toKindGenerics :: gg a -> kg tys

instance Conv U1 U1 tys where
  toGhcGenerics :: U1 tys -> U1 a
toGhcGenerics  U1 tys
U1 = U1 a
forall k (p :: k). U1 p
U1
  toKindGenerics :: U1 a -> U1 tys
toKindGenerics U1 a
U1 = U1 tys
forall k (p :: k). U1 p
U1

instance (Conv f f' tys, Conv g g' tys) => Conv (f :+: g) (f' :+: g') tys where
  toGhcGenerics :: (:+:) f' g' tys -> (:+:) f g a
toGhcGenerics  (L1 f' tys
x) = f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f' tys -> f a
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
kg tys -> gg a
toGhcGenerics  f' tys
x)
  toGhcGenerics  (R1 g' tys
x) = g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g' tys -> g a
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
kg tys -> gg a
toGhcGenerics  g' tys
x)
  toKindGenerics :: (:+:) f g a -> (:+:) f' g' tys
toKindGenerics (L1 f a
x) = f' tys -> (:+:) f' g' tys
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f a -> f' tys
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
gg a -> kg tys
toKindGenerics f a
x)
  toKindGenerics (R1 g a
x) = g' tys -> (:+:) f' g' tys
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g a -> g' tys
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
gg a -> kg tys
toKindGenerics g a
x)

instance (Conv f f' tys, Conv g g' tys) => Conv (f :*: g) (f' :*: g') tys where
  toGhcGenerics :: (:*:) f' g' tys -> (:*:) f g a
toGhcGenerics  (f' tys
x :*: g' tys
y) = f' tys -> f a
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
kg tys -> gg a
toGhcGenerics  f' tys
x f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g' tys -> g a
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
kg tys -> gg a
toGhcGenerics  g' tys
y
  toKindGenerics :: (:*:) f g a -> (:*:) f' g' tys
toKindGenerics (f a
x :*: g a
y) = f a -> f' tys
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
gg a -> kg tys
toKindGenerics f a
x f' tys -> g' tys -> (:*:) f' g' tys
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a -> g' tys
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
gg a -> kg tys
toKindGenerics g a
y

instance {-# OVERLAPPABLE #-} (Conv f f' tys) => Conv (M1 i c f) f' tys where
  toGhcGenerics :: f' tys -> M1 i c f a
toGhcGenerics  f' tys
x = f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f' tys -> f a
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
kg tys -> gg a
toGhcGenerics  f' tys
x)
  toKindGenerics :: M1 i c f a -> f' tys
toKindGenerics (M1 f a
x) = f a -> f' tys
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
gg a -> kg tys
toKindGenerics f a
x

instance {-# OVERLAPS #-} (Conv f f' tys) => Conv (M1 i c f) (M1 i c f') tys where
  toGhcGenerics :: M1 i c f' tys -> M1 i c f a
toGhcGenerics  (M1 f' tys
x) = f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f' tys -> f a
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
kg tys -> gg a
toGhcGenerics  f' tys
x)
  toKindGenerics :: M1 i c f a -> M1 i c f' tys
toKindGenerics (M1 f a
x) = f' tys -> M1 i c f' tys
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f a -> f' tys
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
gg a -> kg tys
toKindGenerics f a
x)

instance (k ~ Interpret t tys, Conv f f' tys)
         => Conv (k GG.:=>: f) (t :=>: f') tys where
  toGhcGenerics :: (:=>:) t f' tys -> (:=>:) k f a
toGhcGenerics (SuchThat f' tys
x) = f a -> (:=>:) k f a
forall k (c :: Constraint) (f :: k -> *) (a :: k).
c =>
f a -> (:=>:) c f a
GG.SuchThat (f' tys -> f a
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
kg tys -> gg a
toGhcGenerics f' tys
x)
  toKindGenerics :: (:=>:) k f a -> (:=>:) t f' tys
toKindGenerics (GG.SuchThat f a
x) = f' tys -> (:=>:) t f' tys
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (f a -> f' tys
forall d (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) a.
Conv gg kg tys =>
gg a -> kg tys
toKindGenerics f a
x)

instance (k ~ Interpret t tys) => Conv (K1 p k) (Field t) tys where
  toGhcGenerics :: Field t tys -> K1 p k a
toGhcGenerics  (Field Interpret t tys
x)  = k -> K1 p k a
forall k i c (p :: k). c -> K1 i c p
K1 k
Interpret t tys
x
  toKindGenerics :: K1 p k a -> Field t tys
toKindGenerics (K1 k
x) = Interpret t tys -> Field t tys
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field k
Interpret t tys
x