Elide unsafeCoerce from promoted nats and select

changelog/2024-11-16T11_59_31+01_00_avoid_using_unsafecoerce

@@ -0,0 +1 @@
+CHANGED: `select` and `selectI` now use `<=` constraints instead of `CmpNat`.

clash-prelude/src/Clash/Promoted/Nat.hs

@@ -1,7 +1,7 @@
 {-|
 Copyright  :  (C) 2013-2016, University of Twente,
                   2016     , Myrtle Software Ltd
-                  2022     , QBayLogic B.V.
+                  2022-2024, QBayLogic B.V.
 License    :  BSD2 (see the file LICENSE)
 Maintainer :  QBayLogic B.V. <[email protected]>
 -}
@@ -70,10 +70,22 @@ module Clash.Promoted.Nat
   )
 where
 
+#if MIN_VERSION_base(4,16,0)
+import Data.Constraint    (Dict(..), (:-)(..))
+import Data.Constraint.Nat (euclideanNat)
+#endif
 import Data.Kind          (Type)
+#if MIN_VERSION_base(4,16,0)
+import Data.Type.Equality ((:~:)(..))
+import Data.Type.Ord      (OrderingI(..))
+#endif
 import GHC.Show           (appPrec)
 import GHC.TypeLits       (KnownNat, Nat, type (+), type (-), type (*),
-                           type (^), type (<=), natVal)
+                           type (^), type (<=),
+#if MIN_VERSION_base(4,16,0)
+                           cmpNat, sameNat,
+#endif
+                           natVal)
 import GHC.TypeLits.Extra (CLog, FLog, Div, Log, Mod, Min, Max)
 import GHC.Natural        (naturalFromInteger)
 import Language.Haskell.TH (appT, conT, litT, numTyLit, sigE)
@@ -82,7 +94,9 @@ import Language.Haskell.TH.Syntax (Lift (..))
 import Language.Haskell.TH.Compat
 #endif
 import Numeric.Natural    (Natural)
+#if !MIN_VERSION_base(4,16,0)
 import Unsafe.Coerce      (unsafeCoerce)
+#endif
 
 import Clash.Annotations.Primitive (hasBlackBox)
 import Clash.XException   (ShowX (..), showsPrecXWith)
@@ -184,11 +198,20 @@ instance KnownNat n => ShowX (UNat n) where
 --
 -- __NB__: Not synthesizable
 toUNat :: forall n . SNat n -> UNat n
+#if MIN_VERSION_base(4,16,0)
+toUNat p@SNat = case cmpNat (SNat @1) p of
+  LTI -> USucc (toUNat @(n - 1) (predSNat p))
+  EQI -> USucc UZero
+  GTI -> case sameNat p (SNat @0) of
+    Just Refl -> UZero
+    _ -> error "toUNat: impossible: 1 > n and n /= 0 for (n :: Nat)"
+#else
 toUNat p@SNat = fromI @n (snatToInteger p)
   where
     fromI :: forall m . Integer -> UNat m
     fromI 0 = unsafeCoerce @(UNat 0) @(UNat m) UZero
     fromI n = unsafeCoerce @(UNat ((m-1)+1)) @(UNat m) (USucc (fromI @(m-1) (n - 1)))
+#endif
 
 -- | Convert a unary-encoded natural number to its singleton representation
 --
@@ -338,10 +361,20 @@ deriving instance Show (SNatLE a b)
 
 -- | Get an ordering relation between two SNats
 compareSNat :: forall a b . SNat a -> SNat b -> SNatLE a b
+#if MIN_VERSION_base(4,16,0)
+compareSNat a@SNat b@SNat = case cmpNat a b of
+  LTI -> SNatLE
+  EQI -> SNatLE
+  GTI -> case cmpNat (succSNat b) a of
+    LTI -> SNatGT
+    EQI -> SNatGT
+    GTI -> error "compareSNat: impossible: a > b and b + 1 > a"
+#else
 compareSNat a b =
   if snatToInteger a <= snatToInteger b
      then unsafeCoerce (SNatLE @0 @0)
      else unsafeCoerce (SNatGT @1 @0)
+#endif
 
 -- | Base-2 encoded natural number
 --
@@ -404,14 +437,28 @@ showBNat = go []
 -- | Convert a singleton natural number to its base-2 representation
 --
 -- __NB__: Not synthesizable
-toBNat :: SNat n -> BNat n
+toBNat :: forall n. SNat n -> BNat n
+#if MIN_VERSION_base(4,16,0)
+toBNat s@SNat = case cmpNat (SNat @1) s of
+  LTI -> case euclideanNat @2 @n of
+    Sub Dict -> case sameNat (SNat @(n `Mod` 2)) (SNat @0) of
+      Just Refl -> B0 (toBNat (SNat @(n `Div` 2)))
+      Nothing -> case sameNat (SNat @(n `Mod` 2)) (SNat @1) of
+        Just Refl -> B1 (toBNat (SNat @(n `Div` 2)))
+        Nothing -> error "toBNat: impossible: n mod 2 is either 0 or 1"
+  EQI -> B1 BT
+  GTI -> case sameNat s (SNat @0) of
+    Just Refl -> BT
+    _ -> error "toBNat: impossible: 1 > n and n /= 0 for (n :: Nat)"
+#else
 toBNat s@SNat = toBNat' (snatToInteger s)
   where
     toBNat' :: forall m . Integer -> BNat m
     toBNat' 0 = unsafeCoerce BT
     toBNat' n = case n `divMod` 2 of
       (n',1) -> unsafeCoerce (B1 (toBNat' @(Div (m-1) 2) n'))
       (n',_) -> unsafeCoerce (B0 (toBNat' @(Div m 2) n'))
+#endif
 
 -- | Convert a base-2 encoded natural number to its singleton representation
 --

clash-prelude/src/Clash/Sized/Vector.hs

@@ -116,7 +116,7 @@ import qualified Data.Foldable    as F
 import Data.Kind                  (Type)
 import Data.Proxy                 (Proxy (..))
 import Data.Singletons            (TyFun,Apply,type (@@))
-import GHC.TypeLits               (CmpNat, KnownNat, Nat, type (+), type (-), type (*),
+import GHC.TypeLits               (KnownNat, Nat, type (+), type (-), type (*),
                                    type (^), type (<=), natVal)
 import GHC.Base                   (Int(I#),Int#,isTrue#)
 import GHC.Generics               hiding (Fixity (..))
@@ -138,7 +138,6 @@ import qualified Data.String.Interpolate as I
 import qualified Prelude          as P
 import Test.QuickCheck
   (Arbitrary(arbitrary, shrink), CoArbitrary(coarbitrary))
-import Unsafe.Coerce              (unsafeCoerce)
 
 import Clash.Annotations.Primitive
   (Primitive(InlineYamlPrimitive), HDL(..), dontTranslate, hasBlackBox)
@@ -1687,18 +1686,24 @@ at n xs = head $ snd $ splitAt n xs
 -- 2 :> 4 :> 6 :> Nil
 -- >>> select d1 d2 d3 (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
 -- 2 :> 4 :> 6 :> Nil
-select :: (CmpNat (i + s) (s * n) ~ 'GT)
+select :: forall i s n f a. s * n + 1 <= i + s
        => SNat f
        -> SNat s
        -> SNat n
        -> Vec (f + i) a
        -> Vec n a
 select f s n xs = select' (toUNat n) $ drop f xs
-  where
-    select' :: UNat n -> Vec i a -> Vec n a
-    select' UZero      _               = Nil
-    select' (USucc n') vs@(x `Cons` _) = x `Cons`
-                                         select' n' (drop s (unsafeCoerce vs))
+ where
+  select' :: forall m j b. (s * m + 1 <= j + s) => UNat m -> Vec j b -> Vec m b
+  select' m vs = case m of
+    UZero -> Nil
+    USucc UZero -> head @(j - 1) vs `Cons` Nil
+    USucc m'@(USucc _) -> case deduce @(s * (m - 1) + 1) @j Proxy Proxy of
+      Dict -> head @(j - 1) vs `Cons` select' m' (drop @s @(j - s) s vs)
+
+  deduce :: e + s <= k + s => p e -> p k -> Dict (e <= k)
+  deduce _ _ = Dict
+
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE select #-}
 {-# ANN select hasBlackBox #-}
@@ -1708,7 +1713,7 @@ select f s n xs = select' (toUNat n) $ drop f xs
 --
 -- >>> selectI d1 d2 (1:>2:>3:>4:>5:>6:>7:>8:>Nil) :: Vec 2 Int
 -- 2 :> 4 :> Nil
-selectI :: (CmpNat (i + s) (s * n) ~ 'GT, KnownNat n)
+selectI :: (1 <= s, s * n + 1 <= i + s, KnownNat n)
         => SNat f
         -> SNat s
         -> Vec (f + i) a