From 5623e4d4e613b89786a225265a4d8373680096f3 Mon Sep 17 00:00:00 2001
From: Justin Le <justin@jle.im>
Date: Wed, 25 May 2016 02:20:49 -0700
Subject: re-implemented exactDim and exactLength in terms of the native GHC
 TypeLits API with sameNat

---
 packages/base/src/Numeric/LinearAlgebra/Static.hs | 19 ++++++++-----------
 1 file 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
-- 
cgit v1.2.3