4 files changed, 12 insertions, 12 deletions
diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs
index 408bf8a..313e9de 100644
--- a/src/Data/Array/Nested/Convert.hs
+++ b/src/Data/Array/Nested/Convert.hs
@@ -103,7 +103,7 @@ withShsFromShR ZSR k = k ZSS
 withShsFromShR (n :$: sh) k =
   withShsFromShR sh $ \sh' ->
     withSomeSNat (fromIntegral @Int @Integer n) $ \case
-      Just sn@SNat -> k (sn :$$ sh')
+      Just sn -> k (sn :$$ sh')
       Nothing -> error $ "withShsFromShR: negative dimension size (" ++ show n ++ ")"
 
 shsFromShX :: IShX (MapJust sh) -> ShS sh
@@ -113,13 +113,13 @@ shsFromShX = coerce
 -- @sh'@ is @MapJust@ of something, use 'shsFromShX' instead.
 withShsFromShX :: IShX sh' -> (forall sh. Rank sh ~ Rank sh' => ShS sh -> r) -> r
 withShsFromShX ZSX k = k ZSS
-withShsFromShX (SKnown sn@SNat :$% sh) k =
+withShsFromShX (SKnown sn :$% sh) k =
   withShsFromShX sh $ \sh' ->
     k (sn :$$ sh')
 withShsFromShX (SUnknown n :$% sh) k =
   withShsFromShX sh $ \sh' ->
     withSomeSNat (fromIntegral @Int @Integer n) $ \case
-      Just sn@SNat -> k (sn :$$ sh')
+      Just sn -> k (sn :$$ sh')
       Nothing -> error $ "withShsFromShX: negative SUnknown dimension size (" ++ show n ++ ")"
 
 -- If it ever matters for performance, this is unsafeCoercible.
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs
index d2557b6..9254728 100644
--- a/src/Data/Array/Nested/Permutation.hs
+++ b/src/Data/Array/Nested/Permutation.hs
@@ -301,11 +301,11 @@ type family MapSucc is where
   MapSucc (i : is) = i + 1 : MapSucc is
 
 permShift1 :: Perm l -> Perm (0 : MapSucc l)
-permShift1 = (SNat @0 `PCons`) . permMapSucc
+permShift1 = (SZ `PCons`) . permMapSucc
   where
     permMapSucc :: Perm l -> Perm (MapSucc l)
     permMapSucc PNil = PNil
-    permMapSucc ((SNat :: SNat i) `PCons` ns) = SNat @(i + 1) `PCons` permMapSucc ns
+    permMapSucc (sn `PCons` ns) = snatSucc sn `PCons` permMapSucc ns
 
 -- | @PermId n@ is the type of the identity permutation of length @n@.
 type family PermId n where
@@ -340,11 +340,11 @@ type family MapPlusN n is where
 
 -- TODO: instead of permAppend and permShiftN define permComp :: Perm l1 -> Perm l2 -> Perm (l1 ++ MapPlusN (Rank l1) l2), where all three are valid permutations
 permShiftN :: forall n l. SNat n -> Perm l -> Perm (PermId n ++ MapPlusN n l)
-permShiftN n@SNat = (permId n `permAppend`) . permMapPlusN
+permShiftN n = (permId n `permAppend`) . permMapPlusN
   where
     permMapPlusN :: Perm l1 -> Perm (MapPlusN n l1)
     permMapPlusN PNil = PNil
-    permMapPlusN ((SNat :: SNat i) `PCons` ns) = SNat @(i + n) `PCons` permMapPlusN ns
+    permMapPlusN (sn `PCons` ns) = snatPlus sn n `PCons` permMapPlusN ns
 
 
 -- * Lemmas
diff --git a/src/Data/Array/Nested/Ranked.hs b/src/Data/Array/Nested/Ranked.hs
index 26c9203..2d8b624 100644
--- a/src/Data/Array/Nested/Ranked.hs
+++ b/src/Data/Array/Nested/Ranked.hs
@@ -65,7 +65,7 @@ rindexPartial (Ranked arr) idx =
 -- 'rgeneratePrim'.
 rgenerate :: forall n a. KnownElt a => IShR n -> (IIxR n -> a) -> Ranked n a
 rgenerate sh f
-  | sn@SNat <- shrRank sh
+  | sn <- shrRank sh
   , Dict <- lemKnownReplicate sn
   , Refl <- lemRankReplicate sn
   = Ranked (mgenerate (shxFromShR sh) (f . ixrFromIxX))
@@ -117,11 +117,11 @@ rsumAllPrim (Ranked arr) = msumAllPrim arr
 
 rtranspose :: forall n a. Elt a => PermR -> Ranked n a -> Ranked n a
 rtranspose perm arr
-  | sn@SNat <- rrank arr
+  | sn <- rrank arr
   , Dict <- lemKnownReplicate sn
-  , length perm <= fromIntegral (natVal (Proxy @n))
+  , length perm <= fromSNat' sn
   = rlift sn
-          (\ssh' -> X.transposeUntyped (natSing @n) ssh' perm)
+          (\ssh' -> X.transposeUntyped sn ssh' perm)
           arr
   | otherwise
   = error "Data.Array.Nested.rtranspose: Permutation longer than rank of array"
diff --git a/src/Data/Array/Nested/Shaped.hs b/src/Data/Array/Nested/Shaped.hs
index 62867a1..f1636c5 100644
--- a/src/Data/Array/Nested/Shaped.hs
+++ b/src/Data/Array/Nested/Shaped.hs
@@ -247,7 +247,7 @@ sreplicatePrim :: forall sh a. PrimElt a => ShS sh -> a -> Shaped sh a
 sreplicatePrim sh x = sfromPrimitive (sreplicatePrimP sh x)
 
 sslice :: Elt a => SNat i -> SNat n -> Shaped (i + n + k : sh) a -> Shaped (n : sh) a
-sslice i n@SNat arr =
+sslice i n arr =
   let _ :$$ sh = sshape arr
   in slift (n :$$ sh) (\_ -> X.slice i n) arr