Enhance error report: hint module expression of module type id (#51)

lib/typing/check.ml

@@ -50,7 +50,7 @@ let rec check_expr (e : T.expr) (env : Env.t) : expr =
     | T.ESeq (e0, e1) -> check_seq e0 e1 env
   with
   | U.UnificationError (t0, t1) ->
-      Report.unification_error t0 t1 e.start_loc e.end_loc
+      Report.unification_error t0 t1 e.start_loc e.end_loc env
   | U.OccurError (tv, te) -> Report.occur_error tv te e.start_loc e.end_loc
   | e -> raise e
 
@@ -374,6 +374,7 @@ and make_mt_by_scope
       module_dict = _;
       curr;
       history;
+      hints = _;
     } =
   I.MTMod
     {
@@ -387,38 +388,54 @@ and make_mt_by_scope
     }
 
 and check_mod (me : T.mod_expr) (env : Env.t) : mod_expr =
-  match me.node with
-  | T.MEName name -> MEName (name, Env.lookup_module_def name env)
-  | T.MEStruct body ->
-      let body_typed, env' = check_top_levels body (Env.enter_env env) in
-      let scope = absorb_history env' env in
-      let mt = make_mt_by_scope scope in
-      MEStruct (body_typed, mt)
-  | T.MEFunctor ((name, ext_mt0), me1) ->
-      let mt0 = normalize_mt ext_mt0 env in
-      let me1_typed = check_mod me1 (Env.add_module name mt0 env) in
-      MEFunctor ((name, mt0), me1_typed)
-  | T.MEField (me, name) -> (
-      let me_typed = check_mod me env in
-      match get_mod_ty me_typed with
-      | I.MTMod { mod_defs; _ } ->
-          MEField (me_typed, name, List.assoc name mod_defs)
-      | I.MTFun _ -> failwith "try get field from functor")
-  | T.MEApply (me0, me1) -> (
-      let me0_typed = check_mod me0 env in
-      let me1_typed = check_mod me1 env in
-      let mt0 = get_mod_ty me0_typed in
-      let mt1 = get_mod_ty me1_typed in
-      match mt0 with
-      | I.MTMod _ -> failwith "try apply a structure"
-      | I.MTFun (para_mt, body_mt) ->
-          MEApply
-            (me0_typed, me1_typed, apply_functor para_mt body_mt mt1 env))
-  | T.MERestrict (me, mt) ->
-      let me_typed = check_mod me env in
-      let mt = normalize_mt mt env in
-      let _subst = check_subtype (get_mod_ty me_typed) mt in
-      MERestrict (me_typed, mt, shift_mt mt env)
+  let me_typed =
+    match me.node with
+    | T.MEName name -> check_mod_name name env
+    | T.MEStruct body -> check_struct body env
+    | T.MEFunctor ((name, ext_mt0), me1) ->
+        check_functor name ext_mt0 me1 env
+    | T.MEField (me, name) -> check_mod_field me name env
+    | T.MEApply (me0, me1) -> check_mod_apply me0 me1 env
+    | T.MERestrict (me, mt) -> check_mod_restrict me mt env
+  in
+  Env.try_record_hint me_typed env;
+  me_typed
+
+and check_mod_name name env = MEName (name, Env.lookup_module_def name env)
+
+and check_struct body env =
+  let body_typed, env' = check_top_levels body (Env.enter_env env) in
+  let scope = absorb_history env' env in
+  let mt = make_mt_by_scope scope in
+  MEStruct (body_typed, mt)
+
+and check_functor name ext_mt0 me1 env =
+  let mt0 = normalize_mt ext_mt0 env in
+  let me1_typed = check_mod me1 (Env.add_module name mt0 env) in
+  MEFunctor ((name, mt0), me1_typed)
+
+and check_mod_field me name env =
+  let me_typed = check_mod me env in
+  match get_mod_ty me_typed with
+  | I.MTMod { mod_defs; _ } ->
+      MEField (me_typed, name, List.assoc name mod_defs)
+  | I.MTFun _ -> failwith "try get field from functor"
+
+and check_mod_apply me0 me1 env =
+  let me0_typed = check_mod me0 env in
+  let me1_typed = check_mod me1 env in
+  let mt0 = get_mod_ty me0_typed in
+  let mt1 = get_mod_ty me1_typed in
+  match mt0 with
+  | I.MTMod _ -> failwith "try apply a structure"
+  | I.MTFun (para_mt, body_mt) ->
+      MEApply (me0_typed, me1_typed, apply_functor para_mt body_mt mt1 env)
+
+and check_mod_restrict me mt env =
+  let me_typed = check_mod me env in
+  let mt = normalize_mt mt env in
+  let _subst = check_subtype (get_mod_ty me_typed) mt in
+  MERestrict (me_typed, mt, shift_mt mt env)
 
 (* apply a functor, add returned module type's id into environment *)
 and apply_functor para_mt body_mt arg_mt env =

lib/typing/env.ml

@@ -1,4 +1,5 @@
 module I = Types_in
+module T = Typedtree
 
 type scope = {
   values : (string * I.bind_ty) list;
@@ -9,7 +10,8 @@ type scope = {
   module_dict : (int * I.mod_ty) list;
       (* UNUSED FIELD: designed for caching module id to their definition *)
   curr : int;
-  history : int list ref;
+  history : int list ref; (* module ids created in this scope *)
+  hints : (int * T.mod_expr) list ref;
 }
 
 type t = scope list
@@ -72,6 +74,15 @@ let record_history id (env : t) =
   | [] -> failwith "neverreach"
   | s :: _ -> s.history := id :: !(s.history)
 
+let try_record_hint me_typed (env : t) =
+  match env with
+  | [] -> failwith "neverreach"
+  | s :: _ -> (
+      let mt = T.get_mod_ty me_typed in
+      match mt with
+      | I.MTMod { id; _ } -> s.hints := (id, me_typed) :: !(s.hints)
+      | _ -> ())
+
 let record_all_history ids (env : t) =
   match env with
   | [] -> failwith "neverreach"
@@ -119,6 +130,14 @@ let rec lookup_type_def tn env =
       | Some def -> (s.curr, def)
       | None -> lookup_type_def tn env')
 
+let rec lookup_hint id env =
+  match env with
+  | [] -> None
+  | s :: env' -> (
+      match List.assoc_opt id !(s.hints) with
+      | None -> lookup_hint id env'
+      | Some me -> Some me)
+
 let get_curr env =
   match env with
   | s :: _ -> s.curr
@@ -134,6 +153,7 @@ let init_scope () =
     module_dict = [];
     curr = 0;
     history = ref [];
+    hints = ref [];
   }
 
 let init () = [ init_scope () ]

lib/typing/render.ml

@@ -174,7 +174,7 @@ module MakePP (Config : PPConfig) = struct
       Fmt.fprintf fmt "@]@])")
     else content_printer ()
 
-  and pp_mod fmt me =
+  and pp_mod fmt ?(env : Env.t option) me =
     match me with
     | MEName (name, _) -> Fmt.pp_print_string fmt name
     | MEStruct (tops, mt) ->
@@ -192,27 +192,27 @@ module MakePP (Config : PPConfig) = struct
         Fmt.fprintf fmt "@[<v 2>functor (%s : " name;
         pp_mod_ty fmt mt;
         Fmt.fprintf fmt ")@\n-> @\n";
-        pp_mod fmt me;
+        pp_mod fmt ?env me;
         Fmt.fprintf fmt "@]"
     | MEField (me, name, _) ->
         Fmt.fprintf fmt "@[";
-        pp_mod fmt me;
+        pp_mod fmt ?env me;
         Fmt.fprintf fmt ".%s" name;
         Fmt.fprintf fmt "@]"
     | MEApply (me0, me1, mt) ->
         pp_is_mod_ty fmt Config.show_mod_ty
           (fun _ ->
-            pp_mod fmt me0;
+            pp_mod fmt ?env me0;
             Fmt.fprintf fmt "(";
-            pp_mod fmt me1;
+            pp_mod fmt ?env me1;
             Fmt.fprintf fmt ")")
           mt
     | MERestrict (me, mt, mt') ->
         pp_is_mod_ty fmt Config.show_mod_ty
           (fun _ ->
             Fmt.fprintf fmt "(";
             Fmt.fprintf fmt "@[";
-            pp_mod fmt me;
+            pp_mod fmt ?env me;
             Fmt.fprintf fmt " : ";
             Fmt.fprintf fmt "@[";
             pp_mod_ty fmt mt;
@@ -298,12 +298,12 @@ module MakePP (Config : PPConfig) = struct
         pp_ty fmt te;
         Fmt.fprintf fmt "@]"
 
-  and pp_ty fmt te =
+  and pp_ty fmt ?env te =
     match te with
     | I.TConsI ((id, name), tes) ->
         Fmt.fprintf fmt "@[";
         (match tes with
-        | [] -> Fmt.fprintf fmt "()"
+        | [] -> Fmt.fprintf fmt "()@ "
         | te0 :: tes ->
             Fmt.fprintf fmt "(";
             pp_ty fmt te0;
@@ -312,8 +312,14 @@ module MakePP (Config : PPConfig) = struct
                 Fmt.fprintf fmt ",@ ";
                 pp_ty fmt te)
               tes;
-            Fmt.fprintf fmt ")");
-        Fmt.fprintf fmt "@ %d.%s" id name;
+            Fmt.fprintf fmt ")@ ");
+        (match (Option.bind env (Env.lookup_hint id), id) with
+        | Some me, _ ->
+            pp_mod fmt ?env me;
+            Fmt.fprintf fmt "."
+        | None, 0 (* 0 is default root module's structure type id *) -> ()
+        | None, _ -> Fmt.fprintf fmt "%d." id);
+        Fmt.fprintf fmt "%s" name;
         Fmt.fprintf fmt "@]"
     | I.TVarI { contents = I.Unbound tv } ->
         Fmt.fprintf fmt "{%s}" (Ident.show_ident tv)
@@ -455,10 +461,10 @@ module MakePP (Config : PPConfig) = struct
       prog;
     Format.pp_print_flush fmt ()
 
-  let pp_str_of_ty ty =
+  let pp_str_of_ty ?env ty =
     let buf = Buffer.create 10 in
     let formatter = Fmt.formatter_of_buffer buf in
-    pp_ty formatter ty;
+    pp_ty formatter ?env ty;
     Fmt.pp_print_flush formatter ();
     Buffer.contents buf
 end
@@ -471,7 +477,16 @@ module ShowAllConfig : PPConfig = struct
   let show_mod_ty = true
 end
 
+module ShowNothingConfig : PPConfig = struct
+  let show_const_ty = false
+
+  let show_bind_ty = false
+
+  let show_mod_ty = false
+end
+
 module DefaultPP = MakePP (ShowAllConfig)
+module NoTypeHintPP = MakePP (ShowNothingConfig)
 
 let default_dbg prog =
   let buf = Buffer.create 50 in

lib/typing/report.ml

@@ -1,15 +1,16 @@
 module T = Types_in
-module PP = Render.DefaultPP
+module PP = Render.NoTypeHintPP
 
 type err =
   | UnificationError of (T.ty * T.ty * Lexing.position * Lexing.position)
 
 (* error reportings *)
 (* todo: support error tolerable type checking *)
-exception UnificationError of T.ty * T.ty * Lexing.position * Lexing.position
+exception
+  UnificationError of T.ty * T.ty * Lexing.position * Lexing.position * Env.t
 
-let unification_error t0 t1 loc1 loc2 =
-  raise (UnificationError (t0, t1, loc1, loc2))
+let unification_error t0 t1 loc1 loc2 env =
+  raise (UnificationError (t0, t1, loc1, loc2, env))
 
 exception ComponentInCompatible of string * T.bind_ty * T.bind_ty
 
@@ -33,10 +34,10 @@ let unknown_location () = Printf.printf "At some unknown location: "
 
 let wrap_with_error_report f =
   try Some (f ()) with
-  | UnificationError (t0, t1, start, last) ->
+  | UnificationError (t0, t1, start, last, env) ->
       print_code_range start last;
-      Printf.printf "Can't unify `%s` with `%s`" (PP.pp_str_of_ty t0)
-        (PP.pp_str_of_ty t1);
+      Printf.printf "Can't unify `%s` with `%s`" (PP.pp_str_of_ty ~env t0)
+        (PP.pp_str_of_ty ~env t1);
       None
   | OccurError (tv, te, start, last) ->
       print_code_range start last;