Update comments

agda · Sep 20, 2024 · fd8f271 · fd8f271
1 parent 0e0b080
commit fd8f271
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
@@ -173,13 +173,13 @@ compileDef f ty args =
 
     defIsClass <- isClassModule defMod
     -- TODO: simplify this when Agda exposes where-provenance in 'Internal' syntax
-    outerWhereModules <- asks whereModules -- W
+    outerWhereModules <- asks whereModules
 
     (ty', args') <-
 
-      -- if the function is called from the same module it's defined in,
+      -- if the function comes from a where-clause
+      -- or is a class-method for the class we are currently defining,
       -- we drop the module parameters
-      -- NOTE(flupe): in the future we're not always gonna be erasing module parameters
       if defMod `elem` outerWhereModules || defIsClass && (mnameToList defMod `isPrefixOf` mnameToList currentMod) then do
         npars <- size <$> lookupSection defMod
         let (pars, rest) = splitAt npars args