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"