Remove args if calling out from an inner module, not into an outer mo…

…dule
agda · Sep 18, 2024 · 88fac19 · 88fac19
1 parent 13ccde1
commit 88fac19
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
@@ -176,8 +176,8 @@ compileDef f ty args =
       -- if the function is called from the same module it's defined in,
       -- we drop the module parameters
       -- NOTE(flupe): in the future we're not always gonna be erasing module parameters
-      if mnameToList currentMod `isPrefixOf` mnameToList defMod then do
-        npars <- size <$> (lookupSection =<< currentModule)
+      if mnameToList defMod `isPrefixOf` mnameToList currentMod then do
+        npars <- size <$> lookupSection defMod
         let (pars, rest) = splitAt npars args
         ty' <- piApplyM ty pars
         pure (ty', rest)