diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,14 +1,17 @@
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeApplications #-}
 
 module Main where
 --import Data.List.NonEmpty (NonEmpty(..))
 --import qualified Data.List.NonEmpty as N
+import qualified GHC.TypeNats as GN
 import Cybus
 
 main :: IO ()
-main = putStr $ show $ mm @(NN 234)
+main = putStr $ show $ mm @'[2,3,4]
 
 tst1 :: Mat '[4,5,3] Int
 tst1 = gen id
@@ -21,22 +24,42 @@
 
 tst4 :: Mat2 4 7 Int
 tst4 = mat2 @4 @3 [1..] `multMat` mat2 @3 @7 [1..]
+
+tst5 :: Mat (2 ': ns) a -> Mat (1 ': ns) a
+tst5 = deleteRow @2
+
+tst6 :: FinC 1 (1 GN.+ n) => Mat (1 GN.+ n ': ns) a -> Mat (n ': ns) a
+tst6 = deleteRow @1
+
 {-
->tst3 (mm @234)
-Mat@[2]
-[Mat@[3,4]
+>tst3 (mm @'[2,3,4])
+Vec@2 [Mat2@(3,4)
   [
      [1,2,3,4],
      [5,6,7,8],
      [9,10,11,12]
   ]
-,Mat@[3,4]
+,Mat2@(3,4)
   [
      [13,14,15,16],
      [17,18,19,20],
      [21,22,23,24]
   ]
 ]
+it :: Mat '[2] (Mat '[3, 4] Int)
 
-it :: Mat '[2] (Mat '[3,4] Int)
+>tst6 (mm @'[9,3])
+Mat2@(8,3)
+  [
+     [4,5,6],
+     [7,8,9],
+     [10,11,12],
+     [13,14,15],
+     [16,17,18],
+     [19,20,21],
+     [22,23,24],
+     [25,26,27]
+  ]
+
+it :: Mat '[8, 3] Int
 -}
diff --git a/cybus.cabal b/cybus.cabal
--- a/cybus.cabal
+++ b/cybus.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           cybus
-version:        0.2.0.0
+version:        0.3.0.0
 synopsis:       multi-dimensional arrays
 description:    A library for typesafe multi-dimensional arrays . Please see the README on GitHub at <https://github.com/gbwey/cybus#readme>
 category:       Data, Containers
@@ -41,8 +41,8 @@
     , distributive
     , indexed-traversable
     , mtl
-    , pos >=0.2.0.0
-    , primus >=0.2.0.0
+    , pos >=0.3.0.0
+    , primus >=0.3.0.0
     , profunctors
     , semigroupoids
     , these
@@ -65,8 +65,8 @@
     , distributive
     , indexed-traversable
     , mtl
-    , pos >=0.2.0.0
-    , primus >=0.2.0.0
+    , pos >=0.3.0.0
+    , primus >=0.3.0.0
     , profunctors
     , semigroupoids
     , these
@@ -99,9 +99,8 @@
     , indexed-traversable
     , lens
     , mtl
-    , pos >=0.2.0.0
-    , pretty-simple
-    , primus >=0.2.0.0
+    , pos >=0.3.0.0
+    , primus >=0.3.0.0
     , profunctors
     , semigroupoids
     , tasty
diff --git a/src/Cybus/Fin.hs b/src/Cybus/Fin.hs
--- a/src/Cybus/Fin.hs
+++ b/src/Cybus/Fin.hs
@@ -32,9 +32,8 @@
   fnN,
   pattern Fin,
   pattern FinU,
-  FinT,
-  FinWithMessageT,
-  finC,
+  FinC (..),
+  FinWithMessageC,
 
   -- * read/show methods
   showFin,
@@ -113,17 +112,17 @@
 
 {-# COMPLETE FinU #-}
 
--- | pattern synonym for validating the fin before construction with a PosT constraint for validating at the typelevel
+-- | pattern synonym for validating the fin before construction with a PosC constraint for validating at the typelevel
 pattern FinU ::
   forall (n :: Nat).
-  (HasCallStack, PosT n) =>
+  (HasCallStack, PosC n) =>
   Pos ->
   Pos ->
   Fin n
 pattern FinU i n <-
   Fin' i n
   where
-    FinU = frp .@ mkFinC -- dont change this: frp is good else breaking the system
+    FinU = frp .@ mkFinC
 
 -- | create a 'Fin' value level "i" and "n" values and validate that "i" is in range
 mkFin :: Pos -> Pos -> Either String (Fin n)
@@ -133,7 +132,7 @@
     else Left $ show p ++ " is too large: maximum is " ++ show n
 
 -- | create a 'Fin' value level "i" and "n" values and validate against expected "n"
-mkFinC :: forall n. PosT n => Pos -> Pos -> Either String (Fin n)
+mkFinC :: forall n. PosC n => Pos -> Pos -> Either String (Fin n)
 mkFinC p n = do
   let n' = fromNP @n
   if n == n'
@@ -141,21 +140,21 @@
     else Left $ "mkFinC: " ++ show n ++ " /= " ++ show n' ++ " at typelevel"
 
 -- | convenience function for conversion from 'Int' to 'Fin'
-fin :: PosT n => Int -> Either String (Fin n)
+fin :: PosC n => Int -> Either String (Fin n)
 fin = finP <=< eitherPos
 
 -- | convenience function for conversion from 'Pos' to 'Fin'
-finP :: forall n. PosT n => Pos -> Either String (Fin n)
+finP :: forall n. PosC n => Pos -> Either String (Fin n)
 finP = flip mkFinC (fromNP @n)
 
-instance PosT n => Monoid (Fin n) where
+instance PosC n => Monoid (Fin n) where
   mempty = minBound
 
 instance Semigroup (Fin n) where
   (<>) = max
 
--- PosT only needed for fromInteger
-instance PosT n => Num (Fin n) where
+-- PosC only needed for fromInteger
+instance PosC n => Num (Fin n) where
   (+) = forceRight "(+)" .@ withOp2 (+)
   (-) = forceRight "(-)" .@ withOp2 (-)
   (*) = forceRight "(*)" .@ withOp2 (*)
@@ -167,18 +166,18 @@
     k <- eitherPos ii
     mkFinC k (fromNP @n)
 
-instance PosT n => Num1 (Fin n) where
+instance PosC n => Num1 (Fin n) where
   signum1 = fmap signum -- have to override as 1 is Fin 2 (there is no zero)
 
-instance PosT n => Enum (Fin n) where
+instance PosC n => Enum (Fin n) where
   toEnum i = forceRight "Enum(Fin n):toEnum" $ do
     p <- eitherPos (i + 1)
     mkFinC p (fromNP @n)
-  fromEnum = subtract 1 . unP . fnPos -- todo: ok subtract one could be a problem
+  fromEnum = subtract 1 . unP . fnPos
   enumFrom = boundedEnumFrom
   enumFromThen = boundedEnumFromThen
 
-instance PosT n => Bounded (Fin n) where
+instance PosC n => Bounded (Fin n) where
   minBound = FinU _1P (fromNP @n)
   maxBound = FinU (fromNP @n) (fromNP @n)
 
@@ -186,15 +185,15 @@
 showFin :: Fin n -> String
 showFin (Fin (Pos i) (Pos n)) = "Fin" ++ show (i, n)
 
-instance PosT n => Read (Fin n) where
+instance PosC n => Read (Fin n) where
   readPrec = PC.readP_to_Prec (const readFinP)
 
 -- | reader for 'Fin'
-readFin :: PosT n => ReadS (Fin n)
+readFin :: PosC n => ReadS (Fin n)
 readFin = P.readP_to_S readFinP
 
 -- | reader for 'showFin'
-readFinP :: forall n. PosT n => P.ReadP (Fin n)
+readFinP :: forall n. PosC n => P.ReadP (Fin n)
 readFinP = do
   P.skipSpaces
   (i, n) <- P.between (P.string "Fin(") (P.string ")") ((,) <$> pPosInt <* P.char ',' <*> pPosInt)
@@ -203,94 +202,96 @@
 instance Show (Fin n) where
   show = showFin
 
--- | create a 'Fin' using typelevel "i" and "n" Nat
-finC :: forall (i :: Nat) (n :: Nat). FinT i n => Fin n
-finC = Fin' (fromNP @i) (fromNP @n)
+-- | class for constraining "i" to positive numbers less than or equal to "n"
+type FinC :: Nat -> Nat -> Constraint
+class (PosC i, PosC n) => FinC i n where
+  finC :: Fin n
 
--- | type constraint for restricting a 'Nat' to positive numbers
-type FinT :: Nat -> Nat -> Constraint
-type FinT i n = (i <=! n, PosT n)
+instance (PosC n, i <=! n) => FinC i n where
+  finC = Fin' (fromNP @i) (fromNP @n)
 
--- | type constraint for restricting a 'Nat' to positive numbers with a custom error message
-type FinWithMessageT :: GL.ErrorMessage -> Nat -> Nat -> Constraint
-type FinWithMessageT msg i n = (LTEQT msg i n, PosT n)
+-- | class for constraining "i" to positive numbers less than or equal to "n" with a custom error message
+type FinWithMessageC :: GL.ErrorMessage -> Nat -> Nat -> Constraint
+class FinWithMessageC msg i n
 
+instance LTEQT msg i n => FinWithMessageC msg i n
+
 -- | type synonym for index 1
-_F1 :: FinT 1 n => Fin n
+_F1 :: FinC 1 n => Fin n
 _F1 = finC @1
 
 -- | type synonym for index 2
-_F2 :: FinT 2 n => Fin n
+_F2 :: FinC 2 n => Fin n
 _F2 = finC @2
 
 -- | type synonym for index 3
-_F3 :: FinT 3 n => Fin n
+_F3 :: FinC 3 n => Fin n
 _F3 = finC @3
 
 -- | type synonym for index 4
-_F4 :: FinT 4 n => Fin n
+_F4 :: FinC 4 n => Fin n
 _F4 = finC @4
 
 -- | type synonym for index 5
-_F5 :: FinT 5 n => Fin n
+_F5 :: FinC 5 n => Fin n
 _F5 = finC @5
 
 -- | type synonym for index 6
-_F6 :: FinT 6 n => Fin n
+_F6 :: FinC 6 n => Fin n
 _F6 = finC @6
 
 -- | type synonym for index 7
-_F7 :: FinT 7 n => Fin n
+_F7 :: FinC 7 n => Fin n
 _F7 = finC @7
 
 -- | type synonym for index 8
-_F8 :: FinT 8 n => Fin n
+_F8 :: FinC 8 n => Fin n
 _F8 = finC @8
 
 -- | type synonym for index 9
-_F9 :: FinT 9 n => Fin n
+_F9 :: FinC 9 n => Fin n
 _F9 = finC @9
 
 -- | type synonym for index 10
-_F10 :: FinT 10 n => Fin n
+_F10 :: FinC 10 n => Fin n
 _F10 = finC @10
 
 -- | type synonym for index 11
-_F11 :: FinT 11 n => Fin n
+_F11 :: FinC 11 n => Fin n
 _F11 = finC @11
 
 -- | type synonym for index 12
-_F12 :: FinT 12 n => Fin n
+_F12 :: FinC 12 n => Fin n
 _F12 = finC @12
 
 -- | type synonym for index 13
-_F13 :: FinT 13 n => Fin n
+_F13 :: FinC 13 n => Fin n
 _F13 = finC @13
 
 -- | type synonym for index 14
-_F14 :: FinT 14 n => Fin n
+_F14 :: FinC 14 n => Fin n
 _F14 = finC @14
 
 -- | type synonym for index 15
-_F15 :: FinT 15 n => Fin n
+_F15 :: FinC 15 n => Fin n
 _F15 = finC @15
 
 -- | type synonym for index 16
-_F16 :: FinT 16 n => Fin n
+_F16 :: FinC 16 n => Fin n
 _F16 = finC @16
 
 -- | type synonym for index 17
-_F17 :: FinT 17 n => Fin n
+_F17 :: FinC 17 n => Fin n
 _F17 = finC @17
 
 -- | type synonym for index 18
-_F18 :: FinT 18 n => Fin n
+_F18 :: FinC 18 n => Fin n
 _F18 = finC @18
 
 -- | type synonym for index 19
-_F19 :: FinT 19 n => Fin n
+_F19 :: FinC 19 n => Fin n
 _F19 = finC @19
 
 -- | type synonym for index 20
-_F20 :: FinT 20 n => Fin n
+_F20 :: FinC 20 n => Fin n
 _F20 = finC @20
diff --git a/src/Cybus/FinMat.hs b/src/Cybus/FinMat.hs
--- a/src/Cybus/FinMat.hs
+++ b/src/Cybus/FinMat.hs
@@ -59,6 +59,7 @@
   finMatFinGet,
 
   -- * lens into the matrix indices
+  _finMatCons,
   _finMatFin,
   _i1,
   _i2,
@@ -134,7 +135,7 @@
 pattern FinMatU i ps <-
   FinMatUnsafe i ps
   where
-    FinMatU = frp .@ mkFinMatC -- dont change this: frp is necessary else breaking the system
+    FinMatU = frp .@ mkFinMatC
 
 -- | create a FinMat value level "i" and "ns" values and validate that "i" is in range
 mkFinMat :: Int -> NonEmpty Pos -> Either String (FinMat ns)
@@ -184,9 +185,9 @@
   FinMatT _is0 _ns0 ind '[] '[] =
     GL.TypeError ( 'GL.Text "FinMatT: empty index 'is' and 'ns' " 'GL.:<>: 'GL.ShowType ind)
   FinMatT _is0 _ns0 ind '[i] '[n] =
-    FinWithMessageT ( 'GL.Text " at index " 'GL.:<>: 'GL.ShowType ind) i n
+    FinWithMessageC ( 'GL.Text " at index " 'GL.:<>: 'GL.ShowType ind) i n
   FinMatT is0 ns0 ind (i ': i' ': is) (n ': n' ': ns) =
-    (FinWithMessageT ( 'GL.Text " at index=" 'GL.:<>: 'GL.ShowType ind) i n, FinMatT is0 ns0 (ind GN.+ 1) (i' ': is) (n' ': ns))
+    (FinWithMessageC ( 'GL.Text " at index=" 'GL.:<>: 'GL.ShowType ind) i n, FinMatT is0 ns0 (ind GN.+ 1) (i' ': is) (n' ': ns))
   FinMatT is0 ns0 _ind (_ ': _ ': _) '[_] =
     GL.TypeError
       ( 'GL.Text "too many indices: length is > length ns:"
@@ -284,7 +285,8 @@
 readFinMatP :: forall ns. NS ns => P.ReadP (FinMat ns)
 readFinMatP = do
   P.skipSpaces
-  (i, ns) <- (,) <$> pInt <* P.char '@' <*> pPositives '{' '}'
+  _ <- P.string "FinMat@"
+  (i, ns) <- (,) <$> pInt <*> pPositives '{' '}'
   either (const P.pfail) pure $ mkFinMatC @ns i ns
 
 neToString :: NonEmpty Pos -> String
@@ -293,12 +295,12 @@
 -- | pretty print FinMat
 showFinMat :: FinMat ns -> String
 showFinMat (FinMat i ns) =
-  show i ++ "@{" ++ neToString ns ++ "}"
+  "FinMat@" ++ show i ++ "{" ++ neToString ns ++ "}"
 
 -- | more detailed pretty print FinMat
 showFinMat' :: forall ns. FinMat ns -> String
 showFinMat' w@(FinMat i ns) =
-  show i ++ "@{" ++ neToString (finMatToNonEmpty w) ++ "|" ++ neToString ns ++ "}"
+  "FinMat@" ++ show i ++ "{" ++ neToString (finMatToNonEmpty w) ++ "|" ++ neToString ns ++ "}"
 
 instance Show (FinMat ns) where
   show = showFinMat
@@ -307,7 +309,7 @@
 type NSRangeC :: Peano -> [Nat] -> Constraint
 class NSRangeC i ns
 
-instance GL.TypeError ('GL.Text "NSRangeC '[]: empty indices") => NSRangeC p '[]
+instance GL.TypeError ( 'GL.Text "NSRangeC '[]: empty indices") => NSRangeC p '[]
 instance NSRangeC ( 'S 'Z) (n ': ns)
 instance NSRangeC ( 'S i) (m ': ns) => NSRangeC ( 'S ( 'S i)) (n ': m ': ns)
 instance
@@ -318,42 +320,50 @@
   GL.TypeError ( 'GL.Text "NSRangeC: zero is not a valid index: index must be one or greater") =>
   NSRangeC 'Z (n ': ns)
 
+-- | iso that conses out the 'Fin' from 'FinMat'
+_finMatCons :: forall n n1 ns . (NS (n1 ': ns), PosC n) => Iso' (FinMat (n ': n1 ': ns)) (Fin n, FinMat (n1 ': ns))
+_finMatCons = iso f g
+  where f (FinMat is (_:|ns)) = forceRightP "_finMatCons lhs" $ do
+           let (a,Pos b) = divModNextP is (productP ns)
+           (,) <$> fin @n (a+1) <*> finMat @(n1 ': ns) (b-1)
+        g (Fin (Pos i) _, FinMat is ns) = forceRightP "_finMatCons rhs" $ finMat @(n ': n1 ': ns) (is + (i-1) * productPInt ns)
+
 -- | a lens for accessing the "i" index in a indices of FinMat
 _finMatFin ::
   forall i n ns.
-  (PosT i, NSRangeC (NatToPeanoT i) ns) =>
+  (PosC i, NSRangeC (NatToPeanoT i) ns) =>
   Lens' (FinMat ns) (Fin n)
 _finMatFin = lens (finMatFinGet @i @n @ns) (finMatFinSet @i @n @ns)
 
 -- | set the 'Fin' at index "i" for the FinMat
 finMatFinSet ::
   forall i n ns.
-  (PosT i, NSRangeC (NatToPeanoT i) ns) =>
+  (PosC i, NSRangeC (NatToPeanoT i) ns) =>
   FinMat ns ->
   Fin n ->
   FinMat ns
-finMatFinSet fm@(FinMat _ ns) (Fin ind _) =
+finMatFinSet fm@(FinMat _ ns) (Fin ind _) = forceRightP "finMatFinSet" $
   let i = fromNP @i
       ps = finMatToNonEmpty fm
    in case setAt1 i ind ps of
-        Nothing -> programmError $ "finMatFinSet: index out of bounds: index is " ++ show i
-        Just ps1 -> frp $ nonEmptyToFinMat' ps1 ns
+        Nothing -> Left $ "index out of bounds: index is " ++ show i
+        Just ps1 -> nonEmptyToFinMat' ps1 ns
 
 {- | get the 'Fin' at index "i" from FinMat
- must rely on FinMat to get "n at index i "which saves us pulling "n" from the typelevel ie we can omit PosT n
+ must rely on FinMat to get "n at index i "which saves us pulling "n" from the typelevel ie we can omit PosC n
 -}
 finMatFinGet ::
   forall i n ns.
-  (PosT i, NSRangeC (NatToPeanoT i) ns) =>
+  (PosC i, NSRangeC (NatToPeanoT i) ns) =>
   FinMat ns ->
   Fin n
-finMatFinGet fm@(FinMat _ ns) =
+finMatFinGet fm@(FinMat _ ns) = forceRightP "finMatFinGet" $
   let i = fromNP @i
       ps = finMatToNonEmpty fm
    in case (at1 i ps, at1 i ns) of
-        (Nothing, _) -> programmError "finMatFinGet: invalid index!"
-        (_, Nothing) -> programmError $ "finMatFinGet: FinMat is corrupt: doesnt have the index at " ++ show i ++ " " ++ show fm
-        (Just p, Just n) -> frp $ mkFin p n
+        (Nothing, _) -> Left "invalid index!"
+        (_, Nothing) -> Left $ "FinMat is corrupt: doesnt have the index at " ++ show i ++ " " ++ show fm
+        (Just p, Just n) -> mkFin p n
 
 -- | lens for index 1
 _i1 :: Lens' (FinMat (n ': ns)) (Fin n)
@@ -394,3 +404,4 @@
 -- | lens for index 10
 _i10 :: Lens' (FinMat (n1 ': n2 ': n3 ': n4 ': n5 ': n6 ': n7 ': n8 ': n9 ': n ': ns)) (Fin n)
 _i10 = _finMatFin @10
+
diff --git a/src/Cybus/Mat.hs b/src/Cybus/Mat.hs
--- a/src/Cybus/Mat.hs
+++ b/src/Cybus/Mat.hs
@@ -20,6 +20,7 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TupleSections #-}
 
 {- |
 Module      : Cybus.Mat
@@ -109,6 +110,10 @@
   cartesian,
   pureMat,
   replicateMat,
+  determinant,
+--  determinantL,
+--  cofactorsL,
+deleteColumnL,
 
   -- * row operations
   deleteRow,
@@ -159,6 +164,8 @@
   concatMat,
   redim,
   reverseDim,
+  rotateLeft,
+  rotateRight,
 
   -- * subset and slicing
   SliceC (..),
@@ -297,6 +304,7 @@
 import Primus.Error
 import Primus.Fold
 import Primus.Lens
+import Primus.List
 import Primus.NonEmpty
 import Primus.Num1
 import Primus.One
@@ -343,7 +351,7 @@
 type Mat6 :: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Type -> Type
 type Mat6 n m p q r s = Mat '[n, m, p, q, r, s]
 
--- | convenient type synonym for specifying the dimensions of a matrix using the 'NN' type family
+-- | convenient type synonym for specifying the dimensions of a matrix using each digit as a dimension
 type MatN :: Nat -> Type -> Type
 type MatN n = Mat (NN n)
 
@@ -369,7 +377,7 @@
 pattern MatIU v ps <-
   MatUnsafe v ps
   where
-    MatIU = frp .@ mkMat -- dont change this: frp is needed
+    MatIU = frp .@ mkMat
 
 {-# COMPLETE MatU #-}
 
@@ -383,7 +391,7 @@
 pattern MatU v ps <-
   MatUnsafe v ps
   where
-    MatU = frp .@ mkMatC -- dont change this: frp is needed
+    MatU = frp .@ mkMatC
 
 instance (Bounded a, Enum a) => Num1 (Mat ns a) where
   fromInteger1 = toEnumTraversable
@@ -425,7 +433,7 @@
    in MatU (V.replicate (productPInt ns) a) ns
 
 -- | creates a matrix of first dimension "n" by replicating the input matrix "n" times
-replicateMat :: forall n n1 ns a. PosT n => Mat (n1 ': ns) a -> Mat (n ': n1 ': ns) a
+replicateMat :: forall n n1 ns a. PosC n => Mat (n1 ': ns) a -> Mat (n ': n1 ': ns) a
 replicateMat (Mat v ns) =
   let n = fromNP @n
    in MatIU (V.concat (replicate (unP n) v)) (n N.<| ns)
@@ -603,11 +611,11 @@
 
 -- | updates a value in a matrix
 updateMat :: (a -> a) -> FinMat ns -> Mat ns a -> Mat ns a
-updateMat f (FinMat i _) (Mat v ps) =
+updateMat f (FinMat i _) (Mat v ps) = forceRightP "updateMat" $ do
   let (v1, v2) = V.splitAt i v
-   in case V.uncons v2 of
-        Just (a, v2') -> MatIU (v1 <> V.cons (f a) v2') ps
-        Nothing -> programmError $ "updateMat: i=" ++ show i
+  case V.uncons v2 of
+        Just (a, v2') -> mkMat (v1 <> V.cons (f a) v2') ps
+        Nothing -> Left $ "i=" ++ show i
 
 -- | cons a value with a 1d matrix
 (.:) :: forall n a a'. a ~ a' => a -> Vec n a' -> Vec (1 GN.+ n) a'
@@ -642,19 +650,19 @@
 se2 (Mat v ps) = MatIU v (_1P N.<| ps)
 
 -- | create a 1d matrix from a list of values
-vec :: forall n a. (HasCallStack, PosT n) => [a] -> Vec n a
+vec :: forall n a. (HasCallStack, PosC n) => [a] -> Vec n a
 vec = mat @'[n]
 
 -- | create a 1d matrix from a list of values with the exact number of elements
-vec' :: forall n a. (HasCallStack, PosT n) => [a] -> Vec n a
+vec' :: forall n a. (HasCallStack, PosC n) => [a] -> Vec n a
 vec' = mat' @'[n]
 
 -- | create a 2d matrix from a list of values
-mat2 :: forall n m a. (HasCallStack, PosT n, PosT m) => [a] -> Mat2 n m a
+mat2 :: forall n m a. (HasCallStack, PosC n, PosC m) => [a] -> Mat2 n m a
 mat2 = mat @'[n, m]
 
 -- | create a 2d matrix from a list of values with the exact number of elements
-mat2' :: forall n m a. (HasCallStack, PosT n, PosT m) => [a] -> Mat2 n m a
+mat2' :: forall n m a. (HasCallStack, PosC n, PosC m) => [a] -> Mat2 n m a
 mat2' = mat' @'[n, m]
 
 -- | map each column
@@ -863,61 +871,65 @@
 instance n ~ n' => SliceC' '[n'] '[n] where
   sliceC' (FinMat i _) (Mat v _) =
     case v V.!? i of
-      Nothing -> programmError $ "sliceC': index " ++ show i ++ " out of bounds"
+      Nothing -> programmError $ "sliceC' '[n] '[n]: index " ++ show i ++ " out of bounds"
       Just a -> a
-  sliceUpdateC' (FinMat i _) (Mat v ps) b =
+  sliceUpdateC' (FinMat i _) (Mat v ps) b = forceRightP "sliceUpdateC' '[n] '[n]" $ do
     let (v1, v2) = V.splitAt i v
-     in case V.uncons v2 of
-          Just (_, v3) -> MatIU (v1 <> V.cons b v3) ps
-          Nothing -> programmError $ "sliceUpdateC': index " ++ show i ++ " out of bounds"
+    case V.uncons v2 of
+          Just (_, v3) -> mkMat (v1 <> V.cons b v3) ps
+          Nothing -> Left $ "index " ++ show i ++ " out of bounds"
 instance n ~ n' => SliceC' '[n'] (n ': m ': ns) where
-  sliceC' (FinMat i _) (Mat v (_ :| ps)) =
+  sliceC' (FinMat i _) (Mat v (_ :| ps)) = forceRightP "sliceC' '[n] (n ': m ': ns)" $ do
     case ps of
-      m : ns ->
+      m : ns -> do
         let ps1 = m :| ns
             len1 = productPInt ps1
-         in MatIU (V.slice (i * len1) len1 v) ps1
-      [] -> programmError $ "sliceC': index " ++ show i ++ ": missing indices"
+        mkMat (V.slice (i * len1) len1 v) ps1
+      [] -> Left $ "index " ++ show i ++ ": missing indices"
 
-  sliceUpdateC' (FinMat i0 _) (Mat v w@(_ :| ps)) b =
+  sliceUpdateC' (FinMat i0 _) (Mat v w@(_ :| ps)) b = forceRightP "sliceUpdateC' '[n] (n ': m ': ns)" $ do
     let len = productPInt ps
         i = i0 + 1
         v1 = V.slice 0 ((i - 1) * len) v
         v2 = V.slice (i * len) (productPInt w - i * len) v
-     in MatIU (v1 <> mVec b <> v2) w
+    mkMat (v1 <> mVec b <> v2) w
 
 instance
   (n ~ n', SliceC' (n1' ': ns') (n1 ': ns)) =>
   SliceC' (n ': n1' ': ns') (n' ': n1 ': ns)
   where
-  sliceC' fm@(FinMat _ (_ :| n1ns')) w@(Mat _ (n :| _)) =
+  sliceC' fm@(FinMat _ (_ :| n1ns')) w@(Mat _ (n :| _)) = forceRightP "sliceC' (n ': n1' ': ns')" $ do
     let x :| xs = finMatToNonEmpty fm
         i = unP x - 1
-     in case (xs, n1ns') of
-          (x1 : x1s, n1 : ns') ->
-            let fn1 = frp $ nonEmptyToFinMat' (x1 :| x1s) (n1 :| ns')
-             in sliceC' @(n1' ': ns') @(n1 ': ns) fn1 (sliceC' @'[n'] @(n ': n1 ': ns) (frp $ mkFinMat i (n :| [])) w)
-          ([], _) -> programmError "sliceC': missing ns' indices"
-          (_, []) -> programmError "sliceC': missing ns indices"
-  sliceUpdateC' fm@(FinMat _ (_ :| n1ns')) (Mat v w@(_ :| ps0)) b =
+    case (xs, n1ns') of
+          (x1 : x1s, n1 : ns') -> do
+            fn1 <- nonEmptyToFinMat' (x1 :| x1s) (n1 :| ns')
+            w1 <- mkFinMat i (n :| [])
+            pure $ sliceC' @(n1' ': ns') @(n1 ': ns) fn1 (sliceC' @'[n'] @(n ': n1 ': ns) w1 w)
+          ([], _) -> Left "missing ns' indices"
+          (_, []) -> Left "missing ns indices"
+  sliceUpdateC' fm@(FinMat _ (_ :| n1ns')) (Mat v w@(_ :| ps0)) b = forceRightP "sliceUpdateC' (n ': n1' ': ns')" $ do
     -- carve out the piece that is to be updated and pass that down then patch it all back together
     let x :| xs = finMatToNonEmpty fm
         i = unP x
-     in case (ps0, xs, n1ns') of
-          (_ : ns, x1 : x1s, n1 : ns') ->
-            let fn1 = frp $ nonEmptyToFinMat' (x1 :| x1s) (n1 :| ns')
-                ps1 = n1 :| ns
+    case (ps0, xs, n1ns') of
+          (_ : ns, x1 : x1s, n1 : ns') -> do
+            fn1 <- nonEmptyToFinMat' (x1 :| x1s) (n1 :| ns')
+            let ps1 = n1 :| ns
                 len = productPInt ps1
                 v1 = V.slice 0 ((i - 1) * len) v
                 v2 = V.slice (i * len) (productPInt w - i * len) v
-                m1 = MatIU (V.slice ((i - 1) * len) len v) ps1
-                mx = sliceUpdateC' @(n1' ': ns') @(n1 ': ns) fn1 m1 b
-             in MatIU (v1 <> mVec mx <> v2) w
-          ([], _, _) -> programmError "sliceUpdateC': missing matrix indices"
-          (_, [], _) -> programmError "sliceUpdateC': missing ns' indices"
-          (_, _, []) -> programmError "sliceUpdateC': missing finmat indices"
+            m1 <- mkMat (V.slice ((i - 1) * len) len v) ps1
+            let mx = sliceUpdateC' @(n1' ': ns') @(n1 ': ns) fn1 m1 b
+            mkMat (v1 <> mVec mx <> v2) w
+          ([], _, _) -> Left "missing matrix indices"
+          (_, [], _) -> Left "missing ns' indices"
+          (_, _, []) -> Left "missing finmat indices"
 
-instance (GL.TypeError ( 'GL.Text "SliceC': too many indices ns': length ns' > length ns")) => SliceC' (n' ': n1' ': ns') '[n] where
+instance
+  GL.TypeError ( 'GL.Text "SliceC': too many indices ns': length ns' > length ns") =>
+  SliceC' (n' ': n1' ': ns') '[n]
+  where
   sliceC' = compileError "sliceC'"
   sliceUpdateC' = compileError "sliceUpdateC'"
 
@@ -999,27 +1011,27 @@
   sliceC = compileError "SliceC:sliceC"
   sliceUpdateC = compileError "SliceC:sliceUpdateC"
 
-instance FinT i n => SliceC '[i] '[n] where
+instance FinC i n => SliceC '[i] '[n] where
   sliceC (Mat v _) =
     let i = fromN @i - 1
      in case v V.!? i of
           Nothing -> programmError $ "sliceC: index " ++ show i ++ " out of bounds"
           Just a -> a
-  sliceUpdateC (Mat v ps) b =
+  sliceUpdateC (Mat v ps) b = forceRightP "sliceC' '[i] '[n]" $ do
     let i = fromN @i - 1
         (v1, v2) = V.splitAt i v
-     in case V.uncons v2 of
-          Just (_, v3) -> MatIU (v1 <> V.cons b v3) ps
-          Nothing -> programmError $ "sliceUpdateC: index " ++ show i ++ " out of bounds"
-instance FinT i n => SliceC '[i] (n ': m ': ns) where
-  sliceC (Mat v (_ :| ps)) =
+    case V.uncons v2 of
+          Just (_, v3) -> mkMat (v1 <> V.cons b v3) ps
+          Nothing -> Left $ "index " ++ show i ++ " out of bounds"
+instance FinC i n => SliceC '[i] (n ': m ': ns) where
+  sliceC (Mat v (_ :| ps)) =  forceRightP "sliceC' '[i] (n ': m ': ns)" $ do
     case ps of
-      m : ns ->
+      m : ns -> do
         let i = fromN @i - 1
             ps1 = m :| ns
             len1 = productPInt ps1
-         in MatIU (V.slice (i * len1) len1 v) ps1
-      [] -> programmError $ "sliceUpdateC: index " ++ show (fromN @i) ++ ": missing indices"
+        mkMat (V.slice (i * len1) len1 v) ps1
+      [] -> Left $ "index " ++ show (fromN @i) ++ ": missing indices"
 
   sliceUpdateC (Mat v w@(_ :| ps)) b =
     let i = fromN @i
@@ -1029,26 +1041,29 @@
      in MatIU (v1 <> mVec b <> v2) w
 
 instance
-  (FinT i n, SliceC (i1 ': is) (n1 ': ns)) =>
+  (FinC i n, SliceC (i1 ': is) (n1 ': ns)) =>
   SliceC (i ': i1 ': is) (n ': n1 ': ns)
   where
   sliceC w =
     sliceC @(i1 ': is) @(n1 ': ns) (sliceC @'[i] @(n ': n1 ': ns) w)
-  sliceUpdateC (Mat v w@(_ :| ps0)) b =
+  sliceUpdateC (Mat v w@(_ :| ps0)) b = forceRightP "sliceUpdateC' (i ': i1 ': is) (n ': m ': ns)" $ do
     -- carve out the piece that is to be updated and pass that down then patch it all back together
     case ps0 of
-      n1 : ns ->
+      n1 : ns -> do
         let i = fromN @i
             ps1 = n1 :| ns
             len = productPInt ps1
             v1 = V.slice 0 ((i - 1) * len) v
             v2 = V.slice (i * len) (productPInt w - i * len) v
-            m1 = MatIU (V.slice ((i - 1) * len) len v) ps1
-            mx = sliceUpdateC @(i1 ': is) @(n1 ': ns) m1 b
-         in MatIU (v1 <> mVec mx <> v2) w
-      [] -> programmError $ "sliceUpdateC: index " ++ show (fromN @i) ++ ": missing indices"
+        m1 <- mkMat (V.slice ((i - 1) * len) len v) ps1
+        let mx = sliceUpdateC @(i1 ': is) @(n1 ': ns) m1 b
+        mkMat (v1 <> mVec mx <> v2) w
+      [] -> Left $ "index " ++ show (fromN @i) ++ ": missing indices"
 
-instance (GL.TypeError ( 'GL.Text "too many indices 'is': length is > length ns")) => SliceC (i ': i1 ': is) '[n] where
+instance
+  GL.TypeError ( 'GL.Text "too many indices 'is': length is > length ns") =>
+  SliceC (i ': i1 ': is) '[n]
+  where
   sliceC = compileError "sliceC (2)"
   sliceUpdateC = compileError "sliceUpdateC (2)"
 
@@ -1062,7 +1077,7 @@
 -- | a lens for acccessing a column
 _col ::
   forall (i :: Nat) n m ns a.
-  (FinT i m) =>
+  (FinC i m) =>
   Lens' (Mat (n ': m ': ns) a) (Mat (n ': ns) a)
 _col = _transposeMat . _row @i
 
@@ -1107,14 +1122,14 @@
   forall n m ns a.
   Mat (n ': m ': ns) a ->
   Vec n (Mat (m ': ns) a)
-rows w@(Mat _ (n :| ps)) =
+rows w@(Mat _ (n :| ps)) = forceRightP "rows" $
   case ps of
-    m : ns ->
-      let zs = frp $ chunkNVMat (unitsF @[] n) (m :| ns) w
-       in MatIU (V.fromList zs) (n :| [])
-    [] -> programmError "rows: missing indices"
+    m : ns -> do
+      zs <- chunkNVMat (unitsF @[] n) (m :| ns) w
+      mkMat (V.fromList zs) (n :| [])
+    [] -> Left "missing indices"
 
--- | unbust from rows @see 'rows'
+-- | unbust from rows see 'rows'
 unrows ::
   forall n m ns a.
   Vec n (Mat (m ': ns) a) ->
@@ -1183,14 +1198,14 @@
   Mat2 n m a ->
   Mat2 m p b ->
   Mat2 n p d
-dot f g w1@(Mat _ (n :| ps1)) w2@(Mat _ (_ :| ps2)) =
+dot f g w1@(Mat _ (n :| ps1)) w2@(Mat _ (_ :| ps2)) = forceRightP "dot" $
   case (ps1, ps2) of
-    ([m], [p]) ->
-      let z1 = frp $ chunkNLen1 n m w1
-          z2 = N.transpose $ frp $ chunkNLen1 m p w2
-          w = liftA2 ((g . frp) .@ zipWithExact f) z1 z2
-       in MatIU (V.fromList $ N.toList w) (n :| [p])
-    o -> programmError $ "dot: missing indices " ++ show o
+    ([m], [p]) -> do
+      z1 <- chunkNLen1 n m w1
+      z2 <- N.transpose <$> chunkNLen1 m p w2
+      w <- sequenceA $ liftA2 (fmap g .@ zipWithExact f) z1 z2
+      mkMat (V.fromList $ N.toList w) (n :| [p])
+    o -> Left $ "missing indices " ++ show o
 
 -- | multiply two matrices together
 multMat ::
@@ -1204,7 +1219,7 @@
 -- | delete a row
 deleteRow ::
   forall (i :: Nat) (n :: Nat) (ns :: [Nat]) a.
-  FinT i (1 GN.+ n) =>
+  FinC i (1 GN.+ n) =>
   Mat (1 GN.+ n ': ns) a ->
   Mat (n ': ns) a
 deleteRow = deleteRow' (finC @i @(1 GN.+ n))
@@ -1215,18 +1230,18 @@
   Fin (1 GN.+ n) ->
   Mat (1 GN.+ n ': ns) a ->
   Mat (n ': ns) a
-deleteRow' (Fin (Pos i) _) (Mat v (sn :| ps)) =
-  let n = frp $ predP sn
-      n1 = productPInt ps
+deleteRow' (Fin (Pos i) _) (Mat v (sn :| ps)) = forceRightP "deleteRow'" $ do
+  n <- predP sn
+  let n1 = productPInt ps
       s = (i - 1) * n1
       v1 = V.slice 0 s v
       v2 = V.slice (s + n1) (productPInt (sn :| ps) - s - n1) v
-   in MatIU (v1 <> v2) (n :| ps)
+  mkMat (v1 <> v2) (n :| ps)
 
 -- | delete a row from a matrix
 insertRow ::
   forall i n m ns a.
-  FinT i (1 GN.+ n) =>
+  FinC i (1 GN.+ n) =>
   Mat (m ': ns) a ->
   Mat (n ': m ': ns) a ->
   Mat (1 GN.+ n ': m ': ns) a
@@ -1248,7 +1263,7 @@
 -- | delete a column from a matrix (2d or higher)
 deleteCol ::
   forall (i :: Nat) (n :: Nat) (n1 :: Nat) ns a.
-  FinT i (1 GN.+ n1) =>
+  FinC i (1 GN.+ n1) =>
   Mat (n ': (1 GN.+ n1) ': ns) a ->
   Mat (n ': n1 ': ns) a
 deleteCol = deleteCol' (finC @i @(1 GN.+ n1))
@@ -1264,7 +1279,7 @@
 -- | insert a column into a mat (2d and above)
 insertCol ::
   forall (i :: Nat) (n :: Nat) (n1 :: Nat) ns a.
-  FinT i (1 GN.+ n1) =>
+  FinC i (1 GN.+ n1) =>
   Mat (n ': ns) a ->
   Mat (n ': n1 ': ns) a ->
   Mat (n ': (1 GN.+ n1) ': ns) a
@@ -1282,7 +1297,7 @@
 -- | swaps mat rows (1d or more)
 swapRow ::
   forall (i :: Nat) (j :: Nat) (n :: Nat) ns a.
-  (FinT i n, FinT j n) =>
+  (FinC i n, FinC j n) =>
   Mat (n ': ns) a ->
   Mat (n ': ns) a
 swapRow = swapRow' (finC @i) (finC @j)
@@ -1312,7 +1327,7 @@
 -- | swaps mat rows (2d or more)
 swapCol ::
   forall (i :: Nat) (j :: Nat) (n :: Nat) (n1 :: Nat) ns a.
-  (FinT i n1, FinT j n1) =>
+  (FinC i n1, FinC j n1) =>
   Mat (n ': n1 ': ns) a ->
   Mat (n ': n1 ': ns) a
 swapCol = swapCol' (finC @i) (finC @j)
@@ -1358,20 +1373,20 @@
   Mat (n ': m ': ns) a ->
   Mat (n ': m' ': ns) a ->
   Mat (n ': (m GN.+ m') ': ns) a
-appendH w@(Mat _ (n :| ps)) w1@(Mat _ (n' :| ps1))
-  | n == n' =
+appendH w@(Mat _ (n :| ps)) w1@(Mat _ (n' :| ps1)) = forceRightP "appendH" $
+  if n == n' then
       case (ps, ps1) of
-        ([], _) -> programmError "appendH:lhs missing indices"
-        (_, []) -> programmError "appendH:rhs missing indices"
+        ([], _) -> Left "lhs missing indices"
+        (_, []) -> Left "rhs missing indices"
         (m : ns, m' : ns')
-          | ns == ns' ->
-              let x1 = frp $ chunkNV (unitsF n) (productP (m :| ns)) (mVec w)
-                  x2 = frp $ chunkNV (unitsF @[] n) (productP (m' :| ns')) (mVec w1)
-                  ret = frp $ zipWithExact (<>) x1 x2
-                  ps2 = n :| ([m +! m'] <> ns)
-               in MatIU (V.concat ret) ps2
-          | otherwise -> programmError $ "appendH:ns/=ns' " ++ show (ns, ns')
-  | otherwise = programmError $ "appendH: n/=n' " ++ show (n, n')
+          | ns == ns' -> do
+              x1 <- chunkNV (unitsF n) (productP (m :| ns)) (mVec w)
+              x2 <- chunkNV (unitsF @[] n) (productP (m' :| ns')) (mVec w1)
+              ret <- zipWithExact (<>) x1 x2
+              let ps2 = n :| ([m +! m'] <> ns)
+              mkMat (V.concat ret) ps2
+          | otherwise -> Left $ "ns/=ns' " ++ show (ns, ns')
+  else Left $ "n/=n' " ++ show (n, n')
 
 -- | return a mat as a permutation of a list (1d only) todo: extend to multidimensions
 permutationsMat :: forall n a. Vec n a -> Mat2 (FacT n) n a
@@ -1440,7 +1455,7 @@
 -- | convert a matrix to a nested tuple
 type MatTupleT :: [Nat] -> Type -> Type
 type family MatTupleT ns a where
-  MatTupleT '[] _ = GL.TypeError ('GL.Text "MatTupleT '[]: undefined for empty indices")
+  MatTupleT '[] _ = GL.TypeError ( 'GL.Text "MatTupleT '[]: undefined for empty indices")
   MatTupleT '[n] a = ListTupleT n a
   MatTupleT (n ': n1 ': ns) a = ListTupleT n (MatTupleT (n1 ': ns) a)
 
@@ -1464,14 +1479,14 @@
     -- | traversal over a well-formed nested tuple
     Traversal (MatTupleT ns a) (MatTupleT ns b) a b
 
-instance GL.TypeError ('GL.Text "MatTupleC '[]: undefined for empty indices") => MatTupleC '[] a where
+instance GL.TypeError ( 'GL.Text "MatTupleC '[]: undefined for empty indices") => MatTupleC '[] a where
   toTupleC = compileError "MatTupleC:toTupleC"
   fromTupleC = compileError "MatTupleC:fromTupleC"
   fmapTupleMatC = compileError "MatTupleC:fmapTupleMatC"
   traversalTupleMatC = compileError "MatTupleC:traversalTupleMatC"
 
 instance ListTupleCInternal n => MatTupleC '[n] a where
-  toTupleC  = toTupleCInternal
+  toTupleC = toTupleCInternal
   fromTupleC = fromTupleCInternal
   fmapTupleMatC = fmapTupleInternal
   traversalTupleMatC = traversalTupleCInternal
@@ -1562,22 +1577,22 @@
 
 -- | transpose a 2d or larger matrix
 transposeMat :: forall n m ns a. Mat (n ': m ': ns) a -> Mat (m ': n ': ns) a
-transposeMat w@(Mat _ (n :| ps)) =
+transposeMat w@(Mat _ (n :| ps)) = forceRightP "transposeMat" $
   case ps of
-    [] -> programmError "transposeMat"
-    m : ns ->
-      let ys = frp $ chunkNLen1 n (productP (m :| ns)) w
-          zs = N.transpose $ N.map (chunksOf1 (productP ns)) ys
-       in MatIU (V.fromList $ N.toList $ sconcat $ sconcat zs) (m :| (n : ns))
+    [] -> Left "transposeMat"
+    m : ns -> do
+      ys <- chunkNLen1 n (productP (m :| ns)) w
+      let zs = N.transpose $ N.map (chunksOf1 (productP ns)) ys
+      mkMat (V.fromList $ N.toList $ sconcat $ sconcat zs) (m :| (n : ns))
 
 -- | validate and convert from a nested list to a matrix
-nestedListToMatValidated :: forall ns x a. (x ~ ListNST ns a, ValidateNestedListC x (ValidateNestedListT x), MatConvertersC ns) => ListNST ns a -> Either String (Mat ns a)
+nestedListToMatValidated :: forall ns a x. (x ~ ListNST ns a, ValidateNestedListC x (ValidateNestedListT x), MatConvertersC ns) => ListNST ns a -> Either String (Mat ns a)
 nestedListToMatValidated w = do
   _ <- validateNestedList w
   nestedListToMatC w
 
 -- | validate and convert from a nested nonempty list to a matrix
-nestedNonEmptyToMatValidated :: forall ns x a. (x ~ NonEmptyNST ns a, ValidateNestedNonEmptyC x (ValidateNestedNonEmptyT x), MatConvertersC ns) => NonEmptyNST ns a -> Either String (Mat ns a)
+nestedNonEmptyToMatValidated :: forall ns a x. (x ~ NonEmptyNST ns a, ValidateNestedNonEmptyC x (ValidateNestedNonEmptyT x), MatConvertersC ns) => NonEmptyNST ns a -> Either String (Mat ns a)
 nestedNonEmptyToMatValidated w = do
   _ <- validateNestedNonEmpty w
   nestedNonEmptyToMatC w
@@ -1602,7 +1617,7 @@
   -- | convert a nested nonempty list to a 'Mat'
   nestedNonEmptyToMatC :: NonEmptyNST ns a -> Either String (Mat ns a)
 
-instance GL.TypeError ('GL.Text "MatConvertersC '[]: undefined for empty indices") => MatConvertersC '[] where
+instance GL.TypeError ( 'GL.Text "MatConvertersC '[]: undefined for empty indices") => MatConvertersC '[] where
   matToNestedVecC = compileError "MatConvertersC"
   nestedVecToMatC = compileError "MatConvertersC"
   matToNestedListC = compileError "MatConvertersC"
@@ -1610,14 +1625,14 @@
   nestedListToMatC = compileError "MatConvertersC"
   nestedNonEmptyToMatC = compileError "MatConvertersC"
 
-instance PosT n => MatConvertersC '[n] where
+instance PosC n => MatConvertersC '[n] where
   matToNestedVecC = id
   nestedVecToMatC = id
   matToNestedListC = toListMat
   matToNestedNonEmptyC = toNonEmptyMat
   nestedListToMatC = matImpl True
   nestedNonEmptyToMatC = matImpl True . N.toList
-instance (PosT n, MatConvertersC (m ': ns)) => MatConvertersC (n ': m ': ns) where
+instance (PosC n, MatConvertersC (m ': ns)) => MatConvertersC (n ': m ': ns) where
   matToNestedVecC lst = fmap matToNestedVecC (rows @n lst)
   nestedVecToMatC lst@(Mat _ (n :| _)) =
     let zs@(Mat _ (m :| ns) :| _) = toNonEmptyMat $ fmap (nestedVecToMatC @(m ': ns)) lst
@@ -1631,7 +1646,7 @@
   nestedNonEmptyToMatC w = nonEmptyMatsToMat =<< traverse (nestedNonEmptyToMatC @(m ': ns)) w
 
 -- | create a matrix of one dimension higher from rows of a sub matrix
-nonEmptyMatsToMat :: forall n m ns a t. (Foldable1 t, PosT n) => t (Mat (m ': ns) a) -> Either String (Mat (n ': m ': ns) a)
+nonEmptyMatsToMat :: forall n m ns a t. (Foldable1 t, PosC n) => t (Mat (m ': ns) a) -> Either String (Mat (n ': m ': ns) a)
 nonEmptyMatsToMat (toNonEmpty -> xs@(Mat _ ps :| _)) = do
   let n = fromNP @n
   ret <- lengthExact1 n xs
@@ -1640,29 +1655,29 @@
 -- | converts mat dimensions to a nested list
 type MatToNestedVecT :: [Nat] -> Type -> Type
 type family MatToNestedVecT ns a where
-  MatToNestedVecT '[] _ = GL.TypeError ('GL.Text "MatToNestedVecT '[]: undefined for empty indices")
+  MatToNestedVecT '[] _ = GL.TypeError ( 'GL.Text "MatToNestedVecT '[]: undefined for empty indices")
   MatToNestedVecT '[n] a = Vec n a
   MatToNestedVecT (n ': n1 ': ns) a = Vec n (MatToNestedVecT (n1 ': ns) a)
 
--- | type synonym for the result of nesting a matrix: @see 'toND'
+-- | type synonym for the result of nesting a matrix: see 'toND'
 type MatToNDT :: Nat -> [Nat] -> Type -> Type
 type MatToNDT i ns a = Mat (MatToMatNTA (NatToPeanoT i) ns) (Mat (MatToMatNTB (NatToPeanoT i) ns) a)
 
 -- | create a nested matrix going "i" levels down: noop is not supported ie 4D matrix to a 4D matrix
 matToNDImpl ::
   forall (i :: Nat) (ns :: [Nat]) a.
-  PosT i =>
+  PosC i =>
   Mat ns a ->
   MatToNDT i ns a
-matToNDImpl w@(Mat _ ps) =
+matToNDImpl w@(Mat _ ps) = forceRightP "matToNDImpl" $
   let i = fromNP @i
       (ps1, bs) = splitAt1 i ps
    in case bs of
-        y : ys ->
+        y : ys -> do
           let ps2 = y :| ys
-              xs = frp $ chunkNVMat (unitsF (productP ps1)) ps2 w
-           in MatIU (V.fromList xs) ps1
-        [] -> programmError "toND:missing indices to the right"
+          xs <- chunkNVMat (unitsF (productP ps1)) ps2 w
+          mkMat (V.fromList xs) ps1
+        [] -> Left "missing indices to the right"
 
 type MatToMatNTA :: Peano -> [Nat] -> [Nat]
 type family MatToMatNTA i ns where
@@ -1686,19 +1701,19 @@
     GL.TypeError ( 'GL.Text "MatToMatNTB: depth is more than the number of indices")
   MatToMatNTB ( 'S ( 'S i)) (_ ': m ': ns) = MatToMatNTB ( 'S i) (m ': ns)
 
--- | create a nd matrix using a Nat @see 'toND
-toND :: forall i ns a. i <=! i => Mat ns a -> MatToNDT i ns a
+-- | create a nd matrix using a Nat see 'toND
+toND :: forall i ns a. PosC i => Mat ns a -> MatToNDT i ns a
 toND = matToNDImpl @i
 
--- | create a nested 1d matrix @see 'toND
+-- | create a nested 1d matrix see 'toND
 toVec :: Mat ns a -> MatToNDT 1 ns a
 toVec = toND @1
 
--- | create a nested 2d matrix @see 'toND
+-- | create a nested 2d matrix see 'toND
 toMat2 :: Mat ns a -> MatToNDT 2 ns a
 toMat2 = toND @2
 
--- | create a nested 3d matrix @see 'toND
+-- | create a nested 3d matrix see 'toND
 toMat3 :: Mat ns a -> MatToNDT 3 ns a
 toMat3 = toND @3
 
@@ -1713,13 +1728,13 @@
 
 -- | gets the diagonal elements of a 2d or greater square matrix: the diagonal of a n * n * ns matrix results in a n * ns matrix
 diagonal :: Mat (n ': n ': ns) a -> Mat (n ': ns) a
-diagonal (Mat v (n :| ps)) =
+diagonal (Mat v (n :| ps)) = forceRightP "diagonal" $
   case ps of
-    _n : ns ->
+    _n : ns -> do
       let len = productPInt ns
           xs = map (\i -> V.slice (i * (unP n + 1) * len) len v) [0 .. unP n - 1]
-       in MatIU (V.concat xs) (n :| ns)
-    [] -> programmError "diagonal: missing indices"
+      mkMat (V.concat xs) (n :| ns)
+    [] -> Left "missing indices"
 
 -- | take a subset of a matrix using the start and end rows
 subsetRows ::
@@ -1727,13 +1742,13 @@
   DiffTC i j n =>
   Mat (n ': ns) a ->
   Mat (DiffT i j n ': ns) a
-subsetRows (Mat v (_ :| ns)) =
+subsetRows (Mat v (_ :| ns)) = forceRightP "subsetRows" $ do
   let i = fromNP @i
       j = fromNP @j
       n1 = (unP i - 1) * productPInt ns
-      n' = frp $ withOp2 ((-) . (+ 1)) j i
-      ps1 = n' :| ns
-   in MatIU (V.slice n1 (productPInt ps1) v) ps1
+  n' <- withOp2 ((-) . (+ 1)) j i
+  let ps1 = n' :| ns
+  mkMat (V.slice n1 (productPInt ps1) v) ps1
 
 -- todo use FinMat versions of subsetRows and subsetCols ie not just typelevel: need typelevel for the count of rows/cols so no point
 
@@ -1764,7 +1779,7 @@
 -- | specialised version of 'readMat' for 'Vec'
 readVec ::
   ( MatConvertersC '[n]
-  , PosT n
+  , PosC n
   , Read [a]
   ) =>
   ReadS (Vec n a)
@@ -1773,8 +1788,8 @@
 -- | specialised version of 'readMat' for 'Mat2'
 readMat2 ::
   ( MatConvertersC '[n, m]
-  , PosT n
-  , PosT m
+  , PosC n
+  , PosC m
   , Read [[a]]
   ) =>
   ReadS (Mat2 n m a)
@@ -1940,105 +1955,105 @@
   _r10 :: Lens' s a
 
 -- | lens into the first row in a 2d or greater matrix
-instance FinT 1 n => Row1 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
+instance FinC 1 n => Row1 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
   _r1 = _row @1
 
 -- |  lens into the first element in a 1d matrix
-instance FinT 1 n => Row1 (Vec n a) a where
+instance FinC 1 n => Row1 (Vec n a) a where
   _r1 = _row @1
 
-instance (FinT 2 n) => Row2 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
+instance FinC 2 n => Row2 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
   _r2 = _row @2
 
-instance (FinT 2 n) => Row2 (Vec n a) a where
+instance FinC 2 n => Row2 (Vec n a) a where
   _r2 = _row @2
 
-instance (FinT 3 n) => Row3 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
+instance FinC 3 n => Row3 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
   _r3 = _row @3
 
-instance (FinT 3 n) => Row3 (Vec n a) a where
+instance FinC 3 n => Row3 (Vec n a) a where
   _r3 = _row @3
 
-instance (FinT 4 n) => Row4 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
+instance FinC 4 n => Row4 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
   _r4 = _row @4
 
-instance (FinT 4 n) => Row4 (Vec n a) a where
+instance FinC 4 n => Row4 (Vec n a) a where
   _r4 = _row @4
 
-instance (FinT 5 n) => Row5 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
+instance FinC 5 n => Row5 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
   _r5 = _row @5
 
-instance (FinT 5 n) => Row5 (Vec n a) a where
+instance FinC 5 n => Row5 (Vec n a) a where
   _r5 = _row @5
 
-instance (FinT 6 n) => Row6 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
+instance FinC 6 n => Row6 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
   _r6 = _row @6
 
-instance (FinT 6 n) => Row6 (Vec n a) a where
+instance FinC 6 n => Row6 (Vec n a) a where
   _r6 = _row @6
 
-instance (FinT 7 n) => Row7 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
+instance FinC 7 n => Row7 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
   _r7 = _row @7
 
-instance (FinT 7 n) => Row7 (Vec n a) a where
+instance FinC 7 n => Row7 (Vec n a) a where
   _r7 = _row @7
 
-instance (FinT 8 n) => Row8 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
+instance FinC 8 n => Row8 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
   _r8 = _row @8
 
-instance (FinT 8 n) => Row8 (Vec n a) a where
+instance FinC 8 n => Row8 (Vec n a) a where
   _r8 = _row @8
 
-instance (FinT 9 n) => Row9 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
+instance FinC 9 n => Row9 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
   _r9 = _row @9
 
-instance (FinT 9 n) => Row9 (Vec n a) a where
+instance FinC 9 n => Row9 (Vec n a) a where
   _r9 = _row @9
 
-instance (FinT 10 n) => Row10 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
+instance FinC 10 n => Row10 (Mat (n ': m ': ns) a) (Mat (m ': ns) a) where
   _r10 = _row @10
 
-instance (FinT 10 n) => Row10 (Vec n a) a where
+instance FinC 10 n => Row10 (Vec n a) a where
   _r10 = _row @10
 
 -- | lens into column 1 of a matrix
-_c1 :: FinT 1 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
+_c1 :: FinC 1 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
 _c1 = _col @1
 
 -- | lens into column 2 of a matrix
-_c2 :: FinT 2 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
+_c2 :: FinC 2 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
 _c2 = _col @2
 
 -- | lens into column 3 of a matrix
-_c3 :: FinT 3 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
+_c3 :: FinC 3 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
 _c3 = _col @3
 
 -- | lens into column 4 of a matrix
-_c4 :: FinT 4 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
+_c4 :: FinC 4 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
 _c4 = _col @4
 
 -- | lens into column 5 of a matrix
-_c5 :: FinT 5 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
+_c5 :: FinC 5 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
 _c5 = _col @5
 
 -- | lens into column 6 of a matrix
-_c6 :: FinT 6 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
+_c6 :: FinC 6 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
 _c6 = _col @6
 
 -- | lens into column 7 of a matrix
-_c7 :: FinT 7 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
+_c7 :: FinC 7 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
 _c7 = _col @7
 
 -- | lens into column 8 of a matrix
-_c8 :: FinT 8 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
+_c8 :: FinC 8 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
 _c8 = _col @8
 
 -- | lens into column 9 of a matrix
-_c9 :: FinT 9 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
+_c9 :: FinC 9 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
 _c9 = _col @9
 
 -- | lens into column 10 of a matrix
-_c10 :: FinT 10 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
+_c10 :: FinC 10 m => Lens' (Mat (n ': (m : ns)) a) (Mat (n ': ns) a)
 _c10 = _col @10
 
 -- | marker representing the last value in a 1d matrix ie singleton
@@ -2099,11 +2114,11 @@
   where
   consMat =
     iso
-      ( \(Mat v0 (sn :| ps)) ->
-          let n = frp $ predP sn
-           in case V.uncons v0 of -- stay within Vector
-                Nothing -> programmError "consMat '[1 GN.+ n]: no data"
-                Just (a, v) -> (a, MatIU v (n :| ps))
+      ( \(Mat v0 (sn :| ps)) -> forceRightP "consMat '[n]" $ do
+          n <- predP sn
+          case V.uncons v0 of -- stay within Vector
+                Nothing -> Left "no data"
+                Just (a, v) -> (a,) <$> mkMat v (n :| ps)
       )
       (\(a, Mat v (p :| ps)) -> MatIU (V.cons a v) (succP p :| ps))
 
@@ -2118,10 +2133,10 @@
   where
   consMat =
     iso
-      ( \(Mat v (_ :| ps)) ->
+      ( \(Mat v (_ :| ps)) -> forceRightP "consMat '(1 ': n1 ': ns)" $
           case ps of
-            m : ns -> (MatIU v (m :| ns), EofN)
-            [] -> programmError "consMat (1 ': m ': ns): missing indices"
+            m : ns -> (,EofN) <$> mkMat v (m :| ns)
+            [] -> Left "missing indices"
       )
       (\(Mat v ps, EofN) -> MatIU v (_1P N.<| ps))
 
@@ -2136,17 +2151,15 @@
   where
   consMat =
     iso
-      ( \(Mat v (sn :| ps)) ->
+      ( \(Mat v (sn :| ps)) -> forceRightP "consMat '(n ': m ': ns)" $ do
           case ps of
-            m : ns ->
-              let n = frp $ predP sn
-                  ps1 = m :| ns
+            m : ns -> do
+              n <- predP sn
+              let ps1 = m :| ns
                   ps2 = n :| (m : ns)
                   (v1, v2) = V.splitAt (productPInt ps1) v
-               in ( MatIU v1 ps1
-                  , MatIU v2 ps2
-                  )
-            [] -> programmError "consMat:(1 GN.+ n ': m ': ns): missing indices"
+              liftA2 (,) (mkMat v1 ps1) (mkMat v2 ps2)
+            [] -> Left "missing indices"
       )
       (\(Mat v1 _, Mat v2 (p2 :| ps2)) -> MatIU (v1 <> v2) (succP p2 :| ps2))
 
@@ -2180,22 +2193,22 @@
   where
   snocMat =
     iso
-      ( \(Mat v0 (sn :| ps)) ->
-          let n = frp $ predP sn
-           in case V.unsnoc v0 of
-                Nothing -> programmError "snocMat '[1 GN.+ n]: no data"
-                Just (v, a) -> (MatIU v (n :| ps), a)
+      ( \(Mat v0 (sn :| ps)) -> forceRightP "snocMat '[n]" $ do
+          n <- predP sn
+          case V.unsnoc v0 of
+                Nothing -> Left "no data"
+                Just (v, a) -> (,a) <$> mkMat v (n :| ps)
       )
       (\(Mat v (p :| ps), a) -> MatIU (V.snoc v a) (succP p :| ps))
 
 instance {-# OVERLAPPING #-} SnocMatC (1 ': n1 ': ns) a b where
   snocMat =
     iso
-      ( \(Mat v (_ :| ps)) ->
+      ( \(Mat v (_ :| ps)) -> forceRightP "snocMat '(1 ': n1 ': ns)" $ do
           case ps of
             m : ns ->
-              (EofN, MatIU v (m :| ns))
-            [] -> programmError "snocMat '[1 GN.+ n]: missing indices"
+              (EofN,) <$> mkMat v (m :| ns)
+            [] -> Left "missing indices"
       )
       (\(EofN, Mat v ps) -> MatIU v (_1P N.<| ps))
 
@@ -2208,17 +2221,15 @@
   where
   snocMat =
     iso
-      ( \(Mat v (sn :| ps)) ->
+      ( \(Mat v (sn :| ps)) -> forceRightP "snocMat '(n ': m ': ns)" $ do
           case ps of
-            m : ns ->
-              let n = frp $ predP sn
-                  ps1 = m :| ns
+            m : ns -> do
+              n <- predP sn
+              let ps1 = m :| ns
                   ps2 = n :| (m : ns)
                   (v2, v1) = V.splitAt (productPInt ps2) v
-               in ( MatIU v2 ps2
-                  , MatIU v1 ps1
-                  )
-            [] -> programmError "snocMat:(1 GN.+ n ': m ': ns): missing indices"
+              liftA2 (,) (mkMat v2 ps2) (mkMat v1 ps1)
+            [] -> Left "missing indices"
       )
       (\(Mat v1 (p1 :| ps1), Mat v2 _) -> MatIU (v1 <> v2) (succP p1 :| ps1))
 
@@ -2233,13 +2244,13 @@
 
 -- | get a row from a matrix using a concrete index see '_row''
 indexRow :: Fin n -> Mat (n ': m ': ns) a -> Mat (m ': ns) a
-indexRow (Fin (Pos i) _n) (Mat v (_ :| ps)) =
+indexRow (Fin (Pos i) _n) (Mat v (_ :| ps)) = forceRightP "indexRow" $
   case ps of
-    m : ns ->
+    m : ns -> do
       let s = (i - 1) * len
           len = productPInt (m :| ns)
-       in MatIU (V.slice s len v) (m :| ns)
-    [] -> programmError "indexRow: missing indices"
+      mkMat (V.slice s len v) (m :| ns)
+    [] -> Left "missing indices"
 
 -- | 'Data.List.scanr' for a vector
 scanrVec :: forall n a b. (a -> b -> b) -> b -> Vec n a -> Vec (n GN.+ 1) b
@@ -2251,14 +2262,14 @@
 scanlVec f c (Mat v (p :| ps)) =
   MatIU (V.scanl' f c v) (succP p :| ps)
 
-{- | @see 'Data.Vector.postscanr''
+{- | see 'Data.Vector.postscanr''
  concrete version of 'Primus.Fold.postscanr
 -}
 postscanrMat :: forall ns a b. (a -> b -> b) -> b -> Mat ns a -> Mat ns b
 postscanrMat f c (Mat v ps) =
   MatIU (V.postscanr' f c v) ps
 
-{- | @see 'Data.Vector.postscanl''
+{- | see 'Data.Vector.postscanl''
  concrete version of 'Primus.Fold.postscanl'
 -}
 postscanlMat :: forall ns a b. (b -> a -> b) -> b -> Mat ns a -> Mat ns b
@@ -2304,3 +2315,54 @@
 -- | matrix of dimension 10
 dim10 :: Mat '[n, m, p, q, r, s, t, u, v, w] a -> Mat '[n, m, p, q, r, s, t, u, v, w] a
 dim10 = id
+
+-- | left rotate a matrix
+rotateLeft :: Mat2 n m a -> Mat2 m n a
+rotateLeft = unrows . sequence1 . fmap reverseT . rows
+
+-- | right rotate a matrix
+rotateRight :: Mat2 n m a -> Mat2 m n a
+rotateRight = unrows . fmap reverseT . sequence1 . rows
+
+cofactorsL :: forall a . Pos -> [a] -> [(a, [a])]
+cofactorsL n xs
+  | n <= _2P = programmError $ "cofactorsL: n is too small: must be greater than 2 but found " ++ show n
+  | len /= len' = programmError $ "cofactorsL: wrong length: expected " ++ show len' ++ " but found " ++ show len
+  | otherwise =
+    let (h,t) = splitAt (unP n) xs
+    in foldl' (\z (i,a) -> (a,deleteColumnL n i t):z) [] (zip [0..] h)
+  where len = length xs
+        len' = unP (n *! n)
+
+-- | delete column "i" from a list of width "n"
+deleteColumnL :: forall a . Pos -> Int -> [a] -> [a]
+deleteColumnL (Pos n) i ys =
+  let (as,bs) = splitAt i ys
+  in as <> concat (L.unfoldr g bs)
+  where
+    g :: [a] -> Maybe ([a],[a])
+    g = list Nothing (\_ -> Just . splitAt (n-1))
+
+determinantL :: forall a . Num a => Pos -> [a] -> a
+determinantL n m0
+  | len /= unP (n *! n) = programmError $ "determinantL: wrong length n=" ++ show n ++ " m=" ++ show len
+  | otherwise =
+  case m0 of
+   [a] -> a
+   [a,b,c,d] -> a * d - b * c
+   _o ->
+    snd $ foldl' f (True, 0) (cofactorsL n m0)
+   where
+    f :: (Bool, a) -> (a, [a]) -> (Bool, a)
+    f (sgn, tot) (a, m) =
+      let val = bool id negate sgn a * determinantL (frp $ predP n) m
+       in (not sgn, tot + val)
+    len = length m0
+
+-- | get the determinant of a matrix
+determinant :: Num a => Mat2 n n a -> a
+determinant (Mat v (n :| _)) =
+  bool negate id (n <= _2P) $ determinantL n (V.toList v)
+
+
+
diff --git a/src/Cybus/NatHelper.hs b/src/Cybus/NatHelper.hs
--- a/src/Cybus/NatHelper.hs
+++ b/src/Cybus/NatHelper.hs
@@ -74,14 +74,14 @@
 import Data.Pos
 import Data.Proxy
 import qualified GHC.TypeLits as GL
-import GHC.TypeNats (Nat)
+import GHC.TypeNats (Nat,KnownNat)
 import qualified GHC.TypeNats as GN
 import Primus.Error
 import Primus.Fold
 import Primus.List
 import Primus.NonEmpty
 import Primus.One
-import qualified Primus.TypeLevel as TP (FailUnless)
+import Primus.TypeLevel (FailUnless)
 
 -- | get the factorial of a 'Nat'
 type FacT :: Nat -> Nat
@@ -93,7 +93,7 @@
 -- | constraint for ensuring that "i" <= "n"
 type (<=!) :: Nat -> Nat -> Constraint
 type i <=! n =
-  ( TP.FailUnless
+  ( FailUnless
       (i GN.<=? n)
       ( 'GL.Text "i>n"
           'GL.:<>: 'GL.Text ": i="
@@ -101,13 +101,13 @@
           'GL.:<>: 'GL.Text " n="
           'GL.:<>: 'GL.ShowType n
       )
-  , PosT i
+  , PosC i
   )
 
 -- | constraint for ensuring that "i" <= "n" with a custom error message
 type LTEQT :: GL.ErrorMessage -> Nat -> Nat -> Constraint
 type LTEQT msg i n =
-  ( TP.FailUnless
+  ( FailUnless
       (i GN.<=? n)
       ( 'GL.Text "i>n"
           'GL.:<>: 'GL.Text ": i="
@@ -116,13 +116,13 @@
           'GL.:<>: 'GL.ShowType n
           'GL.:<>: msg
       )
-  , PosT i
+  , PosC i
   )
 
 -- | constraint for ensuring that "i" <= "n"
 type (<!) :: Nat -> Nat -> Constraint
 type i <! n =
-  ( TP.FailUnless
+  ( FailUnless
       (i GN.+ 1 GN.<=? n)
       ( 'GL.Text "i>=n"
           'GL.:<>: 'GL.Text ": i="
@@ -130,9 +130,25 @@
           'GL.:<>: 'GL.Text " n="
           'GL.:<>: 'GL.ShowType n
       )
-  , GN.KnownNat i
+  , KnownNat i
   )
 
+-- | constraint for positive numbers
+type LTEQC :: Nat -> Nat -> Constraint
+class (KnownNat i, KnownNat n) => LTEQC i n where
+instance
+  ( KnownNat i
+  , KnownNat n
+  , FailUnless
+      (i GL.<=? n)
+      ( 'GL.Text "LTEQC n: requires n >= i but found i="
+          'GL.:<>: 'GL.ShowType i
+          'GL.:<>: 'GL.Text " n="
+          'GL.:<>: 'GL.ShowType n
+      )
+  ) =>
+  LTEQC i n
+
 -- | constraint for DiffC with better error messages
 type DiffTC :: Nat -> Nat -> Nat -> Constraint
 type DiffTC i j n = (i <=! j, j <=! n)
@@ -155,7 +171,7 @@
 -- | product of a type level list as a 'Nat'
 type ProductT :: [Nat] -> Nat
 type family ProductT ns where
-  ProductT '[] = GL.TypeError ('GL.Text "ProductT: empty indices")
+  ProductT '[] = GL.TypeError ( 'GL.Text "ProductT: empty indices")
   ProductT '[n] = n
   ProductT (n ': n1 ': ns) = n GN.* ProductT (n1 ': ns)
 
@@ -193,7 +209,7 @@
       [] -> programmError "ValidateNestedNonEmptyC: ('S 'Z): empty list of indices"
 instance ValidateNestedNonEmptyC x ( 'S zs) => ValidateNestedNonEmptyC (NonEmpty x) ( 'S ( 'S zs)) where
   validateNestedNonEmptyC ixes x@(n :| ns) xs =
-    let cs = map clOrdering $ compareLengths (x :| xs)
+    let cs = map clOrdering $ compareLengths x xs
      in if all (Just EQ ==) cs
           then
             let zs = ns <> concatMap N.toList xs
@@ -215,7 +231,7 @@
 instance ValidateNestedListC x ( 'S n) => ValidateNestedListC [x] ( 'S ( 'S n)) where
   validateNestedListC ixes [] _ = Left $ "validateNestedListC: ixes=" ++ show ixes ++ ":no data!"
   validateNestedListC ixes x@(n : ns) xs =
-    let cs = map clOrdering $ compareLengths (x :| xs)
+    let cs = map clOrdering $ compareLengths x xs
      in if all (Just EQ ==) cs
           then
             let zs = ns <> concat xs
@@ -240,14 +256,14 @@
 -- | convert a matrix index into nested lists
 type ListNST :: [Nat] -> Type -> Type
 type family ListNST ns a where
-  ListNST '[] _ = GL.TypeError ('GL.Text "ListNST: empty indices")
+  ListNST '[] _ = GL.TypeError ( 'GL.Text "ListNST: empty indices")
   ListNST '[_] a = [a]
   ListNST (_ ': n1 ': ns) a = [ListNST (n1 ': ns) a]
 
 -- | convert a matrix index into nested lists
 type NonEmptyNST :: [Nat] -> Type -> Type
 type family NonEmptyNST ns a where
-  NonEmptyNST '[] _ = GL.TypeError ('GL.Text "NonEmptyNST: empty indices")
+  NonEmptyNST '[] _ = GL.TypeError ( 'GL.Text "NonEmptyNST: empty indices")
   NonEmptyNST '[_] a = NonEmpty a
   NonEmptyNST (_ ': n1 ': ns) a = NonEmpty (NonEmptyNST (n1 ': ns) a)
 
@@ -270,12 +286,12 @@
 
   flattenNestedListC :: proxy a -> ListNST ns a -> Either String [a]
 
-instance GL.TypeError ('GL.Text "NestedListC '[]: empty indices") => NestedListC '[] where
+instance GL.TypeError ( 'GL.Text "NestedListC '[]: empty indices") => NestedListC '[] where
   nestedListToNonEmptyC = compileError "NestedListC '[]:nestedListToNonEmptyC"
   nestedNonEmptyToListC = compileError "NestedListC '[]:nestedNonEmptyToListC"
   flattenNestedListC = compileError "NestedListC '[]:flattenNestedListC"
 
-instance PosT n => NestedListC '[n] where
+instance PosC n => NestedListC '[n] where
   nestedListToNonEmptyC _ = \case
     [] -> Left "nestedListToNonEmptyC 'SZ no data"
     x : xs -> lmsg "nestedListToNonEmptyC 'SZ" $ lengthExact1 (fromNP @n) (x :| xs)
@@ -284,7 +300,7 @@
     [] -> Left "flattenNestedListC 'SZ no data"
     x : xs -> lmsg "flattenNestedListC 'SZ" $ lengthExact (fromN @n) (x : xs)
 
-instance (PosT n, NestedListC (n1 ': ns)) => NestedListC (n ': n1 ': ns) where
+instance (PosC n, NestedListC (n1 ': ns)) => NestedListC (n ': n1 ': ns) where
   nestedListToNonEmptyC p = \case
     [] -> Left "nestedListToNonEmptyC 'SS no data"
     x : xs -> do
diff --git a/test/TestFin.hs b/test/TestFin.hs
--- a/test/TestFin.hs
+++ b/test/TestFin.hs
@@ -164,13 +164,13 @@
           @?= Right (FinU @5 _4P _5P)
     , testCase "_Fin" $
         mkFinC @5 _10P _5P
-          @?= Left "mkFin:10P is too large: maximum is 5P"
+          @?= Left "mkFin:_10P is too large: maximum is _5P"
     , testCase "mkFinC" $
         mkFinC @9 _4P _10P
-          @?= Left "mkFinC: 10P /= 9P at typelevel"
+          @?= Left "mkFinC: _10P /= _9P at typelevel"
     , testCase "mkFinC" $
         mkFinC @9 _12P _10P
-          @?= Left "mkFinC: 10P /= 9P at typelevel"
+          @?= Left "mkFinC: _10P /= _9P at typelevel"
     , testCase "signum1" $
         signum1 (Right (FinU @5 _4P _5P))
           @?= Right (FinU @5 _1P _5P)
@@ -229,7 +229,7 @@
     , testCase "fin" $
         fin @10 (-5) @?= Left "eitherPos: i<=0: found -5"
     , testCase "fin" $
-        fin @10 11 @?= Left "mkFin:11P is too large: maximum is 10P"
+        fin @10 11 @?= Left "mkFin:_11P is too large: maximum is _10P"
     , testCase "fin" $
         fin @10 10 @?= Right (FinU _10P _10P)
     , testCase "fin" $
diff --git a/test/TestFinMat.hs b/test/TestFinMat.hs
--- a/test/TestFinMat.hs
+++ b/test/TestFinMat.hs
@@ -214,16 +214,16 @@
               N.last xs @?= maxBound
     , testCase "showFinMat" $
         map showFinMat [FinMatU @'[2, 3, 5] 0 (_2P :| [_3P, _5P]), toEnum 5 ..]
-          @?= ["0@{2,3,5}", "5@{2,3,5}", "10@{2,3,5}", "15@{2,3,5}", "20@{2,3,5}", "25@{2,3,5}"]
+          @?= ["FinMat@0{2,3,5}", "FinMat@5{2,3,5}", "FinMat@10{2,3,5}", "FinMat@15{2,3,5}", "FinMat@20{2,3,5}", "FinMat@25{2,3,5}"]
     , testCase "nonEmptyToFinMat'" $
         nonEmptyToFinMat' (_1P :| [_4P, _3P]) (_1P :| [_3P, _4P])
-          @?= Left "nonEmptyToFinMat:These es=outofbounds (4P,3P) as=(1P,1P) :| [(3P,4P)]"
+          @?= Left "nonEmptyToFinMat:These es=outofbounds (_4P,_3P) as=(_1P,_1P) :| [(_3P,_4P)]"
     , testCase "nonEmptyToFinMat'" $
         nonEmptyToFinMat' (_1P :| [_2P, _3P, _6P]) (_1P :| [_3P, _4P])
-          @?= Left "nonEmptyToFinMat:too many indices: expected 3 is=1P :| [2P,3P,6P] ns=1P :| [3P,4P]"
+          @?= Left "nonEmptyToFinMat:too many indices: expected 3 is=_1P :| [_2P,_3P,_6P] ns=_1P :| [_3P,_4P]"
     , testCase "nonEmptyToFinMat'" $
         nonEmptyToFinMat' (_1P :| [_2P]) (_1P :| [_3P, _4P])
-          @?= Left "nonEmptyToFinMat:not enough indices: expected 3 is=1P :| [2P] ns=1P :| [3P,4P]"
+          @?= Left "nonEmptyToFinMat:not enough indices: expected 3 is=_1P :| [_2P] ns=_1P :| [_3P,_4P]"
     , testCase "nonEmptyToFinMat'" $
         nonEmptyToFinMat' (_3P :| [_1P, _4P]) (_3P :| [_8P, _7P])
           @?= Right (FinMatU @'[3, 8, 7] 115 (_3P :| [_8P, _7P]))
@@ -370,45 +370,45 @@
     , testCase "relPos" $
         relPos ((_4P, _7P) :| [(_3P, _5P), (_2P, _5P)]) @?= (_P @175, 86)
     , testCase "readFinMat" $
-        readFinMat @'[7, 3, 3] "5@{7,3,3}xyz" @?= [(finMatC @'[1, 2, 3] @'[7, 3, 3], "xyz")]
+        readFinMat @'[7, 3, 3] "FinMat@5{7,3,3}xyz" @?= [(finMatC @'[1, 2, 3] @'[7, 3, 3], "xyz")]
     , testCase "readFinMat" $
         let m = finMatC @'[1, 2, 3] @'[7, 3, 3]
          in readFinMat @'[7, 3, 3] (show m ++ "  ") @?= [(m, "  ")]
     , testCase "readFinMat" $
-        readFinMat @'[7, 3, 3] "6@{1,2,3}xyz" @?= []
+        readFinMat @'[7, 3, 3] "FinMat@6{1,2,3}xyz" @?= []
     , testCase "readFinMat" $
-        readFinMat @'[1, 2, 3] "         4@{     1,             2,   3}xy"
+        readFinMat @'[1, 2, 3] "   FinMat@4{     1,             2,   3}xy"
           @?= [(FinMatU @'[1, 2, 3] 4 (_1P :| [_2P, _3P]), "xy")]
     , testCase "showFinMat'" $
         showFinMat' (finMatC @'[2, 3, 5] @'[4, 4, 6])
-          @?= "40@{2,3,5|4,4,6}"
+          @?= "FinMat@40{2,3,5|4,4,6}"
     , testCase "showFinMat'" $
         showFinMat' (finMatC @'[1] @'[1])
-          @?= "0@{1|1}"
+          @?= "FinMat@0{1|1}"
     , testCase "showFinMat'" $
         showFinMat' (finMatC @(NN 123) @(NN 234))
-          @?= "6@{1,2,3|2,3,4}"
+          @?= "FinMat@6{1,2,3|2,3,4}"
     , testCase "showFinMat'" $
         showFinMat' (finMatC @(NN 111) @(NN 234))
-          @?= "0@{1,1,1|2,3,4}"
+          @?= "FinMat@0{1,1,1|2,3,4}"
     , testCase "showFinMat'" $
         showFinMat' (finMatC @(NN 114) @(NN 234))
-          @?= "3@{1,1,4|2,3,4}"
+          @?= "FinMat@3{1,1,4|2,3,4}"
     , testCase "showFinMat'" $
         showFinMat' (finMatC @(NN 9) @(NN 9))
-          @?= "8@{9|9}"
+          @?= "FinMat@8{9|9}"
     , testCase "showFinMat" $
         showFinMat (finMatC @'[1] @'[1])
-          @?= "0@{1}"
+          @?= "FinMat@0{1}"
     , testCase "showFinMat" $
         showFinMat (finMatC @'[1] @'[10])
-          @?= "0@{10}"
+          @?= "FinMat@0{10}"
     , testCase "showFinMat" $
         showFinMat (finMatC @'[10] @'[10])
-          @?= "9@{10}"
+          @?= "FinMat@9{10}"
     , testCase "showFinMat" $
         showFinMat (finMatC @'[4] @'[10])
-          @?= "3@{10}"
+          @?= "FinMat@3{10}"
     , testCase "fromInteger1" $
         fromInteger1 (minBound @(FinMat '[2, 3, 4])) 0
           @?= Right (FinMatU @'[2, 3, 4] 0 (_2P :| [_3P, _4P]))
@@ -434,20 +434,29 @@
         toInteger1 (FinMatU @'[2, 3, 4] 12 (_2P :| [_3P, _4P]))
           @?= 12
     , testCase "index lenses" $
-         finMatC @'[2,5,3,7] @'[2,12,13,8] ^. _i1
-           @?= FinU @2 _2P _2P
+        finMatC @'[2, 5, 3, 7] @'[2, 12, 13, 8] ^. _i1
+          @?= FinU @2 _2P _2P
     , testCase "index lenses" $
-         finMatC @'[2,5,3,7] @'[2,12,13,8] ^. _i2
-           @?= FinU @12 _5P _12P
+        finMatC @'[2, 5, 3, 7] @'[2, 12, 13, 8] ^. _i2
+          @?= FinU @12 _5P _12P
     , testCase "index lenses" $
-         finMatC @'[2,5,3,7] @'[2,12,13,8] ^. _i4
-           @?= FinU @8 _7P _8P
+        finMatC @'[2, 5, 3, 7] @'[2, 12, 13, 8] ^. _i4
+          @?= FinU @8 _7P _8P
     , testCase "finMat finMatC" $
-         finMat @'[2,12,13,8] (6 + 2*8 + 4*13*8 + 1*12*13*8)
-         @?= Right (finMatC @'[2,5,3,7] @'[2,12,13,8])
+        finMat @'[2, 12, 13, 8] (6 + 2 * 8 + 4 * 13 * 8 + 1 * 12 * 13 * 8)
+          @?= Right (finMatC @'[2, 5, 3, 7] @'[2, 12, 13, 8])
     , testCase "finMat finMatC" $
-         finMat @'[21] 0
-         @?= Right (finMatC @'[1] @'[21])
+        finMat @'[21] 0
+          @?= Right (finMatC @'[1] @'[21])
+    , testCase "_finMatCons" $
+      (finMatC @'[2,1] @'[7,1] ^. _finMatCons) @?= (finC @2 @7, finMatC @'[1] @'[1])
+    , testCase "_finMatCons" $
+      (finMatC @'[2,1] @'[7,4] ^. _finMatCons) @?= (finC @2 @7, finMatC @'[1] @'[4])
+    , testCase "_finMatCons" $
+      (finMatC @'[2,2] @'[7,2] ^. _finMatCons) @?= (finC @2 @7, finMatC @'[2] @'[2])
+
+    , testCase "_finMatCons" $
+      (finMatC @'[2,4] @'[7,4] ^. _finMatCons) @?= (finC @2 @7, finMatC @'[4] @'[4])
     ]
 
 fmi237' :: NonEmpty (FinMat '[2, 3, 7])
@@ -461,3 +470,4 @@
 
 fmiNS :: NonEmpty Int -> NonEmpty (NonEmpty Int)
 fmiNS = traverse (N.fromList . enumFromTo 1)
+
diff --git a/test/TestMat.hs b/test/TestMat.hs
--- a/test/TestMat.hs
+++ b/test/TestMat.hs
@@ -1,5 +1,8 @@
 {-# OPTIONS -Wno-orphans #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE OverloadedStrings #-}
@@ -7,6 +10,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
 
 module TestMat where
 
@@ -40,6 +44,9 @@
 import Test.Tasty
 import Test.Tasty.HUnit
 import qualified Test.Tasty.QuickCheck as TQ
+import Unsafe.Coerce
+import qualified GHC.TypeNats as GN
+import Data.Proxy
 
 instance (NS ns, Arbitrary a) => Arbitrary (Mat ns a) where
   arbitrary = sequenceA $ mat @ns (repeat arbitrary)
@@ -126,16 +133,16 @@
         matToNestedListC (fmap (show . succ) m35)
           @?= [["2", "3", "4", "5", "6"], ["7", "8", "9", "10", "11"], ["12", "13", "14", "15", "16"]]
     , testCase "totuple" $
-        toTupleC (mat' @'[2, 3, 2] [1 :: Int .. 12])
+        toTupleC (mat' @'[2, 3, 2] @Int [1 .. 12])
           @?= (((1, 2), (3, 4), (5, 6)), ((7, 8), (9, 10), (11, 12)))
     , testCase "fromtuple" $
         fromTupleC (((1, 2), (3, 4), (5, 6)), ((7, 8), (9, 10), (11, 12)))
-          @?= mat' @'[2, 3, 2] [1 :: Int .. 12]
+          @?= mat' @'[2, 3, 2] @Int [1 .. 12]
     , testCase "change row" $
-        (mat' @'[3, 4] [1 :: Int .. 12] & ixSlice @'[2, 3] .~ 999)
+        (mat' @'[3, 4] @Int [1 .. 12] & ixSlice @'[2, 3] .~ 999)
           @?= mat' @'[3, 4] [1, 2, 3, 4, 5, 6, 999, 8, 9, 10, 11, 12]
     , testCase "change row" $
-        (mat' @'[3, 4] [1 :: Int .. 12] & ixSlice @'[1] *~ 999)
+        (mat' @'[3, 4] @Int [1 .. 12] & ixSlice @'[1] *~ 999)
           @?= mat' @'[3, 4] [999, 1998, 2997, 3996, 5, 6, 7, 8, 9, 10, 11, 12]
     , testCase "change row" $
         m345 ^. ixSlice @'[2, 3]
@@ -144,16 +151,16 @@
         (m35 & ixSlice @'[2] . traverse *~ 100)
           @?= mat' @'[3, 5] [1, 2, 3, 4, 5, 600, 700, 800, 900, 1000, 11, 12, 13, 14, 15]
     , testCase "change row" $
-        (mat' @'[2, 1, 2, 3, 4] [1 :: Int .. 48] & ixSlice @'[2, 1, 1] . traverse *~ 100)
+        (mat' @'[2, 1, 2, 3, 4] @Int [1 .. 48] & ixSlice @'[2, 1, 1] . traverse *~ 100)
           @?= mat' @'[2, 1, 2, 3, 4] [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 2500, 2600, 2700, 2800, 2900, 3000, 3100, 3200, 3300, 3400, 3500, 3600, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48]
     , testCase "change row" $
         m345 ^. ixSlice @'[2]
           @?= mat' @'[4, 5] ['U' .. 'h']
     , testCase "not as useful: nests all stuff" $
-        fmap sum (matToNestedVecC @'[2, 3] (mat' [1 :: Int .. 6]))
+        fmap sum (matToNestedVecC @'[2, 3] (mat' @_ @Int [1 .. 6]))
           @?= 6 .| 15
     , testCase "mapLeaf: change the lowest rows into lists" $
-        mapLeaf (const sum) (mat' @'[4, 3] [1 :: Int .. 12])
+        mapLeaf (const sum) (mat' @'[4, 3] @Int [1 .. 12])
           @?= mat' @'[4] [6, 15, 24, 33]
     , testCase "mapLeafSimple" $
         mapLeafSimple (fmap . (,) . fmPos) (gen' @(NN 43) id)
@@ -174,19 +181,19 @@
         foldMapLeafR (\i m -> [(fmPos i, sum m, toList m)]) (mm @(NN 234))
           @?= [(20, 90, [21, 22, 23, 24]), (16, 74, [17, 18, 19, 20]), (12, 58, [13, 14, 15, 16]), (8, 42, [9, 10, 11, 12]), (4, 26, [5, 6, 7, 8]), (0, 10, [1, 2, 3, 4])]
     , testCase "addition" $
-        mat' @'[2, 3] [1 .. 6] + mat' [100 :: Int .. 105]
+        mat' @'[2, 3] @Int [1 .. 6] + mat' [100 .. 105]
           @?= mat' [101, 103, 105, 107, 109, 111]
     , testCase "multiplication" $
-        mat' @'[2, 3] [1 .. 6] * mat' [100 :: Int .. 105]
+        mat' @'[2, 3] @Int [1 .. 6] * mat' [100 .. 105]
           @?= mat' [100, 202, 306, 412, 520, 630] -- note: have to use mat' for inference to work
     , testCase "transpose" $
-        transposeMat (mat' @'[2, 3] [1 :: Int .. 6])
+        transposeMat (mat' @'[2, 3] @Int [1 .. 6])
           @?= mat' [1, 4, 2, 5, 3, 6]
     , testCase "transpose iso" $
         transposeMat (transposeMat m345)
           @?= m345
     , testCase "diagonal" $
-        diagonal (mat' @'[3, 3, 4] [1 :: Int .. 36])
+        diagonal (mat' @'[3, 3, 4] @Int [1 .. 36])
           @?= mat' [1, 2, 3, 4, 17, 18, 19, 20, 33, 34, 35, 36]
     , testCase "diagonal" $
         diagonal (gen @'[4, 4] succ)
@@ -201,31 +208,31 @@
         finMatMatrix @'[2, 3, 1]
           @?= mat' (toList (N.map (fr . (nonEmptyToFinMat <=< toPositives)) ([1, 1, 1] :| [[1, 2, 1], [1, 3, 1], [2, 1, 1], [2, 2, 1], [2, 3, 1]])))
     , testCase "insert row" $
-        insertRow @2 (mat' @'[3, 4] [100 .. 111]) (mat' @'[2, 3, 4] [1 :: Int .. 24])
+        insertRow @2 (mat' @'[3, 4] [100 .. 111]) (mat' @'[2, 3, 4] @Int [1 .. 24])
           @?= mat' [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24]
     , testCase "insert column" $
-        insertCol @2 (mat' @'[2, 4] [100 .. 107]) (mat' @'[2, 3, 4] [1 :: Int .. 24])
+        insertCol @2 (mat' @'[2, 4] [100 .. 107]) (mat' @'[2, 3, 4] @Int [1 .. 24])
           @?= mat' [1, 2, 3, 4, 100, 101, 102, 103, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 104, 105, 106, 107, 17, 18, 19, 20, 21, 22, 23, 24]
     , testCase "delete row" $
-        deleteRow @2 (mat' @'[2, 3, 4] [1 :: Int .. 24])
+        deleteRow @2 (mat' @'[2, 3, 4] @Int [1 .. 24])
           @?= mat' [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]
     , testCase "insert/delete row" $
         deleteRow @2 (insertRow @2 (mat' @'[4, 5] [100 .. 119]) m345')
           @?= m345'
     , testCase "to nested lists" $
-        matToNestedListC (mat' @'[2, 3, 4] [1 :: Int .. 24])
+        matToNestedListC (mat' @'[2, 3, 4] @Int [1 .. 24])
           @?= [[[1, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12]], [[13, 14, 15, 16], [17, 18, 19, 20], [21, 22, 23, 24]]]
     , testCase "concat vertically" $
-        matToNestedListC (appendV (mat' @'[2, 3, 2] [1 .. 12]) (mat' @'[5, 3, 2] [100 :: Int .. 129]))
+        matToNestedListC (appendV (mat' @'[2, 3, 2] [1 .. 12]) (mat' @'[5, 3, 2] @Int [100 .. 129]))
           @?= [[[1, 2], [3, 4], [5, 6]], [[7, 8], [9, 10], [11, 12]], [[100, 101], [102, 103], [104, 105]], [[106, 107], [108, 109], [110, 111]], [[112, 113], [114, 115], [116, 117]], [[118, 119], [120, 121], [122, 123]], [[124, 125], [126, 127], [128, 129]]]
     , testCase "concat vertically" $
-        matToNestedListC (appendV (mat' @'[2, 3] [1 .. 6]) (mat' @'[7, 3] [100 :: Int .. 120]))
+        matToNestedListC (appendV (mat' @'[2, 3] [1 .. 6]) (mat' @'[7, 3] @Int [100 .. 120]))
           @?= [[1, 2, 3], [4, 5, 6], [100, 101, 102], [103, 104, 105], [106, 107, 108], [109, 110, 111], [112, 113, 114], [115, 116, 117], [118, 119, 120]]
     , testCase "concat horizontally" $
-        matToNestedListC (appendH (mat' @'[5, 2, 2] [1 .. 20]) (mat' @'[5, 3, 2] [100 :: Int .. 129]))
+        matToNestedListC (appendH (mat' @'[5, 2, 2] [1 .. 20]) (mat' @'[5, 3, 2] @Int [100 .. 129]))
           @?= [[[1, 2], [3, 4], [100, 101], [102, 103], [104, 105]], [[5, 6], [7, 8], [106, 107], [108, 109], [110, 111]], [[9, 10], [11, 12], [112, 113], [114, 115], [116, 117]], [[13, 14], [15, 16], [118, 119], [120, 121], [122, 123]], [[17, 18], [19, 20], [124, 125], [126, 127], [128, 129]]]
     , testCase "concat horizontally" $
-        matToNestedListC (appendH (mat' @'[3, 2] [1 .. 6]) (mat' @'[3, 7] [100 :: Int .. 120]))
+        matToNestedListC (appendH (mat' @'[3, 2] @Int [1 .. 6]) (mat' @'[3, 7] @Int [100 .. 120]))
           @?= [[1, 2, 100, 101, 102, 103, 104, 105, 106], [3, 4, 107, 108, 109, 110, 111, 112, 113], [5, 6, 114, 115, 116, 117, 118, 119, 120]]
     , testCase "consMat" $
         (gen @'[3, 4] succ ^. consMat)
@@ -282,20 +289,20 @@
         nestedVecToMatC (matToNestedVecC m345)
           @?= m345 -- works without @'[3,4,5] cos @?= tells us the type
     , testCase "delete item from 1d mat'" $
-        deleteRow @4 (mat' @'[10] [1 :: Int .. 10])
+        deleteRow @4 (mat' @'[10] @Int [1 .. 10])
           @?= mat' [1, 2, 3, 5, 6, 7, 8, 9, 10]
     , testCase "redim" $
-        redim (mat' @'[2, 3, 5] [1 :: Int .. 30])
-          @?= mat' @'[6, 5] [1 :: Int .. 30]
+        redim (mat' @'[2, 3, 5] @Int [1 .. 30])
+          @?= mat' @'[6, 5] @Int [1 .. 30]
     , testCase "redim" $
-        redim (mat' @'[5, 9, 4] [1 :: Int .. 180])
-          @?= mat' @'[3, 6, 10] [1 :: Int .. 180]
+        redim (mat' @'[5, 9, 4] @Int [1 .. 180])
+          @?= mat' @'[3, 6, 10] @Int [1 .. 180]
     , testCase "redim" $
-        redim (mat' @'[18] [1 :: Int .. 18])
-          @?= mat' @'[3, 2, 3] [1 :: Int .. 18]
+        redim (mat' @'[18] @Int [1 .. 18])
+          @?= mat' @'[3, 2, 3] @Int [1 .. 18]
     , testCase "redim" $
-        redim (mat' @'[3, 2, 3] [1 :: Int .. 18])
-          @?= mat' @'[18] [1 :: Int .. 18]
+        redim (mat' @'[3, 2, 3] @Int [1 .. 18])
+          @?= mat' @'[18] @Int [1 .. 18]
     , testCase "diagonal" $
         diagonal (gen @'[4, 4] succ)
           @?= mat' @'[4] [1, 6, 11, 16]
@@ -306,7 +313,7 @@
         diagonal (mm @(NN 99))
           @?= mat' @'[9] [1, 11, 21, 31, 41, 51, 61, 71, 81]
     , testCase "multMat" $
-        multMat (mat' @'[2, 5] [1 :: Int .. 10]) (mat' @'[5, 6] [1 :: Int .. 30])
+        multMat (mat' @'[2, 5] @Int [1 .. 10]) (mat' @'[5, 6] @Int [1 .. 30])
           @?= mat' @'[2, 6] [255, 270, 285, 300, 315, 330, 580, 620, 660, 700, 740, 780]
     , testCase "universe1 enum" $
         toNonEmpty (finMatMatrix @'[2, 3, 7])
@@ -315,16 +322,16 @@
         toList (finMatMatrix @'[2, 3, 7])
           @?= toList fmi237'
     , testCase "D3" $
-        mat' @(D3 2 3 4) [1 :: Int .. 24]
+        mat' @(D3 2 3 4) @Int [1 .. 24]
           @?= mat' @'[2, 3, 4] [1 .. 24]
     , testCase "ixMat" $
-        (mat' @'[2, 3, 4] [1 :: Int .. 24] & ixMat (finMatC @'[2, 3, 1]) +~ 100)
+        (mat' @'[2, 3, 4] @Int [1 .. 24] & ixMat (finMatC @'[2, 3, 1]) +~ 100)
           @?= mat' @'[2, 3, 4] [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 121, 22, 23, 24]
     , testCase "ixMat" $
-        (mat' @'[2, 3, 4] [1 :: Int .. 24] & ixMat (finMatC @'[2, 3, 4]) +~ 100)
+        (mat' @'[2, 3, 4] @Int [1 .. 24] & ixMat (finMatC @'[2, 3, 4]) +~ 100)
           @?= mat' @'[2, 3, 4] [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 124]
     , testCase "read" $
-        (read @(Mat (D1 4) Int) $ show $ mat' @'[4] [1 :: Int .. 4])
+        (read @(Mat (D1 4) Int) $ show $ mat' @'[4] @Int [1 .. 4])
           @?= (1 .: 2 .: 3 .| 4)
     , testCase "read" $
         let m = gen' @'[1] id
@@ -345,10 +352,10 @@
         let m = ('x', True, ['a' .. 'z'], gen' @'[1, 2, 3] id, False)
          in read (show m) @?= m
     , testCase "read" $
-        let m = mat' @'[4, 5] [1 :: Int .. 20]
+        let m = mat' @'[4, 5] @Int [1 .. 20]
          in read @(Mat (D2 4 5) Int) (show m) @?= m
     , testCase "read" $
-        let m = mat' @'[1, 2, 3, 4] [1 :: Int .. 24]
+        let m = mat' @'[1, 2, 3, 4] @Int [1 .. 24]
          in read (show m) @?= m
     , testCase "read" $
         let m = toND @1 (mm @(NN 2352))
@@ -361,15 +368,15 @@
          in read (show m) @?= m
     , testCase "sortByRows" $
         sortByRows (flip compare) (mat' @'[4, 2] [10, 9, 1, 2, 100, 200, 300, 400])
-          @?= mat' [10, 9, 2, 1, 200, 100, 400, 300 :: Int]
+          @?= mat' @_ @Int [10, 9, 2, 1, 200, 100, 400, 300]
     , testCase "sortByT" $
-        sortByT (flip compare) (mat' @'[4] [10 :: Int, 9, 1, 2])
+        sortByT (flip compare) (mat' @'[4] @Int [10, 9, 1, 2])
           @?= (10 .: 9 .: 2 .| 1)
     , testCase "sortByT" $
-        sortByT compare (mat' @'[4] [10 :: Int, 9, 1, 2])
+        sortByT compare (mat' @'[4] @Int [10, 9, 1, 2])
           @?= (1 .: 2 .: 9 .| 10)
     , testCase "sortByRows" $
-        sortByRows compare (mat' @'[4, 2] [10 :: Int, 9, 1, 2, 100, 200, 300, 400])
+        sortByRows compare (mat' @'[4, 2] @Int [10, 9, 1, 2, 100, 200, 300, 400])
           @?= mat' [9, 10, 1, 2, 100, 200, 300, 400]
     , testCase "totuple" $
         toTupleC (vec' "abc")
@@ -381,7 +388,7 @@
         fromTupleC (One 'a')
           @?= se1 'a'
     , testCase "fromtuple" $
-        fromTupleC (1, 2, 3 :: Int)
+        fromTupleC @_ @Int (1, 2, 3)
           @?= 1 .: 2 .| 3
     , testCase "consMat" $
         (mat' @'[1] "x" ^. consMat)
@@ -426,19 +433,19 @@
         (mat' @'[5, 3] ['A' .. 'O'] ^. snocMat)
           @?= (mat' @'[4, 3] ['A' .. 'L'], mat' @'[3] "MNO")
     , testCase "field lens" $
-        (mat' @'[3, 3, 4] [1 :: Int .. 36] ^. _r3 . _r1)
+        (mat' @'[3, 3, 4] @Int [1 .. 36] ^. _r3 . _r1)
           @?= vec' @4 [25, 26, 27, 28]
     , testCase "field lens" $
-        (mat' @'[3, 3, 4] [1 :: Int .. 36] ^. _r3 . _r1)
+        (mat' @'[3, 3, 4] @Int [1 .. 36] ^. _r3 . _r1)
           @?= vec' @4 [25, 26, 27, 28]
     , testCase "field lens update" $
         (mat' @'[2, 1, 4] ['A' .. 'H'] & _r2 . _r1 . _r3 %~ toLower)
           @?= mat' "ABCDEFgH"
     , testCase "field lens" $
-        (mat' @'[7] [1 :: Int .. 7] ^. _r3)
+        (mat' @'[7] @Int [1 .. 7] ^. _r3)
           @?= 3
     , testCase "field lens" $
-        (mat' @'[7, 4] [1 :: Int .. 28] ^. _r3 . _r2)
+        (mat' @'[7, 4] @Int [1 .. 28] ^. _r3 . _r2)
           @?= 10
     , testCase "subsetRows" $
         subsetRows @2 @2 (gen @'[2, 5] succ)
@@ -674,13 +681,13 @@
         (('x', Eof1) ^. from (consMat @'[1]))
           @?= se1 'x'
     , testCase "nestedListToMatC" $
-        nestedListToMatC @'[2, 3, 5] [[[1 :: Int, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]
+        nestedListToMatC @'[2, 3, 5] @Int [[[1, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]
           @?= Right (mat' @'[2, 3, 5] [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30])
     , testCase "nestedListToMatC" $
-        nestedListToMatC @'[3, 3, 5] [[[1 :: Int, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]
+        nestedListToMatC @'[3, 3, 5] @Int [[[1, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]
           @?= Left "LT: not enough elements: expected 3 found 2"
     , testCase "nestedListToMatC" $
-        nestedListToMatC @'[2, 3, 6] [[[1 :: Int, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]
+        nestedListToMatC @'[2, 3, 6] @Int [[[1, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15]], [[16, 17, 18, 19, 20], [21, 22, 23, 24, 25], [26, 27, 28, 29, 30]]]
           @?= Left "not enough elements: expected 6 found 5"
     , testCase "indexRow" $
         indexRow (fr $ fin @7 1) (gen' @(NN 73) id)
@@ -692,19 +699,19 @@
         indexRow (fr $ fin @7 7) (gen' @(NN 73) id)
           @?= vec' [[7, 1], [7, 2], [7, 3]]
     , testCase "readVec" $
-        readVec @5 @Int (show (mm @(NN 5))) @?= [(vec' [1 .. 5], "")]
+        readVec @5 @Int (show (vec' @5 [1::Int ..5])) @?= [(vec' [1 .. 5], "")]
     , testCase "readMat2" $
         let m = mat' @'[3, 7] ['a' .. 'u']
          in readMat2 @3 @7 @Char (show m ++ "xyz") @?= [(m, "xyz")]
     , testCase "readVec" $
         let m = mat' @'[7] ['a' .. 'g']
          in readVec @7 @Char (show m ++ " xyz") @?= [(m, " xyz")]
-    , testCase "readMat2" $
-        let m = mm @(NN 372)
-         in readMat @(NN 372) @Int (show m ++ "xyz") @?= [(m, "xyz")] -- dont need type application but here we have inference
+    , testCase "readMat" $
+        let m = mat' @'[3,7,2] [1::Int .. 42]
+         in readMat @'[3,7,2] @Int (show m ++ "xyz") @?= [(m, "xyz")] -- dont need type application but here we have inference
     , testCase "readMat12" $
-        let m = toVec (mm @(NN 372))
-         in readVec @3 @(Mat2 7 2 Int) (show m ++ "xyz") @?= [(m, "xyz")] -- dont need type application but here we have inference
+        let m = mat' @'[3,7,2] [1::Int .. 42]
+         in readMat @'[3,7,2] @Int (show m ++ "xyz") @?= [(m, "xyz")] -- dont need type application but here we have inference
     , testCase "readMat3456" $
         let m = toMat2 (mm @(NN 3456))
          in readMat2 @3 @4 @(Mat2 5 6 Int) (show m ++ "xyz") @?= [(m, "xyz")] -- dont need type application but here we have inference
@@ -722,19 +729,19 @@
           @?= vec' @1 [99]
     , testCase "(.:)" $
         (12 .: 44 .| 99)
-          @?= vec' @3 [12 :: Int, 44, 99]
+          @?= vec' @3 @Int [12, 44, 99]
     , testCase "(.:)" $
         (5 .| 10 .:: 15 .| 20 .|| (25 .| 30))
-          @?= mat2' @3 @2 [5 :: Int, 10, 15, 20, 25, 30]
+          @?= mat2' @3 @2 @Int [5, 10, 15, 20, 25, 30]
     , testCase "(.:)" $
         se2 (5 .| 10 .:: 15 .| 20 .|| (25 .| 30))
-          @?= mat' @'[1, 3, 2] [5 :: Int, 10, 15, 20, 25, 30]
+          @?= mat' @'[1, 3, 2] @Int [5, 10, 15, 20, 25, 30]
     , testCase "nestedListToMatValidated" $
         let x = [[[[1 :: Int, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12]], [[13, 14, 15, 16], [17, 18, 19, 20], [21, 22, 23, 24, 25, 26, 27]]]]
-         in nestedListToMatValidated @(NN 1234) x @?= Left "validateNestedListC: lengths=[4,4,4,4,4,7] ixes=[1P,2P,3P]"
+         in nestedListToMatValidated @(NN 1234) x @?= Left "validateNestedListC: lengths=[4,4,4,4,4,7] ixes=[_1P,_2P,_3P]"
     , testCase "nestedListToMatValidated" $
         let x = [[[[1 :: Int, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12]], [[13, 14, 15, 16], [17, 18, 19, 20], []]]]
-         in nestedListToMatValidated @(NN 1234) x @?= Left "validateNestedListC: lengths=[4,4,4,4,4,0] ixes=[1P,2P,3P]"
+         in nestedListToMatValidated @(NN 1234) x @?= Left "validateNestedListC: lengths=[4,4,4,4,4,0] ixes=[_1P,_2P,_3P]"
     , testCase "nestedListToMatValidated" $
         let x = [[[[1 :: Int, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12]], [[13, 14, 15, 16], [17, 18, 19, 20], [21, 22, 23, 24]]]]
          in nestedListToMatValidated @(NN 1234) x @?= Right (mat' @'[1, 2, 3, 4] [1 .. 24])
@@ -812,7 +819,7 @@
         unfoldrRep @(Vec 5) (\i s -> (drop 1 s, (fmPos i, head s))) ['a' .. 'h']
           @?= ("fgh", vec' @5 [(0, 'e'), (1, 'd'), (2, 'c'), (3, 'b'), (4, 'a')])
     , testCase "fillTraversable" $
-        fillTraversable @(MatN 234) (pure ()) [1 :: Int .. 40]
+        fillTraversable @(MatN 234) @Int (pure ()) [1.. 40]
           @?= Right ([25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40], mat' @'[2, 3, 4] [1 .. 24])
     , testCase "toInteger1" $
         toInteger1 (pure @(Mat2 4 2) EQ)
@@ -895,14 +902,98 @@
     , testCase "fromInteger1" $
         fromInteger1 (minBound @(Mat '[2, 5] Int8)) (-1276136419117121619201)
           @?= Left "cap=(-1276136419117121619200,1180591620717411303423):padL: negative fill: would need to truncate the data"
-
     , testCase "lenses mixed" $
-       mm @(NN 1234) ^. _r1 . _r1 . _c2 . snocMat . _1 . consMat
-        @?= (2,vec @1 [6])
-
+        mm @(NN 1234) ^. _r1 . _r1 . _c2 . snocMat . _1 . consMat
+          @?= (2, vec @1 [6])
     , testCase "lenses mixed" $
         mm @(NN 734) ^. _c3 . snocMat . _1 . _c4 . _r5
-        @?= 60
+          @?= 60
+    , testCase "withN" $
+        let s = withN 5 $ \(_ :: x n) ->
+              withN 3 $ \(_ :: x m) ->
+                withN 2 $ \(_ :: x p) ->
+                  let w1 :: Mat2 n m Int -- if you use let statements then must have signatures else fails with constraints not satisfied
+                      w1 = mat2 @n @m [1 ..]
+                      w2 :: Mat2 m p Int
+                      w2 = mat2 @m @p [10 ..]
+                      z = multMat w1 w2
+                   in show (fromNSP @'[n, m, p], z)
+         in read @(NonEmpty Pos, Mat2 5 2 Int) s
+              @?= (_5P :| [_3P, _2P], mat2 @5 @2 [76, 82, 184, 199, 292, 316, 400, 433, 508, 550])
+    , testCase "withN" $
+        let s = withN 5 $ \(_ :: x n) ->
+              withN 3 $ \(_ :: x m) ->
+                show (mat2 @n @m @Int [1 ..] `multMat` mat2 @m @n @Int [10 ..])
+         in read @(Mat2 5 5 Int) s @?= mat2' @5 @5 [100, 106, 112, 118, 124, 235, 250, 265, 280, 295, 370, 394, 418, 442, 466, 505, 538, 571, 604, 637, 640, 682, 724, 766, 808]
+    , testCase "withN" $
+        let s = withN 5 $ \(_ :: x n) -> show (vec @n @Int [1 ..])
+         in read @(Vec 5 Int) s @?= vec' @5 [1 .. 5]
+    , testCase "withN" $
+        let s = withN 5 $ \(_ :: x n) ->
+              withN 7 $ \(_ :: x m) -> show (mat2 @n @m @Int [1 ..], mat2 @m @n ['a' ..])
+         in read @(Mat2 5 7 Int, Mat2 7 5 Char) s @?= (mat2' @5 @7 [1 .. 35], mat2 @7 @5 ['a' ..])
+    , testCase "withN2" $
+        let z = withN2 4 5 $ \(_ :: p n) (_ :: p m) -> show (mat2 @n @m ['a' ..])
+         in read @(Mat2 4 5 Char) z @?= mat2' @4 @5 ['a' .. 't']
+    , testCase "withN3" $
+        withN3 2 3 4 (\(_ :: z n) (_ :: z m) (_ :: z q) -> fromNSP @'[n, m, q])
+          @?= _2P :| [_3P, _4P]
+    , testCase "withN3" $
+        let z = withN 4 $ \(_ :: p n) -> show (mat2 @2 @n @Int [1..] ^. _row @1)
+         in read @(Vec 4 Int) z @?= vec' @4 [1 .. 4]
+    , testCase "withN3" $
+        let z = withN 4 $ \(_ :: p n) -> show (mat2 @2 @n @Int [1 ..] ^. _row @2)
+         in read @(Vec 4 Int) z @?= vec' @4 [5 .. 8]
+
+    , testCase "withNMin3" $
+         let z = withNMin3 5 (\(_ :: p n) -> withNMin3 4 (\(_ :: p m) -> show (mat2 @n @m [1::Int ..] ^. _c2)))
+         in read @(Vec 5 Int) z @?= vec' @5 [2,6,10,14,18]
+
+    , testCase "rotateLeft rotateRight" $
+        let z = mm @(NN 57)
+        in rotateLeft (rotateRight z) @?= z
+    , testCase "rotateLeft" $
+        rotateLeft (mm @(NN 35))
+          @?= mat2' @5 @3 [5,10,15,4,9,14,3,8,13,2,7,12,1,6,11]
+      ,testCase "rotateRight" $
+        rotateRight (mm @(NN 35))
+          @?= mat2' @5 @3 [11,6,1,12,7,2,13,8,3,14,9,4,15,10,5]
+    , testCase "rotateRight transpose rotateRight" $
+        let z = mm @(NN 57)
+        in (transposeMat . rotateLeft . transposeMat) z  @?= rotateRight z
+
+    , testCase "determinant" $
+        determinant (mat2' @3 @3 @Int [2, -3, 1, 2, 0, -1, 1, 4, 5])
+          @?= 49
+    , testCase "determinant" $
+        determinant (mat2' @3 @3 @Int [1, 3, 2, -3, -1, -3, 2, 3, 1])
+          @?= (-15)
+    , testCase "determinant" $
+        determinant (mat2' @4 @4 @Int [3, 2, 0, 1, 4, 0, 1, 2, 3, 0, 2, 1, 9, 2, 3, 1])
+          @?= 24
+    , testCase "determinant" $
+        determinant (mat2' @4 @4 @Int [1, 0, 2, -1, 3, 0, 0, 5, 2, 1, 4, -3, 1, 0, 5, 0])
+          @?= 30
+    , testCase "determinant" $
+        determinant (mat2' @4 @4 @Int [1, 0, 4, -6, 2, 5, 0, 3, -1, 2, 3, 5, 2, 1, -2, 3])
+          @?= 318
+    , testCase "determinant" $
+        determinant (mat2' @2 @2 @Int [1, 2, 3, 4])
+          @?= (-2)
+
+    , testCase "determinant" $
+        determinant (mat2' @1 @1 @Int [-5])
+          @?= (-5)
+    , testCase "deleteColumnL" $
+        deleteColumnL _2P 1 [1,2::Int] @?= [1]
+    , testCase "deleteColumnL" $
+        deleteColumnL _2P 0 [1,2::Int] @?= [2]
+    , testCase "deleteColumnL" $
+        deleteColumnL _3P 1 [1::Int .. 12] @?= [1,3,4,6,7,9,10,12]
+    , testCase "deleteColumnL" $
+        deleteColumnL _2P 1 [1..10::Int] @?=  [1,3,5,7,9]
+    , testCase "deleteColumnL" $
+        deleteColumnL _1P 0 [1::Int] @?= []
     ]
 
 suiteCheckers :: TestTree
@@ -920,3 +1011,55 @@
 
 fmi237 :: NonEmpty (NonEmpty Int)
 fmi237 = fmap N.fromList ([1, 1, 1] :| [[1, 1, 2], [1, 1, 3], [1, 1, 4], [1, 1, 5], [1, 1, 6], [1, 1, 7], [1, 2, 1], [1, 2, 2], [1, 2, 3], [1, 2, 4], [1, 2, 5], [1, 2, 6], [1, 2, 7], [1, 3, 1], [1, 3, 2], [1, 3, 3], [1, 3, 4], [1, 3, 5], [1, 3, 6], [1, 3, 7], [2, 1, 1], [2, 1, 2], [2, 1, 3], [2, 1, 4], [2, 1, 5], [2, 1, 6], [2, 1, 7], [2, 2, 1], [2, 2, 2], [2, 2, 3], [2, 2, 4], [2, 2, 5], [2, 2, 6], [2, 2, 7], [2, 3, 1], [2, 3, 2], [2, 3, 3], [2, 3, 4], [2, 3, 5], [2, 3, 6], [2, 3, 7]])
+
+-- ghc 9.2 needs explicit kinds for "i" and "n"
+overrideDictPositive :: forall (i :: Nat) (n :: Nat) p . p n -> (i GN.<=? n) :~: 'True
+overrideDictPositive _ = unsafeCoerce Refl
+
+-- | lift a positive number to the typelevel
+withN :: Int -> (forall n. FinC 1 n => Proxy n -> x) -> x
+withN i f
+  | i <= 1 = normalError $ "withN: index must be at least 1:found " ++ show i
+  | otherwise =
+      case GN.someNatVal (toEnum i) of
+        GN.SomeNat (pn :: Proxy n) ->
+          case overrideDictPositive @1 pn of
+            Refl -> f (Proxy @n)
+
+-- | lift a positive number to the typelevel
+withNMin2 :: Int -> (forall n . (FinC 2 n, FinC 1 n) => Proxy n -> x) -> x
+withNMin2 i f
+  | i < 2 = normalError $ "withNMin2: index must be at least 2:found " ++ show i
+  | otherwise =
+      case GN.someNatVal (toEnum i) of
+        GN.SomeNat (pn :: Proxy n) ->
+          case overrideDictPositive @1 pn of
+            Refl ->
+              case overrideDictPositive @2 pn of
+                 Refl -> f (Proxy @n)
+
+withNMin3 :: Int -> (forall n . (FinC 3 n, FinC 2 n, FinC 1 n) => Proxy n -> x) -> x
+withNMin3 i f
+  | i < 3 = normalError $ "withNMin3: index must be at least 3:found " ++ show i
+  | otherwise =
+      case GN.someNatVal (toEnum i) of
+        GN.SomeNat (pn :: Proxy n) ->
+          case overrideDictPositive @1 pn of
+            Refl ->
+              case overrideDictPositive @2 pn of
+                Refl ->
+                  case overrideDictPositive @3 pn of
+                    Refl -> f (Proxy @n)
+
+-- | lift two positive numbers to the typelevel
+withN2 :: Int -> Int -> (forall n m. (FinC 1 n, FinC 1 m) => Proxy n -> Proxy m -> x) -> x
+withN2 i j f = withN i $ \p1 -> withN j $ \p2 -> f p1 p2
+
+-- | lift three positive numbers to the typelevel
+withN3 :: Int -> Int -> Int -> (forall n m p. (FinC 1 n, FinC 1 m, FinC 1 p) => Proxy n -> Proxy m -> Proxy p -> x) -> x
+withN3 i j k f = withN i $ \p1 -> withN j $ \p2 -> withN k $ \p3 -> f p1 p2 p3
+
+-- | lift four positive numbers to the typelevel
+withN4 :: Int -> Int -> Int -> Int -> (forall n m p q. (FinC 1 n, FinC 1 m, FinC 1 p, FinC 1 q) => Proxy n -> Proxy m -> Proxy p -> Proxy q -> x) -> x
+withN4 i j k l f = withN i $ \p1 -> withN j $ \p2 -> withN k $ \p3 -> withN l $ \p4 -> f p1 p2 p3 p4
+
diff --git a/test/TestNatHelper.hs b/test/TestNatHelper.hs
--- a/test/TestNatHelper.hs
+++ b/test/TestNatHelper.hs
@@ -43,5 +43,5 @@
         validateNestedList ([] :: [()])
           @?= Left "validateNestedListC: ixes=[]:no data!"
     , testCase "validateNestedList" $
-        validateNestedList [[1 :: Int, 2], [1, 2], [1, 2, 3]] @?= Left "validateNestedListC: lengths=[2,2,3] ixes=[3P]"
+        validateNestedList [[1 :: Int, 2], [1, 2], [1, 2, 3]] @?= Left "validateNestedListC: lengths=[2,2,3] ixes=[_3P]"
     ]