[ test ] add regression test for codata unification infinite loop

CONTRIBUTORS

@@ -73,6 +73,7 @@ Rodrigo Oliveira
 Rohit Grover
 Rui Barreiro
 Ruslan Feizerahmanov
+spikedoanz
 Sam Phillips
 Simon Chatterjee
 Stefan Höck

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

tests/idris2/reg/reg060/expected

@@ -0,0 +1 @@
+1/1: Building CoDataEta (CoDataEta.idr)

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