{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE ScopedTypeVariables, RankNTypes, TypeApplications #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures, TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses, AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Gpu.Vulkan.Memory.Bind (

	-- * BIND AND REBIND

	Bindable, Rebindable, BindAll(..), RebindAll(..)

	) where

import Control.Monad

import Data.TypeLevel.Tuple.Uncurry
import Data.HeteroParList qualified as HeteroParList
import Data.HeteroParList (pattern (:**))

import Gpu.Vulkan.Device.Type qualified as Device
import Gpu.Vulkan.Device.Middle qualified as Device.M
import Gpu.Vulkan.Memory.ImageBuffer

import Gpu.Vulkan.Buffer.Type qualified as Buffer
import Gpu.Vulkan.Buffer.Middle qualified as Buffer.M

import Gpu.Vulkan.Image.Type qualified as Image
import Gpu.Vulkan.Image.Middle qualified as Image.M

import Gpu.Vulkan.Memory.Type

import Gpu.Vulkan.Object qualified as VObj

import Debug

class (BindAll ibargs ibargs, Alignments ibargs) => Bindable ibargs
instance (BindAll ibargs ibargs , Alignments ibargs) => Bindable ibargs

class BindAll ibargs mibargs where
	bindAll :: Device.D sd -> HeteroParList.PL (U2 ImageBuffer) ibargs ->
		M sm mibargs -> Device.M.Size ->
		IO (HeteroParList.PL (U2 (ImageBufferBinded sm)) ibargs)

instance BindAll '[] mibargs where bindAll :: forall sd sm.
D sd
-> PL (U2 ImageBuffer) '[]
-> M sm mibargs
-> Size
-> IO (PL (U2 (ImageBufferBinded sm)) '[])
bindAll D sd
_ PL (U2 ImageBuffer) '[]
_ M sm mibargs
_ Size
_ = PL (U2 (ImageBufferBinded sm)) '[]
-> IO (PL (U2 (ImageBufferBinded sm)) '[])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PL (U2 (ImageBufferBinded sm)) '[]
forall {k} (t :: k -> *). PL t '[]
HeteroParList.Nil

instance BindAll ibargs mibargs =>
	BindAll ('(si, ('ImageArg nm fmt)) ': ibargs) mibargs where
	bindAll :: forall sd sm.
D sd
-> PL (U2 ImageBuffer) ('(si, 'ImageArg nm fmt) : ibargs)
-> M sm mibargs
-> Size
-> IO
     (PL (U2 (ImageBufferBinded sm)) ('(si, 'ImageArg nm fmt) : ibargs))
bindAll dv :: D sd
dv@(Device.D D
mdv) (U2 ii :: ImageBuffer s1 s2
ii@(Image (Image.I I
i)) :** PL (U2 ImageBuffer) ss1
ibs) M sm mibargs
m Size
ost = do
		(PL (U2 ImageBuffer) mibargs
_, M
mm) <- M sm mibargs -> IO (PL (U2 ImageBuffer) mibargs, M)
forall s (ibargs :: [(*, ImageBufferArg)]).
M s ibargs -> IO (PL (U2 ImageBuffer) ibargs, M)
readM M sm mibargs
m
		(Size
ost', Size
sz) <- D sd -> ImageBuffer s1 s2 -> Size -> IO (Size, Size)
forall sd sib (ibarg :: ImageBufferArg).
D sd -> ImageBuffer sib ibarg -> Size -> IO (Size, Size)
adjustOffsetSize D sd
dv ImageBuffer s1 s2
ii Size
ost
		Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debug (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Gpu.Vulkan.Memory.Bind.BindAll (ImageArg): (ost', sz) = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Size, Size) -> String
forall a. Show a => a -> String
show (Size
ost', Size
sz)
		D -> I -> M -> Size -> IO ()
Image.M.bindMemory D
mdv I
i M
mm Size
ost'
		(ImageBufferBinded sm si ('ImageArg nm fmt)
-> U2 (ImageBufferBinded sm) '(si, 'ImageArg nm fmt)
forall {k} {k1} (t :: k -> k1 -> *) (s1 :: k) (s2 :: k1).
t s1 s2 -> U2 t '(s1, s2)
U2 (Binded sm si nm fmt -> ImageBufferBinded sm si ('ImageArg nm fmt)
forall sm sib (nm :: Symbol) (fmt :: Format).
Binded sm sib nm fmt -> ImageBufferBinded sm sib ('ImageArg nm fmt)
ImageBinded (Binded sm si nm fmt -> ImageBufferBinded sm si ('ImageArg nm fmt))
-> Binded sm si nm fmt
-> ImageBufferBinded sm si ('ImageArg nm fmt)
forall a b. (a -> b) -> a -> b
$ I -> Binded sm si nm fmt
forall sm si (nm :: Symbol) (fmt :: Format).
I -> Binded sm si nm fmt
Image.Binded I
i) U2 (ImageBufferBinded sm) '(si, 'ImageArg nm fmt)
-> PL (U2 (ImageBufferBinded sm)) ibargs
-> PL
     (U2 (ImageBufferBinded sm)) ('(si, 'ImageArg nm fmt) : ibargs)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:**)
			(PL (U2 (ImageBufferBinded sm)) ibargs
 -> PL
      (U2 (ImageBufferBinded sm)) ('(si, 'ImageArg nm fmt) : ibargs))
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
-> IO
     (PL (U2 (ImageBufferBinded sm)) ('(si, 'ImageArg nm fmt) : ibargs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> D sd
-> PL (U2 ImageBuffer) ibargs
-> M sm mibargs
-> Size
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
forall (ibargs :: [(*, ImageBufferArg)])
       (mibargs :: [(*, ImageBufferArg)]) sd sm.
BindAll ibargs mibargs =>
D sd
-> PL (U2 ImageBuffer) ibargs
-> M sm mibargs
-> Size
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
forall sd sm.
D sd
-> PL (U2 ImageBuffer) ibargs
-> M sm mibargs
-> Size
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
bindAll D sd
dv PL (U2 ImageBuffer) ibargs
PL (U2 ImageBuffer) ss1
ibs M sm mibargs
m (Size
ost' Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
sz)

instance (VObj.SizeAlignmentList objs, BindAll ibargs mibargs) =>
	BindAll ('(sb, ('BufferArg nm objs)) ': ibargs) mibargs where
	bindAll :: forall sd sm.
D sd
-> PL (U2 ImageBuffer) ('(sb, 'BufferArg nm objs) : ibargs)
-> M sm mibargs
-> Size
-> IO
     (PL
        (U2 (ImageBufferBinded sm)) ('(sb, 'BufferArg nm objs) : ibargs))
bindAll dv :: D sd
dv@(Device.D D
mdv)
		(U2 bb :: ImageBuffer s1 s2
bb@(Buffer (Buffer.B PL Length objs
lns B
b)) :** PL (U2 ImageBuffer) ss1
ibs) M sm mibargs
m Size
ost  = do
		(PL (U2 ImageBuffer) mibargs
_, M
mm) <- M sm mibargs -> IO (PL (U2 ImageBuffer) mibargs, M)
forall s (ibargs :: [(*, ImageBufferArg)]).
M s ibargs -> IO (PL (U2 ImageBuffer) ibargs, M)
readM M sm mibargs
m
		(Size
ost', Size
sz) <- D sd -> ImageBuffer s1 s2 -> Size -> IO (Size, Size)
forall sd sib (ibarg :: ImageBufferArg).
D sd -> ImageBuffer sib ibarg -> Size -> IO (Size, Size)
adjustOffsetSize D sd
dv ImageBuffer s1 s2
bb Size
ost
		let	ost'' :: Size
ost'' = Size -> Size -> Size
adjust (forall (objs :: [O]). SizeAlignmentList objs => Size
VObj.sizeAlignmentListWholeAlignment @objs) Size
ost'
		Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debug (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Gpu.Vulkan.Memory.Bind.BindAll (BufferArg): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Size, Size) -> String
forall a. Show a => a -> String
show (Size
ost', Size
sz)
		Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debug (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Gpu.Vulkan.Memory.Bind.BindAll (BufferArg): ost'' = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Size -> String
forall a. Show a => a -> String
show Size
ost''
		D -> B -> M -> Size -> IO ()
Buffer.M.bindMemory D
mdv B
b M
mm Size
ost''
		(ImageBufferBinded sm sb ('BufferArg nm objs)
-> U2 (ImageBufferBinded sm) '(sb, 'BufferArg nm objs)
forall {k} {k1} (t :: k -> k1 -> *) (s1 :: k) (s2 :: k1).
t s1 s2 -> U2 t '(s1, s2)
U2 (Binded sm sb nm objs
-> ImageBufferBinded sm sb ('BufferArg nm objs)
forall sm sib (nm :: Symbol) (objs :: [O]).
Binded sm sib nm objs
-> ImageBufferBinded sm sib ('BufferArg nm objs)
BufferBinded (Binded sm sb nm objs
 -> ImageBufferBinded sm sb ('BufferArg nm objs))
-> Binded sm sb nm objs
-> ImageBufferBinded sm sb ('BufferArg nm objs)
forall a b. (a -> b) -> a -> b
$ PL Length objs -> B -> Binded sm sb nm objs
forall sm sb (nm :: Symbol) (objs :: [O]).
PL Length objs -> B -> Binded sm sb nm objs
Buffer.Binded PL Length objs
PL Length objs
lns B
b) U2 (ImageBufferBinded sm) '(sb, 'BufferArg nm objs)
-> PL (U2 (ImageBufferBinded sm)) ibargs
-> PL
     (U2 (ImageBufferBinded sm)) ('(sb, 'BufferArg nm objs) : ibargs)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:**)
			(PL (U2 (ImageBufferBinded sm)) ibargs
 -> PL
      (U2 (ImageBufferBinded sm)) ('(sb, 'BufferArg nm objs) : ibargs))
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
-> IO
     (PL
        (U2 (ImageBufferBinded sm)) ('(sb, 'BufferArg nm objs) : ibargs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> D sd
-> PL (U2 ImageBuffer) ibargs
-> M sm mibargs
-> Size
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
forall (ibargs :: [(*, ImageBufferArg)])
       (mibargs :: [(*, ImageBufferArg)]) sd sm.
BindAll ibargs mibargs =>
D sd
-> PL (U2 ImageBuffer) ibargs
-> M sm mibargs
-> Size
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
forall sd sm.
D sd
-> PL (U2 ImageBuffer) ibargs
-> M sm mibargs
-> Size
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
bindAll D sd
dv PL (U2 ImageBuffer) ibargs
PL (U2 ImageBuffer) ss1
ibs M sm mibargs
m (Size
ost'' Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
sz)

instance BindAll ibargs mibargs =>
	BindAll ('(sb, 'RawArg) ': ibargs) mibargs where
	bindAll :: forall sd sm.
D sd
-> PL (U2 ImageBuffer) ('(sb, 'RawArg) : ibargs)
-> M sm mibargs
-> Size
-> IO (PL (U2 (ImageBufferBinded sm)) ('(sb, 'RawArg) : ibargs))
bindAll D sd
dv (U2 bb :: ImageBuffer s1 s2
bb@(Raw Size
a Size
s) :** PL (U2 ImageBuffer) ss1
ibs) M sm mibargs
m Size
ost  = do
		(Size
ost', Size
sz) <- D sd -> ImageBuffer s1 s2 -> Size -> IO (Size, Size)
forall sd sib (ibarg :: ImageBufferArg).
D sd -> ImageBuffer sib ibarg -> Size -> IO (Size, Size)
adjustOffsetSize D sd
dv ImageBuffer s1 s2
bb Size
ost
		Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debug (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Gpu.Vulkan.Memory.Bind.BindAll (RawArg): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Size, Size) -> String
forall a. Show a => a -> String
show (Size
ost', Size
sz)
		(ImageBufferBinded sm sb 'RawArg
-> U2 (ImageBufferBinded sm) '(sb, 'RawArg)
forall {k} {k1} (t :: k -> k1 -> *) (s1 :: k) (s2 :: k1).
t s1 s2 -> U2 t '(s1, s2)
U2 (Size -> Size -> ImageBufferBinded sm sb 'RawArg
forall sm sib. Size -> Size -> ImageBufferBinded sm sib 'RawArg
RawBinded Size
a Size
s) U2 (ImageBufferBinded sm) '(sb, 'RawArg)
-> PL (U2 (ImageBufferBinded sm)) ibargs
-> PL (U2 (ImageBufferBinded sm)) ('(sb, 'RawArg) : ibargs)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:**) (PL (U2 (ImageBufferBinded sm)) ibargs
 -> PL (U2 (ImageBufferBinded sm)) ('(sb, 'RawArg) : ibargs))
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
-> IO (PL (U2 (ImageBufferBinded sm)) ('(sb, 'RawArg) : ibargs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> D sd
-> PL (U2 ImageBuffer) ibargs
-> M sm mibargs
-> Size
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
forall (ibargs :: [(*, ImageBufferArg)])
       (mibargs :: [(*, ImageBufferArg)]) sd sm.
BindAll ibargs mibargs =>
D sd
-> PL (U2 ImageBuffer) ibargs
-> M sm mibargs
-> Size
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
forall sd sm.
D sd
-> PL (U2 ImageBuffer) ibargs
-> M sm mibargs
-> Size
-> IO (PL (U2 (ImageBufferBinded sm)) ibargs)
bindAll D sd
dv PL (U2 ImageBuffer) ibargs
PL (U2 ImageBuffer) ss1
ibs M sm mibargs
m (Size
ost' Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
sz)

class (RebindAll ibargs ibargs, Alignments ibargs) => Rebindable ibargs
instance (RebindAll ibargs ibargs, Alignments ibargs) => Rebindable ibargs

class RebindAll ibargs mibargs where
	rebindAll :: Device.D sd ->
		HeteroParList.PL (U2 (ImageBufferBinded sm)) ibargs ->
		M sm mibargs -> Device.M.Size -> IO ()

instance RebindAll '[] mibargs where rebindAll :: forall sd sm.
D sd
-> PL (U2 (ImageBufferBinded sm)) '[]
-> M sm mibargs
-> Size
-> IO ()
rebindAll D sd
_ PL (U2 (ImageBufferBinded sm)) '[]
_ M sm mibargs
_ Size
_ = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance RebindAll ibargs mibargs =>
	RebindAll ('(si, 'ImageArg nm fmt) ': ibargs) mibargs where
	rebindAll :: forall sd sm.
D sd
-> PL
     (U2 (ImageBufferBinded sm)) ('(si, 'ImageArg nm fmt) : ibargs)
-> M sm mibargs
-> Size
-> IO ()
rebindAll dv :: D sd
dv@(Device.D D
mdv)
		(U2 ii :: ImageBufferBinded sm s1 s2
ii@(ImageBinded (Image.Binded I
i)) :** PL (U2 (ImageBufferBinded sm)) ss1
ibs) M sm mibargs
m Size
ost = do
		(PL (U2 ImageBuffer) mibargs
_, M
mm) <- M sm mibargs -> IO (PL (U2 ImageBuffer) mibargs, M)
forall s (ibargs :: [(*, ImageBufferArg)]).
M s ibargs -> IO (PL (U2 ImageBuffer) ibargs, M)
readM M sm mibargs
m
		(Size
ost', Size
sz) <- D sd -> ImageBufferBinded sm s1 s2 -> Size -> IO (Size, Size)
forall sd sm sib (ibarg :: ImageBufferArg).
D sd -> ImageBufferBinded sm sib ibarg -> Size -> IO (Size, Size)
adjustOffsetSizeBinded D sd
dv ImageBufferBinded sm s1 s2
ii Size
ost
		D -> I -> M -> Size -> IO ()
Image.M.bindMemory D
mdv I
i M
mm Size
ost'
		D sd
-> PL (U2 (ImageBufferBinded sm)) ss1
-> M sm mibargs
-> Size
-> IO ()
forall (ibargs :: [(*, ImageBufferArg)])
       (mibargs :: [(*, ImageBufferArg)]) sd sm.
RebindAll ibargs mibargs =>
D sd
-> PL (U2 (ImageBufferBinded sm)) ibargs
-> M sm mibargs
-> Size
-> IO ()
forall sd sm.
D sd
-> PL (U2 (ImageBufferBinded sm)) ss1
-> M sm mibargs
-> Size
-> IO ()
rebindAll D sd
dv PL (U2 (ImageBufferBinded sm)) ss1
ibs M sm mibargs
m (Size -> IO ()) -> Size -> IO ()
forall a b. (a -> b) -> a -> b
$ Size
ost' Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
sz

instance RebindAll ibargs mibargs =>
	RebindAll ('(sb, 'BufferArg nm objs) ': ibargs) mibargs where
	rebindAll :: forall sd sm.
D sd
-> PL
     (U2 (ImageBufferBinded sm)) ('(sb, 'BufferArg nm objs) : ibargs)
-> M sm mibargs
-> Size
-> IO ()
rebindAll dv :: D sd
dv@(Device.D D
mdv)
		(U2 bb :: ImageBufferBinded sm s1 s2
bb@(BufferBinded (Buffer.Binded PL Length objs
_lns B
b)) :** PL (U2 (ImageBufferBinded sm)) ss1
ibs) M sm mibargs
m Size
ost = do
		(PL (U2 ImageBuffer) mibargs
_, M
mm) <- M sm mibargs -> IO (PL (U2 ImageBuffer) mibargs, M)
forall s (ibargs :: [(*, ImageBufferArg)]).
M s ibargs -> IO (PL (U2 ImageBuffer) ibargs, M)
readM M sm mibargs
m
		(Size
ost', Size
sz) <- D sd -> ImageBufferBinded sm s1 s2 -> Size -> IO (Size, Size)
forall sd sm sib (ibarg :: ImageBufferArg).
D sd -> ImageBufferBinded sm sib ibarg -> Size -> IO (Size, Size)
adjustOffsetSizeBinded D sd
dv ImageBufferBinded sm s1 s2
bb Size
ost
		D -> B -> M -> Size -> IO ()
Buffer.M.bindMemory D
mdv B
b M
mm Size
ost'
		D sd
-> PL (U2 (ImageBufferBinded sm)) ss1
-> M sm mibargs
-> Size
-> IO ()
forall (ibargs :: [(*, ImageBufferArg)])
       (mibargs :: [(*, ImageBufferArg)]) sd sm.
RebindAll ibargs mibargs =>
D sd
-> PL (U2 (ImageBufferBinded sm)) ibargs
-> M sm mibargs
-> Size
-> IO ()
forall sd sm.
D sd
-> PL (U2 (ImageBufferBinded sm)) ss1
-> M sm mibargs
-> Size
-> IO ()
rebindAll D sd
dv PL (U2 (ImageBufferBinded sm)) ss1
ibs M sm mibargs
m (Size -> IO ()) -> Size -> IO ()
forall a b. (a -> b) -> a -> b
$ Size
ost' Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
sz

instance RebindAll ibargs mibargs =>
	RebindAll ('(sb, 'RawArg) ': ibargs) mibargs where
	rebindAll :: forall sd sm.
D sd
-> PL (U2 (ImageBufferBinded sm)) ('(sb, 'RawArg) : ibargs)
-> M sm mibargs
-> Size
-> IO ()
rebindAll D sd
dv (U2 ImageBufferBinded sm s1 s2
bb :** PL (U2 (ImageBufferBinded sm)) ss1
ibs) M sm mibargs
m Size
ost = do
		(Size
ost', Size
sz) <- D sd -> ImageBufferBinded sm s1 s2 -> Size -> IO (Size, Size)
forall sd sm sib (ibarg :: ImageBufferArg).
D sd -> ImageBufferBinded sm sib ibarg -> Size -> IO (Size, Size)
adjustOffsetSizeBinded D sd
dv ImageBufferBinded sm s1 s2
bb Size
ost
		D sd
-> PL (U2 (ImageBufferBinded sm)) ss1
-> M sm mibargs
-> Size
-> IO ()
forall (ibargs :: [(*, ImageBufferArg)])
       (mibargs :: [(*, ImageBufferArg)]) sd sm.
RebindAll ibargs mibargs =>
D sd
-> PL (U2 (ImageBufferBinded sm)) ibargs
-> M sm mibargs
-> Size
-> IO ()
forall sd sm.
D sd
-> PL (U2 (ImageBufferBinded sm)) ss1
-> M sm mibargs
-> Size
-> IO ()
rebindAll D sd
dv PL (U2 (ImageBufferBinded sm)) ss1
ibs M sm mibargs
m (Size -> IO ()) -> Size -> IO ()
forall a b. (a -> b) -> a -> b
$ Size
ost' Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
sz