From 5e567bf1e5497048fe3adc82bcc1da99a5f8ba0f Mon Sep 17 00:00:00 2001
From: gensofubi <1353284415@qq.com>
Date: Mon, 20 May 2024 18:28:35 +0800
Subject: [PATCH] incomplete module type created for dot analyzing

---
 src/haz3lcore/dynamics/Elaborator.re       |   2 +-
 src/haz3lcore/dynamics/Transition.re       |  43 +++-----
 src/haz3lcore/statics/Module.re            |   9 +-
 src/haz3lcore/statics/Statics.re           |  12 +--
 src/haz3lcore/statics/Term.re              |  33 +++---
 src/haz3lcore/statics/TypBase.re           | 114 ++++++++++++++-------
 src/haz3lweb/view/CursorInspector.re       |   2 +-
 src/haz3lweb/view/Type.re                  |   9 +-
 src/haz3lweb/view/dhcode/layout/HTypDoc.re |  22 +++-
 9 files changed, 155 insertions(+), 91 deletions(-)

diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index 4779c49b94..b3ff633952 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -312,7 +312,7 @@ let rec dhexp_of_uexp =
           switch (Id.Map.find_opt(Term.UPat.rep_id(p), m)) {
           | Some(InfoPat({ty, _})) =>
             switch (ty) {
-            | Module(c) => c
+            | Module(c) => c.inner_ctx
             | _ => []
             }
           | _ => []
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index f0f377469b..a68498754c 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -103,17 +103,19 @@ module CastHelpers = {
   let grounded_List = NotGroundOrHole(List(Unknown(Internal)));
   let grounded_Module = (ctx: Ctx.t) =>
     NotGroundOrHole(
-      Typ.Module(
-        List.map(
-          fun
-          | Ctx.VarEntry(var_entry) =>
-            Ctx.VarEntry({...var_entry, typ: Unknown(Internal)})
-          | Ctx.ConstructorEntry(var_entry) =>
-            Ctx.ConstructorEntry({...var_entry, typ: Unknown(Internal)})
-          | Ctx.TVarEntry(tvar_entry) => Ctx.TVarEntry(tvar_entry),
-          ctx,
-        ),
-      ),
+      Typ.Module({
+        inner_ctx:
+          List.map(
+            fun
+            | Ctx.VarEntry(var_entry) =>
+              Ctx.VarEntry({...var_entry, typ: Unknown(Internal)})
+            | Ctx.ConstructorEntry(var_entry) =>
+              Ctx.ConstructorEntry({...var_entry, typ: Unknown(Internal)})
+            | Ctx.TVarEntry(tvar_entry) => Ctx.TVarEntry(tvar_entry),
+            ctx,
+          ),
+        incomplete: false,
+      }),
     );
 
   let rec ground_cases_of = (ty: Typ.t): ground_cases => {
@@ -144,19 +146,8 @@ module CastHelpers = {
       } else {
         tys |> List.length |> grounded_Prod;
       }
-    | Module(ctx) =>
-      if (List.for_all(
-            fun
-            | Ctx.VarEntry(var_entry)
-            | Ctx.ConstructorEntry(var_entry) =>
-              var_entry.typ == Unknown(Internal)
-            | Ctx.TVarEntry(_) => true,
-            ctx,
-          )) {
-        Ground;
-      } else {
-        grounded_Module(ctx);
-      }
+    | Module({inner_ctx: [], incomplete: true}) => Ground
+    | Module(_) => NotGroundOrHole(Module({inner_ctx: [], incomplete: true}))
     | Sum(sm) =>
       sm |> ConstructorMap.is_ground(is_ground_arg)
         ? Ground : grounded_Sum(sm)
@@ -311,12 +302,12 @@ module Transition = (EV: EV_MODE) => {
       | (Cast(d3', Module(ctx), Module(ctx')), BoundVar(name))
       | (Cast(d3', Module(ctx), Module(ctx')), Constructor(name)) =>
         let ty =
-          switch (Ctx.lookup_var(ctx, name)) {
+          switch (Ctx.lookup_var(ctx.inner_ctx, name)) {
           | None => Typ.Unknown(Internal)
           | Some(var) => var.typ
           };
         let ty' =
-          switch (Ctx.lookup_var(ctx', name)) {
+          switch (Ctx.lookup_var(ctx'.inner_ctx, name)) {
           | None => Typ.Unknown(Internal)
           | Some(var) => var.typ
           };
diff --git a/src/haz3lcore/statics/Module.re b/src/haz3lcore/statics/Module.re
index 80f9bf3521..d986c16dfe 100644
--- a/src/haz3lcore/statics/Module.re
+++ b/src/haz3lcore/statics/Module.re
@@ -31,7 +31,7 @@ let rec get_module =
   | Constructor(tag_name)
   | Var(tag_name) =>
     switch (Ctx.lookup_var(ctx, tag_name)) {
-    | Some({typ: Module(inner_ctx), _}) =>
+    | Some({typ: Module({inner_ctx, _}), _}) =>
       Some((name ++ tag_name ++ ".", Some(inner_ctx)))
     | _ => Some((name ++ tag_name ++ ".", None))
     }
@@ -41,7 +41,7 @@ let rec get_module =
     let inner_ctx = {
       let* ctx = ctx;
       switch (Ctx.lookup_var(ctx, tag_name)) {
-      | Some({typ: Module(inner_ctx), _}) => Some(inner_ctx)
+      | Some({typ: Module({inner_ctx, _}), _}) => Some(inner_ctx)
       | _ => None
       };
     };
@@ -51,5 +51,8 @@ let rec get_module =
   };
 };
 let mk = (name: Var.t, id: Id.t) => {
-  Typ.Module([VarEntry({name, id, typ: Unknown(Internal)})]);
+  Typ.Module({
+    inner_ctx: [VarEntry({name, id, typ: Unknown(Internal)})],
+    incomplete: true,
+  });
 };
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 4e81e98e4d..b07ba5c7a0 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -524,7 +524,7 @@ and uexp_to_info_map =
       };
     };
     switch (ty) {
-    | Module(inner_ctx) =>
+    | Module({inner_ctx, _}) =>
       let (body, m) = go'(~ctx=inner_ctx, ~mode, e_mem, m);
       let m =
         e_mem.ids
@@ -744,7 +744,7 @@ and upat_to_info_map =
       add the type alias to the current context */
       let ctx = {
         switch (ctx_typ) {
-        | Module(inner_ctx) =>
+        | Module({inner_ctx, _}) =>
           switch (Ctx.lookup_tvar(inner_ctx, ctr)) {
           | Some({kind: Singleton(ty), _}) =>
             /** Currently all type shadowing are disallowed. See TyAlias */
@@ -977,7 +977,7 @@ and uexp_to_module =
       m: Map.t,
       inner_ctx: Ctx.t,
     )
-    : (Ctx.t, Info.exp, Map.t) => {
+    : (Typ.module_typ, Info.exp, Map.t) => {
   let mode =
     switch (mode) {
     | Ana(Unknown(SynSwitch)) => Mode.Syn
@@ -1018,7 +1018,7 @@ and uexp_to_module =
       // Var like patterns are looked up in the module context.
       | Var(name)
       | Constructor(name) =>
-        switch (Ctx.lookup_var(m, name)) {
+        switch (Ctx.lookup_var(m.inner_ctx, name)) {
         | Some(t) => Ana(t.typ)
         | None => Syn
         }
@@ -1286,7 +1286,7 @@ and uexp_to_module =
       let expects: Info.typ_expects =
         switch (mode) {
         | Ana(Module(m)) =>
-          switch (Ctx.lookup_alias(m, name)) {
+          switch (Ctx.lookup_alias(m.inner_ctx, name)) {
           | Some(ty) =>
             /* This check is moved here because utyp_to_info_map
                does not handle recursion. */
@@ -1342,7 +1342,7 @@ and uexp_to_module =
     (
       switch (mode) {
       | Ana(Module(m)) => m
-      | _ => inner_ctx
+      | _ => {inner_ctx, incomplete: false}
       },
       info,
       m,
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 4be6cd1291..7e5b518bb4 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -247,12 +247,14 @@ module UTyp = {
           List.hd(ids);
         };
         let rec upat_to_ctx =
-                ((outer_ctx: Ctx.t, inner_ctx: Ctx.t), upat: TermBase.UPat.t) => {
+                (
+                  (outer_ctx: Ctx.t, inner_ctx: Ctx.t, incomplete: bool),
+                  upat: TermBase.UPat.t,
+                ) => {
           switch (upat.term) {
           | Invalid(_)
           | EmptyHole
           | MultiHole(_)
-          | Wild
           | Int(_)
           | Float(_)
           | Bool(_)
@@ -261,7 +263,9 @@ module UTyp = {
           | ListLit(_)
           | Cons(_)
           | Tuple(_)
-          | Ap(_) => (outer_ctx, inner_ctx)
+          | Wild
+          | Ap(_) => (outer_ctx, inner_ctx, incomplete)
+          // | Wild => (outer_ctx, inner_ctx, true) // disabled due to casting issues.
           | TypeAnn(var, utyp1) =>
             switch (var.term, utyp1.term) {
             | (Var(name), _)
@@ -276,8 +280,9 @@ module UTyp = {
                   }),
                   ...inner_ctx,
                 ],
+                incomplete,
               )
-            | _ => (outer_ctx, inner_ctx)
+            | _ => (outer_ctx, inner_ctx, incomplete)
             }
           | Var(name) => (
               outer_ctx,
@@ -285,6 +290,7 @@ module UTyp = {
                 VarEntry({name, id: rep_id_p(upat), typ: Unknown(TypeHole)}),
                 ...inner_ctx,
               ],
+              incomplete,
             )
           | Constructor(name) => (
               outer_ctx,
@@ -296,6 +302,7 @@ module UTyp = {
                 }),
                 ...inner_ctx,
               ],
+              incomplete,
             )
           | TyAlias(typat, utyp) =>
             switch (typat.term) {
@@ -339,22 +346,23 @@ module UTyp = {
               | Some(sm) => (
                   Ctx.add_ctrs(ctx_body, name, rep_id(utyp), sm),
                   Ctx.add_ctrs(new_inner, name, rep_id(utyp), sm),
+                  incomplete,
                 )
-              | None => (ctx_body, new_inner)
+              | None => (ctx_body, new_inner, incomplete)
               };
 
-            | _ => (outer_ctx, inner_ctx)
+            | _ => (outer_ctx, inner_ctx, incomplete)
             }
-          | Parens(p) => upat_to_ctx((outer_ctx, inner_ctx), p)
+          | Parens(p) => upat_to_ctx((outer_ctx, inner_ctx, incomplete), p)
           };
         };
         let rec get_Tuple: TermBase.UPat.t => Typ.t = (
           ut =>
             switch (ut.term) {
             | Tuple(us) =>
-              let (_, module_ctx) =
-                List.fold_left(upat_to_ctx, (ctx, []), us);
-              Module(module_ctx);
+              let (_, inner_ctx, incomplete) =
+                List.fold_left(upat_to_ctx, (ctx, [], false), us);
+              Module({inner_ctx, incomplete});
             | Parens(p) => get_Tuple(p)
             | TypeAnn(_)
             | Var(_)
@@ -372,8 +380,9 @@ module UTyp = {
             | ListLit(_)
             | Cons(_)
             | Ap(_) =>
-              let (_, module_ctx) = upat_to_ctx((ctx, []), ut);
-              Module(module_ctx);
+              let (_, inner_ctx, incomplete) =
+                upat_to_ctx((ctx, [], false), ut);
+              Module({inner_ctx, incomplete});
             }
         );
         get_Tuple(u);
diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re
index 53221f2d16..d5ad13c0d3 100644
--- a/src/haz3lcore/statics/TypBase.re
+++ b/src/haz3lcore/statics/TypBase.re
@@ -19,6 +19,11 @@ module rec Typ: {
     | Free(TypVar.t)
     | Internal;
 
+  type module_typ = {
+    inner_ctx: Ctx.t,
+    incomplete: bool,
+  };
+
   /* TYP.T: Hazel types */
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
@@ -32,7 +37,7 @@ module rec Typ: {
     | Arrow(t, t)
     | Sum(sum_map)
     | Prod(list(t))
-    | Module(Ctx.t)
+    | Module(module_typ)
     | Member(Token.t, t)
     | Rec(TypVar.t, t)
     | Forall(TypVar.t, t)
@@ -83,7 +88,13 @@ module rec Typ: {
     | Free(TypVar.t)
     | Internal;
 
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type module_typ = {
+    inner_ctx: Ctx.t,
+    incomplete: bool,
+  };
   /* TYP.T: Hazel types */
+
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
     | Unknown(type_provenance)
@@ -96,7 +107,7 @@ module rec Typ: {
     | Arrow(t, t)
     | Sum(sum_map)
     | Prod(list(t))
-    | Module(Ctx.t)
+    | Module(module_typ)
     | Member(Token.t, t)
     | Rec(TypVar.t, t)
     | Forall(TypVar.t, t)
@@ -167,7 +178,7 @@ module rec Typ: {
         List.map(snd, sm),
       )
     | Prod(tys) => ListUtil.flat_map(free_vars(~bound), tys)
-    | Module(inner_ctx) =>
+    | Module({inner_ctx, _}) =>
       let ctx_entry_subst = (l: list(Token.t), e: Ctx.entry): list(Token.t) => {
         switch (e) {
         | VarEntry(t)
@@ -210,7 +221,7 @@ module rec Typ: {
     | Forall(y, ty) => Forall(y, subst(s, x, ty))
     | List(ty) => List(subst(s, x, ty))
     | Var(y) => TypVar.eq(x, y) ? s : Var(y)
-    | Module(inner_ctx) =>
+    | Module({inner_ctx, incomplete}) =>
       let ctx_entry_subst = (e: Ctx.entry): Ctx.entry => {
         switch (e) {
         | VarEntry(t) => VarEntry({...t, typ: subst(s, x, t.typ)})
@@ -219,7 +230,7 @@ module rec Typ: {
         | TVarEntry(_) => e
         };
       };
-      Module(List.map(ctx_entry_subst, inner_ctx));
+      Module({inner_ctx: List.map(ctx_entry_subst, inner_ctx), incomplete});
     | Member(name, ty) => Member(name, subst(s, x, ty))
     };
   };
@@ -257,7 +268,8 @@ module rec Typ: {
         | _ => false
         };
       };
-      List.equal(entry_equal, ctx1, ctx2);
+      List.equal(entry_equal, ctx1.inner_ctx, ctx2.inner_ctx)
+      && ctx1.incomplete == ctx2.incomplete;
     | (Module(_), _) => false
     | (Rec(x1, t1), Rec(x2, t2))
     | (Forall(x1, t1), Forall(x2, t2)) =>
@@ -399,24 +411,39 @@ module rec Typ: {
       List(ty);
     | (List(_), _) => None
     | (Module(ctx1), Module(ctx2)) =>
+      /* Module types can join if and only if for every variable,
+         Either: it appears in both ctxs and the types can join,
+         Or: it appears only in one ctx and the other ctx is incomplete */
       let join_entry =
-          (ctx2: Ctx.t, ctx_joined: option(Ctx.t), ctx1_entry: Ctx.entry)
+          (
+            {inner_ctx, incomplete}: module_typ,
+            ctx_joined: option(Ctx.t),
+            ctx1_entry: Ctx.entry,
+          )
           : option(Ctx.t) => {
+        let do_incomplete = (entry1: 'a, entry2: option('a)): option('a) =>
+          if (incomplete && entry2 == None) {
+            Some(entry1);
+          } else {
+            entry2;
+          };
         let* ctx_joined = ctx_joined;
         switch (ctx1_entry) {
-        | VarEntry({name, typ, id}) =>
-          let* entry2 = Ctx.lookup_var(ctx2, name);
+        | VarEntry({name, typ, id} as entry1) =>
+          let* entry2 =
+            Ctx.lookup_var(inner_ctx, name) |> do_incomplete(entry1);
           let+ typ_joined = join'(typ, entry2.typ);
           Ctx.extend(ctx_joined, VarEntry({name, typ: typ_joined, id}));
-        | ConstructorEntry({name, typ, id}) =>
-          let* entry2 = Ctx.lookup_ctr(ctx2, name);
+        | ConstructorEntry({name, typ, id} as entry1) =>
+          let* entry2 =
+            Ctx.lookup_ctr(inner_ctx, name) |> do_incomplete(entry1);
           let+ typ_joined = join'(typ, entry2.typ);
           Ctx.extend(
             ctx_joined,
             ConstructorEntry({name, typ: typ_joined, id}),
           );
         | TVarEntry({name, kind, id}) =>
-          let* entry2 = Ctx.lookup_tvar(ctx2, name);
+          let* entry2 = Ctx.lookup_tvar(inner_ctx, name);
           let+ kind_joined =
             switch (kind, entry2.kind) {
             | (Abstract, Abstract) => Some(Kind.Abstract)
@@ -428,8 +455,15 @@ module rec Typ: {
           Ctx.extend(ctx_joined, TVarEntry({name, kind: kind_joined, id}));
         };
       };
-      let* ctx = List.fold_left(join_entry(ctx2), Some([]), ctx1);
-      Some(Module(ctx));
+      let* ctx = List.fold_left(join_entry(ctx2), Some([]), ctx1.inner_ctx);
+      let* ctx =
+        List.fold_left(join_entry(ctx1), Some(ctx), ctx2.inner_ctx);
+      Some(
+        Module({
+          inner_ctx: ctx |> Ctx.filter_duplicates,
+          incomplete: ctx1.incomplete && ctx2.incomplete,
+        }),
+      );
     | (Module(_), _) => None
     };
   }
@@ -488,7 +522,7 @@ module rec Typ: {
     | Arrow(t1, t2) => Arrow(normalize(ctx, t1), normalize(ctx, t2))
     | Prod(ts) => Prod(List.map(normalize(ctx), ts))
     | Sum(ts) => Sum(ConstructorMap.map(Option.map(normalize(ctx)), ts))
-    | Module(inner_ctx) =>
+    | Module({inner_ctx, incomplete}) =>
       let ctx_entry_subst = (e: Ctx.entry): Ctx.entry => {
         switch (e) {
         | VarEntry(t) => VarEntry({...t, typ: normalize(ctx, t.typ)})
@@ -497,7 +531,7 @@ module rec Typ: {
         | TVarEntry(_) => e
         };
       };
-      Module(List.map(ctx_entry_subst, inner_ctx));
+      Module({inner_ctx: List.map(ctx_entry_subst, inner_ctx), incomplete});
     | Member(name, ty) => Member(name, normalize(ctx, ty))
     | Rec(name, ty) =>
       /* NOTE: Dummy tvar added has fake id but shouldn't matter
@@ -641,8 +675,9 @@ module rec Typ: {
            ts,
          )
       ++ ")"
-    | Module([]) => "Module"
-    | Module([e, ...es]) =>
+    | Module({inner_ctx: [], incomplete: false}) => "Module"
+    | Module({inner_ctx: [], incomplete: true}) => "Module{...}"
+    | Module({inner_ctx: [e, ...es], incomplete}) =>
       let view_entry = (m: Ctx.entry): string => {
         switch (m) {
         | VarEntry({name: n0, typ: t0, _})
@@ -663,6 +698,7 @@ module rec Typ: {
            es,
          )
       ++ view_entry(e)
+      ++ (incomplete ? ",..." : "")
       ++ "}";
     | Member(name, _) => name
     | Rec(tv, t) => "rec " ++ tv ++ "->" ++ pretty_print(t)
@@ -886,7 +922,7 @@ and Ctx: {
     | Var(n) =>
       x == n
         ? Var(n) : Member(x ++ "." ++ n, Typ.weak_head_normalize(ctx, ty))
-    | Module(inner_ctx) =>
+    | Module({inner_ctx, incomplete}) =>
       let ctx_entry_modulize = (e: entry): entry => {
         switch (e) {
         | VarEntry(t) => VarEntry({...t, typ: modulize_item(ctx, x, t.typ)})
@@ -895,28 +931,36 @@ and Ctx: {
         | TVarEntry(_) => e
         };
       };
-      Module(List.map(ctx_entry_modulize, inner_ctx));
+      Module({
+        inner_ctx: List.map(ctx_entry_modulize, inner_ctx),
+        incomplete,
+      });
     | Forall(_, t) => modulize_item(ctx, x, t)
     };
   };
 
   let modulize = (ty: Typ.t, x: string): Typ.t => {
     switch (ty) {
-    | Module(ctx) =>
-      Module(
-        List.map(
-          (e: entry): entry => {
-            switch (e) {
-            | VarEntry(t) =>
-              VarEntry({...t, typ: modulize_item(ctx, x, t.typ)})
-            | ConstructorEntry(t) =>
-              ConstructorEntry({...t, typ: modulize_item(ctx, x, t.typ)})
-            | TVarEntry(_) => e
-            }
-          },
-          ctx,
-        ),
-      )
+    | Module({inner_ctx, incomplete}) =>
+      Module({
+        inner_ctx:
+          List.map(
+            (e: entry): entry => {
+              switch (e) {
+              | VarEntry(t) =>
+                VarEntry({...t, typ: modulize_item(inner_ctx, x, t.typ)})
+              | ConstructorEntry(t) =>
+                ConstructorEntry({
+                  ...t,
+                  typ: modulize_item(inner_ctx, x, t.typ),
+                })
+              | TVarEntry(_) => e
+              }
+            },
+            inner_ctx,
+          ),
+        incomplete,
+      })
     | _ => ty
     };
   };
diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re
index 1d75fecbc2..00a39466ec 100644
--- a/src/haz3lweb/view/CursorInspector.re
+++ b/src/haz3lweb/view/CursorInspector.re
@@ -153,7 +153,7 @@ let typ_ok_view = (cls: Term.Cls.t, ok: Info.ok_typ) =>
   | Module(name, inner_ctx) => [
       Type.view(Var(String.sub(name, 0, String.length(name) - 1))),
       text("is a module of type"),
-      Type.view(Module(inner_ctx)),
+      Type.view(Module({inner_ctx, incomplete: false})),
     ]
   | Variant(name, sum_ty) => [
       Type.view(Var(name)),
diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re
index 3b80e8a334..bcc190ced5 100644
--- a/src/haz3lweb/view/Type.re
+++ b/src/haz3lweb/view/Type.re
@@ -84,8 +84,11 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t =>
         }
       ),
     )
-  | Module([]) => div(~attr=clss(["typ-view", "Module"]), [text("Module")])
-  | Module([e, ...es]) =>
+  | Module({inner_ctx: [], incomplete: false}) =>
+    div(~attr=clss(["typ-view", "Module"]), [text("Module")])
+  | Module({inner_ctx: [], incomplete: true}) =>
+    div(~attr=clss(["typ-view", "Module"]), [text("Module{...}")])
+  | Module({inner_ctx: [e, ...es], incomplete}) =>
     let view_entry = (m: Haz3lcore.TypBase.Ctx.entry): list(t) => {
       switch (m) {
       | VarEntry({name: n0, typ: t0, _})
@@ -122,7 +125,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t =>
           )
           @ view_entry(e),
         ),
-        text("}"),
+        text((incomplete ? "..." : "") ++ "}"),
       ],
     );
   | Sum(ts) =>
diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re
index 7a1b3f8e09..ab1cd80cb1 100644
--- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re
+++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re
@@ -130,8 +130,15 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => {
         ]),
         parenthesize,
       )
-    | Module([]) => (text("Module{}"), parenthesize)
-    | Module(entries) =>
+    | Module({inner_ctx: [], incomplete: false}) => (
+        text("Module{}"),
+        parenthesize,
+      )
+    | Module({inner_ctx: [], incomplete: true}) => (
+        text("Module{...}"),
+        parenthesize,
+      )
+    | Module({inner_ctx, incomplete}) =>
       let decomp_entry =
           (m: Haz3lcore.TypBase.Ctx.entry): list((string, Typ.t)) => {
         switch (m) {
@@ -140,7 +147,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => {
         | TVarEntry(_) => []
         };
       };
-      let ntpairs = List.map(decomp_entry, entries) |> List.flatten;
+      let ntpairs = List.map(decomp_entry, inner_ctx) |> List.flatten;
       let center =
         List.mapi(
           (i, (name, ty)) =>
@@ -160,7 +167,14 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => {
              hcats([text(","), choices([linebreak(), space()])]),
            )
         |> hcats;
-      (hcats([text("Module{"), center, text("}")]), parenthesize);
+      (
+        hcats([
+          text("Module{"),
+          center,
+          text((incomplete ? "..." : "") ++ "}"),
+        ]),
+        parenthesize,
+      );
     | Member(name, _) => (text(name), parenthesize)
     | Sum(sum_map) =>
       let center =