{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
-- | A class for converting tensors between different forms that contain
-- the same data but varying amounts of shape information.
module HordeAd.Core.ConvertTensor
  ( ConvertTensor(..)
  ) where

import Prelude

import Data.Type.Equality (gcastWith, (:~:) (Refl))
import GHC.TypeLits (KnownNat, Nat, type (+))

import Data.Array.Nested (MapJust, Replicate, type (++))
import Data.Array.Nested.Convert (shxFromShS)
import Data.Array.Nested.Lemmas
import Data.Array.Nested.Mixed.Shape
import Data.Array.Nested.Shaped.Shape
import Data.Array.Nested.Types (unsafeCoerceRefl)

import HordeAd.Core.TensorKind
import HordeAd.Core.Types

class ConvertTensor (target :: Target) where
  -- | The universal conversion function that can emulate all conversion
  -- methods below, but requires an explicit recipe in the first argument.
  --
  -- All conversion operations below could be defined in terms of @tconvert@,
  -- but they'd need additional singleton arguments or constraints
  -- or we'd need to depend on 'HordeAd.Core.Ops.BaseTensor'
  -- to use 'HordeAd.Core.Ops.rshape', etc.
  tconvert :: TKConversion a b -> SingletonTK a -> target a -> target b

  -- | The conversion from a rank 0 ranked tensor to a scalar.
  kfromR :: GoodScalar r => target (TKR 0 r) -> target (TKScalar r)
  kfromR = target (TKS ('[] @Nat) r) -> target (TKScalar r)
forall r.
GoodScalar r =>
target (TKS ('[] @Nat) r) -> target (TKScalar r)
forall (target :: Target) r.
(ConvertTensor target, GoodScalar r) =>
target (TKS ('[] @Nat) r) -> target (TKScalar r)
kfromS (target (TKS ('[] @Nat) r) -> target (TKScalar r))
-> (target (TKR 0 r) -> target (TKS ('[] @Nat) r))
-> target (TKR 0 r)
-> target (TKScalar r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. target (TKR 0 r) -> target (TKS ('[] @Nat) r)
target (TKR2 (Rank @Nat ('[] @Nat)) (TKScalar r))
-> target (TKS ('[] @Nat) r)
forall (sh :: [Nat]) (x :: TK).
(KnownShS sh, KnownSTK x) =>
target (TKR2 (Rank @Nat sh) x) -> target (TKS2 sh x)
forall (target :: Target) (sh :: [Nat]) (x :: TK).
(ConvertTensor target, KnownShS sh, KnownSTK x) =>
target (TKR2 (Rank @Nat sh) x) -> target (TKS2 sh x)
sfromR
  -- | The conversion from an empty shape shaped tensor to a scalar.
  kfromS :: GoodScalar r => target (TKS '[] r) -> target (TKScalar r)
  kfromS = let c :: TKConversion (TKS2 ('[] @Nat) b) b
c = TKConversion (TKX2 ('[] @(Maybe Nat)) b) b
-> TKConversion (TKS2 ('[] @Nat) b) (TKX2 ('[] @(Maybe Nat)) b)
-> TKConversion (TKS2 ('[] @Nat) b) b
forall (b1 :: TK) (b :: TK) (a :: TK).
TKConversion b1 b -> TKConversion a b1 -> TKConversion a b
ConvCmp TKConversion (TKX2 ('[] @(Maybe Nat)) b) b
forall (b :: TK). TKConversion (TKX2 ('[] @(Maybe Nat)) b) b
ConvX0 TKConversion (TKS2 ('[] @Nat) b) (TKX2 ('[] @(Maybe Nat)) b)
TKConversion (TKS2 ('[] @Nat) b) (TKX2 (MapJust @Nat ('[] @Nat)) b)
forall (sh :: [Nat]) (a1 :: TK).
TKConversion (TKS2 sh a1) (TKX2 (MapJust @Nat sh) a1)
ConvSX
           in TKConversion (TKS ('[] @Nat) r) (TKScalar r)
-> SingletonTK (TKS ('[] @Nat) r)
-> target (TKS ('[] @Nat) r)
-> target (TKScalar r)
forall (a :: TK) (b :: TK).
TKConversion a b -> SingletonTK a -> target a -> target b
forall (target :: Target) (a :: TK) (b :: TK).
ConvertTensor target =>
TKConversion a b -> SingletonTK a -> target a -> target b
tconvert TKConversion (TKS ('[] @Nat) r) (TKScalar r)
forall {b :: TK}. TKConversion (TKS2 ('[] @Nat) b) b
c (ShS ('[] @Nat)
-> SingletonTK (TKScalar r) -> SingletonTK (TKS ('[] @Nat) r)
forall (sh :: [Nat]) (x :: TK).
ShS sh -> SingletonTK x -> SingletonTK (TKS2 sh x)
STKS ShS ('[] @Nat)
forall (sh :: [Nat]).
((sh :: [Nat]) ~ ('[] @Nat :: [Nat])) =>
ShS sh
ZSS SingletonTK (TKScalar r)
forall r. GoodScalar r => SingletonTK (TKScalar r)
STKScalar)
  kfromX :: GoodScalar r => target (TKX '[] r) -> target (TKScalar r)
  kfromX = target (TKS ('[] @Nat) r) -> target (TKScalar r)
forall r.
GoodScalar r =>
target (TKS ('[] @Nat) r) -> target (TKScalar r)
forall (target :: Target) r.
(ConvertTensor target, GoodScalar r) =>
target (TKS ('[] @Nat) r) -> target (TKScalar r)
kfromS (target (TKS ('[] @Nat) r) -> target (TKScalar r))
-> (target (TKX ('[] @(Maybe Nat)) r) -> target (TKS ('[] @Nat) r))
-> target (TKX ('[] @(Maybe Nat)) r)
-> target (TKScalar r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. target (TKX ('[] @(Maybe Nat)) r) -> target (TKS ('[] @Nat) r)
forall (sh :: [Nat]) (sh' :: [Maybe Nat]) (x :: TK).
(KnownShS sh,
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKX2 sh' x) -> target (TKS2 sh x)
forall (target :: Target) (sh :: [Nat]) (sh' :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh,
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKX2 sh' x) -> target (TKS2 sh x)
sfromX
  rfromK :: GoodScalar r => target (TKScalar r) -> target (TKR 0 r)
  rfromK = target (TKS2 ('[] @Nat) (TKScalar r))
-> target (TKR2 0 (TKScalar r))
target (TKS2 ('[] @Nat) (TKScalar r))
-> target (TKR2 (Rank @Nat ('[] @Nat)) (TKScalar r))
forall (sh :: [Nat]) (x :: TK).
(KnownShS sh, KnownSTK x) =>
target (TKS2 sh x) -> target (TKR2 (Rank @Nat sh) x)
forall (target :: Target) (sh :: [Nat]) (x :: TK).
(ConvertTensor target, KnownShS sh, KnownSTK x) =>
target (TKS2 sh x) -> target (TKR2 (Rank @Nat sh) x)
rfromS (target (TKS2 ('[] @Nat) (TKScalar r))
 -> target (TKR2 0 (TKScalar r)))
-> (target (TKScalar r) -> target (TKS2 ('[] @Nat) (TKScalar r)))
-> target (TKScalar r)
-> target (TKR2 0 (TKScalar r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. target (TKScalar r) -> target (TKS2 ('[] @Nat) (TKScalar r))
forall r.
GoodScalar r =>
target (TKScalar r) -> target (TKS ('[] @Nat) r)
forall (target :: Target) r.
(ConvertTensor target, GoodScalar r) =>
target (TKScalar r) -> target (TKS ('[] @Nat) r)
sfromK
  -- | The conversion from a shaped tensor to the corresponding ranked tensor
  -- of the same rank.
  rfromS :: forall sh x. (KnownShS sh, KnownSTK x)
         => target (TKS2 sh x) -> target (TKR2 (Rank sh) x)
  rfromS | (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh)) (Rank @Nat sh)
Refl <- ShS sh
-> (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh)) (Rank @Nat sh)
forall (sh :: [Nat]).
ShS sh
-> (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh)) (Rank @Nat sh)
lemRankMapJust (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh) =
    let c :: TKConversion
  (TKS2 sh x) (TKR2 (Rank @(Maybe Nat) (MapJust @Nat sh)) x)
c = TKConversion
  (TKX2 (MapJust @Nat sh) x)
  (TKR2 (Rank @(Maybe Nat) (MapJust @Nat sh)) x)
-> TKConversion (TKS2 sh x) (TKX2 (MapJust @Nat sh) x)
-> TKConversion
     (TKS2 sh x) (TKR2 (Rank @(Maybe Nat) (MapJust @Nat sh)) x)
forall (b1 :: TK) (b :: TK) (a :: TK).
TKConversion b1 b -> TKConversion a b1 -> TKConversion a b
ConvCmp (SingletonTK x
-> TKConversion
     (TKX2 (MapJust @Nat sh) x)
     (TKR2 (Rank @(Maybe Nat) (MapJust @Nat sh)) x)
forall (a1 :: TK) (sh :: [Maybe Nat]).
SingletonTK a1
-> TKConversion (TKX2 sh a1) (TKR2 (Rank @(Maybe Nat) sh) a1)
ConvXR SingletonTK x
forall (y :: TK). KnownSTK y => SingletonTK y
knownSTK) TKConversion (TKS2 sh x) (TKX2 (MapJust @Nat sh) x)
forall (sh :: [Nat]) (a1 :: TK).
TKConversion (TKS2 sh a1) (TKX2 (MapJust @Nat sh) a1)
ConvSX
    in TKConversion (TKS2 sh x) (TKR2 (Rank @Nat sh) x)
-> SingletonTK (TKS2 sh x)
-> target (TKS2 sh x)
-> target (TKR2 (Rank @Nat sh) x)
forall (a :: TK) (b :: TK).
TKConversion a b -> SingletonTK a -> target a -> target b
forall (target :: Target) (a :: TK) (b :: TK).
ConvertTensor target =>
TKConversion a b -> SingletonTK a -> target a -> target b
tconvert TKConversion (TKS2 sh x) (TKR2 (Rank @Nat sh) x)
TKConversion
  (TKS2 sh x) (TKR2 (Rank @(Maybe Nat) (MapJust @Nat sh)) x)
forall {sh :: [Nat]}.
TKConversion
  (TKS2 sh x) (TKR2 (Rank @(Maybe Nat) (MapJust @Nat sh)) x)
c (ShS sh -> SingletonTK x -> SingletonTK (TKS2 sh x)
forall (sh :: [Nat]) (x :: TK).
ShS sh -> SingletonTK x -> SingletonTK (TKS2 sh x)
STKS ShS sh
forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS SingletonTK x
forall (y :: TK). KnownSTK y => SingletonTK y
knownSTK)
  rfromX :: forall sh x. KnownSTK x
         => target (TKX2 sh x) -> target (TKR2 (Rank sh) x)
  sfromK :: GoodScalar r => target (TKScalar r) -> target (TKS '[] r)
  sfromK = let c :: TKConversion (TKScalar r) (TKS2 ('[] @Nat) (TKScalar r))
c = TKConversion
  (TKX2 ('[] @(Maybe Nat)) (TKScalar r))
  (TKS2 ('[] @Nat) (TKScalar r))
-> TKConversion (TKScalar r) (TKX2 ('[] @(Maybe Nat)) (TKScalar r))
-> TKConversion (TKScalar r) (TKS2 ('[] @Nat) (TKScalar r))
forall (b1 :: TK) (b :: TK) (a :: TK).
TKConversion b1 b -> TKConversion a b1 -> TKConversion a b
ConvCmp TKConversion
  (TKX2 ('[] @(Maybe Nat)) (TKScalar r))
  (TKS2 ('[] @Nat) (TKScalar r))
TKConversion
  (TKX2 (MapJust @Nat ('[] @Nat)) (TKScalar r))
  (TKS2 ('[] @Nat) (TKScalar r))
forall (sh :: [Nat]) (a1 :: TK).
TKConversion (TKX2 (MapJust @Nat sh) a1) (TKS2 sh a1)
ConvXS (SingletonTK (TKScalar r)
-> TKConversion (TKScalar r) (TKX2 ('[] @(Maybe Nat)) (TKScalar r))
forall (a :: TK).
SingletonTK a -> TKConversion a (TKX2 ('[] @(Maybe Nat)) a)
Conv0X SingletonTK (TKScalar r)
forall r. GoodScalar r => SingletonTK (TKScalar r)
STKScalar)
           in TKConversion (TKScalar r) (TKS2 ('[] @Nat) (TKScalar r))
-> SingletonTK (TKScalar r)
-> target (TKScalar r)
-> target (TKS2 ('[] @Nat) (TKScalar r))
forall (a :: TK) (b :: TK).
TKConversion a b -> SingletonTK a -> target a -> target b
forall (target :: Target) (a :: TK) (b :: TK).
ConvertTensor target =>
TKConversion a b -> SingletonTK a -> target a -> target b
tconvert TKConversion (TKScalar r) (TKS2 ('[] @Nat) (TKScalar r))
c SingletonTK (TKScalar r)
forall r. GoodScalar r => SingletonTK (TKScalar r)
STKScalar
  -- | The conversion from a ranked tensor to the corresponding shaped tensor
  -- of the same rank.
  sfromR :: (KnownShS sh, KnownSTK x)
         => target (TKR2 (Rank sh) x) -> target (TKS2 sh x)
  sfromX :: (KnownShS sh, Rank sh ~ Rank sh', KnownSTK x)
         => target (TKX2 sh' x) -> target (TKS2 sh x)
  xfromK :: GoodScalar r => target (TKScalar r) -> target (TKX '[] r)
  xfromK = target (TKS2 ('[] @Nat) (TKScalar r))
-> target (TKX2 ('[] @(Maybe Nat)) (TKScalar r))
forall (sh :: [Nat]) (sh' :: [Maybe Nat]) (x :: TK).
(KnownShS sh, KnownShX sh',
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKS2 sh x) -> target (TKX2 sh' x)
forall (target :: Target) (sh :: [Nat]) (sh' :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh, KnownShX sh',
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKS2 sh x) -> target (TKX2 sh' x)
xfromS (target (TKS2 ('[] @Nat) (TKScalar r))
 -> target (TKX2 ('[] @(Maybe Nat)) (TKScalar r)))
-> (target (TKScalar r) -> target (TKS2 ('[] @Nat) (TKScalar r)))
-> target (TKScalar r)
-> target (TKX2 ('[] @(Maybe Nat)) (TKScalar r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. target (TKScalar r) -> target (TKS2 ('[] @Nat) (TKScalar r))
forall r.
GoodScalar r =>
target (TKScalar r) -> target (TKS ('[] @Nat) r)
forall (target :: Target) r.
(ConvertTensor target, GoodScalar r) =>
target (TKScalar r) -> target (TKS ('[] @Nat) r)
sfromK
  xfromR :: (KnownShX sh', KnownSTK x)
         => target (TKR2 (Rank sh') x) -> target (TKX2 sh' x)
  xfromS :: (KnownShS sh, KnownShX sh', Rank sh ~ Rank sh', KnownSTK x)
         => target (TKS2 sh x) -> target (TKX2 sh' x)

  rzip :: forall y z n. (KnownSTK y, KnownSTK z)
       => target (TKProduct (TKR2 n y) (TKR2 n z))
       -> target (TKR2 n (TKProduct y z))
  runzip :: forall y z n.
            target (TKR2 n (TKProduct y z))
         -> target (TKProduct (TKR2 n y) (TKR2 n z))
  szip :: forall y z sh. (KnownSTK y, KnownSTK z)
       => target (TKProduct (TKS2 sh y) (TKS2 sh z))
       -> target (TKS2 sh (TKProduct y z))
  sunzip :: forall y z sh.
            target (TKS2 sh (TKProduct y z))
         -> target (TKProduct (TKS2 sh y) (TKS2 sh z))
  xzip :: forall y z sh. (KnownSTK y, KnownSTK z)
       => target (TKProduct (TKX2 sh y) (TKX2 sh z))
       -> target (TKX2 sh (TKProduct y z))
  xunzip :: forall y z sh.
            target (TKX2 sh (TKProduct y z))
         -> target (TKProduct (TKX2 sh y) (TKX2 sh z))

  rnest :: forall n m x.
           (KnownNat m, KnownSTK x)
        => SNat n -> target (TKR2 (n + m) x)
        -> target (TKR2 n (TKR2 m x))
  rnest n :: SNat n
n@SNat n
SNat =
    (:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> target (TKR2 (n + m) x)
-> target (TKR2 n (TKR2 m x))
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith ((:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
forall {k} (a :: k) (b :: k). (:~:) @k a b
unsafeCoerceRefl :: Rank (Replicate n (Nothing @Nat)) :~: n) ((((Rank
      @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
   ~ (n :: Nat)) =>
  target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
 -> target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> target (TKR2 (n + m) x)
-> target (TKR2 n (TKR2 m x))
forall a b. (a -> b) -> a -> b
$
    (:~:)
  @Nat
  (Rank
     @(Maybe Nat)
     ((++)
        @(Maybe Nat)
        (Replicate @(Maybe Nat) n ('Nothing @Nat))
        (Replicate @(Maybe Nat) m ('Nothing @Nat))))
  (n + m)
-> (((Rank
        @(Maybe Nat)
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (Replicate @(Maybe Nat) m ('Nothing @Nat))) :: Nat)
     ~ (n + m :: Nat)) =>
    target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> target (TKR2 (n + m) x)
-> target (TKR2 n (TKR2 m x))
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith ((:~:)
  @Nat
  (Rank
     @(Maybe Nat)
     ((++)
        @(Maybe Nat)
        (Replicate @(Maybe Nat) n ('Nothing @Nat))
        (Replicate @(Maybe Nat) m ('Nothing @Nat))))
  (n + m)
forall {k} (a :: k) (b :: k). (:~:) @k a b
unsafeCoerceRefl :: Rank (Replicate n (Nothing @Nat)
                                         ++ Replicate m Nothing) :~: n + m) ((((Rank
      @(Maybe Nat)
      ((++)
         @(Maybe Nat)
         (Replicate @(Maybe Nat) n ('Nothing @Nat))
         (Replicate @(Maybe Nat) m ('Nothing @Nat))) :: Nat)
   ~ (n + m :: Nat)) =>
  target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
 -> target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> (((Rank
        @(Maybe Nat)
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (Replicate @(Maybe Nat) m ('Nothing @Nat))) :: Nat)
     ~ (n + m :: Nat)) =>
    target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> target (TKR2 (n + m) x)
-> target (TKR2 n (TKR2 m x))
forall a b. (a -> b) -> a -> b
$
    (:~:)
  @[Maybe Nat]
  (Replicate @(Maybe Nat) (n + m) ('Nothing @Nat))
  ((++)
     @(Maybe Nat)
     (Replicate @(Maybe Nat) n ('Nothing @Nat))
     (Replicate @(Maybe Nat) m ('Nothing @Nat)))
-> (((Replicate @(Maybe Nat) (n + m) ('Nothing @Nat) :: [Maybe
                                                           Nat])
     ~ ((++)
          @(Maybe Nat)
          (Replicate @(Maybe Nat) n ('Nothing @Nat))
          (Replicate @(Maybe Nat) m ('Nothing @Nat)) :: [Maybe Nat])) =>
    target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> target (TKR2 (n + m) x)
-> target (TKR2 n (TKR2 m x))
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith ((:~:)
  @[Maybe Nat]
  (Replicate @(Maybe Nat) (n + m) ('Nothing @Nat))
  ((++)
     @(Maybe Nat)
     (Replicate @(Maybe Nat) n ('Nothing @Nat))
     (Replicate @(Maybe Nat) m ('Nothing @Nat)))
forall {k} (a :: k) (b :: k). (:~:) @k a b
unsafeCoerceRefl :: Replicate (n + m) (Nothing @Nat)
                                    :~: Replicate n (Nothing @Nat)
                                        ++ Replicate m Nothing) ((((Replicate @(Maybe Nat) (n + m) ('Nothing @Nat) :: [Maybe Nat])
   ~ ((++)
        @(Maybe Nat)
        (Replicate @(Maybe Nat) n ('Nothing @Nat))
        (Replicate @(Maybe Nat) m ('Nothing @Nat)) :: [Maybe Nat])) =>
  target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
 -> target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> (((Replicate @(Maybe Nat) (n + m) ('Nothing @Nat) :: [Maybe
                                                           Nat])
     ~ ((++)
          @(Maybe Nat)
          (Replicate @(Maybe Nat) n ('Nothing @Nat))
          (Replicate @(Maybe Nat) m ('Nothing @Nat)) :: [Maybe Nat])) =>
    target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> target (TKR2 (n + m) x)
-> target (TKR2 n (TKR2 m x))
forall a b. (a -> b) -> a -> b
$
    StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> target (TKR2 (n + m) x)
-> target (TKR2 n (TKR2 m x))
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate SNat n
n) ((KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
  target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
 -> target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> target (TKR2 (n + m) x)
-> target (TKR2 n (TKR2 m x))
forall a b. (a -> b) -> a -> b
$
    StaticShX (Replicate @(Maybe Nat) (n + m) ('Nothing @Nat))
-> (KnownShX (Replicate @(Maybe Nat) (n + m) ('Nothing @Nat)) =>
    target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> target (TKR2 (n + m) x)
-> target (TKR2 n (TKR2 m x))
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (SNat (n + m)
-> StaticShX (Replicate @(Maybe Nat) (n + m) ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate (forall (n :: Nat). KnownNat n => SNat n
SNat @(n + m))) ((KnownShX (Replicate @(Maybe Nat) (n + m) ('Nothing @Nat)) =>
  target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
 -> target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> (KnownShX (Replicate @(Maybe Nat) (n + m) ('Nothing @Nat)) =>
    target (TKR2 (n + m) x) -> target (TKR2 n (TKR2 m x)))
-> target (TKR2 (n + m) x)
-> target (TKR2 n (TKR2 m x))
forall a b. (a -> b) -> a -> b
$
    target (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKR2 m x))
-> target (TKR2 n (TKR2 m x))
target (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKR2 m x))
-> target
     (TKR2
        (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
        (TKR2 m x))
forall (sh :: [Maybe Nat]) (x :: TK).
KnownSTK x =>
target (TKX2 sh x) -> target (TKR2 (Rank @(Maybe Nat) sh) x)
forall (target :: Target) (sh :: [Maybe Nat]) (x :: TK).
(ConvertTensor target, KnownSTK x) =>
target (TKX2 sh x) -> target (TKR2 (Rank @(Maybe Nat) sh) x)
rfromX (target
   (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKR2 m x))
 -> target (TKR2 n (TKR2 m x)))
-> (target (TKR2 (n + m) x)
    -> target
         (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKR2 m x)))
-> target (TKR2 (n + m) x)
-> target (TKR2 n (TKR2 m x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target
     (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKR2 m x))
forall (sh1 :: [Maybe Nat]) (m :: Nat) (x :: TK).
(KnownNat m, KnownSTK x) =>
StaticShX sh1
-> target
     (TKX2
        ((++) @(Maybe Nat) sh1 (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKX2 sh1 (TKR2 m x))
forall (target :: Target) (sh1 :: [Maybe Nat]) (m :: Nat)
       (x :: TK).
(ConvertTensor target, KnownNat m, KnownSTK x) =>
StaticShX sh1
-> target
     (TKX2
        ((++) @(Maybe Nat) sh1 (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKX2 sh1 (TKR2 m x))
xnestR (SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate SNat n
n) (target
   (TKX2
      ((++)
         @(Maybe Nat)
         (Replicate @(Maybe Nat) n ('Nothing @Nat))
         (Replicate @(Maybe Nat) m ('Nothing @Nat)))
      x)
 -> target
      (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKR2 m x)))
-> (target (TKR2 (n + m) x)
    -> target
         (TKX2
            ((++)
               @(Maybe Nat)
               (Replicate @(Maybe Nat) n ('Nothing @Nat))
               (Replicate @(Maybe Nat) m ('Nothing @Nat)))
            x))
-> target (TKR2 (n + m) x)
-> target
     (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKR2 m x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (target :: Target) (sh' :: [Maybe Nat]) (x :: TK).
(ConvertTensor target, KnownShX sh', KnownSTK x) =>
target (TKR2 (Rank @(Maybe Nat) sh') x) -> target (TKX2 sh' x)
xfromR @_ @(Replicate (n + m) Nothing)
  -- Some of these operations have awkward type signatures, but the signatures
  -- express the most type-safe, or in other words the strongest versions
  -- of the typing possible.
  rnestS :: forall n sh2 x.
            (KnownShS sh2, KnownSTK x)
         => SNat n -> target (TKX2 (Replicate n Nothing ++ MapJust sh2) x)
         -> target (TKR2 n (TKS2 sh2 x))
  rnestS n :: SNat n
n@SNat n
SNat =
    (:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target
      (TKX2
         ((++)
            @(Maybe Nat)
            (Replicate @(Maybe Nat) n ('Nothing @Nat))
            (MapJust @Nat sh2))
         x)
    -> target (TKR2 n (TKS2 sh2 x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
-> target (TKR2 n (TKS2 sh2 x))
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith ((:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
forall {k} (a :: k) (b :: k). (:~:) @k a b
unsafeCoerceRefl :: Rank (Replicate n (Nothing @Nat)) :~: n) ((((Rank
      @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
   ~ (n :: Nat)) =>
  target
    (TKX2
       ((++)
          @(Maybe Nat)
          (Replicate @(Maybe Nat) n ('Nothing @Nat))
          (MapJust @Nat sh2))
       x)
  -> target (TKR2 n (TKS2 sh2 x)))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (Replicate @(Maybe Nat) n ('Nothing @Nat))
            (MapJust @Nat sh2))
         x)
 -> target (TKR2 n (TKS2 sh2 x)))
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target
      (TKX2
         ((++)
            @(Maybe Nat)
            (Replicate @(Maybe Nat) n ('Nothing @Nat))
            (MapJust @Nat sh2))
         x)
    -> target (TKR2 n (TKS2 sh2 x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
-> target (TKR2 n (TKS2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target
      (TKX2
         ((++)
            @(Maybe Nat)
            (Replicate @(Maybe Nat) n ('Nothing @Nat))
            (MapJust @Nat sh2))
         x)
    -> target (TKR2 n (TKS2 sh2 x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
-> target (TKR2 n (TKS2 sh2 x))
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate SNat n
n) ((KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
  target
    (TKX2
       ((++)
          @(Maybe Nat)
          (Replicate @(Maybe Nat) n ('Nothing @Nat))
          (MapJust @Nat sh2))
       x)
  -> target (TKR2 n (TKS2 sh2 x)))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (Replicate @(Maybe Nat) n ('Nothing @Nat))
            (MapJust @Nat sh2))
         x)
 -> target (TKR2 n (TKS2 sh2 x)))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target
      (TKX2
         ((++)
            @(Maybe Nat)
            (Replicate @(Maybe Nat) n ('Nothing @Nat))
            (MapJust @Nat sh2))
         x)
    -> target (TKR2 n (TKS2 sh2 x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
-> target (TKR2 n (TKS2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    target
  (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKS2 sh2 x))
-> target (TKR2 n (TKS2 sh2 x))
target
  (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKS2 sh2 x))
-> target
     (TKR2
        (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
        (TKS2 sh2 x))
forall (sh :: [Maybe Nat]) (x :: TK).
KnownSTK x =>
target (TKX2 sh x) -> target (TKR2 (Rank @(Maybe Nat) sh) x)
forall (target :: Target) (sh :: [Maybe Nat]) (x :: TK).
(ConvertTensor target, KnownSTK x) =>
target (TKX2 sh x) -> target (TKR2 (Rank @(Maybe Nat) sh) x)
rfromX (target
   (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKS2 sh2 x))
 -> target (TKR2 n (TKS2 sh2 x)))
-> (target
      (TKX2
         ((++)
            @(Maybe Nat)
            (Replicate @(Maybe Nat) n ('Nothing @Nat))
            (MapJust @Nat sh2))
         x)
    -> target
         (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKS2 sh2 x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
-> target (TKR2 n (TKS2 sh2 x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
-> target
     (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKS2 sh2 x))
forall (sh1 :: [Maybe Nat]) (sh2 :: [Nat]) (x :: TK).
(KnownShS sh2, KnownSTK x) =>
StaticShX sh1
-> target (TKX2 ((++) @(Maybe Nat) sh1 (MapJust @Nat sh2)) x)
-> target (TKX2 sh1 (TKS2 sh2 x))
forall (target :: Target) (sh1 :: [Maybe Nat]) (sh2 :: [Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh2, KnownSTK x) =>
StaticShX sh1
-> target (TKX2 ((++) @(Maybe Nat) sh1 (MapJust @Nat sh2)) x)
-> target (TKX2 sh1 (TKS2 sh2 x))
xnestS (SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate SNat n
n)
  rnestX :: forall n sh2 x.
            (KnownShX sh2, KnownSTK x)
         => SNat n -> target (TKX2 (Replicate n Nothing ++ sh2) x)
         -> target (TKR2 n (TKX2 sh2 x))
  rnestX n :: SNat n
n@SNat n
SNat =
    (:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target
      (TKX2
         ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
         x)
    -> target (TKR2 n (TKX2 sh2 x)))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
-> target (TKR2 n (TKX2 sh2 x))
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith ((:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
forall {k} (a :: k) (b :: k). (:~:) @k a b
unsafeCoerceRefl :: Rank (Replicate n (Nothing @Nat)) :~: n) ((((Rank
      @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
   ~ (n :: Nat)) =>
  target
    (TKX2
       ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
       x)
  -> target (TKR2 n (TKX2 sh2 x)))
 -> target
      (TKX2
         ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
         x)
 -> target (TKR2 n (TKX2 sh2 x)))
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target
      (TKX2
         ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
         x)
    -> target (TKR2 n (TKX2 sh2 x)))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
-> target (TKR2 n (TKX2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target
      (TKX2
         ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
         x)
    -> target (TKR2 n (TKX2 sh2 x)))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
-> target (TKR2 n (TKX2 sh2 x))
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate SNat n
n) ((KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
  target
    (TKX2
       ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
       x)
  -> target (TKR2 n (TKX2 sh2 x)))
 -> target
      (TKX2
         ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
         x)
 -> target (TKR2 n (TKX2 sh2 x)))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target
      (TKX2
         ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
         x)
    -> target (TKR2 n (TKX2 sh2 x)))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
-> target (TKR2 n (TKX2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    target
  (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKX2 sh2 x))
-> target (TKR2 n (TKX2 sh2 x))
target
  (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKX2 sh2 x))
-> target
     (TKR2
        (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
        (TKX2 sh2 x))
forall (sh :: [Maybe Nat]) (x :: TK).
KnownSTK x =>
target (TKX2 sh x) -> target (TKR2 (Rank @(Maybe Nat) sh) x)
forall (target :: Target) (sh :: [Maybe Nat]) (x :: TK).
(ConvertTensor target, KnownSTK x) =>
target (TKX2 sh x) -> target (TKR2 (Rank @(Maybe Nat) sh) x)
rfromX (target
   (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKX2 sh2 x))
 -> target (TKR2 n (TKX2 sh2 x)))
-> (target
      (TKX2
         ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
         x)
    -> target
         (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKX2 sh2 x)))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
-> target (TKR2 n (TKX2 sh2 x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
-> target
     (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKX2 sh2 x))
forall (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat]) (x :: TK).
(KnownShX sh2, KnownSTK x) =>
StaticShX sh1
-> target (TKX2 ((++) @(Maybe Nat) sh1 sh2) x)
-> target (TKX2 sh1 (TKX2 sh2 x))
forall (target :: Target) (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShX sh2, KnownSTK x) =>
StaticShX sh1
-> target (TKX2 ((++) @(Maybe Nat) sh1 sh2) x)
-> target (TKX2 sh1 (TKX2 sh2 x))
xnest (SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate SNat n
n)
  snestR :: forall sh1 m x.
            (KnownNat m, KnownSTK x)
         => ShS sh1 -> target (TKX2 (MapJust sh1 ++ Replicate m Nothing) x)
         -> target (TKS2 sh1 (TKR2 m x))
  snestR ShS sh1
sh1 =
    (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x)
    -> target (TKS2 sh1 (TKR2 m x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKS2 sh1 (TKR2 m x))
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith (ShS sh1
-> (:~:)
     @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
forall (sh :: [Nat]).
ShS sh
-> (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh)) (Rank @Nat sh)
lemRankMapJust ShS sh1
sh1) ((((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
   ~ (Rank @Nat sh1 :: Nat)) =>
  target
    (TKX2
       ((++)
          @(Maybe Nat)
          (MapJust @Nat sh1)
          (Replicate @(Maybe Nat) m ('Nothing @Nat)))
       x)
  -> target (TKS2 sh1 (TKR2 m x)))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x)
 -> target (TKS2 sh1 (TKR2 m x)))
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x)
    -> target (TKS2 sh1 (TKR2 m x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKS2 sh1 (TKR2 m x))
forall a b. (a -> b) -> a -> b
$
    ShS sh1
-> (KnownShS sh1 =>
    target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x)
    -> target (TKS2 sh1 (TKR2 m x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKS2 sh1 (TKR2 m x))
forall (sh :: [Nat]) r. ShS sh -> (KnownShS sh => r) -> r
withKnownShS ShS sh1
sh1 ((KnownShS sh1 =>
  target
    (TKX2
       ((++)
          @(Maybe Nat)
          (MapJust @Nat sh1)
          (Replicate @(Maybe Nat) m ('Nothing @Nat)))
       x)
  -> target (TKS2 sh1 (TKR2 m x)))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x)
 -> target (TKS2 sh1 (TKR2 m x)))
-> (KnownShS sh1 =>
    target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x)
    -> target (TKS2 sh1 (TKR2 m x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKS2 sh1 (TKR2 m x))
forall a b. (a -> b) -> a -> b
$
    StaticShX (MapJust @Nat sh1)
-> (KnownShX (MapJust @Nat sh1) =>
    target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x)
    -> target (TKS2 sh1 (TKR2 m x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKS2 sh1 (TKR2 m x))
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS ShS sh1
sh1)) ((KnownShX (MapJust @Nat sh1) =>
  target
    (TKX2
       ((++)
          @(Maybe Nat)
          (MapJust @Nat sh1)
          (Replicate @(Maybe Nat) m ('Nothing @Nat)))
       x)
  -> target (TKS2 sh1 (TKR2 m x)))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x)
 -> target (TKS2 sh1 (TKR2 m x)))
-> (KnownShX (MapJust @Nat sh1) =>
    target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x)
    -> target (TKS2 sh1 (TKR2 m x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKS2 sh1 (TKR2 m x))
forall a b. (a -> b) -> a -> b
$
    target (TKX2 (MapJust @Nat sh1) (TKR2 m x))
-> target (TKS2 sh1 (TKR2 m x))
forall (sh :: [Nat]) (sh' :: [Maybe Nat]) (x :: TK).
(KnownShS sh,
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKX2 sh' x) -> target (TKS2 sh x)
forall (target :: Target) (sh :: [Nat]) (sh' :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh,
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKX2 sh' x) -> target (TKS2 sh x)
sfromX (target (TKX2 (MapJust @Nat sh1) (TKR2 m x))
 -> target (TKS2 sh1 (TKR2 m x)))
-> (target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x)
    -> target (TKX2 (MapJust @Nat sh1) (TKR2 m x)))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKS2 sh1 (TKR2 m x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StaticShX (MapJust @Nat sh1)
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKX2 (MapJust @Nat sh1) (TKR2 m x))
forall (sh1 :: [Maybe Nat]) (m :: Nat) (x :: TK).
(KnownNat m, KnownSTK x) =>
StaticShX sh1
-> target
     (TKX2
        ((++) @(Maybe Nat) sh1 (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKX2 sh1 (TKR2 m x))
forall (target :: Target) (sh1 :: [Maybe Nat]) (m :: Nat)
       (x :: TK).
(ConvertTensor target, KnownNat m, KnownSTK x) =>
StaticShX sh1
-> target
     (TKX2
        ((++) @(Maybe Nat) sh1 (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
-> target (TKX2 sh1 (TKR2 m x))
xnestR (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS ShS sh1
sh1))
  snest :: forall sh1 sh2 x.
           (KnownShS sh2, KnownSTK x)
        => ShS sh1 -> target (TKS2 (sh1 ++ sh2) x)
        -> target (TKS2 sh1 (TKS2 sh2 x))
  snest ShS sh1
sh1 =
    (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith (ShS sh1
-> (:~:)
     @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
forall (sh :: [Nat]).
ShS sh
-> (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh)) (Rank @Nat sh)
lemRankMapJust ShS sh1
sh1) ((((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
   ~ (Rank @Nat sh1 :: Nat)) =>
  target (TKS2 ((++) @Nat sh1 sh2) x)
  -> target (TKS2 sh1 (TKS2 sh2 x)))
 -> target (TKS2 ((++) @Nat sh1 sh2) x)
 -> target (TKS2 sh1 (TKS2 sh2 x)))
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    (:~:)
  @Nat
  (Rank
     @(Maybe Nat)
     ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)))
  (Rank @Nat ((++) @Nat sh1 sh2))
-> (((Rank
        @(Maybe Nat)
        ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) :: Nat)
     ~ (Rank @Nat ((++) @Nat sh1 sh2) :: Nat)) =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith ((:~:)
  @Nat
  (Rank
     @(Maybe Nat)
     ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)))
  (Rank @Nat ((++) @Nat sh1 sh2))
forall {k} (a :: k) (b :: k). (:~:) @k a b
unsafeCoerceRefl :: Rank (MapJust sh1 ++ MapJust sh2)
                                   :~: Rank (sh1 ++ sh2)) ((((Rank
      @(Maybe Nat)
      ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) :: Nat)
   ~ (Rank @Nat ((++) @Nat sh1 sh2) :: Nat)) =>
  target (TKS2 ((++) @Nat sh1 sh2) x)
  -> target (TKS2 sh1 (TKS2 sh2 x)))
 -> target (TKS2 ((++) @Nat sh1 sh2) x)
 -> target (TKS2 sh1 (TKS2 sh2 x)))
-> (((Rank
        @(Maybe Nat)
        ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) :: Nat)
     ~ (Rank @Nat ((++) @Nat sh1 sh2) :: Nat)) =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    ShS sh1
-> (KnownShS sh1 =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall (sh :: [Nat]) r. ShS sh -> (KnownShS sh => r) -> r
withKnownShS ShS sh1
sh1 ((KnownShS sh1 =>
  target (TKS2 ((++) @Nat sh1 sh2) x)
  -> target (TKS2 sh1 (TKS2 sh2 x)))
 -> target (TKS2 ((++) @Nat sh1 sh2) x)
 -> target (TKS2 sh1 (TKS2 sh2 x)))
-> (KnownShS sh1 =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    StaticShX (MapJust @Nat sh1)
-> (KnownShX (MapJust @Nat sh1) =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS ShS sh1
sh1)) ((KnownShX (MapJust @Nat sh1) =>
  target (TKS2 ((++) @Nat sh1 sh2) x)
  -> target (TKS2 sh1 (TKS2 sh2 x)))
 -> target (TKS2 ((++) @Nat sh1 sh2) x)
 -> target (TKS2 sh1 (TKS2 sh2 x)))
-> (KnownShX (MapJust @Nat sh1) =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    ShS ((++) @Nat sh1 sh2)
-> (KnownShS ((++) @Nat sh1 sh2) =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall (sh :: [Nat]) r. ShS sh -> (KnownShS sh => r) -> r
withKnownShS (ShS sh1
sh1 ShS sh1 -> ShS sh2 -> ShS ((++) @Nat sh1 sh2)
forall (sh :: [Nat]) (sh' :: [Nat]).
ShS sh -> ShS sh' -> ShS ((++) @Nat sh sh')
`shsAppend` forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh2) ((KnownShS ((++) @Nat sh1 sh2) =>
  target (TKS2 ((++) @Nat sh1 sh2) x)
  -> target (TKS2 sh1 (TKS2 sh2 x)))
 -> target (TKS2 ((++) @Nat sh1 sh2) x)
 -> target (TKS2 sh1 (TKS2 sh2 x)))
-> (KnownShS ((++) @Nat sh1 sh2) =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    StaticShX ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2))
-> (KnownShX
      ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS ShS sh1
sh1)
                  StaticShX (MapJust @Nat sh1)
-> StaticShX (MapJust @Nat sh2)
-> StaticShX
     ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2))
forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]).
StaticShX sh
-> StaticShX sh' -> StaticShX ((++) @(Maybe Nat) sh sh')
`ssxAppend` ShX (MapJust @Nat sh2) Int -> StaticShX (MapJust @Nat sh2)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh2 -> ShX (MapJust @Nat sh2) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh2))) ((KnownShX
    ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) =>
  target (TKS2 ((++) @Nat sh1 sh2) x)
  -> target (TKS2 sh1 (TKS2 sh2 x)))
 -> target (TKS2 ((++) @Nat sh1 sh2) x)
 -> target (TKS2 sh1 (TKS2 sh2 x)))
-> (KnownShX
      ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) =>
    target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKS2 sh1 (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    target (TKX2 (MapJust @Nat sh1) (TKS2 sh2 x))
-> target (TKS2 sh1 (TKS2 sh2 x))
forall (sh :: [Nat]) (sh' :: [Maybe Nat]) (x :: TK).
(KnownShS sh,
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKX2 sh' x) -> target (TKS2 sh x)
forall (target :: Target) (sh :: [Nat]) (sh' :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh,
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKX2 sh' x) -> target (TKS2 sh x)
sfromX (target (TKX2 (MapJust @Nat sh1) (TKS2 sh2 x))
 -> target (TKS2 sh1 (TKS2 sh2 x)))
-> (target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target (TKX2 (MapJust @Nat sh1) (TKS2 sh2 x)))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKS2 sh1 (TKS2 sh2 x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StaticShX (MapJust @Nat sh1)
-> target
     (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) x)
-> target (TKX2 (MapJust @Nat sh1) (TKS2 sh2 x))
forall (sh1 :: [Maybe Nat]) (sh2 :: [Nat]) (x :: TK).
(KnownShS sh2, KnownSTK x) =>
StaticShX sh1
-> target (TKX2 ((++) @(Maybe Nat) sh1 (MapJust @Nat sh2)) x)
-> target (TKX2 sh1 (TKS2 sh2 x))
forall (target :: Target) (sh1 :: [Maybe Nat]) (sh2 :: [Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh2, KnownSTK x) =>
StaticShX sh1
-> target (TKX2 ((++) @(Maybe Nat) sh1 (MapJust @Nat sh2)) x)
-> target (TKX2 sh1 (TKS2 sh2 x))
xnestS (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS ShS sh1
sh1)) (target
   (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) x)
 -> target (TKX2 (MapJust @Nat sh1) (TKS2 sh2 x)))
-> (target (TKS2 ((++) @Nat sh1 sh2) x)
    -> target
         (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
-> target (TKX2 (MapJust @Nat sh1) (TKS2 sh2 x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. target (TKS2 ((++) @Nat sh1 sh2) x)
-> target
     (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) x)
forall (sh :: [Nat]) (sh' :: [Maybe Nat]) (x :: TK).
(KnownShS sh, KnownShX sh',
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKS2 sh x) -> target (TKX2 sh' x)
forall (target :: Target) (sh :: [Nat]) (sh' :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh, KnownShX sh',
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKS2 sh x) -> target (TKX2 sh' x)
xfromS
  snestX :: forall sh1 sh2 x.
            (KnownShX sh2, KnownSTK x)
         => ShS sh1 -> target (TKX2 (MapJust sh1 ++ sh2) x)
         -> target (TKS2 sh1 (TKX2 sh2 x))
  snestX ShS sh1
sh1 =
    (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
    -> target (TKS2 sh1 (TKX2 sh2 x)))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
-> target (TKS2 sh1 (TKX2 sh2 x))
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith (ShS sh1
-> (:~:)
     @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
forall (sh :: [Nat]).
ShS sh
-> (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh)) (Rank @Nat sh)
lemRankMapJust ShS sh1
sh1) ((((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
   ~ (Rank @Nat sh1 :: Nat)) =>
  target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
  -> target (TKS2 sh1 (TKX2 sh2 x)))
 -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
 -> target (TKS2 sh1 (TKX2 sh2 x)))
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
    -> target (TKS2 sh1 (TKX2 sh2 x)))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
-> target (TKS2 sh1 (TKX2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    ShS sh1
-> (KnownShS sh1 =>
    target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
    -> target (TKS2 sh1 (TKX2 sh2 x)))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
-> target (TKS2 sh1 (TKX2 sh2 x))
forall (sh :: [Nat]) r. ShS sh -> (KnownShS sh => r) -> r
withKnownShS ShS sh1
sh1 ((KnownShS sh1 =>
  target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
  -> target (TKS2 sh1 (TKX2 sh2 x)))
 -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
 -> target (TKS2 sh1 (TKX2 sh2 x)))
-> (KnownShS sh1 =>
    target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
    -> target (TKS2 sh1 (TKX2 sh2 x)))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
-> target (TKS2 sh1 (TKX2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    StaticShX (MapJust @Nat sh1)
-> (KnownShX (MapJust @Nat sh1) =>
    target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
    -> target (TKS2 sh1 (TKX2 sh2 x)))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
-> target (TKS2 sh1 (TKX2 sh2 x))
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS ShS sh1
sh1)) ((KnownShX (MapJust @Nat sh1) =>
  target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
  -> target (TKS2 sh1 (TKX2 sh2 x)))
 -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
 -> target (TKS2 sh1 (TKX2 sh2 x)))
-> (KnownShX (MapJust @Nat sh1) =>
    target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
    -> target (TKS2 sh1 (TKX2 sh2 x)))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
-> target (TKS2 sh1 (TKX2 sh2 x))
forall a b. (a -> b) -> a -> b
$
    target (TKX2 (MapJust @Nat sh1) (TKX2 sh2 x))
-> target (TKS2 sh1 (TKX2 sh2 x))
forall (sh :: [Nat]) (sh' :: [Maybe Nat]) (x :: TK).
(KnownShS sh,
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKX2 sh' x) -> target (TKS2 sh x)
forall (target :: Target) (sh :: [Nat]) (sh' :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh,
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKX2 sh' x) -> target (TKS2 sh x)
sfromX (target (TKX2 (MapJust @Nat sh1) (TKX2 sh2 x))
 -> target (TKS2 sh1 (TKX2 sh2 x)))
-> (target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
    -> target (TKX2 (MapJust @Nat sh1) (TKX2 sh2 x)))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
-> target (TKS2 sh1 (TKX2 sh2 x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StaticShX (MapJust @Nat sh1)
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
-> target (TKX2 (MapJust @Nat sh1) (TKX2 sh2 x))
forall (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat]) (x :: TK).
(KnownShX sh2, KnownSTK x) =>
StaticShX sh1
-> target (TKX2 ((++) @(Maybe Nat) sh1 sh2) x)
-> target (TKX2 sh1 (TKX2 sh2 x))
forall (target :: Target) (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShX sh2, KnownSTK x) =>
StaticShX sh1
-> target (TKX2 ((++) @(Maybe Nat) sh1 sh2) x)
-> target (TKX2 sh1 (TKX2 sh2 x))
xnest (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS ShS sh1
sh1))
  -- These three are primitives; the others are defined from them.
  xnestR :: forall sh1 m x.
            (KnownNat m, KnownSTK x)
         => StaticShX sh1 -> target (TKX2 (sh1 ++ Replicate m Nothing) x)
         -> target (TKX2 sh1 (TKR2 m x))
  xnestS :: forall sh1 sh2 x.
            (KnownShS sh2, KnownSTK x)
         => StaticShX sh1 -> target (TKX2 (sh1 ++ MapJust sh2) x)
         -> target (TKX2 sh1 (TKS2 sh2 x))
  xnest :: forall sh1 sh2 x.
           (KnownShX sh2, KnownSTK x)
        => StaticShX sh1 -> target (TKX2 (sh1 ++ sh2) x)
        -> target (TKX2 sh1 (TKX2 sh2 x))

  runNest :: (KnownNat n, KnownNat m, KnownSTK x)
          => target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x)
  runNest @n @m =
    (:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> target (TKR2 n (TKR2 m x))
-> target (TKR2 (n + m) x)
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith ((:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
forall {k} (a :: k) (b :: k). (:~:) @k a b
unsafeCoerceRefl :: Rank (Replicate n (Nothing @Nat)) :~: n) ((((Rank
      @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
   ~ (n :: Nat)) =>
  target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
 -> target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> target (TKR2 n (TKR2 m x))
-> target (TKR2 (n + m) x)
forall a b. (a -> b) -> a -> b
$
    (:~:)
  @Nat
  (Rank
     @(Maybe Nat)
     ((++)
        @(Maybe Nat)
        (Replicate @(Maybe Nat) n ('Nothing @Nat))
        (Replicate @(Maybe Nat) m ('Nothing @Nat))))
  (n + m)
-> (((Rank
        @(Maybe Nat)
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (Replicate @(Maybe Nat) m ('Nothing @Nat))) :: Nat)
     ~ (n + m :: Nat)) =>
    target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> target (TKR2 n (TKR2 m x))
-> target (TKR2 (n + m) x)
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith ((:~:)
  @Nat
  (Rank
     @(Maybe Nat)
     ((++)
        @(Maybe Nat)
        (Replicate @(Maybe Nat) n ('Nothing @Nat))
        (Replicate @(Maybe Nat) m ('Nothing @Nat))))
  (n + m)
forall {k} (a :: k) (b :: k). (:~:) @k a b
unsafeCoerceRefl :: Rank (Replicate n (Nothing @Nat)
                                          ++ Replicate m Nothing) :~: n + m) ((((Rank
      @(Maybe Nat)
      ((++)
         @(Maybe Nat)
         (Replicate @(Maybe Nat) n ('Nothing @Nat))
         (Replicate @(Maybe Nat) m ('Nothing @Nat))) :: Nat)
   ~ (n + m :: Nat)) =>
  target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
 -> target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> (((Rank
        @(Maybe Nat)
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (Replicate @(Maybe Nat) m ('Nothing @Nat))) :: Nat)
     ~ (n + m :: Nat)) =>
    target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> target (TKR2 n (TKR2 m x))
-> target (TKR2 (n + m) x)
forall a b. (a -> b) -> a -> b
$
    StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> target (TKR2 n (TKR2 m x))
-> target (TKR2 (n + m) x)
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate (forall (n :: Nat). KnownNat n => SNat n
SNat @n)) ((KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
  target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
 -> target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> target (TKR2 n (TKR2 m x))
-> target (TKR2 (n + m) x)
forall a b. (a -> b) -> a -> b
$
    StaticShX
  ((++)
     @(Maybe Nat)
     (Replicate @(Maybe Nat) n ('Nothing @Nat))
     (Replicate @(Maybe Nat) m ('Nothing @Nat)))
-> (KnownShX
      ((++)
         @(Maybe Nat)
         (Replicate @(Maybe Nat) n ('Nothing @Nat))
         (Replicate @(Maybe Nat) m ('Nothing @Nat))) =>
    target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> target (TKR2 n (TKR2 m x))
-> target (TKR2 (n + m) x)
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate (forall (n :: Nat). KnownNat n => SNat n
SNat @n) StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
-> StaticShX (Replicate @(Maybe Nat) m ('Nothing @Nat))
-> StaticShX
     ((++)
        @(Maybe Nat)
        (Replicate @(Maybe Nat) n ('Nothing @Nat))
        (Replicate @(Maybe Nat) m ('Nothing @Nat)))
forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]).
StaticShX sh
-> StaticShX sh' -> StaticShX ((++) @(Maybe Nat) sh sh')
`ssxAppend` SNat m -> StaticShX (Replicate @(Maybe Nat) m ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate (forall (n :: Nat). KnownNat n => SNat n
SNat @m)) ((KnownShX
    ((++)
       @(Maybe Nat)
       (Replicate @(Maybe Nat) n ('Nothing @Nat))
       (Replicate @(Maybe Nat) m ('Nothing @Nat))) =>
  target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
 -> target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> (KnownShX
      ((++)
         @(Maybe Nat)
         (Replicate @(Maybe Nat) n ('Nothing @Nat))
         (Replicate @(Maybe Nat) m ('Nothing @Nat))) =>
    target (TKR2 n (TKR2 m x)) -> target (TKR2 (n + m) x))
-> target (TKR2 n (TKR2 m x))
-> target (TKR2 (n + m) x)
forall a b. (a -> b) -> a -> b
$
    target
  (TKX2
     ((++)
        @(Maybe Nat)
        (Replicate @(Maybe Nat) n ('Nothing @Nat))
        (Replicate @(Maybe Nat) m ('Nothing @Nat)))
     x)
-> target (TKR2 (n + m) x)
target
  (TKX2
     ((++)
        @(Maybe Nat)
        (Replicate @(Maybe Nat) n ('Nothing @Nat))
        (Replicate @(Maybe Nat) m ('Nothing @Nat)))
     x)
-> target
     (TKR2
        (Rank
           @(Maybe Nat)
           ((++)
              @(Maybe Nat)
              (Replicate @(Maybe Nat) n ('Nothing @Nat))
              (Replicate @(Maybe Nat) m ('Nothing @Nat))))
        x)
forall (sh :: [Maybe Nat]) (x :: TK).
KnownSTK x =>
target (TKX2 sh x) -> target (TKR2 (Rank @(Maybe Nat) sh) x)
forall (target :: Target) (sh :: [Maybe Nat]) (x :: TK).
(ConvertTensor target, KnownSTK x) =>
target (TKX2 sh x) -> target (TKR2 (Rank @(Maybe Nat) sh) x)
rfromX (target
   (TKX2
      ((++)
         @(Maybe Nat)
         (Replicate @(Maybe Nat) n ('Nothing @Nat))
         (Replicate @(Maybe Nat) m ('Nothing @Nat)))
      x)
 -> target (TKR2 (n + m) x))
-> (target (TKR2 n (TKR2 m x))
    -> target
         (TKX2
            ((++)
               @(Maybe Nat)
               (Replicate @(Maybe Nat) n ('Nothing @Nat))
               (Replicate @(Maybe Nat) m ('Nothing @Nat)))
            x))
-> target (TKR2 n (TKR2 m x))
-> target (TKR2 (n + m) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. target (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKR2 m x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
forall (sh1 :: [Maybe Nat]) (m :: Nat) (x :: TK).
(KnownShX sh1, KnownNat m, KnownSTK x) =>
target (TKX2 sh1 (TKR2 m x))
-> target
     (TKX2
        ((++) @(Maybe Nat) sh1 (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
forall (target :: Target) (sh1 :: [Maybe Nat]) (m :: Nat)
       (x :: TK).
(ConvertTensor target, KnownShX sh1, KnownNat m, KnownSTK x) =>
target (TKX2 sh1 (TKR2 m x))
-> target
     (TKX2
        ((++) @(Maybe Nat) sh1 (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
xunNestR (target
   (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKR2 m x))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (Replicate @(Maybe Nat) n ('Nothing @Nat))
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x))
-> (target (TKR2 n (TKR2 m x))
    -> target
         (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKR2 m x)))
-> target (TKR2 n (TKR2 m x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (target :: Target) (sh' :: [Maybe Nat]) (x :: TK).
(ConvertTensor target, KnownShX sh', KnownSTK x) =>
target (TKR2 (Rank @(Maybe Nat) sh') x) -> target (TKX2 sh' x)
xfromR @_ @(Replicate n Nothing)
  runNestS :: (KnownNat n, KnownShS sh2, KnownSTK x)
           => target (TKR2 n (TKS2 sh2 x))
           -> target (TKX2 (Replicate n Nothing ++ MapJust sh2) x)
  runNestS @n =
    (:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target (TKR2 n (TKS2 sh2 x))
    -> target
         (TKX2
            ((++)
               @(Maybe Nat)
               (Replicate @(Maybe Nat) n ('Nothing @Nat))
               (MapJust @Nat sh2))
            x))
-> target (TKR2 n (TKS2 sh2 x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith ((:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
forall {k} (a :: k) (b :: k). (:~:) @k a b
unsafeCoerceRefl :: Rank (Replicate n (Nothing @Nat)) :~: n) ((((Rank
      @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
   ~ (n :: Nat)) =>
  target (TKR2 n (TKS2 sh2 x))
  -> target
       (TKX2
          ((++)
             @(Maybe Nat)
             (Replicate @(Maybe Nat) n ('Nothing @Nat))
             (MapJust @Nat sh2))
          x))
 -> target (TKR2 n (TKS2 sh2 x))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (Replicate @(Maybe Nat) n ('Nothing @Nat))
            (MapJust @Nat sh2))
         x))
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target (TKR2 n (TKS2 sh2 x))
    -> target
         (TKX2
            ((++)
               @(Maybe Nat)
               (Replicate @(Maybe Nat) n ('Nothing @Nat))
               (MapJust @Nat sh2))
            x))
-> target (TKR2 n (TKS2 sh2 x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
forall a b. (a -> b) -> a -> b
$
    StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target (TKR2 n (TKS2 sh2 x))
    -> target
         (TKX2
            ((++)
               @(Maybe Nat)
               (Replicate @(Maybe Nat) n ('Nothing @Nat))
               (MapJust @Nat sh2))
            x))
-> target (TKR2 n (TKS2 sh2 x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate (forall (n :: Nat). KnownNat n => SNat n
SNat @n)) ((KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
  target (TKR2 n (TKS2 sh2 x))
  -> target
       (TKX2
          ((++)
             @(Maybe Nat)
             (Replicate @(Maybe Nat) n ('Nothing @Nat))
             (MapJust @Nat sh2))
          x))
 -> target (TKR2 n (TKS2 sh2 x))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (Replicate @(Maybe Nat) n ('Nothing @Nat))
            (MapJust @Nat sh2))
         x))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target (TKR2 n (TKS2 sh2 x))
    -> target
         (TKX2
            ((++)
               @(Maybe Nat)
               (Replicate @(Maybe Nat) n ('Nothing @Nat))
               (MapJust @Nat sh2))
            x))
-> target (TKR2 n (TKS2 sh2 x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
forall a b. (a -> b) -> a -> b
$
    target
  (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKS2 sh2 x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
forall (sh1 :: [Maybe Nat]) (sh2 :: [Nat]) (x :: TK).
(KnownShX sh1, KnownShS sh2, KnownSTK x) =>
target (TKX2 sh1 (TKS2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) sh1 (MapJust @Nat sh2)) x)
forall (target :: Target) (sh1 :: [Maybe Nat]) (sh2 :: [Nat])
       (x :: TK).
(ConvertTensor target, KnownShX sh1, KnownShS sh2, KnownSTK x) =>
target (TKX2 sh1 (TKS2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) sh1 (MapJust @Nat sh2)) x)
xunNestS (target
   (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKS2 sh2 x))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (Replicate @(Maybe Nat) n ('Nothing @Nat))
            (MapJust @Nat sh2))
         x))
-> (target (TKR2 n (TKS2 sh2 x))
    -> target
         (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKS2 sh2 x)))
-> target (TKR2 n (TKS2 sh2 x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (Replicate @(Maybe Nat) n ('Nothing @Nat))
           (MapJust @Nat sh2))
        x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (target :: Target) (sh' :: [Maybe Nat]) (x :: TK).
(ConvertTensor target, KnownShX sh', KnownSTK x) =>
target (TKR2 (Rank @(Maybe Nat) sh') x) -> target (TKX2 sh' x)
xfromR @_ @(Replicate n Nothing)
  runNestX :: (KnownNat n, KnownShX sh2, KnownSTK x)
           => target (TKR2 n (TKX2 sh2 x))
           -> target (TKX2 (Replicate n Nothing ++ sh2) x)
  runNestX @n @sh2=
    (:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target (TKR2 n (TKX2 sh2 x))
    -> target
         (TKX2
            ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
            x))
-> target (TKR2 n (TKX2 sh2 x))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith ((:~:)
  @Nat
  (Rank @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)))
  n
forall {k} (a :: k) (b :: k). (:~:) @k a b
unsafeCoerceRefl :: Rank (Replicate n (Nothing @Nat)) :~: n) ((((Rank
      @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
   ~ (n :: Nat)) =>
  target (TKR2 n (TKX2 sh2 x))
  -> target
       (TKX2
          ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
          x))
 -> target (TKR2 n (TKX2 sh2 x))
 -> target
      (TKX2
         ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
         x))
-> (((Rank
        @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) :: Nat)
     ~ (n :: Nat)) =>
    target (TKR2 n (TKX2 sh2 x))
    -> target
         (TKX2
            ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
            x))
-> target (TKR2 n (TKX2 sh2 x))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
forall a b. (a -> b) -> a -> b
$
    StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target (TKR2 n (TKX2 sh2 x))
    -> target
         (TKX2
            ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
            x))
-> target (TKR2 n (TKX2 sh2 x))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate (forall (n :: Nat). KnownNat n => SNat n
SNat @n)) ((KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
  target (TKR2 n (TKX2 sh2 x))
  -> target
       (TKX2
          ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
          x))
 -> target (TKR2 n (TKX2 sh2 x))
 -> target
      (TKX2
         ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
         x))
-> (KnownShX (Replicate @(Maybe Nat) n ('Nothing @Nat)) =>
    target (TKR2 n (TKX2 sh2 x))
    -> target
         (TKX2
            ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
            x))
-> target (TKR2 n (TKX2 sh2 x))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
forall a b. (a -> b) -> a -> b
$
    StaticShX
  ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
-> (KnownShX
      ((++)
         @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2) =>
    target (TKR2 n (TKX2 sh2 x))
    -> target
         (TKX2
            ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
            x))
-> target (TKR2 n (TKX2 sh2 x))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
forall (n :: Nat).
SNat n -> StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
ssxReplicate (forall (n :: Nat). KnownNat n => SNat n
SNat @n) StaticShX (Replicate @(Maybe Nat) n ('Nothing @Nat))
-> StaticShX sh2
-> StaticShX
     ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]).
StaticShX sh
-> StaticShX sh' -> StaticShX ((++) @(Maybe Nat) sh sh')
`ssxAppend` forall (sh :: [Maybe Nat]). KnownShX sh => StaticShX sh
knownShX @sh2) ((KnownShX
    ((++)
       @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2) =>
  target (TKR2 n (TKX2 sh2 x))
  -> target
       (TKX2
          ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
          x))
 -> target (TKR2 n (TKX2 sh2 x))
 -> target
      (TKX2
         ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
         x))
-> (KnownShX
      ((++)
         @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2) =>
    target (TKR2 n (TKX2 sh2 x))
    -> target
         (TKX2
            ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
            x))
-> target (TKR2 n (TKX2 sh2 x))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
forall a b. (a -> b) -> a -> b
$
    target
  (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKX2 sh2 x))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
forall (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat]) (x :: TK).
(KnownShX sh1, KnownShX sh2, KnownSTK x) =>
target (TKX2 sh1 (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) sh1 sh2) x)
forall (target :: Target) (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShX sh1, KnownShX sh2, KnownSTK x) =>
target (TKX2 sh1 (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) sh1 sh2) x)
xunNest (target
   (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKX2 sh2 x))
 -> target
      (TKX2
         ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
         x))
-> (target (TKR2 n (TKX2 sh2 x))
    -> target
         (TKX2 (Replicate @(Maybe Nat) n ('Nothing @Nat)) (TKX2 sh2 x)))
-> target (TKR2 n (TKX2 sh2 x))
-> target
     (TKX2
        ((++) @(Maybe Nat) (Replicate @(Maybe Nat) n ('Nothing @Nat)) sh2)
        x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (target :: Target) (sh' :: [Maybe Nat]) (x :: TK).
(ConvertTensor target, KnownShX sh', KnownSTK x) =>
target (TKR2 (Rank @(Maybe Nat) sh') x) -> target (TKX2 sh' x)
xfromR @_ @(Replicate n Nothing)
  sunNestR :: (KnownShS sh1, KnownNat m, KnownSTK x)
           => target (TKS2 sh1 (TKR2 m x))
           -> target (TKX2 (MapJust sh1 ++ Replicate m Nothing) x)
  sunNestR @sh1 =
    (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target (TKS2 sh1 (TKR2 m x))
    -> target
         (TKX2
            ((++)
               @(Maybe Nat)
               (MapJust @Nat sh1)
               (Replicate @(Maybe Nat) m ('Nothing @Nat)))
            x))
-> target (TKS2 sh1 (TKR2 m x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith (ShS sh1
-> (:~:)
     @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
forall (sh :: [Nat]).
ShS sh
-> (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh)) (Rank @Nat sh)
lemRankMapJust (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh1)) ((((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
   ~ (Rank @Nat sh1 :: Nat)) =>
  target (TKS2 sh1 (TKR2 m x))
  -> target
       (TKX2
          ((++)
             @(Maybe Nat)
             (MapJust @Nat sh1)
             (Replicate @(Maybe Nat) m ('Nothing @Nat)))
          x))
 -> target (TKS2 sh1 (TKR2 m x))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x))
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target (TKS2 sh1 (TKR2 m x))
    -> target
         (TKX2
            ((++)
               @(Maybe Nat)
               (MapJust @Nat sh1)
               (Replicate @(Maybe Nat) m ('Nothing @Nat)))
            x))
-> target (TKS2 sh1 (TKR2 m x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
forall a b. (a -> b) -> a -> b
$
    StaticShX (MapJust @Nat sh1)
-> (KnownShX (MapJust @Nat sh1) =>
    target (TKS2 sh1 (TKR2 m x))
    -> target
         (TKX2
            ((++)
               @(Maybe Nat)
               (MapJust @Nat sh1)
               (Replicate @(Maybe Nat) m ('Nothing @Nat)))
            x))
-> target (TKS2 sh1 (TKR2 m x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh1))) ((KnownShX (MapJust @Nat sh1) =>
  target (TKS2 sh1 (TKR2 m x))
  -> target
       (TKX2
          ((++)
             @(Maybe Nat)
             (MapJust @Nat sh1)
             (Replicate @(Maybe Nat) m ('Nothing @Nat)))
          x))
 -> target (TKS2 sh1 (TKR2 m x))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x))
-> (KnownShX (MapJust @Nat sh1) =>
    target (TKS2 sh1 (TKR2 m x))
    -> target
         (TKX2
            ((++)
               @(Maybe Nat)
               (MapJust @Nat sh1)
               (Replicate @(Maybe Nat) m ('Nothing @Nat)))
            x))
-> target (TKS2 sh1 (TKR2 m x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
forall a b. (a -> b) -> a -> b
$
    target (TKX2 (MapJust @Nat sh1) (TKR2 m x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
forall (sh1 :: [Maybe Nat]) (m :: Nat) (x :: TK).
(KnownShX sh1, KnownNat m, KnownSTK x) =>
target (TKX2 sh1 (TKR2 m x))
-> target
     (TKX2
        ((++) @(Maybe Nat) sh1 (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
forall (target :: Target) (sh1 :: [Maybe Nat]) (m :: Nat)
       (x :: TK).
(ConvertTensor target, KnownShX sh1, KnownNat m, KnownSTK x) =>
target (TKX2 sh1 (TKR2 m x))
-> target
     (TKX2
        ((++) @(Maybe Nat) sh1 (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
xunNestR (target (TKX2 (MapJust @Nat sh1) (TKR2 m x))
 -> target
      (TKX2
         ((++)
            @(Maybe Nat)
            (MapJust @Nat sh1)
            (Replicate @(Maybe Nat) m ('Nothing @Nat)))
         x))
-> (target (TKS2 sh1 (TKR2 m x))
    -> target (TKX2 (MapJust @Nat sh1) (TKR2 m x)))
-> target (TKS2 sh1 (TKR2 m x))
-> target
     (TKX2
        ((++)
           @(Maybe Nat)
           (MapJust @Nat sh1)
           (Replicate @(Maybe Nat) m ('Nothing @Nat)))
        x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (target :: Target) (sh :: [Nat]) (sh' :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh, KnownShX sh',
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKS2 sh x) -> target (TKX2 sh' x)
xfromS @_ @_ @(MapJust sh1)
  sunNest :: (KnownShS sh1, KnownShS sh2, KnownSTK x)
          => target (TKS2 sh1 (TKS2 sh2 x)) -> target (TKS2 (sh1 ++ sh2) x)
  sunNest @sh1 @sh2 =
    (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target (TKS2 sh1 (TKS2 sh2 x))
    -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith (ShS sh1
-> (:~:)
     @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
forall (sh :: [Nat]).
ShS sh
-> (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh)) (Rank @Nat sh)
lemRankMapJust (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh1)) ((((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
   ~ (Rank @Nat sh1 :: Nat)) =>
  target (TKS2 sh1 (TKS2 sh2 x))
  -> target (TKS2 ((++) @Nat sh1 sh2) x))
 -> target (TKS2 sh1 (TKS2 sh2 x))
 -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target (TKS2 sh1 (TKS2 sh2 x))
    -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall a b. (a -> b) -> a -> b
$
    (:~:)
  @Nat
  (Rank
     @(Maybe Nat)
     ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)))
  (Rank @Nat ((++) @Nat sh1 sh2))
-> (((Rank
        @(Maybe Nat)
        ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) :: Nat)
     ~ (Rank @Nat ((++) @Nat sh1 sh2) :: Nat)) =>
    target (TKS2 sh1 (TKS2 sh2 x))
    -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith ((:~:)
  @Nat
  (Rank
     @(Maybe Nat)
     ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)))
  (Rank @Nat ((++) @Nat sh1 sh2))
forall {k} (a :: k) (b :: k). (:~:) @k a b
unsafeCoerceRefl
               :: Rank (MapJust sh1 ++ MapJust sh2) :~: Rank (sh1 ++ sh2)) ((((Rank
      @(Maybe Nat)
      ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) :: Nat)
   ~ (Rank @Nat ((++) @Nat sh1 sh2) :: Nat)) =>
  target (TKS2 sh1 (TKS2 sh2 x))
  -> target (TKS2 ((++) @Nat sh1 sh2) x))
 -> target (TKS2 sh1 (TKS2 sh2 x))
 -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> (((Rank
        @(Maybe Nat)
        ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) :: Nat)
     ~ (Rank @Nat ((++) @Nat sh1 sh2) :: Nat)) =>
    target (TKS2 sh1 (TKS2 sh2 x))
    -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall a b. (a -> b) -> a -> b
$
    ShS ((++) @Nat sh1 sh2)
-> (KnownShS ((++) @Nat sh1 sh2) =>
    target (TKS2 sh1 (TKS2 sh2 x))
    -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall (sh :: [Nat]) r. ShS sh -> (KnownShS sh => r) -> r
withKnownShS (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh1 ShS sh1 -> ShS sh2 -> ShS ((++) @Nat sh1 sh2)
forall (sh :: [Nat]) (sh' :: [Nat]).
ShS sh -> ShS sh' -> ShS ((++) @Nat sh sh')
`shsAppend` forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh2) ((KnownShS ((++) @Nat sh1 sh2) =>
  target (TKS2 sh1 (TKS2 sh2 x))
  -> target (TKS2 ((++) @Nat sh1 sh2) x))
 -> target (TKS2 sh1 (TKS2 sh2 x))
 -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> (KnownShS ((++) @Nat sh1 sh2) =>
    target (TKS2 sh1 (TKS2 sh2 x))
    -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall a b. (a -> b) -> a -> b
$
    StaticShX (MapJust @Nat sh1)
-> (KnownShX (MapJust @Nat sh1) =>
    target (TKS2 sh1 (TKS2 sh2 x))
    -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh1))) ((KnownShX (MapJust @Nat sh1) =>
  target (TKS2 sh1 (TKS2 sh2 x))
  -> target (TKS2 ((++) @Nat sh1 sh2) x))
 -> target (TKS2 sh1 (TKS2 sh2 x))
 -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> (KnownShX (MapJust @Nat sh1) =>
    target (TKS2 sh1 (TKS2 sh2 x))
    -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall a b. (a -> b) -> a -> b
$
    StaticShX ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2))
-> (KnownShX
      ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) =>
    target (TKS2 sh1 (TKS2 sh2 x))
    -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh1))
                  StaticShX (MapJust @Nat sh1)
-> StaticShX (MapJust @Nat sh2)
-> StaticShX
     ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2))
forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]).
StaticShX sh
-> StaticShX sh' -> StaticShX ((++) @(Maybe Nat) sh sh')
`ssxAppend` ShX (MapJust @Nat sh2) Int -> StaticShX (MapJust @Nat sh2)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh2 -> ShX (MapJust @Nat sh2) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh2))) ((KnownShX
    ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) =>
  target (TKS2 sh1 (TKS2 sh2 x))
  -> target (TKS2 ((++) @Nat sh1 sh2) x))
 -> target (TKS2 sh1 (TKS2 sh2 x))
 -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> (KnownShX
      ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) =>
    target (TKS2 sh1 (TKS2 sh2 x))
    -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall a b. (a -> b) -> a -> b
$
    target
  (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) x)
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall (sh :: [Nat]) (sh' :: [Maybe Nat]) (x :: TK).
(KnownShS sh,
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKX2 sh' x) -> target (TKS2 sh x)
forall (target :: Target) (sh :: [Nat]) (sh' :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh,
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKX2 sh' x) -> target (TKS2 sh x)
sfromX (target
   (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) x)
 -> target (TKS2 ((++) @Nat sh1 sh2) x))
-> (target (TKS2 sh1 (TKS2 sh2 x))
    -> target
         (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) x))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target (TKS2 ((++) @Nat sh1 sh2) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. target (TKX2 (MapJust @Nat sh1) (TKS2 sh2 x))
-> target
     (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) x)
forall (sh1 :: [Maybe Nat]) (sh2 :: [Nat]) (x :: TK).
(KnownShX sh1, KnownShS sh2, KnownSTK x) =>
target (TKX2 sh1 (TKS2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) sh1 (MapJust @Nat sh2)) x)
forall (target :: Target) (sh1 :: [Maybe Nat]) (sh2 :: [Nat])
       (x :: TK).
(ConvertTensor target, KnownShX sh1, KnownShS sh2, KnownSTK x) =>
target (TKX2 sh1 (TKS2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) sh1 (MapJust @Nat sh2)) x)
xunNestS (target (TKX2 (MapJust @Nat sh1) (TKS2 sh2 x))
 -> target
      (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) x))
-> (target (TKS2 sh1 (TKS2 sh2 x))
    -> target (TKX2 (MapJust @Nat sh1) (TKS2 sh2 x)))
-> target (TKS2 sh1 (TKS2 sh2 x))
-> target
     (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) (MapJust @Nat sh2)) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (target :: Target) (sh :: [Nat]) (sh' :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh, KnownShX sh',
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKS2 sh x) -> target (TKX2 sh' x)
xfromS @_ @_ @(MapJust sh1)
  sunNestX :: (KnownShS sh1, KnownShX sh2, KnownSTK x)
           => target (TKS2 sh1 (TKX2 sh2 x))
           -> target (TKX2 (MapJust sh1 ++ sh2) x)
  sunNestX @sh1 @sh2 =
    (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target (TKS2 sh1 (TKX2 sh2 x))
    -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
-> target (TKS2 sh1 (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
forall {k} (a :: k) (b :: k) r.
(:~:) @k a b -> (((a :: k) ~ (b :: k)) => r) -> r
gcastWith (ShS sh1
-> (:~:)
     @Nat (Rank @(Maybe Nat) (MapJust @Nat sh1)) (Rank @Nat sh1)
forall (sh :: [Nat]).
ShS sh
-> (:~:) @Nat (Rank @(Maybe Nat) (MapJust @Nat sh)) (Rank @Nat sh)
lemRankMapJust (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh1)) ((((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
   ~ (Rank @Nat sh1 :: Nat)) =>
  target (TKS2 sh1 (TKX2 sh2 x))
  -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
 -> target (TKS2 sh1 (TKX2 sh2 x))
 -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
-> (((Rank @(Maybe Nat) (MapJust @Nat sh1) :: Nat)
     ~ (Rank @Nat sh1 :: Nat)) =>
    target (TKS2 sh1 (TKX2 sh2 x))
    -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
-> target (TKS2 sh1 (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
forall a b. (a -> b) -> a -> b
$
    StaticShX (MapJust @Nat sh1)
-> (KnownShX (MapJust @Nat sh1) =>
    target (TKS2 sh1 (TKX2 sh2 x))
    -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
-> target (TKS2 sh1 (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh1))) ((KnownShX (MapJust @Nat sh1) =>
  target (TKS2 sh1 (TKX2 sh2 x))
  -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
 -> target (TKS2 sh1 (TKX2 sh2 x))
 -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
-> (KnownShX (MapJust @Nat sh1) =>
    target (TKS2 sh1 (TKX2 sh2 x))
    -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
-> target (TKS2 sh1 (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
forall a b. (a -> b) -> a -> b
$
    StaticShX ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2)
-> (KnownShX ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) =>
    target (TKS2 sh1 (TKX2 sh2 x))
    -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
-> target (TKS2 sh1 (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
forall (sh :: [Maybe Nat]) r.
StaticShX sh -> (KnownShX sh => r) -> r
withKnownShX (ShX (MapJust @Nat sh1) Int -> StaticShX (MapJust @Nat sh1)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (ShS sh1 -> ShX (MapJust @Nat sh1) Int
forall (sh :: [Nat]). ShS sh -> IShX (MapJust @Nat sh)
shxFromShS (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh1))
                  StaticShX (MapJust @Nat sh1)
-> StaticShX sh2
-> StaticShX ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2)
forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]).
StaticShX sh
-> StaticShX sh' -> StaticShX ((++) @(Maybe Nat) sh sh')
`ssxAppend` forall (sh :: [Maybe Nat]). KnownShX sh => StaticShX sh
knownShX @sh2) ((KnownShX ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) =>
  target (TKS2 sh1 (TKX2 sh2 x))
  -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
 -> target (TKS2 sh1 (TKX2 sh2 x))
 -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
-> (KnownShX ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) =>
    target (TKS2 sh1 (TKX2 sh2 x))
    -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
-> target (TKS2 sh1 (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
forall a b. (a -> b) -> a -> b
$
    target (TKX2 (MapJust @Nat sh1) (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
forall (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat]) (x :: TK).
(KnownShX sh1, KnownShX sh2, KnownSTK x) =>
target (TKX2 sh1 (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) sh1 sh2) x)
forall (target :: Target) (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShX sh1, KnownShX sh2, KnownSTK x) =>
target (TKX2 sh1 (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) sh1 sh2) x)
xunNest (target (TKX2 (MapJust @Nat sh1) (TKX2 sh2 x))
 -> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x))
-> (target (TKS2 sh1 (TKX2 sh2 x))
    -> target (TKX2 (MapJust @Nat sh1) (TKX2 sh2 x)))
-> target (TKS2 sh1 (TKX2 sh2 x))
-> target (TKX2 ((++) @(Maybe Nat) (MapJust @Nat sh1) sh2) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (target :: Target) (sh :: [Nat]) (sh' :: [Maybe Nat])
       (x :: TK).
(ConvertTensor target, KnownShS sh, KnownShX sh',
 (Rank @Nat sh :: Nat) ~ (Rank @(Maybe Nat) sh' :: Nat),
 KnownSTK x) =>
target (TKS2 sh x) -> target (TKX2 sh' x)
xfromS @_ @_ @(MapJust sh1)
  -- These three are primitives; the others are defined from them.
  xunNestR :: (KnownShX sh1, KnownNat m, KnownSTK x)
           => target (TKX2 sh1 (TKR2 m x))
           -> target (TKX2 (sh1 ++ Replicate m Nothing) x)
  xunNestS :: (KnownShX sh1, KnownShS sh2, KnownSTK x)
           => target (TKX2 sh1 (TKS2 sh2 x))
           -> target (TKX2 (sh1 ++ MapJust sh2) x)
  xunNest :: (KnownShX sh1, KnownShX sh2, KnownSTK x)
          => target (TKX2 sh1 (TKX2 sh2 x)) -> target (TKX2 (sh1 ++ sh2) x)

  -- Two aliases to make the class sufficient for Unwind.
  -- | A clone of tpair, to make this class independent of @BaseTensor@
  -- but sufficient for "Unwind".
  tpairConv :: target x -> target z -> target (TKProduct x z)
  -- | A clone of tunpair, if @ShareTensor@ is available, or an implementation
  -- that duplicates the argument, otherwise.
  tunpairConv :: target (TKProduct x z) -> (target x, target z)