From 752ac7a911296cc7fdae6c97d4dafbac1b78be44 Mon Sep 17 00:00:00 2001
From: Koz Ross <koz.ross@retro-freedom.nz>
Date: Wed, 18 Dec 2024 12:56:17 +1300
Subject: [PATCH 1/4] PNatural

---
 CHANGELOG.md                 |  1 +
 Plutarch/Internal/Lift.hs    |  1 +
 Plutarch/Internal/Numeric.hs | 82 +++++++++++++++++++++++++++++++++---
 Plutarch/Prelude.hs          |  3 ++
 4 files changed, 82 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5e370baf4..69edfd154 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -40,6 +40,7 @@
 * New methods for `Data` and Scott encoding derivation
 * `optimizeTerm` for separate optimization via UPLC from compilation
 * New numerical hierarchy in `Plutarch.Internal.Numeric`, plus new instances
+* `PNatural` type, corresponding to the Haskell `Natural`
 
 ## Changed
 
diff --git a/Plutarch/Internal/Lift.hs b/Plutarch/Internal/Lift.hs
index e3fab2d64..a6f256df6 100644
--- a/Plutarch/Internal/Lift.hs
+++ b/Plutarch/Internal/Lift.hs
@@ -33,6 +33,7 @@ module Plutarch.Internal.Lift (
   getPLifted,
   PLiftedClosed (..),
   LiftError (..),
+  punsafeCoercePLifted,
 ) where
 
 import Plutarch.Builtin.BLS (
diff --git a/Plutarch/Internal/Numeric.hs b/Plutarch/Internal/Numeric.hs
index bf73d7fe4..63cc24806 100644
--- a/Plutarch/Internal/Numeric.hs
+++ b/Plutarch/Internal/Numeric.hs
@@ -5,6 +5,7 @@ module Plutarch.Internal.Numeric (
   -- * Types
   PPositive,
   Positive,
+  PNatural,
 
   -- * Type classes
   PAdditiveSemigroup (..),
@@ -18,6 +19,8 @@ module Plutarch.Internal.Numeric (
   -- * Functions
   ptryPositive,
   ppositive,
+  ptryNatural,
+  pnatural,
   pbySquaringDefault,
   pdiv,
   pmod,
@@ -28,6 +31,7 @@ module Plutarch.Internal.Numeric (
 import Data.Coerce (coerce)
 import Data.Kind (Type)
 import GHC.Generics (Generic)
+import Numeric.Natural (Natural)
 import Plutarch.Builtin.BLS (
   PBuiltinBLS12_381_G1_Element,
   PBuiltinBLS12_381_G2_Element,
@@ -57,8 +61,16 @@ import Plutarch.Internal.Fix (pfix)
 import Plutarch.Internal.IsData (PIsData)
 import Plutarch.Internal.Lift (
   DeriveNewtypePLiftable,
-  PLiftable,
+  PLiftable (
+    AsHaskell,
+    PlutusRepr,
+    fromPlutarch,
+    fromPlutarchRepr,
+    toPlutarch,
+    toPlutarchRepr
+  ),
   PLifted (PLifted),
+  punsafeCoercePLifted,
  )
 import Plutarch.Internal.Newtype (PlutusTypeNewtype)
 import Plutarch.Internal.Ord (POrd ((#<=)))
@@ -149,6 +161,43 @@ instance Function Positive where
   {-# INLINEABLE function #-}
   function = functionMap @Integer coerce coerce
 
+-- | @since WIP
+newtype PNatural (s :: S) = PNatural (Term s PInteger)
+  deriving stock
+    ( -- | @since WIP
+      Generic
+    )
+  deriving anyclass
+    ( -- | @since WIP
+      PlutusType
+    , -- | @since WIP
+      PIsData
+    , -- | @since WIP
+      PEq
+    , -- | @since WIP
+      POrd
+    )
+
+-- | @since WIP
+instance DerivePlutusType PNatural where
+  type DPTStrat _ = PlutusTypeNewtype
+
+-- | @since WIP
+instance PLiftable PNatural where
+  type AsHaskell PNatural = Natural
+  type PlutusRepr PNatural = Integer
+  {-# INLINEABLE toPlutarchRepr #-}
+  toPlutarchRepr = fromIntegral
+  {-# INLINEABLE toPlutarch #-}
+  toPlutarch = punsafeCoercePLifted . toPlutarch @PInteger . fromIntegral
+  {-# INLINEABLE fromPlutarchRepr #-}
+  fromPlutarchRepr x =
+    if x < 0
+      then Nothing
+      else Just . fromIntegral $ x
+  {-# INLINEABLE fromPlutarch #-}
+  fromPlutarch t = fromIntegral <$> fromPlutarch @PInteger (punsafeCoercePLifted t)
+
 {- | The addition operation.
 
 = Laws
@@ -403,7 +452,7 @@ instance PMultiplicativeMonoid PInteger where
   {-# INLINEABLE pone #-}
   pone = pconstantInteger 1
 
-{- | Partial version of 'PPositive'. Errors if argument is zero.
+{- | Partial version of 'ppositive'. Errors if argument is not positive.
 
 @since WIP
 -}
@@ -411,16 +460,16 @@ ptryPositive :: forall (s :: S). Term s (PInteger :--> PPositive)
 ptryPositive = phoistAcyclic $
   plam $ \i ->
     pif
-      (i #<= pzero)
+      (i #<= pconstantInteger 0)
       (ptraceInfo "ptryPositive: building with non positive" perror)
       (punsafeCoerce i)
 
--- | Build a 'PPositive' from a 'PInteger'. Yields 'PNothing' if argument is zero.
+-- | Build a 'PPositive' from a 'PInteger'. Yields 'PNothing' if argument is not positive.
 ppositive :: Term s (PInteger :--> PMaybe PPositive)
 ppositive = phoistAcyclic $
   plam $ \i ->
     pif
-      (i #<= pzero)
+      (i #<= pconstantInteger 0)
       (pcon PNothing)
       $ pcon . PJust . pcon
       $ PPositive i
@@ -564,3 +613,26 @@ pquot = punsafeBuiltin PLC.QuotientInteger
 -- | @since WIP
 prem :: forall (s :: S). Term s (PInteger :--> PInteger :--> PInteger)
 prem = punsafeBuiltin PLC.RemainderInteger
+
+{- | Partial version of 'pnatural'. Errors if argument is negative.
+
+@since WIP
+-}
+ptryNatural :: forall (s :: S). Term s (PInteger :--> PNatural)
+ptryNatural = phoistAcyclic $ plam $ \i ->
+  pif
+    (i #<= pconstantInteger (-1))
+    (ptraceInfo "ptryNatural: building with negative" perror)
+    (punsafeCoerce i)
+
+{- | Build a 'PNatural' from a 'PInteger'. Yields 'PNothing' if given a negative
+value.
+
+@since WIP
+-}
+pnatural :: forall (s :: S). Term s (PInteger :--> PMaybe PNatural)
+pnatural = phoistAcyclic $ plam $ \i ->
+  pif
+    (i #<= pconstantInteger (-1))
+    (pcon PNothing)
+    (pcon . PJust . pcon . PNatural $ i)
diff --git a/Plutarch/Prelude.hs b/Plutarch/Prelude.hs
index 5ca8c3a71..b7b62bb18 100644
--- a/Plutarch/Prelude.hs
+++ b/Plutarch/Prelude.hs
@@ -164,6 +164,7 @@ module Plutarch.Prelude (
   -- * Numeric
   Positive,
   PPositive,
+  PNatural,
   PAdditiveSemigroup (..),
   PAdditiveMonoid (..),
   PAdditiveGroup (..),
@@ -177,6 +178,8 @@ module Plutarch.Prelude (
   pmod,
   ppositive,
   ptryPositive,
+  pnatural,
+  ptryNatural,
 
   -- * Other
   pto,

From 200f8eed57cad53895426115b371034db6a18336 Mon Sep 17 00:00:00 2001
From: Koz Ross <koz.ross@retro-freedom.nz>
Date: Wed, 18 Dec 2024 13:02:33 +1300
Subject: [PATCH 2/4] Numerical instances for PNatural

---
 Plutarch/Internal/Numeric.hs | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/Plutarch/Internal/Numeric.hs b/Plutarch/Internal/Numeric.hs
index 63cc24806..3ac4236c5 100644
--- a/Plutarch/Internal/Numeric.hs
+++ b/Plutarch/Internal/Numeric.hs
@@ -246,6 +246,13 @@ instance PAdditiveSemigroup PPositive where
   {-# INLINEABLE pscalePositive #-}
   pscalePositive = punsafeBuiltin PLC.MultiplyInteger
 
+-- | @since WIP
+instance PAdditiveSemigroup PNatural where
+  {-# INLINEABLE (#+) #-}
+  x #+ y = punsafeCoerce $ paddInteger # pto x # pto y
+  {-# INLINEABLE pscalePositive #-}
+  pscalePositive = punsafeBuiltin PLC.MultiplyInteger
+
 -- | @since WIP
 instance PAdditiveSemigroup PInteger where
   {-# INLINEABLE (#+) #-}
@@ -288,6 +295,11 @@ instance PAdditiveMonoid PInteger where
   {-# INLINEABLE pzero #-}
   pzero = pconstantInteger 0
 
+-- | @since WIP
+instance PAdditiveMonoid PNatural where
+  {-# INLINEABLE pzero #-}
+  pzero = punsafeCoerce . pconstantInteger $ 0
+
 -- | @since WIP
 instance PAdditiveMonoid PBuiltinBLS12_381_G1_Element where
   {-# INLINEABLE pzero #-}
@@ -425,6 +437,11 @@ instance PMultiplicativeSemigroup PPositive where
   {-# INLINEABLE (#*) #-}
   x #* y = punsafeCoerce $ pmultiplyInteger # pto x # pto y
 
+-- | @since WIP
+instance PMultiplicativeSemigroup PNatural where
+  {-# INLINEABLE (#*) #-}
+  x #* y = punsafeCoerce $ pmultiplyInteger # pto x # pto y
+
 -- | @since WIP
 instance PMultiplicativeSemigroup PInteger where
   {-# INLINEABLE (#*) #-}
@@ -447,6 +464,11 @@ instance PMultiplicativeMonoid PPositive where
   {-# INLINEABLE pone #-}
   pone = punsafeCoerce $ pconstantInteger 1
 
+-- | @since WIP
+instance PMultiplicativeMonoid PNatural where
+  {-# INLINEABLE pone #-}
+  pone = punsafeCoerce $ pconstantInteger 1
+
 -- | @since WIP
 instance PMultiplicativeMonoid PInteger where
   {-# INLINEABLE pone #-}

From bbc9fd63f38ce7fc2441ea21e7e5701b1e44fc59 Mon Sep 17 00:00:00 2001
From: Koz Ross <koz.ross@retro-freedom.nz>
Date: Thu, 19 Dec 2024 10:37:38 +1300
Subject: [PATCH 3/4] Add pscaleNatural, ppowNatural, supplement instances

---
 Plutarch/Internal/Numeric.hs                  | 57 +++++++++++++++++--
 Plutarch/Prelude.hs                           |  1 +
 Plutarch/Rational.hs                          | 12 +++-
 .../src/Plutarch/LedgerApi/V1/Time.hs         |  3 +
 .../Plutarch/Test/Suite/Plutarch/TryFrom.hs   | 10 ++--
 5 files changed, 72 insertions(+), 11 deletions(-)

diff --git a/Plutarch/Internal/Numeric.hs b/Plutarch/Internal/Numeric.hs
index 3ac4236c5..7f1ab07e3 100644
--- a/Plutarch/Internal/Numeric.hs
+++ b/Plutarch/Internal/Numeric.hs
@@ -21,6 +21,7 @@ module Plutarch.Internal.Numeric (
   ppositive,
   ptryNatural,
   pnatural,
+  ppositiveToNatural,
   pbySquaringDefault,
   pdiv,
   pmod,
@@ -198,7 +199,7 @@ instance PLiftable PNatural where
   {-# INLINEABLE fromPlutarch #-}
   fromPlutarch t = fromIntegral <$> fromPlutarch @PInteger (punsafeCoercePLifted t)
 
-{- | The addition operation.
+{- | The addition operation, and the notion of scaling by a positive.
 
 = Laws
 
@@ -276,8 +277,7 @@ instance PAdditiveSemigroup PBuiltinBLS12_381_G2_Element where
   pscalePositive = phoistAcyclic $ plam $ \x p ->
     pbls12_381_G2_scalarMul # pto p # x
 
-{- | The notion of zero, as well as a (kind of) reversal of 'pscalePositive',
-similar to floor division by positive integers.
+{- | The notion of zero, as well as a way to scale by naturals.
 
 = Laws
 
@@ -285,30 +285,56 @@ similar to floor division by positive integers.
 2. @pscalePositive # pzero # n@ @=@
    @pzero@ (@pzero@ does not scale up)
 
+If you define 'pscaleNatural', ensure the following as well:
+
+3. @pscaleNatural # x #$ ppositiveToNatural # p@ @=@
+   @pscalePositive # x # p@
+4. @pscaleNatural # x # pzero@ @=@ @pzero@
+
+The default implementation of 'pscaleNatural' ensures these laws are
+followed.
+
 @since WIP
 -}
 class PAdditiveSemigroup a => PAdditiveMonoid (a :: S -> Type) where
   pzero :: forall (s :: S). Term s a
+  {-# INLINEABLE pscaleNatural #-}
+  pscaleNatural :: forall (s :: S). Term s (a :--> PNatural :--> a)
+  pscaleNatural = phoistAcyclic $ plam $ \x n ->
+    pif
+      (n #== pzero)
+      pzero
+      (pscalePositive # x # punsafeCoerce n)
 
 -- | @since WIP
 instance PAdditiveMonoid PInteger where
   {-# INLINEABLE pzero #-}
   pzero = pconstantInteger 0
+  {-# INLINEABLE pscaleNatural #-}
+  pscaleNatural = punsafeBuiltin PLC.MultiplyInteger
 
 -- | @since WIP
 instance PAdditiveMonoid PNatural where
   {-# INLINEABLE pzero #-}
   pzero = punsafeCoerce . pconstantInteger $ 0
+  {-# INLINEABLE pscaleNatural #-}
+  pscaleNatural = punsafeBuiltin PLC.MultiplyInteger
 
 -- | @since WIP
 instance PAdditiveMonoid PBuiltinBLS12_381_G1_Element where
   {-# INLINEABLE pzero #-}
   pzero = pbls12_381_G1_uncompress # pbls12_381_G1_compressed_zero
+  {-# INLINEABLE pscaleNatural #-}
+  pscaleNatural = phoistAcyclic $ plam $ \x n ->
+    pbls12_381_G1_scalarMul # pto n # x
 
 -- | @since WIP
 instance PAdditiveMonoid PBuiltinBLS12_381_G2_Element where
   {-# INLINEABLE pzero #-}
   pzero = pbls12_381_G2_uncompress # pbls12_381_G2_compressed_zero
+  {-# INLINEABLE pscaleNatural #-}
+  pscaleNatural = phoistAcyclic $ plam $ \x n ->
+    pbls12_381_G2_scalarMul # pto n # x
 
 {- | The notion of additive inverses, and the subtraction operation.
 
@@ -447,17 +473,32 @@ instance PMultiplicativeSemigroup PInteger where
   {-# INLINEABLE (#*) #-}
   x #* y = pmultiplyInteger # x # y
 
-{- | The notion of one (multiplicative identity).
+{- | The notion of one (multiplicative identity), and exponentiation by
+ - naturals.
 
 = Laws
 
 1. @pone #* x@ @=@ @x@ (@pone@ is the left identity of @#*@)
 2. @x #* pone@ @=@ @x@ (@pone@ is the right identity of @#*@)
+3. @ppowPositive # pone # p@ @=@ @pone@ (@pone@ does not scale up)
+
+If you define 'ppowNatural', ensure the following as well:
+
+4. @ppowNatural # x #$ ppositiveToNatural # p@ @=@
+   @ppowPositive # x # p@
+5. @ppowNatural # x # pzero@ @=@ @pone@
 
 @since WIP
 -}
 class PMultiplicativeSemigroup a => PMultiplicativeMonoid (a :: S -> Type) where
   pone :: forall (s :: S). Term s a
+  {-# INLINEABLE ppowNatural #-}
+  ppowNatural :: forall (s :: S). Term s (a :--> PNatural :--> a)
+  ppowNatural = phoistAcyclic $ plam $ \x n ->
+    pif
+      (n #== pzero)
+      pone
+      (ppowPositive # x # punsafeCoerce n)
 
 -- | @since WIP
 instance PMultiplicativeMonoid PPositive where
@@ -658,3 +699,11 @@ pnatural = phoistAcyclic $ plam $ \i ->
     (i #<= pconstantInteger (-1))
     (pcon PNothing)
     (pcon . PJust . pcon . PNatural $ i)
+
+{- | \'Relax\' a 'PPositive' to 'PNatural'. This uses 'punsafeCoerce'
+underneath, but because any positive is also a natural, is safe.
+
+@since WIP
+-}
+ppositiveToNatural :: forall (s :: S). Term s (PPositive :--> PNatural)
+ppositiveToNatural = phoistAcyclic $ plam $ \x -> punsafeCoerce x
diff --git a/Plutarch/Prelude.hs b/Plutarch/Prelude.hs
index b7b62bb18..9f6e1f1b4 100644
--- a/Plutarch/Prelude.hs
+++ b/Plutarch/Prelude.hs
@@ -180,6 +180,7 @@ module Plutarch.Prelude (
   ptryPositive,
   pnatural,
   ptryNatural,
+  ppositiveToNatural,
 
   -- * Other
   pto,
diff --git a/Plutarch/Rational.hs b/Plutarch/Rational.hs
index c3b74b79c..583e94c57 100644
--- a/Plutarch/Rational.hs
+++ b/Plutarch/Rational.hs
@@ -38,10 +38,10 @@ import Plutarch.Internal.Lift (
 import Plutarch.Internal.ListLike (phead, pnil, ptail)
 import Plutarch.Internal.Numeric (
   PAdditiveGroup (pnegate, pscaleInteger, (#-)),
-  PAdditiveMonoid (pzero),
+  PAdditiveMonoid (pscaleNatural, pzero),
   PAdditiveSemigroup (pscalePositive, (#+)),
   PIntegralDomain (pabs, psignum),
-  PMultiplicativeMonoid (pone),
+  PMultiplicativeMonoid (pone, ppowNatural),
   PMultiplicativeSemigroup (ppowPositive, (#*)),
   PPositive,
   PRing (pfromInteger),
@@ -172,6 +172,10 @@ instance PAdditiveSemigroup PRational where
 instance PAdditiveMonoid PRational where
   {-# INLINEABLE pzero #-}
   pzero = pcon . PRational pzero $ pone
+  {-# INLINEABLE pscaleNatural #-}
+  pscaleNatural = phoistAcyclic $ plam $ \x n ->
+    pmatch x $ \(PRational xn xd) ->
+      preduce' # (xn #* pto n) # pto xd
 
 -- | @since WIP
 instance PAdditiveGroup PRational where
@@ -225,6 +229,10 @@ instance PMultiplicativeSemigroup PRational where
 instance PMultiplicativeMonoid PRational where
   {-# INLINEABLE pone #-}
   pone = pcon . PRational pone $ pone
+  {-# INLINEABLE ppowNatural #-}
+  ppowNatural = phoistAcyclic $ plam $ \x n ->
+    pmatch x $ \(PRational xn xd) ->
+      pcon . PRational (ppowNatural # xn # n) $ ppowNatural # xd # n
 
 -- | @since WIP
 instance PRing PRational where
diff --git a/plutarch-ledger-api/src/Plutarch/LedgerApi/V1/Time.hs b/plutarch-ledger-api/src/Plutarch/LedgerApi/V1/Time.hs
index 927d31b44..eb9227be2 100644
--- a/plutarch-ledger-api/src/Plutarch/LedgerApi/V1/Time.hs
+++ b/plutarch-ledger-api/src/Plutarch/LedgerApi/V1/Time.hs
@@ -67,6 +67,9 @@ instance PAdditiveSemigroup PPosixTime where
 instance PAdditiveMonoid PPosixTime where
   {-# INLINEABLE pzero #-}
   pzero = pposixTime pzero
+  {-# INLINEABLE pscaleNatural #-}
+  pscaleNatural = phoistAcyclic $ plam $ \t n ->
+    pposixTime (unPPosixTime t #* pto n)
 
 -- | @since WIP
 instance PAdditiveGroup PPosixTime where
diff --git a/plutarch-testlib/test/Plutarch/Test/Suite/Plutarch/TryFrom.hs b/plutarch-testlib/test/Plutarch/Test/Suite/Plutarch/TryFrom.hs
index 644bb3cbb..e440d6dd3 100644
--- a/plutarch-testlib/test/Plutarch/Test/Suite/Plutarch/TryFrom.hs
+++ b/plutarch-testlib/test/Plutarch/Test/Suite/Plutarch/TryFrom.hs
@@ -276,20 +276,20 @@ fullCheck = unTermCont $ fst <$> TermCont (ptryFrom $ pforgetData sampleStructur
 
 ------------------- Example: untrusted Redeemer ------------------------------------
 
-newtype PNatural (s :: S) = PMkNatural (Term s PInteger)
+newtype PNaturalle (s :: S) = PMkNatural (Term s PInteger)
   deriving stock (Generic)
   deriving anyclass (PlutusType, PIsData, PEq, POrd)
-instance DerivePlutusType PNatural where type DPTStrat _ = PlutusTypeNewtype
+instance DerivePlutusType PNaturalle where type DPTStrat _ = PlutusTypeNewtype
 
 -- | partial
-pmkNatural :: Term s (PInteger :--> PNatural)
+pmkNatural :: Term s (PInteger :--> PNaturalle)
 pmkNatural = plam $ \i -> pif (i #< 0) (ptraceInfoError "could not make natural") (pcon $ PMkNatural i)
 
 newtype Flip f b a = Flip (f a b)
   deriving stock (Generic)
 
-instance PTryFrom PData (PAsData PNatural) where
-  type PTryFromExcess PData (PAsData PNatural) = Flip Term PNatural
+instance PTryFrom PData (PAsData PNaturalle) where
+  type PTryFromExcess PData (PAsData PNaturalle) = Flip Term PNaturalle
   ptryFrom' opq = runTermCont $ do
     (ter, exc) <- TermCont $ ptryFrom @(PAsData PInteger) opq
     ver <- tcont $ plet $ pmkNatural # exc

From cc48d5598fc0d043299a7c31d63c224bbb41437c Mon Sep 17 00:00:00 2001
From: Koz Ross <koz.ross@retro-freedom.nz>
Date: Fri, 20 Dec 2024 09:18:23 +1300
Subject: [PATCH 4/4] Use punsafeCoerce less

---
 Plutarch/Internal/Numeric.hs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Plutarch/Internal/Numeric.hs b/Plutarch/Internal/Numeric.hs
index 7f1ab07e3..906016ab6 100644
--- a/Plutarch/Internal/Numeric.hs
+++ b/Plutarch/Internal/Numeric.hs
@@ -250,7 +250,7 @@ instance PAdditiveSemigroup PPositive where
 -- | @since WIP
 instance PAdditiveSemigroup PNatural where
   {-# INLINEABLE (#+) #-}
-  x #+ y = punsafeCoerce $ paddInteger # pto x # pto y
+  x #+ y = pcon . PNatural $ paddInteger # pto x # pto y
   {-# INLINEABLE pscalePositive #-}
   pscalePositive = punsafeBuiltin PLC.MultiplyInteger
 
@@ -316,7 +316,7 @@ instance PAdditiveMonoid PInteger where
 -- | @since WIP
 instance PAdditiveMonoid PNatural where
   {-# INLINEABLE pzero #-}
-  pzero = punsafeCoerce . pconstantInteger $ 0
+  pzero = pcon . PNatural . pconstantInteger $ 0
   {-# INLINEABLE pscaleNatural #-}
   pscaleNatural = punsafeBuiltin PLC.MultiplyInteger
 
@@ -466,7 +466,7 @@ instance PMultiplicativeSemigroup PPositive where
 -- | @since WIP
 instance PMultiplicativeSemigroup PNatural where
   {-# INLINEABLE (#*) #-}
-  x #* y = punsafeCoerce $ pmultiplyInteger # pto x # pto y
+  x #* y = pcon . PNatural $ pmultiplyInteger # pto x # pto y
 
 -- | @since WIP
 instance PMultiplicativeSemigroup PInteger where
@@ -498,7 +498,7 @@ class PMultiplicativeSemigroup a => PMultiplicativeMonoid (a :: S -> Type) where
     pif
       (n #== pzero)
       pone
-      (ppowPositive # x # punsafeCoerce n)
+      (ppowPositive # x # pcon (PPositive $ pto n))
 
 -- | @since WIP
 instance PMultiplicativeMonoid PPositive where
@@ -508,7 +508,7 @@ instance PMultiplicativeMonoid PPositive where
 -- | @since WIP
 instance PMultiplicativeMonoid PNatural where
   {-# INLINEABLE pone #-}
-  pone = punsafeCoerce $ pconstantInteger 1
+  pone = pcon . PNatural $ pconstantInteger 1
 
 -- | @since WIP
 instance PMultiplicativeMonoid PInteger where
@@ -686,7 +686,7 @@ ptryNatural = phoistAcyclic $ plam $ \i ->
   pif
     (i #<= pconstantInteger (-1))
     (ptraceInfo "ptryNatural: building with negative" perror)
-    (punsafeCoerce i)
+    (pcon . PNatural $ i)
 
 {- | Build a 'PNatural' from a 'PInteger'. Yields 'PNothing' if given a negative
 value.