{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | How can we automatically inject normal Haskell types into the logic, using GHC.Generics
module Constrained.Generic where

import Constrained.List (
  Append,
  FunTy,
  List (..),
  TypeList,
  appendList,
  curryList_,
  listShape,
  uncurryList_,
 )

import Data.Functor.Const
import Data.Functor.Identity
import Data.Kind
import Data.Typeable
import GHC.Generics
import GHC.TypeLits (Symbol)

-- Sum and Prod and their operations came from Constrained.Univ
-- Since that file is basically about Fn, which is going to disappear
-- this seems like the appropriate place for them. We will need FunctionSymbol's
-- for fst_ snd_ pair_ injectLeft_  and injectRight_ defined someplace else
------------------------------------------------------------------------
-- Pairs
------------------------------------------------------------------------

data Prod a b = Prod {forall a b. Prod a b -> a
prodFst :: a, forall a b. Prod a b -> b
prodSnd :: b}
  deriving (Prod a b -> Prod a b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => Prod a b -> Prod a b -> Bool
/= :: Prod a b -> Prod a b -> Bool
$c/= :: forall a b. (Eq a, Eq b) => Prod a b -> Prod a b -> Bool
== :: Prod a b -> Prod a b -> Bool
$c== :: forall a b. (Eq a, Eq b) => Prod a b -> Prod a b -> Bool
Eq, Prod a b -> Prod a b -> Bool
Prod a b -> Prod a b -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a} {b}. (Ord a, Ord b) => Eq (Prod a b)
forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool
forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Ordering
forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Prod a b
min :: Prod a b -> Prod a b -> Prod a b
$cmin :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Prod a b
max :: Prod a b -> Prod a b -> Prod a b
$cmax :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Prod a b
>= :: Prod a b -> Prod a b -> Bool
$c>= :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool
> :: Prod a b -> Prod a b -> Bool
$c> :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool
<= :: Prod a b -> Prod a b -> Bool
$c<= :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool
< :: Prod a b -> Prod a b -> Bool
$c< :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool
compare :: Prod a b -> Prod a b -> Ordering
$ccompare :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Ordering
Ord)

instance (Show a, Show b) => Show (Prod a b) where
  show :: Prod a b -> String
show (Prod a
x b
y) = String
"(Prod " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
x forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show b
y forall a. [a] -> [a] -> [a]
++ String
")"

type family ProdOver as where
  ProdOver '[] = ()
  ProdOver '[a] = a
  ProdOver (a : as) = Prod a (ProdOver as)

listToProd :: (ProdOver as -> r) -> List Identity as -> r
listToProd :: forall (as :: [*]) r. (ProdOver as -> r) -> List Identity as -> r
listToProd ProdOver as -> r
k List Identity as
Nil = ProdOver as -> r
k ()
listToProd ProdOver as -> r
k (Identity a
a :> List Identity as1
Nil) = ProdOver as -> r
k a
a
listToProd ProdOver as -> r
k (Identity a
a :> Identity a
b :> List Identity as1
as) = ProdOver as -> r
k (forall a b. a -> b -> Prod a b
Prod a
a (forall (as :: [*]) r. (ProdOver as -> r) -> List Identity as -> r
listToProd forall a. a -> a
id (Identity a
b forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Identity as1
as)))

prodToList :: forall as. TypeList as => ProdOver as -> List Identity as
prodToList :: forall (as :: [*]). TypeList as => ProdOver as -> List Identity as
prodToList = forall (ts :: [*]).
List (Const ()) ts -> ProdOver ts -> List Identity ts
go (forall (as :: [*]). TypeList as => List (Const ()) as
listShape @as)
  where
    go ::
      forall ts.
      List (Const ()) ts ->
      ProdOver ts ->
      List Identity ts
    go :: forall (ts :: [*]).
List (Const ()) ts -> ProdOver ts -> List Identity ts
go List (Const ()) ts
Nil ProdOver ts
_ = forall {k} (f :: k -> *). List f '[]
Nil
    go (Const () a
_ :> List (Const ()) as1
Nil) ProdOver ts
a = forall a. a -> Identity a
Identity ProdOver ts
a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil
    go (Const () a
_ :> Const () a
ix :> List (Const ()) as1
ixs) (Prod a
a ProdOver (a : as1)
as) = forall a. a -> Identity a
Identity a
a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall (ts :: [*]).
List (Const ()) ts -> ProdOver ts -> List Identity ts
go (Const () a
ix forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List (Const ()) as1
ixs) ProdOver (a : as1)
as

appendProd ::
  forall xs ys.
  (TypeList xs, TypeList ys) =>
  ProdOver xs ->
  ProdOver ys ->
  ProdOver (Append xs ys)
appendProd :: forall (xs :: [*]) (ys :: [*]).
(TypeList xs, TypeList ys) =>
ProdOver xs -> ProdOver ys -> ProdOver (Append xs ys)
appendProd ProdOver xs
xs ProdOver ys
ys = forall (as :: [*]) r. (ProdOver as -> r) -> List Identity as -> r
listToProd forall a. a -> a
id (forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList @Identity @xs @ys (forall (as :: [*]). TypeList as => ProdOver as -> List Identity as
prodToList ProdOver xs
xs) (forall (as :: [*]). TypeList as => ProdOver as -> List Identity as
prodToList ProdOver ys
ys))

splitProd ::
  forall xs ys.
  (TypeList xs, TypeList ys) =>
  ProdOver (Append xs ys) ->
  Prod (ProdOver xs) (ProdOver ys)
splitProd :: forall (xs :: [*]) (ys :: [*]).
(TypeList xs, TypeList ys) =>
ProdOver (Append xs ys) -> Prod (ProdOver xs) (ProdOver ys)
splitProd = forall (as :: [*]) (bs :: [*]).
List (Const ()) as
-> List (Const ()) bs
-> ProdOver (Append as bs)
-> Prod (ProdOver as) (ProdOver bs)
go (forall (as :: [*]). TypeList as => List (Const ()) as
listShape @xs) (forall (as :: [*]). TypeList as => List (Const ()) as
listShape @ys)
  where
    go ::
      List (Const ()) as ->
      List (Const ()) bs ->
      ProdOver (Append as bs) ->
      Prod (ProdOver as) (ProdOver bs)
    go :: forall (as :: [*]) (bs :: [*]).
List (Const ()) as
-> List (Const ()) bs
-> ProdOver (Append as bs)
-> Prod (ProdOver as) (ProdOver bs)
go List (Const ()) as
Nil List (Const ()) bs
_ ProdOver (Append as bs)
p = forall a b. a -> b -> Prod a b
Prod () ProdOver (Append as bs)
p
    go (Const () a
_ :> List (Const ()) as1
Nil) List (Const ()) bs
Nil ProdOver (Append as bs)
p = forall a b. a -> b -> Prod a b
Prod ProdOver (Append as bs)
p ()
    go (Const () a
_ :> List (Const ()) as1
Nil) (Const () a
_ :> List (Const ()) as1
_) ProdOver (Append as bs)
p = ProdOver (Append as bs)
p
    go (Const () a
_ :> Const () a
a :> List (Const ()) as1
as) List (Const ()) bs
bs (Prod a
x ProdOver (a : Append as1 bs)
xs) = forall a b. a -> b -> Prod a b
Prod (forall a b. a -> b -> Prod a b
Prod a
x ProdOver (a : as1)
p0) ProdOver bs
p1
      where
        Prod ProdOver (a : as1)
p0 ProdOver bs
p1 = forall (as :: [*]) (bs :: [*]).
List (Const ()) as
-> List (Const ()) bs
-> ProdOver (Append as bs)
-> Prod (ProdOver as) (ProdOver bs)
go (Const () a
a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List (Const ()) as1
as) List (Const ()) bs
bs ProdOver (a : Append as1 bs)
xs

------------------------------------------------------------------------
-- Sums
------------------------------------------------------------------------

-- | Generic way to represent Sums
data Sum a b
  = SumLeft a
  | SumRight b
  deriving (Sum a b -> Sum a b -> Bool
Sum a b -> Sum a b -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a} {b}. (Ord a, Ord b) => Eq (Sum a b)
forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool
forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Ordering
forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Sum a b
min :: Sum a b -> Sum a b -> Sum a b
$cmin :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Sum a b
max :: Sum a b -> Sum a b -> Sum a b
$cmax :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Sum a b
>= :: Sum a b -> Sum a b -> Bool
$c>= :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool
> :: Sum a b -> Sum a b -> Bool
$c> :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool
<= :: Sum a b -> Sum a b -> Bool
$c<= :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool
< :: Sum a b -> Sum a b -> Bool
$c< :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool
compare :: Sum a b -> Sum a b -> Ordering
$ccompare :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Ordering
Ord, Sum a b -> Sum a b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => Sum a b -> Sum a b -> Bool
/= :: Sum a b -> Sum a b -> Bool
$c/= :: forall a b. (Eq a, Eq b) => Sum a b -> Sum a b -> Bool
== :: Sum a b -> Sum a b -> Bool
$c== :: forall a b. (Eq a, Eq b) => Sum a b -> Sum a b -> Bool
Eq, Int -> Sum a b -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> Sum a b -> ShowS
forall a b. (Show a, Show b) => [Sum a b] -> ShowS
forall a b. (Show a, Show b) => Sum a b -> String
showList :: [Sum a b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [Sum a b] -> ShowS
show :: Sum a b -> String
$cshow :: forall a b. (Show a, Show b) => Sum a b -> String
showsPrec :: Int -> Sum a b -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> Sum a b -> ShowS
Show)

type family SumOver as where
  SumOver '[a] = a
  SumOver (a : as) = Sum a (SumOver as)

-- =========================================================================
-- The idea is for each type, we define a type family (HasSimpleRep) the maps
-- that type to another type we already know how to deal with. The methods
-- 'toSimpleRep' and 'fromSimpleRep' cature that knowledge. The strategy
-- we want to use most of the time, is to use GHC.Generics, to construct
-- the SimpleRep out of Sum and Prod, and to write the 'toSimpleRep' and
-- 'fromSimpleRep' methods automatically. If we can do that, then
-- every thing else will come for free. Note that it is not REQUIRED to make
-- the (SimpleRep t) out of Sum and Prod, but it helps. Note the default
-- method instances use Sum and Prod, but that is not required.
-- ==========================================================================

class Typeable (SimpleRep a) => HasSimpleRep a where
  type SimpleRep a
  type TheSop a :: [Type]
  toSimpleRep :: a -> SimpleRep a
  fromSimpleRep :: SimpleRep a -> a

  type TheSop a = SOPOf (Rep a)
  type SimpleRep a = SOP (TheSop a)

  default toSimpleRep ::
    ( Generic a
    , SimpleGeneric (Rep a)
    , SimpleRep a ~ SimplifyRep (Rep a)
    ) =>
    a ->
    SimpleRep a
  toSimpleRep = forall (rep :: * -> *) p.
SimpleGeneric rep =>
rep p -> SimplifyRep rep
toSimpleRep' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. Generic a => a -> Rep a x
from

  default fromSimpleRep ::
    ( Generic a
    , SimpleGeneric (Rep a)
    , SimpleRep a ~ SimplifyRep (Rep a)
    ) =>
    SimpleRep a ->
    a
  fromSimpleRep = forall a x. Generic a => Rep a x -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rep :: * -> *) p.
SimpleGeneric rep =>
SimplifyRep rep -> rep p
fromSimpleRep'

type family SimplifyRep f where
  SimplifyRep f = SOP (SOPOf f)

instance HasSimpleRep Bool

-- ===============================================================
-- How to move back and forth from (SimpleRep a) to 'a' in a
-- generic way, derived by the Generics machinery is captured
-- by the SimpleGeneric class
-- ===============================================================

class SimpleGeneric rep where
  toSimpleRep' :: rep p -> SimplifyRep rep
  fromSimpleRep' :: SimplifyRep rep -> rep p

instance SimpleGeneric f => SimpleGeneric (D1 d f) where
  toSimpleRep' :: forall p. D1 d f p -> SimplifyRep (D1 d f)
toSimpleRep' (M1 f p
f) = forall (rep :: * -> *) p.
SimpleGeneric rep =>
rep p -> SimplifyRep rep
toSimpleRep' f p
f
  fromSimpleRep' :: forall p. SimplifyRep (D1 d f) -> D1 d f p
fromSimpleRep' SimplifyRep (D1 d f)
a = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (rep :: * -> *) p.
SimpleGeneric rep =>
SimplifyRep rep -> rep p
fromSimpleRep' SimplifyRep (D1 d f)
a)

instance
  ( SimpleGeneric f
  , SimpleGeneric g
  , SopList (SOPOf f) (SOPOf g)
  ) =>
  SimpleGeneric (f :+: g)
  where
  toSimpleRep' :: forall p. (:+:) f g p -> SimplifyRep (f :+: g)
toSimpleRep' (L1 f p
f) = forall (xs :: [*]) (ys :: [*]).
SopList xs ys =>
SOP xs -> SOP (Append xs ys)
injectSOPLeft @(SOPOf f) @(SOPOf g) forall a b. (a -> b) -> a -> b
$ forall (rep :: * -> *) p.
SimpleGeneric rep =>
rep p -> SimplifyRep rep
toSimpleRep' f p
f
  toSimpleRep' (R1 g p
g) = forall (xs :: [*]) (ys :: [*]).
SopList xs ys =>
SOP ys -> SOP (Append xs ys)
injectSOPRight @(SOPOf f) @(SOPOf g) forall a b. (a -> b) -> a -> b
$ forall (rep :: * -> *) p.
SimpleGeneric rep =>
rep p -> SimplifyRep rep
toSimpleRep' g p
g
  fromSimpleRep' :: forall p. SimplifyRep (f :+: g) -> (:+:) f g p
fromSimpleRep' SimplifyRep (f :+: g)
sop =
    case forall (xs :: [*]) (ys :: [*]).
SopList xs ys =>
SOP (Append xs ys) -> Sum (SOP xs) (SOP ys)
caseSOP @(SOPOf f) @(SOPOf g) SimplifyRep (f :+: g)
sop of
      SumLeft SOP (SOPOf f)
l -> forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall (rep :: * -> *) p.
SimpleGeneric rep =>
SimplifyRep rep -> rep p
fromSimpleRep' SOP (SOPOf f)
l)
      SumRight SOP (SOPOf g)
r -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (forall (rep :: * -> *) p.
SimpleGeneric rep =>
SimplifyRep rep -> rep p
fromSimpleRep' SOP (SOPOf g)
r)

instance SimpleConstructor f => SimpleGeneric (C1 ('MetaCons c a b) f) where
  toSimpleRep' :: forall p.
C1 ('MetaCons c a b) f p -> SimplifyRep (C1 ('MetaCons c a b) f)
toSimpleRep' (M1 f p
f) = forall (rep :: * -> *) p.
SimpleConstructor rep =>
rep p -> ProdOver (Constr rep)
toSimpleCon' f p
f
  fromSimpleRep' :: forall p.
SimplifyRep (C1 ('MetaCons c a b) f) -> C1 ('MetaCons c a b) f p
fromSimpleRep' SimplifyRep (C1 ('MetaCons c a b) f)
a = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (rep :: * -> *) p.
SimpleConstructor rep =>
ProdOver (Constr rep) -> rep p
fromSimpleCon' SimplifyRep (C1 ('MetaCons c a b) f)
a)

-- ================================================================================
--    This part of the code base is responsible for implementing the conversion
--    from a `Generic` type to a `Sum` over `Prod` representation that automatically
--    gives you an instance of `HasSpec`. The user has three options for building their
--    own instances of `HasSpec`, either they hand-roll an instance, they go with the
--    entirely `Generic` instance, or they provide their own `SimpleRep` for their type.
--
--    The latter may be appropriate when the type is an optimized representation:
--
--    ```
--    newtype Foo = Foo { unFoo :: MemoBytes ActualFoo }
--
--    instance HasSimpleRep Foo where
--      type SimpleRep Foo = ActualFoo
--      toSimpleRep = unMemoBytes . unFoo
--      fromSimpleRep = Foo . memoBytes
--    ```
--
--    This would then allow for `Foo` to be treated as a simple `newtype` over `ActualFoo`
--    in constraints:
--
--    ```
--    fooSpec :: Specification Foo
--    fooSpec = constrained $ \ foo ->
--      match foo $ \ actualFoo -> ...
--    ```
-- =========================================================================================

-- Building a SOP type (Sum Of Prod) --------------------------------------

-- | A constructor name with the types of its arguments
data (c :: Symbol) ::: (ts :: [Type])

-- | Turn a `Rep` into a list that flattens the sum
-- structre and gives the constructors names:
--   Maybe Int -> '["Nothing" ::: '[()], "Just" ::: '[Int]]
--   Either Int Bool -> '["Left" ::: '[Int], "Right" ::: '[Bool]]
--   data Foo = Foo Int Bool | Bar Double -> '["Foo" ::: '[Int, Bool], "Bar" ::: '[Double]]
type family SOPOf f where
  SOPOf (D1 _ f) = SOPOf f
  SOPOf (f :+: g) = Append (SOPOf f) (SOPOf g)
  SOPOf (C1 ('MetaCons constr _ _) f) = '[constr ::: Constr f]

-- | Flatten a single constructor
type family Constr f where
  -- TODO: Here we should put in the selector names
  -- so that they can be re-used to create selectors more
  -- easily than the current disgusting `Fst . Snd . Snd . Snd ...`
  -- method.
  Constr (S1 _ f) = Constr f
  Constr (K1 _ k) = '[k]
  Constr U1 = '[()]
  Constr (f :*: g) = Append (Constr f) (Constr g)

-- | Turn a list from `SOPOf` into a `Sum` over
-- `Prod` representation.
type family SOP constrs where
  SOP '[c ::: prod] = ProdOver prod
  SOP ((c ::: prod) : constrs) = Sum (ProdOver prod) (SOP constrs)

-- =====================================================
-- Constructing a SOP ----------------------------------

type family ConstrOf c sop where
  ConstrOf c (c ::: constr : sop) = constr
  ConstrOf c (_ : sop) = ConstrOf c sop

class Inject c constrs r where
  inject' :: (SOP constrs -> r) -> FunTy (ConstrOf c constrs) r

instance TypeList prod => Inject c '[c ::: prod] r where
  inject' :: (SOP '[c ::: prod] -> r) -> FunTy (ConstrOf c '[c ::: prod]) r
inject' SOP '[c ::: prod] -> r
k = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. a -> f a) -> (List f ts -> r) -> FunTy ts r
curryList_ @prod forall a. a -> Identity a
Identity (forall (as :: [*]) r. (ProdOver as -> r) -> List Identity as -> r
listToProd SOP '[c ::: prod] -> r
k)

instance TypeList prod => Inject c ((c ::: prod) : prod' : constrs) r where
  inject' :: (SOP ((c ::: prod) : prod' : constrs) -> r)
-> FunTy (ConstrOf c ((c ::: prod) : prod' : constrs)) r
inject' SOP ((c ::: prod) : prod' : constrs) -> r
k = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. a -> f a) -> (List f ts -> r) -> FunTy ts r
curryList_ @prod forall a. a -> Identity a
Identity (forall (as :: [*]) r. (ProdOver as -> r) -> List Identity as -> r
listToProd (SOP ((c ::: prod) : prod' : constrs) -> r
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Sum a b
SumLeft @_ @(SOP (prod' : constrs))))

instance
  {-# OVERLAPPABLE #-}
  ( FunTy (ConstrOf c ((c' ::: prod) : con : constrs)) r ~ FunTy (ConstrOf c (con : constrs)) r
  , -- \^ An unfortunately roundabout way of saying `c !~ c'`
    Inject c (con : constrs) r
  ) =>
  Inject c ((c' ::: prod) : con : constrs) r
  where
  inject' :: (SOP ((c' ::: prod) : con : constrs) -> r)
-> FunTy (ConstrOf c ((c' ::: prod) : con : constrs)) r
inject' SOP ((c' ::: prod) : con : constrs) -> r
k = forall (c :: Symbol) (constrs :: [*]) r.
Inject c constrs r =>
(SOP constrs -> r) -> FunTy (ConstrOf c constrs) r
inject' @c @(con : constrs) (SOP ((c' ::: prod) : con : constrs) -> r
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Sum a b
SumRight)

inject ::
  forall c constrs. Inject c constrs (SOP constrs) => FunTy (ConstrOf c constrs) (SOP constrs)
inject :: forall (c :: Symbol) (constrs :: [*]).
Inject c constrs (SOP constrs) =>
FunTy (ConstrOf c constrs) (SOP constrs)
inject = forall (c :: Symbol) (constrs :: [*]) r.
Inject c constrs r =>
(SOP constrs -> r) -> FunTy (ConstrOf c constrs) r
inject' @c @constrs forall a. a -> a
id

-- =====================================================
-- Deconstructing a SOP --------------------------------

-- | An `ALG constrs r` is a function that takes a way to turn every
-- constructor into an `r`:
-- ```
-- ALG (SOPOf (Rep (Either Int Bool))) r = (Int -> r) -> (Bool -> r) -> r
-- ```
type family ALG constrs r where
  ALG '[c ::: prod] r = FunTy prod r -> r
  ALG ((c ::: prod) : constrs) r = FunTy prod r -> ALG constrs r

class SOPLike constrs r where
  -- | Run a `SOP`
  algebra :: SOP constrs -> ALG constrs r

  -- | Ignore everything in the `SOP`
  consts :: r -> ALG constrs r

instance TypeList prod => SOPLike '[c ::: prod] r where
  algebra :: SOP '[c ::: prod] -> ALG '[c ::: prod] r
algebra SOP '[c ::: prod]
prod FunTy prod r
f = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
uncurryList_ @prod forall a. Identity a -> a
runIdentity FunTy prod r
f forall a b. (a -> b) -> a -> b
$ forall (as :: [*]). TypeList as => ProdOver as -> List Identity as
prodToList SOP '[c ::: prod]
prod
  consts :: r -> ALG '[c ::: prod] r
consts r
r FunTy prod r
_ = r
r

instance (TypeList prod, SOPLike (con : cases) r) => SOPLike ((c ::: prod) : con : cases) r where
  algebra :: SOP ((c ::: prod) : con : cases)
-> ALG ((c ::: prod) : con : cases) r
algebra (SumLeft ProdOver prod
prod) FunTy prod r
f = forall (constrs :: [*]) r. SOPLike constrs r => r -> ALG constrs r
consts @(con : cases) @r (forall (constrs :: [*]) r.
SOPLike constrs r =>
SOP constrs -> ALG constrs r
algebra @'[c ::: prod] ProdOver prod
prod FunTy prod r
f)
  algebra (SumRight SOP (con : cases)
rest) FunTy prod r
_ = forall (constrs :: [*]) r.
SOPLike constrs r =>
SOP constrs -> ALG constrs r
algebra @(con : cases) @r SOP (con : cases)
rest

  consts :: r -> ALG ((c ::: prod) : con : cases) r
consts r
r FunTy prod r
_ = forall (constrs :: [*]) r. SOPLike constrs r => r -> ALG constrs r
consts @(con : cases) r
r

-- ========================================================
-- The individual constructor level -----------------------

class SimpleConstructor rep where
  toSimpleCon' :: rep p -> ProdOver (Constr rep)
  fromSimpleCon' :: ProdOver (Constr rep) -> rep p
instance
  ( SimpleConstructor f
  , SimpleConstructor g
  , TypeList (Constr f)
  , TypeList (Constr g)
  ) =>
  SimpleConstructor (f :*: g)
  where
  toSimpleCon' :: forall p. (:*:) f g p -> ProdOver (Constr (f :*: g))
toSimpleCon' (f p
a :*: g p
b) = forall (xs :: [*]) (ys :: [*]).
(TypeList xs, TypeList ys) =>
ProdOver xs -> ProdOver ys -> ProdOver (Append xs ys)
appendProd @(Constr f) @(Constr g) (forall (rep :: * -> *) p.
SimpleConstructor rep =>
rep p -> ProdOver (Constr rep)
toSimpleCon' f p
a) (forall (rep :: * -> *) p.
SimpleConstructor rep =>
rep p -> ProdOver (Constr rep)
toSimpleCon' g p
b)
  fromSimpleCon' :: forall p. ProdOver (Constr (f :*: g)) -> (:*:) f g p
fromSimpleCon' ProdOver (Constr (f :*: g))
constr =
    let Prod ProdOver (Constr f)
a ProdOver (Constr g)
b = forall (xs :: [*]) (ys :: [*]).
(TypeList xs, TypeList ys) =>
ProdOver (Append xs ys) -> Prod (ProdOver xs) (ProdOver ys)
splitProd @(Constr f) @(Constr g) ProdOver (Constr (f :*: g))
constr
     in (forall (rep :: * -> *) p.
SimpleConstructor rep =>
ProdOver (Constr rep) -> rep p
fromSimpleCon' ProdOver (Constr f)
a forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (rep :: * -> *) p.
SimpleConstructor rep =>
ProdOver (Constr rep) -> rep p
fromSimpleCon' ProdOver (Constr g)
b)

instance SimpleConstructor f => SimpleConstructor (S1 s f) where
  toSimpleCon' :: forall p. S1 s f p -> ProdOver (Constr (S1 s f))
toSimpleCon' (M1 f p
f) = forall (rep :: * -> *) p.
SimpleConstructor rep =>
rep p -> ProdOver (Constr rep)
toSimpleCon' f p
f
  fromSimpleCon' :: forall p. ProdOver (Constr (S1 s f)) -> S1 s f p
fromSimpleCon' ProdOver (Constr (S1 s f))
a = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (rep :: * -> *) p.
SimpleConstructor rep =>
ProdOver (Constr rep) -> rep p
fromSimpleCon' ProdOver (Constr (S1 s f))
a)

instance SimpleConstructor (K1 i k) where
  toSimpleCon' :: forall p. K1 i k p -> ProdOver (Constr (K1 i k))
toSimpleCon' (K1 k
k) = k
k
  fromSimpleCon' :: forall p. ProdOver (Constr (K1 i k)) -> K1 i k p
fromSimpleCon' ProdOver (Constr (K1 i k))
k = forall k i c (p :: k). c -> K1 i c p
K1 ProdOver (Constr (K1 i k))
k

instance SimpleConstructor U1 where
  toSimpleCon' :: forall p. U1 p -> ProdOver (Constr U1)
toSimpleCon' U1 p
U1 = ()
  fromSimpleCon' :: forall p. ProdOver (Constr U1) -> U1 p
fromSimpleCon' ProdOver (Constr U1)
_ = forall k (p :: k). U1 p
U1

-- ===================================================
-- The sum type level --------------------------------

-- | Construct and deconstruct cases in a `SOP`
class SopList xs ys where
  injectSOPLeft :: SOP xs -> SOP (Append xs ys)
  injectSOPRight :: SOP ys -> SOP (Append xs ys)
  caseSOP :: SOP (Append xs ys) -> Sum (SOP xs) (SOP ys)

instance SopList '[c ::: x] (y : ys) where
  injectSOPLeft :: SOP '[c ::: x] -> SOP (Append '[c ::: x] (y : ys))
injectSOPLeft = forall a b. a -> Sum a b
SumLeft
  injectSOPRight :: SOP (y : ys) -> SOP (Append '[c ::: x] (y : ys))
injectSOPRight = forall a b. b -> Sum a b
SumRight
  caseSOP :: SOP (Append '[c ::: x] (y : ys))
-> Sum (SOP '[c ::: x]) (SOP (y : ys))
caseSOP = forall a. a -> a
id

instance SopList (x' : xs) (y : ys) => SopList (c ::: x : x' : xs) (y : ys) where
  injectSOPLeft :: SOP ((c ::: x) : x' : xs)
-> SOP (Append ((c ::: x) : x' : xs) (y : ys))
injectSOPLeft (SumLeft ProdOver x
a) = forall a b. a -> Sum a b
SumLeft ProdOver x
a
  injectSOPLeft (SumRight SOP (x' : xs)
b) = forall a b. b -> Sum a b
SumRight (forall (xs :: [*]) (ys :: [*]).
SopList xs ys =>
SOP xs -> SOP (Append xs ys)
injectSOPLeft @(x' : xs) @(y : ys) SOP (x' : xs)
b)

  injectSOPRight :: SOP (y : ys) -> SOP (Append ((c ::: x) : x' : xs) (y : ys))
injectSOPRight SOP (y : ys)
a = forall a b. b -> Sum a b
SumRight (forall (xs :: [*]) (ys :: [*]).
SopList xs ys =>
SOP ys -> SOP (Append xs ys)
injectSOPRight @(x' : xs) @(y : ys) SOP (y : ys)
a)

  caseSOP :: SOP (Append ((c ::: x) : x' : xs) (y : ys))
-> Sum (SOP ((c ::: x) : x' : xs)) (SOP (y : ys))
caseSOP (SumLeft ProdOver x
a) = forall a b. a -> Sum a b
SumLeft (forall a b. a -> Sum a b
SumLeft ProdOver x
a)
  caseSOP (SumRight SOP (x' : Append xs (y : ys))
b) = case forall (xs :: [*]) (ys :: [*]).
SopList xs ys =>
SOP (Append xs ys) -> Sum (SOP xs) (SOP ys)
caseSOP @(x' : xs) @(y : ys) SOP (x' : Append xs (y : ys))
b of
    SumLeft SOP (x' : xs)
b' -> forall a b. a -> Sum a b
SumLeft (forall a b. b -> Sum a b
SumRight SOP (x' : xs)
b')
    SumRight SOP (y : ys)
b' -> forall a b. b -> Sum a b
SumRight SOP (y : ys)
b'

-- ===========================================================
-- How it works
-- If the TypeSpec method of the HasSpec class has a SimpleRep instance, Like this
-- type TypeSpec = a
-- where 'a' has a Sum Product representation then all of the other methods
-- can use the default implementation. This saves lots of trouble for mundane types.
--
-- `HasSimpleRep` and `GenericsFn` are meant to allow you to express that a
-- type is isomorphic to some other type 't' that has a (HasSpec t) instance.
--
-- The trick is that the default instance of `HasSpec a` assumes
-- `HasSimpleRep a` and defines `TypeSpec a = TypeSpec (SimpleRep a)`.
--
-- From this it's possible to work with things of type `a` in constraints by
-- treating them like things of type `SimpleRep a`. This allows us to do case
-- matching etc. on `a` when `SimpleRep a` is a `Sum` type, for example.
--
-- Or alternatively it allows us to treat `a` as a newtype over `SimpleRep a`
-- when using `match`.
-- ====================================================================