{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- |
-- Module      : Data.Type.Functor.XProduct
-- Copyright   : (c) Justin Le 2018
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Generalize "Data.Vinyl.XRec": provides a version of products in
-- "Data.Type.Functor.Product" that "erases" newtype wrappers and other
-- syntactical noise.
--
-- "Data.Type.Functor.Product" is the "main functionality", but this module
-- provides an alternative interface that may be more convenient in some
-- situations, in the same way that 'XRec' can be more convenient than
-- 'Rec' in some situations.
module Data.Type.Functor.XProduct (
  XProd,
  fromXProd,
  toXProd,

  -- * Functions
  mapProdX,
  mapProdXEndo,
  imapProdX,
  zipWithProdX,
  ixProdX,
  traverseProdX,
  traverseProdXEndo,
  itraverseProdX,
  foldMapProdX,
  ifoldMapProdX,

  -- * Instances
  XRec,
  pattern (::&),
  pattern XRNil,
  XMaybe,
  pattern XNothing,
  pattern XJust,
  XEither,
  pattern XLeft,
  pattern XRight,
  XNERec,
  pattern (::&|),
  XTup,
  pattern XTup,
  XIdentity,
  pattern XIdentity,
) where

import Data.Functor.Identity
import Data.Kind
import Data.List.NonEmpty (NonEmpty (..))
import Data.Singletons
import Data.Type.Functor.Product
import Data.Vinyl
import qualified Data.Vinyl.Functor as V
import Data.Vinyl.XRec
import Lens.Micro

-- | Generalize 'XRec' to work over any foldable @f@ that implements
-- 'FProd'.  See 'Prod' and 'FProd' for more information.
type XProd f g = (Prod f (XData g) :: f k -> Type)

-- | Convert an 'XProd' back into a regular ol' 'Prod'.
fromXProd :: forall f g as. (FProd f, PureProdC f (IsoHKD g) as) => XProd f g as -> Prod f g as
fromXProd :: forall {k} (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, PureProdC f (IsoHKD g) as) =>
XProd f g as -> Prod f g as
fromXProd =
  (forall (a :: k). Lift (->) (XData g) g a -> XData g a -> g a)
-> Prod f (Lift (->) (XData g) g) as
-> Prod f (XData g) as
-> Prod f g as
forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *) (as :: f k).
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd
    (\(V.Lift XData g a -> g a
u) XData g a
x -> XData g a -> g a
u XData g a
x)
    (forall {k} (f :: * -> *) (c :: k -> Constraint) (as :: f k)
       (g :: k -> *).
PureProdC f c as =>
(forall (a :: k). c a => g a) -> Prod f g as
forall (f :: * -> *) (c :: k -> Constraint) (as :: f k)
       (g :: k -> *).
PureProdC f c as =>
(forall (a :: k). c a => g a) -> Prod f g as
pureProdC @_ @(IsoHKD g) ((XData g a -> g a) -> Lift (->) (XData g) g a
forall l l' k (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l')
       (x :: k).
op (f x) (g x) -> Lift op f g x
V.Lift (HKD g a -> g a
forall {k} (f :: k -> *) (a :: k). IsoHKD f a => HKD f a -> f a
unHKD (HKD g a -> g a) -> (XData g a -> HKD g a) -> XData g a -> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XData g a -> HKD g a
forall {k} (t :: k -> *) (a :: k). XData t a -> HKD t a
unX)))

-- | Convert a 'Prod' into a fancy 'XProd'.
toXProd :: forall f g as. (FProd f, PureProdC f (IsoHKD g) as) => Prod f g as -> XProd f g as
toXProd :: forall {k} (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, PureProdC f (IsoHKD g) as) =>
Prod f g as -> XProd f g as
toXProd =
  (forall (a :: k). Lift (->) g (XData g) a -> g a -> XData g a)
-> Prod f (Lift (->) g (XData g)) as
-> Prod f g as
-> Prod f (XData g) as
forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *) (as :: f k).
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd
    (\(V.Lift g a -> XData g a
u) g a
x -> g a -> XData g a
u g a
x)
    (forall {k} (f :: * -> *) (c :: k -> Constraint) (as :: f k)
       (g :: k -> *).
PureProdC f c as =>
(forall (a :: k). c a => g a) -> Prod f g as
forall (f :: * -> *) (c :: k -> Constraint) (as :: f k)
       (g :: k -> *).
PureProdC f c as =>
(forall (a :: k). c a => g a) -> Prod f g as
pureProdC @_ @(IsoHKD g) ((g a -> XData g a) -> Lift (->) g (XData g) a
forall l l' k (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l')
       (x :: k).
op (f x) (g x) -> Lift op f g x
V.Lift (HKD g a -> XData g a
forall {k} (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD g a -> XData g a) -> (g a -> HKD g a) -> g a -> XData g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> HKD g a
forall {k} (f :: k -> *) (a :: k). IsoHKD f a => f a -> HKD f a
toHKD)))

-- | Convenient wrapper over 'mapProd' that lets you deal with the
-- "simplified" inner types.  Generalizes 'rmapX'.
mapProdX ::
  forall f g h as.
  FProd f =>
  (forall a. HKD g a -> HKD h a) ->
  XProd f g as ->
  XProd f h as
mapProdX :: forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). HKD g a -> HKD h a)
-> XProd f g as -> XProd f h as
mapProdX forall (a :: k). HKD g a -> HKD h a
f = (forall (a :: k). XData g a -> XData h a)
-> Prod f (XData g) as -> Prod f (XData h) as
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((forall (a :: k). XData g a -> XData h a)
 -> Prod f (XData g) as -> Prod f (XData h) as)
-> (forall (a :: k). XData g a -> XData h a)
-> Prod f (XData g) as
-> Prod f (XData h) as
forall a b. (a -> b) -> a -> b
$ \(XData HKD g a
x :: XData g a) -> HKD h a -> XData h a
forall {k} (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (forall (a :: k). HKD g a -> HKD h a
f @a HKD g a
x)

-- | A version of 'mapProdX' that doesn't change the context @g@; this can
-- be easier for type inference in some situations.  Generalizes
-- 'rmapXEndo'.
mapProdXEndo ::
  forall f g as.
  FProd f =>
  (forall a. HKD g a -> HKD g a) ->
  XProd f g as ->
  XProd f g as
mapProdXEndo :: forall {k} (f :: * -> *) (g :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). HKD g a -> HKD g a)
-> XProd f g as -> XProd f g as
mapProdXEndo forall (a :: k). HKD g a -> HKD g a
f = (forall (a :: k). XData g a -> XData g a)
-> Prod f (XData g) as -> Prod f (XData g) as
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((forall (a :: k). XData g a -> XData g a)
 -> Prod f (XData g) as -> Prod f (XData g) as)
-> (forall (a :: k). XData g a -> XData g a)
-> Prod f (XData g) as
-> Prod f (XData g) as
forall a b. (a -> b) -> a -> b
$ \(XData HKD g a
x :: XData g a) -> HKD g a -> XData g a
forall {k} (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (forall (a :: k). HKD g a -> HKD g a
f @a HKD g a
x)

-- | A version of 'mapProdX' that passes along the index 'Elem' with each
-- value.  This can help with type inference in some situations.
imapProdX ::
  forall f g h as.
  FProd f =>
  (forall a. Elem f as a -> HKD g a -> HKD h a) ->
  XProd f g as ->
  XProd f h as
imapProdX :: forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). Elem f as a -> HKD g a -> HKD h a)
-> XProd f g as -> XProd f h as
imapProdX forall (a :: k). Elem f as a -> HKD g a -> HKD h a
f = (forall (a :: k). Elem f as a -> XData g a -> XData h a)
-> Prod f (XData g) as -> Prod f (XData h) as
forall {k} (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *).
FProd f =>
(forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd ((forall (a :: k). Elem f as a -> XData g a -> XData h a)
 -> Prod f (XData g) as -> Prod f (XData h) as)
-> (forall (a :: k). Elem f as a -> XData g a -> XData h a)
-> Prod f (XData g) as
-> Prod f (XData h) as
forall a b. (a -> b) -> a -> b
$ \Elem f as a
i -> HKD h a -> XData h a
forall {k} (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD h a -> XData h a)
-> (XData g a -> HKD h a) -> XData g a -> XData h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elem f as a -> HKD g a -> HKD h a
forall (a :: k). Elem f as a -> HKD g a -> HKD h a
f Elem f as a
i (HKD g a -> HKD h a)
-> (XData g a -> HKD g a) -> XData g a -> HKD h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XData g a -> HKD g a
forall {k} (t :: k -> *) (a :: k). XData t a -> HKD t a
unX

-- | Zip two 'XProd's together by supplying a function that works on their
-- simplified 'HKD' values.
zipWithProdX ::
  forall f g h j as.
  FProd f =>
  (forall a. HKD g a -> HKD h a -> HKD j a) ->
  XProd f g as ->
  XProd f h as ->
  XProd f j as
zipWithProdX :: forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: f k).
FProd f =>
(forall (a :: k). HKD g a -> HKD h a -> HKD j a)
-> XProd f g as -> XProd f h as -> XProd f j as
zipWithProdX forall (a :: k). HKD g a -> HKD h a -> HKD j a
f = (forall (a :: k). XData g a -> XData h a -> XData j a)
-> Prod f (XData g) as
-> Prod f (XData h) as
-> Prod f (XData j) as
forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *) (as :: f k).
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd ((forall (a :: k). XData g a -> XData h a -> XData j a)
 -> Prod f (XData g) as
 -> Prod f (XData h) as
 -> Prod f (XData j) as)
-> (forall (a :: k). XData g a -> XData h a -> XData j a)
-> Prod f (XData g) as
-> Prod f (XData h) as
-> Prod f (XData j) as
forall a b. (a -> b) -> a -> b
$ \(XData HKD g a
x :: XData g a) (XData HKD h a
y) -> HKD j a -> XData j a
forall {k} (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (forall (a :: k). HKD g a -> HKD h a -> HKD j a
f @a HKD g a
x HKD h a
y)

-- | Given an index into an 'XProd', provides a lens into the simplified
-- item that that index points to.
ixProdX ::
  FProd f =>
  Elem f as a ->
  Lens' (XProd f g as) (HKD g a)
ixProdX :: forall {k} (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Lens' (XProd f g as) (HKD g a)
ixProdX Elem f as a
i = Elem f as a -> Lens' (Prod f (XData g) as) (XData g a)
forall {k} (as :: f k) (a :: k) (g :: k -> *).
Elem f as a -> Lens' (Prod f g as) (g a)
forall (f :: * -> *) {k} (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Lens' (Prod f g as) (g a)
ixProd Elem f as a
i ((XData g a -> f (XData g a))
 -> Prod f (XData g) as -> f (Prod f (XData g) as))
-> ((HKD g a -> f (HKD g a)) -> XData g a -> f (XData g a))
-> (HKD g a -> f (HKD g a))
-> Prod f (XData g) as
-> f (Prod f (XData g) as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\HKD g a -> f (HKD g a)
f (XData HKD g a
x) -> HKD g a -> XData g a
forall {k} (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD g a -> XData g a) -> f (HKD g a) -> f (XData g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HKD g a -> f (HKD g a)
f HKD g a
x)

-- | Convenient wrapper over 'traverseProd' that lets you deal with the
-- "simplified" inner types.
traverseProdX ::
  forall f g h m as.
  (FProd f, Applicative m) =>
  (forall a. HKD g a -> m (HKD h a)) ->
  XProd f g as ->
  m (XProd f h as)
traverseProdX :: forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (m :: * -> *)
       (as :: f k).
(FProd f, Applicative m) =>
(forall (a :: k). HKD g a -> m (HKD h a))
-> XProd f g as -> m (XProd f h as)
traverseProdX forall (a :: k). HKD g a -> m (HKD h a)
f = (forall (a :: k). XData g a -> m (XData h a))
-> Prod f (XData g) as -> m (Prod f (XData h) as)
forall {k} (g :: k -> *) (h :: k -> *) (as :: f k) (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (as :: f k)
       (m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd ((forall (a :: k). XData g a -> m (XData h a))
 -> Prod f (XData g) as -> m (Prod f (XData h) as))
-> (forall (a :: k). XData g a -> m (XData h a))
-> Prod f (XData g) as
-> m (Prod f (XData h) as)
forall a b. (a -> b) -> a -> b
$ \(XData HKD g a
x :: XData g a) -> HKD h a -> XData h a
forall {k} (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD h a -> XData h a) -> m (HKD h a) -> m (XData h a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). HKD g a -> m (HKD h a)
f @a HKD g a
x

-- | A version of 'traverseProdX' that doesn't change the context @g@; this can
-- be easier for type inference in some situations.
traverseProdXEndo ::
  forall f g m as.
  (FProd f, Applicative m) =>
  (forall a. HKD g a -> m (HKD g a)) ->
  XProd f g as ->
  m (XProd f g as)
traverseProdXEndo :: forall {k} (f :: * -> *) (g :: k -> *) (m :: * -> *) (as :: f k).
(FProd f, Applicative m) =>
(forall (a :: k). HKD g a -> m (HKD g a))
-> XProd f g as -> m (XProd f g as)
traverseProdXEndo forall (a :: k). HKD g a -> m (HKD g a)
f = (forall (a :: k). XData g a -> m (XData g a))
-> Prod f (XData g) as -> m (Prod f (XData g) as)
forall {k} (g :: k -> *) (h :: k -> *) (as :: f k) (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (as :: f k)
       (m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd ((forall (a :: k). XData g a -> m (XData g a))
 -> Prod f (XData g) as -> m (Prod f (XData g) as))
-> (forall (a :: k). XData g a -> m (XData g a))
-> Prod f (XData g) as
-> m (Prod f (XData g) as)
forall a b. (a -> b) -> a -> b
$ \(XData HKD g a
x :: XData g a) -> HKD g a -> XData g a
forall {k} (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD g a -> XData g a) -> m (HKD g a) -> m (XData g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). HKD g a -> m (HKD g a)
f @a HKD g a
x

-- | A version of 'traverseProdX' that passes along the index 'Elem' with
-- each value.  This can help with type inference in some situations.
itraverseProdX ::
  forall f g h m as.
  (FProd f, Applicative m) =>
  (forall a. Elem f as a -> HKD g a -> m (HKD h a)) ->
  XProd f g as ->
  m (XProd f h as)
itraverseProdX :: forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (m :: * -> *)
       (as :: f k).
(FProd f, Applicative m) =>
(forall (a :: k). Elem f as a -> HKD g a -> m (HKD h a))
-> XProd f g as -> m (XProd f h as)
itraverseProdX forall (a :: k). Elem f as a -> HKD g a -> m (HKD h a)
f = (forall (a :: k). Elem f as a -> XData g a -> m (XData h a))
-> Prod f (XData g) as -> m (Prod f (XData h) as)
forall {k} (f :: * -> *) (m :: * -> *) (as :: f k) (g :: k -> *)
       (h :: k -> *).
(FProd f, Applicative m) =>
(forall (a :: k). Elem f as a -> g a -> m (h a))
-> Prod f g as -> m (Prod f h as)
itraverseProd ((forall (a :: k). Elem f as a -> XData g a -> m (XData h a))
 -> Prod f (XData g) as -> m (Prod f (XData h) as))
-> (forall (a :: k). Elem f as a -> XData g a -> m (XData h a))
-> Prod f (XData g) as
-> m (Prod f (XData h) as)
forall a b. (a -> b) -> a -> b
$ \Elem f as a
i -> (HKD h a -> XData h a) -> m (HKD h a) -> m (XData h a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HKD h a -> XData h a
forall {k} (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (m (HKD h a) -> m (XData h a))
-> (XData g a -> m (HKD h a)) -> XData g a -> m (XData h a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elem f as a -> HKD g a -> m (HKD h a)
forall (a :: k). Elem f as a -> HKD g a -> m (HKD h a)
f Elem f as a
i (HKD g a -> m (HKD h a))
-> (XData g a -> HKD g a) -> XData g a -> m (HKD h a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XData g a -> HKD g a
forall {k} (t :: k -> *) (a :: k). XData t a -> HKD t a
unX

-- | Convenient wrapper over 'foldMapProd' that lets you deal with the
-- "simplified" inner types.
foldMapProdX ::
  forall f g m as.
  (FProd f, Monoid m) =>
  (forall a. HKD g a -> m) ->
  XProd f g as ->
  m
foldMapProdX :: forall {k} (f :: * -> *) (g :: k -> *) m (as :: f k).
(FProd f, Monoid m) =>
(forall (a :: k). HKD g a -> m) -> XProd f g as -> m
foldMapProdX forall (a :: k). HKD g a -> m
f = (forall (a :: k). XData g a -> m) -> Prod f (XData g) as -> m
forall {k} (f :: * -> *) m (g :: k -> *) (as :: f k).
(FProd f, Monoid m) =>
(forall (a :: k). g a -> m) -> Prod f g as -> m
foldMapProd ((forall (a :: k). XData g a -> m) -> Prod f (XData g) as -> m)
-> (forall (a :: k). XData g a -> m) -> Prod f (XData g) as -> m
forall a b. (a -> b) -> a -> b
$ \(XData HKD g a
x :: XData g a) -> forall (a :: k). HKD g a -> m
f @a HKD g a
x

-- | A version of 'foldMapProdX' that passes along the index 'Elem' with
-- each value.  This can help with type inference in some situations.
ifoldMapProdX ::
  forall f g m as.
  (FProd f, Monoid m) =>
  (forall a. Elem f as a -> HKD g a -> m) ->
  XProd f g as ->
  m
ifoldMapProdX :: forall {k} (f :: * -> *) (g :: k -> *) m (as :: f k).
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> HKD g a -> m) -> XProd f g as -> m
ifoldMapProdX forall (a :: k). Elem f as a -> HKD g a -> m
f = (forall (a :: k). Elem f as a -> XData g a -> m)
-> Prod f (XData g) as -> m
forall {k} (f :: * -> *) m (as :: f k) (g :: k -> *).
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
ifoldMapProd ((forall (a :: k). Elem f as a -> XData g a -> m)
 -> Prod f (XData g) as -> m)
-> (forall (a :: k). Elem f as a -> XData g a -> m)
-> Prod f (XData g) as
-> m
forall a b. (a -> b) -> a -> b
$ \Elem f as a
i -> Elem f as a -> HKD g a -> m
forall (a :: k). Elem f as a -> HKD g a -> m
f Elem f as a
i (HKD g a -> m) -> (XData g a -> HKD g a) -> XData g a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XData g a -> HKD g a
forall {k} (t :: k -> *) (a :: k). XData t a -> HKD t a
unX

-- | 'PMaybe' over 'HKD'-d types.
type XMaybe f = PMaybe (XData f)

-- | 'PEither' over 'HKD'-d types.
type XEither f = PEither (XData f)

-- | 'NERec' over 'HKD'-d types.
type XNERec f = NERec (XData f)

-- | 'PTup' over 'HKD'-d types.
type XTup f = PTup (XData f)

-- | 'PIdentity' over 'HKD'-d types.
type XIdentity f = PIdentity (XData f)

-- | 'PNothing' for 'XMaybe'.
pattern XNothing :: XMaybe f 'Nothing
pattern $mXNothing :: forall {r} {k} {f :: k -> *}.
XMaybe f 'Nothing -> ((# #) -> r) -> ((# #) -> r) -> r
$bXNothing :: forall {k} (f :: k -> *). XMaybe f 'Nothing
XNothing = PNothing

-- | 'PJust' for 'XMaybe': allows you to provide the simplified type.
pattern XJust :: HKD f a -> XMaybe f ('Just a)
pattern $mXJust :: forall {r} {a1} {f :: a1 -> *} {a2 :: a1}.
XMaybe f ('Just a2) -> (HKD f a2 -> r) -> ((# #) -> r) -> r
$bXJust :: forall {a1} (f :: a1 -> *) (a2 :: a1).
HKD f a2 -> XMaybe f ('Just a2)
XJust x = PJust (XData x)

-- | 'PLeft' for 'XEither'.
pattern XLeft :: Sing e -> XEither f ('Left e)
pattern $mXLeft :: forall {r} {j} {k} {e :: j} {f :: k -> *}.
XEither f ('Left e) -> (Sing e -> r) -> ((# #) -> r) -> r
$bXLeft :: forall {j} {k} (e :: j) (f :: k -> *).
Sing e -> XEither f ('Left e)
XLeft e = PLeft e

-- | 'PRight' for 'XEither': allows you to provide the simplified type.
pattern XRight :: HKD f a -> XEither f ('Right a)
pattern $mXRight :: forall {r} {b} {j} {f :: b -> *} {a :: b}.
XEither f ('Right a) -> (HKD f a -> r) -> ((# #) -> r) -> r
$bXRight :: forall {b} {j} (f :: b -> *) (a :: b).
HKD f a -> XEither f ('Right a)
XRight x = PRight (XData x)

-- | A version of ':&|' that allows you to provide the simplified type, for
-- 'XNERec'.
pattern (::&|) :: HKD f a -> XRec f as -> XNERec f (a ':| as)
pattern x $m::&| :: forall {r} {a1} {f :: a1 -> *} {a2 :: a1} {as :: [a1]}.
XNERec f (a2 ':| as)
-> (HKD f a2 -> XRec f as -> r) -> ((# #) -> r) -> r
$b::&| :: forall {a1} (f :: a1 -> *) (a2 :: a1) (as :: [a1]).
HKD f a2 -> XRec f as -> XNERec f (a2 ':| as)
::&| xs = XData x :&| xs

-- | A version of 'PTup' that allows you to provide the simplified type,
-- for 'XTup'.
pattern XTup :: Sing w -> HKD f a -> XTup f '(w, a)
pattern $mXTup :: forall {r} {j} {k} {w :: j} {f :: k -> *} {a :: k}.
XTup f '(w, a) -> (Sing w -> HKD f a -> r) -> ((# #) -> r) -> r
$bXTup :: forall {j} {k} (w :: j) (f :: k -> *) (a :: k).
Sing w -> HKD f a -> XTup f '(w, a)
XTup w x = PTup w (XData x)

-- | A version of 'PIdentity' that allows you to provide the simplified
-- type, for 'XIdentity'.
pattern XIdentity :: HKD f a -> XIdentity f ('Identity a)
pattern $mXIdentity :: forall {r} {a1} {f :: a1 -> *} {a2 :: a1}.
XIdentity f ('Identity a2) -> (HKD f a2 -> r) -> ((# #) -> r) -> r
$bXIdentity :: forall {a1} (f :: a1 -> *) (a2 :: a1).
HKD f a2 -> XIdentity f ('Identity a2)
XIdentity x = PIdentity (XData x)

{-# COMPLETE (::&|) #-}
{-# COMPLETE XIdentity #-}
{-# COMPLETE XJust #-}
{-# COMPLETE XLeft #-}
{-# COMPLETE XNothing #-}
{-# COMPLETE XRight #-}
{-# COMPLETE XTup #-}