{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# 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 GHC.TypeLits (Symbol)

import Constrained.List
import Data.Functor.Const
import Data.Functor.Identity
import Data.Kind
import Data.Typeable
import GHC.Generics

-- 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)

-- ===============================================================
-- 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`.
-- ====================================================================