From 6a657f27c50b42a06cdee58abaf8acd1e6eec2b3 Mon Sep 17 00:00:00 2001
From: sigma-andex <77549848+sigma-andex@users.noreply.github.com>
Date: Mon, 26 Jun 2023 09:00:44 +0100
Subject: [PATCH 1/2] Switch to VTAs

---
 src/Data/FastVect/Common.purs                 |  98 +++++-
 src/Data/FastVect/FastVect.purs               | 124 +++++--
 src/Data/FastVect/FastVect/Matrix.purs        |  30 +-
 src/Data/FastVect/Sparse/Read.purs            |  52 +--
 src/Data/FastVect/Sparse/Write.purs           |  56 ++--
 test/Data/FastVect/FastVectSpec.purs          | 316 +++++++++---------
 .../FastVect/FastVectSpec/MatrixSpec.purs     | 221 ++++++------
 7 files changed, 527 insertions(+), 370 deletions(-)

diff --git a/src/Data/FastVect/Common.purs b/src/Data/FastVect/Common.purs
index 20bebd0..28316b5 100644
--- a/src/Data/FastVect/Common.purs
+++ b/src/Data/FastVect/Common.purs
@@ -2,30 +2,40 @@ module Data.FastVect.Common
   ( Append
   , Cons
   , Drop
+  , DropP
   , Empty
   , Generate
+  , GenerateP
   , Head
   , HeadM
-  , Last
   , Index
   , IndexM
+  , IndexMP
   , IndexModulo
   , IndexModuloM
+  , IndexP
+  , Last
   , MapWithTerm
   , Modify
+  , ModifyP
   , NegOne
   , One
   , Replicate
+  , ReplicateP
   , Set
+  , SetP
   , Singleton
   , Snoc
   , Sparse
   , SplitAt
+  , SplitAtP
   , Take
+  , TakeP
   , Zero
   , class IsVect
   , term
   , toInt
+  , toIntP
   ) where
 
 import Data.Maybe (Maybe)
@@ -46,8 +56,11 @@ term :: forall (i :: Int). Proxy i
 term = Proxy
 
 -- | Convert a term to an Int
-toInt :: forall (len :: Int). Reflectable len Int => Proxy len -> Int
-toInt = reflectType
+toIntP :: forall (len :: Int). Reflectable len Int => Proxy len -> Int
+toIntP = reflectType
+
+toInt :: forall (@len :: Int). Reflectable len Int => Int
+toInt = reflectType (Proxy :: Proxy len)
 
 -- | Create a `Vect` by replicating `len` times the given element
 -- |
@@ -56,6 +69,12 @@ toInt = reflectType
 -- | vect = replicate (term :: _ 300) "a"
 -- | ```
 type Replicate vect len elem =
+  Compare len NegOne GT
+  => Reflectable len Int
+  => elem
+  -> vect len elem
+
+type ReplicateP vect len elem =
   Compare len NegOne GT
   => Reflectable len Int
   => Proxy len
@@ -122,6 +141,15 @@ type Append vect m n m_plus_n elem =
 -- | ```
 type Drop :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
 type Drop vect m n m_plus_n elem =
+  Add m n m_plus_n
+  => Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => vect m_plus_n elem
+  -> vect n elem
+
+type DropP :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
+type DropP vect m n m_plus_n elem =
   Add m n m_plus_n
   => Reflectable m Int
   => Compare m NegOne GT
@@ -142,6 +170,15 @@ type Drop vect m n m_plus_n elem =
 -- | ```
 type Take :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
 type Take vect m n m_plus_n elem =
+  Add m n m_plus_n
+  => Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => vect m_plus_n elem
+  -> vect m elem
+
+type TakeP :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
+type TakeP vect m n m_plus_n elem =
   Add m n m_plus_n
   => Reflectable m Int
   => Compare m NegOne GT
@@ -160,6 +197,15 @@ type Take vect m n m_plus_n elem =
 -- | newVect = modify (term :: _ 100) (append "b") vect
 -- | ```
 type Modify vect m n elem =
+  Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => Compare m n LT
+  => (elem -> elem)
+  -> vect n elem
+  -> vect n elem
+
+type ModifyP vect m n elem =
   Reflectable m Int
   => Compare m NegOne GT
   => Compare n NegOne GT
@@ -179,6 +225,15 @@ type Modify vect m n elem =
 -- | newVect = modify (term :: _ 100) "b" vect
 -- | `
 type Set vect m n elem =
+  Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => Compare m n LT
+  => elem
+  -> vect n elem
+  -> vect n elem
+
+type SetP vect m n elem =
   Reflectable m Int
   => Compare m NegOne GT
   => Compare n NegOne GT
@@ -202,6 +257,15 @@ type Set vect m n elem =
 -- | ```
 type SplitAt :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
 type SplitAt vect m n m_plus_n elem =
+  Add m n m_plus_n
+  => Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => vect m_plus_n elem
+  -> { before :: vect m elem, after :: vect n elem }
+
+type SplitAtP :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
+type SplitAtP vect m n m_plus_n elem =
   Add m n m_plus_n
   => Reflectable m Int
   => Compare m NegOne GT
@@ -243,6 +307,14 @@ type IndexModuloM vect m elem =
 -- | elem = index (term :: _ 299) vect
 -- | ```
 type Index vect m n elem =
+  Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => Compare m n LT
+  => vect n elem
+  -> elem
+
+type IndexP vect m n elem =
   Reflectable m Int
   => Compare m NegOne GT
   => Compare n NegOne GT
@@ -252,6 +324,14 @@ type Index vect m n elem =
   -> elem
 
 type IndexM vect m n elem =
+  Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => Compare m n LT
+  => vect n elem
+  -> Maybe elem
+
+type IndexMP vect m n elem =
   Reflectable m Int
   => Compare m NegOne GT
   => Compare n NegOne GT
@@ -312,6 +392,18 @@ type Snoc vect len len_plus_1 elem =
   -> vect len_plus_1 elem
 
 type Generate vect m elem =
+  Reflectable m Int
+  => Compare m NegOne GT
+  => ( forall i
+        . Compare i NegOne GT
+       => Compare i m LT
+       => Reflectable i Int
+       => Proxy i
+       -> elem
+     )
+  -> vect m elem
+
+type GenerateP vect m elem =
   Reflectable m Int
   => Compare m NegOne GT
   => Proxy m
diff --git a/src/Data/FastVect/FastVect.purs b/src/Data/FastVect/FastVect.purs
index df2d427..aae79c0 100644
--- a/src/Data/FastVect/FastVect.purs
+++ b/src/Data/FastVect/FastVect.purs
@@ -2,26 +2,36 @@ module Data.FastVect.FastVect
   ( (:)
   , Vect
   , adjust
+  , adjustP
   , adjustM
+  , adjustMP
   , append
   , cons
   , drop
+  , dropP
   , empty
   , fromArray
+  , fromArrayP
   , generate
   , head
-  , last
   , index
   , indexModulo
+  , indexP
+  , last
   , mapWithTerm
   , modify
+  , modifyP
   , reifyVect
   , replicate
+  , replicateP
   , set
+  , setP
   , singleton
   , snoc
   , splitAt
+  , splitAtP
   , take
+  , takeP
   , toArray
   , toNonEmptyArray
   ) where
@@ -60,7 +70,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)
@@ -69,7 +79,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
 
 instance (Compare len Common.NegOne GT, Reflectable len Int) => Bind (Vect len) where
   bind vec f = distribute f <*> vec
@@ -97,10 +107,10 @@ instance (Compare len Common.Zero GT) => Traversable1.Traversable1 (Vect len) wh
 
 instance (Compare len Common.NegOne GT, Reflectable len Int) => Distributive (Vect len) where
   distribute :: forall a g. Functor g => g (Vect len a) -> Vect len (g a)
-  distribute xss = generate (Proxy :: _ len) f
+  distribute xss = generate @len f
     where
     f :: forall i. Compare i Common.NegOne GT => Compare i len LT => Reflectable i Int => Proxy i -> g a
-    f _ = index (Proxy :: _ i) <$> xss
+    f _ = index @i <$> xss
   collect = collectDefault
 
 instance Semigroup a => Semigroup (Vect len a) where
@@ -126,8 +136,11 @@ instance (Compare len Common.NegOne GT, Reflectable len Int, CommutativeRing a)
 -- | vect :: Vect 300 String
 -- | vect = replicate (Common.term :: _ 300) "a"
 -- | ```
-replicate :: forall len elem. Common.Replicate Vect len elem
-replicate proxy elem = Vect $ Array.replicate (Common.toInt proxy) elem
+replicate :: forall @len elem. Common.Replicate Vect len elem
+replicate elem = Vect $ Array.replicate (Common.toInt @len) elem
+
+replicateP :: forall len elem. Common.ReplicateP Vect len elem
+replicateP _ = replicate @len
 
 -- | Creates the empty `Vect`.
 -- |
@@ -172,8 +185,12 @@ append (Vect xs) (Vect ys) = Vect (xs <> ys)
 -- | newVect :: Vect 200 String
 -- | newVect = drop (Common.term :: _ 100) vect
 -- | ```
-drop :: forall m n m_plus_n elem. Common.Drop Vect m n m_plus_n elem
-drop proxy (Vect xs) = Vect (Array.drop (Common.toInt proxy) xs)
+drop :: forall @m n m_plus_n elem. Common.Drop Vect m n m_plus_n elem
+drop (Vect xs) = Vect (Array.drop (Common.toInt @m) xs)
+
+-- | Same as `drop` but takes a `Proxy` instead of a visible type application.
+dropP :: forall m n m_plus_n elem. Common.DropP Vect m n m_plus_n elem
+dropP _ = drop @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.
@@ -185,8 +202,12 @@ drop proxy (Vect xs) = Vect (Array.drop (Common.toInt proxy) xs)
 -- | newVect :: Vect 100 String
 -- | newVect = take (Common.term :: _ 100) vect
 -- | ```
-take :: forall m n m_plus_n elem. Common.Take Vect m n m_plus_n elem
-take proxy (Vect xs) = Vect (Array.take (Common.toInt proxy) xs)
+take :: forall @m n m_plus_n elem. Common.Take Vect m n m_plus_n elem
+take (Vect xs) = Vect (Array.take (Common.toInt @m) xs)
+
+-- | Same as `take` but takes a `Proxy` instead of a visible type application.
+takeP :: forall m n m_plus_n elem. Common.TakeP Vect m n m_plus_n elem
+takeP _ = take @m
 
 foreign import modifyImpl :: forall n elem. Int -> (elem -> elem) -> Vect n elem -> Vect n elem
 
@@ -199,8 +220,12 @@ foreign import modifyImpl :: forall n elem. Int -> (elem -> elem) -> Vect n elem
 -- | newVect :: Vect 100 String
 -- | newVect = modify (Common.term :: _ 100) (append "b") vect
 -- | ```
-modify :: forall m n elem. Common.Modify Vect m n elem
-modify proxy = modifyImpl (Common.toInt proxy)
+modify :: forall @m n elem. Common.Modify Vect m n elem
+modify = modifyImpl (Common.toInt @m)
+
+-- | Same as `modify` but takes a `Proxy` instead of a visible type application.
+modifyP :: forall m n elem. Common.ModifyP Vect m n elem
+modifyP _ = modify @m
 
 -- | Safely set element `m` from a `Vect`.
 -- |
@@ -211,8 +236,11 @@ modify proxy = modifyImpl (Common.toInt proxy)
 -- | newVect :: Vect 100 String
 -- | newVect = modify (Common.term :: _ 100) "b" vect
 -- | `
-set :: forall m n elem. Common.Set Vect m n elem
-set proxy = modify proxy <<< const
+set :: forall @m n elem. Common.Set Vect m n elem
+set = modify @m <<< const
+
+setP :: forall m n elem. Common.SetP Vect m n elem
+setP _ = set @m
 
 -- | Split the `Vect` into two sub vectors `before` and `after`, where before contains up to `m` elements.
 -- |
@@ -226,10 +254,13 @@ set proxy = modify proxy <<< const
 -- |   }
 -- | split = splitAt (Common.term :: _ 3) vect
 -- | ```
-splitAt :: forall 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 :: forall @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 } = Array.splitAt (Common.toInt proxy) xs
+  { before, after } = Array.splitAt (Common.toInt @m) xs
+
+splitAtP :: forall m n m_plus_n elem. Common.SplitAtP Vect m n m_plus_n elem
+splitAtP _ = splitAt @m
 
 -- | Safely access the `n`-th modulo m element of a `Vect`.
 -- |
@@ -241,7 +272,7 @@ splitAt proxy (Vect xs) = { before: Vect before, after: Vect after }
 -- | elem = indexModulo 5352523 vect
 -- | ```
 indexModulo :: forall 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
 
@@ -254,8 +285,12 @@ foreign import indexImpl :: forall m elem. Int -> Vect m elem -> elem
 -- | elem :: String
 -- | elem = index (Common.term :: _ 299) vect
 -- | ```
-index :: forall m n elem. Common.Index Vect m n elem
-index = indexImpl <<< Common.toInt
+index :: forall @m n elem. Common.Index Vect m n elem
+index = Common.toInt @m # indexImpl
+
+-- | Same as `index`, but takes a `Proxy` instead of a visible type application.
+indexP :: forall m n elem. Common.IndexP Vect m n elem
+indexP p = index @m
 
 -- | Safely access the head of a `Vect`.
 -- |
@@ -279,7 +314,7 @@ head = indexImpl 0
 -- | elem = last vect
 -- | ```
 last :: forall m elem. Common.Last Vect m elem
-last = indexImpl $ Common.toInt (Common.term :: _ m) - 1
+last = indexImpl $ Common.toInt @m - 1
 
 -- | Attempt to create a `Vect` of a given size from an `Array`.
 -- |
@@ -289,14 +324,23 @@ last = indexImpl $ Common.toInt (Common.term :: _ m) - 1
 -- | fromArray (Common.term :: _ 4) ["a", "b", "c"] = Nothing
 -- | ```
 fromArray
+  :: forall @len elem
+   . Reflectable len Int
+  => Compare len Common.NegOne GT
+  => Array elem
+  -> Maybe (Vect len elem)
+fromArray array | Array.length array == Common.toInt @len = Just (Vect array)
+fromArray _ = Nothing
+
+-- | Same as `fromArray`, but takes a `Proxy` instead of a visible type application.
+fromArrayP
   :: forall len elem
    . Reflectable len Int
   => Compare len Common.NegOne GT
   => Proxy len
   -> Array elem
   -> Maybe (Vect len elem)
-fromArray proxy array | Array.length array == Common.toInt proxy = Just (Vect array)
-fromArray _ _ = Nothing
+fromArrayP _ = fromArray @len
 
 -- | Converts the `Vect` to an `Array`, effectively dropping the size information.
 toArray
@@ -322,20 +366,38 @@ toNonEmptyArray (Vect arr) = NonEmptyArray arr
 -- | toArray $ adjust (Common.term :: _ 3) 0 [ 0, 0, 0, 0, 1, 2, 3 ] == [ 1, 2, 3 ]
 -- | ```
 adjust
-  :: forall len elem
+  :: forall @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 $ Array.replicate (abs len) elem <> array
   len -> Vect $ Array.drop len array
 
+adjustP
+  :: forall len elem
+   . Reflectable len Int
+  => Compare len Common.NegOne GT
+  => Proxy len
+  -> elem
+  -> Array elem
+  -> Vect len elem
+adjustP _ = adjust @len
+
 -- | Like `adjust` but uses the Moinoid instance of elem to create the elements.
 adjustM
+  :: forall @len elem
+   . Monoid elem
+  => Reflectable len Int
+  => Compare len Common.NegOne GT
+  => Array elem
+  -> Vect len elem
+adjustM = adjust @len mempty
+
+adjustMP
   :: forall len elem
    . Monoid elem
   => Reflectable len Int
@@ -343,7 +405,7 @@ adjustM
   => Proxy len
   -> Array elem
   -> Vect len elem
-adjustM proxy = adjust proxy mempty
+adjustMP _ = adjustM @len
 
 -- | Attaches an element to the front of the `Vect`, creating a new `Vect` with size incremented.
 -- |
@@ -400,8 +462,8 @@ unsafeCoerceTerm _ f i = internal f unit unit { reflectType: \_ -> i } Proxy
   internal = unsafeCoerce
 
 -- | Generate a `Vect` of the given size by applying a function to each type level index.
-generate :: forall len elem. Common.Generate Vect len elem
-generate _ f = Vect $ map (\i -> unsafeCoerceTerm (Proxy :: _ len) f i) $ Array.range 0 (Common.toInt (Proxy :: _ len) - 1)
+generate :: forall @len elem. Common.Generate Vect len elem
+generate f = Vect $ map (\i -> unsafeCoerceTerm (Proxy :: _ len) f i) $ Array.range 0 (Common.toInt @len - 1)
 
 -- | Map a function over a `Vect` with the type level index of each element.
 mapWithTerm :: forall len elem elem'. Common.MapWithTerm Vect len elem elem'
diff --git a/src/Data/FastVect/FastVect/Matrix.purs b/src/Data/FastVect/FastVect/Matrix.purs
index 8d55610..4f0b83d 100644
--- a/src/Data/FastVect/FastVect/Matrix.purs
+++ b/src/Data/FastVect/FastVect/Matrix.purs
@@ -31,6 +31,7 @@ import Prelude
 
 import Control.Apply (lift2)
 import Data.Distributive (class Distributive, collectDefault, distribute)
+import Data.FastVect.Common (NegOne)
 import Data.FastVect.Common as Common
 import Data.FastVect.Common.Matrix as CommonM
 import Data.FastVect.FastVect (Vect)
@@ -45,7 +46,8 @@ import Data.Traversable (class Foldable, class Traversable, foldMap, foldl, fold
 import Data.TraversableWithIndex (class TraversableWithIndex, traverseWithIndex)
 import Data.Tuple (Tuple(..))
 import Prim.Int (class Compare)
-import Prim.Ordering (GT)
+import Prim.Ordering (GT, LT)
+import Type.Proxy (Proxy)
 
 -- | A matrix of elements of type `a`, implemented as a array vector of array vectors.
 -- | The first type argument represents the height of the matrix and the second type argument represents the width.
@@ -125,15 +127,15 @@ instance (Compare h Common.NegOne GT, Reflectable h Int, Compare w Common.NegOne
 
 -- | Safely accesses the `j` -th element of the `i` -th row of `Matrix`.
 index :: forall h w i j elem. CommonM.Index Matrix h w i j elem
-index _ _ (Matrix m) = V.index (Common.term :: _ i) $ V.index (Common.term :: _ j) m
+index _ _ (Matrix m) = V.index @i $ V.index @j m
 
 -- | Create a `Matrix` by replicating the given element.
 replicate :: forall h w a. CommonM.Replicate Matrix h w a
-replicate _ _ a = Matrix $ V.replicate Common.term $ V.replicate Common.term a
+replicate _ _ a = Matrix $ V.replicate @w $ V.replicate @h a
 
 -- | Generate a `Matrix` by applying the given function to each type-level index.
 generate :: forall h w elem. CommonM.Generate Matrix h w elem
-generate _ _ f = Matrix $ V.generate Common.term \j -> V.generate Common.term \i -> f i j
+generate _ _ f = Matrix $ V.generate @w \j -> V.generate @h \i -> f i j
 
 -- | Map a function over the elements of a `Matrix` with its type-level indices.
 mapWithTerm :: forall h w elem elem'. CommonM.MapWithTerm Matrix h w elem elem'
@@ -161,7 +163,7 @@ toVect
    . Compare h Common.NegOne GT
   => Matrix h 1 elem
   -> Vect h elem
-toVect (Matrix m) = V.index (Common.term :: _ 0) m
+toVect (Matrix m) = V.index @0 m
 
 -- | Convert a `Matrix` to a array of arrays.
 toArrayArray
@@ -187,7 +189,7 @@ fromVectArray
   => Reflectable w Int
   => Array (Vect h elem)
   -> Maybe (Matrix h w elem)
-fromVectArray arr = Matrix <$> V.fromArray Common.term arr
+fromVectArray arr = Matrix <$> V.fromArray @w arr
 
 -- | Convert a vector to a nx1 `Matrix`.
 fromVect :: forall h elem. Compare h Common.NegOne GT => Vect h elem -> Matrix h 1 elem
@@ -203,7 +205,7 @@ fromArrayArray
   => Reflectable h Int
   => Array (Array elem)
   -> Maybe (Matrix h w elem)
-fromArrayArray arr = fromVectArray =<< (sequence $ map (V.fromArray Common.term) arr)
+fromArrayArray arr = fromVectArray =<< (sequence $ map (V.fromArray @h) arr)
 
 -- | Create `Matrix` of one element.
 singleton :: forall elem. elem -> Matrix 1 1 elem
@@ -228,11 +230,14 @@ outerProduct = outerMap (*)
 -- | Create Matrix from its diagonal elements.
 diag :: forall h elem. CommonM.Diag Vect Matrix h elem
 diag v = generate Common.term Common.term
-  \i j -> if Common.toInt i == Common.toInt j then V.index i v else zero
+  \i j -> if Common.toIntP i == Common.toIntP j then vIndex i else zero
+  where
+  vIndex :: forall i. Reflectable i Int => Compare i NegOne GT => Compare i h LT => Proxy i -> elem
+  vIndex _ = V.index @i v
 
 -- | Get the diagonal elements of a `Matrix`.
 traced :: forall h elem. CommonM.Traced Vect Matrix h elem
-traced m = V.generate Common.term \i -> index i i m
+traced m = V.generate @h \i -> index i i m
 
 -- | Get sum of diagonal elements of a `Matrix`.
 trace :: forall h elem. CommonM.Trace Matrix h elem
@@ -240,7 +245,10 @@ trace m = sum $ traced m
 
 -- | Transform a `Vector` by a `Matrix`.
 transform :: forall h w elem. CommonM.Transform Vect Matrix h w elem
-transform m v = V.generate Common.term \i -> sum $ V.generate (Common.term :: _ w) \j -> index i j m * V.index j v
+transform m v = V.generate @h \i -> sum $ V.generate @w \j -> index i j m * vIndex j
+  where
+  vIndex :: forall j. Reflectable j Int => Compare j NegOne GT => Compare j w LT => Proxy j -> elem
+  vIndex _ = V.index @j v
 
 -- | Matrix multiplication.
 product :: forall h m w elem. CommonM.Product Matrix h m w elem
@@ -252,7 +260,7 @@ empty = Matrix $ V.empty
 
 -- | Modify the `j` -th element of the `i` -th row of a `Matrix`.
 modify :: forall h w i j elem. CommonM.Modify Matrix h w i j elem
-modify _ _ f (Matrix m) = Matrix $ V.modify (Common.term :: _ j) (V.modify (Common.term :: _ i) f) m
+modify _ _ f (Matrix m) = Matrix $ V.modify @j (V.modify @i f) m
 
 -- | Set the `j` -th element of the `i` -th row of a `Matrix`.
 set :: forall h w i j elem. CommonM.Set Matrix h w i j elem
diff --git a/src/Data/FastVect/Sparse/Read.purs b/src/Data/FastVect/Sparse/Read.purs
index 36c5047..2565c7e 100644
--- a/src/Data/FastVect/Sparse/Read.purs
+++ b/src/Data/FastVect/Sparse/Read.purs
@@ -55,14 +55,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)
@@ -76,10 +76,10 @@ derive newtype instance TraversableWithIndex Int (Vect len)
 -- | vect :: Vect 300 String
 -- | vect = replicate (Common.term :: _ 300) "a"
 -- | ```
-replicate :: forall 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 :: forall @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`.
 -- |
@@ -121,7 +121,7 @@ singleton elem = Vect (Map.singleton 0 elem)
 -- | cs = append as bs
 -- | ```
 append :: forall 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 (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.
@@ -133,10 +133,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 :: forall 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 :: forall @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.
@@ -148,10 +148,10 @@ drop proxy (Vect xs) = Vect ((Map.fromFoldable :: Array _ -> _) $ filterMap (\(i
 -- | newVect :: Vect 100 String
 -- | newVect = take (Common.term :: _ 100) vect
 -- | ```
-take :: forall 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 :: forall @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`.
 -- |
@@ -162,8 +162,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 :: forall m n elem. Common.Modify Vect m n elem
-modify proxy f (Vect xs) = Vect $ Map.update (f >>> Just) (Common.toInt proxy) xs
+modify :: forall @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`.
 -- |
@@ -174,8 +174,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 :: forall 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 :: forall @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.
 -- |
@@ -190,9 +190,9 @@ set proxy a (Vect xs) = Vect $ Map.alter (const (Just a)) (Common.toInt proxy) x
 -- | split = splitAt (Common.term :: _ 3) vect
 -- | ```
 splitAt :: forall 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 (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`.
 -- |
@@ -204,7 +204,7 @@ splitAt proxy (Vect xs) = ((\{ yes, no } -> { before: Vect $ Map.fromFoldable ye
 -- | elem = indexModulo 5352523 vect
 -- | ```
 indexModulo :: forall 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`.
 -- |
@@ -215,8 +215,8 @@ indexModulo i (Vect xs) = Map.lookup (i `mod` Common.toInt (Proxy :: _ m)) xs
 -- | elem :: String
 -- | elem = index (Common.term :: _ 299) vect
 -- | ```
-index :: forall m n elem. Common.IndexM Vect m n elem
-index proxy (Vect xs) = Map.lookup (Common.toInt proxy) xs
+index :: forall @m n elem. Common.IndexM Vect m n elem
+index (Vect xs) = Map.lookup (Common.toInt @m) xs
 
 -- | Safely access the head of a `Vect`.
 -- |
@@ -246,7 +246,7 @@ fromMap
   -> Maybe (Vect len elem)
 fromMap proxy mp
   | Just { key } <- Map.findMax mp
-  , key < Common.toInt proxy && key >= 0 = Just (Vect mp)
+  , key < Common.toInt @len && key >= 0 = Just (Vect mp)
 fromMap _ _ = Nothing
 
 -- | Converts the `Vect` to an `Array`, effectively dropping the size information.
@@ -264,7 +264,7 @@ cons elem (Vect arr) = Vect (Map.insert 0 elem (Map.fromFoldable $ map (first (a
 
 snoc
   :: forall 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 !!
@@ -300,11 +300,11 @@ unsafeCoerceTerm _ f i = internal f unit unit { reflectType: \_ -> i } Proxy
   internal = unsafeCoerce
 
 -- | Generate a `Vect` of the given size by applying a function to each type level index.
-generate :: forall len elem. Common.Generate Vect len elem
-generate _ f = Vect
+generate :: forall @len elem. Common.Generate Vect len elem
+generate f = Vect
   $ Map.fromFoldable
   $ map (\i -> Tuple i (unsafeCoerceTerm (Proxy :: _ len) f i))
-  $ Array.range 0 (Common.toInt (Proxy :: _ len) - 1)
+  $ Array.range 0 (Common.toInt @len - 1)
 
 -- | Map a function over a `Vect` with the type level index of each element.
 mapWithTerm :: forall len elem elem'. Common.MapWithTerm Vect len elem elem'
diff --git a/src/Data/FastVect/Sparse/Write.purs b/src/Data/FastVect/Sparse/Write.purs
index b67aa08..3832d9f 100644
--- a/src/Data/FastVect/Sparse/Write.purs
+++ b/src/Data/FastVect/Sparse/Write.purs
@@ -52,7 +52,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
 
@@ -88,7 +88,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
@@ -138,10 +138,10 @@ instance TraversableWithIndex Int (Vect len) where
 -- | vect :: Vect 300 String
 -- | vect = replicate (Common.term :: _ 300) "a"
 -- | ```
-replicate :: forall 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 :: forall @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`.
 -- |
@@ -183,7 +183,7 @@ singleton elem = Vect (pure { ix: 0, elem })
 -- | cs = append as bs
 -- | ```
 append :: forall 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.
@@ -195,10 +195,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 :: forall 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 :: forall @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.
@@ -210,10 +210,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 :: forall 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 :: forall @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`.
 -- |
@@ -224,8 +224,8 @@ take proxy (Vect xs) = Vect (filter (\{ ix } -> ix < takes) $ xs)
 -- | newVect :: Vect 100 String
 -- | newVect = modify (Common.term :: _ 100) (append "b") vect
 -- | ```
-modify :: forall 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 :: forall @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`.
 -- |
@@ -236,11 +236,11 @@ modify proxy f (Vect xs) = Vect $ asListOfTuples $ Map.update (f >>> Just) (Comm
 -- | newVect :: Vect 100 String
 -- | newVect = modify (Common.term :: _ 100) "b" vect
 -- | ```
-set :: forall m n elem. Common.Set Vect m n elem
+set :: forall @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.
 -- |
@@ -254,10 +254,10 @@ set proxy elem (Vect xs) = Vect $ List.Cons { ix: Common.toInt proxy, elem } xs
 -- |   }
 -- | split = splitAt (Common.term :: _ 3) vect
 -- | ```
-splitAt :: forall 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 :: forall @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`.
 -- |
@@ -271,7 +271,7 @@ splitAt proxy (Vect xs) = ((\{ yes, no } -> { before: Vect $ yes, after: Vect $
 indexModulo :: forall 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`.
 -- |
@@ -282,10 +282,10 @@ indexModulo i (Vect xs) = List.findMap (\{ ix, elem } -> if moded == ix then Jus
 -- | elem :: String
 -- | elem = index (Common.term :: _ 299) vect
 -- | ```
-index :: forall m n elem. Common.IndexM Vect m n elem
-index proxy (Vect xs) = List.findMap (\{ ix, elem } -> if ixInt == ix then Just elem else Nothing) xs
+index :: forall @m n elem. Common.IndexM Vect m 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 @m
 
 -- | Safely access the head of a `Vect`.
 -- |
@@ -315,7 +315,7 @@ fromMap
   -> Maybe (Vect len elem)
 fromMap proxy mp
   | Just { key } <- Map.findMax mp
-  , key < Common.toInt proxy && key >= 0 = Just (Vect $ asListOfTuples mp)
+  , key < Common.toInt @len && key >= 0 = Just (Vect $ asListOfTuples mp)
 fromMap _ _ = Nothing
 
 -- | Converts the `Vect` to an `List`, effectively dropping the size information.
@@ -335,7 +335,7 @@ snoc :: forall 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 !!
@@ -371,10 +371,10 @@ unsafeCoerceTerm _ f i = internal f unit unit { reflectType: \_ -> i } Proxy
   internal = unsafeCoerce
 
 -- | Generate a `Vect` of the given size by applying a function to each type level index.
-generate :: forall len elem. Common.Generate Vect len elem
-generate _ f = Vect
+generate :: forall @len elem. Common.Generate Vect len elem
+generate f = Vect
   $ map (\i -> { ix: i, elem: unsafeCoerceTerm (Proxy :: _ len) f i })
-  $ List.range 0 (Common.toInt (Proxy :: _ len) - 1)
+  $ List.range 0 (Common.toInt @len - 1)
 
 -- | Map a function over a `Vect` with the type level index of each element.
 mapWithTerm :: forall len elem elem'. Common.MapWithTerm Vect len elem elem'
diff --git a/test/Data/FastVect/FastVectSpec.purs b/test/Data/FastVect/FastVectSpec.purs
index e6558ab..faa7d1c 100644
--- a/test/Data/FastVect/FastVectSpec.purs
+++ b/test/Data/FastVect/FastVectSpec.purs
@@ -14,170 +14,166 @@ import Data.Traversable (traverse)
 import Data.Tuple.Nested ((/\))
 import Test.Spec (Spec, describe, it)
 import Test.Spec.Assertions (shouldEqual)
-import Type.Proxy (Proxy(..))
 
 spec :: Spec Unit
 spec =
   describe "FastVect" do
     describe "Data.FastVect.FastVect" do
-      describe "fromArray" do
-        it "should create a Vect from an Array" do
-          let
-            actualSuccess = FV.fromArray (C.term :: _ 3) [ "a", "b", "c" ]
-
-            expectedSuccess = FV.append (FV.singleton "a") (FV.append (FV.singleton "b") (FV.singleton "c"))
-            actualFail1 = FV.fromArray (C.term :: _ 4) [ "a", "b", "c" ]
-
-            actualFail2 = FV.fromArray (C.term :: _ 2) [ "a", "b", "c" ]
-          actualSuccess `shouldEqual` (Just expectedSuccess)
-          actualFail1 `shouldEqual` Nothing
-          actualFail2 `shouldEqual` Nothing
-
-        it "should successfully acccess elements from a Vect" do
-          let
-            vect = FV.cons 1 $ FV.cons 2 $ FV.cons 3 $ FV.cons 4 FV.empty
-          (foldl (+) 0 vect) `shouldEqual` 10
-          (foldl1 (+) vect) `shouldEqual` 10
-          (foldr1 (+) 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)
-          --(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)
-          --(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)
-          --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 ]
-
-            expectedDrop = [ 1, 2, 3 ]
-
-            actualDrop = FV.adjust (C.term :: _ 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 ]
-
-            expectedPadM = [ "", "", "", "", "a", "b", "c" ]
-            actualPadM = FV.adjustM (C.term :: _ 7) [ "a", "b", "c" ]
-          (FV.toArray actualPad) `shouldEqual` expectedPad
-          (FV.toArray actualDrop) `shouldEqual` expectedDrop
-          (FV.toArray actualEqual) `shouldEqual` expectedEqual
-          (FV.toArray actualPadM) `shouldEqual` expectedPadM
-        it "should apply" do
-          let
-            applies = FV.cons (add 1) $ FV.cons (add 42) $ FV.cons (mul 5) $ FV.cons (sub 6) FV.empty
-
-            expectedApplies = FV.cons 6 $ FV.cons 47 $ FV.cons 25 $ FV.cons 1 FV.empty
-            actualApplies = applies <*> pure 5
-
-          actualApplies `shouldEqual` expectedApplies
-
-        it "should be generated" do
-          let
-            generated = FV.generate (C.term :: _ 4) \i -> C.toInt i
-            expectedGenerated = FV.cons 0 $ FV.cons 1 $ FV.cons 2 $ FV.cons 3 FV.empty
-          generated `shouldEqual` expectedGenerated
-
-        it "should be mapped with terms" do
-          let
-            vector = FV.cons 1 $ FV.cons 2 $ FV.cons 3 $ FV.cons 4 FV.empty
-
-            mapped = FV.mapWithTerm (\i a -> C.toInt i + a) vector
-            expectedMapped = FV.cons 1 $ FV.cons 3 $ FV.cons 5 $ FV.cons 7 FV.empty
-
-          mapped `shouldEqual` expectedMapped
+      it "should create a Vect from an Array" do
+        let
+          actualSuccess = FV.fromArray @3 [ "a", "b", "c" ]
+
+          expectedSuccess = FV.append (FV.singleton "a") (FV.append (FV.singleton "b") (FV.singleton "c"))
+          actualFail1 = FV.fromArray @4 [ "a", "b", "c" ]
+
+          actualFail2 = FV.fromArray @2 [ "a", "b", "c" ]
+        actualSuccess `shouldEqual` (Just expectedSuccess)
+        actualFail1 `shouldEqual` Nothing
+        actualFail2 `shouldEqual` Nothing
+
+      it "should successfully acccess elements from a Vect" do
+        let
+          vect = FV.cons 1 $ FV.cons 2 $ FV.cons 3 $ FV.cons 4 FV.empty
+        (foldl (+) 0 vect) `shouldEqual` 10
+        (foldl1 (+) vect) `shouldEqual` 10
+        (foldr1 (+) vect) `shouldEqual` 10
+        (FV.head vect) `shouldEqual` 1
+        --(head empty) `shouldEqual` 1 -- should not compile
+        (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 @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 @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 @10 0 [ 1, 2, 3 ]
+
+          expectedDrop = [ 1, 2, 3 ]
+
+          actualDrop = FV.adjust @3 0 [ 0, 0, 0, 0, 1, 2, 3 ]
+
+          expectedEqual = [ 1, 2, 3, 4, 5 ]
+          actualEqual = FV.adjust @5 0 [ 1, 2, 3, 4, 5 ]
+
+          expectedPadM = [ "", "", "", "", "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
+        (FV.toArray actualPadM) `shouldEqual` expectedPadM
+      it "should apply" do
+        let
+          applies = FV.cons (add 1) $ FV.cons (add 42) $ FV.cons (mul 5) $ FV.cons (sub 6) FV.empty
+
+          expectedApplies = FV.cons 6 $ FV.cons 47 $ FV.cons 25 $ FV.cons 1 FV.empty
+          actualApplies = applies <*> pure 5
+
+        actualApplies `shouldEqual` expectedApplies
+
+      it "should be generated" do
+        let
+          generated = FV.generate @4 \i -> C.toIntP i
+          expectedGenerated = FV.cons 0 $ FV.cons 1 $ FV.cons 2 $ FV.cons 3 FV.empty
+        generated `shouldEqual` expectedGenerated
+
+      it "should be mapped with terms" do
+        let
+          vector = FV.cons 1 $ FV.cons 2 $ FV.cons 3 $ FV.cons 4 FV.empty
+
+          mapped = FV.mapWithTerm (\i a -> C.toIntP i + a) vector
+          expectedMapped = FV.cons 1 $ FV.cons 3 $ FV.cons 5 $ FV.cons 7 FV.empty
+
+        mapped `shouldEqual` expectedMapped
     describe "Data.FastVect.Sparse.Read" do
-      describe "fromArray" do
-        it "should create a Vect from an Array" do
-          let
-            actualSuccess = FVR.fromMap (C.term :: _ 3) $ Map.fromFoldable [ 0 /\ "a", 2 /\ "b", 1 /\ "c" ]
-
-            expectedSuccess = FVR.append (FVR.singleton "a") (FVR.append (FVR.singleton "c") (FVR.singleton "b"))
-            actualFail1 = FVR.fromMap (C.term :: _ 4) $ Map.fromFoldable [ 0 /\ "a", 22 /\ "b" ]
-
-            actualFail2 = FVR.fromMap (C.term :: _ 2) $ Map.fromFoldable [ 0 /\ "a", 52 /\ "b" ]
-          actualSuccess `shouldEqual` (Just expectedSuccess)
-          actualFail1 `shouldEqual` Nothing
-          actualFail2 `shouldEqual` Nothing
-
-        it "should successfully acccess elements from a Vect" do
-          let
-            vect = FVR.cons 1 $ FVR.cons 2 $ FVR.cons 3 $ FVR.cons 4 FVR.empty
-          (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)
-          --(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)
-          --(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)
-          --let _ = (take (term :: _ 5) vect) -- should not compile
-          pure unit
-        it "should apply" do
-          let
-            applies = FVR.cons (add 1) $ FVR.cons (add 42) $ FVR.cons (mul 5) $ FVR.cons (sub 6) FVR.empty
-
-            expectedApplies = FVR.cons 6 $ FVR.cons 47 $ FVR.cons 25 $ FVR.cons 1 FVR.empty
-            actualApplies = applies <*> pure 5
-
-          actualApplies `shouldEqual` expectedApplies
+      it "should create a Vect from an Array" do
+        let
+          actualSuccess = FVR.fromMap (C.term :: _ 3) $ Map.fromFoldable [ 0 /\ "a", 2 /\ "b", 1 /\ "c" ]
+
+          expectedSuccess = FVR.append (FVR.singleton "a") (FVR.append (FVR.singleton "c") (FVR.singleton "b"))
+          actualFail1 = FVR.fromMap (C.term :: _ 4) $ Map.fromFoldable [ 0 /\ "a", 22 /\ "b" ]
+
+          actualFail2 = FVR.fromMap (C.term :: _ 2) $ Map.fromFoldable [ 0 /\ "a", 52 /\ "b" ]
+        actualSuccess `shouldEqual` (Just expectedSuccess)
+        actualFail1 `shouldEqual` Nothing
+        actualFail2 `shouldEqual` Nothing
+
+      it "should successfully acccess elements from a Vect" do
+        let
+          vect = FVR.cons 1 $ FVR.cons 2 $ FVR.cons 3 $ FVR.cons 4 FVR.empty
+        (foldl (+) 0 vect) `shouldEqual` 10
+        (FVR.head vect) `shouldEqual` (Just 1)
+        --(head empty) `shouldEqual` 1 -- should not compile
+        (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 @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 @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
+        let
+          applies = FVR.cons (add 1) $ FVR.cons (add 42) $ FVR.cons (mul 5) $ FVR.cons (sub 6) FVR.empty
+
+          expectedApplies = FVR.cons 6 $ FVR.cons 47 $ FVR.cons 25 $ FVR.cons 1 FVR.empty
+          actualApplies = applies <*> pure 5
+
+        actualApplies `shouldEqual` expectedApplies
     describe "Data.FastVect.Sparse.Write" do
-      describe "fromArray" do
-        it "should create a Vect from an Array" do
-          let
-            actualSuccess = FVW.fromMap (C.term :: _ 3) $ Map.fromFoldable [ 0 /\ "a", 2 /\ "b", 1 /\ "c" ]
-
-            expectedSuccess = FVW.append (FVW.singleton "a") (FVW.append (FVW.singleton "c") (FVW.singleton "b"))
-            actualFail1 = FVW.fromMap (C.term :: _ 4) $ Map.fromFoldable [ 0 /\ "a", 22 /\ "b" ]
-
-            actualFail2 = FVW.fromMap (C.term :: _ 2) $ Map.fromFoldable [ 0 /\ "a", 52 /\ "b" ]
-          actualSuccess `shouldEqual` (Just expectedSuccess)
-          actualFail1 `shouldEqual` Nothing
-          actualFail2 `shouldEqual` Nothing
-
-        it "should successfully acccess elements from a Vect" do
-          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
-          (traverse Just vect) `shouldEqual` Just vect
-          (traverse Just $ (FVW.set (Proxy :: _ 0) 101 vect)) `shouldEqual` Just (FVW.set (Proxy :: _ 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)
-          --(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)
-          --(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)
-          --let _ = (take (term :: _ 5) vect) -- should not compile
-          pure unit
-        it "should apply" do
-          let
-            applies = FVW.cons (add 1) $ FVW.cons (add 42) $ FVW.cons (mul 5) $ FVW.cons (sub 6) FVW.empty
-
-            expectedApplies = FVW.cons 6 $ FVW.cons 47 $ FVW.cons 25 $ FVW.cons 1 FVW.empty
-            actualApplies = applies <*> pure 5
-
-          actualApplies `shouldEqual` expectedApplies
+      it "should create a Vect from an Array" do
+        let
+          actualSuccess = FVW.fromMap (C.term :: _ 3) $ Map.fromFoldable [ 0 /\ "a", 2 /\ "b", 1 /\ "c" ]
+
+          expectedSuccess = FVW.append (FVW.singleton "a") (FVW.append (FVW.singleton "c") (FVW.singleton "b"))
+          actualFail1 = FVW.fromMap (C.term :: _ 4) $ Map.fromFoldable [ 0 /\ "a", 22 /\ "b" ]
+
+          actualFail2 = FVW.fromMap (C.term :: _ 2) $ Map.fromFoldable [ 0 /\ "a", 52 /\ "b" ]
+        actualSuccess `shouldEqual` (Just expectedSuccess)
+        actualFail1 `shouldEqual` Nothing
+        actualFail2 `shouldEqual` Nothing
+
+      it "should successfully acccess elements from a Vect" do
+        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 @0 101 vect)) `shouldEqual` 110
+        (traverse Just vect) `shouldEqual` Just 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 @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 @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 @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
+        let
+          applies = FVW.cons (add 1) $ FVW.cons (add 42) $ FVW.cons (mul 5) $ FVW.cons (sub 6) FVW.empty
+
+          expectedApplies = FVW.cons 6 $ FVW.cons 47 $ FVW.cons 25 $ FVW.cons 1 FVW.empty
+          actualApplies = applies <*> pure 5
+
+        actualApplies `shouldEqual` expectedApplies
diff --git a/test/Data/FastVect/FastVectSpec/MatrixSpec.purs b/test/Data/FastVect/FastVectSpec/MatrixSpec.purs
index eab1d2c..4d81bf6 100644
--- a/test/Data/FastVect/FastVectSpec/MatrixSpec.purs
+++ b/test/Data/FastVect/FastVectSpec/MatrixSpec.purs
@@ -18,158 +18,157 @@ spec :: Spec Unit
 spec =
   describe "FastVect" do
     describe "Data.FastVect.FastVect.Matrix" do
-      describe "fromArray" do
-        it "should create a Matrix from an Array of Array" do
-          let
-            testArr :: Array (Array Int)
-            testArr = [ [ 1, 2, 3 ], [ 4, 5, 6 ] ]
+      it "should create a Matrix from an Array of Array" do
+        let
+          testArr :: Array (Array Int)
+          testArr = [ [ 1, 2, 3 ], [ 4, 5, 6 ] ]
 
-            actualSuccess :: Maybe (FM.Matrix 3 2 Int)
-            actualSuccess = FM.fromArrayArray testArr
+          actualSuccess :: Maybe (FM.Matrix 3 2 Int)
+          actualSuccess = FM.fromArrayArray testArr
 
-            expectedSuccess = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
+          expectedSuccess = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
 
-            actualFail :: Maybe (FM.Matrix 3 3 Int)
-            actualFail = FM.fromArrayArray testArr
+          actualFail :: Maybe (FM.Matrix 3 3 Int)
+          actualFail = FM.fromArrayArray testArr
 
-          actualSuccess `shouldEqual` (Just expectedSuccess)
-          actualFail `shouldEqual` Nothing
+        actualSuccess `shouldEqual` (Just expectedSuccess)
+        actualFail `shouldEqual` Nothing
 
-        it "should successfully acccess elements from a Matrix" do
-          let
-            matrix :: FM.Matrix 3 2 Int
-            matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
-          (foldl (+) 0 matrix) `shouldEqual` 21
-          (foldl1 (+) matrix) `shouldEqual` 21
-          (foldr1 (+) matrix) `shouldEqual` 21
-          (FM.index (C.term :: _ 0) (C.term :: _ 0) matrix) `shouldEqual` 1
-          (FM.index (C.term :: _ 2) (C.term :: _ 1) matrix) `shouldEqual` 6
-          (FM.modify (C.term :: _ 1) (C.term :: _ 1) (add 100) matrix) `shouldEqual` (FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 105 : 6 : FV.empty) : FV.empty)
+      it "should successfully acccess elements from a Matrix" do
+        let
+          matrix :: FM.Matrix 3 2 Int
+          matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
+        (foldl (+) 0 matrix) `shouldEqual` 21
+        (foldl1 (+) matrix) `shouldEqual` 21
+        (foldr1 (+) matrix) `shouldEqual` 21
+        (FM.index (C.term :: _ 0) (C.term :: _ 0) matrix) `shouldEqual` 1
+        (FM.index (C.term :: _ 2) (C.term :: _ 1) matrix) `shouldEqual` 6
+        (FM.modify (C.term :: _ 1) (C.term :: _ 1) (add 100) matrix) `shouldEqual` (FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 105 : 6 : FV.empty) : FV.empty)
 
-        it "should apply" do
-          let
-            applies = FM.Matrix $ (add 1 : add 2 : add 3 : FV.empty) : (add 4 : add 5 : add 6 : FV.empty) : FV.empty
-            matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
+      it "should apply" do
+        let
+          applies = FM.Matrix $ (add 1 : add 2 : add 3 : FV.empty) : (add 4 : add 5 : add 6 : FV.empty) : FV.empty
+          matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
 
-            expectedApplies = FM.Matrix $ (2 : 4 : 6 : FV.empty) : (8 : 10 : 12 : FV.empty) : FV.empty
-            actualApplies = applies <*> matrix
+          expectedApplies = FM.Matrix $ (2 : 4 : 6 : FV.empty) : (8 : 10 : 12 : FV.empty) : FV.empty
+          actualApplies = applies <*> matrix
 
-          actualApplies `shouldEqual` expectedApplies
+        actualApplies `shouldEqual` expectedApplies
 
-        it "should be generated" do
-          let
-            generated = FM.generate (term :: _ 3) (term :: _ 2) \i j -> Common.toInt i + Common.toInt j
-            matrix = FM.Matrix $ (0 : 1 : 2 : FV.empty) : (1 : 2 : 3 : FV.empty) : FV.empty
+      it "should be generated" do
+        let
+          generated = FM.generate (term :: _ 3) (term :: _ 2) \i j -> Common.toIntP i + Common.toIntP j
+          matrix = FM.Matrix $ (0 : 1 : 2 : FV.empty) : (1 : 2 : 3 : FV.empty) : FV.empty
 
-          generated `shouldEqual` matrix
+        generated `shouldEqual` matrix
 
-        it "should be mapped with terms" do
-          let
-            matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
-            mapped = FM.mapWithTerm (\i j x -> Common.toInt i + Common.toInt j + x) matrix
-            expected = FM.Matrix $ (1 : 3 : 5 : FV.empty) : (5 : 7 : 9 : FV.empty) : FV.empty
+      it "should be mapped with terms" do
+        let
+          matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
+          mapped = FM.mapWithTerm (\i j x -> Common.toIntP i + Common.toIntP j + x) matrix
+          expected = FM.Matrix $ (1 : 3 : 5 : FV.empty) : (5 : 7 : 9 : FV.empty) : FV.empty
 
-          mapped `shouldEqual` expected
+        mapped `shouldEqual` expected
 
-        it "should successfully transform" do
-          let
-            matrix :: FM.Matrix 3 2 Int
-            matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
+      it "should successfully transform" do
+        let
+          matrix :: FM.Matrix 3 2 Int
+          matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
 
-            vect :: FV.Vect 2 Int
-            vect = 1 : 2 : FV.empty
+          vect :: FV.Vect 2 Int
+          vect = 1 : 2 : FV.empty
 
-            expectedTransformedVect :: FV.Vect 3 Int
-            expectedTransformedVect = 9 : 12 : 15 : FV.empty
+          expectedTransformedVect :: FV.Vect 3 Int
+          expectedTransformedVect = 9 : 12 : 15 : FV.empty
 
-            actualTransformedVect :: FV.Vect 3 Int
-            actualTransformedVect = FM.transform matrix vect
+          actualTransformedVect :: FV.Vect 3 Int
+          actualTransformedVect = FM.transform matrix vect
 
-          actualTransformedVect `shouldEqual` expectedTransformedVect
+        actualTransformedVect `shouldEqual` expectedTransformedVect
 
-        it "should successfully product" do
-          let
-            matrix :: FM.Matrix 3 2 Int
-            matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
+      it "should successfully product" do
+        let
+          matrix :: FM.Matrix 3 2 Int
+          matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
 
-            matrix2 :: FM.Matrix 2 2 Int
-            matrix2 = FM.Matrix $ (1 : 2 : FV.empty) : (3 : 4 : FV.empty) : FV.empty
+          matrix2 :: FM.Matrix 2 2 Int
+          matrix2 = FM.Matrix $ (1 : 2 : FV.empty) : (3 : 4 : FV.empty) : FV.empty
 
-            expectedProductMatrix :: FM.Matrix 3 2 Int
-            expectedProductMatrix = FM.Matrix $ (9 : 12 : 15 : FV.empty) : (19 : 26 : 33 : FV.empty) : FV.empty
+          expectedProductMatrix :: FM.Matrix 3 2 Int
+          expectedProductMatrix = FM.Matrix $ (9 : 12 : 15 : FV.empty) : (19 : 26 : 33 : FV.empty) : FV.empty
 
-            actualProductMatrix :: FM.Matrix 3 2 Int
-            actualProductMatrix = matrix `FM.product` matrix2
+          actualProductMatrix :: FM.Matrix 3 2 Int
+          actualProductMatrix = matrix `FM.product` matrix2
 
-          actualProductMatrix `shouldEqual` expectedProductMatrix
+        actualProductMatrix `shouldEqual` expectedProductMatrix
 
-        it "should successfully transpose" do
-          let
-            matrix :: FM.Matrix 3 2 Int
-            matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
+      it "should successfully transpose" do
+        let
+          matrix :: FM.Matrix 3 2 Int
+          matrix = FM.Matrix $ (1 : 2 : 3 : FV.empty) : (4 : 5 : 6 : FV.empty) : FV.empty
 
-            expectedTransposedMatrix :: FM.Matrix 2 3 Int
-            expectedTransposedMatrix = FM.Matrix $ (1 : 4 : FV.empty) : (2 : 5 : FV.empty) : (3 : 6 : FV.empty) : FV.empty
+          expectedTransposedMatrix :: FM.Matrix 2 3 Int
+          expectedTransposedMatrix = FM.Matrix $ (1 : 4 : FV.empty) : (2 : 5 : FV.empty) : (3 : 6 : FV.empty) : FV.empty
 
-            actualTransposedMatrix :: FM.Matrix 2 3 Int
-            actualTransposedMatrix = FM.transpose matrix
+          actualTransposedMatrix :: FM.Matrix 2 3 Int
+          actualTransposedMatrix = FM.transpose matrix
 
-          actualTransposedMatrix `shouldEqual` expectedTransposedMatrix
+        actualTransposedMatrix `shouldEqual` expectedTransposedMatrix
 
-        it "should successfully trace" do
-          let
-            matrix :: FM.Matrix 2 2 Int
-            matrix = FM.Matrix $ (1 : 2 : FV.empty) : (3 : 4 : FV.empty) : FV.empty
+      it "should successfully trace" do
+        let
+          matrix :: FM.Matrix 2 2 Int
+          matrix = FM.Matrix $ (1 : 2 : FV.empty) : (3 : 4 : FV.empty) : FV.empty
 
-            expectedTracedVector :: FV.Vect 2 Int
-            expectedTracedVector = 1 : 4 : FV.empty
+          expectedTracedVector :: FV.Vect 2 Int
+          expectedTracedVector = 1 : 4 : FV.empty
 
-            actualTracedVector :: FV.Vect 2 Int
-            actualTracedVector = FM.traced matrix
+          actualTracedVector :: FV.Vect 2 Int
+          actualTracedVector = FM.traced matrix
 
-          actualTracedVector `shouldEqual` expectedTracedVector
+        actualTracedVector `shouldEqual` expectedTracedVector
 
-        it "should successfully dot-product" do
-          let
-            vect :: FV.Vect 2 Int
-            vect = 1 : 2 : FV.empty
+      it "should successfully dot-product" do
+        let
+          vect :: FV.Vect 2 Int
+          vect = 1 : 2 : FV.empty
 
-            vect2 :: FV.Vect 2 Int
-            vect2 = 3 : 4 : FV.empty
+          vect2 :: FV.Vect 2 Int
+          vect2 = 3 : 4 : FV.empty
 
-            expectedDotProduct :: Int
-            expectedDotProduct = 11
+          expectedDotProduct :: Int
+          expectedDotProduct = 11
 
-            actualDotProduct :: Int
-            actualDotProduct = FM.dotProduct vect vect2
+          actualDotProduct :: Int
+          actualDotProduct = FM.dotProduct vect vect2
 
-          actualDotProduct `shouldEqual` expectedDotProduct
+        actualDotProduct `shouldEqual` expectedDotProduct
 
-        it "should successfully outer-product" do
-          let
-            vect :: FV.Vect 2 Int
-            vect = 1 : 2 : FV.empty
+      it "should successfully outer-product" do
+        let
+          vect :: FV.Vect 2 Int
+          vect = 1 : 2 : FV.empty
 
-            vect2 :: FV.Vect 2 Int
-            vect2 = 3 : 4 : FV.empty
+          vect2 :: FV.Vect 2 Int
+          vect2 = 3 : 4 : FV.empty
 
-            expectedOuterProduct :: FM.Matrix 2 2 Int
-            expectedOuterProduct = FM.Matrix $ (3 : 6 : FV.empty) : (4 : 8 : FV.empty) : FV.empty
+          expectedOuterProduct :: FM.Matrix 2 2 Int
+          expectedOuterProduct = FM.Matrix $ (3 : 6 : FV.empty) : (4 : 8 : FV.empty) : FV.empty
 
-            actualOuterProduct :: FM.Matrix 2 2 Int
-            actualOuterProduct = FM.outerProduct vect vect2
+          actualOuterProduct :: FM.Matrix 2 2 Int
+          actualOuterProduct = FM.outerProduct vect vect2
 
-          actualOuterProduct `shouldEqual` expectedOuterProduct
+        actualOuterProduct `shouldEqual` expectedOuterProduct
 
-        it "should successfully make diag matrix" do
-          let
-            vect :: FV.Vect 2 Int
-            vect = 1 : 2 : FV.empty
+      it "should successfully make diag matrix" do
+        let
+          vect :: FV.Vect 2 Int
+          vect = 1 : 2 : FV.empty
 
-            expectedDiagMatrix :: FM.Matrix 2 2 Int
-            expectedDiagMatrix = FM.Matrix $ (1 : 0 : FV.empty) : (0 : 2 : FV.empty) : FV.empty
+          expectedDiagMatrix :: FM.Matrix 2 2 Int
+          expectedDiagMatrix = FM.Matrix $ (1 : 0 : FV.empty) : (0 : 2 : FV.empty) : FV.empty
 
-            actualDiagMatrix :: FM.Matrix 2 2 Int
-            actualDiagMatrix = FM.diag vect
+          actualDiagMatrix :: FM.Matrix 2 2 Int
+          actualDiagMatrix = FM.diag vect
 
-          actualDiagMatrix `shouldEqual` expectedDiagMatrix
+        actualDiagMatrix `shouldEqual` expectedDiagMatrix

From 1d4433fb076a9187314ed3b2b22fb6a28a73f236 Mon Sep 17 00:00:00 2001
From: sigma-andex <77549848+sigma-andex@users.noreply.github.com>
Date: Mon, 26 Jun 2023 09:01:43 +0100
Subject: [PATCH 2/2] Update ci

---
 .github/workflows/ci.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index f1edb87..3c003a7 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -13,6 +13,8 @@ jobs:
       - uses: actions/checkout@v2
 
       - uses: purescript-contrib/setup-purescript@main
+        with:
+          purescript: "unstable"
 
       - uses: actions/setup-node@v2
         with: