finitary 2.2.0.1 → 2.2.1.0

raw patch · 4 files changed

+213/−28 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

CHANGELOG.md +7/−0
finitary.cabal +20/−7
src/Data/Finitary.hs +183/−20
test/Main.hs +3/−1

CHANGELOG.md view

@@ -1,5 +1,12 @@ # Revision history for finitary
 
+## 2.2.1.0 -- 2026-08-06
+
+* Adds the `typechecker-plugins` manual flag.
+  Disable this flag to compile the library without using typechecker plugins.
+  This does not change the API of the library, but it does entail passing
+  more `KnownNat` dictionaries around at runtime.
+
 ## 2.2.0.1 -- 2026-04-18
 
 * Relax upper bounds:

finitary.cabal view

@@ -1,6 +1,6 @@ cabal-version:      2.2
 name:               finitary
-version:            2.2.0.1
+version:            2.2.1.0
 synopsis:           A better, more type-safe Enum.
 description:
   Provides a type class witnessing that a type has
@@ -33,6 +33,14 @@   default: True
   manual: True
 
+flag typechecker-plugins
+  description:
+    Use typechecker plugins in the library.
+    With typechecker plugins disabled, some workarounds are used that may
+    cause additional 'KnownNat' dictionaries to be passed at runtime.
+  default: True
+  manual: True
+
 source-repository head
   type:     git
   location: https://codeberg.org/sheaf/finitary.git
@@ -44,13 +52,18 @@     , base
         >= 4.12     && < 5
     , finite-typelits
-        >= 0.1.4.2 && < 0.3
-    , ghc-typelits-knownnat
-        >= 0.7.2   && < 0.9
-    , ghc-typelits-natnormalise
-        >= 0.7.2   && < 0.10
+        >= 0.1.4.2  && < 0.3
     , template-haskell
-       >= 2.14.0.0 && < 3
+        >= 2.14.0.0 && < 3
+
+  if flag(typechecker-plugins)
+    cpp-options:
+      -DTCPLUGINS
+    build-depends:
+      , ghc-typelits-knownnat
+          >= 0.7.2   && < 0.9
+      , ghc-typelits-natnormalise
+          >= 0.7.2   && < 0.10
 
   if flag(bitvec)
     cpp-options:

src/Data/Finitary.hs view

@@ -1,11 +1,13 @@ {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstrainedClassMethods #-}
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MagicHash #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE Trustworthy #-}
@@ -15,9 +17,16 @@ {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE NoStarIsType #-}
 {-# LANGUAGE PatternSynonyms #-}
+
+#ifdef TCPLUGINS
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+#endif
 
+#if __GLASGOW_HASKELL__ >= 914
+{-# OPTIONS_GHC -Wno-pattern-namespace-specifier #-}
+#endif
+
 {-
  - Copyright (C) 2019-2020  Koz Ross <koz.ross@retro-freedom.nz>
  -
@@ -105,6 +114,9 @@ import Data.Ord (Down (..))
 import Data.Proxy (Proxy (..))
 import Data.Semigroup (All, Any, Dual, First, Last, Max, Min, Product, Sum)
+#if !defined(TCPLUGINS) || defined(VECTOR)
+import Data.Type.Equality ((:~:) (..))
+#endif
 import Data.Void (Void)
 import Data.Word (Word16, Word32, Word64, Word8)
 import GHC.Exts (proxy#)
@@ -121,9 +133,13 @@     to,
   )
 import GHC.TypeNats
+#ifndef TCPLUGINS
+import Unsafe.Coerce (unsafeCoerce)
+#endif
 
 -- finitary
 import Data.Finitary.TH
+  ( charCardinality, cardinalityOf, adjustmentOf )
 
 -- finite-typelits
 import Data.Finite
@@ -150,7 +166,6 @@ import Control.Monad (forM_)
 import Control.Monad.Primitive (PrimMonad (..))
 import Control.Monad.ST (ST, runST)
-import Data.Type.Equality ((:~:) (..))
 import Foreign.Storable (Storable)
 
 -- finite-typelits
@@ -290,15 +305,35 @@   {-# INLINE gToFinite #-}
   gToFinite = toFinite . unK1
 
-instance (GFinitary a, GFinitary b) => GFinitary (a :+: b) where
+instance
+  ( GFinitary a
+  , GFinitary b
+#ifndef TCPLUGINS
+  , KnownNat (GCardinality a + GCardinality b)
+#endif
+  ) => GFinitary (a :+: b) where
   type GCardinality (a :+: b) = GCardinality a + GCardinality b
   {-# INLINE gFromFinite #-}
   gFromFinite = either (L1 . gFromFinite) (R1 . gFromFinite) . separateSum
   {-# INLINABLE gToFinite #-}
-  gToFinite (L1 x) = weakenN . gToFinite $ x
-  gToFinite (R1 x) = shiftN . gToFinite $ x
+  gToFinite (L1 x) =
+#ifndef TCPLUGINS
+    claimLE @( GCardinality a ) @( GCardinality a + GCardinality b ) $
+#endif
+    weakenN . gToFinite $ x
+  gToFinite (R1 x) =
+#ifndef TCPLUGINS
+    claimLE @( GCardinality b ) @( GCardinality a + GCardinality b ) $
+#endif
+    shiftN . gToFinite $ x
 
-instance (GFinitary a, GFinitary b) => GFinitary (a :*: b) where
+instance
+  ( GFinitary a
+  , GFinitary b
+#ifndef TCPLUGINS
+  , KnownNat (GCardinality a * GCardinality b)
+#endif
+  ) => GFinitary (a :*: b) where
   type GCardinality (a :*: b) = GCardinality a * GCardinality b
   {-# INLINABLE gFromFinite #-}
   gFromFinite i =
@@ -553,23 +588,61 @@   previous = fmap dec . guarded (/= minBound)
 
 -- | @Maybe a@ introduces one additional inhabitant (namely, 'Nothing') to @a@.
-instance (Finitary a) => Finitary (Maybe a)
+instance ( Finitary a
+#ifndef TCPLUGINS
+         , KnownNat (1 + Cardinality a)
+#endif
+         ) => Finitary (Maybe a)
 
 -- | The sum of two finite types will also be finite, with a cardinality equal
 -- to the sum of their cardinalities.
-instance (Finitary a, Finitary b) => Finitary (Either a b)
+instance ( Finitary a, Finitary b
+#ifndef TCPLUGINS
+         , KnownNat (Cardinality a + Cardinality b)
+#endif
+         ) => Finitary (Either a b)
 
 -- | The product of two finite types will also be finite, with a cardinality
 -- equal to the product of their cardinalities.
-instance (Finitary a, Finitary b) => Finitary (a, b)
+instance ( Finitary a, Finitary b
+#ifndef TCPLUGINS
+         , KnownNat (Cardinality a * Cardinality b)
+#endif
+         ) => Finitary (a, b)
 
-instance (Finitary a, Finitary b, Finitary c) => Finitary (a, b, c)
+instance ( Finitary a, Finitary b, Finitary c
+#ifndef TCPLUGINS
+         , KnownNat (Cardinality a * (Cardinality b * Cardinality c))
+         , KnownNat (Cardinality b * Cardinality c)
+#endif
+         ) => Finitary (a, b, c)
 
-instance (Finitary a, Finitary b, Finitary c, Finitary d) => Finitary (a, b, c, d)
+instance ( Finitary a, Finitary b, Finitary c, Finitary d
+#ifndef TCPLUGINS
+         , KnownNat ((Cardinality a * Cardinality b) * (Cardinality c * Cardinality d))
+         , KnownNat (Cardinality a * Cardinality b)
+         , KnownNat (Cardinality c * Cardinality d)
+#endif
+         ) => Finitary (a, b, c, d)
 
-instance (Finitary a, Finitary b, Finitary c, Finitary d, Finitary e) => Finitary (a, b, c, d, e)
+instance ( Finitary a, Finitary b, Finitary c, Finitary d, Finitary e
+#ifndef TCPLUGINS
+         , KnownNat ((Cardinality a * Cardinality b) * (Cardinality c * (Cardinality d * Cardinality e)))
+         , KnownNat (Cardinality a * Cardinality b)
+         , KnownNat (Cardinality c * (Cardinality d * Cardinality e))
+         , KnownNat (Cardinality d * Cardinality e)
+#endif
+         ) => Finitary (a, b, c, d, e)
 
-instance (Finitary a, Finitary b, Finitary c, Finitary d, Finitary e, Finitary f) => Finitary (a, b, c, d, e, f)
+instance ( Finitary a, Finitary b, Finitary c, Finitary d, Finitary e, Finitary f
+#ifndef TCPLUGINS
+         , KnownNat ((Cardinality a * (Cardinality b * Cardinality c)) * (Cardinality d * (Cardinality e * Cardinality f)))
+         , KnownNat (Cardinality a * (Cardinality b * Cardinality c))
+         , KnownNat (Cardinality b * Cardinality c)
+         , KnownNat (Cardinality d * (Cardinality e * Cardinality f))
+         , KnownNat (Cardinality e * Cardinality f)
+#endif
+         ) => Finitary (a, b, c, d, e, f)
 
 instance (Finitary a) => Finitary (Const a b)
 
@@ -608,7 +681,11 @@ -- with the ordering determined by the @Finitary a@ instance (thus, the
 -- \'first\' such @Vector@ is the one where each element is @start :: a@, and
 -- the \'last\' is the one where each element is @end :: a@).
-instance (Finitary a, KnownNat n) => Finitary (VS.Vector n a) where
+instance ( Finitary a, KnownNat n
+#ifndef TCPLUGINS
+         , KnownNat (Cardinality a ^ n)
+#endif
+         ) => Finitary (VS.Vector n a) where
   type Cardinality (VS.Vector n a) = Cardinality a ^ n
   {-# INLINABLE fromFinite #-}
   fromFinite i = runST (go i)
@@ -621,7 +698,11 @@   {-# INLINE toFinite #-}
   toFinite = roll
 
-instance (Finitary a, VUMS.Unbox a, KnownNat n) => Finitary (VUS.Vector n a) where
+instance ( Finitary a, VUMS.Unbox a, KnownNat n
+#ifndef TCPLUGINS
+         , KnownNat (Cardinality a ^ n)
+#endif
+         ) => Finitary (VUS.Vector n a) where
   type Cardinality (VUS.Vector n a) = Cardinality a ^ n
   {-# INLINABLE fromFinite #-}
   fromFinite i = runST (go i)
@@ -634,7 +715,11 @@   {-# INLINE toFinite #-}
   toFinite = roll
 
-instance (Finitary a, Storable a, KnownNat n) => Finitary (VSS.Vector n a) where
+instance ( Finitary a, Storable a, KnownNat n
+#ifndef TCPLUGINS
+         , KnownNat (Cardinality a ^ n)
+#endif
+         ) => Finitary (VSS.Vector n a) where
   type Cardinality (VSS.Vector n a) = Cardinality a ^ n
   {-# INLINABLE fromFinite #-}
   fromFinite i = runST (go i)
@@ -647,21 +732,41 @@   {-# INLINE toFinite #-}
   toFinite = roll
 
-unroll :: forall a m v n. (Finitary a, PrimMonad m, KnownNat n, VGM.MVector v a) => VGMS.MVector v n (PrimState m) a -> Finite (Cardinality a ^ n) -> m ()
+unroll
+  :: forall a m v n
+  .  ( Finitary a, PrimMonad m, KnownNat n, VGM.MVector v a )
+  => VGMS.MVector v n (PrimState m) a
+  -> Finite (Cardinality a ^ n)
+  -> m ()
 unroll v acc =
   forM_ @_ @_ @_ @()
     (isLE (Proxy @1) (Proxy @n))
-    ( \Refl -> do
-        let (d, r) = separateProduct @(Cardinality a ^ (n -1)) @(Cardinality a) acc
+    ( \ _pf@Refl ->
+#ifndef TCPLUGINS
+      withPeel @a @n _pf $
+#endif
+      do
+        let (d, r) = separateProduct @(Cardinality a ^ (n - 1)) @(Cardinality a) acc
         let x = fromFinite r
         VGMS.write v 0 x
         unroll (VGMS.tail v) d
     )
 
-roll :: forall a v n. (Finitary a, VG.Vector v a, KnownNat n) => VGS.Vector v n a -> Finite (Cardinality a ^ n)
+roll
+  :: forall a v n
+  .  ( Finitary a, VG.Vector v a, KnownNat n
+#ifndef TCPLUGINS
+     , KnownNat (Cardinality a ^ n)
+#endif
+     )
+  => VGS.Vector v n a
+  -> Finite (Cardinality a ^ n)
 roll v = case isLE (Proxy @1) (Proxy @n) of
   Nothing -> 0
-  Just Refl ->
+  Just _pf@Refl ->
+#ifndef TCPLUGINS
+    withPeel @a @n _pf $
+#endif
     let (h, t) = (VGS.head v, VGS.tail v)
      in combineProduct (roll t, toFinite h)
 #endif
@@ -728,3 +833,61 @@ {-# INLINE opp #-}
 opp :: forall a. (KnownNat (Cardinality a)) => Finite (Cardinality a) -> Finite (Cardinality a)
 opp = ( maxBound - )
+
+--------------------------------------------------------------------------------
+-- Workarounds when typechecker plugins aren't available.
+
+#ifndef TCPLUGINS
+
+-- | Claim @a <= b@, when a typechecker plugin would otherwise prove it.
+claimLE
+  :: forall (a :: Nat) (b :: Nat) r. ( a <= b => r ) -> r
+claimLE f
+  | Refl <- unsafeCoerce Refl :: ( a <=? b ) :~: True
+  = f
+{-# INLINE claimLE #-}
+
+#ifdef VECTOR
+-- | Claim @a~b@, when a typechecker plugin would otherwise prove it.
+claimEq
+  :: forall (a :: Nat) (b :: Nat) r. ( a ~ b => r ) -> r
+claimEq f
+  | Refl <- unsafeCoerce Refl :: a :~: b
+  = f
+{-# INLINE claimEq #-}
+
+-- | Claim @KnownNat n@, when a typechecker plugin would otherwise prove it.
+claimKN
+  :: forall n r. Natural -> ( KnownNat n => r ) -> r
+claimKN i f = case someNatVal i of
+  SomeNat ( _ :: Proxy m )
+    | Refl <- ( unsafeCoerce Refl :: n :~: m )
+    -> f
+{-# INLINE claimKN #-}
+
+-- | Bring into scope the facts needed to peel the first element off a vector
+-- of length @n@ with elements in @a@, given a proof that @n@ is non-zero.
+withPeel
+  :: forall a n r
+  .  ( Finitary a, KnownNat n )
+  => ( 1 <=? n ) :~: True
+  -> ( ( n ~ 1 + (n - 1)
+       , Cardinality a ^ n ~ (Cardinality a ^ (n - 1)) * Cardinality a
+       , KnownNat (n - 1)
+       , KnownNat (Cardinality a ^ (n - 1))
+       ) => r
+     )
+  -> r
+withPeel Refl f =
+  claimEq @n @( 1 + (n - 1) ) $
+  claimEq @( Cardinality a ^ n ) @( (Cardinality a ^ (n - 1)) * Cardinality a ) $
+  claimKN @(n - 1) m $
+  claimKN @(Cardinality a ^ (n - 1)) (natVal' @(Cardinality a) proxy# ^ m) $
+  f
+  where
+    m :: Natural
+    m = natVal' @n proxy# - 1
+{-# INLINE withPeel #-}
+
+#endif
+#endif

test/Main.hs view

@@ -6,6 +6,9 @@ {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+
 {-
  - Copyright (C) 2019  Koz Ross <koz.ross@retro-freedom.nz>
  -
@@ -276,4 +279,3 @@     previous (start @a) `shouldBe` Nothing
   it ("(end :: " <> name <> ") should have no successor") $
     next (end @a) `shouldBe` Nothing
-