{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- | Leads are a concept which emerge from the bidirectional aspect of stacked
-- applicatives and monads. This module defines leads generically for every
-- constructor of a type with a 'Generic' instance (see 'lead' below).
--
-- == What is a lead?
--
-- When implementing a traversal with regular applicative functors, we write
-- things like
--
-- > foo :: (Applicative f) => (a -> f b) -> Maybe a -> f (Maybe b)
-- > foo f (Just a) = Just <$> f a
-- > foo _ Maybe = Maybe
--
-- With stacked applicatives, however, the argument is on the abstract stack,
-- rather than a proper argument to the function. That is we want a function:
--
-- > bar :: (Indexed.Applicative m, Stacked m)
-- >     => m (a -> r) r b -> m (Maybe a -> r) r (Maybe b)
--
-- So we have to provide a way to pattern-match on the the top element of the
-- stack. This is what lead provide. Leads are effectful actions, because they
-- can fail, representing each constructor. Because they're effectful they are
-- used with @(<*>)@ rather than @(<$>)@ like constructors are. So that @bar@
-- would be implemented as
--
-- > bar f =
-- >   lead @"Just" <*> f
-- >   <|> lead @None
--
-- Or, with @OverloadedLabels@ and "Control.Monad.Indexed.Cont2.Lead.Labels",
--
-- > bar f =
-- >   #Just <*> f
-- >   <|> #None
--
-- The strength of stacked applicatives (or monads) is that leads extend to
-- constructors with several fields in much the same way as regular applicatives
-- do.
--
-- > data OneOrTwo a b = One a | Two a b
-- >   deriving (Generic)
-- >
-- > baz :: (Indexed.Applicative m, Stacked m)
-- >     => m (a -> r) r b -> m (OneOrTwo a a -> r) r (OneOrTwo b b)
-- > baz f =
-- >   #One <*> f
-- >   <|> #Two <*> f <*> f
-- >
-- > baz2 :: (Indexed.Applicative m, Stacked m)
-- >      => m (a -> r) r a' -> m (b -> r) r b' -> m (OneOrTwo a b -> r) r (OneOrTwo a' b')
-- > baz2 f g =
-- >   #One <*> f
-- >   <|> #Two <*> f <*> g
module Control.Monad.Indexed.Cont2.Lead.Generic
  ( lead,

    -- * Auxiliary definitions
    Leading,
    CFieldsType,
  )
where

import Control.Monad.Indexed qualified as Indexed
import Control.Monad.Indexed.Cont2 qualified as Cont2
import Data.Kind
import GHC.Generics
import GHC.TypeLits

-- Partly inspired by (and some code lifted from)
-- https://github.com/tweag/linear-dest/blob/0e7db2e6b24aad348837ac78d8137712c1d8d12a/src/Compact/Pure/Internal.hs
-- Partly inspired by generic lens
-- https://hackage.haskell.org/package/generic-lens-core-2.2.1.0/docs/src/Data.Generics.Sum.Internal.Constructors.html

type Leading :: Symbol -> Type -> Constraint
class Leading c t where
  match :: (t -> i) -> CFieldsType c (Rep t ()) i -> t -> i
  unmatch :: (t -> i) -> CFieldsType c (Rep t ()) i

-- the_constr :: CFieldsType c (Rep t ()) tgt

-- | 'lead' @C@ is the lead for any constructor @C@ of a 'Generic' data type.
-- For instance
--
-- > lead @Just :: m (Maybe a -> r) (a -> r) (b -> Maybe b)
--
-- With @OverloadedLabels@ and "Control.Monad.Indexed.Cont2.Lead.Labels", this
-- can be written simply @#Just@ instead.
--
-- For a constructors with several arguments the type would be
--
-- > data OneOrTwo a b = One a | Two a b
-- >   deriving (Generic)
-- >
-- > lead @Two :: m (OneOrTwo a b -> r) (a -> b -> r) (c -> d -> OneOrTwo c d)
--
-- == __Manual definitions__
-- Here are some manual, specialised, definitions of 'lead' for inspiration if
-- the generic derivation aren't enough.
--
-- > lead @True :: (Indexed.MonadPlus m, Cont2.Stacked m) => m (Bool -> r) r Bool
-- > lead @True = Indexed.do
-- >   Cont2.stack (\cases _ k True -> k; fl _ b -> fl b) (\k -> k True)
-- >   Indexed.pure True
--
-- > lead @Just :: (Indexed.MonadPlus m, Cont2.Stacked m) => m (Maybe a -> r) (a -> r) (b -> Maybe b)
-- > lead @Just = Indexed.do
-- >   Cont2.stack (\cases _ k (Just a) -> k a; fl _ b -> fl b) (\k a -> k (Just a))
-- >   Indexed.pure Just
--
-- > lead @Two :: (Indexed.MonadPlus m, Cont2.Stacked m) => m (OneOrTwo a b -> r) (a -> b -> r) (c -> d -> OneOrTwo c d)
-- > lead @Two = Indexed.do
-- >   Cont2.stack (\cases _ k (Two a b) -> k a b; fl _ b -> fl b) (\k a b -> k (Two a b))
-- >   Indexed.pure Two
lead :: forall c t r m. (Leading c t, Indexed.MonadPlus m, Cont2.Stacked m) => m (t -> r) (CFieldsType c (Rep t ()) r) (CFieldsType c (Rep t ()) t)
lead :: forall (c :: Symbol) t r (m :: * -> * -> * -> *).
(Leading c t, MonadPlus m, Stacked m) =>
m (t -> r)
  (CFieldsType c (Rep t ()) r)
  (CFieldsType c (Rep t ()) t)
lead = Indexed.do
  ((t -> r) -> CFieldsType c (Rep t ()) r -> t -> r)
-> ((t -> r) -> CFieldsType c (Rep t ()) r)
-> m (t -> r) (CFieldsType c (Rep t ()) r) ()
forall (m :: * -> * -> * -> *) i j.
(Applicative m, Stacked m) =>
(i -> j -> i) -> (i -> j) -> m i j ()
Cont2.stack (forall (c :: Symbol) t i.
Leading c t =>
(t -> i) -> CFieldsType c (Rep t ()) i -> t -> i
match @c @t @r) (forall (c :: Symbol) t i.
Leading c t =>
(t -> i) -> CFieldsType c (Rep t ()) i
unmatch @c @t @r)
  CFieldsType c (Rep t ()) t
-> m (FieldsType (FromJust (SelectConstructor c (Rep t ()))) r)
     (FieldsType (FromJust (SelectConstructor c (Rep t ()))) r)
     (CFieldsType c (Rep t ()) t)
forall a i. a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
Indexed.pure (CFieldsType c (Rep t ()) t
 -> m (FieldsType (FromJust (SelectConstructor c (Rep t ()))) r)
      (FieldsType (FromJust (SelectConstructor c (Rep t ()))) r)
      (CFieldsType c (Rep t ()) t))
-> CFieldsType c (Rep t ()) t
-> m (FieldsType (FromJust (SelectConstructor c (Rep t ()))) r)
     (FieldsType (FromJust (SelectConstructor c (Rep t ()))) r)
     (CFieldsType c (Rep t ()) t)
forall a b. (a -> b) -> a -> b
$ forall (c :: Symbol) t i.
Leading c t =>
(t -> i) -> CFieldsType c (Rep t ()) i
unmatch @c @t @t t -> t
forall a. a -> a
id

------------------------------------------------------------------------------
--
-- Below, the generic machinery
--
------------------------------------------------------------------------------

instance (Generic t, Defined (Rep t) (TypeError (NoGeneric t)) (() :: Constraint), GLeading c (Rep t) ()) => Leading c t where
  match :: forall i. (t -> i) -> CFieldsType c (Rep t ()) i -> t -> i
match t -> i
fl CFieldsType c (Rep t ()) i
k t
t = forall (c :: Symbol) (rep :: * -> *) x i.
GLeading c rep x =>
(rep x -> i) -> CFieldsType c (rep x) i -> rep x -> i
gmatch @c @(Rep t) @() (t -> i
fl (t -> i) -> (Rep t () -> t) -> Rep t () -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep t () -> t
forall a x. Generic a => Rep a x -> a
forall x. Rep t x -> t
to) CFieldsType c (Rep t ()) i
k (t -> Rep t ()
forall x. t -> Rep t x
forall a x. Generic a => a -> Rep a x
from t
t)
  unmatch :: forall i. (t -> i) -> CFieldsType c (Rep t ()) i
unmatch t -> i
k = forall (c :: Symbol) (rep :: * -> *) x i.
GLeading c rep x =>
(rep x -> i) -> CFieldsType c (rep x) i
gunmatch @c @(Rep t) @() (t -> i
k (t -> i) -> (Rep t () -> t) -> Rep t () -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep t () -> t
forall a x. Generic a => Rep a x -> a
forall x. Rep t x -> t
to)

type NoGeneric t = 'Text "No instance for " ':<>: QuoteType (Generic t)

type QuoteType t = 'Text "‘" ':<>: 'ShowType t ':<>: 'Text "’"

type GLeading :: Symbol -> (Type -> Type) -> Type -> Constraint
class GLeading c rep x where
  gmatch :: (rep x -> i) -> CFieldsType c (rep x) i -> rep x -> i
  gunmatch :: (rep x -> i) -> CFieldsType c (rep x) i

-- gthe_constr :: CFieldsType c rep t

instance (GSumLeading c (IsJust (SelectConstructor c (l x))) (SelectConstructor c ((l :+: r) x)) l r x) => GLeading c (l :+: r) x where
  gmatch :: forall i.
((:+:) l r x -> i)
-> CFieldsType c ((:+:) l r x) i -> (:+:) l r x -> i
gmatch (:+:) l r x -> i
fl CFieldsType c ((:+:) l r x) i
k (:+:) l r x
t =
    forall (c :: Symbol) (inl :: Bool) (k :: Maybe (*)) (l :: * -> *)
       (r :: * -> *) x i.
GSumLeading c inl k l r x =>
((:+:) l r x -> i) -> FieldsType (FromJust k) i -> (:+:) l r x -> i
gsum_match @c @(IsJust (SelectConstructor c (l x))) @(SelectConstructor c ((l :+: r) x)) @l @r @x (:+:) l r x -> i
fl CFieldsType c ((:+:) l r x) i
FieldsType (FromJust (SelectConstructor c ((:+:) l r x))) i
k (:+:) l r x
t
  gunmatch :: forall i. ((:+:) l r x -> i) -> CFieldsType c ((:+:) l r x) i
gunmatch (:+:) l r x -> i
k =
    forall (c :: Symbol) (inl :: Bool) (k :: Maybe (*)) (l :: * -> *)
       (r :: * -> *) x i.
GSumLeading c inl k l r x =>
((:+:) l r x -> i) -> FieldsType (FromJust k) i
gsum_unmatch @c @(IsJust (SelectConstructor c (l x))) @(SelectConstructor c ((l :+: r) x)) @l @r @x (:+:) l r x -> i
k

instance (GProdLeading f x) => GLeading c (M1 C ('MetaCons c fixity fields) f) x where
  gmatch :: forall i.
(M1 C ('MetaCons c fixity fields) f x -> i)
-> CFieldsType c (M1 C ('MetaCons c fixity fields) f x) i
-> M1 C ('MetaCons c fixity fields) f x
-> i
gmatch M1 C ('MetaCons c fixity fields) f x -> i
_fl CFieldsType c (M1 C ('MetaCons c fixity fields) f x) i
k (M1 f x
t) = FieldsType (f x) i -> f x -> i
forall i. FieldsType (f x) i -> f x -> i
forall {k} (t :: k -> *) (x :: k) i.
GProdLeading t x =>
FieldsType (t x) i -> t x -> i
gapply CFieldsType c (M1 C ('MetaCons c fixity fields) f x) i
FieldsType (f x) i
k f x
t
  gunmatch :: forall i.
(M1 C ('MetaCons c fixity fields) f x -> i)
-> CFieldsType c (M1 C ('MetaCons c fixity fields) f x) i
gunmatch M1 C ('MetaCons c fixity fields) f x -> i
k = (M1 C ('MetaCons c fixity fields) f x -> i)
-> FieldsType (M1 C ('MetaCons c fixity fields) f x) i
forall i.
(M1 C ('MetaCons c fixity fields) f x -> i)
-> FieldsType (M1 C ('MetaCons c fixity fields) f x) i
forall {k} (t :: k -> *) (x :: k) i.
GProdLeading t x =>
(t x -> i) -> FieldsType (t x) i
gbuild M1 C ('MetaCons c fixity fields) f x -> i
k

instance (GLeading c f x) => GLeading c (D1 meta f) x where
  gmatch :: forall i.
(D1 meta f x -> i)
-> CFieldsType c (D1 meta f x) i -> D1 meta f x -> i
gmatch D1 meta f x -> i
fl CFieldsType c (D1 meta f x) i
k (M1 f x
t) = forall (c :: Symbol) (rep :: * -> *) x i.
GLeading c rep x =>
(rep x -> i) -> CFieldsType c (rep x) i -> rep x -> i
gmatch @c @f @x (D1 meta f x -> i
fl (D1 meta f x -> i) -> (f x -> D1 meta f x) -> f x -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> D1 meta f x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1) CFieldsType c (f x) i
CFieldsType c (D1 meta f x) i
k f x
t
  gunmatch :: forall i. (D1 meta f x -> i) -> CFieldsType c (D1 meta f x) i
gunmatch (D1 meta f x -> i
k :: D1 meta f x -> i) = forall (c :: Symbol) (rep :: * -> *) x i.
GLeading c rep x =>
(rep x -> i) -> CFieldsType c (rep x) i
gunmatch @c @f @x @i (D1 meta f x -> i
k (D1 meta f x -> i) -> (f x -> D1 meta f x) -> f x -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> D1 meta f x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1)

type GSumLeading :: Symbol -> Bool -> Maybe Type -> (Type -> Type) -> (Type -> Type) -> Type -> Constraint
class GSumLeading c inl k l r x where
  gsum_match :: ((l :+: r) x -> i) -> FieldsType (FromJust k) i -> (l :+: r) x -> i
  gsum_unmatch :: ((l :+: r) x -> i) -> FieldsType (FromJust k) i

instance (GLeading c l x, SelectConstructor c (l x) ~ 'Just k) => GSumLeading c 'True ('Just k) l r x where
  gsum_match :: forall i.
((:+:) l r x -> i)
-> FieldsType (FromJust ('Just k)) i -> (:+:) l r x -> i
gsum_match (:+:) l r x -> i
fl FieldsType (FromJust ('Just k)) i
k (L1 l x
tl) = forall (c :: Symbol) (rep :: * -> *) x i.
GLeading c rep x =>
(rep x -> i) -> CFieldsType c (rep x) i -> rep x -> i
gmatch @c @l @x ((:+:) l r x -> i
fl ((:+:) l r x -> i) -> (l x -> (:+:) l r x) -> l x -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. l x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1) CFieldsType c (l x) i
FieldsType (FromJust ('Just k)) i
k l x
tl
  gsum_match (:+:) l r x -> i
fl FieldsType (FromJust ('Just k)) i
_k (R1 r x
tr) = (:+:) l r x -> i
fl (r x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 r x
tr)

  gsum_unmatch :: forall i. ((:+:) l r x -> i) -> FieldsType (FromJust ('Just k)) i
gsum_unmatch (:+:) l r x -> i
k = forall (c :: Symbol) (rep :: * -> *) x i.
GLeading c rep x =>
(rep x -> i) -> CFieldsType c (rep x) i
gunmatch @c @l @x ((:+:) l r x -> i
k ((:+:) l r x -> i) -> (l x -> (:+:) l r x) -> l x -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. l x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1)

instance (GLeading c r x, SelectConstructor c (r x) ~ 'Just k) => GSumLeading c 'False ('Just k) l r x where
  gsum_match :: forall i.
((:+:) l r x -> i)
-> FieldsType (FromJust ('Just k)) i -> (:+:) l r x -> i
gsum_match (:+:) l r x -> i
fl FieldsType (FromJust ('Just k)) i
_k (L1 l x
tl) = (:+:) l r x -> i
fl (l x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 l x
tl)
  gsum_match (:+:) l r x -> i
fl FieldsType (FromJust ('Just k)) i
k (R1 r x
tr) = forall (c :: Symbol) (rep :: * -> *) x i.
GLeading c rep x =>
(rep x -> i) -> CFieldsType c (rep x) i -> rep x -> i
gmatch @c @r @x ((:+:) l r x -> i
fl ((:+:) l r x -> i) -> (r x -> (:+:) l r x) -> r x -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1) CFieldsType c (r x) i
FieldsType (FromJust ('Just k)) i
k r x
tr

  gsum_unmatch :: forall i. ((:+:) l r x -> i) -> FieldsType (FromJust ('Just k)) i
gsum_unmatch (:+:) l r x -> i
k = forall (c :: Symbol) (rep :: * -> *) x i.
GLeading c rep x =>
(rep x -> i) -> CFieldsType c (rep x) i
gunmatch @c @r @x ((:+:) l r x -> i
k ((:+:) l r x -> i) -> (r x -> (:+:) l r x) -> r x -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1)

class GProdLeading t x where
  gapply :: FieldsType (t x) i -> t x -> i
  gbuild :: (t x -> i) -> FieldsType (t x) i

-- gconstr :: FieldsType (t x) tgt

instance (GProdLeading l x, GProdLeading r x) => GProdLeading (l :*: r) x where
  gapply :: forall i. FieldsType ((:*:) l r x) i -> (:*:) l r x -> i
gapply FieldsType ((:*:) l r x) i
k (l x
l :*: r x
r) = FieldsType (r x) i -> r x -> i
forall i. FieldsType (r x) i -> r x -> i
forall {k} (t :: k -> *) (x :: k) i.
GProdLeading t x =>
FieldsType (t x) i -> t x -> i
gapply (FieldsType (l x) (FieldsType (r x) i) -> l x -> FieldsType (r x) i
forall i. FieldsType (l x) i -> l x -> i
forall {k} (t :: k -> *) (x :: k) i.
GProdLeading t x =>
FieldsType (t x) i -> t x -> i
gapply FieldsType (l x) (FieldsType (r x) i)
FieldsType ((:*:) l r x) i
k l x
l) r x
r
  gbuild :: forall i. ((:*:) l r x -> i) -> FieldsType ((:*:) l r x) i
gbuild ((:*:) l r x -> i
k :: (l :*: r) x -> i) = forall {k} (t :: k -> *) (x :: k) i.
GProdLeading t x =>
(t x -> i) -> FieldsType (t x) i
forall (t :: k -> *) (x :: k) i.
GProdLeading t x =>
(t x -> i) -> FieldsType (t x) i
gbuild @l @x @(FieldsType (r x) i) (\l x
l -> forall {k} (t :: k -> *) (x :: k) i.
GProdLeading t x =>
(t x -> i) -> FieldsType (t x) i
forall (t :: k -> *) (x :: k) i.
GProdLeading t x =>
(t x -> i) -> FieldsType (t x) i
gbuild @r @x @i (\r x
r -> (:*:) l r x -> i
k (l x
l l x -> r x -> (:*:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: r x
r)))

instance (GProdLeading f x) => GProdLeading (M1 i meta f) x where
  gapply :: forall i. FieldsType (M1 i meta f x) i -> M1 i meta f x -> i
gapply FieldsType (M1 i meta f x) i
k (M1 f x
x) = FieldsType (f x) i -> f x -> i
forall i. FieldsType (f x) i -> f x -> i
forall {k} (t :: k -> *) (x :: k) i.
GProdLeading t x =>
FieldsType (t x) i -> t x -> i
gapply FieldsType (f x) i
FieldsType (M1 i meta f x) i
k f x
x
  gbuild :: forall i. (M1 i meta f x -> i) -> FieldsType (M1 i meta f x) i
gbuild M1 i meta f x -> i
k = (f x -> i) -> FieldsType (f x) i
forall i. (f x -> i) -> FieldsType (f x) i
forall {k} (t :: k -> *) (x :: k) i.
GProdLeading t x =>
(t x -> i) -> FieldsType (t x) i
gbuild (M1 i meta f x -> i
k (M1 i meta f x -> i) -> (f x -> M1 i meta f x) -> f x -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> M1 i meta f x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1)

instance GProdLeading U1 x where
  gapply :: forall i. FieldsType (U1 x) i -> U1 x -> i
gapply FieldsType (U1 x) i
k U1 x
_ = i
FieldsType (U1 x) i
k
  gbuild :: forall i. (U1 x -> i) -> FieldsType (U1 x) i
gbuild U1 x -> i
k = U1 x -> i
k U1 x
forall k (p :: k). U1 p
U1

instance GProdLeading (K1 i t) x where
  gapply :: forall i. FieldsType (K1 i t x) i -> K1 i t x -> i
gapply FieldsType (K1 i t x) i
k (K1 t
t) = FieldsType (K1 i t x) i
t -> i
k t
t
  gbuild :: forall i. (K1 i t x -> i) -> FieldsType (K1 i t x) i
gbuild K1 i t x -> i
k = K1 i t x -> i
k (K1 i t x -> i) -> (t -> K1 i t x) -> t -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> K1 i t x
forall k i c (p :: k). c -> K1 i c p
K1

type SelectConstructor :: Symbol -> Type -> Maybe Type
type family SelectConstructor c rep where
  SelectConstructor c (C1 ('MetaCons c _ _) f p) = 'Just (f p)
  SelectConstructor c (C1 ('MetaCons _ _ _) _ _) = 'Nothing
  SelectConstructor c ((f :+: g) p) = SelectConstructor c (f p) <|> SelectConstructor c (g p)
  SelectConstructor c (V1 _) = 'Nothing
  SelectConstructor c (M1 _ _ f p) = SelectConstructor c (f p)
  SelectConstructor _ _ = TypeError ('Text "SelectConstructor: unexpected representation")

type (<|>) :: Maybe k -> Maybe k -> Maybe k
type family x <|> y where
  ('Just v) <|> _ = 'Just v
  'Nothing <|> y = y

type IsJust :: Maybe k -> Bool
type family IsJust x where
  IsJust ('Just v) = 'True
  IsJust 'Nothing = 'False

type FromJust :: Maybe k -> k
type family FromJust x where
  FromJust ('Just v) = v
  FromJust 'Nothing = TypeError ('Text "FromJust: This constructor doesn't seem to exist")

type FieldsType :: Type -> Type -> Type
type family FieldsType rep tgt where
  -- FieldsType (S1 _ f p) tgt = StripMetadata (f p) -> tgt
  FieldsType (U1 _) tgt = tgt
  FieldsType ((f :*: g) p) tgt = FieldsType (f p) (FieldsType (g p) tgt)
  FieldsType (M1 _ _ f p) tgt = FieldsType (f p) tgt
  FieldsType (K1 _ c _) tgt = c -> tgt
  FieldsType _ _ = TypeError ('Text "FieldsType: unexpected representation")

type family CFieldsType c rep tgt where
  CFieldsType c rep tgt = FieldsType (FromJust (SelectConstructor c rep)) tgt

------------------------------------------------------------------------------
--
-- Error messages
--
------------------------------------------------------------------------------

-- See https://blog.csongor.co.uk/report-stuck-families/ and
-- https://hackage.haskell.org/package/generic-lens-core-2.2.1.0/docs/Data-Generics-Internal-Errors.html#t:Defined
type family Defined (break :: Type -> Type) (err :: Constraint) (a :: k) :: k where
  Defined Apart _ _ = Daemon
  Defined _ _ k = k

data Apart a

type family Daemon :: k