Modules I

.gitignore

@@ -64,3 +64,6 @@ node_modules
 
 # Claude Code
 .claude/
+
+# Project plans (local only)
+plans/

src/haz3lcore/ProbePerform.re

@@ -52,8 +52,9 @@ let rec target_subterm_ids = (id: Id.t, info_map: Statics.Map.t) =>
       IdTagged.rep_id(body),
       IdTagged.rep_id(pat),
     ]
-  | Some(InfoExp({term: {term: Let(_pat, def, _), _}, _})) =>
-    /* If trying to probe a let, probe the definition instead.
+  | Some(InfoExp({term: {term: Let(_, def, _), _}, _}))
+  | Some(InfoExp({term: {term: ModuleExp(_, def, _), _}, _})) =>
+    /* If trying to probe a let/module, probe the definition instead.
        Recurse so that if def is a fun literal, the above case will get it */
     target_subterm_ids(IdTagged.rep_id(def), info_map)
 

src/haz3lcore/TyDi/ErrorPrint.re

@@ -200,6 +200,9 @@ let term_string_of: Info.t => string =
   | InfoPat({term, _}) => Print.term(Pat(term))
   | InfoTyp({term, _}) => Print.term(Typ(term))
   | InfoTPat({term, _}) => Print.term(TPat(term))
+  | InfoMod({term, _}) => Print.term(Mod(term))
+  | InfoSig({term, _}) => Print.term(Sig(term))
+  | InfoMPat({term, _}) => Print.term(MPat(term))
   | Secondary(_) => failwith("ChatLSP: term_string_of: Secondary");
 
 let all = (info_map: Statics.Map.t): list(string) => {

src/haz3lcore/TyDi/TyDi.re

@@ -27,12 +27,33 @@ let suggest = (ci: Info.t, z: Zipper.t): list(t) => {
    * recency bias in ctx. Revisit this later. I'm sorting before
    * combination because we want backpack candidates to show up first */
   switch (ci) {
+  | InfoExp({dot_labels, _}) when dot_labels != [] =>
+    List.map(
+      label =>
+        TyDiSuggestion.{
+          content: label,
+          strategy: Exp(Common(FromCtx(Label(label) |> Typ.fresh))),
+        },
+      dot_labels,
+    )
+  | InfoTyp({expects: LabelProjectionExpected(Some(labels)), _})
+      when labels != [] =>
+    List.map(
+      label =>
+        TyDiSuggestion.{
+          content: label,
+          strategy: Typ(FromCtx),
+        },
+      labels,
+    )
+  | InfoExp({label_sort: true, _})
+  | InfoPat({label_sort: true, _})
   | InfoExp({cls: Exp(Label), _})
   | InfoPat({cls: Pat(Label), _})
   | InfoTyp({cls: Typ(Label), _})
   | InfoExp({cls: Exp(TupLabel), _})
   | InfoPat({cls: Pat(TupLabel), _})
-  | InfoTyp({cls: Typ(TupLabel), _}) => [] // TODO: Autocomplete for labels
+  | InfoTyp({cls: Typ(TupLabel), _}) => []
   | _ =>
     suggest_backpack(z)
     @ (

src/haz3lcore/TyDi/TyDiCtx.re

@@ -104,6 +104,71 @@ let bound_constructor_aps =
     ctx.entries,
   );
 
+/* Suggest qualified module member access: for variables with labeled tuple
+ * (module) types, suggest Name.label for fields consistent with the expected
+ * type. E.g., if String has type (empty=String, length=String->Int), and we
+ * expect String, suggest "String.empty".
+ *
+ * TODO: Only goes one level deep. Nested qualified access (A.B.x) would
+ * require recursive expansion. See also: List(Prod) types could generate
+ * qualified suggestions where field types are wrapped in List(...). */
+let bound_qualified = (ty_expect: Typ.t, ctx: Ctx.t): list(TyDiSuggestion.t) =>
+  List.concat_map(
+    fun
+    | Ctx.VarEntry({typ, name, _}) =>
+      switch (Typ.normalize(ctx, typ) |> Typ.term_of) {
+      | Prod(ts) =>
+        List.filter_map(
+          label_ty =>
+            switch (Typ.match_tup_label(label_ty)) {
+            | Some((label, field_ty))
+                when Typ.is_consistent(ctx, ty_expect, field_ty) =>
+              Some({
+                content: name ++ "." ++ label,
+                strategy: Exp(Common(FromCtx(field_ty))),
+              })
+            | _ => None
+            },
+          ts,
+        )
+      | _ => []
+      }
+    | _ => [],
+    ctx.entries,
+  );
+
+/* Like bound_qualified but for arrow-typed fields: suggest Name.label(
+ * when the field's return type is consistent with the expected type.
+ * E.g., if String has (length=String->Int) and we expect Int,
+ * suggest "String.length(". */
+let bound_qualified_aps =
+    (ty_expect: Typ.t, ctx: Ctx.t): list(TyDiSuggestion.t) =>
+  List.concat_map(
+    fun
+    | Ctx.VarEntry({typ, name, _}) =>
+      switch (Typ.normalize(ctx, typ) |> Typ.term_of) {
+      | Prod(ts) =>
+        List.filter_map(
+          label_ty =>
+            switch (Typ.match_tup_label(label_ty)) {
+            | Some((label, {term: Arrow(_, ty_out), _} as field_ty))
+                when
+                  Typ.is_consistent(ctx, ty_expect, ty_out)
+                  && !Typ.is_consistent(ctx, ty_expect, field_ty) =>
+              Some({
+                content: name ++ "." ++ label ++ "(",
+                strategy: Exp(Common(FromCtxAp(ty_out))),
+              })
+            | _ => None
+            },
+          ts,
+        )
+      | _ => []
+      }
+    | _ => [],
+    ctx.entries,
+  );
+
 /* Suggest bound type aliases in type annotations or definitions */
 let typ_context_entries = (ctx: Ctx.t): list(TyDiSuggestion.t) =>
   List.filter_map(
@@ -117,6 +182,13 @@ let typ_context_entries = (ctx: Ctx.t): list(TyDiSuggestion.t) =>
     ctx.entries,
   );
 
+/* NOTE(perf): suggest_variable and suggest_lookahead_variable each iterate
+ * over ctx.entries multiple times (currently ~7 passes in suggest_variable,
+ * up to ~33 in lookahead worst case for Bool). At typical context sizes
+ * (<500 entries) this is negligible. If it becomes a bottleneck, the main
+ * optimization is a single-pass refactor that classifies entries into
+ * buckets in one traversal, and/or pre-caching results for the fixed
+ * builtin context. */
 let suggest_variable = (ci: Info.t): list(TyDiSuggestion.t) => {
   let ctx = Info.ctx_of(ci);
   let ctx = Ctx.filter_shadowed(ctx); /* Remove shadowing */
@@ -125,6 +197,8 @@ let suggest_variable = (ci: Info.t): list(TyDiSuggestion.t) => {
     bound_variables(ana, ctx)
     @ bound_livelits(ana, ctx)
     @ bound_aps(ana, ctx)
+    @ bound_qualified(ana, ctx)
+    @ bound_qualified_aps(ana, ctx)
     @ bound_constructors(x => Exp(Common(x)), ana, ctx)
     @ bound_constructor_aps(x => Exp(Common(x)), ana, ctx)
   | InfoPat({ana, co_ctx, _}) =>
@@ -169,9 +243,11 @@ let suggest_lookahead_variable = (ci: Info.t): list(TyDiSuggestion.t) => {
   | InfoExp({ana, _}) =>
     let exp_refs = ty =>
       bound_variables(ty, ctx)
+      @ bound_qualified(ty, ctx)
       @ bound_constructors(x => Exp(Common(x)), ty, ctx);
     let exp_aps = ty =>
       bound_aps(ty, ctx)
+      @ bound_qualified_aps(ty, ctx)
       @ bound_constructor_aps(x => Exp(Common(x)), ty, ctx);
     switch (ana |> Typ.term_of) {
     | List(ty) =>

src/haz3lcore/TyDi/TyDiForms.re

@@ -100,13 +100,16 @@ module Delims = {
   let leading = (sort: Sort.t): list(Token.t) =>
     Form.delims
     |> List.map(token => {
-         let (lbl, _) = Form.Expansion.get(token);
-         List.filter_map(
-           (m: Mold.t) =>
-             List.length(lbl) > 1 && token == List.hd(lbl) && m.out == sort
-               ? Some(token ++ leading_expander) : None,
-           Form.Molds.get(lbl),
-         );
+         let (lbl, _) = Form.Expansion.get(sort, token);
+         switch (Form.Molds.try_get(sort, lbl)) {
+         | None => []
+         | Some(molds) =>
+           molds
+           |> List.filter_map((_: Mold.t) =>
+                List.length(lbl) > 1 && token == List.hd(lbl)
+                  ? Some(token ++ leading_expander) : None
+              )
+         };
        })
     |> List.flatten
     |> List.sort_uniq(compare);
@@ -151,18 +154,28 @@ module Delims = {
   let const_mono = (sort: Sort.t): list(Token.t) =>
     Token.const_mono_delims
     |> List.map(token => {
-         List.filter_map(
-           (m: Mold.t) =>
-             m.out == sort && List.mem(token, Token.const_mono_delims)
-               ? Some(token) : None,
-           Form.Molds.get([token]),
-         )
+         switch (Form.Molds.try_get(sort, [token])) {
+         | None => []
+         | Some(molds) =>
+           molds
+           |> List.filter_map((_: Mold.t) =>
+                List.mem(token, Token.const_mono_delims) ? Some(token) : None
+              )
+         }
        })
     |> List.flatten
     |> List.sort_uniq(compare);
 
-  let const_mono_exp = const_mono(Exp);
-  let const_mono_pat = const_mono(Pat);
+  /* base_typs (String, Int, Float, Bool, Nat, SInt) have Exp/Pat-sort
+   * molds (as constructors) but no type entry in Typ.of_const_mono_delim.
+   * Without an entry, filter_by assigns Unknown type, making them match
+   * any expected type. Exclude them from Exp and Pat suggestions;
+   * constructor suggestions come from TyDiCtx.bound_constructors instead.
+   * They remain in Typ sort for type-position completion. */
+  let const_mono_exp =
+    const_mono(Exp) |> List.filter(t => !List.mem(t, Token.base_typs));
+  let const_mono_pat =
+    const_mono(Pat) |> List.filter(t => !List.mem(t, Token.base_typs));
   let const_mono_typ = const_mono(Typ);
 
   let const_mono = (sort: Sort.t): list(string) =>

src/haz3lcore/derived/AutoProbe.re

@@ -195,6 +195,18 @@ let term_is_let = (term: Language.Any.t): bool =>
   | _ => false
   };
 
+/* Module declarations (ModLet, ModType, ModuleMod) don't have runtime
+ * values — they're declarations, not expressions. Auto-probe should
+ * never probe them; it should probe their definition subexpression
+ * instead (which appears as a separate candidate on the same line).
+ * ModExp (bare expression in module body) is excluded — it wraps
+ * an expression that does have a value. */
+let term_is_mod_declaration = (term: Language.Any.t): bool =>
+  switch (term) {
+  | Mod({term: ModLet(_, _) | ModType(_, _) | ModuleMod(_, _), _}) => true
+  | _ => false
+  };
+
 let let_body_is_hole = (term: Language.Any.t): bool =>
   switch (term) {
   | Exp({term: Let(_, _, body), _}) => term_is_hole(Exp(body))
@@ -492,6 +504,13 @@ let candidate_allowed_by_term_sort =
     Language.Statics.Map.lookup(candidate_id, env.info_map),
   );
 
+let candidate_allowed_by_mod_declaration =
+    (candidate_id: Id.t, env: selection_env): bool =>
+  switch (get_term(candidate_id, env.terms)) {
+  | Some(term) => !term_is_mod_declaration(term)
+  | None => true
+  };
+
 let candidate_is_allowed =
     (
       candidate_id: Id.t,
@@ -501,6 +520,7 @@ let candidate_is_allowed =
     )
     : bool =>
   candidate_allowed_by_term_sort(candidate_id, env)
+  && candidate_allowed_by_mod_declaration(candidate_id, env)
   && candidate_allowed_by_holes(candidate_id, row, env)
   && candidate_allowed_by_function_types(candidate_id, env)
   && candidate_allowed_by_container(candidate_id, env)