re-implemented exactDim and exactLength in terms of the native GHC TypeLits API with sameNat

1 files changed, 8 insertions, 11 deletions

diff --git a/packages/base/src/Numeric/LinearAlgebra/Static.hs b/packages/base/src/Numeric/LinearAlgebra/Static.hs
index 3e772b2..a55ae44 100644
--- a/packages/base/src/Numeric/LinearAlgebra/Static.hs
+++ b/packages/base/src/Numeric/LinearAlgebra/Static.hs
@@ -78,6 +78,7 @@ import Data.Proxy(Proxy(..))
 import Internal.Static
 import Control.Arrow((***))
 import Text.Printf
+import Data.Type.Equality ((:~:)(Refl))
 
 ud1 :: R n -> Vector ℝ
 ud1 (R (Dim v)) = v
@@ -444,11 +445,9 @@ exactLength
     :: forall n m . (KnownNat n, KnownNat m)
     => R m
     -> Maybe (R n)
-exactLength v
-    | natVal (Proxy :: Proxy n) == natVal (Proxy :: Proxy m)
-        = Just (mkR (unwrap v))
-    | otherwise
-        = Nothing
+exactLength v = do
+    Refl <- sameNat (Proxy :: Proxy n) (Proxy :: Proxy m)
+    return $ mkR (unwrap v)
 
 withMatrix
     :: forall z
@@ -470,12 +469,10 @@ exactDims
     :: forall n m j k . (KnownNat n, KnownNat m, KnownNat j, KnownNat k)
     => L m n
     -> Maybe (L j k)
-exactDims m
-    | natVal (Proxy :: Proxy m) == natVal (Proxy :: Proxy j)
-   && natVal (Proxy :: Proxy n) == natVal (Proxy :: Proxy k)
-        = Just (mkL (unwrap m))
-    | otherwise
-        = Nothing
+exactDims m = do
+    Refl <- sameNat (Proxy :: Proxy m) (Proxy :: Proxy j)
+    Refl <- sameNat (Proxy :: Proxy n) (Proxy :: Proxy k)
+    return $ mkL (unwrap m)
 
 randomVector
     :: forall n . KnownNat n