diff --git a/CHANGELOG.md b/CHANGELOG.md
index dab7fc3..8617260 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Changelog
 
+## Unreleased
+
+**Breaking changes**
+- Update to use VTAs
+
 ## [v0.7.0]
 - Add read & write optimised sparse vectors (#10 by @mikesol)
 
diff --git a/README.md b/README.md
index dc876ce..8beaa88 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,10 @@
 
 Fast, type-safe vector libary for Purescript inspired by [Idris](https://www.idris-lang.org/). A vector is list with its size encoded in the type.
 
+https://user-images.githubusercontent.com/77549848/179352478-36ddb5ee-dc51-4d53-ad5c-19b244cd2f7b.mp4
+
+
+
 ## Installation
 
 ```bash
@@ -41,7 +45,7 @@ You will get an `elem` back, no need to handle a `Maybe`. And this operation is
 
 Similarly, the `index` function has the following type signature (conceptually - the real one is slightly more complex):
 ```purescript
-index :: forall i m elem. Term i -> Vect m elem -> elem
+index :: forall @i m elem. Vect m elem -> elem
 ```
 If the index `i` (represented as a typelevel symbol) is in bounds, i.e. `i < m`, you will get an `elem` back, otherwise you will get a compile-time error. 
 
@@ -59,35 +63,35 @@ import Prelude
 
 import Data.FastVect.FastVect (Vect)
 import Data.FastVect.FastVect as FV
-import Typelevel.Arithmetic.Add (Term, term)
 
 as :: Vect 300 String
-as = FV.replicate (term :: Term 300) "a"
--- Note you could also leave out the Term type annotation, as PS can infer it:
--- as = FV.replicate (term :: _ 300) "a"
+as = FV.replicate @300 "a"
+-- Note: you can leave out the type annotation, as PS can infer it:
+-- as = FV.replicate @300 "a"
 
 bs :: Vect 200 String
-bs = FV.replicate (term :: Term 200) "b"
+bs = FV.replicate @200 "b"
 
 cs :: Vect 500 String
 cs = FV.append as bs
 
 ds :: Vect 2 String
-ds = cs # FV.drop (term :: Term 299) # FV.take (term :: Term 2)
+ds = cs # FV.drop @299 # FV.take @2
 
 x :: String
-x = FV.index (term :: Term 499) cs
+x = FV.index @499 cs
 
 y :: String
 y = FV.head (FV.singleton "a")
 
 big1 :: Vect 23923498230498230420 String
-big1 = FV.replicate (term :: Term 23923498230498230420) "a"
+big1 = FV.replicate @23923498230498230420 "a"
 
 big2 :: Vect 203948023984590684596840586 String
-big2 = FV.replicate (term :: Term 203948023984590684596840586) "b"
+big2 = FV.replicate @203948023984590684596840586 "b"
 
 big :: Vect 203948047908088915095071006 String
 big = FV.append big1 big2
--- Note the big example will blow up during runtime.
+-- Note: the big example will blow up during runtime. Need to increase Node.js memory for this ;)
 ```
+
diff --git a/purescript-vect.gif b/purescript-vect.gif
new file mode 100644
index 0000000..1d0be08
Binary files /dev/null and b/purescript-vect.gif differ
diff --git a/src/Data/FastVect/Common.purs b/src/Data/FastVect/Common.purs
index cbf9dc4..95e9266 100644
--- a/src/Data/FastVect/Common.purs
+++ b/src/Data/FastVect/Common.purs
@@ -41,8 +41,8 @@ class TraversableWithIndex Int f <= IsVect f
 term ∷ forall (i ∷ Int). Proxy i
 term = Proxy
 
-toInt ∷ forall (len ∷ Int). Reflectable len Int ⇒ Proxy len → Int
-toInt = reflectType
+toInt ∷ forall (@len ∷ Int). Reflectable len Int ⇒ Int
+toInt = reflectType (Proxy :: _ len)
 
 -- -- | Create a `Vect` by replicating `len` times the given element
 -- -- |
@@ -53,8 +53,7 @@ toInt = reflectType
 type Replicate vect len elem =
   Compare len NegOne GT
   ⇒ Reflectable len Int
-  ⇒ Proxy len
-  → elem
+  ⇒ elem
   → vect len elem
 
 -- -- | Creates the empty `Vect`.
@@ -121,8 +120,7 @@ type Drop vect m n m_plus_n elem =
   ⇒ Reflectable m Int
   ⇒ Compare m NegOne GT
   ⇒ Compare n NegOne GT
-  ⇒ Proxy m
-  → vect m_plus_n elem
+  ⇒ vect m_plus_n elem
   → vect n elem
 
 -- -- | Safely take `m` elements from a `Vect`.
@@ -141,8 +139,7 @@ type Take vect m n m_plus_n elem =
   ⇒ Reflectable m Int
   ⇒ Compare m NegOne GT
   ⇒ Compare n NegOne GT
-  ⇒ Proxy m
-  → vect m_plus_n elem
+  ⇒ vect m_plus_n elem
   → vect m elem
 
 -- -- | Safely modify element `m` from a `Vect`.
@@ -159,8 +156,7 @@ type Modify vect m n elem =
   ⇒ Compare m NegOne GT
   ⇒ Compare n NegOne GT
   ⇒ Compare m n LT
-  ⇒ Proxy m
-  → (elem → elem)
+  ⇒ (elem → elem)
   → vect n elem
   → vect n elem
 
@@ -178,8 +174,7 @@ type Set vect m n elem =
   ⇒ Compare m NegOne GT
   ⇒ Compare n NegOne GT
   ⇒ Compare m n LT
-  ⇒ Proxy m
-  → elem
+  ⇒ elem
   → vect n elem
   → vect n elem
 
@@ -201,8 +196,7 @@ type SplitAt vect m n m_plus_n elem =
   ⇒ Reflectable m Int
   ⇒ Compare m NegOne GT
   ⇒ Compare n NegOne GT
-  ⇒ Proxy m
-  → vect m_plus_n elem
+  ⇒ vect m_plus_n elem
   → { before ∷ vect m elem, after ∷ vect n elem }
 
 -- -- | Safely access the `n`-th modulo m element of a `Vect`.
@@ -243,8 +237,7 @@ type Index vect m m_minus_one i n elem =
   ⇒ Add i n m_minus_one
   ⇒ Compare i NegOne GT
   ⇒ Reflectable i Int
-  ⇒ Proxy i
-  → vect m elem
+  ⇒ vect m elem
   → elem
 
 type IndexM vect m m_minus_one i n elem =
@@ -254,8 +247,7 @@ type IndexM vect m m_minus_one i n elem =
   ⇒ Add i n m_minus_one
   ⇒ Compare i NegOne GT
   ⇒ Reflectable i Int
-  ⇒ Proxy i
-  → vect m elem
+  ⇒ vect m elem
   → Maybe elem
 -- -- | Safely access the head of a `Vect`.
 -- -- |
diff --git a/src/Data/FastVect/FastVect.purs b/src/Data/FastVect/FastVect.purs
index 573f7d9..8edb00e 100644
--- a/src/Data/FastVect/FastVect.purs
+++ b/src/Data/FastVect/FastVect.purs
@@ -49,7 +49,7 @@ newtype Vect ∷ Int → Type → Type
 newtype Vect len elem = Vect (Array elem)
 
 instance (Show elem, Reflectable len Int) ⇒ Show (Vect len elem) where
-  show (Vect elems) = "Vect " <> show (Common.toInt (Common.term ∷ _ len)) <> " " <> show elems
+  show (Vect elems) = "Vect " <> show (Common.toInt @len) <> " " <> show elems
 
 derive newtype instance Eq elem ⇒ Eq (Vect len elem)
 derive newtype instance Ord elem ⇒ Ord (Vect len elem)
@@ -58,7 +58,7 @@ instance Apply (Vect len) where
   apply (Vect fab) (Vect a) = Vect (Array.zipWith ($) fab a)
 
 instance (Compare len Common.NegOne GT, Reflectable len Int) ⇒ Applicative (Vect len) where
-  pure = replicate (Proxy :: _ len)
+  pure = replicate @len
 
 derive newtype instance FunctorWithIndex Int (Vect len)
 derive newtype instance Foldable (Vect len)
@@ -72,8 +72,8 @@ derive newtype instance TraversableWithIndex Int (Vect len)
 -- -- | vect ∷ Vect 300 String
 -- -- | vect = replicate (Common.term ∷ _ 300) "a"
 -- -- | ```
-replicate ∷ ∀ len elem. Common.Replicate Vect len elem
-replicate proxy elem = Vect $ A.replicate (Common.toInt proxy) elem
+replicate ∷ ∀ @len elem. Common.Replicate Vect len elem
+replicate elem = Vect $ A.replicate (Common.toInt @len) elem
 
 -- -- | Creates the empty `Vect`.
 -- -- |
@@ -118,8 +118,8 @@ append (Vect xs) (Vect ys) = Vect (xs <> ys)
 -- -- | newVect ∷ Vect 200 String
 -- -- | newVect = drop (Common.term ∷ _ 100) vect
 -- -- | ```
-drop ∷ ∀ m n m_plus_n elem. Common.Drop Vect m n m_plus_n elem
-drop proxy (Vect xs) = Vect (A.drop (Common.toInt proxy) xs)
+drop ∷ ∀ @m n m_plus_n elem. Common.Drop Vect m n m_plus_n elem
+drop (Vect xs) = Vect (A.drop (Common.toInt @m) xs)
 
 -- -- | Safely take `m` elements from a `Vect`.
 -- -- | Will result in a compile-time error if you are trying to take more elements than exist in the vector.
@@ -131,8 +131,8 @@ drop proxy (Vect xs) = Vect (A.drop (Common.toInt proxy) xs)
 -- -- | newVect ∷ Vect 100 String
 -- -- | newVect = take (Common.term ∷ _ 100) vect
 -- -- | ```
-take ∷ ∀ m n m_plus_n elem. Common.Take Vect m n m_plus_n elem
-take proxy (Vect xs) = Vect (A.take (Common.toInt proxy) xs)
+take ∷ ∀ @m n m_plus_n elem. Common.Take Vect m n m_plus_n elem
+take (Vect xs) = Vect (A.take (Common.toInt @m) xs)
 
 foreign import modifyImpl :: forall n elem. Int → (elem → elem) → Vect n elem → Vect n elem
 
@@ -145,8 +145,8 @@ foreign import modifyImpl :: forall n elem. Int → (elem → elem) → Vect n e
 -- -- | newVect ∷ Vect 100 String
 -- -- | newVect = modify (Common.term ∷ _ 100) (append "b") vect
 -- -- | ```
-modify ∷ ∀ m n elem. Common.Modify Vect m n elem
-modify proxy = modifyImpl (Common.toInt proxy)
+modify ∷ ∀ @m n elem. Common.Modify Vect m n elem
+modify = modifyImpl (Common.toInt @m)
 
 -- -- | Safely set element `m` from a `Vect`.
 -- -- |
@@ -158,7 +158,7 @@ modify proxy = modifyImpl (Common.toInt proxy)
 -- -- | newVect = modify (Common.term ∷ _ 100) "b" vect
 -- -- | `
 set ∷ ∀ m n elem. Common.Set Vect m n elem
-set proxy = modify proxy <<< const
+set = modify @m <<< const
 
 -- -- | Split the `Vect` into two sub vectors `before` and `after`, where before contains up to `m` elements.
 -- -- |
@@ -172,10 +172,10 @@ set proxy = modify proxy <<< const
 -- -- |   }
 -- -- | split = splitAt (Common.term ∷ _ 3) vect
 -- -- | ```
-splitAt ∷ ∀ m n m_plus_n elem. Common.SplitAt Vect m n m_plus_n elem
-splitAt proxy (Vect xs) = { before: Vect before, after: Vect after }
+splitAt ∷ ∀ @m n m_plus_n elem. Common.SplitAt Vect m n m_plus_n elem
+splitAt (Vect xs) = { before: Vect before, after: Vect after }
   where
-  { before, after } = A.splitAt (Common.toInt proxy) xs
+  { before, after } = A.splitAt (Common.toInt @m) xs
 
 -- -- | Safely access the `n`-th modulo m element of a `Vect`.
 -- -- |
@@ -187,7 +187,7 @@ splitAt proxy (Vect xs) = { before: Vect before, after: Vect after }
 -- -- | elem = indexModulo 5352523 vect
 -- -- | ```
 indexModulo ∷ ∀ m elem. Common.IndexModulo Vect m elem
-indexModulo i = indexImpl (i `mod` Common.toInt (Proxy ∷ _ m))
+indexModulo i = indexImpl (i `mod` Common.toInt @m)
 
 foreign import indexImpl :: forall m elem. Int → Vect m elem → elem
 
@@ -200,8 +200,8 @@ foreign import indexImpl :: forall m elem. Int → Vect m elem → elem
 -- -- | elem ∷ String
 -- -- | elem = index (Common.term ∷ _ 299) vect
 -- -- | ```
-index ∷ ∀ m m_minus_one i n elem. Common.Index Vect m m_minus_one i n elem
-index = indexImpl <<< Common.toInt
+index ∷ ∀ m m_minus_one @i n elem. Common.Index Vect m m_minus_one i n elem
+index = indexImpl (Common.toInt @i)
 
 -- -- | Safely access the head of a `Vect`.
 -- -- |
@@ -223,14 +223,13 @@ head = indexImpl 0
 -- -- | fromArray (Common.term ∷ _ 4) ["a", "b", "c"] = Nothing
 -- -- | ```
 fromArray
-  ∷ ∀ len elem
+  ∷ ∀ @len elem
   . Reflectable len Int
   ⇒ Compare len Common.NegOne GT
-  ⇒ Proxy len
-  → Array elem
+  ⇒ Array elem
   → Maybe (Vect len elem)
-fromArray proxy array | Array.length array == Common.toInt proxy = Just (Vect array)
-fromArray _ _ = Nothing
+fromArray array | Array.length array == Common.toInt @len = Just (Vect array)
+fromArray _ = Nothing
 
 -- -- | Converts the `Vect` to an `Array`, effectively dropping the size information.
 toArray
@@ -248,28 +247,26 @@ toArray (Vect arr) = arr
 -- -- | toArray $ adjust (Common.term ∷ _ 3) 0 [ 0, 0, 0, 0, 1, 2, 3 ] == [ 1, 2, 3 ]
 -- -- | ```
 adjust
-  ∷ ∀ len elem
+  ∷ ∀ @len elem
   . Reflectable len Int
   ⇒ Compare len Common.NegOne GT
-  ⇒ Proxy len
-  → elem
+  ⇒ elem
   → Array elem
   → Vect len elem
-adjust proxy elem array = case Array.length array - Common.toInt proxy of
+adjust elem array = case Array.length array - Common.toInt @len of
   0 → Vect array
   len | len < 0 → Vect $ A.replicate (abs len) elem <> array
   len → Vect $ A.drop len array
 
 -- -- | Like `adjust` but uses the Moinoid instance of elem to create the elements.
 adjustM
-  ∷ ∀ len elem
+  ∷ ∀ @len elem
   . Monoid elem
   ⇒ Reflectable len Int
   ⇒ Compare len Common.NegOne GT
-  ⇒ Proxy len
-  → Array elem
+  ⇒ Array elem
   → Vect len elem
-adjustM proxy = adjust proxy mempty
+adjustM = adjust @len mempty
 
 -- -- | Attaches an element to the front of the `Vect`, creating a new `Vect` with size incremented.
 -- -- |
diff --git a/src/Data/FastVect/Sparse/Read.purs b/src/Data/FastVect/Sparse/Read.purs
index 75de5b3..d3b45c6 100644
--- a/src/Data/FastVect/Sparse/Read.purs
+++ b/src/Data/FastVect/Sparse/Read.purs
@@ -52,14 +52,14 @@ newtype Vect ∷ Int → Type → Type
 newtype Vect len elem = Vect (Map Int elem)
 
 instance (Show elem, Reflectable len Int) ⇒ Show (Vect len elem) where
-  show (Vect elems) = "Vect.Sparse.Read " <> show (Common.toInt (Common.term ∷ _ len)) <> " " <> show elems
+  show (Vect elems) = "Vect.Sparse.Read " <> show (Common.toInt @len) <> " " <> show elems
 
 derive newtype instance Eq elem ⇒ Eq (Vect len elem)
 derive newtype instance Ord elem ⇒ Ord (Vect len elem)
 derive newtype instance Functor (Vect len)
 derive newtype instance Apply (Vect len)
 instance (Compare len Common.NegOne GT, Reflectable len Int) ⇒ Applicative (Vect len) where
-  pure = replicate (Proxy :: _ len)
+  pure = replicate @len
 
 derive newtype instance FunctorWithIndex Int (Vect len)
 derive newtype instance Foldable (Vect len)
@@ -73,10 +73,10 @@ derive newtype instance TraversableWithIndex Int (Vect len)
 -- -- | vect ∷ Vect 300 String
 -- -- | vect = replicate (Common.term ∷ _ 300) "a"
 -- -- | ```
-replicate ∷ ∀ len elem. Common.Replicate Vect len elem
-replicate proxy elem = Vect $ (Map.fromFoldable :: Array _ -> _) $ (unfoldr (\i@(ix /\ b) -> if ix == terminus then Nothing else Just (i /\ ((ix + 1) /\ b))) (0 /\ elem))
+replicate ∷ ∀ @len elem. Common.Replicate Vect len elem
+replicate elem = Vect $ (Map.fromFoldable :: Array _ -> _) $ (unfoldr (\i@(ix /\ b) -> if ix == terminus then Nothing else Just (i /\ ((ix + 1) /\ b))) (0 /\ elem))
   where
-  terminus = Common.toInt proxy
+  terminus = Common.toInt @len
 
 -- -- | Creates the empty `Vect`.
 -- -- |
@@ -117,8 +117,8 @@ singleton elem = Vect (Map.singleton 0 elem)
 -- -- | cs ∷ Vect 500 String
 -- -- | cs = append as bs
 -- -- | ```
-append ∷ ∀ m n m_plus_n elem. Common.Append Vect m n m_plus_n elem
-append (Vect xs) (Vect ys) = Vect (Map.union xs (Map.fromFoldable $ map (first (add (Common.toInt (Proxy :: _ m)))) $ (Map.toUnfoldableUnordered :: _ -> Array _) ys))
+append ∷ ∀ @m n m_plus_n elem. Common.Append Vect m n m_plus_n elem
+append (Vect xs) (Vect ys) = Vect (Map.union xs (Map.fromFoldable $ map (first (add (Common.toInt @m))) $ (Map.toUnfoldableUnordered :: _ -> Array _) ys))
 
 -- -- | Safely drop `m` elements from a `Vect`.
 -- -- | Will result in a compile-time error if you are trying to drop more elements than exist in the vector.
@@ -130,10 +130,10 @@ append (Vect xs) (Vect ys) = Vect (Map.union xs (Map.fromFoldable $ map (first (
 -- -- | newVect ∷ Vect 200 String
 -- -- | newVect = drop (Common.term ∷ _ 100) vect
 -- -- | ```
-drop ∷ ∀ m n m_plus_n elem. Common.Drop Vect m n m_plus_n elem
-drop proxy (Vect xs) = Vect ((Map.fromFoldable :: Array _ -> _) $ filterMap (\(ix /\ a) -> if ix >= drops then Just ((ix - drops) /\ a) else Nothing) $ Map.toUnfoldableUnordered xs)
+drop ∷ ∀ @m n m_plus_n elem. Common.Drop Vect m n m_plus_n elem
+drop (Vect xs) = Vect ((Map.fromFoldable :: Array _ -> _) $ filterMap (\(ix /\ a) -> if ix >= drops then Just ((ix - drops) /\ a) else Nothing) $ Map.toUnfoldableUnordered xs)
   where
-  drops = Common.toInt proxy
+  drops = Common.toInt @m
 
 -- -- | Safely take `m` elements from a `Vect`.
 -- -- | Will result in a compile-time error if you are trying to take more elements than exist in the vector.
@@ -145,10 +145,10 @@ drop proxy (Vect xs) = Vect ((Map.fromFoldable :: Array _ -> _) $ filterMap (\(i
 -- -- | newVect ∷ Vect 100 String
 -- -- | newVect = take (Common.term ∷ _ 100) vect
 -- -- | ```
-take ∷ ∀ m n m_plus_n elem. Common.Take Vect m n m_plus_n elem
-take proxy (Vect xs) = Vect (Map.fromFoldable $ Array.filter (fst >>> (_ < takes)) $ Map.toUnfoldableUnordered xs)
+take ∷ ∀ @m n m_plus_n elem. Common.Take Vect m n m_plus_n elem
+take (Vect xs) = Vect (Map.fromFoldable $ Array.filter (fst >>> (_ < takes)) $ Map.toUnfoldableUnordered xs)
   where
-  takes = Common.toInt proxy
+  takes = Common.toInt @m
 
 -- -- | Safely modify element `m` from a `Vect`.
 -- -- |
@@ -159,8 +159,8 @@ take proxy (Vect xs) = Vect (Map.fromFoldable $ Array.filter (fst >>> (_ < takes
 -- -- | newVect ∷ Vect 100 String
 -- -- | newVect = modify (Common.term ∷ _ 100) (append "b") vect
 -- -- | ```
-modify ∷ ∀ m n elem. Common.Modify Vect m n elem
-modify proxy f (Vect xs) = Vect $ Map.update (f >>> Just) (Common.toInt proxy) xs
+modify ∷ ∀ @m n elem. Common.Modify Vect m n elem
+modify f (Vect xs) = Vect $ Map.update (f >>> Just) (Common.toInt @m) xs
 
 -- -- | Safely set element `m` from a `Vect`.
 -- -- |
@@ -171,8 +171,8 @@ modify proxy f (Vect xs) = Vect $ Map.update (f >>> Just) (Common.toInt proxy) x
 -- -- | newVect ∷ Vect 100 String
 -- -- | newVect = modify (Common.term ∷ _ 100) "b" vect
 -- -- | `
-set ∷ ∀ m n elem. Common.Set Vect m n elem
-set proxy a (Vect xs) = Vect $ Map.alter (const (Just a)) (Common.toInt proxy) xs
+set ∷ ∀ @m n elem. Common.Set Vect m n elem
+set a (Vect xs) = Vect $ Map.alter (const (Just a)) (Common.toInt @m) xs
 
 -- -- | Split the `Vect` into two sub vectors `before` and `after`, where before contains up to `m` elements.
 -- -- |
@@ -186,10 +186,10 @@ set proxy a (Vect xs) = Vect $ Map.alter (const (Just a)) (Common.toInt proxy) x
 -- -- |   }
 -- -- | split = splitAt (Common.term ∷ _ 3) vect
 -- -- | ```
-splitAt ∷ ∀ m n m_plus_n elem. Common.SplitAt Vect m n m_plus_n elem
-splitAt proxy (Vect xs) = ((\{ yes, no } -> { before: Vect $ Map.fromFoldable yes, after: Vect $ Map.fromFoldable no }) $ Array.partition (fst >>> (_ < splits)) $ Map.toUnfoldableUnordered xs)
+splitAt ∷ ∀ @m n m_plus_n elem. Common.SplitAt Vect m n m_plus_n elem
+splitAt (Vect xs) = ((\{ yes, no } -> { before: Vect $ Map.fromFoldable yes, after: Vect $ Map.fromFoldable no }) $ Array.partition (fst >>> (_ < splits)) $ Map.toUnfoldableUnordered xs)
   where
-  splits = Common.toInt proxy
+  splits = Common.toInt @m
 
 -- -- | Safely access the `n`-th modulo m element of a `Vect`.
 -- -- |
@@ -201,7 +201,7 @@ splitAt proxy (Vect xs) = ((\{ yes, no } -> { before: Vect $ Map.fromFoldable ye
 -- -- | elem = indexModulo 5352523 vect
 -- -- | ```
 indexModulo ∷ ∀ m elem. Common.IndexModuloM Vect m elem
-indexModulo i (Vect xs) = Map.lookup (i `mod` Common.toInt (Proxy ∷ _ m)) xs
+indexModulo i (Vect xs) = Map.lookup (i `mod` Common.toInt @m) xs
 
 -- -- | Safely access the `i`-th element of a `Vect`.
 -- -- |
@@ -212,8 +212,8 @@ indexModulo i (Vect xs) = Map.lookup (i `mod` Common.toInt (Proxy ∷ _ m)) xs
 -- -- | elem ∷ String
 -- -- | elem = index (Common.term ∷ _ 299) vect
 -- -- | ```
-index ∷ ∀ m m_minus_one i n elem. Common.IndexM Vect m m_minus_one i n elem
-index proxy (Vect xs) = Map.lookup (Common.toInt proxy) xs
+index ∷ ∀ m m_minus_one @i n elem. Common.IndexM Vect m m_minus_one i n elem
+index (Vect xs) = Map.lookup (Common.toInt @i) xs
 
 -- -- | Safely access the head of a `Vect`.
 -- -- |
@@ -235,16 +235,15 @@ head (Vect xs) = Map.lookup 0 xs
 -- -- | fromArray (Common.term ∷ _ 4) ["a", "b", "c"] = Nothing
 -- -- | ```
 fromMap
-  ∷ ∀ len elem
+  ∷ ∀ @len elem
   . Reflectable len Int
   ⇒ Compare len Common.NegOne GT
-  ⇒ Proxy len
-  → Map.Map Int elem
+  ⇒ Map.Map Int elem
   → Maybe (Vect len elem)
-fromMap proxy mp
+fromMap mp
   | Just { key } <- Map.findMax mp
-  , key < Common.toInt proxy && key >= 0 = Just (Vect mp)
-fromMap _ _ = Nothing
+  , key < Common.toInt @len && key >= 0 = Just (Vect mp)
+fromMap _ = Nothing
 
 -- -- | Converts the `Vect` to an `Array`, effectively dropping the size information.
 toMap
@@ -261,7 +260,7 @@ cons elem (Vect arr) = Vect (Map.insert 0 elem (Map.fromFoldable $ map (first (a
 
 snoc
   ∷ ∀ len len_plus_1 elem. Common.Snoc Vect len len_plus_1 elem
-snoc (Vect xs) elem = Vect $ Map.insert (Common.toInt (Proxy :: _ len)) elem xs
+snoc (Vect xs) elem = Vect $ Map.insert (Common.toInt @len) elem xs
 
 infixr 6 cons as :
 infixr 6 index as !!
diff --git a/src/Data/FastVect/Sparse/Write.purs b/src/Data/FastVect/Sparse/Write.purs
index 242dba7..777e384 100644
--- a/src/Data/FastVect/Sparse/Write.purs
+++ b/src/Data/FastVect/Sparse/Write.purs
@@ -49,7 +49,7 @@ newtype Vect ∷ Int → Type → Type
 newtype Vect len elem = Vect (List.List { ix :: Int, elem :: elem })
 
 instance (Show elem, Reflectable len Int) ⇒ Show (Vect len elem) where
-  show (Vect elems) = "Vect.Sparse.Read " <> show (Common.toInt (Common.term ∷ _ len)) <> " " <> show elems
+  show (Vect elems) = "Vect.Sparse.Read " <> show (Common.toInt @len) <> " " <> show elems
 
 data JSSet
 
@@ -85,7 +85,7 @@ instance Apply (Vect len) where
   apply (Vect fab) (Vect a) = Vect $ asListOfTuples (asMap fab <*> asMap a)
 
 instance (Compare len Common.NegOne GT, Reflectable len Int) ⇒ Applicative (Vect len) where
-  pure = replicate (Proxy :: _ len)
+  pure = replicate @len
 
 instance FunctorWithIndex Int (Vect len) where
   mapWithIndex f (Vect xs) = Vect $ map (\{ ix, elem } -> { ix, elem: f ix elem }) xs
@@ -135,10 +135,10 @@ instance TraversableWithIndex Int (Vect len) where
 -- -- | vect ∷ Vect 300 String
 -- -- | vect = replicate (Common.term ∷ _ 300) "a"
 -- -- | ```
-replicate ∷ ∀ len elem. Common.Replicate Vect len elem
-replicate proxy elem = Vect $ (unfoldr (\i@{ ix } -> if ix == terminus then Nothing else Just (i /\ { ix: ix + 1, elem })) { ix: 0, elem })
+replicate ∷ ∀ @len elem. Common.Replicate Vect len elem
+replicate elem = Vect $ (unfoldr (\i@{ ix } -> if ix == terminus then Nothing else Just (i /\ { ix: ix + 1, elem })) { ix: 0, elem })
   where
-  terminus = Common.toInt proxy
+  terminus = Common.toInt @len
 
 -- -- | Creates the empty `Vect`.
 -- -- |
@@ -180,7 +180,7 @@ singleton elem = Vect (pure { ix: 0, elem })
 -- -- | cs = append as bs
 -- -- | ```
 append ∷ ∀ m n m_plus_n elem. Common.Append Vect m n m_plus_n elem
-append (Vect xs) (Vect ys) = Vect (xs <> map (\{ ix, elem } -> { ix: ix + (Common.toInt (Proxy :: _ m)), elem }) ys)
+append (Vect xs) (Vect ys) = Vect (xs <> map (\{ ix, elem } -> { ix: ix + (Common.toInt @m), elem }) ys)
 
 -- -- | Safely drop `m` elements from a `Vect`.
 -- -- | Will result in a compile-time error if you are trying to drop more elements than exist in the vector.
@@ -192,10 +192,10 @@ append (Vect xs) (Vect ys) = Vect (xs <> map (\{ ix, elem } -> { ix: ix + (Commo
 -- -- | newVect ∷ Vect 200 String
 -- -- | newVect = drop (Common.term ∷ _ 100) vect
 -- -- | ```
-drop ∷ ∀ m n m_plus_n elem. Common.Drop Vect m n m_plus_n elem
-drop proxy (Vect xs) = Vect (filterMap (\{ ix, elem } -> if ix >= drops then Just { ix: (ix - drops), elem } else Nothing) $ xs)
+drop ∷ ∀ @m n m_plus_n elem. Common.Drop Vect m n m_plus_n elem
+drop (Vect xs) = Vect (filterMap (\{ ix, elem } -> if ix >= drops then Just { ix: (ix - drops), elem } else Nothing) $ xs)
   where
-  drops = Common.toInt proxy
+  drops = Common.toInt @m
 
 -- -- | Safely take `m` elements from a `Vect`.
 -- -- | Will result in a compile-time error if you are trying to take more elements than exist in the vector.
@@ -207,10 +207,10 @@ drop proxy (Vect xs) = Vect (filterMap (\{ ix, elem } -> if ix >= drops then Jus
 -- -- | newVect ∷ Vect 100 String
 -- -- | newVect = take (Common.term ∷ _ 100) vect
 -- -- | ```
-take ∷ ∀ m n m_plus_n elem. Common.Take Vect m n m_plus_n elem
-take proxy (Vect xs) = Vect (filter (\{ ix } -> ix < takes) $ xs)
+take ∷ ∀ @m n m_plus_n elem. Common.Take Vect m n m_plus_n elem
+take (Vect xs) = Vect (filter (\{ ix } -> ix < takes) $ xs)
   where
-  takes = Common.toInt proxy
+  takes = Common.toInt @m
 
 -- -- | Safely modify element `m` from a `Vect`.
 -- -- |
@@ -221,8 +221,8 @@ take proxy (Vect xs) = Vect (filter (\{ ix } -> ix < takes) $ xs)
 -- -- | newVect ∷ Vect 100 String
 -- -- | newVect = modify (Common.term ∷ _ 100) (append "b") vect
 -- -- | ```
-modify ∷ ∀ m n elem. Common.Modify Vect m n elem
-modify proxy f (Vect xs) = Vect $ asListOfTuples $ Map.update (f >>> Just) (Common.toInt proxy) (asMap xs)
+modify ∷ ∀ @m n elem. Common.Modify Vect m n elem
+modify f (Vect xs) = Vect $ asListOfTuples $ Map.update (f >>> Just) (Common.toInt @m) (asMap xs)
 
 -- -- | Safely set element `m` from a `Vect`.
 -- -- |
@@ -234,11 +234,11 @@ modify proxy f (Vect xs) = Vect $ asListOfTuples $ Map.update (f >>> Just) (Comm
 -- -- | newVect = modify (Common.term ∷ _ 100) "b" vect
 -- -- | `
 
-set ∷ ∀ m n elem. Common.Set Vect m n elem
+set ∷ ∀ @m n elem. Common.Set Vect m n elem
 -- we use cons to represent that this is a newer value
 -- this will often cause a duplicate, but we don't care
 -- as we weed out duplicates during traversals
-set proxy elem (Vect xs) = Vect $ List.Cons { ix: Common.toInt proxy, elem } xs
+set elem (Vect xs) = Vect $ List.Cons { ix: Common.toInt @m, elem } xs
 
 -- -- | Split the `Vect` into two sub vectors `before` and `after`, where before contains up to `m` elements.
 -- -- |
@@ -252,10 +252,10 @@ set proxy elem (Vect xs) = Vect $ List.Cons { ix: Common.toInt proxy, elem } xs
 -- -- |   }
 -- -- | split = splitAt (Common.term ∷ _ 3) vect
 -- -- | ```
-splitAt ∷ ∀ m n m_plus_n elem. Common.SplitAt Vect m n m_plus_n elem
-splitAt proxy (Vect xs) = ((\{ yes, no } -> { before: Vect $ yes, after: Vect $ no }) $ List.partition (\{ ix } -> ix < splits) $ xs)
+splitAt ∷ ∀ @m n m_plus_n elem. Common.SplitAt Vect m n m_plus_n elem
+splitAt (Vect xs) = ((\{ yes, no } -> { before: Vect $ yes, after: Vect $ no }) $ List.partition (\{ ix } -> ix < splits) $ xs)
   where
-  splits = Common.toInt proxy
+  splits = Common.toInt @m
 
 -- -- | Safely access the `n`-th modulo m element of a `Vect`.
 -- -- |
@@ -269,7 +269,7 @@ splitAt proxy (Vect xs) = ((\{ yes, no } -> { before: Vect $ yes, after: Vect $
 indexModulo ∷ ∀ m elem. Common.IndexModuloM Vect m elem
 indexModulo i (Vect xs) = List.findMap (\{ ix, elem } -> if moded == ix then Just elem else Nothing) xs
   where
-  moded = i `mod` Common.toInt (Proxy ∷ _ m)
+  moded = i `mod` Common.toInt @m
 
 -- -- | Safely access the `i`-th element of a `Vect`.
 -- -- |
@@ -280,10 +280,10 @@ indexModulo i (Vect xs) = List.findMap (\{ ix, elem } -> if moded == ix then Jus
 -- -- | elem ∷ String
 -- -- | elem = index (Common.term ∷ _ 299) vect
 -- -- | ```
-index ∷ ∀ m m_minus_one i n elem. Common.IndexM Vect m m_minus_one i n elem
-index proxy (Vect xs) = List.findMap (\{ ix, elem } -> if ixInt == ix then Just elem else Nothing) xs
+index ∷ ∀ m m_minus_one @i n elem. Common.IndexM Vect m m_minus_one i n elem
+index (Vect xs) = List.findMap (\{ ix, elem } -> if ixInt == ix then Just elem else Nothing) xs
   where
-  ixInt = Common.toInt proxy
+  ixInt = Common.toInt @i
 
 -- -- | Safely access the head of a `Vect`.
 -- -- |
@@ -305,16 +305,15 @@ head (Vect xs) = List.findMap (\{ ix, elem } -> if ix == 0 then Just elem else N
 -- -- | fromList (Common.term ∷ _ 4) ["a", "b", "c"] = Nothing
 -- -- | ```
 fromMap
-  ∷ ∀ len elem
+  ∷ ∀ @len elem
   . Reflectable len Int
   ⇒ Compare len Common.NegOne GT
-  ⇒ Proxy len
-  → Map.Map Int elem
+  ⇒ Map.Map Int elem
   → Maybe (Vect len elem)
-fromMap proxy mp
+fromMap mp
   | Just { key } <- Map.findMax mp
-  , key < Common.toInt proxy && key >= 0 = Just (Vect $ asListOfTuples mp)
-fromMap _ _ = Nothing
+  , key < Common.toInt @len && key >= 0 = Just (Vect $ asListOfTuples mp)
+fromMap _ = Nothing
 
 -- -- | Converts the `Vect` to an `List`, effectively dropping the size information.
 toList
@@ -329,11 +328,11 @@ toList (Vect arr) = arr
 cons ∷ ∀ len len_plus_1 elem. Common.Cons Vect len len_plus_1 elem
 cons elem (Vect arr) = Vect (List.Cons { ix: 0, elem } (map (\{ ix, elem: elt } -> { ix: ix + 1, elem: elt }) arr))
 
-snoc ∷ ∀ len len_plus_1 elem. Common.Snoc Vect len len_plus_1 elem
+snoc ∷ ∀ @len len_plus_1 elem. Common.Snoc Vect len len_plus_1 elem
 -- we use cons to represent that this is a newer value
 -- this will often cause a duplicate, but we don't care
 -- as we weed out duplicates during traversals
-snoc (Vect xs) elem = Vect $ List.Cons { ix: Common.toInt (Proxy :: _ len), elem } xs
+snoc (Vect xs) elem = Vect $ List.Cons { ix: Common.toInt @len, elem } xs
 
 infixr 6 cons as :
 infixr 6 index as !!
diff --git a/test/Data/FastVect/FastVectSpec.purs b/test/Data/FastVect/FastVectSpec.purs
index 69b1d91..479c7d2 100644
--- a/test/Data/FastVect/FastVectSpec.purs
+++ b/test/Data/FastVect/FastVectSpec.purs
@@ -23,14 +23,14 @@ spec =
         it "should create a Vect from an Array" do
           let
             actualSuccess ∷ Maybe (FV.Vect 3 String)
-            actualSuccess = FV.fromArray (C.term ∷ _ 3) [ "a", "b", "c" ]
+            actualSuccess = FV.fromArray @3 [ "a", "b", "c" ]
 
             expectedSuccess = FV.append (FV.singleton "a") (FV.append (FV.singleton "b") (FV.singleton "c"))
             actualFail1 ∷ Maybe (FV.Vect 4 String)
-            actualFail1 = FV.fromArray (C.term ∷ _ 4) [ "a", "b", "c" ]
+            actualFail1 = FV.fromArray @4 [ "a", "b", "c" ]
 
             actualFail2 ∷ Maybe (FV.Vect 2 String)
-            actualFail2 = FV.fromArray (C.term ∷ _ 2) [ "a", "b", "c" ]
+            actualFail2 = FV.fromArray @2 [ "a", "b", "c" ]
           actualSuccess `shouldEqual` (Just expectedSuccess)
           actualFail1 `shouldEqual` Nothing
           actualFail2 `shouldEqual` Nothing
@@ -41,34 +41,34 @@ spec =
           (foldl (+) 0 vect) `shouldEqual` 10
           (FV.head vect) `shouldEqual` 1
           --(head empty) `shouldEqual` 1 -- should not compile
-          (FV.index (C.term :: _ 0) vect) `shouldEqual` 1
-          (FV.index (C.term :: _ 3) vect) `shouldEqual` 4
-          (FV.modify (C.term :: _ 3) (add 100) vect) `shouldEqual` (FV.cons 1 $ FV.cons 2 $ FV.cons 3 $ FV.cons 104 FV.empty)
+          (FV.index @0 vect) `shouldEqual` 1
+          (FV.index @3 vect) `shouldEqual` 4
+          (FV.modify @3 (add 100) vect) `shouldEqual` (FV.cons 1 $ FV.cons 2 $ FV.cons 3 $ FV.cons 104 FV.empty)
           --(index (term :: _ 4) vect) `shouldEqual` 1 -- should not compile
 
-          (FV.drop (C.term :: _ 4) vect) `shouldEqual` FV.empty
-          (FV.drop (C.term :: _ 3) vect) `shouldEqual` (FV.singleton 4)
+          (FV.drop @4 vect) `shouldEqual` FV.empty
+          (FV.drop @3 vect) `shouldEqual` (FV.singleton 4)
           --(drop (term :: _ 5) vect) `shouldEqual` (singleton 4) -- should not compile
 
-          (FV.take (C.term :: _ 4) vect) `shouldEqual` vect
-          (FV.take (C.term :: _ 3) vect) `shouldEqual` (FV.cons 1 $ FV.cons 2 $ FV.cons 3 FV.empty)
+          (FV.take @4 vect) `shouldEqual` vect
+          (FV.take @3 vect) `shouldEqual` (FV.cons 1 $ FV.cons 2 $ FV.cons 3 FV.empty)
           --let _ = (take (term :: _ 5) vect) -- should not compile
           pure unit
         it "should adjust an Array to a Vect" do
           let
             expectedPad = [ 0, 0, 0, 0, 0, 0, 0, 1, 2, 3 ]
 
-            actualPad = FV.adjust (C.term ∷ _ 10) 0 [ 1, 2, 3 ]
+            actualPad = FV.adjust @10 0 [ 1, 2, 3 ]
 
             expectedDrop = [ 1, 2, 3 ]
 
-            actualDrop = FV.adjust (C.term ∷ _ 3) 0 [ 0, 0, 0, 0, 1, 2, 3 ]
+            actualDrop = FV.adjust @3 0 [ 0, 0, 0, 0, 1, 2, 3 ]
 
             expectedEqual = [ 1, 2, 3, 4, 5 ]
-            actualEqual = FV.adjust (C.term ∷ _ 5) 0 [ 1, 2, 3, 4, 5 ]
+            actualEqual = FV.adjust @5 0 [ 1, 2, 3, 4, 5 ]
 
             expectedPadM = [ "", "", "", "", "a", "b", "c" ]
-            actualPadM = FV.adjustM (C.term ∷ _ 7) [ "a", "b", "c" ]
+            actualPadM = FV.adjustM @7 [ "a", "b", "c" ]
           (FV.toArray actualPad) `shouldEqual` expectedPad
           (FV.toArray actualDrop) `shouldEqual` expectedDrop
           (FV.toArray actualEqual) `shouldEqual` expectedEqual
@@ -86,14 +86,14 @@ spec =
         it "should create a Vect from an Array" do
           let
             actualSuccess ∷ Maybe (FVR.Vect 3 String)
-            actualSuccess = FVR.fromMap (C.term ∷ _ 3) $ Map.fromFoldable [ 0 /\ "a", 2 /\ "b", 1 /\ "c" ]
+            actualSuccess = FVR.fromMap @3 $ Map.fromFoldable [ 0 /\ "a", 2 /\ "b", 1 /\ "c" ]
 
             expectedSuccess = FVR.append (FVR.singleton "a") (FVR.append (FVR.singleton "c") (FVR.singleton "b"))
             actualFail1 ∷ Maybe (FVR.Vect 4 String)
-            actualFail1 = FVR.fromMap (C.term ∷ _ 4) $ Map.fromFoldable [ 0 /\ "a", 22 /\ "b"]
+            actualFail1 = FVR.fromMap @4 $ Map.fromFoldable [ 0 /\ "a", 22 /\ "b"]
 
             actualFail2 ∷ Maybe (FVR.Vect 2 String)
-            actualFail2 = FVR.fromMap (C.term ∷ _ 2) $ Map.fromFoldable [ 0 /\ "a", 52 /\ "b" ]
+            actualFail2 = FVR.fromMap @2 $ Map.fromFoldable [ 0 /\ "a", 52 /\ "b" ]
           actualSuccess `shouldEqual` (Just expectedSuccess)
           actualFail1 `shouldEqual` Nothing
           actualFail2 `shouldEqual` Nothing
@@ -104,17 +104,17 @@ spec =
           (foldl (+) 0 vect) `shouldEqual` 10
           (FVR.head vect) `shouldEqual` (Just 1)
           --(head empty) `shouldEqual` 1 -- should not compile
-          (FVR.index (C.term :: _ 0) vect) `shouldEqual` (Just 1)
-          (FVR.index (C.term :: _ 3) vect) `shouldEqual` (Just 4)
-          (FVR.modify (C.term :: _ 3) (add 100) vect) `shouldEqual` (FVR.cons 1 $ FVR.cons 2 $ FVR.cons 3 $ FVR.cons 104 FVR.empty)
+          (FVR.index @0 vect) `shouldEqual` (Just 1)
+          (FVR.index @3 vect) `shouldEqual` (Just 4)
+          (FVR.modify @3 (add 100) vect) `shouldEqual` (FVR.cons 1 $ FVR.cons 2 $ FVR.cons 3 $ FVR.cons 104 FVR.empty)
           --(index (term :: _ 4) vect) `shouldEqual` 1 -- should not compile
 
-          (FVR.drop (C.term :: _ 4) vect) `shouldEqual` FVR.empty
-          (FVR.drop (C.term :: _ 3) vect) `shouldEqual` (FVR.singleton 4)
+          (FVR.drop @4 vect) `shouldEqual` FVR.empty
+          (FVR.drop @3 vect) `shouldEqual` (FVR.singleton 4)
           --(drop (term :: _ 5) vect) `shouldEqual` (singleton 4) -- should not compile
 
-          (FVR.take (C.term :: _ 4) vect) `shouldEqual` vect
-          (FVR.take (C.term :: _ 3) vect) `shouldEqual` (FVR.cons 1 $ FVR.cons 2 $ FVR.cons 3 FVR.empty)
+          (FVR.take @4 vect) `shouldEqual` vect
+          (FVR.take @3 vect) `shouldEqual` (FVR.cons 1 $ FVR.cons 2 $ FVR.cons 3 FVR.empty)
           --let _ = (take (term :: _ 5) vect) -- should not compile
           pure unit
         it "should apply" do
@@ -130,14 +130,14 @@ spec =
         it "should create a Vect from an Array" do
           let
             actualSuccess ∷ Maybe (FVW.Vect 3 String)
-            actualSuccess = FVW.fromMap (C.term ∷ _ 3) $ Map.fromFoldable [ 0 /\ "a", 2 /\ "b", 1 /\ "c" ]
+            actualSuccess = FVW.fromMap @3 $ Map.fromFoldable [ 0 /\ "a", 2 /\ "b", 1 /\ "c" ]
 
             expectedSuccess = FVW.append (FVW.singleton "a") (FVW.append (FVW.singleton "c") (FVW.singleton "b"))
             actualFail1 ∷ Maybe (FVW.Vect 4 String)
-            actualFail1 = FVW.fromMap (C.term ∷ _ 4) $ Map.fromFoldable [ 0 /\ "a", 22 /\ "b"]
+            actualFail1 = FVW.fromMap @4 $ Map.fromFoldable [ 0 /\ "a", 22 /\ "b"]
 
             actualFail2 ∷ Maybe (FVW.Vect 2 String)
-            actualFail2 = FVW.fromMap (C.term ∷ _ 2) $ Map.fromFoldable [ 0 /\ "a", 52 /\ "b" ]
+            actualFail2 = FVW.fromMap @2 $ Map.fromFoldable [ 0 /\ "a", 52 /\ "b" ]
           actualSuccess `shouldEqual` (Just expectedSuccess)
           actualFail1 `shouldEqual` Nothing
           actualFail2 `shouldEqual` Nothing
@@ -146,22 +146,22 @@ spec =
           let
             vect = FVW.cons 1 $ FVW.cons 2 $ FVW.cons 3 $ FVW.cons 4 FVW.empty
           (foldl (+) 0 vect) `shouldEqual` 10
-          (foldl (+) 0 (FVW.set (Proxy :: _ 0) 101 vect)) `shouldEqual` 110
+          (foldl (+) 0 (FVW.set @0 101 vect)) `shouldEqual` 110
           (traverse Just vect) `shouldEqual` Just vect
-          (traverse Just $ (FVW.set (Proxy :: _ 0) 101 vect)) `shouldEqual` Just (FVW.set (Proxy :: _ 0) 101 vect)
+          (traverse Just $ (FVW.set @0 101 vect)) `shouldEqual` Just (FVW.set @0 101 vect)
           (FVW.head vect) `shouldEqual` (Just 1)
           --(head empty) `shouldEqual` 1 -- should not compile
-          (FVW.index (C.term :: _ 0) vect) `shouldEqual` (Just 1)
-          (FVW.index (C.term :: _ 3) vect) `shouldEqual` (Just 4)
-          (FVW.modify (C.term :: _ 3) (add 100) vect) `shouldEqual` (FVW.cons 1 $ FVW.cons 2 $ FVW.cons 3 $ FVW.cons 104 FVW.empty)
+          (FVW.index @0 vect) `shouldEqual` (Just 1)
+          (FVW.index @3 vect) `shouldEqual` (Just 4)
+          (FVW.modify @3 (add 100) vect) `shouldEqual` (FVW.cons 1 $ FVW.cons 2 $ FVW.cons 3 $ FVW.cons 104 FVW.empty)
           --(index (term :: _ 4) vect) `shouldEqual` 1 -- should not compile
 
-          (FVW.drop (C.term :: _ 4) vect) `shouldEqual` FVW.empty
-          (FVW.drop (C.term :: _ 3) vect) `shouldEqual` (FVW.singleton 4)
+          (FVW.drop @4 vect) `shouldEqual` FVW.empty
+          (FVW.drop @3 vect) `shouldEqual` (FVW.singleton 4)
           --(drop (term :: _ 5) vect) `shouldEqual` (singleton 4) -- should not compile
 
-          (FVW.take (C.term :: _ 4) vect) `shouldEqual` vect
-          (FVW.take (C.term :: _ 3) vect) `shouldEqual` (FVW.cons 1 $ FVW.cons 2 $ FVW.cons 3 FVW.empty)
+          (FVW.take @4 vect) `shouldEqual` vect
+          (FVW.take @3 vect) `shouldEqual` (FVW.cons 1 $ FVW.cons 2 $ FVW.cons 3 FVW.empty)
           --let _ = (take (term :: _ 5) vect) -- should not compile
           pure unit
         it "should apply" do