From 676805cb6d50d4372329bd89d70c65ebbc4a48ee Mon Sep 17 00:00:00 2001
From: spike <spikedoanz@gmail.com>
Date: Thu, 1 Jan 2026 00:23:28 -0500
Subject: [PATCH] Add regression test for issue #3705: codata unification
 infinite loop

Adds test idris2/reg/reg060 which reproduces the infinite loop when
unifying eta-equivalent functions in codata context.

The test includes a 5-second timeout to detect the hang.
---
 CONTRIBUTORS                          |  1 +
 tests/idris2/reg/reg060/CoDataEta.idr | 11 +++++++++++
 tests/idris2/reg/reg060/expected      |  1 +
 tests/idris2/reg/reg060/run           | 11 +++++++++++
 4 files changed, 24 insertions(+)
 create mode 100644 tests/idris2/reg/reg060/CoDataEta.idr
 create mode 100644 tests/idris2/reg/reg060/expected
 create mode 100644 tests/idris2/reg/reg060/run

diff --git a/CONTRIBUTORS b/CONTRIBUTORS
index 88f01e10a3a..3e2e0bc88cc 100644
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -73,6 +73,7 @@ Rodrigo Oliveira
 Rohit Grover
 Rui Barreiro
 Ruslan Feizerahmanov
+spikedoanz
 Sam Phillips
 Simon Chatterjee
 Stefan Höck
diff --git a/tests/idris2/reg/reg060/CoDataEta.idr b/tests/idris2/reg/reg060/CoDataEta.idr
new file mode 100644
index 00000000000..897dfd15830
--- /dev/null
+++ b/tests/idris2/reg/reg060/CoDataEta.idr
@@ -0,0 +1,11 @@
+tabulate : (Nat -> a) -> Stream a
+tabulate f = f 0 :: tabulate (f . S)
+
+index : Stream a -> Nat -> a
+index (x :: _)  Z     = x
+index (_ :: xs) (S n) = index xs n
+
+lemma : (f : Nat -> Nat)
+        -> (k : Nat)
+        -> index (tabulate (f . S)) k = index (tabulate (\m => f (S m))) k
+lemma f k = Refl
diff --git a/tests/idris2/reg/reg060/expected b/tests/idris2/reg/reg060/expected
new file mode 100644
index 00000000000..82e87d69e1e
--- /dev/null
+++ b/tests/idris2/reg/reg060/expected
@@ -0,0 +1 @@
+1/1: Building CoDataEta (CoDataEta.idr)
diff --git a/tests/idris2/reg/reg060/run b/tests/idris2/reg/reg060/run
new file mode 100644
index 00000000000..9837282b580
--- /dev/null
+++ b/tests/idris2/reg/reg060/run
@@ -0,0 +1,11 @@
+. ../../../testutils.sh
+
+# This test must complete within 5 seconds.
+# Without the fix for codata unification, it would hang indefinitely
+# trying to unify eta-equivalent functions in codata context.
+timeout 5 $idris2 --no-banner --no-color --console-width 0 --check CoDataEta.idr
+
+if [ $? -eq 124 ]; then
+    echo "TIMEOUT: Unification hung (this indicates the bug is present)"
+    exit 1
+fi