From 13cbeff8bf8b90805bdde2fb722c2b6c26fbf397 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Mon, 16 Sep 2024 23:14:35 +0300
Subject: [PATCH] [ refactor ] Make `argDeps` function to be pure, not monadic

---
 src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr   | 2 +-
 src/Deriving/DepTyCheck/Util/Reflection.idr       | 4 ++--
 tests/derivation/utils/arg-deps/_common/Infra.idr | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
index 9a2b712ea..ab20a3a2c 100644
--- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
+++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
@@ -159,7 +159,7 @@ namespace NonObligatoryExts
               `(Prelude.pure {f=Test.DepTyCheck.Gen.Gen _} ~consExpr)
 
       -- Get dependencies of constructor's arguments
-      rawDeps <- argDeps con.args
+      let rawDeps = argDeps con.args
       let deps = downmap ((`difference` givs) . mapIn weakenToSuper) rawDeps
 
       -------------------------------------------------
diff --git a/src/Deriving/DepTyCheck/Util/Reflection.idr b/src/Deriving/DepTyCheck/Util/Reflection.idr
index ae82f9c11..18e6fc7d2 100644
--- a/src/Deriving/DepTyCheck/Util/Reflection.idr
+++ b/src/Deriving/DepTyCheck/Util/Reflection.idr
@@ -618,9 +618,9 @@ genTypeName g = do
 ----------------------------------------------
 
 export
-argDeps : Elaboration m => (args : List Arg) -> m $ DVect args.length $ SortedSet . Fin . Fin.finToNat
+argDeps : (args : List Arg) -> DVect args.length $ SortedSet . Fin . Fin.finToNat
 argDeps args = do
   let nameToIndices = SortedMap.fromList $ mapI args $ \i, arg => (argName arg, SortedSet.singleton i)
   let args = Vect.fromList args <&> \arg => allVarNames arg.type |> map (fromMaybe empty . lookup' nameToIndices)
-  pure $ flip upmapI args $ \i, argDeps => flip concatMap argDeps $ \candidates =>
+  flip upmapI args $ \i, argDeps => flip concatMap argDeps $ \candidates =>
     maybe empty singleton $ last' $ mapMaybe tryToFit $ SortedSet.toList candidates
diff --git a/tests/derivation/utils/arg-deps/_common/Infra.idr b/tests/derivation/utils/arg-deps/_common/Infra.idr
index bb461c86f..eab87c14b 100644
--- a/tests/derivation/utils/arg-deps/_common/Infra.idr
+++ b/tests/derivation/utils/arg-deps/_common/Infra.idr
@@ -21,7 +21,7 @@ ppTys tys = do
   let tys = unlist tys
   for_ tys $ \expr => do
     let (args, ret) = unPi expr
-    deps <- map SortedSet.toList <$> argDeps args
+    let deps = map SortedSet.toList $ argDeps args
     let expr' = piAll ret $ {piInfo := ExplicitArg} <$> args -- as if all arguments were explicit
     logSugaredTerm "deptycheck.arg-deps" 0 "type        " expr'
     logMsg         "deptycheck.arg-deps" 0 "dependencies: \{show deps}\n"