From e1c5c2fd8ee45685e09c61bfa03be8107376bbbb Mon Sep 17 00:00:00 2001
From: stefan-hoeck <hock@zhaw.ch>
Date: Mon, 22 Apr 2024 15:44:35 +0200
Subject: [PATCH] [ fix ] issue 3266

---
 libs/base/Data/Fin.idr              | 3 ++-
 tests/base/data_fin/fromInteger.idr | 5 +++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr
index 997b5c65b..0eff1af21 100644
--- a/libs/base/Data/Fin.idr
+++ b/libs/base/Data/Fin.idr
@@ -230,8 +230,9 @@ finFromInteger x = natToFinLt (fromInteger x)
 -- even when the function is unused (issue #2032)
 public export
 integerLessThanNat : Integer -> Nat -> Bool
+integerLessThanNat 0 (S m) = True
 integerLessThanNat x n with (x < the Integer 0)
-  integerLessThanNat _ _     | True  = True                            -- if `x < 0` then `x < n` for any `n : Nat`
+  integerLessThanNat _ _     | True  = False                           -- don't support negative literals
   integerLessThanNat x (S m) | False = integerLessThanNat (x-1) m      -- recursive case
   integerLessThanNat x Z     | False = False                           -- `x >= 0` contradicts `x < Z`
 
diff --git a/tests/base/data_fin/fromInteger.idr b/tests/base/data_fin/fromInteger.idr
index 87cc10128..00b403c5a 100644
--- a/tests/base/data_fin/fromInteger.idr
+++ b/tests/base/data_fin/fromInteger.idr
@@ -20,3 +20,8 @@ eq1 = Refl
 -- and anybody measures the time it takes this test to run...
 addFourMillion : Int -> Int
 addFourMillion x = 4000000 + x
+
+-- issue #3266
+failing
+  fin0 : Fin 0
+  fin0 = (-1)