From 72f11b0571cd8e8c2a468a777072abb93d9acbcb Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Wed, 5 Aug 2026 15:35:32 +0200
Subject: [PATCH] [ fix #385 ] Implement `predNat` primitive

---
 CHANGELOG.md                    |  6 ++++++
 lib/base/Haskell/Extra/Nat.agda | 11 +++++++++++
 src/Agda2Hs/Compile/Term.hs     |  9 +++++++++
 test/Succeed/PredNat.agda       | 27 +++++++++++++++++++++++++++
 test/Succeed/PredNat.hs         | 13 +++++++++++++
 5 files changed, 66 insertions(+)
 create mode 100644 lib/base/Haskell/Extra/Nat.agda
 create mode 100644 test/Succeed/PredNat.agda
 create mode 100644 test/Succeed/PredNat.hs

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8a82e310..094d3c24 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,12 @@ See https://github.com/agda/agda2hs/issues?q=milestone%3A1.5+is%3Apr for the ful
 Additions to the agda2hs Prelude
 --------------------------------
 
+- Added `predNat` to `Haskell.Extra.Nat`: the predecessor of a nonzero
+  natural number, returning the predecessor together with a proof that
+  the original number is its successor. It compiles to Haskell's `pred`
+  and enables defining functions such as a `Nat` recursor on top of
+  `ifDec` (see issue #385).
+
 
 Fixed issues
 ------------
diff --git a/lib/base/Haskell/Extra/Nat.agda b/lib/base/Haskell/Extra/Nat.agda
new file mode 100644
index 00000000..0e5178cf
--- /dev/null
+++ b/lib/base/Haskell/Extra/Nat.agda
@@ -0,0 +1,11 @@
+module Haskell.Extra.Nat where
+
+open import Haskell.Prelude
+open import Haskell.Extra.Refinement
+
+-- | The predecessor of a nonzero natural number, together with a proof
+-- that the original number is its successor. Since pattern matching on
+-- 'Nat' is not allowed in Haskell, this is provided as a primitive that
+-- compiles to Haskell's 'pred'.
+postulate
+  predNat : (n : Nat) → @0 (n ≡ 0 → ⊥) → ∃ Nat λ m → n ≡ suc m
diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
index 0171b5bd..bc6b8851 100644
--- a/src/Agda2Hs/Compile/Term.hs
+++ b/src/Agda2Hs/Compile/Term.hs
@@ -66,6 +66,7 @@ isSpecialDef q = case prettyShow q of
   "Haskell.Prim.the"             -> Just expTypeSig
   "Haskell.Extra.Delay.runDelay" -> Just compileErasedApp
   "Agda.Builtin.Word.primWord64FromNat" -> Just primWord64FromNat
+  "Haskell.Extra.Nat.predNat"            -> Just predNat
   _                              -> Nothing
 
 
@@ -137,6 +138,14 @@ primWord64FromNat ty args = compileArgs ty args >>= \case
   -- anything else
   _ -> agda2hsError "primWord64FromNat must be applied to a literal"
 
+-- | Compile 'predNat' to Haskell's 'pred'. The erased proof argument is
+-- dropped by 'compileArgs', so the single remaining argument is the
+-- natural number whose predecessor we want.
+predNat :: DefCompileRule
+predNat ty args = compileArgs ty args >>= \case
+  n : es' -> return $ eApp (hsVar "pred") [n] `eApp` es'
+  _       -> agda2hsError "predNat must be applied to a natural number"
+
 
 compileVar :: Int -> Type -> [Term] -> C (Hs.Exp ())
 compileVar i ty es = do
diff --git a/test/Succeed/PredNat.agda b/test/Succeed/PredNat.agda
new file mode 100644
index 00000000..65ce7066
--- /dev/null
+++ b/test/Succeed/PredNat.agda
@@ -0,0 +1,27 @@
+module PredNat where
+
+open import Haskell.Prelude
+open import Haskell.Extra.Dec
+open import Haskell.Extra.Nat
+open import Haskell.Extra.Refinement
+open import Haskell.Law.Eq
+open import Haskell.Law.Eq.Instances
+
+-- The predecessor of a nonzero natural number.
+predNat' : (n : Nat) → @0 (n ≡ 0 → ⊥) → Nat
+predNat' n neq = predNat n neq .value
+
+{-# COMPILE AGDA2HS predNat' #-}
+
+-- A recursor for natural numbers, as suggested in issue #385.
+recNat : (a : @0 Nat → Set)
+       → (z : a 0)
+       → (s : (m : Nat) → a m → a (suc m))
+       → (n : Nat) → a n
+recNat a z s n = ifDec (n ≟ 0)
+  (λ where {{refl}} → z)
+  (λ {{n≠0}} →
+    case predNat n n≠0 of λ where
+      (m ⟨ refl ⟩) → s m (recNat a z s m))
+
+{-# COMPILE AGDA2HS recNat #-}
diff --git a/test/Succeed/PredNat.hs b/test/Succeed/PredNat.hs
new file mode 100644
index 00000000..92b795ab
--- /dev/null
+++ b/test/Succeed/PredNat.hs
@@ -0,0 +1,13 @@
+module PredNat where
+
+import Numeric.Natural (Natural)
+
+predNat' :: Natural -> Natural
+predNat' n = pred n
+
+recNat :: a -> (Natural -> a -> a) -> Natural -> a
+recNat z s n
+  = if n == 0 then z else
+      case pred n of
+          m -> s m (recNat z s m)
+