{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.Vec.Lazy.Lens  (
    -- * Indexing
    ix,
    _Cons,
    _head,
    _tail,
    -- * Conversions
    _Pull,
    _Vec,
    ) where

import Control.Applicative ((<$>))
import Data.Fin            (Fin (..))
import Data.Nat            (Nat (..))
import Prelude             ((.))

import qualified Control.Lens  as L
import qualified Data.Type.Nat as N
import qualified Data.Vec.Pull as P

import Data.Vec.Lazy

-- $setup
-- >>> :set -XScopedTypeVariables
-- >>> import Data.Vec.Lazy
-- >>> import Data.Fin (Fin (..))
-- >>> import Prelude (Maybe (..), Char, Bool (..))
-- >>> import Control.Lens ((^.), (&), (.~), over, (^?), (#))
-- >>> import qualified Data.Type.Nat as N

-------------------------------------------------------------------------------
-- Indexing
-------------------------------------------------------------------------------

-- | Index lens.
--
-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
-- 'b'
--
-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
-- 'a' ::: 'x' ::: 'c' ::: VNil
--
ix :: Fin n -> L.Lens' (Vec n a) a
ix :: Fin n -> Lens' (Vec n a) a
ix Fin n
FZ     a -> f a
f (a
x ::: Vec n1 a
xs) = (a -> Vec n1 a -> Vec ('S n1) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec n1 a
xs) (a -> Vec ('S n1) a) -> f a -> f (Vec ('S n1) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f a
x
ix (FS Fin n1
n) a -> f a
f (a
x ::: Vec n1 a
xs) = (a
x a -> Vec n1 a -> Vec ('S n1) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
:::)  (Vec n1 a -> Vec ('S n1) a) -> f (Vec n1 a) -> f (Vec ('S n1) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Fin n1 -> (a -> f a) -> Vec n1 a -> f (Vec n1 a)
forall (n :: Nat) a. Fin n -> Lens' (Vec n a) a
ix Fin n1
n a -> f a
f Vec n1 a
Vec n1 a
xs

-- | Match on non-empty 'Vec'.
--
-- /Note:/ @lens@ 'L._Cons' is a 'L.Prism'.
-- In fact, @'Vec' n a@ cannot have an instance of 'L.Cons' as types don't match.
--
_Cons :: L.Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)
_Cons :: p (a, Vec n a) (f (b, Vec n b))
-> p (Vec ('S n) a) (f (Vec ('S n) b))
_Cons = (Vec ('S n) a -> (a, Vec n a))
-> ((b, Vec n b) -> Vec ('S n) b)
-> Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
L.iso (\(a
x ::: Vec n1 a
xs) -> (a
x, Vec n1 a
xs)) (\(b
x, Vec n b
xs) -> b
x b -> Vec n b -> Vec ('S n) b
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec n b
xs)

-- | Head lens. /Note:/ @lens@ 'L._head' is a 'L.Traversal''.
--
-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. _head
-- 'a'
--
-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'
-- 'x' ::: 'b' ::: 'c' ::: VNil
--
_head :: L.Lens' (Vec ('S n) a) a
_head :: (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
_head a -> f a
f (a
x ::: Vec n1 a
xs) = (a -> Vec n1 a -> Vec ('S n1) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec n1 a
xs) (a -> Vec ('S n1) a) -> f a -> f (Vec ('S n1) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f a
x
{-# INLINE _head #-}

-- | Tail lens.
_tail :: L.Lens' (Vec ('S n) a) (Vec n a)
_tail :: (Vec n a -> f (Vec n a)) -> Vec ('S n) a -> f (Vec ('S n) a)
_tail Vec n a -> f (Vec n a)
f (a
x ::: Vec n1 a
xs) = (a
x a -> Vec n a -> Vec ('S n) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
:::) (Vec n a -> Vec ('S n) a) -> f (Vec n a) -> f (Vec ('S n) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec n a -> f (Vec n a)
f Vec n a
Vec n1 a
xs
{-# INLINE _tail #-}

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

-- | An 'I.Iso' from 'toPull' and 'fromPull'.
_Pull :: N.SNatI n => L.Iso (Vec n a) (Vec n b) (P.Vec n a) (P.Vec n b)
_Pull :: Iso (Vec n a) (Vec n b) (Vec n a) (Vec n b)
_Pull = (Vec n a -> Vec n a)
-> (Vec n b -> Vec n b)
-> Iso (Vec n a) (Vec n b) (Vec n a) (Vec n b)
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
L.iso Vec n a -> Vec n a
forall (n :: Nat) a. Vec n a -> Vec n a
toPull Vec n b -> Vec n b
forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
fromPull

-- | Prism from list.
--
-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)
-- Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)
-- Nothing
--
-- >>> _Vec # (True ::: False ::: VNil)
-- [True,False]
--
_Vec :: N.SNatI n => L.Prism' [a] (Vec n a)
_Vec :: Prism' [a] (Vec n a)
_Vec = (Vec n a -> [a])
-> ([a] -> Maybe (Vec n a)) -> Prism' [a] (Vec n a)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
L.prism' Vec n a -> [a]
forall (n :: Nat) a. Vec n a -> [a]
toList [a] -> Maybe (Vec n a)
forall (n :: Nat) a. SNatI n => [a] -> Maybe (Vec n a)
fromList

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

#if !MIN_VERSION_lens(5,0,0)
instance L.FunctorWithIndex (Fin n) (Vec n) where
    imap = imap

instance L.FoldableWithIndex (Fin n) (Vec n) where
    ifoldMap = ifoldMap
    ifoldr   = ifoldr

instance L.TraversableWithIndex (Fin n) (Vec n) where
    itraverse = itraverse
#endif

instance L.Each (Vec n a) (Vec n b) a b where
    each :: (a -> f b) -> Vec n a -> f (Vec n b)
each = (a -> f b) -> Vec n a -> f (Vec n b)
forall (n :: Nat) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse

type instance L.Index (Vec n a)   = Fin n
type instance L.IxValue (Vec n a) = a

-- | 'Vec' doesn't have 'L.At' instance, as we __cannot__ remove value from 'Vec'.
-- See 'ix' in "Data.Vec.Lazy" module for an 'L.Lens' (not 'L.Traversal').
instance L.Ixed (Vec n a) where
    ix :: Index (Vec n a) -> Traversal' (Vec n a) (IxValue (Vec n a))
ix Index (Vec n a)
i = Fin n -> Lens' (Vec n a) a
forall (n :: Nat) a. Fin n -> Lens' (Vec n a) a
ix Fin n
Index (Vec n a)
i

instance L.Field1 (Vec ('S n) a) (Vec ('S n) a) a a where
    _1 :: (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
_1 = (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (n :: Nat) a. Lens (Vec ('S n) a) (Vec ('S n) a) a a
_head

instance L.Field2 (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a where
    _2 :: (a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a)
_2 = (Vec ('S n) a -> f (Vec ('S n) a))
-> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S n) a -> f (Vec ('S n) a))
 -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (n :: Nat) a. Lens (Vec ('S n) a) (Vec ('S n) a) a a
_head

instance L.Field3 (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a where
    _3 :: (a -> f a) -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a)
_3 = (Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
 -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S n) a -> f (Vec ('S n) a))
-> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S n) a -> f (Vec ('S n) a))
 -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (n :: Nat) a. Lens (Vec ('S n) a) (Vec ('S n) a) a a
_head

instance L.Field4 (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a where
    _4 :: (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a)
_4 = (Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
 -> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
 -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S n) a -> f (Vec ('S n) a))
-> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S n) a -> f (Vec ('S n) a))
 -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (n :: Nat) a. Lens (Vec ('S n) a) (Vec ('S n) a) a a
_head

instance L.Field5 (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S ('S n))))) a) a a where
    _5 :: (a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
_5 = (Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
 -> Vec ('S ('S ('S ('S ('S n))))) a
 -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
 -> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
 -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S n) a -> f (Vec ('S n) a))
-> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S n) a -> f (Vec ('S n) a))
 -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (n :: Nat) a. Lens (Vec ('S n) a) (Vec ('S n) a) a a
_head

instance L.Field6 (Vec ('S ('S ('S ('S ('S ('S n)))))) a) (Vec ('S ('S ('S ('S ('S ('S n)))))) a) a a where
    _6 :: (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
_6 = (Vec ('S ('S ('S ('S ('S n))))) a
 -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S ('S n))))) a
  -> f (Vec ('S ('S ('S ('S ('S n))))) a))
 -> Vec ('S ('S ('S ('S ('S ('S n)))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S ('S n))))) a
    -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
 -> Vec ('S ('S ('S ('S ('S n))))) a
 -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
 -> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
 -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S n) a -> f (Vec ('S n) a))
-> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S n) a -> f (Vec ('S n) a))
 -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (n :: Nat) a. Lens (Vec ('S n) a) (Vec ('S n) a) a a
_head

instance L.Field7 (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a) a a where
    _7 :: (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
_7 = (Vec ('S ('S ('S ('S ('S ('S n)))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S ('S ('S n)))))) a
  -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
 -> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S ('S ('S n)))))) a
    -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S ('S ('S n))))) a
 -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S ('S n))))) a
  -> f (Vec ('S ('S ('S ('S ('S n))))) a))
 -> Vec ('S ('S ('S ('S ('S ('S n)))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S ('S n))))) a
    -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
 -> Vec ('S ('S ('S ('S ('S n))))) a
 -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
 -> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
 -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S n) a -> f (Vec ('S n) a))
-> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S n) a -> f (Vec ('S n) a))
 -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (n :: Nat) a. Lens (Vec ('S n) a) (Vec ('S n) a) a a
_head

instance L.Field8 (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a) a a where
    _8 :: (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
_8 = (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a))
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
  -> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a))
 -> Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
    -> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S ('S ('S ('S n)))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S ('S ('S n)))))) a
  -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
 -> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S ('S ('S n)))))) a
    -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S ('S ('S n))))) a
 -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S ('S n))))) a
  -> f (Vec ('S ('S ('S ('S ('S n))))) a))
 -> Vec ('S ('S ('S ('S ('S ('S n)))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S ('S n))))) a
    -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
 -> Vec ('S ('S ('S ('S ('S n))))) a
 -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
 -> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
 -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S n) a -> f (Vec ('S n) a))
-> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S n) a -> f (Vec ('S n) a))
 -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (n :: Nat) a. Lens (Vec ('S n) a) (Vec ('S n) a) a a
_head

instance L.Field9 (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a) a a where
    _9 :: (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
_9 = (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a))
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
  -> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a))
 -> Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
    -> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a))
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
  -> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a))
 -> Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
    -> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S ('S ('S ('S n)))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S ('S ('S n)))))) a
  -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
 -> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S ('S ('S n)))))) a
    -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S ('S ('S n))))) a
 -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S ('S n))))) a
  -> f (Vec ('S ('S ('S ('S ('S n))))) a))
 -> Vec ('S ('S ('S ('S ('S ('S n)))))) a
 -> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S ('S n))))) a
    -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
 -> Vec ('S ('S ('S ('S ('S n))))) a
 -> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
 -> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> ((a -> f a)
    -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
 -> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S n) a -> f (Vec ('S n) a))
-> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail ((Vec ('S n) a -> f (Vec ('S n) a))
 -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (n :: Nat) a. Lens (Vec ('S n) a) (Vec ('S n) a) a a
_head