From 1e802f1837c541102335c21c744f13c893056b27 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves.strub@pqshield.com>
Date: Mon, 12 Jan 2026 15:08:14 +0100
Subject: [PATCH] Fix dependency analysis

Check modules in types + properly classify declared modules as declared
---
 src/ecCoreModules.ml  |  3 +++
 src/ecCoreModules.mli |  2 ++
 src/ecSection.ml      | 34 ++++++++++++++++++++--------------
 3 files changed, 25 insertions(+), 14 deletions(-)

diff --git a/src/ecCoreModules.ml b/src/ecCoreModules.ml
index 6f96118ab..a07f9ab2a 100644
--- a/src/ecCoreModules.ml
+++ b/src/ecCoreModules.ml
@@ -494,6 +494,9 @@ type top_module_expr = {
   tme_loca : locality;
 }
 
+let is_me_body_alias (body : module_body) =
+  match body with ME_Alias _ -> true | _ -> false
+
 (* -------------------------------------------------------------------- *)
 let ur_hash = EcAst.ur_hash
 
diff --git a/src/ecCoreModules.mli b/src/ecCoreModules.mli
index 1b84c0df2..178b4c581 100644
--- a/src/ecCoreModules.mli
+++ b/src/ecCoreModules.mli
@@ -247,6 +247,8 @@ type top_module_expr = {
   tme_loca : locality;
 }
 
+val is_me_body_alias : module_body -> bool
+
 (* -------------------------------------------------------------------- *)
 val mty_equal :
   module_type ->
diff --git a/src/ecSection.ml b/src/ecSection.ml
index 8f54c0bc0..68d221568 100644
--- a/src/ecSection.ml
+++ b/src/ecSection.ml
@@ -42,7 +42,10 @@ let pp_cbarg env fmt (who : cbarg) =
   | `Module mp ->
     let ppe =
       match mp.m_top with
-      | `Local id -> EcPrinting.PPEnv.add_locals ppe [id]
+      | `Local id ->
+        if EcEnv.Mod.is_declared id env then
+          ppe
+        else EcPrinting.PPEnv.add_locals ppe [id]
       | _ -> ppe in
     Format.fprintf fmt "module %a" (EcPrinting.pp_topmod ppe) mp
   | `ModuleType p ->
@@ -152,7 +155,7 @@ and on_ty (aenv : aenv) (ty : ty) =
   match ty.ty_node with
   | Tunivar _        -> ()
   | Tvar    _        -> ()
-  | Tglob   _        -> ()
+  | Tglob   m        -> aenv.cb (`Module (mident m))
   | Ttuple tys       -> List.iter (on_ty aenv) tys
   | Tconstr (p, tys) -> aenv.cb (`Type p); List.iter (on_ty aenv) tys
   | Tfun (ty1, ty2)  -> List.iter (on_ty aenv) [ty1; ty2]
@@ -370,10 +373,10 @@ and on_module (aenv : aenv) (me : module_expr) =
 
 (* -------------------------------------------------------------------- *)
 and on_mstruct (aenv : aenv) (st : module_structure) =
-  List.iter (on_mpath_mstruct1 aenv) st.ms_body
+  List.iter (on_mstruct1 aenv) st.ms_body
 
 (* -------------------------------------------------------------------- *)
-and on_mpath_mstruct1 (aenv : aenv) (item : module_item) =
+and on_mstruct1 (aenv : aenv) (item : module_item) =
   match item with
   | MI_Module   me -> on_module aenv me
   | MI_Variable x  -> on_ty aenv x.v_type
@@ -568,15 +571,16 @@ let pp_thname scenv =
 (* -------------------------------------------------------------------- *)
 let locality (env : EcEnv.env) (who : cbarg) =
   match who with
-  | `Type p -> (EcEnv.    Ty.by_path p env).tyd_loca
-  | `Op   p -> (EcEnv.    Op.by_path p env).op_loca
-  | `Ax   p -> (EcEnv.    Ax.by_path p env).ax_loca
-  | `Typeclass  p -> ((EcEnv.TypeClass.by_path p env).tc_loca :> locality)
-  | `Module mp    ->
-    begin match EcEnv.Mod.by_mpath_opt mp env with
+  | `Type p -> (EcEnv.Ty.by_path p env).tyd_loca
+  | `Op   p -> (EcEnv.Op.by_path p env).op_loca
+  | `Ax   p -> (EcEnv.Ax.by_path p env).ax_loca
+  | `Typeclass p -> ((EcEnv.TypeClass.by_path p env).tc_loca :> locality)
+  | `Module mp -> begin
+    match EcEnv.Mod.by_mpath_opt mp env with
     | Some (_, Some lc) -> lc
-     (* in this case it should be a quantified module *)
-    | _         -> `Global
+    | _ ->
+      let id = EcPath.mget_ident mp in
+      if EcEnv.Mod.is_declared id env then `Declare else `Global
     end
   | `ModuleType p -> ((EcEnv.ModTy.by_path p env).tms_loca :> locality)
   | `Instance _ -> assert false
@@ -1322,17 +1326,19 @@ let check_module scenv prefix tme =
   match tme.tme_loca with
   | `Local -> check_section scenv from
   | `Global ->
-    if scenv.sc_insec then
+    if scenv.sc_insec then begin
+      let isalias = EcModules.is_me_body_alias tme.tme_expr.me_body in
       let cd =
         { d_ty    = [`Global];
           d_op    = [`Global];
           d_ax    = [];
           d_sc    = [];
-          d_mod   = [`Global]; (* FIXME section: add local *)
+          d_mod   = [`Global] @ (if isalias then [`Declare] else []);
           d_modty = [`Global];
           d_tc    = [`Global];
         } in
       on_module (mkaenv scenv.sc_env (cb scenv from cd)) me
+    end
   | `Declare -> (* Should be SC_decl_mod ... *)
     assert false