From 26a30bca71a229161fd880b55bae542e8c596283 Mon Sep 17 00:00:00 2001 From: Kristian Larsson Date: Wed, 8 Oct 2025 12:36:37 +0200 Subject: [PATCH] Add transitive witness propagation for protocol extensions Protocol extensions (witnesses) provide method implementations for protocols. Previously, witnesses were only imported from directly imported modules. This meant that when module m3 imports m2, and m2 imports m1 (where m1 has an extension making Thing implement Iterable), m3 couldn't use Thing as an Iterable without explicitly importing m1. This change enhances witness importing to handle transitive dependencies: - Extract importWitsFromModule as a reusable function to import witnesses from a single module's type environment - Modify importWits to be IO-based and process transitive dependencies by reading .ty files and importing witnesses from dependencies that are already loaded in the environment - Call importWitsFromModule in subImp to ensure witnesses are imported as each transitive dependency is loaded The key insight is to check if dependencies are loaded in the environment (via lookupMod) rather than requiring them to be in the imports list. This allows protocol implementations to properly propagate through module dependency chains. Before: When compiling m3 which imports m2, importWits would only add witnesses from m2's TEnv to m3's environment. Even though m1 was loaded into the module cache (via subImp when processing m2's dependencies), m1's witnesses were never imported because the old importWits only processed the module being directly imported. Now: When compiling m3 which imports m2, subImp loads m1 (as m2's dependency) and immediately imports m1's witnesses via importWitsFromModule. Later, when importWits processes m2, it reads m2.ty to find m2's dependencies, sees m1 is already in the module cache, and imports m1's witnesses into the current environment. The subImp change ensures witnesses are available as soon as modules are loaded, while the importWits change ensures they propagate to modules that need them. --- compiler/lib/src/Acton/Env.hs | 52 +++++++++++++++++++++++++++++------ 1 file changed, 43 insertions(+), 9 deletions(-) diff --git a/compiler/lib/src/Acton/Env.hs b/compiler/lib/src/Acton/Env.hs index 19118a751..3a7925884 100644 --- a/compiler/lib/src/Acton/Env.hs +++ b/compiler/lib/src/Acton/Env.hs @@ -23,6 +23,7 @@ import System.Directory (doesFileExist) import System.Environment (getExecutablePath) import Control.Monad import Control.Monad.Except +import Data.Maybe (isNothing, fromJust, isJust) import Acton.Syntax import Acton.Builtin @@ -451,7 +452,8 @@ initEnv path False = do (_,nmod,_) <- InterfaceFiles.readFile (joinPath witnesses = primWits, thismod = Nothing, envX = () } - env = importAll mBuiltin envBuiltin $ importWits mBuiltin envBuiltin $ env0 + -- Pass empty search path for builtin since it has no dependencies + env <- importAll mBuiltin envBuiltin <$> importWits [] mBuiltin envBuiltin env0 return env withModulesFrom :: EnvF x -> EnvF x -> EnvF x @@ -1183,13 +1185,16 @@ impModule spath env (Import _ ms) imp env (ModuleItem m as : is) = do (env1,te) <- doImp spath env m let env2 = maybe (addImport m) (\n->define [(n, NMAlias m)]) as env1 - imp (importWits m te env2) is + env3 <- importWits spath m te env2 + imp env3 is impModule spath env (FromImport _ (ModRef (0,Just m)) items) = do (env1,te) <- doImp spath env m - return $ importSome items m te $ importWits m te $ env1 + env2 <- importWits spath m te env1 + return $ importSome items m te env2 impModule spath env (FromImportAll _ (ModRef (0,Just m))) = do (env1,te) <- doImp spath env m - return $ importAll m te $ importWits m te $ env1 + env2 <- importWits spath m te env1 + return $ importAll m te env2 impModule _ _ i = illegalImport (loc i) @@ -1198,8 +1203,9 @@ moduleRefs env = nub $ imports env ++ [ m | (_,NMAlias m) <- na moduleRefs1 env = moduleRefs env \\ [mPrim, mBuiltin] subImp spath env [] = return env -subImp spath env (m:ms) = do (env',_) <- doImp spath env m - subImp spath env' ms +subImp spath env (m:ms) = do (env',te) <- doImp spath env m + let env'' = importWitsFromModule m te env' + subImp spath env'' ms findTyFile spaths mn = go spaths where @@ -1247,9 +1253,37 @@ impNames m te = mapMaybe imp te imp (n, NDef t d _) = Just (n, NAlias (GName m n)) imp _ = Nothing -- cannot happen -importWits :: ModName -> TEnv -> EnvF x -> EnvF x -importWits m te env = foldl addWit env ws - where ws = [ WClass q (tCon c) p (GName m n) ws | (n, NExt q c ps te' _) <- te, (ws,p) <- ps ] +-- Extract and import witnesses from a module's TEnv +importWitsFromModule :: ModName -> TEnv -> EnvF x -> EnvF x +importWitsFromModule mod modTe modEnv = foldl addWit modEnv ws + where + ws = [ WClass q (tCon $ qualifyTCon mod c) p (GName mod n) ws | (n, NExt q c ps te' _) <- modTe, (ws,p) <- ps ] + -- Ensure the type constructor is properly qualified with the module name + qualifyTCon md (TC n ts) = TC (qualifyName md n) ts + qualifyName md (NoQ n) = GName md n + qualifyName md qn = qn + +-- Import witnesses from a module and its transitive dependencies +importWits :: [FilePath] -> ModName -> TEnv -> EnvF x -> IO (EnvF x) +importWits spath m te env = do + -- First import witnesses from the module itself + let env' = importWitsFromModule m te env + + -- Then import witnesses from dependencies that are already loaded + -- This ensures we get transitive witnesses without loading new modules + tyFile <- findTyFile spath m + case tyFile of + Nothing -> return env' -- No .ty file (e.g., builtin) + Just tyF -> do + (deps, _, _) <- InterfaceFiles.readFile tyF + -- Process dependencies that are already loaded in the environment + let cachedDeps = filter (\d -> isJust (lookupMod d env)) deps + foldM importDepWits env' cachedDeps + where + importDepWits envAcc dep = + case lookupMod dep envAcc of + Just depTe -> return $ importWitsFromModule dep depTe envAcc + Nothing -> return envAcc -- Shouldn't happen if dep is loaded