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

module Gpu.Vulkan.DescriptorSetLayout.UpdateDynamicLengths (

	-- * UPDATE DYNAMIC LENGTHS

	UpdateDynamicLength(..) ) where

import Gpu.Vulkan.Object qualified as VObj
import Gpu.Vulkan.Object.Base qualified as KObj
import Data.HeteroParList qualified as HeteroParList
import Data.HeteroParList (pattern (:**))

import qualified Gpu.Vulkan.DescriptorSetLayout.Type as Layout

class VObj.OnlyDynamicLengths objs => UpdateDynamicLength bts objs where
	updateDynamicLength ::
		HeteroParList.PL
			(HeteroParList.PL KObj.Length)
			(Layout.BindingTypeListBufferOnlyDynamics bts) ->
		HeteroParList.PL KObj.Length
			(VObj.OnlyDynamics objs) ->
		HeteroParList.PL
			(HeteroParList.PL KObj.Length)
			(Layout.BindingTypeListBufferOnlyDynamics bts)

instance UpdateDynamicLength _bts '[] where updateDynamicLength :: PL (PL Length) (BindingTypeListBufferOnlyDynamics _bts)
-> PL Length (OnlyDynamics '[])
-> PL (PL Length) (BindingTypeListBufferOnlyDynamics _bts)
updateDynamicLength PL (PL Length) (BindingTypeListBufferOnlyDynamics _bts)
x PL Length (OnlyDynamics '[])
_ = PL (PL Length) (BindingTypeListBufferOnlyDynamics _bts)
x

instance UpdateDynamicLength bts (o ': os) =>
	UpdateDynamicLength ('Layout.Buffer '[] ': bts) (o ': os) where
	updateDynamicLength :: PL
  (PL Length) (BindingTypeListBufferOnlyDynamics ('Buffer '[] : bts))
-> PL Length (OnlyDynamics (o : os))
-> PL
     (PL Length) (BindingTypeListBufferOnlyDynamics ('Buffer '[] : bts))
updateDynamicLength (PL Length s
HeteroParList.Nil :** PL (PL Length) ss1
lnss) PL Length (OnlyDynamics (o : os))
lns =
		PL Length '[]
forall {k} (t :: k -> *). PL t '[]
HeteroParList.Nil PL Length '[] -> PL (PL Length) ss1 -> PL (PL Length) ('[] : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** forall (bts :: [BindingType]) (objs :: [O]).
UpdateDynamicLength bts objs =>
PL (PL Length) (BindingTypeListBufferOnlyDynamics bts)
-> PL Length (OnlyDynamics objs)
-> PL (PL Length) (BindingTypeListBufferOnlyDynamics bts)
updateDynamicLength @bts @(o ': os) PL (PL Length) ss1
PL (PL Length) (BindingTypeListBufferOnlyDynamics bts)
lnss PL Length (OnlyDynamics (o : os))
lns

instance (UpdateDynamicLengthPrefix os os', VObj.OnlyDynamicLengths os) =>
	UpdateDynamicLength
		('Layout.Buffer (VObj.Static algn 'Nothing ot t ': os') ': bts)
		(VObj.Static algn ('Just _nm) ot t ': os) where
	updateDynamicLength :: PL
  (PL Length)
  (BindingTypeListBufferOnlyDynamics
     ('Buffer (Static algn 'Nothing ot t : os') : bts))
-> PL Length (OnlyDynamics (Static algn ('Just _nm) ot t : os))
-> PL
     (PL Length)
     (BindingTypeListBufferOnlyDynamics
        ('Buffer (Static algn 'Nothing ot t : os') : bts))
updateDynamicLength (PL Length s
lns' :** PL (PL Length) ss1
lnss) PL Length (OnlyDynamics (Static algn ('Just _nm) ot t : os))
lns =
		forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length s
PL Length (OnlyDynamics os')
lns' PL Length (OnlyDynamics os)
PL Length (OnlyDynamics (Static algn ('Just _nm) ot t : os))
lns PL Length s -> PL (PL Length) ss1 -> PL (PL Length) (s : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (PL Length) ss1
lnss

instance (UpdateDynamicLengthPrefix os os', VObj.OnlyDynamicLengths os) =>
	UpdateDynamicLength
		('Layout.Buffer (VObj.Static algn ('Just _nm) ot t ': os') ': bts)
		(VObj.Static algn 'Nothing ot t ': os) where
	updateDynamicLength :: PL
  (PL Length)
  (BindingTypeListBufferOnlyDynamics
     ('Buffer (Static algn ('Just _nm) ot t : os') : bts))
-> PL Length (OnlyDynamics (Static algn 'Nothing ot t : os))
-> PL
     (PL Length)
     (BindingTypeListBufferOnlyDynamics
        ('Buffer (Static algn ('Just _nm) ot t : os') : bts))
updateDynamicLength (PL Length s
lns' :** PL (PL Length) ss1
lnss) PL Length (OnlyDynamics (Static algn 'Nothing ot t : os))
lns =
		forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length s
PL Length (OnlyDynamics os')
lns' PL Length (OnlyDynamics os)
PL Length (OnlyDynamics (Static algn 'Nothing ot t : os))
lns PL Length s -> PL (PL Length) ss1 -> PL (PL Length) (s : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (PL Length) ss1
lnss

instance (UpdateDynamicLengthPrefix os os', VObj.OnlyDynamicLengths os) =>
	UpdateDynamicLength
		('Layout.Buffer (VObj.Dynamic n algn 'Nothing ot t ': os') ': bts)
		(VObj.Dynamic n algn ('Just _nm) ot t ': os) where
	updateDynamicLength :: PL
  (PL Length)
  (BindingTypeListBufferOnlyDynamics
     ('Buffer (Dynamic n algn 'Nothing ot t : os') : bts))
-> PL Length (OnlyDynamics (Dynamic n algn ('Just _nm) ot t : os))
-> PL
     (PL Length)
     (BindingTypeListBufferOnlyDynamics
        ('Buffer (Dynamic n algn 'Nothing ot t : os') : bts))
updateDynamicLength ((Length s
_ln :** PL Length ss1
lns') :** PL (PL Length) ss1
lnss) (Length s
ln :** PL Length ss1
lns) =
		(Length ('O algn ('Just _nm) ot t) -> Length ('O algn 'Nothing ot t)
forall (algn :: Alignment) (mnm :: Maybe Symbol) (ot :: ObjectType)
       t (mnm' :: Maybe Symbol).
Length ('O algn mnm ot t) -> Length ('O algn mnm' ot t)
KObj.renameLength Length s
Length ('O algn ('Just _nm) ot t)
ln Length ('O algn 'Nothing ot t)
-> PL Length ss1 -> PL Length ('O algn 'Nothing ot t : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length ss1
PL Length (OnlyDynamics os')
lns' PL Length ss1
PL Length (OnlyDynamics os)
lns) PL Length ('O algn 'Nothing ot t : ss1)
-> PL (PL Length) ss1
-> PL (PL Length) (('O algn 'Nothing ot t : ss1) : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (PL Length) ss1
lnss

instance (UpdateDynamicLengthPrefix os os', VObj.OnlyDynamicLengths os) =>
	UpdateDynamicLength
		('Layout.Buffer (VObj.Dynamic n algn ('Just _nm) ot t ': os') ': bts)
		(VObj.Dynamic n algn 'Nothing ot t ': os) where
	updateDynamicLength :: PL
  (PL Length)
  (BindingTypeListBufferOnlyDynamics
     ('Buffer (Dynamic n algn ('Just _nm) ot t : os') : bts))
-> PL Length (OnlyDynamics (Dynamic n algn 'Nothing ot t : os))
-> PL
     (PL Length)
     (BindingTypeListBufferOnlyDynamics
        ('Buffer (Dynamic n algn ('Just _nm) ot t : os') : bts))
updateDynamicLength ((Length s
_ln :** PL Length ss1
lns') :** PL (PL Length) ss1
lnss) (Length s
ln :** PL Length ss1
lns) =
		(Length ('O algn 'Nothing ot t) -> Length ('O algn ('Just _nm) ot t)
forall (algn :: Alignment) (mnm :: Maybe Symbol) (ot :: ObjectType)
       t (mnm' :: Maybe Symbol).
Length ('O algn mnm ot t) -> Length ('O algn mnm' ot t)
KObj.renameLength Length s
Length ('O algn 'Nothing ot t)
ln Length ('O algn ('Just _nm) ot t)
-> PL Length ss1 -> PL Length ('O algn ('Just _nm) ot t : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length ss1
PL Length (OnlyDynamics os')
lns' PL Length ss1
PL Length (OnlyDynamics os)
lns) PL Length ('O algn ('Just _nm) ot t : ss1)
-> PL (PL Length) ss1
-> PL (PL Length) (('O algn ('Just _nm) ot t : ss1) : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (PL Length) ss1
lnss

instance (UpdateDynamicLengthPrefix os os', VObj.OnlyDynamicLengths os) =>
	UpdateDynamicLength
		('Layout.Buffer (VObj.Static_ o ': os') ': bts)
		(VObj.Static_ o ': os) where
	updateDynamicLength :: PL
  (PL Length)
  (BindingTypeListBufferOnlyDynamics
     ('Buffer ('Static_ o : os') : bts))
-> PL Length (OnlyDynamics ('Static_ o : os))
-> PL
     (PL Length)
     (BindingTypeListBufferOnlyDynamics
        ('Buffer ('Static_ o : os') : bts))
updateDynamicLength (PL Length s
lns' :** PL (PL Length) ss1
lnss) PL Length (OnlyDynamics ('Static_ o : os))
lns =
		forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length s
PL Length (OnlyDynamics os')
lns' PL Length (OnlyDynamics os)
PL Length (OnlyDynamics ('Static_ o : os))
lns PL Length s -> PL (PL Length) ss1 -> PL (PL Length) (s : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (PL Length) ss1
lnss

instance (UpdateDynamicLengthPrefix os os', VObj.OnlyDynamicLengths os) =>
	UpdateDynamicLength
		('Layout.Buffer ('VObj.Dynamic n o ': os') ': bts)
		('VObj.Dynamic n o ': os) where
	updateDynamicLength :: PL
  (PL Length)
  (BindingTypeListBufferOnlyDynamics
     ('Buffer ('Dynamic n o : os') : bts))
-> PL Length (OnlyDynamics ('Dynamic n o : os))
-> PL
     (PL Length)
     (BindingTypeListBufferOnlyDynamics
        ('Buffer ('Dynamic n o : os') : bts))
updateDynamicLength ((Length s
_ln :** PL Length ss1
lns') :** PL (PL Length) ss1
lnss) (Length s
ln :** PL Length ss1
lns) =
		(Length s
ln Length s -> PL Length ss1 -> PL Length (s : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length ss1
PL Length (OnlyDynamics os')
lns' PL Length ss1
PL Length (OnlyDynamics os)
lns) PL Length (s : ss1)
-> PL (PL Length) ss1 -> PL (PL Length) ((s : ss1) : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (PL Length) ss1
lnss

instance {-# OVERLAPPABLE #-}
	UpdateDynamicLength
		('Layout.Buffer os' ': bts) (oo ': os) =>
	UpdateDynamicLength
		('Layout.Buffer (VObj.Static_ o ': os') ': bts) (oo ': os) where
	updateDynamicLength :: PL
  (PL Length)
  (BindingTypeListBufferOnlyDynamics
     ('Buffer ('Static_ o : os') : bts))
-> PL Length (OnlyDynamics (oo : os))
-> PL
     (PL Length)
     (BindingTypeListBufferOnlyDynamics
        ('Buffer ('Static_ o : os') : bts))
updateDynamicLength PL
  (PL Length)
  (BindingTypeListBufferOnlyDynamics
     ('Buffer ('Static_ o : os') : bts))
lnss PL Length (OnlyDynamics (oo : os))
lns =
		forall (bts :: [BindingType]) (objs :: [O]).
UpdateDynamicLength bts objs =>
PL (PL Length) (BindingTypeListBufferOnlyDynamics bts)
-> PL Length (OnlyDynamics objs)
-> PL (PL Length) (BindingTypeListBufferOnlyDynamics bts)
updateDynamicLength
			@('Layout.Buffer os' ': bts) @(oo ': os) PL
  (PL Length) (BindingTypeListBufferOnlyDynamics ('Buffer os' : bts))
PL
  (PL Length)
  (BindingTypeListBufferOnlyDynamics
     ('Buffer ('Static_ o : os') : bts))
lnss PL Length (OnlyDynamics (oo : os))
lns

instance {-# OVERLAPPABLE #-}
	UpdateDynamicLength
		('Layout.Buffer os' ': bts) (oo ': os) =>
	UpdateDynamicLength
		('Layout.Buffer ('VObj.Dynamic n o ': os') ': bts) (oo ': os) where
	updateDynamicLength :: PL
  (PL Length)
  (BindingTypeListBufferOnlyDynamics
     ('Buffer ('Dynamic n o : os') : bts))
-> PL Length (OnlyDynamics (oo : os))
-> PL
     (PL Length)
     (BindingTypeListBufferOnlyDynamics
        ('Buffer ('Dynamic n o : os') : bts))
updateDynamicLength ((Length s
ln :** PL Length ss1
lns') :** PL (PL Length) ss1
lnss) PL Length (OnlyDynamics (oo : os))
lns = let
		PL Length ss1
PL Length s
ls' :** PL (PL Length) ss1
PL (PL Length) ss1
lss = forall (bts :: [BindingType]) (objs :: [O]).
UpdateDynamicLength bts objs =>
PL (PL Length) (BindingTypeListBufferOnlyDynamics bts)
-> PL Length (OnlyDynamics objs)
-> PL (PL Length) (BindingTypeListBufferOnlyDynamics bts)
updateDynamicLength
			@('Layout.Buffer os' ': bts) @(oo ': os) (PL Length ss1
lns' PL Length ss1 -> PL (PL Length) ss1 -> PL (PL Length) (ss1 : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (PL Length) ss1
lnss) PL Length (OnlyDynamics (oo : os))
lns in
		(Length s
ln Length s -> PL Length ss1 -> PL Length (s : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL Length ss1
ls') PL Length (s : ss1)
-> PL (PL Length) ss1 -> PL (PL Length) ((s : ss1) : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (PL Length) ss1
lss

class UpdateDynamicLengthPrefix (objs :: [VObj.O]) (objs' :: [VObj.O]) where
	updateDynamicLengthPrefix ::
		HeteroParList.PL KObj.Length (VObj.OnlyDynamics objs') ->
		HeteroParList.PL KObj.Length (VObj.OnlyDynamics objs) ->
		HeteroParList.PL KObj.Length (VObj.OnlyDynamics objs')

instance UpdateDynamicLengthPrefix '[] objs where
	updateDynamicLengthPrefix :: PL Length (OnlyDynamics objs)
-> PL Length (OnlyDynamics '[]) -> PL Length (OnlyDynamics objs)
updateDynamicLengthPrefix PL Length (OnlyDynamics objs)
lns PL Length (OnlyDynamics '[])
_ = PL Length (OnlyDynamics objs)
lns

instance UpdateDynamicLengthPrefix os os' =>
	UpdateDynamicLengthPrefix
		(VObj.Static algn 'Nothing ot t ': os)
		(VObj.Static algn ('Just _nm) ot t ': os') where
	updateDynamicLengthPrefix :: PL Length (OnlyDynamics (Static algn ('Just _nm) ot t : os'))
-> PL Length (OnlyDynamics (Static algn 'Nothing ot t : os))
-> PL Length (OnlyDynamics (Static algn ('Just _nm) ot t : os'))
updateDynamicLengthPrefix PL Length (OnlyDynamics (Static algn ('Just _nm) ot t : os'))
lns' PL Length (OnlyDynamics (Static algn 'Nothing ot t : os))
lns  =
		forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length (OnlyDynamics os')
PL Length (OnlyDynamics (Static algn ('Just _nm) ot t : os'))
lns' PL Length (OnlyDynamics os)
PL Length (OnlyDynamics (Static algn 'Nothing ot t : os))
lns

instance UpdateDynamicLengthPrefix os os' =>
	UpdateDynamicLengthPrefix
		(VObj.Static algn ('Just _nm) ot t ': os)
		(VObj.Static algn 'Nothing ot t ': os') where
	updateDynamicLengthPrefix :: PL Length (OnlyDynamics (Static algn 'Nothing ot t : os'))
-> PL Length (OnlyDynamics (Static algn ('Just _nm) ot t : os))
-> PL Length (OnlyDynamics (Static algn 'Nothing ot t : os'))
updateDynamicLengthPrefix PL Length (OnlyDynamics (Static algn 'Nothing ot t : os'))
lns' PL Length (OnlyDynamics (Static algn ('Just _nm) ot t : os))
lns  =
		forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length (OnlyDynamics os')
PL Length (OnlyDynamics (Static algn 'Nothing ot t : os'))
lns' PL Length (OnlyDynamics os)
PL Length (OnlyDynamics (Static algn ('Just _nm) ot t : os))
lns

instance UpdateDynamicLengthPrefix os os' =>
	UpdateDynamicLengthPrefix
		(VObj.Dynamic n algn 'Nothing ot t ': os)
		(VObj.Dynamic n algn ('Just _nm) ot t ': os') where
	updateDynamicLengthPrefix :: PL Length (OnlyDynamics (Dynamic n algn ('Just _nm) ot t : os'))
-> PL Length (OnlyDynamics (Dynamic n algn 'Nothing ot t : os))
-> PL Length (OnlyDynamics (Dynamic n algn ('Just _nm) ot t : os'))
updateDynamicLengthPrefix (Length s
_ln :** PL Length ss1
lns') (Length s
ln :** PL Length ss1
lns)  =
		Length ('O algn 'Nothing ot t) -> Length ('O algn ('Just _nm) ot t)
forall (algn :: Alignment) (mnm :: Maybe Symbol) (ot :: ObjectType)
       t (mnm' :: Maybe Symbol).
Length ('O algn mnm ot t) -> Length ('O algn mnm' ot t)
KObj.renameLength Length s
Length ('O algn 'Nothing ot t)
ln Length ('O algn ('Just _nm) ot t)
-> PL Length ss1 -> PL Length ('O algn ('Just _nm) ot t : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length ss1
PL Length (OnlyDynamics os')
lns' PL Length ss1
PL Length (OnlyDynamics os)
lns

instance UpdateDynamicLengthPrefix os os' =>
	UpdateDynamicLengthPrefix
		(VObj.Dynamic n algn ('Just _nm) ot t ': os)
		(VObj.Dynamic n algn 'Nothing ot t ': os') where
	updateDynamicLengthPrefix :: PL Length (OnlyDynamics (Dynamic n algn 'Nothing ot t : os'))
-> PL Length (OnlyDynamics (Dynamic n algn ('Just _nm) ot t : os))
-> PL Length (OnlyDynamics (Dynamic n algn 'Nothing ot t : os'))
updateDynamicLengthPrefix (Length s
_ln :** PL Length ss1
lns') (Length s
ln :** PL Length ss1
lns)  =
		Length ('O algn ('Just _nm) ot t) -> Length ('O algn 'Nothing ot t)
forall (algn :: Alignment) (mnm :: Maybe Symbol) (ot :: ObjectType)
       t (mnm' :: Maybe Symbol).
Length ('O algn mnm ot t) -> Length ('O algn mnm' ot t)
KObj.renameLength Length s
Length ('O algn ('Just _nm) ot t)
ln Length ('O algn 'Nothing ot t)
-> PL Length ss1 -> PL Length ('O algn 'Nothing ot t : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length ss1
PL Length (OnlyDynamics os')
lns' PL Length ss1
PL Length (OnlyDynamics os)
lns

instance UpdateDynamicLengthPrefix os os' =>
	UpdateDynamicLengthPrefix
		(VObj.Static_ o : os) (VObj.Static_ o : os') where
	updateDynamicLengthPrefix :: PL Length (OnlyDynamics ('Static_ o : os'))
-> PL Length (OnlyDynamics ('Static_ o : os))
-> PL Length (OnlyDynamics ('Static_ o : os'))
updateDynamicLengthPrefix PL Length (OnlyDynamics ('Static_ o : os'))
lns' PL Length (OnlyDynamics ('Static_ o : os))
lns  =
		forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length (OnlyDynamics os')
PL Length (OnlyDynamics ('Static_ o : os'))
lns' PL Length (OnlyDynamics os)
PL Length (OnlyDynamics ('Static_ o : os))
lns

instance UpdateDynamicLengthPrefix os os' =>
	UpdateDynamicLengthPrefix
		('VObj.Dynamic n o : os) ('VObj.Dynamic n o : os') where
	updateDynamicLengthPrefix :: PL Length (OnlyDynamics ('Dynamic n o : os'))
-> PL Length (OnlyDynamics ('Dynamic n o : os))
-> PL Length (OnlyDynamics ('Dynamic n o : os'))
updateDynamicLengthPrefix (Length s
_ln :** PL Length ss1
lns') (Length s
ln :** PL Length ss1
lns) =
		Length s
ln Length s -> PL Length ss1 -> PL Length (s : ss1)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** forall (objs :: [O]) (objs' :: [O]).
UpdateDynamicLengthPrefix objs objs' =>
PL Length (OnlyDynamics objs')
-> PL Length (OnlyDynamics objs) -> PL Length (OnlyDynamics objs')
updateDynamicLengthPrefix @os @os' PL Length ss1
PL Length (OnlyDynamics os')
lns' PL Length ss1
PL Length (OnlyDynamics os)
lns