From 2c128e216c367c1e76d5445962d6bb316c93d4e9 Mon Sep 17 00:00:00 2001
From: troiganto <troiganto@proton.me>
Date: Thu, 23 May 2024 10:00:56 -0500
Subject: [PATCH] refactor(base): move implementation of `Data.Vect.nubBy` to
 global scope

Closes #3285
---
 CHANGELOG_NEXT.md       |  3 +++
 CONTRIBUTORS            |  1 +
 libs/base/Data/Vect.idr | 17 +++++++++--------
 3 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
index aadb887eb5..ebfcf88fc0 100644
--- a/CHANGELOG_NEXT.md
+++ b/CHANGELOG_NEXT.md
@@ -144,6 +144,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * Added `funExt0` and `funExt1`, functions analogous to `funExt` but for functions
   with quantities 0 and 1 respectively.
 
+* Moved definition of `Data.Vect.nubBy` to the global scope as `nubByImpl` to
+  allow compile time proofs on `nubBy` and `nub`.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.
diff --git a/CONTRIBUTORS b/CONTRIBUTORS
index 4e2d89f902..58c15bb497 100644
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -76,6 +76,7 @@ Thomas E. Hansen
 Tim Süberkrüb
 Timmy Jose
 Tom Harley
+troiganto
 Wen Kokke
 Wind Wong
 Zoe Stafford
diff --git a/libs/base/Data/Vect.idr b/libs/base/Data/Vect.idr
index 8ddf862e58..75fdce123d 100644
--- a/libs/base/Data/Vect.idr
+++ b/libs/base/Data/Vect.idr
@@ -662,6 +662,14 @@ filter p (x::xs) =
       else
         (_ ** tail)
 
+public export
+nubByImpl : Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
+nubByImpl acc p []      = (_ ** [])
+nubByImpl acc p (x::xs) with (elemBy p x acc)
+  nubByImpl acc p (x :: xs) | True  = nubByImpl acc p xs
+  nubByImpl acc p (x :: xs) | False with (nubByImpl (x::acc) p xs)
+    nubByImpl acc p (x :: xs) | False | (_ ** tail) = (_ ** x::tail)
+
 ||| Make the elements of some vector unique by some test
 |||
 ||| ```idris example
@@ -669,14 +677,7 @@ filter p (x::xs) =
 ||| ```
 public export
 nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
-nubBy = nubBy' []
-  where
-    nubBy' : forall len . Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
-    nubBy' acc p []      = (_ ** [])
-    nubBy' acc p (x::xs) with (elemBy p x acc)
-      nubBy' acc p (x :: xs) | True  = nubBy' acc p xs
-      nubBy' acc p (x :: xs) | False with (nubBy' (x::acc) p xs)
-        nubBy' acc p (x :: xs) | False | (_ ** tail) = (_ ** x::tail)
+nubBy = nubByImpl []
 
 ||| Make the elements of some vector unique by the default Boolean equality
 |||