From 96ec7003f054333692ab18d17659accf6b0fef6f Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Sun, 29 Jun 2025 15:44:54 +0200
Subject: Permutations: withKnownPerm

---
 src/Data/Array/Nested/Permutation.hs | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'src/Data/Array')

diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs
index 1f90dc5..af9efed 100644
--- a/src/Data/Array/Nested/Permutation.hs
+++ b/src/Data/Array/Nested/Permutation.hs
@@ -24,6 +24,7 @@ import Data.Proxy
 import Data.Type.Bool
 import Data.Type.Equality
 import Data.Type.Ord
+import GHC.Exts (withDict)
 import GHC.TypeError
 import GHC.TypeLits
 import GHC.TypeNats qualified as TN
@@ -125,6 +126,9 @@ class KnownPerm l where makePerm :: Perm l
 instance KnownPerm '[] where makePerm = PNil
 instance (KnownNat n, KnownPerm l) => KnownPerm (n : l) where makePerm = natSing `PCons` makePerm
 
+withKnownPerm :: forall l r. Perm l -> (KnownPerm l => r) -> r
+withKnownPerm = withDict @(KnownPerm l)
+
 -- | Untyped permutations for ranked arrays
 type PermR = [Int]
 
@@ -230,7 +234,7 @@ permInverse = \perm k ->
                ++ " ; invperm = " ++ show invperm)
       (permCheckPermutation invperm
         (k invperm
-           (\ssh -> case provePermInverse perm invperm ssh of
+           (\ssh -> case permCheckInverse perm invperm ssh of
                       Just eq -> eq
                       Nothing -> error $ "permInverse: did not generate inverse? perm = " ++ show perm
                                              ++ " ; invperm = " ++ show invperm)))
@@ -244,9 +248,9 @@ permInverse = \perm k ->
         toHList [] k = k PNil
         toHList (n : ns) k = toHList ns $ \l -> TN.withSomeSNat n $ \sn -> k (PCons sn l)
 
-    provePermInverse :: Perm is -> Perm is' -> StaticShX sh
+    permCheckInverse :: Perm is -> Perm is' -> StaticShX sh
                      -> Maybe (Permute is' (Permute is sh) :~: sh)
-    provePermInverse perm perminv ssh =
+    permCheckInverse perm perminv ssh =
       ssxEqType (ssxPermute perminv (ssxPermute perm ssh)) ssh
 
 type family MapSucc is where
-- 
cgit v1.2.3-70-g09d2