refactor(base): move implementation of Data.Vect.nubBy to global scope

Closes #3285

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`.

CONTRIBUTORS

@@ -76,6 +76,7 @@ Thomas E. Hansen
 Tim Süberkrüb
 Timmy Jose
 Tom Harley
+troiganto
 Wen Kokke
 Wind Wong
 Zoe Stafford

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' []
+nubBy = nubByImpl []
-  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)
 
 ||| Make the elements of some vector unique by the default Boolean equality
 |||