{- | 'strengthen' over generic representations.

As with base instances, generic strengthening collates all failures rather than
short-circuiting on the first failure. Failures are annotated with precise
information describing where the failure occurred:

  * data type name
  * constructor name
  * field index
  * field name (if present)
-}

-- required due to type class design
{-# LANGUAGE AllowAmbiguousTypes, UndecidableInstances #-}

{-# LANGUAGE OverloadedStrings #-} -- required for failure

module Strongweak.Strengthen.Generic where

import Data.Kind ( type Constraint )
import Strongweak.Strengthen
import GHC.Generics
import Data.Kind ( Type )
import GHC.TypeNats ( Natural, type (+), KnownNat )
import Strongweak.Util.TypeNats ( natVal'' )
import Data.Text.Builder.Linear qualified as TBL
import GHC.Exts ( Symbol, fromString, proxy# )
import GHC.TypeLits ( KnownSymbol, symbolVal' )

-- | Strengthen a value generically.
--
-- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for
-- the definition of compatibility in this context.
strengthenGeneric
    :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s))
    => w -> Either StrengthenFailure' s
strengthenGeneric :: forall w s.
(Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) =>
w -> Either StrengthenFailure' s
strengthenGeneric = (Rep s Any -> s)
-> Either StrengthenFailure' (Rep s Any)
-> Either StrengthenFailure' s
forall a b.
(a -> b)
-> Either StrengthenFailure' a -> Either StrengthenFailure' b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep s Any -> s
forall a x. Generic a => Rep a x -> a
forall x. Rep s x -> s
to (Either StrengthenFailure' (Rep s Any)
 -> Either StrengthenFailure' s)
-> (w -> Either StrengthenFailure' (Rep s Any))
-> w
-> Either StrengthenFailure' s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep w Any -> Either StrengthenFailure' (Rep s Any)
forall p. Rep w p -> Either StrengthenFailure' (Rep s p)
forall {k} (w :: k -> Type) (s :: k -> Type) (p :: k).
GStrengthenD w s =>
w p -> Either StrengthenFailure' (s p)
gstrengthenD (Rep w Any -> Either StrengthenFailure' (Rep s Any))
-> (w -> Rep w Any) -> w -> Either StrengthenFailure' (Rep s Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. w -> Rep w Any
forall x. w -> Rep w x
forall a x. Generic a => a -> Rep a x
from

-- | Generic strengthening at the datatype level.
class GStrengthenD w s where
    gstrengthenD :: w p -> Either StrengthenFailure' (s p)

-- | Strengthen a generic data type, replacing its metadata wrapping.
instance GStrengthenC wdn sdn w s
  => GStrengthenD
        (D1 (MetaData wdn _wmd2 _wmd3 _wmd4) w)
        (D1 (MetaData sdn _smd2 _smd3 _smd4) s) where
    gstrengthenD :: forall (p :: k).
D1 ('MetaData wdn _wmd2 _wmd3 _wmd4) w p
-> Either
     StrengthenFailure' (D1 ('MetaData sdn _smd2 _smd3 _smd4) s p)
gstrengthenD = (s p -> D1 ('MetaData sdn _smd2 _smd3 _smd4) s p)
-> Either StrengthenFailure' (s p)
-> Either
     StrengthenFailure' (D1 ('MetaData sdn _smd2 _smd3 _smd4) s p)
forall a b.
(a -> b)
-> Either StrengthenFailure' a -> Either StrengthenFailure' b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap s p -> D1 ('MetaData sdn _smd2 _smd3 _smd4) s p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (Either StrengthenFailure' (s p)
 -> Either
      StrengthenFailure' (D1 ('MetaData sdn _smd2 _smd3 _smd4) s p))
-> (D1 ('MetaData wdn _wmd2 _wmd3 _wmd4) w p
    -> Either StrengthenFailure' (s p))
-> D1 ('MetaData wdn _wmd2 _wmd3 _wmd4) w p
-> Either
     StrengthenFailure' (D1 ('MetaData sdn _smd2 _smd3 _smd4) s p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (wdn :: Symbol) (sdn :: Symbol) (w :: k -> Type)
       (s :: k -> Type) (p :: k).
GStrengthenC wdn sdn w s =>
w p -> Either StrengthenFailure' (s p)
forall (wdn :: Symbol) (sdn :: Symbol) (w :: k -> Type)
       (s :: k -> Type) (p :: k).
GStrengthenC wdn sdn w s =>
w p -> Either StrengthenFailure' (s p)
gstrengthenC @wdn @sdn (w p -> Either StrengthenFailure' (s p))
-> (D1 ('MetaData wdn _wmd2 _wmd3 _wmd4) w p -> w p)
-> D1 ('MetaData wdn _wmd2 _wmd3 _wmd4) w p
-> Either StrengthenFailure' (s p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. D1 ('MetaData wdn _wmd2 _wmd3 _wmd4) w p -> w p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1

-- | Generic strengthening at the constructor sum level.
class GStrengthenC (wdn :: Symbol) (sdn :: Symbol) w s where
    gstrengthenC :: w p -> Either StrengthenFailure' (s p)

-- | Nothing to do for empty datatypes.
instance GStrengthenC wdn sdn V1 V1 where gstrengthenC :: forall (p :: k). V1 p -> Either StrengthenFailure' (V1 p)
gstrengthenC = V1 p -> Either StrengthenFailure' (V1 p)
forall a b. b -> Either a b
Right

-- | Strengthen sum types by casing and strengthening left or right.
instance
  ( GStrengthenC wdn sdn wl sl
  , GStrengthenC wdn sdn wr sr
  ) => GStrengthenC wdn sdn (wl :+: wr) (sl :+: sr) where
    gstrengthenC :: forall (p :: k).
(:+:) wl wr p -> Either StrengthenFailure' ((:+:) sl sr p)
gstrengthenC = \case L1 wl p
l -> sl p -> (:+:) sl sr p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (sl p -> (:+:) sl sr p)
-> Either StrengthenFailure' (sl p)
-> Either StrengthenFailure' ((:+:) sl sr p)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (wdn :: Symbol) (sdn :: Symbol) (w :: k -> Type)
       (s :: k -> Type) (p :: k).
GStrengthenC wdn sdn w s =>
w p -> Either StrengthenFailure' (s p)
forall (wdn :: Symbol) (sdn :: Symbol) (w :: k -> Type)
       (s :: k -> Type) (p :: k).
GStrengthenC wdn sdn w s =>
w p -> Either StrengthenFailure' (s p)
gstrengthenC @wdn @sdn wl p
l
                         R1 wr p
r -> sr p -> (:+:) sl sr p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (sr p -> (:+:) sl sr p)
-> Either StrengthenFailure' (sr p)
-> Either StrengthenFailure' ((:+:) sl sr p)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (wdn :: Symbol) (sdn :: Symbol) (w :: k -> Type)
       (s :: k -> Type) (p :: k).
GStrengthenC wdn sdn w s =>
w p -> Either StrengthenFailure' (s p)
forall (wdn :: Symbol) (sdn :: Symbol) (w :: k -> Type)
       (s :: k -> Type) (p :: k).
GStrengthenC wdn sdn w s =>
w p -> Either StrengthenFailure' (s p)
gstrengthenC @wdn @sdn wr p
r

-- | Enter a constructor, stripping its metadata wrapper.
instance (GStrengthenS 0 w s, ReifyCstrs wcd wcn scd scn)
  => GStrengthenC wcd scd
        (C1 (MetaCons wcn _wmc2 _wmc3) w)
        (C1 (MetaCons scn _smc2 _smc3) s) where
    gstrengthenC :: forall (p :: k).
C1 ('MetaCons wcn _wmc2 _wmc3) w p
-> Either StrengthenFailure' (C1 ('MetaCons scn _smc2 _smc3) s p)
gstrengthenC (M1 w p
w) =
        case forall (i :: Natural) (w :: k -> Type) (s :: k -> Type) (p :: k).
GStrengthenS i w s =>
w p -> Either [(Builder, StrengthenFailure')] (s p)
forall {k} (i :: Natural) (w :: k -> Type) (s :: k -> Type)
       (p :: k).
GStrengthenS i w s =>
w p -> Either [(Builder, StrengthenFailure')] (s p)
gstrengthenS @0 w p
w of
          Right s p
s -> C1 ('MetaCons scn _smc2 _smc3) s p
-> Either StrengthenFailure' (C1 ('MetaCons scn _smc2 _smc3) s p)
forall a b. b -> Either a b
Right (s p -> C1 ('MetaCons scn _smc2 _smc3) s p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 s p
s)
          Left  [(Builder, StrengthenFailure')]
e -> [Builder]
-> [(Builder, StrengthenFailure')]
-> Either StrengthenFailure' (C1 ('MetaCons scn _smc2 _smc3) s p)
forall text a.
[text]
-> [(text, StrengthenFailure text)]
-> Either (StrengthenFailure text) a
failStrengthen [forall (ld :: Symbol) (lc :: Symbol) (rd :: Symbol) (rc :: Symbol).
ReifyCstrs ld lc rd rc =>
Builder
reifyCstrs @wcd @wcn @scd @scn] [(Builder, StrengthenFailure')]
e

type ReifyCstrs :: Symbol -> Symbol -> Symbol -> Symbol -> Constraint
class ReifyCstrs ld lc rd rc where reifyCstrs :: TBL.Builder

-- | Special case: data type and constructor names are equivalent: simplify
instance {-# OVERLAPPING #-} (KnownSymbol d, KnownSymbol c)
  => ReifyCstrs d c d c where
    {-# INLINE reifyCstrs #-}
    reifyCstrs :: Builder
reifyCstrs = Builder
dBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
"."Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
c
      where
        d :: Builder
d = String -> Builder
forall a. IsString a => String -> a
fromString (Proxy# d -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @d))
        c :: Builder
c = String -> Builder
forall a. IsString a => String -> a
fromString (Proxy# c -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @c))

instance (KnownSymbol ld, KnownSymbol lc, KnownSymbol rd, KnownSymbol rc)
  => ReifyCstrs ld lc rd rc where
    {-# INLINE reifyCstrs #-}
    reifyCstrs :: Builder
reifyCstrs = Builder
ldBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
"."Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
lcBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" -> "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
rdBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
"."Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
rc
      where
        ld :: Builder
ld = String -> Builder
forall a. IsString a => String -> a
fromString (Proxy# ld -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @ld))
        lc :: Builder
lc = String -> Builder
forall a. IsString a => String -> a
fromString (Proxy# lc -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @lc))
        rd :: Builder
rd = String -> Builder
forall a. IsString a => String -> a
fromString (Proxy# rd -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @rd))
        rc :: Builder
rc = String -> Builder
forall a. IsString a => String -> a
fromString (Proxy# rc -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @rc))

-- | Generic strengthening at the constructor level.
class GStrengthenS (i :: Natural) w s where
    gstrengthenS :: w p -> Either [(TBL.Builder, StrengthenFailure')] (s p)

-- | Nothing to do for empty constructors.
instance GStrengthenS i U1 U1 where gstrengthenS :: forall (p :: k).
U1 p -> Either [(Builder, StrengthenFailure')] (U1 p)
gstrengthenS = U1 p -> Either [(Builder, StrengthenFailure')] (U1 p)
forall a b. b -> Either a b
Right

-- | Strengthen product types by strengthening left and right.
instance
  ( GStrengthenS i                  wl sl
  , GStrengthenS (i + ProdArity wl) wr sr
  ) => GStrengthenS i (wl :*: wr) (sl :*: sr) where
    gstrengthenS :: forall (p :: k).
(:*:) wl wr p
-> Either [(Builder, StrengthenFailure')] ((:*:) sl sr p)
gstrengthenS (wl p
l :*: wr p
r) =
        -- With @Validation@, @A.liftA2 (:*:)@. But I don't have a use for it
        -- elsewhere, so let's just be explicit.
        case forall (i :: Natural) (w :: k -> Type) (s :: k -> Type) (p :: k).
GStrengthenS i w s =>
w p -> Either [(Builder, StrengthenFailure')] (s p)
forall {k} (i :: Natural) (w :: k -> Type) (s :: k -> Type)
       (p :: k).
GStrengthenS i w s =>
w p -> Either [(Builder, StrengthenFailure')] (s p)
gstrengthenS @i wl p
l of
          Right sl p
la ->
            case forall (i :: Natural) (w :: k -> Type) (s :: k -> Type) (p :: k).
GStrengthenS i w s =>
w p -> Either [(Builder, StrengthenFailure')] (s p)
forall {k} (i :: Natural) (w :: k -> Type) (s :: k -> Type)
       (p :: k).
GStrengthenS i w s =>
w p -> Either [(Builder, StrengthenFailure')] (s p)
gstrengthenS @(i + ProdArity wl) wr p
r of
              Right  sr p
ra -> (:*:) sl sr p
-> Either [(Builder, StrengthenFailure')] ((:*:) sl sr p)
forall a b. b -> Either a b
Right (sl p
la sl p -> sr p -> (:*:) sl sr p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: sr p
ra)
              Left   [(Builder, StrengthenFailure')]
re -> [(Builder, StrengthenFailure')]
-> Either [(Builder, StrengthenFailure')] ((:*:) sl sr p)
forall a b. a -> Either a b
Left [(Builder, StrengthenFailure')]
re
          Left  [(Builder, StrengthenFailure')]
le ->
            case forall (i :: Natural) (w :: k -> Type) (s :: k -> Type) (p :: k).
GStrengthenS i w s =>
w p -> Either [(Builder, StrengthenFailure')] (s p)
forall {k} (i :: Natural) (w :: k -> Type) (s :: k -> Type)
       (p :: k).
GStrengthenS i w s =>
w p -> Either [(Builder, StrengthenFailure')] (s p)
gstrengthenS @(i + ProdArity wl) @_ @sr wr p
r of
              Right sr p
_ra -> [(Builder, StrengthenFailure')]
-> Either [(Builder, StrengthenFailure')] ((:*:) sl sr p)
forall a b. a -> Either a b
Left [(Builder, StrengthenFailure')]
le
              Left   [(Builder, StrengthenFailure')]
re -> [(Builder, StrengthenFailure')]
-> Either [(Builder, StrengthenFailure')] ((:*:) sl sr p)
forall a b. a -> Either a b
Left ([(Builder, StrengthenFailure')]
le [(Builder, StrengthenFailure')]
-> [(Builder, StrengthenFailure')]
-> [(Builder, StrengthenFailure')]
forall a. Semigroup a => a -> a -> a
<> [(Builder, StrengthenFailure')]
re)

-- | Special case: if source and target types are equivalent, just replace meta.
--
-- Note that we have to expand the metadata awkwardly for the overlapping
-- instances to work correctly. (There should be a better way to write this, but
-- it's purely style, so light TODO.)
instance {-# OVERLAPPING #-} GStrengthenS i
  (S1 (MetaSel _wms1 _wms2 _wms3 _wms4) (Rec0 a))
  (S1 (MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a)) where
    gstrengthenS :: forall (p :: k).
S1 ('MetaSel _wms1 _wms2 _wms3 _wms4) (Rec0 a) p
-> Either
     [(Builder, StrengthenFailure')]
     (S1 ('MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a) p)
gstrengthenS = S1 ('MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a) p
-> Either
     [(Builder, StrengthenFailure')]
     (S1 ('MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a) p)
forall a b. b -> Either a b
Right (S1 ('MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a) p
 -> Either
      [(Builder, StrengthenFailure')]
      (S1 ('MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a) p))
-> (S1 ('MetaSel _wms1 _wms2 _wms3 _wms4) (Rec0 a) p
    -> S1 ('MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a) p)
-> S1 ('MetaSel _wms1 _wms2 _wms3 _wms4) (Rec0 a) p
-> Either
     [(Builder, StrengthenFailure')]
     (S1 ('MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a) p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec0 a p -> S1 ('MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a) p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (Rec0 a p -> S1 ('MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a) p)
-> (S1 ('MetaSel _wms1 _wms2 _wms3 _wms4) (Rec0 a) p -> Rec0 a p)
-> S1 ('MetaSel _wms1 _wms2 _wms3 _wms4) (Rec0 a) p
-> S1 ('MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. S1 ('MetaSel _wms1 _wms2 _wms3 _wms4) (Rec0 a) p -> Rec0 a p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1

-- | Strengthen a field using the existing 'Strengthen' instance.
instance
  ( Weakened s ~ w -- required, else "illegal typesym family app in instance"
  , Strengthen s
  , ReifySelector i wmr smr
  ) => GStrengthenS i
        (S1 (MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w))
        (S1 (MetaSel smr _sms2 _sms3 _sms4) (Rec0 s)) where
    gstrengthenS :: forall (p :: k).
S1 ('MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w) p
-> Either
     [(Builder, StrengthenFailure')]
     (S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p)
gstrengthenS = M1 S ('MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w) p -> Rec0 w p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1 (M1 S ('MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w) p -> Rec0 w p)
-> (Rec0 w p -> w)
-> M1 S ('MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w) p
-> w
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> Rec0 w p -> w
forall k i c (p :: k). K1 i c p -> c
unK1 (M1 S ('MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w) p -> w)
-> (w -> Either StrengthenFailure' s)
-> M1 S ('MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w) p
-> Either StrengthenFailure' s
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> w -> Either StrengthenFailure' s
Weakened s -> Either StrengthenFailure' s
forall a. Strengthen a => Weakened a -> Either StrengthenFailure' a
strengthen (M1 S ('MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w) p
 -> Either StrengthenFailure' s)
-> (Either StrengthenFailure' s
    -> Either
         [(Builder, StrengthenFailure')]
         (S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p))
-> M1 S ('MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w) p
-> Either
     [(Builder, StrengthenFailure')]
     (S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> \case
      Right s
s -> S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p
-> Either
     [(Builder, StrengthenFailure')]
     (S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p)
forall a b. b -> Either a b
Right (S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p
 -> Either
      [(Builder, StrengthenFailure')]
      (S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p))
-> S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p
-> Either
     [(Builder, StrengthenFailure')]
     (S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p)
forall a b. (a -> b) -> a -> b
$ Rec0 s p -> S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (Rec0 s p -> S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p)
-> Rec0 s p -> S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p
forall a b. (a -> b) -> a -> b
$ s -> Rec0 s p
forall k i c (p :: k). c -> K1 i c p
K1 s
s
      Left  StrengthenFailure'
e -> [(Builder, StrengthenFailure')]
-> Either
     [(Builder, StrengthenFailure')]
     (S1 ('MetaSel smr _sms2 _sms3 _sms4) (Rec0 s) p)
forall a b. a -> Either a b
Left  [(forall (i :: Natural) (l :: Maybe Symbol) (r :: Maybe Symbol).
ReifySelector i l r =>
Builder
reifySelector @i @wmr @smr, StrengthenFailure'
e)]

{- TODO
* how to separate index and record name? @.@ is good and bad, uses same syntax
  as @dt.cstr@ for different reason BUT is pretty clear
* how to lay out precisely? fairly arbitrary
-}
class ReifySelector (i :: Natural) (l :: Maybe Symbol) (r :: Maybe Symbol) where
    reifySelector :: TBL.Builder

-- | Special case: both types had a record name, and they're equal
instance {-# OVERLAPPING #-} (KnownNat i, KnownSymbol lnm)
  => ReifySelector i (Just lnm) (Just lnm) where
    -- TODO check overlap works correct
    {-# INLINE reifySelector #-}
    reifySelector :: Builder
reifySelector = Builder
iBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
"."Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
lnm
      where
        i :: Builder
i   = String -> Builder
forall a. IsString a => String -> a
fromString (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ Natural -> String
forall a. Show a => a -> String
show (Natural -> String) -> Natural -> String
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
natVal'' @i
        lnm :: Builder
lnm = String -> Builder
forall a. IsString a => String -> a
fromString (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ Proxy# lnm -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @lnm)

instance (KnownNat i, KnownSymbol lnm, KnownSymbol rnm)
  => ReifySelector i (Just lnm) (Just rnm) where
    {-# INLINE reifySelector #-}
    reifySelector :: Builder
reifySelector = Builder
iBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
"."Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
lnmBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" -> "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
rnm
      where
        i :: Builder
i   = String -> Builder
forall a. IsString a => String -> a
fromString (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ Natural -> String
forall a. Show a => a -> String
show (Natural -> String) -> Natural -> String
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
natVal'' @i
        lnm :: Builder
lnm = String -> Builder
forall a. IsString a => String -> a
fromString (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ Proxy# lnm -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @lnm)
        rnm :: Builder
rnm = String -> Builder
forall a. IsString a => String -> a
fromString (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ Proxy# rnm -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @rnm)

instance KnownNat i => ReifySelector i Nothing Nothing where
    {-# INLINE reifySelector #-}
    reifySelector :: Builder
reifySelector = String -> Builder
forall a. IsString a => String -> a
fromString (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ Natural -> String
forall a. Show a => a -> String
show (Natural -> String) -> Natural -> String
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
natVal'' @i

instance (KnownNat i, KnownSymbol lnm)
  => ReifySelector i (Just lnm) Nothing where
    {-# INLINE reifySelector #-}
    reifySelector :: Builder
reifySelector = Builder
iBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
"."Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
lnm
      where
        i :: Builder
i   = String -> Builder
forall a. IsString a => String -> a
fromString (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ Natural -> String
forall a. Show a => a -> String
show (Natural -> String) -> Natural -> String
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
natVal'' @i
        lnm :: Builder
lnm = String -> Builder
forall a. IsString a => String -> a
fromString (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ Proxy# lnm -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @lnm)

instance (KnownNat i, KnownSymbol rnm)
  => ReifySelector i Nothing (Just rnm) where
    {-# INLINE reifySelector #-}
    reifySelector :: Builder
reifySelector = Builder
iBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" -> "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
rnm
      where
        i :: Builder
i   = String -> Builder
forall a. IsString a => String -> a
fromString (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ Natural -> String
forall a. Show a => a -> String
show (Natural -> String) -> Natural -> String
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
natVal'' @i
        rnm :: Builder
rnm = String -> Builder
forall a. IsString a => String -> a
fromString (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ Proxy# rnm -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @rnm)

--------------------------------------------------------------------------------

-- from flow
(.>) :: (a -> b) -> (b -> c) -> a -> c
a -> b
f .> :: forall a b c. (a -> b) -> (b -> c) -> a -> c
.> b -> c
g = b -> c
g (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f

--------------------------------------------------------------------------------

-- could define this with @Generic.Type.Function.FoldMap.GTFoldMapC (+) 0 _@...
-- but pretty dumb LOL
type family ProdArity (f :: k -> Type) :: Natural where
    ProdArity (S1 c f)  = 1
    ProdArity (l :*: r) = ProdArity l + ProdArity r