diff --git a/bin/main.ml b/bin/main.ml
index 3a79a52..5aaebe6 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -2,7 +2,8 @@ let usage =
   {|coollang toolchain
 
 사용법:
-  cool check <file.cool>...   타입/effect/capability 검사 (fast path)
+  cool check <file.cool>...   타입/effect/capability 검사 (import를 따라 모듈 그래프 전체)
+  cool iface <file.cool>      interface 표면과 해시 출력
   cool run <file.cool>        typed IR 인터프리터로 실행
   cool tokens <file.cool>     토큰 덤프 (렉서 디버깅)
   cool ast <file.cool>        구문 트리 덤프 (파서 디버깅)
@@ -32,6 +33,33 @@ let dump_ast file =
         m.Coollang.Ast.items;
       0
 
+(* import를 따라 모듈 그래프를 로드하고 전부 검사한다. root는 첫 파일의 디렉터리다. *)
+let check_graph files =
+  match files with
+  | [] ->
+      prerr_endline "검사할 파일이 없습니다";
+      2
+  | first :: _ ->
+      let st = Coollang.Session.create ~root:(Filename.dirname first) () in
+      List.iter (fun f -> Coollang.Session.load st f) files;
+      let errors = Coollang.Session.errors st in
+      List.iter
+        (fun e -> prerr_endline (Coollang.Session.string_of_error e))
+        errors;
+      if errors = [] then 0 else 1
+
+let dump_iface file =
+  let st = Coollang.Session.create ~root:(Filename.dirname file) () in
+  Coollang.Session.load st file;
+  match Coollang.Session.find st file with
+  | None -> 1
+  | Some e ->
+      Printf.printf "hash %s\n" e.iface.Coollang.Iface.hash;
+      List.iter
+        (fun it -> print_endline (Coollang.Ast.show_item it))
+        e.iface.Coollang.Iface.items;
+      0
+
 let dump_deps file =
   match Coollang.Driver.resolve file with
   | Error errors -> report_errors errors
@@ -46,7 +74,8 @@ let () =
   let argv = Array.to_list Sys.argv in
   let code =
     match List.tl argv with
-    | "check" :: files -> report (Coollang.Driver.check files)
+    | "check" :: files -> check_graph files
+    | [ "iface"; file ] -> dump_iface file
     | [ "run"; file ] -> report (Coollang.Driver.run file)
     | [ "tokens"; file ] -> dump_tokens file
     | [ "ast"; file ] -> dump_ast file
diff --git a/lib/ast.ml b/lib/ast.ml
index 8940e40..ddd365f 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -11,7 +11,14 @@ type eff_atom = Eff_var of string | Eff_set of eff_name list
 type eff_result = eff_atom list (* 합집합. 길이 1이면 단일 *)
 
 type ty =
-  | T_named of { name : string; args : targ list; pos : pos }
+  (* modl: 다른 모듈의 타입은 별칭으로 한정한다 (Shapes.Shape).
+     한정하지 않으면 이 모듈의 이름이다 — 암묵적으로 끌어오지 않는다. *)
+  | T_named of {
+      modl : string option;
+      name : string;
+      args : targ list;
+      pos : pos;
+    }
   | T_fn of {
       affine : bool;
       params : ty list;
@@ -28,7 +35,12 @@ type pattern =
   | P_wild of pos
   | P_lit of lit * pos
   | P_bind of string * pos
-  | P_ctor of { name : string; args : pattern list; pos : pos }
+  | P_ctor of {
+      modl : string option;
+      name : string;
+      args : pattern list;
+      pos : pos;
+    }
 
 type unop = U_not | U_neg
 
@@ -164,7 +176,8 @@ let buf_eff_atom b = function
         names
 
 let rec buf_ty b = function
-  | T_named { name; args; _ } ->
+  | T_named { modl; name; args; _ } ->
+      let name = match modl with None -> name | Some m -> m ^ "." ^ name in
       if args = [] then Buffer.add_string b name
       else (
         Buffer.add_string b ("(" ^ name);
@@ -202,7 +215,8 @@ let rec buf_pattern b = function
   | P_wild _ -> Buffer.add_char b '_'
   | P_lit (l, _) -> buf_lit b l
   | P_bind (n, _) -> Buffer.add_string b n
-  | P_ctor { name; args; _ } ->
+  | P_ctor { modl; name; args; _ } ->
+      let name = match modl with None -> name | Some m -> m ^ "." ^ name in
       Buffer.add_string b ("(" ^ name);
       List.iter
         (fun p ->
diff --git a/lib/exhaust.ml b/lib/exhaust.ml
index 25158f4..5a66871 100644
--- a/lib/exhaust.ml
+++ b/lib/exhaust.ml
@@ -56,7 +56,8 @@ let rec of_pattern env (p : Ast.pattern) : cpat =
   | Ast.P_lit (Ast.L_int n, _) -> CCtor ("<" ^ n ^ ">", [])
   | Ast.P_lit (Ast.L_str v, _) -> CCtor ("<" ^ String.escaped v ^ ">", [])
   | Ast.P_bind (n, _) -> if env.is_ctor n then CCtor (n, []) else CWild
-  | Ast.P_ctor { name; args; _ } ->
+  | Ast.P_ctor { modl; name; args; _ } ->
+      let name = match modl with Some a -> a ^ "." ^ name | None -> name in
       if env.is_ctor name then CCtor (name, List.map (of_pattern env) args)
       else CWild
 
diff --git a/lib/iface.ml b/lib/iface.ml
new file mode 100644
index 0000000..4294c8f
--- /dev/null
+++ b/lib/iface.ml
@@ -0,0 +1,193 @@
+(* interface artifact와 그 해시.
+
+   hash 입력 = 모듈 exported surface 전체의 의미적 정규형이다 (문서 P7).
+   함수 시그니처(effect 포함), 타입 정의 본문(struct 필드, enum variant),
+   타입의 affinity, 상수의 타입과 값, capability 선언, 그리고 reexport된
+   선언을 완전히 해소한 정의 본문.
+
+   원칙: downstream 검사 결과에 영향을 줄 수 있는 모든 것을 포함한다.
+   의심스러우면 넣는다 — 과잉 포함의 비용은 재검사지만 누락의 비용은
+   잘못된 캐시라는 비대칭이 있다.
+
+   함수 본문은 들어가지 않는다. 본문 한 줄 수정이 해시를 흔들면 incremental
+   전제가 무너진다. *)
+
+open Ast
+
+type t = { items : item list; (* 본문을 벗긴 exported surface *) hash : string }
+
+let strip_body (d : fn_decl) = { d with fn_body = None }
+
+let is_exported = function
+  | I_fn { pub; _ } -> pub
+  | I_struct { pub; _ } -> pub
+  | I_enum { pub; _ } -> pub
+  | I_capability { pub; _ } -> pub
+  | I_const { pub; _ } -> pub
+  | I_reexport _ -> true
+  | I_import _ -> false
+
+let strip = function
+  | I_fn { pub; decl } -> I_fn { pub; decl = strip_body decl }
+  | it -> it
+
+let item_name = function
+  | I_fn { decl; _ } -> decl.fn_name
+  | I_struct { name; _ } -> name
+  | I_enum { name; _ } -> name
+  | I_capability { name; _ } -> name
+  | I_const { name; _ } -> name
+  | I_reexport { name; _ } -> name
+  | I_import { alias; _ } -> alias
+
+(* reexport는 이름이 아니라 해소된 정의 본문이 hash에 들어간다.
+   A의 enum에 variant가 추가되면 B의 소스가 그대로여도 B의 hash가 변하고,
+   C의 exhaustive match가 재검사된다. *)
+let surface (m : modul) : item list =
+  let is_definition = function
+    | I_reexport _ | I_import _ -> false
+    | _ -> true
+  in
+  let find name =
+    List.find_opt (fun it -> is_definition it && item_name it = name) m.items
+  in
+  List.concat_map
+    (fun it ->
+      match it with
+      | I_reexport { name; _ } -> (
+          match find name with Some d -> [ strip d ] | None -> [])
+      | it when is_exported it && is_definition it -> [ strip it ]
+      | _ -> [])
+    m.items
+
+(* 정규형: 항목을 이름순으로 정렬해 선언 순서가 해시에 새지 않게 한다.
+   소스에서 함수 둘의 위치를 바꾸는 것은 downstream에 아무 영향이 없다. *)
+let render (items : item list) : string =
+  items |> List.map show_item |> List.sort compare |> String.concat "\n"
+
+let of_module (m : modul) : t =
+  let items = surface m in
+  { items; hash = Digest.to_hex (Digest.string (render items)) }
+
+(* ------------------------------------------------------------------ *)
+(* 소비 측 한정                                                        *)
+(* ------------------------------------------------------------------ *)
+
+(* 가져온 모듈의 exported surface를 소비 측 이름 공간으로 옮긴다.
+   `import "shapes" as Shapes`라면 Shape는 "Shapes.Shape"가 된다.
+
+   왜 소비 시점인가 — 별칭은 가져오는 쪽의 선택이므로 정의한 모듈의
+   interface hash에 새어서는 안 된다. of_module은 한정하지 않은 표면을
+   해시하고, 한정은 여기서만 한다.
+
+   v0의 한계 두 가지, 의도적으로 남긴다:
+   - 가져온 모듈이 다시 다른 모듈의 타입을 참조하면(전이 참조) 불투명해진다.
+   - effect atom의 capability 이름은 한정하지 않는다. 즉 effect 이름은 v0에서
+     전역이다. 모듈별 identity는 v1 과제다. *)
+
+let builtin_ty_names =
+  [ "Int"; "Bool"; "String"; "Unit"; "List"; "Option"; "Result"; "TaskScope" ]
+
+let opaque pos = T_named { modl = None; name = "«외부»"; args = []; pos }
+
+let rec q_ty alias defined gen (t : ty) : ty =
+  match t with
+  | T_named { modl = Some _; pos; _ } -> opaque pos
+  | T_named { modl = None; name; args; pos } ->
+      let args = List.map (q_targ alias defined gen) args in
+      if List.mem name gen || List.mem name builtin_ty_names then
+        T_named { modl = None; name; args; pos }
+      else if List.mem name defined then
+        T_named { modl = None; name = alias ^ "." ^ name; args; pos }
+      else opaque pos
+  | T_fn { affine; params; eff; ret; pos } ->
+      T_fn
+        {
+          affine;
+          params = List.map (q_ty alias defined gen) params;
+          eff;
+          ret = Option.map (q_ty alias defined gen) ret;
+          pos;
+        }
+
+and q_targ alias defined gen = function
+  | TA_ty t -> TA_ty (q_ty alias defined gen t)
+  | TA_eff e -> TA_eff e
+
+let q_fn alias defined (d : fn_decl) : fn_decl =
+  let gen = List.map (fun g -> g.gp_name) d.fn_gen in
+  {
+    d with
+    fn_params =
+      List.map
+        (fun p -> { p with p_ty = q_ty alias defined gen p.p_ty })
+        d.fn_params;
+    fn_ret = Option.map (q_ty alias defined gen) d.fn_ret;
+    fn_body = None;
+  }
+
+let defined_names (items : item list) =
+  List.filter_map
+    (function
+      | I_struct { name; _ } | I_enum { name; _ } | I_capability { name; _ } ->
+          Some name
+      | _ -> None)
+    items
+
+let qualify (alias : string) (items : item list) : item list =
+  let defined = defined_names items in
+  let p n = alias ^ "." ^ n in
+  List.map
+    (fun it ->
+      match it with
+      | I_fn { pub; decl } ->
+          I_fn
+            {
+              pub;
+              decl = { (q_fn alias defined decl) with fn_name = p decl.fn_name };
+            }
+      | I_struct { pub; copyable; name; gen; fields; pos } ->
+          let g = List.map (fun x -> x.gp_name) gen in
+          I_struct
+            {
+              pub;
+              copyable;
+              name = p name;
+              gen;
+              fields =
+                List.map
+                  (fun f -> { f with f_ty = q_ty alias defined g f.f_ty })
+                  fields;
+              pos;
+            }
+      | I_enum { pub; name; gen; variants; pos } ->
+          let g = List.map (fun x -> x.gp_name) gen in
+          I_enum
+            {
+              pub;
+              name = p name;
+              gen;
+              variants =
+                List.map
+                  (fun v ->
+                    {
+                      v with
+                      v_name = p v.v_name;
+                      v_args = List.map (q_ty alias defined g) v.v_args;
+                    })
+                  variants;
+              pos;
+            }
+      | I_capability { pub; name; methods; pos } ->
+          I_capability
+            {
+              pub;
+              name = p name;
+              methods = List.map (q_fn alias defined) methods;
+              pos;
+            }
+      | I_const { pub; name; ty; value; pos } ->
+          I_const
+            { pub; name = p name; ty = q_ty alias defined [] ty; value; pos }
+      | it -> it)
+    items
diff --git a/lib/move.ml b/lib/move.ml
index 8483e6b..e93a8ec 100644
--- a/lib/move.ml
+++ b/lib/move.ml
@@ -55,7 +55,8 @@ let builtin_containers = [ "List"; "Option"; "Result" ]
 let rec ty_affine st (t : Ast.ty) =
   match t with
   | T_fn { affine; _ } -> affine
-  | T_named { name; args; _ } ->
+  | T_named { modl; name; args; _ } ->
+      let name = match modl with Some a -> a ^ "." ^ name | None -> name in
       let self =
         match Hashtbl.find_opt st.aff name with Some b -> b | None -> false
       in
@@ -68,7 +69,7 @@ let rec ty_affine st (t : Ast.ty) =
 
 (* capability가 뿌리다. struct/enum은 필드에서 전이된다. 상호 재귀 타입을 위해
    변화가 없을 때까지 돈다. *)
-let derive_affinity st (m : modul) =
+let derive_affinity st (items : item list) =
   List.iter
     (fun it ->
       match it with
@@ -76,7 +77,7 @@ let derive_affinity st (m : modul) =
       | I_struct { name; _ } -> Hashtbl.replace st.aff name false
       | I_enum { name; _ } -> Hashtbl.replace st.aff name false
       | _ -> ())
-    m.items;
+    items;
   let changed = ref true in
   while !changed do
     changed := false;
@@ -96,7 +97,7 @@ let derive_affinity st (m : modul) =
                  (fun v -> List.exists (ty_affine st) v.v_args)
                  variants)
         | _ -> ())
-      m.items
+      items
   done;
   (* copyable 선언과 affine 필드는 공존할 수 없다 *)
   List.iter
@@ -112,7 +113,7 @@ let derive_affinity st (m : modul) =
             fields;
           ignore pos
       | _ -> ())
-    m.items
+    items
 
 (* ------------------------------------------------------------------ *)
 (* 스코프                                                              *)
@@ -398,7 +399,8 @@ and callee_info st callee =
           with
           | Some f -> Some f
           | None -> None)
-      | None -> None)
+      (* 모듈 별칭을 통한 호출: 가져온 함수는 "Alias.f" 키로 들어와 있다 *)
+      | None -> Hashtbl.find_opt st.fns (o ^ "." ^ name))
   | _ -> None
 
 (* ------------------------------------------------------------------ *)
@@ -431,7 +433,7 @@ let check_fn st (d : fn_decl) =
       | _ -> ());
       pop st
 
-let check (m : modul) : error list =
+let check ?(imports : item list = []) (m : modul) : error list =
   let st =
     {
       aff = Hashtbl.create 16;
@@ -445,7 +447,7 @@ let check (m : modul) : error list =
       errors = [];
     }
   in
-  derive_affinity st m;
+  derive_affinity st (imports @ m.items);
   List.iter
     (fun it ->
       match it with
@@ -459,7 +461,7 @@ let check (m : modul) : error list =
                  (d.fn_name, { f_params = d.fn_params; f_ret = d.fn_ret }))
                methods)
       | _ -> ())
-    m.items;
+    (imports @ m.items);
   List.iter
     (fun it -> match it with I_fn { decl; _ } -> check_fn st decl | _ -> ())
     m.items;
diff --git a/lib/parser.ml b/lib/parser.ml
index 86aaa36..aea7d2c 100644
--- a/lib/parser.ml
+++ b/lib/parser.ml
@@ -129,8 +129,14 @@ let rec parse_ty st =
   | Token.Ident n ->
       let p = pos st in
       adv st;
+      let modl, n =
+        if kind st = Token.Dot then (
+          adv st;
+          (Some n, ident st "타입 이름"))
+        else (None, n)
+      in
       let args = if kind st = Token.LBracket then parse_targs st else [] in
-      T_named { name = n; args; pos = p }
+      T_named { modl; name = n; args; pos = p }
   | _ -> err_expect st "타입"
 
 and parse_fn_ty st affine p =
@@ -190,8 +196,14 @@ let rec parse_pattern st =
   | Token.Kw_false ->
       adv st;
       P_lit (L_bool false, p)
-  | Token.Ident n ->
+  | Token.Ident n -> (
       adv st;
+      let modl, n =
+        if kind st = Token.Dot then (
+          adv st;
+          (Some n, ident st "생성자 이름"))
+        else (None, n)
+      in
       if kind st = Token.LParen then (
         adv st;
         let rec loop acc =
@@ -203,8 +215,11 @@ let rec parse_pattern st =
         in
         let args = if kind st = Token.RParen then [] else loop [] in
         expect_close st Token.RParen ")";
-        P_ctor { name = n; args; pos = p })
-      else P_bind (n, p)
+        P_ctor { modl; name = n; args; pos = p })
+      else
+        match modl with
+        | Some _ -> P_ctor { modl; name = n; args = []; pos = p }
+        | None -> P_bind (n, p))
   | _ -> err_expect st "패턴"
 
 (* ------------------------------------------------------------------ *)
diff --git a/lib/resolve.ml b/lib/resolve.ml
index 70c62ea..cb29e34 100644
--- a/lib/resolve.ml
+++ b/lib/resolve.ml
@@ -77,7 +77,12 @@ let resolve_eff_atom st = function
         names
 
 let rec resolve_ty st = function
-  | T_named { name; args; pos } ->
+  (* 한정된 이름은 별칭이 이 모듈에 있는지만 본다. 그 모듈 안에 그 타입이
+     있는지는 모듈 하나만 보고 결정할 수 없다 — 외부 참조로 기록한다. *)
+  | T_named { modl = Some a; args; pos; _ } ->
+      if Hashtbl.find_opt st.items a <> Some K_import then external_ref st a pos;
+      List.iter (resolve_targ st pos) args
+  | T_named { modl = None; name; args; pos } ->
       if
         (not (List.mem name st.ty_params))
         && (not (List.mem name builtin_types))
@@ -118,7 +123,10 @@ let rec resolve_pattern st seen = function
           else (
             seen := n :: !seen;
             bind st pos n false))
-  | P_ctor { name; args; pos } ->
+  | P_ctor { modl = Some a; args; pos; _ } ->
+      if Hashtbl.find_opt st.items a <> Some K_import then external_ref st a pos;
+      List.iter (resolve_pattern st seen) args
+  | P_ctor { modl = None; name; args; pos } ->
       (match Hashtbl.find_opt st.ctors name with
       | Some (enum, arity) when arity <> List.length args ->
           error st pos
@@ -144,7 +152,7 @@ let rec resolve_expr st = function
         else external_ref st n pos
   | E_list (xs, _) -> List.iter (resolve_expr st) xs
   | E_struct { name; fields; pos } ->
-      resolve_ty st (T_named { name; args = []; pos });
+      resolve_ty st (T_named { modl = None; name; args = []; pos });
       List.iter (fun (_, e) -> resolve_expr st e) fields
   | E_closure c ->
       push st;
diff --git a/lib/session.ml b/lib/session.ml
new file mode 100644
index 0000000..a90968e
--- /dev/null
+++ b/lib/session.ml
@@ -0,0 +1,181 @@
+(* 모듈 로딩, interface 캐시, 그리고 고정점 invalidation.
+
+   여기가 v0가 존재하는 이유다. 검사 자체보다 "무엇을 다시 검사해야 하는가"를
+   좁게 유지하는 것이 아키텍처의 주장이고, 그 주장은 측정으로만 증명된다.
+
+   전파는 고정점 규칙이다 (문서 P8):
+     1. 변경된 모듈 자체를 재검사
+     2. 재검사 전후의 interface hash를 비교
+     3. 달라졌을 때만 그 모듈의 dependents를 큐에 추가
+     4. 큐가 빌 때까지 반복
+   순서가 중요하다. dependents를 먼저 재검사하면 "본문만 수정 시 downstream
+   0건"이 성립하지 않는다 — hash 비교가 dependents 재검사보다 앞서야 한다. *)
+
+type error = { file : string; line : int; col : int; message : string }
+
+let string_of_error { file; line; col; message } =
+  Printf.sprintf "%s:%d:%d: %s" file line col message
+
+type entry = {
+  path : string;
+  ast : Ast.modul;
+  imports : (string * string) list; (* 별칭 -> 해소된 경로 *)
+  iface : Iface.t;
+  errors : error list;
+}
+
+type t = {
+  root : string;
+  modules : (string, entry) Hashtbl.t;
+  (* 통계: 무엇이 몇 번 재검사됐는지. 측정이 목적이므로 처음부터 센다. *)
+  mutable checked : string list;
+}
+
+let create ?(root = ".") () =
+  { root; modules = Hashtbl.create 16; checked = [] }
+
+(* 패키지 경로와 지역 모듈 경로를 구분한다. 첫 세그먼트에 점이 있으면
+   패키지 참조다 (cool.dev/std/list). v0에는 패키지 해소가 없으므로 그런
+   import는 불투명하게 남는다 — 없다고 말하지 않는다. *)
+let is_package path =
+  match String.index_opt path '/' with
+  | Some i -> String.contains (String.sub path 0 i) '.'
+  | None -> String.contains path '.'
+
+let resolve_import st path = Filename.concat st.root (path ^ ".cool")
+
+let read_file file =
+  let ic = open_in_bin file in
+  let n = in_channel_length ic in
+  let s = really_input_string ic n in
+  close_in ic;
+  s
+
+let err_of file (pos : Token.pos) msg =
+  { file; line = pos.line; col = pos.col; message = msg }
+
+let parse_file file =
+  match Lexer.lex_result (read_file file) with
+  | Error e -> Error (err_of file e.pos e.msg)
+  | Ok toks -> (
+      match Parser.parse_result toks with
+      | Error e -> Error (err_of file e.pos e.msg)
+      | Ok m -> Ok m)
+
+let imports_of (m : Ast.modul) =
+  List.filter_map
+    (function
+      | Ast.I_import { path; alias; _ } -> Some (alias, path) | _ -> None)
+    m.items
+
+(* 한 모듈을 검사한다. 의존 모듈의 interface는 이미 로드되어 있어야 한다. *)
+let check_module st path : entry =
+  st.checked <- path :: st.checked;
+  match parse_file path with
+  | Error e ->
+      {
+        path;
+        ast = { items = [] };
+        imports = [];
+        iface = { items = []; hash = "" };
+        errors = [ e ];
+      }
+  | Ok ast ->
+      let imports =
+        List.filter_map
+          (fun (a, p) ->
+            if is_package p then None else Some (a, resolve_import st p))
+          (imports_of ast)
+      in
+      (* 의존 모듈의 exported surface를 소비 측 별칭으로 한정해 합친다.
+         여기서부터 검사기는 "이 모듈 + 아는 외부 표면"만 본다. *)
+      let dep_surface =
+        List.concat_map
+          (fun (alias, p) ->
+            match Hashtbl.find_opt st.modules p with
+            | Some e -> Iface.qualify alias e.iface.Iface.items
+            | None -> [])
+          imports
+      in
+      let iface = Iface.of_module ast in
+      let _, rerrors = Resolve.resolve ast in
+      let errors =
+        List.map (fun (e : Resolve.error) -> err_of path e.pos e.msg) rerrors
+      in
+      let errors =
+        if errors <> [] then errors
+        else
+          List.map
+            (fun (e : Typecheck.error) -> err_of path e.pos e.msg)
+            (Typecheck.check ~imports:dep_surface ast)
+          @ List.map
+              (fun (e : Move.error) -> err_of path e.pos e.msg)
+              (Move.check ~imports:dep_surface ast)
+      in
+      let errors =
+        List.sort (fun a b -> compare (a.line, a.col) (b.line, b.col)) errors
+      in
+      { path; ast; imports; iface; errors }
+
+(* 의존 순서대로 로드한다. 순환은 오류다. *)
+let rec load st ?(visiting = []) path : unit =
+  if Hashtbl.mem st.modules path then ()
+  else if List.mem path visiting then ()
+  else if not (Sys.file_exists path) then
+    Hashtbl.replace st.modules path
+      {
+        path;
+        ast = { items = [] };
+        imports = [];
+        iface = { items = []; hash = "" };
+        errors =
+          [ { file = path; line = 0; col = 0; message = "모듈을 찾을 수 없습니다" } ];
+      }
+  else begin
+    (match parse_file path with
+    | Error _ -> ()
+    | Ok ast ->
+        List.iter
+          (fun (_, p) ->
+            if not (is_package p) then
+              load st ~visiting:(path :: visiting) (resolve_import st p))
+          (imports_of ast));
+    Hashtbl.replace st.modules path (check_module st path)
+  end
+
+let dependents st path =
+  Hashtbl.fold
+    (fun p e acc ->
+      if List.exists (fun (_, d) -> d = path) e.imports then p :: acc else acc)
+    st.modules []
+
+(* 고정점 전파. 반환값은 실제로 재검사한 모듈 목록이다. *)
+let recheck st (changed : string list) : string list =
+  st.checked <- [];
+  let queue = ref changed in
+  let seen = Hashtbl.create 8 in
+  while !queue <> [] do
+    let path = List.hd !queue in
+    queue := List.tl !queue;
+    if not (Hashtbl.mem seen path) then begin
+      Hashtbl.replace seen path ();
+      let before =
+        match Hashtbl.find_opt st.modules path with
+        | Some e -> e.iface.Iface.hash
+        | None -> ""
+      in
+      let entry = check_module st path in
+      Hashtbl.replace st.modules path entry;
+      (* hash 비교가 dependents 재검사보다 앞선다 *)
+      if entry.iface.Iface.hash <> before then
+        queue := !queue @ dependents st path
+    end
+  done;
+  List.rev st.checked
+
+let errors st =
+  Hashtbl.fold (fun _ e acc -> e.errors @ acc) st.modules []
+  |> List.sort (fun a b ->
+      compare (a.file, a.line, a.col) (b.file, b.line, b.col))
+
+let find st path = Hashtbl.find_opt st.modules path
diff --git a/lib/typecheck.ml b/lib/typecheck.ml
index f1c67ee..3edf47a 100644
--- a/lib/typecheck.ml
+++ b/lib/typecheck.ml
@@ -26,6 +26,9 @@ type env = {
   fns : (string, scheme) Hashtbl.t;
   consts : (string, T.t) Hashtbl.t;
   ctors : (string, string) Hashtbl.t; (* variant -> enum *)
+  (* 가져온 모듈의 별칭. `Alias.x`는 "Alias.x"라는 하나의 키로 찾는다 —
+     별칭은 식별자에 쓸 수 없는 점(.)을 포함하므로 지역 이름과 충돌하지 않는다. *)
+  aliases : string list;
   mutable locals : (string * T.t) list list;
   mutable ret : T.t; (* 현재 함수의 선언된 반환 타입 *)
   (* 현재 본문이 수행한 effect. 위치를 같이 들고 다녀야 "어디서 수행했는지"를
@@ -71,15 +74,16 @@ let conv_eff_result (atoms : Ast.eff_result) : T.eff =
 
 let rec conv env (gen : string list) (t : Ast.ty) : T.t =
   match t with
-  | T_named { name; args; _ } -> (
+  | T_named { modl; name; args; _ } -> (
       let args =
         List.filter_map
           (function TA_ty t -> Some (conv env gen t) | TA_eff _ -> None)
           args
       in
-      if List.mem name gen then T.TVar name
+      let name = match modl with Some a -> a ^ "." ^ name | None -> name in
+      if modl = None && List.mem name gen then T.TVar name
       else
-        match name with
+        match if modl = None then name else "" with
         | "Int" -> T.TInt
         | "Bool" -> T.TBool
         | "String" -> T.TString
@@ -491,33 +495,59 @@ and infer_field env obj name pos =
         (Printf.sprintf
            "capability %s의 메서드는 값을 통해서만 부를 수 있습니다 (%s를 파라미터로 받아야 합니다)" n n)
   | _ -> ());
-  let t = infer env obj in
-  match T.resolve t with
-  | T.TUnknown -> T.TUnknown
-  | T.TCon (cname, args) -> (
-      match Hashtbl.find_opt env.structs cname with
-      | Some (gen, fields) -> (
-          let sub = List.map2 (fun v a -> (v, a)) gen (adjust gen args) in
-          match List.assoc_opt name fields with
-          | Some ft -> T.subst sub [] ft
-          | None ->
-              err env pos (Printf.sprintf "%s에 %s 필드가 없습니다" cname name);
-              T.TUnknown)
+  match obj with
+  | E_ident (a, _) when lookup env a = None && List.mem a env.aliases -> (
+      (* 모듈 별칭을 통한 접근. 가져온 표면은 "Alias.name" 키로 들어와 있다. *)
+      let key = a ^ "." ^ name in
+      let unknown () =
+        err env pos (Printf.sprintf "%s에 %s이(가) 없습니다" a name);
+        T.TUnknown
+      in
+      match Hashtbl.find_opt env.consts key with
+      | Some t -> t
       | None -> (
-          match Hashtbl.find_opt env.caps cname with
-          | Some methods -> (
-              match List.assoc_opt name methods with
-              | Some s ->
-                  let params, eff, ret = instantiate s in
-                  T.TFn { affine = false; params; eff; ret }
+          match Hashtbl.find_opt env.fns key with
+          | Some s ->
+              let params, eff, ret = instantiate s in
+              T.TFn { affine = false; params; eff; ret }
+          | None -> (
+              match Hashtbl.find_opt env.ctors key with
+              | Some enum -> (
+                  match Hashtbl.find_opt env.enums enum with
+                  | Some (_, variants)
+                    when List.assoc_opt key variants = Some [] ->
+                      nullary_ctor env enum key
+                  | Some _ -> ctor_fn env enum key
+                  | None -> T.TUnknown)
+              | None -> unknown ())))
+  | _ -> (
+      let t = infer env obj in
+      match T.resolve t with
+      | T.TUnknown -> T.TUnknown
+      | T.TCon (cname, args) -> (
+          match Hashtbl.find_opt env.structs cname with
+          | Some (gen, fields) -> (
+              let sub = List.map2 (fun v a -> (v, a)) gen (adjust gen args) in
+              match List.assoc_opt name fields with
+              | Some ft -> T.subst sub [] ft
               | None ->
-                  err env pos
-                    (Printf.sprintf "capability %s에 %s 메서드가 없습니다" cname name);
+                  err env pos (Printf.sprintf "%s에 %s 필드가 없습니다" cname name);
                   T.TUnknown)
-          | None -> T.TUnknown))
-  | other ->
-      err env pos (Printf.sprintf "%s에는 필드가 없습니다" (T.show other));
-      T.TUnknown
+          | None -> (
+              match Hashtbl.find_opt env.caps cname with
+              | Some methods -> (
+                  match List.assoc_opt name methods with
+                  | Some s ->
+                      let params, eff, ret = instantiate s in
+                      T.TFn { affine = false; params; eff; ret }
+                  | None ->
+                      err env pos
+                        (Printf.sprintf "capability %s에 %s 메서드가 없습니다" cname name);
+                      T.TUnknown)
+              | None -> T.TUnknown))
+      | other ->
+          err env pos (Printf.sprintf "%s에는 필드가 없습니다" (T.show other));
+          T.TUnknown)
 
 and adjust gen args =
   let n = List.length gen in
@@ -567,7 +597,8 @@ and check_pattern env (scrutinee : T.t) (p : pattern) =
       | Some enum ->
           check_ctor env scrutinee enum n [] Token.{ line = 0; col = 0 }
       | None -> bind env n scrutinee)
-  | P_ctor { name; args; pos } -> (
+  | P_ctor { modl; name; args; pos } -> (
+      let name = match modl with Some a -> a ^ "." ^ name | None -> name in
       match Hashtbl.find_opt env.ctors name with
       | Some enum -> check_ctor env scrutinee enum name args pos
       | None -> List.iter (check_pattern env T.TUnknown) args)
@@ -671,7 +702,7 @@ let check_fn env (d : fn_decl) =
       env.performed <- [];
       pop env
 
-let check (m : modul) : error list =
+let check ?(imports : item list = []) (m : modul) : error list =
   let env =
     {
       structs = Hashtbl.create 16;
@@ -680,6 +711,27 @@ let check (m : modul) : error list =
       fns = Hashtbl.create 16;
       consts = Hashtbl.create 16;
       ctors = Hashtbl.create 16;
+      (* 표면을 실제로 받아온 별칭만 안다. 해소되지 않은 모듈(예: 아직 가져오지
+         못한 패키지)의 별칭은 모르는 것이므로 그 아래 이름을 틀렸다고 말하지
+         않는다. *)
+      aliases =
+        List.sort_uniq compare
+          (List.filter_map
+             (fun it ->
+               let n =
+                 match it with
+                 | I_fn { decl; _ } -> decl.fn_name
+                 | I_struct { name; _ }
+                 | I_enum { name; _ }
+                 | I_capability { name; _ }
+                 | I_const { name; _ } ->
+                     name
+                 | _ -> ""
+               in
+               match String.index_opt n '.' with
+               | Some i -> Some (String.sub n 0 i)
+               | None -> None)
+             imports);
       locals = [];
       ret = T.TUnit;
       performed = [];
@@ -698,7 +750,7 @@ let check (m : modul) : error list =
           List.iter (fun v -> Hashtbl.replace env.ctors v.v_name name) variants
       | I_capability { name; _ } -> Hashtbl.replace env.caps name []
       | _ -> ())
-    m.items;
+    (imports @ m.items);
   (* 2차: 본문을 채운다 *)
   List.iter
     (fun it ->
@@ -722,7 +774,7 @@ let check (m : modul) : error list =
       | I_const { name; ty; _ } ->
           Hashtbl.replace env.consts name (conv env [] ty)
       | _ -> ())
-    m.items;
+    (imports @ m.items);
   (* 3차: 본문 검사 *)
   List.iter
     (fun it ->
diff --git a/samples/modules/area.cool b/samples/modules/area.cool
new file mode 100644
index 0000000..002312a
--- /dev/null
+++ b/samples/modules/area.cool
@@ -0,0 +1,13 @@
+// 모듈 B. A의 표면에만 의존한다.
+//
+// Shape의 variant가 늘면 이 match가 깨진다 — 그래서 enum 정의 본문이
+// interface hash 입력이고, A의 시그니처 변경은 여기까지 전파되어야 한다.
+
+import "shapes" as Shapes
+
+pub fn area(s: Shapes.Shape) -> Int {
+    match s {
+        Shapes.Circle(r) => Shapes.double(r),
+        Shapes.Square(w) => w * w,
+    }
+}
diff --git a/samples/modules/shapes.cool b/samples/modules/shapes.cool
new file mode 100644
index 0000000..19dbaa7
--- /dev/null
+++ b/samples/modules/shapes.cool
@@ -0,0 +1,11 @@
+// 모듈 A. downstream이 보는 것은 이 파일의 exported surface뿐이다.
+
+pub enum Shape {
+    Circle(Int),
+    Square(Int),
+}
+
+pub fn double(n: Int) -> Int {
+    // 본문. 이 안을 아무리 고쳐도 interface hash는 변하지 않는다.
+    n + n
+}
diff --git a/test/test_coollang.ml b/test/test_coollang.ml
index f77e8fd..cd0efc7 100644
--- a/test/test_coollang.ml
+++ b/test/test_coollang.ml
@@ -913,3 +913,76 @@ let () =
   in
   check "variant 둘일 때는 통과" (type_ok (two ^ user));
   check "variant가 늘면 같은 코드가 깨진다" (type_has (three ^ user) "빠진 경우: C")
+
+(* ------------------------------------------------------------------ *)
+(* 모듈 경계와 incremental 전파                                        *)
+(*                                                                     *)
+(* 이 세 검사가 아키텍처 주장 전체다:                                  *)
+(*   1. 다른 모듈의 타입과 생성자가 별칭으로 보인다                    *)
+(*   2. 본문만 고치면 downstream은 재검사되지 않는다                   *)
+(*   3. 시그니처를 고치면 downstream까지 전파되고, 실제로 깨진다       *)
+(* ------------------------------------------------------------------ *)
+
+let has_sub hay needle =
+  let n = String.length needle and h = String.length hay in
+  let rec go i = i + n <= h && (String.sub hay i n = needle || go (i + 1)) in
+  n = 0 || go 0
+
+let write file s =
+  let oc = open_out_bin file in
+  output_string oc s;
+  close_out oc
+
+let () =
+  let dir = Filename.concat (Filename.get_temp_dir_name ()) "cool_modtest" in
+  ignore (Sys.command (Printf.sprintf "mkdir -p %s" (Filename.quote dir)));
+  let a = Filename.concat dir "shapes.cool" in
+  let b = Filename.concat dir "area.cool" in
+  let shapes_body body =
+    "pub enum Shape {\n\
+    \  Circle(Int),\n\
+    \  Square(Int),\n\
+     }\n\n\
+     pub fn double(n: Int) -> Int {\n\
+    \  " ^ body ^ "\n}\n"
+  in
+  let shapes_three =
+    "pub enum Shape {\n\
+    \  Circle(Int),\n\
+    \  Square(Int),\n\
+    \  Tri(Int),\n\
+     }\n\n\
+     pub fn double(n: Int) -> Int {\n\
+    \  n + n\n\
+     }\n"
+  in
+  let area =
+    "import \"shapes\" as Shapes\n\n\
+     pub fn area(s: Shapes.Shape) -> Int {\n\
+    \  match s {\n\
+    \    Shapes.Circle(r) => Shapes.double(r),\n\
+    \    Shapes.Square(w) => w * w,\n\
+    \  }\n\
+     }\n"
+  in
+  write a (shapes_body "n + n");
+  write b area;
+  let st = Session.create ~root:dir () in
+  Session.load st b;
+  check "모듈 경계를 넘는 타입과 생성자가 보인다" (Session.errors st = []);
+
+  (* 본문만 수정 — hash가 그대로이므로 downstream은 손대지 않는다 *)
+  write a (shapes_body "n * 2");
+  let touched = Session.recheck st [ a ] in
+  check "본문만 고치면 자기 자신만 재검사된다" (touched = [ a ]);
+  check "본문 수정 후에도 오류 없음" (Session.errors st = []);
+
+  (* 시그니처 수정 — hash가 변하므로 dependents까지 전파된다 *)
+  write a shapes_three;
+  let touched = Session.recheck st [ a ] in
+  check "variant를 추가하면 downstream까지 전파된다" (List.mem b touched);
+  check "전파된 downstream이 실제로 깨진다"
+    (List.exists
+       (fun (e : Session.error) ->
+         e.file = b && String.length e.message > 0 && has_sub e.message "빠진 경우")
+       (Session.errors st))