{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
module Data.Functor.Polynomial.Class(
  Polynomial(..),
) where

import Data.Functor.Identity(Identity(..))
import Data.Functor.Const
import Data.Proxy
import Data.Functor.Sum
import Data.Functor.Product
import Data.Functor.Compose
import Data.Functor.Day

import GHC.Generics
import Data.Coerce (coerce)
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))

import Data.Finitary
import qualified Data.Vector.Sized as SV

import Data.Functor.Pow
import Data.Functor.Polynomial.Tag
import Data.Functor.Polynomial
import Data.Void
import Data.GADT.HasFinitary (toInhabitants)
import GHC.TypeNats.Extra (SNat(SNat))

-- | A class for 'Functor' which can be represented as 'Poly'.
--   
--   'toPoly' and 'fromPoly' are isomorphisms.
--   
--   > toPoly . fromPoly = id
--   > fromPoly . toPoly = id
class (Functor f) => Polynomial f where
  type Tag f :: Type -> Type

  toPoly :: f x -> Poly (Tag f) x
  fromPoly :: Poly (Tag f) x -> f x

instance Polynomial ((->) r) where
  type Tag ((->) r) = (:~:) r

  toPoly :: forall x. (r -> x) -> Poly (Tag ((->) r)) x
toPoly = (r :~: r) -> (r -> x) -> Poly ((:~:) r) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P r :~: r
forall {k} (a :: k). a :~: a
Refl
  fromPoly :: forall x. Poly (Tag ((->) r)) x -> r -> x
fromPoly (P r :~: n
Tag ((->) r) n
Refl n -> x
f) = r -> x
n -> x
f

---- Instances ----
instance Polynomial Maybe where
  type Tag Maybe = TagMaybe

  toPoly :: forall x. Maybe x -> Poly (Tag Maybe) x
toPoly Maybe x
mx = case Maybe x
mx of
    Maybe x
Nothing -> TagMaybe Void -> (Void -> x) -> Poly TagMaybe x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P TagMaybe Void
TagNothing Void -> x
forall a. Void -> a
absurd
    Just x
x  -> TagMaybe () -> (() -> x) -> Poly TagMaybe x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P TagMaybe ()
TagJust (x -> () -> x
forall a b. a -> b -> a
const x
x)
  fromPoly :: forall x. Poly (Tag Maybe) x -> Maybe x
fromPoly (P Tag Maybe n
tag n -> x
rep) = case Tag Maybe n
tag of
    TagMaybe n
Tag Maybe n
TagNothing -> Maybe x
forall a. Maybe a
Nothing
    TagMaybe n
Tag Maybe n
TagJust -> x -> Maybe x
forall a. a -> Maybe a
Just (n -> x
rep ())

instance Polynomial [] where
  type Tag [] = TagList

  toPoly :: forall x. [x] -> Poly TagList x
  toPoly :: forall x. [x] -> Poly TagList x
toPoly [x]
xs = [x]
-> (forall {n :: Nat}. KnownNat n => Vector n x -> Poly TagList x)
-> Poly TagList x
forall a r.
[a] -> (forall (n :: Nat). KnownNat n => Vector n a -> r) -> r
SV.withSizedList [x]
xs ((forall {n :: Nat}. KnownNat n => Vector n x -> Poly TagList x)
 -> Poly TagList x)
-> (forall {n :: Nat}. KnownNat n => Vector n x -> Poly TagList x)
-> Poly TagList x
forall a b. (a -> b) -> a -> b
$ \Vector n x
v -> TagList (Finite Integer n)
-> (Finite Integer n -> x) -> Poly TagList x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P TagList (Finite Integer n)
forall (n :: Nat). KnownNat n => TagList (Finite Integer n)
TagList (Vector n x -> Finite Integer n -> x
forall (n :: Nat) a. Vector n a -> Finite n -> a
SV.index Vector n x
v)

  fromPoly :: forall x. Poly TagList x -> [x]
  fromPoly :: forall x. Poly TagList x -> [x]
fromPoly (P TagList n
sn n -> x
f) = n -> x
f (n -> x) -> [n] -> [x]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> TagList n -> [n]
forall (tag :: Type -> Type) a. HasFinitary tag => tag a -> [a]
toInhabitants TagList n
sn

instance Polynomial V1 where
  type Tag V1 = TagV
  toPoly :: forall x. V1 x -> Poly (Tag V1) x
toPoly V1 x
v = case V1 x
v of { }
  fromPoly :: forall x. Poly (Tag V1) x -> V1 x
fromPoly (P Tag V1 n
v n -> x
_) = case Tag V1 n
v of { }

instance Polynomial U1 where
  type Tag U1 = TagFn Void

  toPoly :: forall x. U1 x -> Poly (Tag U1) x
toPoly U1 x
_ = (Void :~: Void) -> (Void -> x) -> Poly ((:~:) Void) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P Void :~: Void
forall {k} (a :: k). a :~: a
Refl Void -> x
forall a. Void -> a
absurd
  fromPoly :: forall x. Poly (Tag U1) x -> U1 x
fromPoly Poly (Tag U1) x
_ = U1 x
forall k (p :: k). U1 p
U1

instance Polynomial Proxy where
  type Tag Proxy = TagFn Void

  toPoly :: forall x. Proxy x -> Poly (Tag Proxy) x
toPoly Proxy x
_ = (Void :~: Void) -> (Void -> x) -> Poly ((:~:) Void) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P Void :~: Void
forall {k} (a :: k). a :~: a
Refl Void -> x
forall a. Void -> a
absurd
  fromPoly :: forall x. Poly (Tag Proxy) x -> Proxy x
fromPoly Poly (Tag Proxy) x
_ = Proxy x
forall {k} (t :: k). Proxy t
Proxy

instance Polynomial (K1 i c) where
  type Tag (K1 i c) = TagK c

  toPoly :: forall x. K1 i c x -> Poly (Tag (K1 i c)) x
toPoly (K1 c
c) = TagK c Void -> (Void -> x) -> Poly (TagK c) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P (c -> TagK c Void
forall c. c -> TagK c Void
TagK c
c) Void -> x
forall a. Void -> a
absurd
  fromPoly :: forall x. Poly (Tag (K1 i c)) x -> K1 i c x
fromPoly (P (TagK c
c) n -> x
_) = c -> K1 i c x
forall k i c (p :: k). c -> K1 i c p
K1 c
c

instance Polynomial (Const c) where
  type Tag (Const c) = TagK c

  toPoly :: forall x. Const c x -> Poly (Tag (Const c)) x
toPoly (Const c
c) = TagK c Void -> (Void -> x) -> Poly (TagK c) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P (c -> TagK c Void
forall c. c -> TagK c Void
TagK c
c) Void -> x
forall a. Void -> a
absurd
  fromPoly :: forall x. Poly (Tag (Const c)) x -> Const c x
fromPoly (P (TagK c
c) n -> x
_) = c -> Const c x
forall {k} a (b :: k). a -> Const a b
Const c
c

instance Polynomial f => Polynomial (M1 i c f) where
  type Tag (M1 i c f) = Tag f
  fromPoly :: forall x. Poly (Tag (M1 i c f)) x -> M1 i c f x
fromPoly = f x -> M1 i c f x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (f x -> M1 i c f x)
-> (Poly (Tag f) x -> f x) -> Poly (Tag f) x -> M1 i c f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly (Tag f) x -> f x
forall x. Poly (Tag f) x -> f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly
  toPoly :: forall x. M1 i c f x -> Poly (Tag (M1 i c f)) x
toPoly = f x -> Poly (Tag f) x
forall x. f x -> Poly (Tag f) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly (f x -> Poly (Tag f) x)
-> (M1 i c f x -> f x) -> M1 i c f x -> Poly (Tag f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f x -> f x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1

instance Polynomial f => Polynomial (Rec1 f) where
  type Tag (Rec1 f) = Tag f
  fromPoly :: forall x. Poly (Tag (Rec1 f)) x -> Rec1 f x
fromPoly = f x -> Rec1 f x
forall k (f :: k -> Type) (p :: k). f p -> Rec1 f p
Rec1 (f x -> Rec1 f x)
-> (Poly (Tag f) x -> f x) -> Poly (Tag f) x -> Rec1 f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly (Tag f) x -> f x
forall x. Poly (Tag f) x -> f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly
  toPoly :: forall x. Rec1 f x -> Poly (Tag (Rec1 f)) x
toPoly = f x -> Poly (Tag f) x
forall x. f x -> Poly (Tag f) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly (f x -> Poly (Tag f) x)
-> (Rec1 f x -> f x) -> Rec1 f x -> Poly (Tag f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec1 f x -> f x
forall k (f :: k -> Type) (p :: k). Rec1 f p -> f p
unRec1

instance Polynomial Par1 where
  type Tag Par1 = TagFn ()

  toPoly :: forall x. Par1 x -> Poly (Tag Par1) x
toPoly (Par1 x
x) = (() :~: ()) -> (() -> x) -> Poly ((:~:) ()) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P () :~: ()
forall {k} (a :: k). a :~: a
Refl (x -> () -> x
forall a b. a -> b -> a
const x
x)
  fromPoly :: forall x. Poly (Tag Par1) x -> Par1 x
fromPoly (P () :~: n
Tag Par1 n
Refl n -> x
x') = x -> Par1 x
forall p. p -> Par1 p
Par1 (n -> x
x' ())

instance Polynomial Identity where
  type Tag Identity = TagFn ()

  toPoly :: forall x. Identity x -> Poly (Tag Identity) x
toPoly (Identity x
x) = (() :~: ()) -> (() -> x) -> Poly ((:~:) ()) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P () :~: ()
forall {k} (a :: k). a :~: a
Refl (x -> () -> x
forall a b. a -> b -> a
const x
x)
  fromPoly :: forall x. Poly (Tag Identity) x -> Identity x
fromPoly (P () :~: n
Tag Identity n
Refl n -> x
e) = x -> Identity x
forall a. a -> Identity a
Identity (n -> x
e ())

instance (Polynomial f, Polynomial g) => Polynomial (f :+: g) where
  type Tag (f :+: g) = TagSum (Tag f) (Tag g)

  toPoly :: forall x. (:+:) f g x -> Poly (Tag (f :+: g)) x
toPoly (L1 f x
fx) = case f x -> Poly (Tag f) x
forall x. f x -> Poly (Tag f) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly f x
fx of
    P Tag f n
tag n -> x
rep -> (:+:) (Tag f) (Tag g) n -> (n -> x) -> Poly (Tag f :+: Tag g) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P (Tag f n -> (:+:) (Tag f) (Tag g) n
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 Tag f n
tag) n -> x
rep
  toPoly (R1 g x
gx) = case g x -> Poly (Tag g) x
forall x. g x -> Poly (Tag g) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly g x
gx of
    P Tag g n
tag n -> x
rep -> (:+:) (Tag f) (Tag g) n -> (n -> x) -> Poly (Tag f :+: Tag g) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P (Tag g n -> (:+:) (Tag f) (Tag g) n
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 Tag g n
tag) n -> x
rep

  fromPoly :: forall x. Poly (Tag (f :+: g)) x -> (:+:) f g x
fromPoly (P (L1 Tag f n
tag) n -> x
rep) = f x -> (:+:) f g x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (Poly (Tag f) x -> f x
forall x. Poly (Tag f) x -> f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (Tag f n -> (n -> x) -> Poly (Tag f) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P Tag f n
tag n -> x
rep))
  fromPoly (P (R1 Tag g n
tag) n -> x
rep) = g x -> (:+:) f g x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (Poly (Tag g) x -> g x
forall x. Poly (Tag g) x -> g x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (Tag g n -> (n -> x) -> Poly (Tag g) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P Tag g n
tag n -> x
rep))

instance (Polynomial f, Polynomial g) => Polynomial (Sum f g) where
  type Tag (Sum f g) = TagSum (Tag f) (Tag g)

  toPoly :: forall x. Sum f g x -> Poly (Tag (Sum f g)) x
toPoly = (:+:) f g x -> Poly (TagSum (Tag f) (Tag g)) x
(:+:) f g x -> Poly (Tag (f :+: g)) x
forall x. (:+:) f g x -> Poly (Tag (f :+: g)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly ((:+:) f g x -> Poly (TagSum (Tag f) (Tag g)) x)
-> (Sum f g x -> (:+:) f g x)
-> Sum f g x
-> Poly (TagSum (Tag f) (Tag g)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sum f g x -> (:+:) f g x
forall {k} {f :: k -> Type} {g :: k -> Type} {p :: k}.
Sum f g p -> (:+:) f g p
toGenerics
    where
      toGenerics :: Sum f g p -> (:+:) f g p
toGenerics (InL f p
fx) = f p -> (:+:) f g p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 f p
fx
      toGenerics (InR g p
gx) = g p -> (:+:) f g p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 g p
gx

  fromPoly :: forall x. Poly (Tag (Sum f g)) x -> Sum f g x
fromPoly = (:+:) f g x -> Sum f g x
forall {k} {f :: k -> Type} {g :: k -> Type} {a :: k}.
(:+:) f g a -> Sum f g a
fromGenerics ((:+:) f g x -> Sum f g x)
-> (Poly (TagSum (Tag f) (Tag g)) x -> (:+:) f g x)
-> Poly (TagSum (Tag f) (Tag g)) x
-> Sum f g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly (TagSum (Tag f) (Tag g)) x -> (:+:) f g x
Poly (Tag (f :+: g)) x -> (:+:) f g x
forall x. Poly (Tag (f :+: g)) x -> (:+:) f g x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly
    where
      fromGenerics :: (:+:) f g a -> Sum f g a
fromGenerics (L1 f a
fx) = f a -> Sum f g a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
f a -> Sum f g a
InL f a
fx
      fromGenerics (R1 g a
gx) = g a -> Sum f g a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
g a -> Sum f g a
InR g a
gx

instance (Polynomial f, Polynomial g) => Polynomial (f :*: g) where
  type Tag (f :*: g) = TagMul (Tag f) (Tag g)

  toPoly :: forall x. (:*:) f g x -> Poly (Tag (f :*: g)) x
toPoly (f x
fx :*: g x
gx) =
    case (f x -> Poly (Tag f) x
forall x. f x -> Poly (Tag f) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly f x
fx, g x -> Poly (Tag g) x
forall x. g x -> Poly (Tag g) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly g x
gx) of
      (P Tag f n
tagF n -> x
repF, P Tag g n
tagG n -> x
repG) ->
        TagMul (Tag f) (Tag g) (Either n n)
-> (Either n n -> x) -> Poly (TagMul (Tag f) (Tag g)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P (Tag f n -> Tag g n -> TagMul (Tag f) (Tag g) (Either n n)
forall (f :: Type -> Type) x1 (g :: Type -> Type) y.
f x1 -> g y -> TagMul f g (Either x1 y)
TagMul Tag f n
tagF Tag g n
tagG) ((n -> x) -> (n -> x) -> Either n n -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either n -> x
repF n -> x
repG)

  fromPoly :: forall x. Poly (Tag (f :*: g)) x -> (:*:) f g x
fromPoly (P (TagMul Tag f x1
tagF Tag g y
tagG) n -> x
rep) =
    let pf :: Poly (Tag f) x
pf = Tag f x1 -> (x1 -> x) -> Poly (Tag f) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P Tag f x1
tagF (n -> x
rep (n -> x) -> (x1 -> n) -> x1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x1 -> n
x1 -> Either x1 y
forall a b. a -> Either a b
Left)
        pg :: Poly (Tag g) x
pg = Tag g y -> (y -> x) -> Poly (Tag g) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P Tag g y
tagG (n -> x
rep (n -> x) -> (y -> n) -> y -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. y -> n
y -> Either x1 y
forall a b. b -> Either a b
Right)
     in Poly (Tag f) x -> f x
forall x. Poly (Tag f) x -> f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly Poly (Tag f) x
pf f x -> g x -> (:*:) f g x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Poly (Tag g) x -> g x
forall x. Poly (Tag g) x -> g x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly Poly (Tag g) x
pg

instance (Polynomial f, Polynomial g) => Polynomial (Product f g) where
  type Tag (Product f g) = TagMul (Tag f) (Tag g)

  toPoly :: forall x. Product f g x -> Poly (Tag (Product f g)) x
toPoly = (:*:) f g x -> Poly (TagMul (Tag f) (Tag g)) x
(:*:) f g x -> Poly (Tag (f :*: g)) x
forall x. (:*:) f g x -> Poly (Tag (f :*: g)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly ((:*:) f g x -> Poly (TagMul (Tag f) (Tag g)) x)
-> (Product f g x -> (:*:) f g x)
-> Product f g x
-> Poly (TagMul (Tag f) (Tag g)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product f g x -> (:*:) f g x
forall {k} {f :: k -> Type} {g :: k -> Type} {p :: k}.
Product f g p -> (:*:) f g p
toGenerics
    where
      toGenerics :: Product f g p -> (:*:) f g p
toGenerics (Pair f p
fx g p
gx) = f p
fx f p -> g p -> (:*:) f g p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: g p
gx

  fromPoly :: forall x. Poly (Tag (Product f g)) x -> Product f g x
fromPoly = (:*:) f g x -> Product f g x
forall {k} {f :: k -> Type} {g :: k -> Type} {a :: k}.
(:*:) f g a -> Product f g a
fromGenerics ((:*:) f g x -> Product f g x)
-> (Poly (TagMul (Tag f) (Tag g)) x -> (:*:) f g x)
-> Poly (TagMul (Tag f) (Tag g)) x
-> Product f g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly (TagMul (Tag f) (Tag g)) x -> (:*:) f g x
Poly (Tag (f :*: g)) x -> (:*:) f g x
forall x. Poly (Tag (f :*: g)) x -> (:*:) f g x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly
    where
      fromGenerics :: (:*:) f g a -> Product f g a
fromGenerics (f a
fx :*: g a
gx) = f a -> g a -> Product f g a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
f a -> g a -> Product f g a
Pair f a
fx g a
gx

instance (Polynomial f) => Polynomial (Pow n f) where
  type Tag (Pow n f) = TagPow n (Tag f)

  toPoly :: forall x. Pow n f x -> Poly (TagPow n (Tag f)) x
  toPoly :: forall x. Pow n f x -> Poly (TagPow n (Tag f)) x
toPoly Pow n f x
Pow0 = TagPow 0 (Tag f) Void -> (Void -> x) -> Poly (TagPow 0 (Tag f)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P TagPow 0 (Tag f) Void
forall (t :: Type -> Type). TagPow 0 t Void
TagPow0 Void -> x
forall a. Void -> a
absurd
  toPoly (PowNZ Pow' n f x
fs) = case Pow' n f x -> Poly (Tag (Pow' n f)) x
forall x. Pow' n f x -> Poly (Tag (Pow' n f)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly Pow' n f x
fs of
      (P Tag (Pow' n f) n
tagF n -> x
repF) -> TagPow n (Tag f) n -> (n -> x) -> Poly (TagPow n (Tag f)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P (TagPow' n (Tag f) n -> TagPow n (Tag f) n
forall (n :: Nat) (t :: Type -> Type) xs.
TagPow' n t xs -> TagPow n t xs
TagPowNZ TagPow' n (Tag f) n
Tag (Pow' n f) n
tagF) n -> x
repF

  fromPoly :: forall x. Poly (TagPow n (Tag f)) x -> Pow n f x
  fromPoly :: forall x. Poly (TagPow n (Tag f)) x -> Pow n f x
fromPoly (P TagPow n (Tag f) n
tag n -> x
rep) = case TagPow n (Tag f) n
tag of
    TagPow n (Tag f) n
TagPow0 -> Pow n f x
Pow 0 f x
forall {k} (f :: k -> Type) (x :: k). Pow 0 f x
Pow0
    TagPowNZ TagPow' n (Tag f) n
tagFs -> Pow' n f x -> Pow n f x
forall {k} (n :: Nat) (f :: k -> Type) (x :: k).
Pow' n f x -> Pow n f x
PowNZ (Poly (Tag (Pow' n f)) x -> Pow' n f x
forall x. Poly (Tag (Pow' n f)) x -> Pow' n f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (TagPow' n (Tag f) n -> (n -> x) -> Poly (TagPow' n (Tag f)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P TagPow' n (Tag f) n
tagFs n -> x
rep))

instance (Polynomial f) => Polynomial (Pow' n f) where
  type Tag (Pow' n f) = TagPow' n (Tag f)

  toPoly :: forall x. Pow' n f x -> Poly (TagPow' n (Tag f)) x
  toPoly :: forall x. Pow' n f x -> Poly (TagPow' n (Tag f)) x
toPoly (Pow1 f x
fx) = case f x -> Poly (Tag f) x
forall x. f x -> Poly (Tag f) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly f x
fx of
    P Tag f n
tag n -> x
rep -> TagPow' 1 (Tag f) n -> (n -> x) -> Poly (TagPow' 1 (Tag f)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P (Tag f n -> TagPow' 1 (Tag f) n
forall (t :: Type -> Type) xs. t xs -> TagPow' 1 t xs
TagPow1 Tag f n
tag) n -> x
rep
  toPoly (PowEven Pow' m f x
fs1 Pow' m f x
fs2) = case (Pow' m f x -> Poly (Tag (Pow' m f)) x
forall x. Pow' m f x -> Poly (Tag (Pow' m f)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly Pow' m f x
fs1, Pow' m f x -> Poly (Tag (Pow' m f)) x
forall x. Pow' m f x -> Poly (Tag (Pow' m f)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly Pow' m f x
fs2) of
    (P TagPow' m (Tag f) n
tag1 n -> x
rep1, P TagPow' m (Tag f) n
tag2 n -> x
rep2) -> TagPow' n (Tag f) (Either n n)
-> (Either n n -> x) -> Poly (TagPow' n (Tag f)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P (TagPow' m (Tag f) n
-> TagPow' m (Tag f) n -> TagPow' n (Tag f) (Either n n)
forall (n :: Nat) (m :: Nat) (t :: Type -> Type) xs1 xs2.
(KnownNat n, n ~ (m * 2)) =>
TagPow' m t xs1 -> TagPow' m t xs2 -> TagPow' n t (Either xs1 xs2)
TagPowEven TagPow' m (Tag f) n
tag1 TagPow' m (Tag f) n
tag2) ((n -> x) -> (n -> x) -> Either n n -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either n -> x
rep1 n -> x
rep2)
  toPoly (PowOdd f x
fx Pow' m f x
fs1 Pow' m f x
fs2) = case (f x -> Poly (Tag f) x
forall x. f x -> Poly (Tag f) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly f x
fx, Pow' m f x -> Poly (Tag (Pow' m f)) x
forall x. Pow' m f x -> Poly (Tag (Pow' m f)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly Pow' m f x
fs1, Pow' m f x -> Poly (Tag (Pow' m f)) x
forall x. Pow' m f x -> Poly (Tag (Pow' m f)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly Pow' m f x
fs2) of
    (P Tag f n
tag n -> x
rep, P TagPow' m (Tag f) n
tag1 n -> x
rep1, P TagPow' m (Tag f) n
tag2 n -> x
rep2) -> TagPow' n (Tag f) (Either n (Either n n))
-> (Either n (Either n n) -> x) -> Poly (TagPow' n (Tag f)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P (Tag f n
-> TagPow' m (Tag f) n
-> TagPow' m (Tag f) n
-> TagPow' n (Tag f) (Either n (Either n n))
forall (n :: Nat) (m :: Nat) (t :: Type -> Type) x xs1 xs2.
(KnownNat n, n ~ ((m * 2) + 1)) =>
t x
-> TagPow' m t xs1
-> TagPow' m t xs2
-> TagPow' n t (Either x (Either xs1 xs2))
TagPowOdd Tag f n
tag TagPow' m (Tag f) n
tag1 TagPow' m (Tag f) n
tag2) ((n -> x) -> (Either n n -> x) -> Either n (Either n n) -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either n -> x
rep ((n -> x) -> (n -> x) -> Either n n -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either n -> x
rep1 n -> x
rep2))

  fromPoly :: forall x. Poly (TagPow' n (Tag f)) x -> Pow' n f x
  fromPoly :: forall x. Poly (TagPow' n (Tag f)) x -> Pow' n f x
fromPoly (P TagPow' n (Tag f) n
tag n -> x
rep) = case TagPow' n (Tag f) n
tag of
    TagPow1 Tag f n
tag' -> f x -> Pow' 1 f x
forall {k} (f :: k -> Type) (x :: k). f x -> Pow' 1 f x
Pow1 (Poly (Tag f) x -> f x
forall x. Poly (Tag f) x -> f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (Tag f n -> (n -> x) -> Poly (Tag f) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P Tag f n
tag' n -> x
rep))
    TagPowEven TagPow' m (Tag f) xs1
tag1 TagPow' m (Tag f) xs2
tag2 -> Pow' m f x -> Pow' m f x -> Pow' n f x
forall {k} (n :: Nat) (m :: Nat) (f :: k -> Type) (x :: k).
(KnownNat n, n ~ (m * 2)) =>
Pow' m f x -> Pow' m f x -> Pow' n f x
PowEven (Poly (Tag (Pow' m f)) x -> Pow' m f x
forall x. Poly (Tag (Pow' m f)) x -> Pow' m f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (TagPow' m (Tag f) xs1 -> (xs1 -> x) -> Poly (TagPow' m (Tag f)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P TagPow' m (Tag f) xs1
tag1 (n -> x
rep (n -> x) -> (xs1 -> n) -> xs1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. xs1 -> n
xs1 -> Either xs1 xs2
forall a b. a -> Either a b
Left))) (Poly (Tag (Pow' m f)) x -> Pow' m f x
forall x. Poly (Tag (Pow' m f)) x -> Pow' m f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (TagPow' m (Tag f) xs2 -> (xs2 -> x) -> Poly (TagPow' m (Tag f)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P TagPow' m (Tag f) xs2
tag2 (n -> x
rep (n -> x) -> (xs2 -> n) -> xs2 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. xs2 -> n
xs2 -> Either xs1 xs2
forall a b. b -> Either a b
Right)))
    TagPowOdd Tag f x
tag' TagPow' m (Tag f) xs1
tag1 TagPow' m (Tag f) xs2
tag2 ->
      let rep' :: x -> x
rep' = n -> x
rep (n -> x) -> (x -> n) -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> n
x -> Either x (Either xs1 xs2)
forall a b. a -> Either a b
Left
          rep1 :: xs1 -> x
rep1 = n -> x
rep (n -> x) -> (xs1 -> n) -> xs1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either xs1 xs2 -> n
Either xs1 xs2 -> Either x (Either xs1 xs2)
forall a b. b -> Either a b
Right (Either xs1 xs2 -> n) -> (xs1 -> Either xs1 xs2) -> xs1 -> n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. xs1 -> Either xs1 xs2
forall a b. a -> Either a b
Left
          rep2 :: xs2 -> x
rep2 = n -> x
rep (n -> x) -> (xs2 -> n) -> xs2 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either xs1 xs2 -> n
Either xs1 xs2 -> Either x (Either xs1 xs2)
forall a b. b -> Either a b
Right (Either xs1 xs2 -> n) -> (xs2 -> Either xs1 xs2) -> xs2 -> n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. xs2 -> Either xs1 xs2
forall a b. b -> Either a b
Right
      in f x -> Pow' m f x -> Pow' m f x -> Pow' n f x
forall {k} (n :: Nat) (m :: Nat) (f :: k -> Type) (x :: k).
(KnownNat n, n ~ ((m * 2) + 1)) =>
f x -> Pow' m f x -> Pow' m f x -> Pow' n f x
PowOdd (Poly (Tag f) x -> f x
forall x. Poly (Tag f) x -> f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (Tag f x -> (x -> x) -> Poly (Tag f) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P Tag f x
tag' x -> x
rep')) (Poly (Tag (Pow' m f)) x -> Pow' m f x
forall x. Poly (Tag (Pow' m f)) x -> Pow' m f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (TagPow' m (Tag f) xs1 -> (xs1 -> x) -> Poly (TagPow' m (Tag f)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P TagPow' m (Tag f) xs1
tag1 xs1 -> x
rep1)) (Poly (Tag (Pow' m f)) x -> Pow' m f x
forall x. Poly (Tag (Pow' m f)) x -> Pow' m f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (TagPow' m (Tag f) xs2 -> (xs2 -> x) -> Poly (TagPow' m (Tag f)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P TagPow' m (Tag f) xs2
tag2 xs2 -> x
rep2))

instance (Polynomial f, HasFinitary (Tag f), Polynomial g) => Polynomial (f :.: g) where
  type Tag (f :.: g) = TagComp (Tag f) (Tag g)

  toPoly :: forall x. (f :.: g) x -> Poly (TagComp (Tag f) (Tag g)) x
  toPoly :: forall x. (:.:) f g x -> Poly (TagComp (Tag f) (Tag g)) x
toPoly (Comp1 f (g x)
fgy) = case f (g x) -> Poly (Tag f) (g x)
forall x. f x -> Poly (Tag f) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly f (g x)
fgy of
    P Tag f n
tagF n -> g x
repF ->
      case Tag f n
-> (Finitary n => Poly (TagPow (Cardinality n) (Tag g)) x)
-> Poly (TagPow (Cardinality n) (Tag g)) x
forall n r. Tag f n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary Tag f n
tagF (Pow (Cardinality n) g x -> Poly (Tag (Pow (Cardinality n) g)) x
forall x.
Pow (Cardinality n) g x -> Poly (Tag (Pow (Cardinality n) g)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly (SNat (Cardinality n)
-> (Finite (Cardinality n) -> g x) -> Pow (Cardinality n) g x
forall {k} (n :: Nat) (f :: k -> Type) (x :: k).
SNat n -> (Finite n -> f x) -> Pow n f x
functionToPow SNat (Cardinality n)
forall (n :: Nat). KnownNat n => SNat n
SNat (n -> g x
repF (n -> g x)
-> (Finite (Cardinality n) -> n) -> Finite (Cardinality n) -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (Cardinality n) -> n
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite))) of
        P TagPow (Cardinality n) (Tag g) n
tagPowG n -> x
repPow -> TagComp (Tag f) (Tag g) n
-> (n -> x) -> Poly (TagComp (Tag f) (Tag g)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P (Tag f n
-> TagPow (Cardinality n) (Tag g) n -> TagComp (Tag f) (Tag g) n
forall (t :: Type -> Type) a (u :: Type -> Type) n.
t a -> TagPow (Cardinality a) u n -> TagComp t u n
TagComp Tag f n
tagF TagPow (Cardinality n) (Tag g) n
tagPowG) n -> x
repPow

  fromPoly :: forall x. Poly (TagComp (Tag f) (Tag g)) x -> (f :.: g) x
  fromPoly :: forall x. Poly (TagComp (Tag f) (Tag g)) x -> (:.:) f g x
fromPoly (P (TagComp Tag f a
tagF TagPow (Cardinality a) (Tag g) n
tagPowG) n -> x
rep) =
    let repF :: Finite (Cardinality a) -> g x
repF = Pow (Cardinality a) g x -> Finite (Cardinality a) -> g x
forall {k} (n :: Nat) (f :: k -> Type) (x :: k).
Pow n f x -> Finite n -> f x
powToFunction (Pow (Cardinality a) g x -> Finite (Cardinality a) -> g x)
-> Pow (Cardinality a) g x -> Finite (Cardinality a) -> g x
forall a b. (a -> b) -> a -> b
$ Poly (Tag (Pow (Cardinality a) g)) x -> Pow (Cardinality a) g x
forall x.
Poly (Tag (Pow (Cardinality a) g)) x -> Pow (Cardinality a) g x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (TagPow (Cardinality a) (Tag g) n
-> (n -> x) -> Poly (TagPow (Cardinality a) (Tag g)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P TagPow (Cardinality a) (Tag g) n
tagPowG n -> x
rep)
    in  Tag f a -> (Finitary a => (:.:) f g x) -> (:.:) f g x
forall n r. Tag f n -> (Finitary n => r) -> r
forall (tag :: Type -> Type) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary Tag f a
tagF ((Finitary a => (:.:) f g x) -> (:.:) f g x)
-> (Finitary a => (:.:) f g x) -> (:.:) f g x
forall a b. (a -> b) -> a -> b
$ f (g x) -> (:.:) f g x
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (f (g x) -> (:.:) f g x) -> f (g x) -> (:.:) f g x
forall a b. (a -> b) -> a -> b
$ Poly (Tag f) (g x) -> f (g x)
forall x. Poly (Tag f) x -> f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (Tag f a -> (a -> g x) -> Poly (Tag f) (g x)
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P Tag f a
tagF (Finite (Cardinality a) -> g x
repF (Finite (Cardinality a) -> g x)
-> (a -> Finite (Cardinality a)) -> a -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite))

instance (Polynomial f, HasFinitary (Tag f), Polynomial g) => Polynomial (Compose f g) where
  type Tag (Compose f g) = TagComp (Tag f) (Tag g)

  toPoly :: forall x. Compose f g x -> Poly (Tag (Compose f g)) x
toPoly = (:.:) f g x -> Poly (TagComp (Tag f) (Tag g)) x
(:.:) f g x -> Poly (Tag (f :.: g)) x
forall x. (:.:) f g x -> Poly (Tag (f :.: g)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly ((:.:) f g x -> Poly (TagComp (Tag f) (Tag g)) x)
-> (Compose f g x -> (:.:) f g x)
-> Compose f g x
-> Poly (TagComp (Tag f) (Tag g)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f g x -> (:.:) f g x
forall x. Compose f g x -> (:.:) f g x
toGenerics
    where
      toGenerics :: forall x. Compose f g x -> (f :.: g) x 
      toGenerics :: forall x. Compose f g x -> (:.:) f g x
toGenerics = Compose f g x -> (:.:) f g x
forall a b. Coercible a b => a -> b
coerce

  fromPoly :: forall x. Poly (Tag (Compose f g)) x -> Compose f g x
fromPoly = (:.:) f g x -> Compose f g x
forall x. (:.:) f g x -> Compose f g x
fromGenerics ((:.:) f g x -> Compose f g x)
-> (Poly (TagComp (Tag f) (Tag g)) x -> (:.:) f g x)
-> Poly (TagComp (Tag f) (Tag g)) x
-> Compose f g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly (TagComp (Tag f) (Tag g)) x -> (:.:) f g x
Poly (Tag (f :.: g)) x -> (:.:) f g x
forall x. Poly (Tag (f :.: g)) x -> (:.:) f g x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly
    where
      fromGenerics :: forall x. (f :.: g) x -> Compose f g x
      fromGenerics :: forall x. (:.:) f g x -> Compose f g x
fromGenerics = (:.:) f g x -> Compose f g x
forall a b. Coercible a b => a -> b
coerce


instance (Polynomial f, Polynomial g) => Polynomial (Day f g) where
    type Tag (Day f g) = TagDay (Tag f) (Tag g)

    toPoly :: forall x. Day f g x -> Poly (Tag (Day f g)) x
toPoly (Day f b
fa g c
gb b -> c -> x
op) = case (f b -> Poly (Tag f) b
forall x. f x -> Poly (Tag f) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly f b
fa, g c -> Poly (Tag g) c
forall x. g x -> Poly (Tag g) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly g c
gb) of
        (P Tag f n
tagF n -> b
repF, P Tag g n
tagG n -> c
repG) ->
            let repFG :: (n, n) -> x
repFG (n
n,n
m) = b -> c -> x
op (n -> b
repF n
n) (n -> c
repG n
m) 
            in TagDay (Tag f) (Tag g) (n, n)
-> ((n, n) -> x) -> Poly (TagDay (Tag f) (Tag g)) x
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P (Tag f n -> Tag g n -> TagDay (Tag f) (Tag g) (n, n)
forall (t :: Type -> Type) n1 (u :: Type -> Type) m.
t n1 -> u m -> TagDay t u (n1, m)
TagDay Tag f n
tagF Tag g n
tagG) (n, n) -> x
repFG

    fromPoly :: forall x. Poly (Tag (Day f g)) x -> Day f g x
fromPoly (P (TagDay Tag f n1
tagF Tag g m
tagG) n -> x
repFG) =
        let op :: n1 -> m -> x
op n1
n m
m = n -> x
repFG (n1
n,m
m)
        in f n1 -> g m -> (n1 -> m -> x) -> Day f g x
forall (f :: Type -> Type) (g :: Type -> Type) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day (Poly (Tag f) n1 -> f n1
forall x. Poly (Tag f) x -> f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (Tag f n1 -> (n1 -> n1) -> Poly (Tag f) n1
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P Tag f n1
tagF n1 -> n1
forall a. a -> a
id)) (Poly (Tag g) m -> g m
forall x. Poly (Tag g) x -> g x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly (Tag g m -> (m -> m) -> Poly (Tag g) m
forall (tag :: Type -> Type) n x. tag n -> (n -> x) -> Poly tag x
P Tag g m
tagG m -> m
forall a. a -> a
id)) n1 -> m -> x
op

-- | @fromPoly = toPoly = id@
instance Polynomial (Poly tag) where
  type Tag (Poly tag) = tag

  fromPoly :: forall x. Poly (Tag (Poly tag)) x -> Poly tag x
fromPoly = Poly tag x -> Poly tag x
Poly (Tag (Poly tag)) x -> Poly tag x
forall a. a -> a
id
  toPoly :: forall x. Poly tag x -> Poly (Tag (Poly tag)) x
toPoly = Poly tag x -> Poly tag x
Poly tag x -> Poly (Tag (Poly tag)) x
forall a. a -> a
id

---- Generic definitions ----
instance (Generic1 f, Polynomial (Rep1 f)) => Polynomial (Generically1 f) where
  type Tag (Generically1 f) = Tag (Rep1 f)

  toPoly :: forall x. Generically1 f x -> Poly (Tag (Generically1 f)) x
toPoly (Generically1 f x
fx) = Rep1 f x -> Poly (Tag (Rep1 f)) x
forall x. Rep1 f x -> Poly (Tag (Rep1 f)) x
forall (f :: Type -> Type) x. Polynomial f => f x -> Poly (Tag f) x
toPoly (f x -> Rep1 f x
forall a. f a -> Rep1 f a
forall k (f :: k -> Type) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f x
fx)
  fromPoly :: forall x. Poly (Tag (Generically1 f)) x -> Generically1 f x
fromPoly Poly (Tag (Generically1 f)) x
p = f x -> Generically1 f x
forall {k} (f :: k -> Type) (a :: k). f a -> Generically1 f a
Generically1 (f x -> Generically1 f x) -> f x -> Generically1 f x
forall a b. (a -> b) -> a -> b
$ Rep1 f x -> f x
forall a. Rep1 f a -> f a
forall k (f :: k -> Type) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (Poly (Tag (Rep1 f)) x -> Rep1 f x
forall x. Poly (Tag (Rep1 f)) x -> Rep1 f x
forall (f :: Type -> Type) x. Polynomial f => Poly (Tag f) x -> f x
fromPoly Poly (Tag (Rep1 f)) x
Poly (Tag (Generically1 f)) x
p)

deriving via (Generically1 (Either a))
  instance Polynomial (Either a)

deriving via (Generically1 ((,) a))
  instance Polynomial ((,) a)