docs: README

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E

README.md

@@ -0,0 +1,111 @@
+# coollang
+
+되돌리기 비싼 결정부터 확정하는 프로그래밍 언어. 현재 v0 — 설계 검증판.
+
+```
+$ coolc check samples/run/hello.cool
+$ coolc run   samples/run/hello.cool
+area = 12
+area = 9
+area = 3
+```
+
+## 무엇을 위한 언어인가
+
+세 가지 목표가 나머지 모든 결정을 지배한다.
+
+1. **오류를 더 빨리 잡는다** — null 없음, Option/Result, 소진적 match,
+   확정 초기화, 선언되지 않은 effect는 컴파일 오류.
+2. **검증이 더 빠르다** — fast path / slow path 분리, 전역 추론 없음,
+   복잡한 trait solver 없음, 임의 매크로 없음, 인터페이스 해시 기반 무효화.
+3. **피해 범위가 좁다** — 명시적 capability, ambient authority 없음,
+   affine 소유권.
+
+설계의 전문은 [`docs/thesis.md`](docs/thesis.md), 문법은
+[`docs/grammar.ebnf`](docs/grammar.ebnf)에 있다.
+
+## 지금 되는 것
+
+`lex → parse → 이름 해소 → 타입 검사 → effect/capability 검사 →
+move/affinity 검사 → 소진성 검사 → interface 해시 → typed IR → 인터프리터`
+
+여섯 종류의 오류를 한국어 진단으로 보고한다: 문법, 이름, 타입, effect,
+capability, 소유권. 여기에 match 소진성과 두 가지 lint(미사용 import,
+effect 과잉 선언)가 더해진다.
+
+```
+$ coolc check samples/12_stdlib_effects.cool
+samples/12_stdlib_effects.cool:20:14: 선언되지 않은 effect Console.print
+  (leaks_effect의 effects 절은 {}입니다)
+```
+
+## 증분 검사
+
+이 프로젝트의 중심 주장이다. 10만 줄 / 200 모듈에서 측정 (`bench/bench.ml`):
+
+| | 시간 | 재검사한 모듈 |
+|---|---|---|
+| 전체 검사 (cold) | 253ms | 200 |
+| 함수 **본문**만 수정 | 0.8ms | **1** |
+| 함수 **시그니처** 수정 | 2.5ms | **2** |
+
+핵심은 시간이 아니라 범위다. 본문 수정이 downstream을 한 칸도 건드리지
+않는 것, 그리고 시그니처 수정이 사슬 끝까지 가지 않고 해시가 변한 곳에서
+멈추는 것 — 이 둘이 아키텍처의 주장 전부다.
+
+시그니처 수정 시나리오에서는 두 모듈 건너의 `match`가 실제로 깨진다:
+
+```
+m100.cool:15:3: match가 모든 경우를 덮지 않습니다 (빠진 경우: Tri(_))
+m101.cool:21:3: match가 모든 경우를 덮지 않습니다 (빠진 경우: Up.Tri(_))
+```
+
+## 빌드
+
+OCaml 5.x와 dune이 필요하다.
+
+```
+opam install dune
+dune build
+dune test          # 175개 검사
+dune exec bench/bench.exe
+```
+
+`coolc`는 `_build/default/bin/main.exe`다. 설치하려면 `dune install`.
+
+## 저장소 구성
+
+```
+lib/          컴파일러 (약 4,900줄 OCaml)
+  lexer.ml      어휘 분석 — 문법을 하나도 모른다
+  parser.ml     재귀 하강, LL(1), backtracking 없음
+  resolve.ml    이름 해소 — 모듈 하나만 보고 결정할 수 있는 것
+  typecheck.ml  타입 + effect + capability
+  move.ml       move / affinity
+  exhaust.ml    소진성 (Maranget usefulness)
+  iface.ml      interface artifact + 해시
+  session.ml    모듈 로딩 + 고정점 invalidation
+  ir.ml         얇은 typed IR
+  interp.ml     트리 워킹 인터프리터
+std/          표준 라이브러리 (본문 없는 선언, 런타임이 구현)
+samples/      예제 — 통과용 9개, 일부러 틀린 것 7개
+bench/        증분 루프 측정
+```
+
+## v0의 성격
+
+이것은 쓸 수 있는 언어가 아니라 **설계가 옳은지 증명된 언어**다.
+되돌리기 비싼 결정 — 문법, 타입, effect, capability, 소유권, 증분
+아키텍처 — 이 전부 코드와 테스트로 못 박혔고, 빠른 검증 루프라는 시스템
+속성이 측정으로 증명됐다.
+
+그래서 이 코드를 통째로 버리고 v1로 번역해도 잃을 것이 없다. 애초에
+그것이 v0의 목적이었다.
+
+아직 없는 것: 진짜 컴파일(해석 실행만 한다), 병렬 실행(`scope`는 순차),
+파일·네트워크 IO, 완전한 제네릭, 에디터 지원, 패키지 관리자. 표준
+라이브러리는 `len`, `each`, `map`, `concat`, `show` 수준이다.
+
+## 이름
+
+언어는 coollang, 툴체인 바이너리는 `coolc`. 소스 확장자는 `.cool`.

bench/bench.ml

@@ -0,0 +1,128 @@
+(* 빠른 검증 루프는 주장이 아니라 측정이다.
+
+   측정하는 것은 두 가지다:
+     1. 전체 검사 시간 (cold) — 규모가 커져도 파국이 아닌가
+     2. 증분 재검사 시간 (warm) — 그리고 무엇이 재검사되었는가
+
+   두 번째가 본체다. 아키텍처의 주장은 "빠르다"가 아니라 "다시 볼 것이
+   적다"이고, 그것은 시간이 아니라 재검사된 모듈 수로 먼저 증명된다.
+   시간은 그 수가 옳다는 것의 따름 결과다. *)
+
+open Coollang
+
+let modules = 200
+let fns_per_module = 68
+let now () = Unix.gettimeofday ()
+
+let find_sub hay needle =
+  let n = String.length needle and h = String.length hay in
+  let rec go i =
+    if i + n > h then failwith "not found"
+    else if String.sub hay i n = needle then i
+    else go (i + 1)
+  in
+  go 0
+
+let write file s =
+  let oc = open_out_bin file in
+  output_string oc s;
+  close_out oc
+
+(* i번 모듈은 i-1번 모듈을 가져온다. 사슬이므로 시그니처 변경은 끝까지
+   전파되어야 하고, 본문 변경은 한 칸도 가면 안 된다. *)
+let gen_module i ~body =
+  let b = Buffer.create 8192 in
+  if i > 0 then
+    Buffer.add_string b (Printf.sprintf "import \"m%d\" as Up\n\n" (i - 1));
+  Buffer.add_string b "pub enum Shape {\n  Circle(Int),\n  Square(Int),\n}\n\n";
+  Buffer.add_string b "pub copyable struct Point {\n  x: Int,\n  y: Int,\n}\n\n";
+  Buffer.add_string b
+    (Printf.sprintf
+       "pub fn area(s: Shape) -> Int {\n\
+       \  match s {\n\
+       \    Circle(r) => r * r,\n\
+       \    Square(w) => w * w,\n\
+       \  }\n\
+        }\n\n");
+  if i > 0 then
+    Buffer.add_string b
+      "pub fn up_area(s: Up.Shape) -> Int {\n\
+      \  match s {\n\
+      \    Up.Circle(r) => Up.area(s),\n\
+      \    Up.Square(w) => w * w,\n\
+      \  }\n\
+       }\n\n";
+  for k = 0 to fns_per_module - 1 do
+    Buffer.add_string b
+      (Printf.sprintf
+         "pub fn f%d(p: Point, n: Int) -> Int {\n\
+         \  let a = p.x + n\n\
+         \  let b = p.y * %d\n\
+         \  let c = if a > b { a } else { b }\n\
+         \  %s\n\
+          }\n\n"
+         k (k + 1) body)
+  done;
+  Buffer.contents b
+
+let count_lines s =
+  String.fold_left (fun n c -> if c = '\n' then n + 1 else n) 0 s
+
+let ms t = Printf.sprintf "%.1fms" (t *. 1000.)
+
+let () =
+  let dir = Filename.concat (Filename.get_temp_dir_name ()) "cool_bench" in
+  ignore
+    (Sys.command
+       (Printf.sprintf "rm -rf %s && mkdir -p %s" (Filename.quote dir)
+          (Filename.quote dir)));
+  let path i = Filename.concat dir (Printf.sprintf "m%d.cool" i) in
+  let lines = ref 0 in
+  for i = 0 to modules - 1 do
+    let s = gen_module i ~body:"a + c" in
+    lines := !lines + count_lines s;
+    write (path i) s
+  done;
+  Printf.printf "모듈 %d개, %d줄 생성\n" modules !lines;
+
+  (* 1. cold: 전체 그래프 로드와 검사 *)
+  let st = Session.create ~root:dir () in
+  let t0 = now () in
+  Session.load st (path (modules - 1));
+  let cold = now () -. t0 in
+  let errs = Session.errors st in
+  Printf.printf "cold  전체 검사      %s  (오류 %d건)\n" (ms cold) (List.length errs);
+  if errs <> [] then
+    List.iter
+      (fun e -> prerr_endline (Session.string_of_error e))
+      (List.filteri (fun i _ -> i < 5) errs);
+
+  (* 2. warm: 사슬 한가운데 모듈의 본문만 수정 *)
+  let mid = modules / 2 in
+  write (path mid) (gen_module mid ~body:"a + c + 1");
+  let t0 = now () in
+  let touched = Session.recheck st [ path mid ] in
+  let warm_body = now () -. t0 in
+  Printf.printf "warm  본문만 수정    %s  (재검사 %d개, 오류 %d건)\n" (ms warm_body)
+    (List.length touched)
+    (List.length (Session.errors st));
+
+  (* 3. warm: 같은 모듈의 시그니처 수정 — variant 추가 *)
+  let sig_src =
+    let s = gen_module mid ~body:"a + c + 1" in
+    let needle = "  Square(Int),\n" in
+    let i = find_sub s needle in
+    String.sub s 0 (i + String.length needle)
+    ^ "  Tri(Int),\n"
+    ^ String.sub s
+        (i + String.length needle)
+        (String.length s - i - String.length needle)
+  in
+  write (path mid) sig_src;
+  let t0 = now () in
+  let touched = Session.recheck st [ path mid ] in
+  let warm_sig = now () -. t0 in
+  let errs = Session.errors st in
+  Printf.printf "warm  시그니처 수정  %s  (재검사 %d개, 오류 %d건)\n" (ms warm_sig)
+    (List.length touched) (List.length errs);
+  List.iter (fun e -> print_endline ("      " ^ Session.string_of_error e)) errs

bench/dune

@@ -0,0 +1,3 @@
+(executable
+ (name bench)
+ (libraries coollang unix))

bin/dune

@@ -1,4 +1,4 @@
 (executable
  (name main)
- (public_name cool)
+ (public_name coolc)
  (libraries coollang))

bin/main.ml

@@ -2,12 +2,13 @@ let usage =
   {|coollang toolchain
 
 사용법:
-  cool check <file.cool>...   타입/effect/capability 검사 (fast path)
+  coolc check <file.cool>...   타입/effect/capability 검사 (import를 따라 모듈 그래프 전체)
-  cool run <file.cool>        typed IR 인터프리터로 실행
+  coolc iface <file.cool>      interface 표면과 해시 출력
-  cool tokens <file.cool>     토큰 덤프 (렉서 디버깅)
+  coolc run <file.cool>        typed IR 인터프리터로 실행
-  cool ast <file.cool>        구문 트리 덤프 (파서 디버깅)
+  coolc tokens <file.cool>     토큰 덤프 (렉서 디버깅)
-  cool deps <file.cool>       외부 참조 목록 (모듈의 의존 표면)
+  coolc ast <file.cool>        구문 트리 덤프 (파서 디버깅)
-  cool version                버전 출력
+  coolc deps <file.cool>       외부 참조 목록 (모듈의 의존 표면)
+  coolc version                버전 출력
 |}
 
 let report_errors errors =
@@ -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,8 +74,17 @@ 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
-    | [ "run"; file ] -> report (Coollang.Driver.run file)
+    | [ "iface"; file ] -> dump_iface file
+    | [ "run"; file ] -> (
+        let st = Coollang.Session.create ~root:(Filename.dirname file) () in
+        match Coollang.Session.run st file with
+        | Ok out ->
+            print_string out;
+            0
+        | Error e ->
+            prerr_endline (Coollang.Session.string_of_error e);
+            1)
     | [ "tokens"; file ] -> dump_tokens file
     | [ "ast"; file ] -> dump_ast file
     | [ "deps"; file ] -> dump_deps file

docs/thesis.md

@@ -8,6 +8,11 @@ AI의 코드 생성 속도 >> 신뢰 확보 속도.
 1. 오류는 더 일찍: 컴파일 타임으로 최대한 끌어당김
    → null 없음(Option), Result, exhaustive matching, definite init,
      미선언 effect = compile error
+   ※ definite init은 문법이 이미 보장한다: let은 항상 초기화식을 요구하고
+     미초기화 바인딩을 쓸 방법이 없다. 별도 검사가 필요 없는 것이 맞다
+   ※ exhaustive matching은 interface hash가 enum 정의 본문을 입력으로 삼는
+     이유이기도 하다. upstream에 variant가 하나 늘면 downstream의 match가
+     깨져야 하는데, 이 검사가 없으면 깨질 것이 없다
 2. 검증은 더 빨리: 검증 속도가 언어 설계의 헌법
    → fast path(check) / slow path(release, deep verify) 분리
    → 컴파일을 느리게/비결정적으로 만드는 기능 원천 배제
@@ -45,6 +50,13 @@ Alias/Move 모델 (철학 1,3에서 파생 — 언어 전체의 토대):
   미해제는 검사하지 않는다 (오용 금지, 누수 허용).
   linear 검사와 해제 보장은 v1 과제
 - v0에 first-class reference는 없다. mutable 데이터는 소유 변수를 통해서만 변경
+- 클로저는 mut 바인딩을 capture할 수 없다. 참조가 없으므로 별칭을 만들 수도,
+  조용히 복사할 수도 없기 때문이다. spawn 클로저 제한은 이 일반 규칙의 특수 사례다
+- v0에 부분 move는 없다. 필드 접근은 빌림이고 결과도 빌린 값이다
+  ※ struct에서 affine 필드만 꺼내 가려면 부분 move 상태 추적이 필요한데,
+     그 복잡도는 v0가 사려는 것이 아니다. 필요하면 통째로 own으로 받는다
+- 외부 타입은 affine임을 증명할 수 없으므로 copyable로 본다.
+  모르는 것을 위반이라고 말하지 않는다 — 모듈 로딩이 생기면 판정된다
 - 공유는 deep immutable 값만 가능 (내부 가변성 타입은 v0에 없음)
 근거: "safe code에 data race 없음"은 spawn만 막아서 성립하지 않는다. closure,
 channel, container, 인자/반환 전 경로에서 mutable alias가 없어야 하며, 값 의미론
@@ -107,8 +119,8 @@ Affinity 전이 (보안 주장의 필수 전제):
 - structured concurrency만 허용: 태스크 수명 = 블록 구조 (locality)
 - 데이터 경쟁은 격리로: mutable은 단일 소유, channel로 소유권 이동,
   공유는 deep immutable만 (borrow checker는 complexity budget 초과)
-- spawn closure는 by-move capture 또는 immutable capture만 허용.
+- spawn closure는 by-move capture 또는 immutable capture만 허용
-  mutable 참조 capture는 문법적으로 금지
+  (Alias/Move 모델의 mut capture 금지가 그대로 적용된다)
 - spawn은 primitive가 아니라 TaskScope capability의 메서드다.
   effect spawn은 아래 "정적/동적 층 분리"대로 그 타입에 묶인다
   (PaymentGateway.refund와 동형)
@@ -268,12 +280,23 @@ Generics (철학 2에서 파생):
   ※ 각 단계는 그 단계가 소유한 성질만 판정한다. 예: affinity는 타입 동등성이
      아니라 substructural 성질이므로 타입 검사가 아니라 move 검사가 소유한다.
      단계가 서로의 결론을 앞지르면 진단이 엉뚱한 곳에서 난다
+  ※ 다만 effect 검사는 타입 검사와 같은 순회에서 돈다. effect 변수의 해소가
+     타입 변수와 같은 지점(호출 지점의 지역 unification)에서 일어나므로,
+     떼어내면 순회와 인스턴스화를 두 번 하게 된다. 소유는 나뉘되 순회는 하나다
+  ※ v0는 과잉 선언(선언했으나 수행하지 않는 effect)을 오류로 보지 않는다.
+     외부 모듈의 effect를 모르는 상태에서는 판정할 수 없기 때문이다.
+     모듈 로딩이 생기면 lint 대상이다
 - move/affinity 검사, capability use 규칙, affinity 전이
 - effect 변수 (effect 다형성)
 - interface artifact + hash 기반 incremental invalidation
-- cool check
+- coolc check
-- 얇은 typed IR + tree-walking interpreter (cool run 대용)
+- 얇은 typed IR + tree-walking interpreter (coolc run)
   ※ IR을 미루면 non-IR 전제가 스며들어 재작성 됨. 지금, 얇게.
+  ※ 실행 시점에도 권한의 출처는 런타임 하나다. main이 선언한 capability만
+     넘어가고, 소스에는 capability를 만드는 문법이 없다 — 보안 정리 (i)의
+     실행 시점 대응물. TaskScope의 뿌리도 같은 이유로 런타임이 준다.
+  ※ v0의 scope 실행 의미는 순차다. 구조가 먼저고 병렬성은 그 위의 최적화다 —
+     순서가 반대면 취소와 전파를 나중에 끼워 넣게 된다.
   ※ effect check가 fast path 예산 안에 드는지가 사활 → 최우선 검증 대상
 
 제외 (아키텍처 검증 후 얹어도 되는 것):
@@ -314,3 +337,42 @@ L2 빠른 테스트 / L3 fuzzing / L4 formal proof → 요청 시, 분리 실행
 오류를 더 빨리 잡는가? / 컴파일 복잡도·시간은 예측 가능한가? /
 invalidation 범위를 넓히는가? / unrelated code 의미를 바꾸는가? /
 기존 개념의 중복 표현인가? → 강한 이유 없으면 거절
+
+■ lint (오류다, 경고가 아니다)
+- 미사용 import: 쓰지 않는 모듈의 시그니처가 바뀌면 이 모듈이 재검사된다.
+  증분 루프의 비용을 이유 없이 넓히는 선언은 남겨둘 수 없다.
+- effect 과잉 선언: 선언하고 수행하지 않으면 호출자가 하지도 않는 일에
+  의무를 진다. 시그니처는 실제보다 좁아도 안 되고 넓어도 안 된다.
+  단, effect 변수가 있거나 본문에 모르는 이름이 있으면 판정하지 않는다 —
+  무엇이 묶일지는 호출 지점이 정하고, 외부 타입의 메서드는 effect를 모른다.
+lint는 blocking이 아니다. 이름 해소 실패는 뒤 단계를 막지만 lint는 막지
+않는다 — lint 하나가 진짜 타입 오류를 가리면 루프가 느려진다.
+
+■ 파서 오류 복구
+항목 단위로만 회복한다. 오류가 난 선언은 통째로 버리고 다음 선언에서
+다시 시작한다. 문 단위로 더 잘게 회복하려 하면 파서가 추측을 하게 되고,
+틀린 추측은 없는 오류를 지어낸다. 한 항목에 오류 하나가 상한이라는 것은
+정직한 한계이지 숨길 것이 아니다.
+동기화 지점: 중괄호 깊이 0 + 줄 첫머리 + 선언 시작 토큰. 셋 다 필요하다.
+
+■ 표준 라이브러리 (std/)
+본문 없는 선언 파일이다. 런타임이 구현하고 .cool 파일은 계약만 말한다.
+구현이 아니라 시험대인 것이 요점 — effect 다형성이 실제로 쓸 만한지가
+List.each와 List.map에서 결정된다. 규칙이 틀렸으면 여기서 드러난다.
+prelude는 없다. std도 명시적으로 가져온다 — 암묵적으로 끌어오지 않는다는
+규칙에 예외를 두지 않는다.
+※ std를 넣자마자 샘플 01이 깨졌다. List.each에 Result를 반환하는 클로저를
+   넘기고 그 안에서 ?를 쓰고 있었다. 검사되지 않던 코드가 검사되기 시작한
+   것이고, 이것이 std를 "부채 상환"이 아니라 "검증"으로 본 이유다.
+   결과를 버릴 방법이 언어에 없다는 성질도 여기서 처음 확인됐다.
+
+■ 측정 (2026-08, v0 fast path)
+100,391줄 / 200 모듈 (사슬 의존). bench/bench.ml로 재현.
+  cold 전체 검사      245ms
+  본문만 수정         0.8ms, 재검사 1개 모듈
+  시그니처 수정       2.1ms, 재검사 2개 모듈 (+ downstream 소진성 위반 검출)
+증분 루프의 비용은 시간이 아니라 재검사 범위가 결정한다. 본문 수정이
+downstream을 한 칸도 건드리지 않는 것이 이 아키텍처의 주장이고, 위 수치의
+"재검사 1개"가 그 주장이다. 시그니처 수정이 사슬 끝까지 가지 않고 2개에서
+멈추는 것도 같은 규칙의 결과다 — m101의 interface는 변하지 않으므로 m102는
+다시 볼 이유가 없다.

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 ->

lib/driver.ml

@@ -1,8 +1,10 @@
 (* v0 파이프라인.
    parse -> name resolution -> type check -> effect/capability check
-   -> interface artifact + hash -> (cool run 시) 얇은 typed IR -> interpreter
+   -> interface artifact + hash -> (coolc run 시) 얇은 typed IR -> interpreter
 
-   현재 구현된 단계: 어휘 분석, 구문 분석. *)
+   이 파일은 단일 파일 도구(tokens/ast/deps)만 남았다. 모듈 그래프를 다루는
+   check와 run은 Session이 소유한다 — import를 따라가야 하는 순간부터
+   "파일 하나"는 더 이상 단위가 아니다. *)
 
 type error = { file : string; line : int; col : int; message : string }
 
@@ -69,19 +71,27 @@ let typecheck (file : string) : (unit, error list) result =
                  { file; line = e.pos.line; col = e.pos.col; message = e.msg })
                rerrors)
       | [] -> (
-          match Typecheck.check m with
+          let terrors =
+            List.map
+              (fun (e : Typecheck.error) ->
+                { file; line = e.pos.line; col = e.pos.col; message = e.msg })
+              (Typecheck.check m)
+          in
+          (* move/affinity는 타입·effect와 달리 별도 순회다. 소유하는 성질이
+             다르고 해소를 공유할 지점도 없기 때문이다. *)
+          let merrors =
+            List.map
+              (fun (e : Move.error) ->
+                { file; line = e.pos.line; col = e.pos.col; message = e.msg })
+              (Move.check m)
+          in
+          match
+            List.sort
+              (fun a b -> compare (a.line, a.col) (b.line, b.col))
+              (terrors @ merrors)
+          with
           | [] -> Ok ()
-          | terrors ->
+          | errors -> Error errors))
-              Error
-                (List.map
-                   (fun (e : Typecheck.error) ->
-                     {
-                       file;
-                       line = e.pos.line;
-                       col = e.pos.col;
-                       message = e.msg;
-                     })
-                   terrors)))
 
 let check (files : string list) : (unit, error list) result =
   match files with
@@ -94,21 +104,4 @@ let check (files : string list) : (unit, error list) result =
           files
         |> List.concat
       in
-      if errors <> [] then Error errors
+      if errors <> [] then Error errors else Ok ()
-      else
-        (* 타입 검사는 통과했다. 통과했다고 말하지 않는다 — 파이프라인의
-           나머지가 아직 없으므로 검사되지 않은 것이다. *)
-        Error
-          (List.map
-             (fun f ->
-               {
-                 file = f;
-                 line = 0;
-                 col = 0;
-                 message =
-                   "타입 검사까지 통과. effect/capability 검사와 move 검사가 아직 구현되지 않았습니다";
-               })
-             files)
-
-let run (file : string) : (unit, error list) result =
-  Error [ { file; line = 0; col = 0; message = "interpreter가 아직 구현되지 않았습니다" } ]

lib/exhaust.ml

@@ -0,0 +1,203 @@
+(* match exhaustiveness와 도달 불가 팔 검사 (Maranget의 usefulness 알고리즘).
+
+   철학 1의 대표 항목이다. 그리고 interface hash가 enum 정의 본문을 입력으로
+   삼는 이유이기도 하다 — upstream에 variant가 하나 늘면 downstream의 match가
+   깨져야 하는데, 이 검사가 없으면 깨질 것이 없다.
+
+   생성자 집합을 알 수 없는 타입(외부 타입, 미지수)은 검사하지 않는다.
+   모르는 것을 위반이라고 말하지 않는다. *)
+
+module T = Types
+
+(* 패턴을 검사용 형태로 줄인다. 바인딩은 와일드카드와 같다 —
+   무엇을 덮는가만 중요하다. *)
+type cpat = CWild | CCtor of string * cpat list
+type ctor = { c_name : string; c_args : T.t list }
+type ctors = Finite of ctor list | Infinite
+
+type env = {
+  (* enum 이름 -> variant 목록. 제네릭은 인스턴스화해서 넘어온다 *)
+  variants : string -> T.t list -> (string * T.t list) list option;
+  is_ctor : string -> bool;
+}
+
+let ctors_of env (t : T.t) : ctors =
+  match T.resolve t with
+  | T.TBool ->
+      Finite
+        [ { c_name = "true"; c_args = [] }; { c_name = "false"; c_args = [] } ]
+  | T.TUnit -> Finite [ { c_name = "unit"; c_args = [] } ]
+  | T.TCon ("Option", [ a ]) ->
+      Finite
+        [
+          { c_name = "Some"; c_args = [ a ] }; { c_name = "None"; c_args = [] };
+        ]
+  | T.TCon ("Result", [ a; b ]) ->
+      Finite
+        [
+          { c_name = "Ok"; c_args = [ a ] }; { c_name = "Err"; c_args = [ b ] };
+        ]
+  | T.TCon (n, args) -> (
+      match env.variants n args with
+      | Some vs ->
+          Finite
+            (List.map (fun (name, tys) -> { c_name = name; c_args = tys }) vs)
+      | None -> Infinite)
+  | _ -> Infinite
+
+let rec of_pattern env (p : Ast.pattern) : cpat =
+  match p with
+  | Ast.P_wild _ -> CWild
+  | Ast.P_lit (Ast.L_bool true, _) -> CCtor ("true", [])
+  | Ast.P_lit (Ast.L_bool false, _) -> CCtor ("false", [])
+  (* 리터럴은 인자 없는 생성자다. 와일드카드로 바꾸면 모든 값을 덮는 것이 되어
+     Int 리터럴 몇 개로 exhaustive가 되어버린다. 타입의 생성자 집합이 무한하므로
+     리터럴만으로는 결코 완전해지지 않는다. *)
+  | 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 { 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
+
+let wilds n = List.init n (fun _ -> CWild)
+
+(* 행렬을 생성자 c로 특수화한다 *)
+let specialize (c : ctor) (matrix : cpat list list) : cpat list list =
+  let arity = List.length c.c_args in
+  List.filter_map
+    (fun row ->
+      match row with
+      | CCtor (n, args) :: rest ->
+          if n = c.c_name then Some (args @ rest) else None
+      | CWild :: rest -> Some (wilds arity @ rest)
+      | [] -> None)
+    matrix
+
+let default_matrix (matrix : cpat list list) : cpat list list =
+  List.filter_map
+    (fun row ->
+      match row with
+      | CCtor _ :: _ -> None
+      | CWild :: rest -> Some rest
+      | [] -> None)
+    matrix
+
+let head_names (matrix : cpat list list) =
+  List.filter_map
+    (fun row -> match row with CCtor (n, _) :: _ -> Some n | _ -> None)
+    matrix
+
+(* 행렬이 덮지 못하는 반례 벡터를 찾는다. None이면 완전하다. *)
+let rec witness env (matrix : cpat list list) (tys : T.t list) :
+    cpat list option =
+  match tys with
+  | [] -> if matrix = [] then Some [] else None
+  | th :: rest -> (
+      let heads = head_names matrix in
+      match ctors_of env th with
+      | Finite cs
+        when List.for_all (fun c -> List.mem c.c_name heads) cs && cs <> [] ->
+          (* 모든 생성자가 나타났다: 각각으로 파고든다 *)
+          let rec try_each = function
+            | [] -> None
+            | c :: more -> (
+                let arity = List.length c.c_args in
+                match witness env (specialize c matrix) (c.c_args @ rest) with
+                | Some ws ->
+                    let args = List.filteri (fun i _ -> i < arity) ws in
+                    let tail = List.filteri (fun i _ -> i >= arity) ws in
+                    Some (CCtor (c.c_name, args) :: tail)
+                | None -> try_each more)
+          in
+          try_each cs
+      | kind -> (
+          (* 빠진 생성자가 있거나 집합이 무한하다 *)
+          match witness env (default_matrix matrix) rest with
+          | None -> None
+          | Some ws ->
+              let head =
+                match kind with
+                | Finite cs -> (
+                    match
+                      List.find_opt (fun c -> not (List.mem c.c_name heads)) cs
+                    with
+                    | Some c -> CCtor (c.c_name, wilds (List.length c.c_args))
+                    | None -> CWild)
+                | Infinite -> CWild
+              in
+              Some (head :: ws)))
+
+let rec show_cpat = function
+  | CWild -> "_"
+  | CCtor (n, []) -> n
+  | CCtor (n, args) ->
+      n ^ "(" ^ String.concat ", " (List.map show_cpat args) ^ ")"
+
+(* 행 q가 행렬 P에 대해 쓸모 있는가 = P가 덮지 못하는 값을 q가 덮는가 *)
+let useful env (matrix : cpat list list) (q : cpat list) (tys : T.t list) : bool
+    =
+  let rec go matrix q tys =
+    match (q, tys) with
+    | [], [] -> matrix = []
+    | qh :: qt, th :: tt -> (
+        match qh with
+        | CCtor (n, args) -> (
+            match ctors_of env th with
+            | Finite cs -> (
+                match List.find_opt (fun c -> c.c_name = n) cs with
+                | Some c -> go (specialize c matrix) (args @ qt) (c.c_args @ tt)
+                | None -> go (default_matrix matrix) qt tt)
+            | Infinite ->
+                let c =
+                  { c_name = n; c_args = List.map (fun _ -> T.TUnknown) args }
+                in
+                go (specialize c matrix) (args @ qt) (c.c_args @ tt))
+        | CWild -> (
+            let heads = head_names matrix in
+            match ctors_of env th with
+            | Finite cs
+              when List.for_all (fun c -> List.mem c.c_name heads) cs
+                   && cs <> [] ->
+                List.exists
+                  (fun c ->
+                    go (specialize c matrix)
+                      (wilds (List.length c.c_args) @ qt)
+                      (c.c_args @ tt))
+                  cs
+            | _ -> go (default_matrix matrix) qt tt))
+    | _ -> false
+  in
+  go matrix q tys
+
+type result = {
+  missing : string option; (* 빠진 경우의 반례 *)
+  unreachable : int list; (* 도달할 수 없는 팔의 번호 (0부터) *)
+}
+
+let check env (scrutinee : T.t) (pats : Ast.pattern list) : result =
+  match ctors_of env scrutinee with
+  | Infinite when T.resolve scrutinee = T.TUnknown ->
+      (* 생성자 집합을 모르면 검사하지 않는다 *)
+      { missing = None; unreachable = [] }
+  | _ ->
+      let rows = List.map (fun p -> [ of_pattern env p ]) pats in
+      let unreachable =
+        let acc = ref [] in
+        List.iteri
+          (fun i row ->
+            let before = List.filteri (fun j _ -> j < i) rows in
+            if not (useful env before row [ scrutinee ]) then acc := i :: !acc)
+          rows;
+        List.rev !acc
+      in
+      let missing =
+        (* 리터럴 패턴이 섞이면 정확한 반례를 만들 수 없다 — 그 열은 무한
+           집합이므로 와일드카드가 없으면 불완전으로 본다 *)
+        match witness env rows [ scrutinee ] with
+        | Some ws -> (
+            match ws with [ w ] -> Some (show_cpat w) | _ -> Some "_")
+        | None -> None
+      in
+      { missing; unreachable }

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

lib/interp.ml

@@ -0,0 +1,342 @@
+(* 트리 워킹 인터프리터.
+
+   여기 도달한 프로그램은 이미 타입, effect, capability, ownership 검사를
+   통과했다. 그러므로 이 파일은 검사하지 않는다 — 검사기가 이미 답한 질문을
+   실행 시점에 다시 묻는 것은 두 번째 진실을 만드는 일이다.
+
+   실행 시점 오류로 남는 것은 검사기가 원리적으로 못 잡는 것뿐이다:
+   0으로 나누기, 리스트 범위, 그리고 아직 없는 표준 라이브러리 이름.
+
+   권한의 유일한 출처는 런타임이다. 소스에는 capability를 만드는 문법이 없고,
+   main은 자기가 선언한 capability만 받는다. 선언하지 않은 권한은 프로그램
+   어디에도 존재하지 않는다 — 보안 정리 (i)의 실행 시점 대응물이다. *)
+
+type value =
+  | VUnit
+  | VInt of int
+  | VBool of bool
+  | VStr of string
+  | VList of value list
+  | VStruct of string * (string * value ref) list
+  | VEnum of string * string * value list (* enum, variant, 인자 *)
+  | VClosure of { params : string list; body : Ir.t; env : env }
+  | VFn of Ir.fn
+  | VCtor of string * string * int (* 아직 인자를 안 받은 생성자 *)
+  | VBuiltin of string
+  | VNative of (value list -> value)
+  | VCap of string * (string * (value list -> value)) list
+  | VScope of string
+
+and env = (string * value ref) list list
+
+exception Return_exc of value
+exception Fail of Token.pos * string
+
+let fail pos msg = raise (Fail (pos, msg))
+
+let rec show = function
+  | VUnit -> "unit"
+  | VInt n -> string_of_int n
+  | VBool b -> if b then "true" else "false"
+  | VStr s -> s
+  | VList xs -> "[" ^ String.concat ", " (List.map show xs) ^ "]"
+  | VStruct (n, fs) ->
+      n ^ "{"
+      ^ String.concat ", " (List.map (fun (k, v) -> k ^ ": " ^ show !v) fs)
+      ^ "}"
+  | VEnum (_, v, []) -> v
+  | VEnum (_, v, args) ->
+      v ^ "(" ^ String.concat ", " (List.map show args) ^ ")"
+  | VClosure _ | VFn _ | VBuiltin _ | VCtor _ | VNative _ -> "<fn>"
+  | VCap (n, _) -> "<capability " ^ n ^ ">"
+  | VScope n -> "<scope " ^ n ^ ">"
+
+let rec eq a b =
+  match (a, b) with
+  | VInt x, VInt y -> x = y
+  | VBool x, VBool y -> x = y
+  | VStr x, VStr y -> x = y
+  | VUnit, VUnit -> true
+  | VList x, VList y -> List.length x = List.length y && List.for_all2 eq x y
+  | VEnum (_, v1, a1), VEnum (_, v2, a2) ->
+      v1 = v2 && List.length a1 = List.length a2 && List.for_all2 eq a1 a2
+  | _ -> false
+
+(* ------------------------------------------------------------------ *)
+(* 환경                                                                *)
+(* ------------------------------------------------------------------ *)
+
+let lookup (env : env) n =
+  let rec go = function
+    | [] -> None
+    | s :: r -> (
+        match List.assoc_opt n s with Some v -> Some v | None -> go r)
+  in
+  go env
+
+let bind (env : env) n v : env =
+  match env with s :: r -> ((n, ref v) :: s) :: r | [] -> [ [ (n, ref v) ] ]
+
+(* ------------------------------------------------------------------ *)
+(* 런타임이 제공하는 것                                                *)
+(* ------------------------------------------------------------------ *)
+
+let out = Buffer.create 1024
+
+let root_capability name : value option =
+  match name with
+  | "Console" ->
+      Some
+        (VCap
+           ( "Console",
+             [
+               ( "print",
+                 fun args ->
+                   List.iter (fun v -> Buffer.add_string out (show v)) args;
+                   Buffer.add_char out '\n';
+                   VUnit );
+             ] ))
+  | "TaskScope" ->
+      (* 루트 스코프. 구조적 동시성의 뿌리도 런타임이 준다 — 프로그램이
+         스스로 만들 수 있으면 부모 없는 작업이 생긴다. *)
+      Some (VScope "root")
+  | _ -> None
+
+let builtin pos name (args : value list) : value =
+  match (name, args) with
+  | "string.concat", [ VStr a; VStr b ] -> VStr (a ^ b)
+  | "string.len", [ VStr a ] -> VInt (String.length a)
+  | "int.show", [ VInt n ] -> VStr (string_of_int n)
+  | "int.abs", [ VInt n ] -> VInt (abs n)
+  | "bool.show", [ VBool b ] -> VStr (if b then "true" else "false")
+  | "list.len", [ VList xs ] -> VInt (List.length xs)
+  | _ ->
+      fail pos (Printf.sprintf "%s은(는) 런타임이 제공하지 않습니다 (표준 라이브러리가 아직 없습니다)" name)
+
+(* ------------------------------------------------------------------ *)
+(* 실행                                                                *)
+(* ------------------------------------------------------------------ *)
+
+type st = { prog : Ir.program }
+
+let rec eval st (env : env) (e : Ir.t) : value =
+  match e with
+  | Ir.I_unit -> VUnit
+  | Ir.I_lit (Ast.L_int n) -> VInt (int_of_string n)
+  | Ir.I_lit (Ast.L_str s) -> VStr s
+  | Ir.I_lit (Ast.L_bool b) -> VBool b
+  | Ir.I_ref (k, pos) -> eval_ref st env k pos
+  | Ir.I_list xs -> VList (List.map (eval st env) xs)
+  | Ir.I_make (n, fields) ->
+      VStruct (n, List.map (fun (k, e) -> (k, ref (eval st env e))) fields)
+  | Ir.I_closure c -> VClosure { params = c.c_params; body = c.c_body; env }
+  | Ir.I_if { cond; then_; else_ } -> (
+      match eval st env cond with
+      | VBool true -> eval st ([] :: env) then_
+      | _ -> eval st ([] :: env) else_)
+  | Ir.I_match { scrutinee; arms; pos } ->
+      let v = eval st env scrutinee in
+      let rec go = function
+        | [] -> fail pos "match에서 어떤 팔도 맞지 않았습니다"
+        | (p, body) :: rest -> (
+            match match_pat v p with
+            | None -> go rest
+            | Some binds ->
+                let env =
+                  List.fold_left (fun e (n, v) -> bind e n v) ([] :: env) binds
+                in
+                eval st env body)
+      in
+      go arms
+  | Ir.I_scope { name; body; _ } ->
+      (* v0의 실행 의미: 자식 작업은 순차로 돈다. 블록을 나가는 것이 join이다.
+         구조가 먼저고 병렬성은 그 위의 최적화다 — 순서가 반대면 취소와
+         전파를 나중에 끼워 넣게 된다. *)
+      let env = bind ([] :: env) name (VScope name) in
+      eval st env body
+  | Ir.I_seq (stmts, tail) ->
+      let env = List.fold_left (fun env s -> exec st env s) ([] :: env) stmts in
+      eval st env tail
+  | Ir.I_call { callee; args; pos } ->
+      let f = eval st env callee in
+      let args = List.map (eval st env) args in
+      apply st pos f args
+  | Ir.I_field { obj; name; pos } -> (
+      match eval st env obj with
+      | VStruct (sn, fields) -> (
+          match List.assoc_opt name fields with
+          | Some r -> !r
+          | None -> fail pos (Printf.sprintf "%s에 %s 필드가 없습니다" sn name))
+      | VCap (cn, meths) -> (
+          (* capability 메서드는 값을 통해서만 나온다. 여기가 권한이 코드로
+             흐르는 유일한 통로다. *)
+          match List.assoc_opt name meths with
+          | Some f -> VNative f
+          | None ->
+              fail pos (Printf.sprintf "capability %s에 %s이(가) 없습니다" cn name))
+      | VScope _ when name = "spawn" ->
+          VNative
+            (fun args ->
+              match args with
+              | [ f ] -> apply st pos f []
+              | _ -> fail pos "spawn은 함수 하나를 받습니다")
+      | other -> fail pos (Printf.sprintf "%s에는 필드가 없습니다" (show other)))
+  | Ir.I_unary (op, e, pos) -> (
+      match (op, eval st env e) with
+      | Ast.U_not, VBool b -> VBool (not b)
+      | Ast.U_neg, VInt n -> VInt (-n)
+      | _ -> fail pos "단항 연산자의 피연산자가 맞지 않습니다")
+  | Ir.I_binary (op, a, b, pos) -> eval_binary st env op a b pos
+
+and eval_ref st env k pos =
+  match k with
+  | Ir.R_local n -> (
+      match lookup env n with
+      | Some r -> !r
+      | None -> fail pos (Printf.sprintf "%s이(가) 묶여 있지 않습니다" n))
+  | Ir.R_ctor (enum, name) -> (
+      match Hashtbl.find_opt st.prog.Ir.ctors name with
+      | Some (_, 0) -> VEnum (enum, name, [])
+      | Some (_, n) -> VCtor (enum, name, n)
+      | None -> VEnum (enum, name, []))
+  | Ir.R_global n -> (
+      match Hashtbl.find_opt st.prog.Ir.fns n with
+      | Some f -> VFn f
+      | None -> (
+          match Hashtbl.find_opt st.prog.Ir.consts n with
+          | Some e -> eval st [ [] ] e
+          | None -> fail pos (Printf.sprintf "%s을(를) 찾을 수 없습니다" n)))
+  | Ir.R_builtin n -> VBuiltin n
+
+and apply st pos f args =
+  match f with
+  | VFn fn -> (
+      let env = [ List.map2 (fun p a -> (p, ref a)) fn.Ir.fn_params args ] in
+      try eval st env fn.Ir.fn_body with Return_exc v -> v)
+  | VClosure { params; body; env } -> (
+      let env = List.map2 (fun p a -> (p, ref a)) params args :: env in
+      try eval st env body with Return_exc v -> v)
+  | VCtor (enum, name, _) -> VEnum (enum, name, args)
+  (* 고차 builtin은 여기서 처리한다 — apply를 다시 부를 수 있어야 하므로 *)
+  | VBuiltin "list.each" -> (
+      match args with
+      | [ VList xs; f ] ->
+          List.iter (fun x -> ignore (apply st pos f [ x ])) xs;
+          VUnit
+      | _ -> fail pos "list.each는 리스트와 함수를 받습니다")
+  | VBuiltin "list.map" -> (
+      match args with
+      | [ VList xs; f ] -> VList (List.map (fun x -> apply st pos f [ x ]) xs)
+      | _ -> fail pos "list.map은 리스트와 함수를 받습니다")
+  | VBuiltin n -> builtin pos n args
+  | VNative f -> f args
+  | other -> fail pos (Printf.sprintf "%s은(는) 부를 수 없습니다" (show other))
+
+and exec st env (s : Ir.stmt) : env =
+  match s with
+  | Ir.S_do e ->
+      ignore (eval st env e);
+      env
+  | Ir.S_return (e, _) -> raise (Return_exc (eval st env e))
+  | Ir.S_let (p, e, pos) -> (
+      let v = eval st env e in
+      match match_pat v p with
+      | None -> fail pos "let 패턴이 값과 맞지 않습니다"
+      | Some binds -> List.fold_left (fun e (n, v) -> bind e n v) env binds)
+  | Ir.S_assign { place; value; pos } -> (
+      let v = eval st env value in
+      match place with
+      | Ir.I_ref (Ir.R_local n, _) -> (
+          match lookup env n with
+          | Some r ->
+              r := v;
+              env
+          | None -> fail pos (Printf.sprintf "%s이(가) 묶여 있지 않습니다" n))
+      | Ir.I_field { obj; name; _ } -> (
+          match eval st env obj with
+          | VStruct (_, fields) -> (
+              match List.assoc_opt name fields with
+              | Some r ->
+                  r := v;
+                  env
+              | None -> fail pos (Printf.sprintf "%s 필드가 없습니다" name))
+          | _ -> fail pos "필드에 대입할 수 없습니다")
+      | _ -> fail pos "대입할 수 없는 자리입니다")
+
+and match_pat v (p : Ir.pat) : (string * value) list option =
+  match (p, v) with
+  | Ir.IP_wild, _ -> Some []
+  | Ir.IP_bind n, _ -> Some [ (n, v) ]
+  | Ir.IP_lit (Ast.L_int n), VInt m ->
+      if int_of_string n = m then Some [] else None
+  | Ir.IP_lit (Ast.L_str s), VStr t -> if s = t then Some [] else None
+  | Ir.IP_lit (Ast.L_bool b), VBool c -> if b = c then Some [] else None
+  | Ir.IP_ctor (name, ps), VEnum (_, vn, args) ->
+      if name <> vn || List.length ps <> List.length args then None
+      else
+        List.fold_left2
+          (fun acc p a ->
+            match (acc, match_pat a p) with
+            | Some xs, Some ys -> Some (xs @ ys)
+            | _ -> None)
+          (Some []) ps args
+  | _ -> None
+
+and eval_binary st env op a b pos =
+  match op with
+  (* 단축 평가. 오른쪽을 먼저 계산하면 && 의 의미가 달라진다 *)
+  | Ast.B_and -> (
+      match eval st env a with VBool false -> VBool false | _ -> eval st env b)
+  | Ast.B_or -> (
+      match eval st env a with VBool true -> VBool true | _ -> eval st env b)
+  | _ -> (
+      let x = eval st env a and y = eval st env b in
+      match (op, x, y) with
+      | Ast.B_eq, _, _ -> VBool (eq x y)
+      | Ast.B_ne, _, _ -> VBool (not (eq x y))
+      | Ast.B_lt, VInt m, VInt n -> VBool (m < n)
+      | Ast.B_le, VInt m, VInt n -> VBool (m <= n)
+      | Ast.B_gt, VInt m, VInt n -> VBool (m > n)
+      | Ast.B_ge, VInt m, VInt n -> VBool (m >= n)
+      | Ast.B_add, VInt m, VInt n -> VInt (m + n)
+      | Ast.B_sub, VInt m, VInt n -> VInt (m - n)
+      | Ast.B_mul, VInt m, VInt n -> VInt (m * n)
+      | Ast.B_div, VInt _, VInt 0 -> fail pos "0으로 나눌 수 없습니다"
+      | Ast.B_div, VInt m, VInt n -> VInt (m / n)
+      | Ast.B_rem, VInt _, VInt 0 -> fail pos "0으로 나눌 수 없습니다"
+      | Ast.B_rem, VInt m, VInt n -> VInt (m mod n)
+      | _ -> fail pos "연산자의 피연산자 타입이 맞지 않습니다")
+
+(* ------------------------------------------------------------------ *)
+(* 진입                                                                *)
+(* ------------------------------------------------------------------ *)
+
+(* main이 선언한 capability만 런타임이 넘긴다. 선언하지 않은 권한은
+   프로그램 안에 존재하지 않는다. *)
+let run (prog : Ir.program) (entry : string)
+    (main_params : (string * string) list) : (string, Token.pos * string) result
+    =
+  Buffer.clear out;
+  let st = { prog } in
+  match Hashtbl.find_opt prog.Ir.fns (entry ^ "#main") with
+  | None -> Error (Token.{ line = 0; col = 0 }, "main 함수가 없습니다")
+  | Some fn -> (
+      let args =
+        List.map
+          (fun (_, tyname) ->
+            match root_capability tyname with
+            | Some v -> Ok v
+            | None ->
+                Error (Printf.sprintf "런타임이 %s capability를 제공하지 않습니다" tyname))
+          main_params
+      in
+      match List.find_opt Result.is_error args with
+      | Some (Error m) -> Error (Token.{ line = 0; col = 0 }, m)
+      | _ -> (
+          let args = List.map Result.get_ok args in
+          try
+            ignore (apply st Token.{ line = 0; col = 0 } (VFn fn) args);
+            Ok (Buffer.contents out)
+          with
+          | Fail (pos, msg) -> Error (pos, msg)
+          | Return_exc _ -> Ok (Buffer.contents out)))

lib/ir.ml

@@ -0,0 +1,383 @@
+(* 얇은 typed IR.
+
+   왜 AST를 직접 해석하지 않는가 — 표면 문법이 실행 의미에 닿지 않는다는 것을
+   구조로 강제하기 위해서다. v1이 백엔드를 무엇으로 바꾸든 소비하는 것은 이
+   IR이고, 문법을 고쳐도 여기가 그대로면 실행 의미는 그대로다.
+
+   얇다는 것의 뜻: 새 개념을 만들지 않는다. 검사 단계가 이미 답한 질문을
+   다시 묻지 않는다 — 여기 도달한 프로그램은 타입, effect, capability,
+   ownership 검사를 모두 통과했다. 그래서 IR에는 타입 검사가 없다.
+
+   낮추기에서 사라지는 것:
+   - E_try: Result에 대한 match로 펼친다. `?`는 설탕이다
+   - E_inst: 타입 인자는 실행에 영향이 없다 (단형화 없음, 값 표현이 같다)
+   - 한정 이름: "Alias.f" 하나의 이름으로 평탄화된다 (검사 단계와 같은 규칙) *)
+
+type pos = Token.pos
+
+(* 이름은 낮추기 시점에 분류된다. 실행 중에 "이게 지역인가 전역인가"를
+   다시 묻지 않는다. *)
+(* 전역 이름은 정규화된다: "<모듈 경로>#<이름>". 별칭은 가져오는 쪽의 선택이라
+   실행 의미에 들어와서는 안 된다 — 같은 함수가 부르는 자리마다 다른 이름이 되면
+   IR은 더 이상 v1의 번역 대상이 아니다. *)
+type ref_kind =
+  | R_local of string
+  | R_global of string (* "<경로>#<이름>" *)
+  | R_ctor of string * string (* enum 이름, 정규화된 variant 이름 *)
+  | R_builtin of string (* 본문 없는 선언 = 런타임이 구현한다 *)
+
+type pat =
+  | IP_wild
+  | IP_lit of Ast.lit
+  | IP_bind of string
+  | IP_ctor of string * pat list (* variant 이름 *)
+
+type t =
+  | I_unit
+  | I_lit of Ast.lit
+  | I_ref of ref_kind * pos
+  | I_list of t list
+  | I_make of string * (string * t) list (* struct 생성 *)
+  | I_closure of closure
+  | I_if of { cond : t; then_ : t; else_ : t }
+  | I_match of { scrutinee : t; arms : (pat * t) list; pos : pos }
+  | I_scope of { name : string; body : t; pos : pos }
+  | I_seq of stmt list * t (* 블록: 문 나열 + 꼬리 값 *)
+  | I_call of { callee : t; args : t list; pos : pos }
+  | I_field of { obj : t; name : string; pos : pos }
+  | I_unary of Ast.unop * t * pos
+  | I_binary of Ast.binop * t * t * pos
+
+and stmt =
+  | S_let of pat * t * pos
+  | S_assign of { place : t; value : t; pos : pos }
+  | S_return of t * pos
+  | S_do of t
+
+and closure = { c_params : string list; c_body : t; c_pos : pos }
+
+type fn = { fn_name : string; fn_params : string list; fn_body : t }
+
+type program = {
+  fns : (string, fn) Hashtbl.t;
+  (* variant 이름 -> (enum 이름, 인자 개수) *)
+  ctors : (string, string * int) Hashtbl.t;
+  caps : (string, string list) Hashtbl.t; (* capability -> 메서드 이름 *)
+  consts : (string, t) Hashtbl.t;
+}
+
+(* ------------------------------------------------------------------ *)
+(* 낮추기                                                              *)
+(* ------------------------------------------------------------------ *)
+
+let qual modl name = match modl with Some a -> a ^ "." ^ name | None -> name
+
+(* 지역 이름 스택. 검사 단계가 아니라 분류만 한다 — 여기서 못 찾은 이름은
+   전역이거나 생성자이거나 런타임 제공이다. *)
+type modinfo = {
+  m_path : string; (* 정규 경로 *)
+  m_ast : Ast.modul;
+  m_deps : (string * string) list; (* 별칭 -> 정규 경로 *)
+}
+
+(* 본문 없는 선언은 런타임이 구현한다. 그 이름은 모듈 파일 이름에서 온다:
+   std/list.cool의 each는 "list.each"다. 가져오는 쪽의 별칭과 무관하다. *)
+let builtin_name path name =
+  Filename.remove_extension (Filename.basename path) ^ "." ^ name
+
+type lctx = {
+  prog : program;
+  mods : (string, modinfo) Hashtbl.t;
+  cur : modinfo;
+  mutable locals : string list list;
+}
+
+let lpush c = c.locals <- [] :: c.locals
+let lpop c = match c.locals with _ :: r -> c.locals <- r | [] -> ()
+
+let lbind c n =
+  match c.locals with
+  | s :: r -> c.locals <- (n :: s) :: r
+  | [] -> c.locals <- [ [ n ] ]
+
+let is_local c n = List.exists (fun s -> List.mem n s) c.locals
+let builtin_ctors = [ "Ok"; "Err"; "Some"; "None" ]
+
+(* 한 모듈 안에서 이름 하나를 분류한다. 지역이 아니면 그 모듈의 정의를 본다. *)
+let in_module c (mi : modinfo) name =
+  let key = mi.m_path ^ "#" ^ name in
+  if Hashtbl.mem c.prog.ctors key then
+    match Hashtbl.find_opt c.prog.ctors key with
+    | Some (enum, _) -> Some (R_ctor (enum, key))
+    | None -> None
+  else if Hashtbl.mem c.prog.consts key then Some (R_global key)
+  else
+    let decl =
+      List.find_map
+        (function
+          | Ast.I_fn { decl; _ } when decl.fn_name = name -> Some decl
+          | _ -> None)
+        mi.m_ast.items
+    in
+    match decl with
+    | Some d when d.fn_body <> None -> Some (R_global key)
+    | Some _ -> Some (R_builtin (builtin_name mi.m_path name))
+    | None -> None
+
+let classify c name =
+  if is_local c name then R_local name
+  else if List.mem name builtin_ctors then
+    R_ctor ((if name = "Ok" || name = "Err" then "Result" else "Option"), name)
+  else
+    match in_module c c.cur name with
+    | Some k -> k
+    | None -> (
+        (* 한정 이름 "A.f": A가 이 모듈의 import면 그 모듈에서 찾는다. *)
+        match String.index_opt name '.' with
+        | None -> R_builtin name
+        | Some i -> (
+            let a = String.sub name 0 i in
+            let f = String.sub name (i + 1) (String.length name - i - 1) in
+            match List.assoc_opt a c.cur.m_deps with
+            | None -> R_builtin name
+            | Some path -> (
+                match Hashtbl.find_opt c.mods path with
+                | None -> R_builtin name
+                | Some mi -> (
+                    match in_module c mi f with
+                    | Some k -> k
+                    | None -> R_builtin (builtin_name path f)))))
+
+(* 패턴의 생성자도 정규 이름으로 접는다. 값 쪽과 같은 키를 써야 match가
+   성립한다 — 두 곳이 다른 규칙을 쓰면 조용히 안 맞는다. *)
+let ctor_key c modl name : string option =
+  if List.mem name builtin_ctors then Some name
+  else
+    let path =
+      match modl with
+      | None -> Some c.cur.m_path
+      | Some a -> List.assoc_opt a c.cur.m_deps
+    in
+    match path with
+    | None -> None
+    | Some p ->
+        let k = p ^ "#" ^ name in
+        if Hashtbl.mem c.prog.ctors k then Some k else None
+
+let rec lower_pat c (p : Ast.pattern) : pat =
+  match p with
+  | Ast.P_wild _ -> IP_wild
+  | Ast.P_lit (l, _) -> IP_lit l
+  | Ast.P_bind (n, _) -> (
+      (* 인자 없는 생성자는 이름만 쓴다. 바인딩과 구별은 여기서 끝난다. *)
+      match ctor_key c None n with
+      | Some k -> IP_ctor (k, [])
+      | None ->
+          lbind c n;
+          IP_bind n)
+  | Ast.P_ctor { modl; name; args; _ } ->
+      let k =
+        match ctor_key c modl name with Some k -> k | None -> qual modl name
+      in
+      IP_ctor (k, List.map (lower_pat c) args)
+
+let rec lower c (e : Ast.expr) : t =
+  match e with
+  | Ast.E_lit (l, _) -> I_lit l
+  | Ast.E_ident (n, pos) -> I_ref (classify c n, pos)
+  | Ast.E_list (xs, _) -> I_list (List.map (lower c) xs)
+  | Ast.E_struct { name; fields; _ } ->
+      I_make (name, List.map (fun (n, e) -> (n, lower c e)) fields)
+  | Ast.E_closure cl ->
+      lpush c;
+      List.iter (fun (n, _) -> lbind c n) cl.cl_params;
+      let body = lower_block c cl.cl_body in
+      lpop c;
+      I_closure
+        {
+          c_params = List.map fst cl.cl_params;
+          c_body = body;
+          c_pos = cl.cl_pos;
+        }
+  | Ast.E_if { cond; then_; else_; _ } ->
+      let cond = lower c cond in
+      lpush c;
+      let t = lower_block c then_ in
+      lpop c;
+      let e =
+        match else_ with
+        | None -> I_unit
+        | Some e ->
+            lpush c;
+            let v = lower c e in
+            lpop c;
+            v
+      in
+      I_if { cond; then_ = t; else_ = e }
+  | Ast.E_match { scrutinee; arms; pos } ->
+      let s = lower c scrutinee in
+      let arms =
+        List.map
+          (fun (a : Ast.arm) ->
+            lpush c;
+            let p = lower_pat c a.arm_pat in
+            let b = lower c a.arm_body in
+            lpop c;
+            (p, b))
+          arms
+      in
+      I_match { scrutinee = s; arms; pos }
+  | Ast.E_scope { name; body; pos; _ } ->
+      lpush c;
+      lbind c name;
+      let b = lower_block c body in
+      lpop c;
+      I_scope { name; body = b; pos }
+  | Ast.E_block b ->
+      lpush c;
+      let v = lower_block c b in
+      lpop c;
+      v
+  | Ast.E_call { callee; args; pos } ->
+      I_call { callee = lower c callee; args = List.map (lower c) args; pos }
+  | Ast.E_field { obj; name; pos } -> (
+      (* Alias.f / String.concat 처럼 이름공간 접근은 하나의 이름으로 접는다.
+         값의 필드 접근과 구별되는 지점은 obj가 지역 이름이 아닌 것뿐이다. *)
+      match obj with
+      | Ast.E_ident (o, _) when not (is_local c o) ->
+          I_ref (classify c (o ^ "." ^ name), pos)
+      | _ -> I_field { obj = lower c obj; name; pos })
+  | Ast.E_inst { callee; _ } -> lower c callee
+  | Ast.E_try { inner; pos } ->
+      (* `?`는 설탕이다: Ok(v) => v, Err(e) => return Err(e) *)
+      I_match
+        {
+          scrutinee = lower c inner;
+          arms =
+            [
+              (IP_ctor ("Ok", [ IP_bind "?v" ]), I_ref (R_local "?v", pos));
+              ( IP_ctor ("Err", [ IP_bind "?e" ]),
+                I_seq
+                  ( [
+                      S_return
+                        ( I_call
+                            {
+                              callee = I_ref (R_ctor ("Result", "Err"), pos);
+                              args = [ I_ref (R_local "?e", pos) ];
+                              pos;
+                            },
+                          pos );
+                    ],
+                    I_unit ) );
+            ];
+          pos;
+        }
+  | Ast.E_unary { op; operand; pos } -> I_unary (op, lower c operand, pos)
+  | Ast.E_binary { op; lhs; rhs; pos } ->
+      I_binary (op, lower c lhs, lower c rhs, pos)
+
+and lower_block c (b : Ast.block) : t =
+  let rec go = function
+    | [] -> I_unit
+    | [ Ast.S_expr e ] -> lower c e
+    | s :: rest -> (
+        let s = lower_stmt c s in
+        let tail = go rest in
+        match tail with
+        | I_seq (ss, t) -> I_seq (s :: ss, t)
+        | t -> I_seq ([ s ], t))
+  in
+  go b.stmts
+
+and lower_stmt c (s : Ast.stmt) : stmt =
+  match s with
+  | Ast.S_let { pat; value; pos; _ } ->
+      let v = lower c value in
+      (* 값을 먼저 낮춘다 — 바인딩은 그 뒤에야 보인다 *)
+      S_let (lower_pat c pat, v, pos)
+  | Ast.S_return { value; pos } ->
+      S_return ((match value with Some e -> lower c e | None -> I_unit), pos)
+  | Ast.S_assign { place; value; pos } ->
+      S_assign { place = lower c place; value = lower c value; pos }
+  | Ast.S_expr e -> S_do (lower c e)
+
+(* 모듈 그래프 전체를 하나의 IR 프로그램으로 낮춘다.
+
+   모듈 하나씩 낮추고 싶은 유혹이 있지만, 그러면 별칭이 실행 의미에 남는다.
+   같은 함수가 A에서는 Shapes.double, B에서는 Geo.double이 되어 IR이 더 이상
+   프로그램의 정규형이 아니게 된다. 정규 경로로 한 번 접는다. *)
+let of_program (mods : modinfo list) : program =
+  let prog =
+    {
+      fns = Hashtbl.create 64;
+      ctors = Hashtbl.create 64;
+      caps = Hashtbl.create 16;
+      consts = Hashtbl.create 16;
+    }
+  in
+  let index = Hashtbl.create 16 in
+  List.iter (fun mi -> Hashtbl.replace index mi.m_path mi) mods;
+  (* 1차: 이름부터. 낮추기가 이름을 분류하려면 그래프 전체가 먼저 보여야 한다. *)
+  List.iter
+    (fun mi ->
+      let key n = mi.m_path ^ "#" ^ n in
+      List.iter
+        (fun (it : Ast.item) ->
+          match it with
+          | Ast.I_enum { name; variants; _ } ->
+              List.iter
+                (fun (v : Ast.variant) ->
+                  Hashtbl.replace prog.ctors (key v.v_name)
+                    (name, List.length v.v_args))
+                variants
+          | Ast.I_capability { name; methods; _ } ->
+              Hashtbl.replace prog.caps name
+                (List.map (fun (d : Ast.fn_decl) -> d.fn_name) methods)
+          | Ast.I_const { name; _ } ->
+              Hashtbl.replace prog.consts (key name) I_unit
+          | _ -> ())
+        mi.m_ast.items)
+    mods;
+  List.iter
+    (fun (v, e, n) -> Hashtbl.replace prog.ctors v (e, n))
+    [
+      ("Ok", "Result", 1);
+      ("Err", "Result", 1);
+      ("Some", "Option", 1);
+      ("None", "Option", 0);
+    ];
+  (* 2차: 본문 *)
+  List.iter
+    (fun mi ->
+      let c = { prog; mods = index; cur = mi; locals = [] } in
+      let key n = mi.m_path ^ "#" ^ n in
+      List.iter
+        (fun (it : Ast.item) ->
+          match it with
+          | Ast.I_fn { decl; _ } -> (
+              match decl.fn_body with
+              | None -> ()
+              | Some body ->
+                  c.locals <- [];
+                  lpush c;
+                  List.iter
+                    (fun (p : Ast.param) -> lbind c p.p_name)
+                    decl.fn_params;
+                  let b = lower_block c body in
+                  lpop c;
+                  Hashtbl.replace prog.fns (key decl.fn_name)
+                    {
+                      fn_name = key decl.fn_name;
+                      fn_params =
+                        List.map
+                          (fun (p : Ast.param) -> p.p_name)
+                          decl.fn_params;
+                      fn_body = b;
+                    })
+          | Ast.I_const { name; value; _ } ->
+              c.locals <- [];
+              Hashtbl.replace prog.consts (key name) (lower c value)
+          | _ -> ())
+        mi.m_ast.items)
+    mods;
+  prog

lib/move.ml

@@ -0,0 +1,473 @@
+(* move / affinity 검사.
+
+   보안 정리 (ii) — safe code에서 capability는 복제·위조되지 않는다 — 를 코드로
+   닫는 단계다. 검사는 전부 함수 로컬 데이터플로우다. 전역 분석이 없다.
+
+   affinity의 뿌리는 capability다. capability를 필드로 가진 타입은 전이적으로
+   affine이고(철학 3), 이 전이가 없으면 wrapper 하나를 복사해 capability가
+   사실상 복제된다.
+
+   외부 타입은 affine임을 증명할 수 없으므로 copyable로 본다 — 모르는 것을
+   위반이라고 말하지 않는다. 그래서 이 검사를 시험하려면 자원 타입을 모듈
+   안에서 정의해야 한다 (samples/05). *)
+
+open Ast
+
+type error = { pos : Token.pos; msg : string }
+
+(* 값이 무엇인가: 소유한 affine 값인가, 빌린 값인가. 둘은 직교한다. *)
+type vinfo = { v_affine : bool; v_use : bool }
+
+let v_copy = { v_affine = false; v_use = false }
+
+type binding = {
+  b_id : int;
+  b_name : string;
+  b_affine : bool;
+  b_use : bool;
+  b_mut : bool;
+  b_depth : int;
+}
+
+type fninfo = { f_params : param list; f_ret : Ast.ty option }
+
+type state = {
+  aff : (string, bool) Hashtbl.t;
+  fns : (string, fninfo) Hashtbl.t;
+  meths : (string, (string * fninfo) list) Hashtbl.t;
+  mutable scopes : binding list list;
+  moved : (int, Token.pos) Hashtbl.t;
+  mutable next_id : int;
+  mutable depth : int;
+  (* 클로저 프레임: (프레임 깊이, 잡아온 바깥 바인딩). 중첩 클로저를 위해 스택 *)
+  mutable frames : (int * binding list ref) list;
+  mutable errors : error list;
+}
+
+let err st pos msg = st.errors <- { pos; msg } :: st.errors
+
+(* ------------------------------------------------------------------ *)
+(* affinity 유도                                                       *)
+(* ------------------------------------------------------------------ *)
+
+let builtin_containers = [ "List"; "Option"; "Result" ]
+
+let rec ty_affine st (t : Ast.ty) =
+  match t with
+  | T_fn { affine; _ } -> affine
+  | 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
+      let arg_affine =
+        List.exists
+          (function TA_ty t -> ty_affine st t | TA_eff _ -> false)
+          args
+      in
+      self || (List.mem name builtin_containers && arg_affine) || arg_affine
+
+(* capability가 뿌리다. struct/enum은 필드에서 전이된다. 상호 재귀 타입을 위해
+   변화가 없을 때까지 돈다. *)
+let derive_affinity st (items : item list) =
+  List.iter
+    (fun it ->
+      match it with
+      | I_capability { name; _ } -> Hashtbl.replace st.aff name true
+      | I_struct { name; _ } -> Hashtbl.replace st.aff name false
+      | I_enum { name; _ } -> Hashtbl.replace st.aff name false
+      | _ -> ())
+    items;
+  let changed = ref true in
+  while !changed do
+    changed := false;
+    List.iter
+      (fun it ->
+        let update name affine =
+          if affine && Hashtbl.find_opt st.aff name <> Some true then (
+            Hashtbl.replace st.aff name true;
+            changed := true)
+        in
+        match it with
+        | I_struct { name; fields; _ } ->
+            update name (List.exists (fun f -> ty_affine st f.f_ty) fields)
+        | I_enum { name; variants; _ } ->
+            update name
+              (List.exists
+                 (fun v -> List.exists (ty_affine st) v.v_args)
+                 variants)
+        | _ -> ())
+      items
+  done;
+  (* copyable 선언과 affine 필드는 공존할 수 없다 *)
+  List.iter
+    (fun it ->
+      match it with
+      | I_struct { copyable = true; name; fields; pos; _ } ->
+          List.iter
+            (fun f ->
+              if ty_affine st f.f_ty then
+                err st f.f_pos
+                  (Printf.sprintf "%s은(는) copyable로 선언되었지만 %s 필드가 affine입니다"
+                     name f.f_name))
+            fields;
+          ignore pos
+      | _ -> ())
+    items
+
+(* ------------------------------------------------------------------ *)
+(* 스코프                                                              *)
+(* ------------------------------------------------------------------ *)
+
+let push st = st.scopes <- [] :: st.scopes
+let pop st = match st.scopes with _ :: r -> st.scopes <- r | [] -> ()
+
+let add st name ~affine ~use ~mut_ =
+  st.next_id <- st.next_id + 1;
+  let b =
+    {
+      b_id = st.next_id;
+      b_name = name;
+      b_affine = affine;
+      b_use = use;
+      b_mut = mut_;
+      b_depth = st.depth;
+    }
+  in
+  (match st.scopes with
+  | s :: r -> st.scopes <- (b :: s) :: r
+  | [] -> st.scopes <- [ [ b ] ]);
+  b
+
+let find st name =
+  let rec go = function
+    | [] -> None
+    | s :: r -> (
+        match List.find_opt (fun b -> b.b_name = name) s with
+        | Some b -> Some b
+        | None -> go r)
+  in
+  go st.scopes
+
+(* 클로저 안에서 바깥 바인딩을 건드리면 capture다. 프레임마다 기록한다. *)
+let note_capture st b =
+  List.iter
+    (fun (fdepth, acc) ->
+      if b.b_depth < fdepth && not (List.exists (fun x -> x.b_id = b.b_id) !acc)
+      then acc := b :: !acc)
+    st.frames
+
+(* ------------------------------------------------------------------ *)
+(* 분기 병합 — 보수적 합집합                                            *)
+(* ------------------------------------------------------------------ *)
+
+let snapshot st = Hashtbl.copy st.moved
+
+let restore st snap =
+  Hashtbl.reset st.moved;
+  Hashtbl.iter (fun k v -> Hashtbl.replace st.moved k v) snap
+
+let merge st snaps =
+  (* 한 분기에서라도 moved면 병합 지점 이후 moved *)
+  Hashtbl.reset st.moved;
+  List.iter
+    (fun snap ->
+      Hashtbl.iter
+        (fun k v ->
+          if not (Hashtbl.mem st.moved k) then Hashtbl.replace st.moved k v)
+        snap)
+    snaps
+
+(* ------------------------------------------------------------------ *)
+(* 식                                                                  *)
+(* ------------------------------------------------------------------ *)
+
+type ctx = Borrow | Move of string (* 어디로 옮겨가는지 — 진단에 쓴다 *)
+
+let rec walk st (ctx : ctx) (e : expr) : vinfo =
+  match e with
+  | E_lit _ -> v_copy
+  | E_ident (n, pos) -> (
+      match find st n with
+      | None -> v_copy
+      | Some b ->
+          note_capture st b;
+          (match Hashtbl.find_opt st.moved b.b_id with
+          | Some mp ->
+              err st pos
+                (Printf.sprintf "%s은(는) 이미 move되었습니다 (%d:%d에서 소비)" n
+                   mp.Token.line mp.Token.col)
+          | None -> ());
+          (match ctx with
+          | Borrow -> ()
+          | Move where ->
+              if b.b_use then
+                err st pos
+                  (Printf.sprintf "%s은(는) 빌린 값이라 %s 없습니다 (own으로 받아야 합니다)" n
+                     where)
+              else if b.b_affine then Hashtbl.replace st.moved b.b_id pos);
+          { v_affine = b.b_affine; v_use = b.b_use })
+  | E_list (xs, _) ->
+      let infos = List.map (walk st (Move "컨테이너에 넣을 수")) xs in
+      { v_affine = List.exists (fun i -> i.v_affine) infos; v_use = false }
+  | E_struct { name; fields; _ } ->
+      List.iter (fun (_, e) -> ignore (walk st (Move "struct에 저장할 수") e)) fields;
+      {
+        v_affine =
+          (match Hashtbl.find_opt st.aff name with
+          | Some b -> b
+          | None -> false);
+        v_use = false;
+      }
+  | E_closure c -> (
+      let r = walk_closure st c in
+      (* use의 전염: 빌린 값을 capture한 클로저는 그 자체가 빌린 값이라
+         소유를 가져가는 자리로 갈 수 없다. 별도의 nonescaping 개념 없이
+         use 규칙 하나로 닫힌다. *)
+      match ctx with
+      | Move where when r.v_use ->
+          err st c.cl_pos
+            (Printf.sprintf "빌린 값을 capture한 클로저는 %s 없습니다 (use 값은 탈출하지 못합니다)"
+               where);
+          r
+      | _ -> r)
+  | E_if { cond; then_; else_; _ } ->
+      ignore (walk st Borrow cond);
+      let before = snapshot st in
+      let t1 = walk_block st ctx then_ in
+      let s1 = snapshot st in
+      restore st before;
+      let t2 = match else_ with None -> v_copy | Some e -> walk st ctx e in
+      let s2 = snapshot st in
+      merge st [ s1; s2 ];
+      { v_affine = t1.v_affine || t2.v_affine; v_use = t1.v_use || t2.v_use }
+  | E_match { scrutinee; arms; _ } ->
+      let sinfo = walk st Borrow scrutinee in
+      let before = snapshot st in
+      let results =
+        List.map
+          (fun a ->
+            restore st before;
+            push st;
+            bind_pattern st sinfo a.arm_pat;
+            let r = walk st ctx a.arm_body in
+            pop st;
+            (r, snapshot st))
+          arms
+      in
+      if results <> [] then merge st (List.map snd results);
+      {
+        v_affine = List.exists (fun (r, _) -> r.v_affine) results;
+        v_use = List.exists (fun (r, _) -> r.v_use) results;
+      }
+  | E_scope { name; parent; body; _ } ->
+      ignore (walk st Borrow (E_ident (parent, Token.{ line = 0; col = 0 })));
+      push st;
+      (* 자식 TaskScope는 second-class다 — 블록 밖으로 나갈 수 없다 *)
+      ignore (add st name ~affine:true ~use:true ~mut_:false);
+      let r = walk_block st ctx body in
+      pop st;
+      r
+  | E_block b ->
+      push st;
+      let r = walk_block st ctx b in
+      pop st;
+      r
+  | E_call { callee; args; pos } -> walk_call st callee args pos
+  | E_field { obj; _ } ->
+      (* v0에 부분 move는 없다. 필드 접근은 빌림이고 결과도 빌린 값이다. *)
+      let o = walk st Borrow obj in
+      if o.v_affine || o.v_use then { v_affine = true; v_use = true }
+      else v_copy
+  | E_inst { callee; _ } -> walk st Borrow callee
+  | E_try { inner; _ } -> walk st ctx inner
+  | E_unary { operand; _ } -> walk st Borrow operand
+  | E_binary { lhs; rhs; _ } ->
+      ignore (walk st Borrow lhs);
+      ignore (walk st Borrow rhs);
+      v_copy
+
+and bind_pattern st (info : vinfo) p =
+  match p with
+  | P_wild _ | P_lit _ -> ()
+  | P_bind (n, _) ->
+      ignore (add st n ~affine:info.v_affine ~use:info.v_use ~mut_:false)
+  | P_ctor { args; _ } -> List.iter (bind_pattern st info) args
+
+and walk_block st ctx (b : block) : vinfo =
+  let rec go = function
+    | [] -> v_copy
+    | [ S_expr e ] -> walk st ctx e (* 꼬리 식은 블록의 값이다 *)
+    | s :: rest ->
+        walk_stmt st s;
+        go rest
+  in
+  go b.stmts
+
+and walk_stmt st = function
+  | S_let { mut_; pat; value; _ } ->
+      let info = walk st (Move "다른 이름에 묶을 수") value in
+      let rec bind p =
+        match p with
+        | P_bind (n, _) ->
+            ignore (add st n ~affine:info.v_affine ~use:info.v_use ~mut_)
+        | P_ctor { args; _ } -> List.iter bind args
+        | _ -> ()
+      in
+      bind pat
+  | S_return { value; _ } -> (
+      match value with
+      | None -> ()
+      | Some e -> ignore (walk st (Move "반환할 수") e))
+  | S_assign { place; value; _ } ->
+      ignore (walk st (Move "대입할 수") value);
+      ignore (walk st Borrow place)
+  | S_expr e -> ignore (walk st Borrow e)
+
+(* 클로저: 무엇을 잡아왔는지가 클로저 자신의 성질을 정한다 (전이 규칙) *)
+and walk_closure st (c : closure) : vinfo =
+  st.depth <- st.depth + 1;
+  let acc = ref [] in
+  st.frames <- (st.depth, acc) :: st.frames;
+  push st;
+  List.iter
+    (fun (n, ann) ->
+      let affine = match ann with Some t -> ty_affine st t | None -> false in
+      ignore (add st n ~affine ~use:false ~mut_:false))
+    c.cl_params;
+  ignore (walk_block st (Move "반환할 수") c.cl_body);
+  pop st;
+  st.frames <- List.tl st.frames;
+  st.depth <- st.depth - 1;
+  let captured = !acc in
+  let affine = ref false and use_ = ref false in
+  List.iter
+    (fun b ->
+      if b.b_mut then
+        err st c.cl_pos
+          (Printf.sprintf
+             "클로저는 mut 바인딩 %s을(를) capture할 수 없습니다 (v0에 참조가 없으므로 별칭도 복사도 만들지 \
+              않는다)"
+             b.b_name);
+      if b.b_use then use_ := true;
+      if b.b_affine && not b.b_use then (
+        (* by-move capture: 바깥에서는 여기서 소비된다 *)
+        affine := true;
+        if not (Hashtbl.mem st.moved b.b_id) then
+          Hashtbl.replace st.moved b.b_id c.cl_pos))
+    captured;
+  { v_affine = !affine; v_use = !use_ }
+
+and walk_call st callee args pos =
+  let info = callee_info st callee in
+  ignore (walk st Borrow callee);
+  let params = match info with Some f -> f.f_params | None -> [] in
+  List.iteri
+    (fun i a ->
+      let p = List.nth_opt params i in
+      let own = match p with Some p -> p.p_own | None -> false in
+      let pty = Option.map (fun p -> p.p_ty) p in
+      let ctx = if own then Move "다른 함수에 넘길 수" else Borrow in
+      let got = walk st ctx a in
+      (* callable affinity: affine 클로저를 fn 자리에 넘길 수 없다 *)
+      match pty with
+      | Some (T_fn { affine = false; _ }) when got.v_affine && not got.v_use ->
+          err st pos
+            "affine 값을 capture한 클로저는 fn 자리에 넘길 수 없습니다 (affine fn이어야 합니다)"
+      | _ -> ())
+    args;
+  match info with
+  | Some { f_ret = Some t; _ } -> { v_affine = ty_affine st t; v_use = false }
+  | _ -> v_copy
+
+and callee_info st callee =
+  match callee with
+  | E_ident (n, _) when find st n = None -> Hashtbl.find_opt st.fns n
+  | E_inst { callee = E_ident (n, _); _ } when find st n = None ->
+      Hashtbl.find_opt st.fns n
+  | E_field { obj = E_ident (o, _); name; _ } -> (
+      match find st o with
+      | Some _ -> (
+          (* 값의 메서드: 타입을 모르면 넘어간다. capability 메서드는 아래에서 *)
+          match
+            Hashtbl.fold
+              (fun _ methods acc ->
+                match acc with
+                | Some _ -> acc
+                | None -> List.assoc_opt name methods)
+              st.meths None
+          with
+          | Some f -> Some f
+          | None -> None)
+      (* 모듈 별칭을 통한 호출: 가져온 함수는 "Alias.f" 키로 들어와 있다 *)
+      | None -> Hashtbl.find_opt st.fns (o ^ "." ^ name))
+  | _ -> None
+
+(* ------------------------------------------------------------------ *)
+(* 선언                                                                *)
+(* ------------------------------------------------------------------ *)
+
+let check_fn st (d : fn_decl) =
+  match d.fn_body with
+  | None -> ()
+  | Some body ->
+      st.scopes <- [];
+      Hashtbl.reset st.moved;
+      st.depth <- 0;
+      st.frames <- [];
+      push st;
+      List.iter
+        (fun p ->
+          let affine = ty_affine st p.p_ty in
+          (* 무표기 = 빌림. own만이 소유 이전이다. *)
+          let use_ = affine && not p.p_own in
+          ignore (add st p.p_name ~affine ~use:use_ ~mut_:p.p_mut))
+        d.fn_params;
+      let r = walk_block st (Move "반환할 수") body in
+      (match d.fn_ret with
+      | Some (T_fn { affine = false; _ }) when r.v_affine && not r.v_use ->
+          err st d.fn_pos
+            (Printf.sprintf
+               "%s이(가) affine 값을 capture한 클로저를 fn 타입으로 반환합니다 (affine fn이어야 합니다)"
+               d.fn_name)
+      | _ -> ());
+      pop st
+
+let check ?(imports : item list = []) (m : modul) : error list =
+  let st =
+    {
+      aff = Hashtbl.create 16;
+      fns = Hashtbl.create 16;
+      meths = Hashtbl.create 16;
+      scopes = [];
+      moved = Hashtbl.create 16;
+      next_id = 0;
+      depth = 0;
+      frames = [];
+      errors = [];
+    }
+  in
+  derive_affinity st (imports @ m.items);
+  List.iter
+    (fun it ->
+      match it with
+      | I_fn { decl; _ } ->
+          Hashtbl.replace st.fns decl.fn_name
+            { f_params = decl.fn_params; f_ret = decl.fn_ret }
+      | I_capability { name; methods; _ } ->
+          Hashtbl.replace st.meths name
+            (List.map
+               (fun d ->
+                 (d.fn_name, { f_params = d.fn_params; f_ret = d.fn_ret }))
+               methods)
+      | _ -> ())
+    (imports @ m.items);
+  List.iter
+    (fun it -> match it with I_fn { decl; _ } -> check_fn st decl | _ -> ())
+    m.items;
+  List.sort
+    (fun a b ->
+      compare
+        (a.pos.Token.line, a.pos.Token.col)
+        (b.pos.Token.line, b.pos.Token.col))
+    (List.rev st.errors)

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 })
+        P_ctor { modl; name = n; args; pos = p })
-      else P_bind (n, p)
+      else
+        match modl with
+        | Some _ -> P_ctor { modl; name = n; args = []; pos = p }
+        | None -> P_bind (n, p))
   | _ -> err_expect st "패턴"
 
 (* ------------------------------------------------------------------ *)
@@ -769,20 +784,79 @@ let parse_item st =
           I_const { pub; name; ty; value; pos = p }
       | _ -> err_expect st "선언 (fn, struct, enum, capability, const)")
 
+(* ------------------------------------------------------------------ *)
+(* 오류 복구                                                           *)
+(*                                                                     *)
+(* 항목 단위로만 회복한다. 오류가 난 선언은 통째로 버리고 다음 선언에서       *)
+(* 다시 시작한다 — 문 단위로 더 잘게 회복하려 하면 파서가 추측을 하게 되고,   *)
+(* 틀린 추측은 없는 오류를 지어낸다. 한 항목에 오류 하나가 상한이라는 것은     *)
+(* 정직한 한계이지 숨길 것이 아니다.                                        *)
+(*                                                                     *)
+(* 동기화 지점: 중괄호 깊이 0이고, 줄 첫머리이며, 선언을 시작할 수 있는 토큰.   *)
+(* 세 조건이 다 필요하다. 본문 안의 fn을 새 항목으로 오인하면 그 뒤가 전부      *)
+(* 어긋난다. *)
+
+let item_starts =
+  [
+    Token.Kw_import;
+    Token.Kw_reexport;
+    Token.Kw_pub;
+    Token.Kw_fn;
+    Token.Kw_struct;
+    Token.Kw_enum;
+    Token.Kw_capability;
+    Token.Kw_const;
+    Token.Kw_copyable;
+  ]
+
+let at_line_start st = st.i > 0 && st.toks.(st.i - 1).Token.kind = Token.Newline
+
+let sync st =
+  let depth = ref 0 in
+  let fin = ref false in
+  while not !fin do
+    match kind st with
+    | Token.Eof -> fin := true
+    | Token.LBrace ->
+        incr depth;
+        adv st
+    | Token.RBrace ->
+        decr depth;
+        adv st
+    | k ->
+        if !depth <= 0 && at_line_start st && List.mem k item_starts then
+          fin := true
+        else adv st
+  done
+
 let parse_module st =
   skip_nl st;
+  let errors = ref [] in
   let rec loop acc =
     if kind st = Token.Eof then List.rev acc
     else
-      let it = parse_item st in
+      match parse_item st with
-      skip_nl st;
+      | it ->
-      loop (it :: acc)
+          skip_nl st;
+          loop (it :: acc)
+      | exception Error e ->
+          errors := e :: !errors;
+          let before = st.i in
+          sync st;
+          (* 진행 보장. 같은 자리에서 다시 실패하면 무한 루프다. *)
+          if st.i = before then adv st;
+          skip_nl st;
+          loop acc
   in
-  { items = loop [] }
+  let items = loop [] in
+  ({ items }, List.rev !errors)
 
-let parse (tokens : Token.t list) : modul =
+let parse_all (tokens : Token.t list) : modul * error list =
   let st = { toks = Array.of_list tokens; i = 0; no_struct = false } in
   parse_module st
 
+let parse (tokens : Token.t list) : modul =
+  match parse_all tokens with m, [] -> m | _, e :: _ -> raise (Error e)
+
 let parse_result tokens =
-  match parse tokens with m -> Ok m | exception Error e -> Error e
+  match parse_all tokens with m, [] -> Ok m | _, e :: _ -> Error e

lib/resolve.ml

@@ -11,7 +11,10 @@
 
 open Ast
 
-type error = { pos : Token.pos; msg : string }
+(* blocking: 이름을 해소하지 못했다는 뜻이고, 이후 단계는 의미가 없다.
+   lint는 다르다 — 코드는 분석 가능하고 검사도 계속되어야 한다.
+   둘을 같은 통에 넣으면 lint 하나가 진짜 타입 오류를 가린다. *)
+type error = { pos : Token.pos; msg : string; blocking : bool }
 type info = { externals : (string * Token.pos) list }
 type item_kind = K_fn | K_type | K_const | K_import
 
@@ -23,13 +26,20 @@ type state = {
   mutable scopes : (string * bool) list list; (* 이름 -> 가변 여부 *)
   mutable errors : error list;
   mutable ext : (string * Token.pos) list;
+  (* 실제로 참조된 import 별칭 *)
+  used : (string, unit) Hashtbl.t;
 }
 
 let builtin_types =
   [ "Int"; "Bool"; "String"; "Unit"; "List"; "Option"; "Result" ]
 
 let builtin_values = [ "unit"; "Ok"; "Err"; "Some"; "None" ]
-let error st pos msg = st.errors <- { pos; msg } :: st.errors
+let error st pos msg = st.errors <- { pos; msg; blocking = true } :: st.errors
+let lint st pos msg = st.errors <- { pos; msg; blocking = false } :: st.errors
+
+let use_alias st a =
+  if Hashtbl.find_opt st.items a = Some K_import then
+    Hashtbl.replace st.used a ()
 
 let external_ref st name pos =
   if not (List.mem_assoc name st.ext) then st.ext <- (name, pos) :: st.ext
@@ -77,7 +87,13 @@ 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; _ } ->
+      use_alias st a;
+      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 +134,11 @@ 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; _ } ->
+      use_alias st a;
+      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 +164,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;
@@ -191,7 +211,12 @@ let rec resolve_expr st = function
   | E_call { callee; args; _ } ->
       resolve_expr st callee;
       List.iter (resolve_expr st) args
-  | E_field { obj; _ } -> resolve_expr st obj
+  | E_field { obj; _ } ->
+      (* Alias.f — 별칭 접근도 사용이다 *)
+      (match obj with
+      | E_ident (o, _) when lookup_local st o = None -> use_alias st o
+      | _ -> ());
+      resolve_expr st obj
   | E_inst { callee; args; pos } ->
       resolve_expr st callee;
       List.iter (resolve_targ st pos) args
@@ -304,6 +329,7 @@ let resolve (m : modul) : info * error list =
       scopes = [];
       errors = [];
       ext = [];
+      used = Hashtbl.create 8;
     }
   in
   (* 1차: 모듈 수준 이름을 모은다. 선언 순서에 의존하지 않는다. *)
@@ -354,6 +380,17 @@ let resolve (m : modul) : info * error list =
           resolve_expr st value;
           pop st)
     m.items;
+  (* 미사용 import는 오류다. 취향 문제가 아니라 invalidation 표면 문제다 —
+     쓰지도 않는 모듈의 시그니처가 바뀌면 이 모듈이 재검사된다. 증분 루프의
+     비용을 아무 이유 없이 넓히는 선언은 남겨둘 수 없다. *)
+  List.iter
+    (fun it ->
+      match it with
+      | I_import { alias; pos; _ } when not (Hashtbl.mem st.used alias) ->
+          lint st pos
+            (Printf.sprintf "%s을(를) 가져왔지만 쓰지 않습니다 (재검사 범위만 넓힙니다)" alias)
+      | _ -> ())
+    m.items;
   let by_pos (_, a) (_, b) =
     compare (a.Token.line, a.Token.col) (b.Token.line, b.Token.col)
   in

lib/session.ml

@@ -0,0 +1,280 @@
+(* 모듈 로딩, 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;
+  std : string option; (* 표준 라이브러리 디렉터리 *)
+  modules : (string, entry) Hashtbl.t;
+  (* 통계: 무엇이 몇 번 재검사됐는지. 측정이 목적이므로 처음부터 센다. *)
+  mutable checked : string list;
+}
+
+(* 표준 라이브러리를 찾는다. COOL_STD가 있으면 그것, 없으면 위로 올라가며
+   std/list.cool을 찾는다. 못 찾으면 없는 것이고, 그때 std 이름들은 외부
+   참조로 남는다 — 없다고 말하지 않는다. *)
+let find_std root =
+  match Sys.getenv_opt "COOL_STD" with
+  | Some d when Sys.file_exists d -> Some d
+  | _ ->
+      let rec up dir n =
+        if n = 0 then None
+        else
+          let cand = Filename.concat dir "std" in
+          if Sys.file_exists (Filename.concat cand "list.cool") then Some cand
+          else
+            let parent = Filename.dirname dir in
+            if parent = dir then None else up parent (n - 1)
+      in
+      up
+        (if Filename.is_relative root then Filename.concat (Sys.getcwd ()) root
+         else root)
+        8
+
+let create ?(root = ".") ?std () =
+  {
+    root;
+    std = (match std with Some _ -> std | None -> find_std 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 std_prefix = "cool.dev/std/"
+
+let starts_with p s =
+  String.length s >= String.length p && String.sub s 0 (String.length p) = p
+
+(* 경로를 파일로 바꾼다. 바꿀 수 없으면 None — v0에는 패키지 해소가 없으므로
+   표준 라이브러리 밖의 패키지는 불투명하게 남는다. *)
+let resolve_import st path : string option =
+  if starts_with std_prefix path then
+    let name =
+      String.sub path (String.length std_prefix)
+        (String.length path - String.length std_prefix)
+    in
+    match st.std with
+    | Some d -> Some (Filename.concat d (name ^ ".cool"))
+    | None -> None
+  else if is_package path then None
+  else Some (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_all toks with
+      | m, [] -> Ok m
+      | _, errs ->
+          Error
+            (List.map (fun (e : Parser.error) -> err_of file e.pos e.msg) errs))
+
+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 es ->
+      {
+        path;
+        ast = { items = [] };
+        imports = [];
+        iface = { items = []; hash = "" };
+        errors = es;
+      }
+  | Ok ast ->
+      let imports =
+        List.filter_map
+          (fun (a, p) ->
+            match resolve_import st p with
+            | Some f -> Some (a, f)
+            | None -> None)
+          (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
+      (* 이름을 해소하지 못했으면 뒤 단계는 의미가 없다. lint는 막지 않는다. *)
+      let blocking =
+        List.filter (fun (e : Resolve.error) -> e.blocking) rerrors
+      in
+      let errors =
+        List.map (fun (e : Resolve.error) -> err_of path e.pos e.msg) rerrors
+      in
+      let errors =
+        if blocking <> [] then errors
+        else
+          errors
+          @ 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) ->
+            match resolve_import st p with
+            | Some f -> load st ~visiting:(path :: visiting) f
+            | None -> ())
+          (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
+
+(* ------------------------------------------------------------------ *)
+(* 실행                                                                *)
+(* ------------------------------------------------------------------ *)
+
+(* main이 선언한 파라미터의 타입 이름을 뽑는다. 런타임은 이 목록만 보고
+   권한을 만든다 — 선언하지 않은 capability는 프로그램에 존재하지 않는다. *)
+let main_params (m : Ast.modul) =
+  let rec ty_name (t : Ast.ty) =
+    match t with
+    | Ast.T_named { modl; name; _ } -> (
+        match modl with Some a -> a ^ "." ^ name | None -> name)
+    | Ast.T_fn _ -> "<fn>"
+  in
+  List.concat_map
+    (function
+      | Ast.I_fn { decl; _ } when decl.fn_name = "main" ->
+          List.map
+            (fun (p : Ast.param) -> (p.p_name, ty_name p.p_ty))
+            decl.fn_params
+      | _ -> [])
+    m.items
+
+let run st path : (string, error) result =
+  load st path;
+  let errs = errors st in
+  if errs <> [] then Error (List.hd errs)
+  else
+    match find st path with
+    | None ->
+        Error { file = path; line = 0; col = 0; message = "모듈을 찾을 수 없습니다" }
+    | Some e -> (
+        (* IR은 그래프 전체를 받는다. 별칭이 실행 의미에 남지 않도록. *)
+        let mods =
+          Hashtbl.fold
+            (fun p (d : entry) acc ->
+              { Ir.m_path = p; m_ast = d.ast; m_deps = d.imports } :: acc)
+            st.modules []
+        in
+        let prog = Ir.of_program mods in
+        match Interp.run prog path (main_params e.ast) with
+        | Ok out -> Ok out
+        | Error (pos, msg) -> Error (err_of path pos msg))

lib/typecheck.ml

@@ -12,8 +12,10 @@ module T = Types
 type error = { pos : Token.pos; msg : string }
 
 type scheme = {
-  s_gen : string list; (* 타입 파라미터 이름 (effect 파라미터는 제외) *)
+  s_gen : string list; (* 타입 파라미터 *)
+  s_eff_gen : string list; (* effect 파라미터 *)
   s_params : T.t list;
+  s_eff : T.eff; (* 이 함수를 부르면 수행되는 effect *)
   s_ret : T.t;
 }
 
@@ -24,8 +26,18 @@ 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. 위치를 같이 들고 다녀야 "어디서 수행했는지"를
+     말할 수 있다. 클로저에 들어가면 저장하고 비운다 — 클로저의 effect는
+     정의한 자리가 아니라 부르는 자리에서 일어난다. *)
+  mutable performed : (T.atom * Token.pos) list;
+  (* 이 본문에서 모르는 것을 만났는가. 과잉 선언 판정에만 쓴다 — 외부 타입의
+     메서드는 effect를 알 수 없으므로 "수행하지 않았다"고 말할 근거가 없다. *)
+  mutable saw_unknown : bool;
   mutable errors : error list;
 }
 
@@ -55,17 +67,26 @@ let lookup env n =
 (* Ast.ty -> Types.t                                                   *)
 (* ------------------------------------------------------------------ *)
 
+let conv_eff_atom (a : Ast.eff_atom) : T.eff =
+  match a with
+  | Eff_var v -> [ T.A_var v ]
+  | Eff_set names -> List.map (fun { cap; meth } -> T.A_name (cap, meth)) names
+
+let conv_eff_result (atoms : Ast.eff_result) : T.eff =
+  T.eff_resolve (List.concat_map conv_eff_atom atoms)
+
 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
@@ -77,11 +98,12 @@ let rec conv env (gen : string list) (t : Ast.ty) : T.t =
               || Hashtbl.mem env.enums name || Hashtbl.mem env.caps name
             then T.TCon (name, args)
             else T.TUnknown)
-  | T_fn { affine; params; ret; _ } ->
+  | T_fn { affine; params; eff; ret; _ } ->
       T.TFn
         {
           affine;
           params = List.map (conv env gen) params;
+          eff = (match eff with None -> [] | Some a -> conv_eff_atom a);
           ret = (match ret with None -> T.TUnit | Some r -> conv env gen r);
         }
 
@@ -91,20 +113,34 @@ let scheme_of env (d : fn_decl) : scheme =
       (fun g -> if g.gp_effect then None else Some g.gp_name)
       d.fn_gen
   in
+  let egen =
+    List.filter_map
+      (fun g -> if g.gp_effect then Some g.gp_name else None)
+      d.fn_gen
+  in
   {
     s_gen = gen;
+    s_eff_gen = egen;
     s_params = List.map (fun p -> conv env gen p.p_ty) d.fn_params;
+    s_eff =
+      (match d.fn_eff with None -> [] | Some atoms -> conv_eff_result atoms);
     s_ret = (match d.fn_ret with None -> T.TUnit | Some r -> conv env gen r);
   }
 
 (* 호출 지점 인스턴스화: 타입 파라미터마다 새 미지수 *)
 let instantiate (s : scheme) =
   let sub = List.map (fun v -> (v, T.fresh ())) s.s_gen in
-  (List.map (T.subst sub) s.s_params, T.subst sub s.s_ret)
+  let esub = List.map (fun v -> (v, T.fresh_eff ())) s.s_eff_gen in
+  ( List.map (T.subst sub esub) s.s_params,
+    T.subst_eff esub s.s_eff,
+    T.subst sub esub s.s_ret )
 
 let instantiate_with (s : scheme) (args : T.t list) =
   let sub = List.map2 (fun v a -> (v, a)) s.s_gen args in
-  (List.map (T.subst sub) s.s_params, T.subst sub s.s_ret)
+  let esub = List.map (fun v -> (v, T.fresh_eff ())) s.s_eff_gen in
+  ( List.map (T.subst sub esub) s.s_params,
+    T.subst_eff esub s.s_eff,
+    T.subst sub esub s.s_ret )
 
 (* ------------------------------------------------------------------ *)
 (* 내장 생성자                                                          *)
@@ -144,12 +180,14 @@ let rec infer env (e : expr) : T.t =
               | _ -> (
                   match Hashtbl.find_opt env.fns n with
                   | Some s ->
-                      let params, ret = instantiate s in
+                      let params, eff, ret = instantiate s in
-                      T.TFn { affine = false; params; ret }
+                      T.TFn { affine = false; params; eff; ret }
                   | None -> (
                       match Hashtbl.find_opt env.ctors n with
                       | Some enum -> nullary_ctor env enum n
-                      | None -> T.TUnknown)))))
+                      | None ->
+                          env.saw_unknown <- true;
+                          T.TUnknown)))))
   | E_list (xs, pos) ->
       let elem = T.fresh () in
       List.iter
@@ -187,6 +225,7 @@ let rec infer env (e : expr) : T.t =
           pop env)
         arms;
       if arms = [] then err env pos "match에 팔이 없습니다";
+      check_exhaustive env s arms pos;
       result
   | E_scope { name; parent; body; pos } ->
       (match lookup env parent with
@@ -247,6 +286,40 @@ let rec infer env (e : expr) : T.t =
           if not (T.unify a b) then mismatch env pos a b "같은 타입끼리만 비교할 수 있습니다";
           T.TBool)
 
+(* exhaustiveness: 철학 1의 대표 항목이자 interface hash가 enum 본문을
+   입력으로 삼는 이유다 *)
+and check_exhaustive env scrutinee arms pos =
+  let eenv : Exhaust.env =
+    {
+      variants =
+        (fun name args ->
+          match Hashtbl.find_opt env.enums name with
+          | None -> None
+          | Some (gen, variants) ->
+              let sub =
+                try List.map2 (fun v a -> (v, a)) gen args
+                with Invalid_argument _ -> []
+              in
+              Some
+                (List.map
+                   (fun (n, tys) -> (n, List.map (T.subst sub []) tys))
+                   variants));
+      is_ctor =
+        (fun n ->
+          Hashtbl.mem env.ctors n || List.mem n [ "Ok"; "Err"; "Some"; "None" ]);
+    }
+  in
+  let r = Exhaust.check eenv scrutinee (List.map (fun a -> a.arm_pat) arms) in
+  (match r.missing with
+  | None -> ()
+  | Some w -> err env pos (Printf.sprintf "match가 모든 경우를 덮지 않습니다 (빠진 경우: %s)" w));
+  List.iter
+    (fun i ->
+      match List.nth_opt arms i with
+      | Some a -> err env a.arm_pos "이 팔은 앞의 팔들에 가려 도달할 수 없습니다"
+      | None -> ())
+    r.unreachable
+
 and nullary_ctor env enum name =
   match Hashtbl.find_opt env.enums enum with
   | None -> T.TUnknown
@@ -268,7 +341,7 @@ and infer_struct env name fields pos =
           match List.assoc_opt fname decl_fields with
           | None -> err env pos (Printf.sprintf "%s에 %s 필드가 없습니다" name fname)
           | Some ft ->
-              let want = T.subst sub ft in
+              let want = T.subst sub [] ft in
               let got = infer env fe in
               if not (T.unify want got) then
                 mismatch env pos want got (Printf.sprintf "%s.%s 필드" name fname))
@@ -302,19 +375,41 @@ and infer_closure env (c : closure) (expected : T.t option) =
       c.cl_params expected_params
   in
   let declared_ret = Option.map (conv env []) c.cl_ret in
-  let saved = env.ret in
+  let saved_ret = env.ret in
   env.ret <-
     (match declared_ret with
     | Some t -> t
     | None -> ( match expected_ret with Some t -> t | None -> T.TUnknown));
+  (* 클로저 본문의 effect는 바깥 함수가 수행하는 것이 아니다. 저장하고 비운다. *)
+  let saved_perf = env.performed in
+  env.performed <- [];
   let body = infer_block env c.cl_body in
+  let inner = env.performed in
+  env.performed <- saved_perf;
+  let declared_eff = Option.map conv_eff_atom c.cl_eff in
+  let eff =
+    match declared_eff with
+    | Some d ->
+        (* 클로저가 effects를 명시했으면 본문이 그 안에 들어야 한다 *)
+        List.iter
+          (fun (a, pos) ->
+            List.iter
+              (fun m ->
+                err env pos
+                  (Printf.sprintf "클로저가 선언하지 않은 effect %s을(를) 수행합니다 (선언: %s)"
+                     (T.atom_show m) (T.eff_show d)))
+              (T.eff_missing ~declared:d ~performed:[ a ]))
+          inner;
+        d
+    | None -> T.eff_resolve (List.map fst inner)
+  in
   (match declared_ret with
   | Some t when not (T.unify t body) -> mismatch env c.cl_pos t body "클로저의 반환"
   | _ -> ());
   let ret = match declared_ret with Some t -> t | None -> body in
-  env.ret <- saved;
+  env.ret <- saved_ret;
   pop env;
-  T.TFn { affine = false; params = param_tys; ret }
+  T.TFn { affine = false; params = param_tys; eff; ret }
 
 and infer_call env callee args pos =
   let fn_ty =
@@ -324,12 +419,13 @@ and infer_call env callee args pos =
         | Some enum -> Some (ctor_fn env enum n)
         | None -> (
             match builtin_ctor n with
-            | Some (params, ret) -> Some (T.TFn { affine = false; params; ret })
+            | Some (params, ret) ->
+                Some (T.TFn { affine = false; params; eff = []; ret })
             | None -> (
                 match Hashtbl.find_opt env.fns n with
                 | Some s ->
-                    let params, ret = instantiate s in
+                    let params, eff, ret = instantiate s in
-                    Some (T.TFn { affine = false; params; ret })
+                    Some (T.TFn { affine = false; params; eff; ret })
                 | None -> None)))
     | _ -> (
         match T.resolve (infer env callee) with
@@ -338,9 +434,13 @@ and infer_call env callee args pos =
   in
   match fn_ty with
   | None ->
+      env.saw_unknown <- true;
       List.iter (fun a -> ignore (infer env a)) args;
       T.TUnknown
-  | Some (T.TFn { params; ret; _ }) ->
+  | Some (T.TFn { params; eff; ret; _ }) ->
+      List.iter
+        (fun a -> env.performed <- (a, pos) :: env.performed)
+        (T.eff_resolve eff);
       if List.length params <> List.length args then (
         err env pos
           (Printf.sprintf "인자 %d개가 필요한데 %d개가 주어졌습니다" (List.length params)
@@ -354,7 +454,22 @@ and infer_call env callee args pos =
               | E_closure c -> infer_closure env c (Some p)
               | _ -> infer env a
             in
-            if not (T.unify p got) then mismatch env pos p got "인자")
+            (* 먼저 unify한다. 결정 위치의 effect 변수는 여기서 인자의
+               effect로 묶인다 — 제약이 아니라 해소다. 그 뒤에 남는 차이만이
+               진짜 위반이다. *)
+            if not (T.unify p got) then mismatch env pos p got "인자";
+            match (T.resolve p, T.resolve got) with
+            | T.TFn pf, T.TFn gf ->
+                let missing =
+                  T.eff_missing ~declared:pf.eff ~performed:gf.eff
+                in
+                if missing <> [] then
+                  err env pos
+                    (Printf.sprintf
+                       "넘긴 함수가 %s을(를) 수행하는데 파라미터가 허용한 effect는 %s입니다"
+                       (String.concat ", " (List.map T.atom_show missing))
+                       (T.eff_show pf.eff))
+            | _ -> ())
           params args;
       ret
   | Some _ -> T.TUnknown
@@ -366,39 +481,79 @@ and ctor_fn env enum name =
       let sub = List.map (fun v -> (v, T.fresh ())) gen in
       let params =
         match List.assoc_opt name variants with
-        | Some ts -> List.map (T.subst sub) ts
+        | Some ts -> List.map (T.subst sub []) ts
         | None -> []
       in
-      T.TFn { affine = false; params; ret = T.TCon (enum, List.map snd sub) }
+      T.TFn
+        {
+          affine = false;
+          params;
+          eff = [];
+          ret = T.TCon (enum, List.map snd sub);
+        }
 
 and infer_field env obj name pos =
-  let t = infer env obj in
+  (* capability 메서드는 값을 통해서만 부를 수 있다. 타입 이름으로 부를 수 있으면
-  match T.resolve t with
+     capability 없이 effect를 수행하게 되어 보안 정리 (i)이 무너진다. *)
-  | T.TUnknown -> T.TUnknown
+  (match obj with
-  | T.TCon (cname, args) -> (
+  | E_ident (n, _) when lookup env n = None && Hashtbl.mem env.caps n ->
-      match Hashtbl.find_opt env.structs cname with
+      err env pos
-      | Some (gen, fields) -> (
+        (Printf.sprintf
-          let sub = List.map2 (fun v a -> (v, a)) gen (adjust gen args) in
+           "capability %s의 메서드는 값을 통해서만 부를 수 있습니다 (%s를 파라미터로 받아야 합니다)" n n)
-          match List.assoc_opt name fields with
+  | _ -> ());
-          | Some ft -> T.subst sub ft
+  match obj with
-          | None ->
+  | E_ident (a, _) when lookup env a = None && List.mem a env.aliases -> (
-              err env pos (Printf.sprintf "%s에 %s 필드가 없습니다" cname name);
+      (* 모듈 별칭을 통한 접근. 가져온 표면은 "Alias.name" 키로 들어와 있다. *)
-              T.TUnknown)
+      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
+          match Hashtbl.find_opt env.fns key with
-          | Some methods -> (
+          | Some s ->
-              match List.assoc_opt name methods with
+              let params, eff, ret = instantiate s in
-              | Some s ->
+              T.TFn { affine = false; params; eff; ret }
-                  let params, ret = instantiate s in
+          | None -> (
-                  T.TFn { affine = false; params; ret }
+              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
+                  err env pos (Printf.sprintf "%s에 %s 필드가 없습니다" cname name);
-                    (Printf.sprintf "capability %s에 %s 메서드가 없습니다" cname name);
                   T.TUnknown)
-          | None -> T.TUnknown))
+          | None -> (
-  | other ->
+              match Hashtbl.find_opt env.caps cname with
-      err env pos (Printf.sprintf "%s에는 필드가 없습니다" (T.show other));
+              | Some methods -> (
-      T.TUnknown
+                  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
@@ -428,8 +583,8 @@ and infer_inst env callee args pos =
                  (List.length s.s_gen) (List.length tys));
             T.TUnknown)
           else
-            let params, ret = instantiate_with s tys in
+            let params, eff, ret = instantiate_with s tys in
-            T.TFn { affine = false; params; ret })
+            T.TFn { affine = false; params; eff; ret })
   | _ -> T.TUnknown
 
 and check_pattern env (scrutinee : T.t) (p : pattern) =
@@ -448,7 +603,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)
@@ -466,7 +622,7 @@ and check_ctor env scrutinee enum name args pos =
       in
       if List.length fields = List.length args then
         List.iter2
-          (fun ft ap -> check_pattern env (T.subst sub ft) ap)
+          (fun ft ap -> check_pattern env (T.subst sub [] ft) ap)
           fields args
 
 (* ------------------------------------------------------------------ *)
@@ -527,13 +683,63 @@ let check_fn env (d : fn_decl) =
         match d.fn_ret with None -> T.TUnit | Some r -> conv env gen r
       in
       env.ret <- declared;
+      env.performed <- [];
+      env.saw_unknown <- false;
       let got = infer_block env body in
       if not (T.unify declared got) then
         mismatch env d.fn_pos declared got
           (Printf.sprintf "%s의 본문이 남기는 값" d.fn_name);
+      (* 미선언 effect = compile error (철학 1).
+         수행한 자리를 알고 있으므로 그 자리에 진단을 붙인다. *)
+      let declared_eff =
+        match d.fn_eff with None -> [] | Some atoms -> conv_eff_result atoms
+      in
+      List.iter
+        (fun (a, pos) ->
+          match T.eff_missing ~declared:declared_eff ~performed:[ a ] with
+          | [] -> ()
+          | missing ->
+              List.iter
+                (fun m ->
+                  err env pos
+                    (Printf.sprintf "선언되지 않은 effect %s (%s의 effects 절은 %s입니다)"
+                       (T.atom_show m) d.fn_name (T.eff_show declared_eff)))
+                missing)
+        (List.rev env.performed);
+      (* 과잉 선언도 오류다. 선언한 effect를 수행하지 않으면 호출자는 하지도
+         않는 일에 대한 의무를 진다 — 자기 effects 절을 넓히거나 capability를
+         받아오게 된다. 시그니처는 실제보다 좁아도 안 되고 넓어도 안 된다.
+
+         effect 변수가 있으면 판정하지 않는다. e에 무엇이 묶일지는 호출
+         지점이 정하고, 본문만 보고는 알 수 없다 — 모르는 것을 틀렸다고
+         말하지 않는다. *)
+      let has_var =
+        List.exists (function T.A_var _ -> true | _ -> false) declared_eff
+      in
+      if (not has_var) && not env.saw_unknown then
+        List.iter
+          (fun a ->
+            match a with
+            | T.A_name (cap, meth) ->
+                let performed = List.map fst env.performed |> T.eff_resolve in
+                if
+                  not
+                    (List.exists
+                       (function
+                         | T.A_name (c, m) -> c = cap && m = meth
+                         | T.A_var _ | T.A_meta _ -> true)
+                       performed)
+                then
+                  err env d.fn_pos
+                    (Printf.sprintf
+                       "%s은(는) %s을(를) 선언했지만 수행하지 않습니다 (effects 절에서 지우십시오)"
+                       d.fn_name (T.atom_show a))
+            | _ -> ())
+          declared_eff;
+      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;
@@ -542,8 +748,31 @@ 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 = [];
+      saw_unknown = false;
       errors = [];
     }
   in
@@ -559,7 +788,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 ->
@@ -583,7 +812,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 ->

lib/types.ml

@@ -1,11 +1,12 @@
-(* 타입 표현과 지역 unification.
+(* 타입과 effect 표현, 그리고 지역 unification.
 
    TUnknown이 핵심이다. 외부 모듈에서 오는 이름은 모듈 로딩이 없는 v0에서
    해소할 수 없다. 그런 타입은 TUnknown이 되고 무엇과도 맞는다 — 모르는 것을
-   틀렸다고 말하지 않기 위해서다. 아는 범위에서만 검사한다.
+   틀렸다고 말하지 않기 위해서다.
 
-   TMeta는 호출 지점에서 제네릭을 인스턴스화할 때 생기는 미지수다. 함수 하나
+   effect는 순서 없는 집합이고 합성은 합집합이다. 변수는 집합 변수이며,
-   범위에서만 살고 전역으로 흐르지 않는다 (철학 2: 전역 추론 없음). *)
+   호출 지점에서 결정 위치(파라미터의 effect 자리에 단독으로 선 변수)를 통해
+   메타에 묶인다. 함수 하나 범위를 넘지 않는다. *)
 
 type t =
   | TUnknown
@@ -15,20 +16,84 @@ type t =
   | TUnit
   | TVar of string
   | TCon of string * t list
-  | TFn of { affine : bool; params : t list; ret : t }
+  | TFn of { affine : bool; params : t list; eff : eff; ret : t }
   | TMeta of meta ref
 
 and meta = Unbound of int | Bound of t
 
+(* effect 집합. 원소는 구체 이름, 집합 변수, 또는 호출 지점의 미지수다. *)
+and eff = atom list
+
+and atom =
+  | A_name of string * string (* Cap.method *)
+  | A_var of string
+  | A_meta of emeta ref
+
+and emeta = EUnbound of int | EBound of eff
+
 let counter = ref 0
 
 let fresh () =
   incr counter;
   TMeta (ref (Unbound !counter))
 
+let fresh_eff () =
+  incr counter;
+  [ A_meta (ref (EUnbound !counter)) ]
+
 let rec resolve t =
   match t with TMeta { contents = Bound u } -> resolve u | _ -> t
 
+(* 묶인 메타를 펼치고 중복을 없앤다. 집합이므로 순서는 의미가 없다. *)
+let rec eff_resolve (e : eff) : eff =
+  let expand a =
+    match a with
+    | A_meta { contents = EBound inner } -> eff_resolve inner
+    | _ -> [ a ]
+  in
+  let flat = List.concat_map expand e in
+  let mem a acc =
+    List.exists
+      (fun b ->
+        match (a, b) with
+        | A_name (c1, m1), A_name (c2, m2) -> c1 = c2 && m1 = m2
+        | A_var x, A_var y -> x = y
+        | A_meta r, A_meta r' -> r == r'
+        | _ -> false)
+      acc
+  in
+  List.fold_left (fun acc a -> if mem a acc then acc else a :: acc) [] flat
+  |> List.rev
+
+let atom_show = function
+  | A_name (c, m) -> c ^ "." ^ m
+  | A_var v -> v
+  | A_meta { contents = EUnbound n } -> Printf.sprintf "_e%d" n
+  | A_meta { contents = EBound _ } -> "?"
+
+let eff_show e =
+  match eff_resolve e with
+  | [] -> "{}"
+  | atoms -> "{" ^ String.concat ", " (List.map atom_show atoms) ^ "}"
+
+let atom_eq a b =
+  match (a, b) with
+  | A_name (c1, m1), A_name (c2, m2) -> c1 = c2 && m1 = m2
+  | A_var x, A_var y -> x = y
+  | A_meta r, A_meta r' -> r == r'
+  | _ -> false
+
+(* declared가 덮지 못하는 원소들. 미지수는 판정을 미룬다 —
+   결정되지 않은 것을 위반이라고 말하지 않는다. *)
+let eff_missing ~declared ~performed =
+  let declared = eff_resolve declared in
+  List.filter
+    (fun a ->
+      match a with
+      | A_meta { contents = EUnbound _ } -> false
+      | _ -> not (List.exists (atom_eq a) declared))
+    (eff_resolve performed)
+
 let rec show t =
   match resolve t with
   | TUnknown -> "?"
@@ -39,10 +104,11 @@ let rec show t =
   | TVar v -> v
   | TCon (n, []) -> n
   | TCon (n, args) -> n ^ "[" ^ String.concat ", " (List.map show args) ^ "]"
-  | TFn { affine; params; ret } -> (
+  | TFn { affine; params; eff; ret } -> (
       (if affine then "affine fn(" else "fn(")
       ^ String.concat ", " (List.map show params)
       ^ ")"
+      ^ (match eff_resolve eff with [] -> "" | e -> " effects " ^ eff_show e)
       ^ match resolve ret with TUnit -> "" | r -> " -> " ^ show r)
   | TMeta { contents = Unbound n } -> Printf.sprintf "_%d" n
   | TMeta { contents = Bound _ } -> "?"
@@ -54,8 +120,19 @@ let rec occurs r t =
   | TFn { params; ret; _ } -> List.exists (occurs r) params || occurs r ret
   | _ -> false
 
-(* 성공하면 true. 실패해도 예외를 던지지 않는다 — 호출자가 위치를 알고
+(* 결정 위치의 해소: 파라미터의 effect 자리에 단독으로 선 미지수만 묶는다.
-   진단을 만든다. *)
+   그 외에는 참을 돌려주고, 실제 포함 검사는 호출 지점에서 방향을 아는
+   쪽이 한다 (진단 품질 때문에). *)
+let unify_eff a b =
+  match (eff_resolve a, eff_resolve b) with
+  | [ A_meta ({ contents = EUnbound _ } as r) ], other ->
+      r := EBound other;
+      true
+  | other, [ A_meta ({ contents = EUnbound _ } as r) ] ->
+      r := EBound other;
+      true
+  | _ -> true
+
 let rec unify a b =
   match (resolve a, resolve b) with
   | TUnknown, _ | _, TUnknown -> true
@@ -75,19 +152,30 @@ let rec unify a b =
          소유한다. 여기서 섞으면 두 검사가 서로의 결론을 앞질러 버린다. *)
       List.length f.params = List.length g.params
       && List.for_all2 unify f.params g.params
-      && unify f.ret g.ret
+      && unify_eff f.eff g.eff && unify f.ret g.ret
   | _ -> false
 
-(* 제네릭 인스턴스화: TVar를 주어진 대입으로 바꾼다 *)
+(* 제네릭 인스턴스화: 타입 변수와 effect 변수를 동시에 바꾼다 *)
-let rec subst env t =
+let rec subst tenv eenv t =
   match resolve t with
-  | TVar v -> ( match List.assoc_opt v env with Some u -> u | None -> TVar v)
+  | TVar v -> ( match List.assoc_opt v tenv with Some u -> u | None -> TVar v)
-  | TCon (n, args) -> TCon (n, List.map (subst env) args)
+  | TCon (n, args) -> TCon (n, List.map (subst tenv eenv) args)
   | TFn f ->
       TFn
         {
           affine = f.affine;
-          params = List.map (subst env) f.params;
+          params = List.map (subst tenv eenv) f.params;
-          ret = subst env f.ret;
+          eff = subst_eff eenv f.eff;
+          ret = subst tenv eenv f.ret;
         }
   | u -> u
+
+and subst_eff eenv (e : eff) : eff =
+  eff_resolve
+    (List.concat_map
+       (fun a ->
+         match a with
+         | A_var v -> (
+             match List.assoc_opt v eenv with Some s -> s | None -> [ a ])
+         | _ -> [ a ])
+       e)

samples/01_capability_signature.cool

@@ -43,12 +43,15 @@ pub fn checkout(
 }
 
 // 빌린 값을 다른 빌림 자리로 넘기는 것은 허용된다 (복제가 아니다).
+//
+// each가 아니라 map인 이유: 결과를 버릴 방법이 언어에 없다. each는 값을
+// 남기지 않는 클로저만 받으므로 Result를 삼킬 수 없고, ?는 클로저 밖으로
+// 나가지 못한다. 실패를 못 본 척하려면 명시적으로 match해야 한다.
 pub fn refund_all(
     pay: PaymentGateway,
     ids: List[OrderId],
-) effects {PaymentGateway.refund} -> Result[Unit, PayError] {
+) effects {PaymentGateway.refund} -> List[Result[Receipt, PayError]] {
-    List.each(ids, fn(id) {
+    List.map(ids, fn(id) {
-        refund_order(pay, id)?
+        refund_order(pay, id)
-        Ok(unit)
     })
 }

samples/05_move_errors.cool

@@ -1,26 +1,38 @@
-// 05. 컴파일 에러가 나야 하는 코드
+// 05. move / affinity 검사기가 거부해야 하는 코드
 //
-// 각 함수는 주석에 적힌 진단 하나를 정확히 내야 한다.
+// 09, 10과 같은 이유로 외부 타입이 하나도 없다. affinity의 뿌리는 capability라
-// 체커가 생기면 그대로 테스트 케이스가 된다.
+// 자원 타입을 이 파일에서 정의해야 검사기가 affine임을 알 수 있다.
+// 외부 타입은 affine임을 증명할 수 없으므로 copyable로 취급된다.
 
-// close는 파일을 소비한다: own 유표기
+pub capability File {
+    fn size() -> Int
+}
+
+pub capability Gateway {
+    fn refund(id: Int) effects {Gateway.refund}
+}
+
+pub capability Registry {
+    fn add(h: fn()) effects {Registry.add}
+}
+
+// 파일을 소비하는 함수: own 유표기
 pub fn close(own f: File) effects {File.close}
 
-// [E-move-after-move] affine 값의 이중 소비
+// 빌리기만 하는 함수: 무표기
-pub fn double_close(own f: File) effects {File.close} {
+pub fn size_of(f: File) -> Int {
+    f.size()
+}
+
+// --- 통과해야 하는 것 ---
+
+pub fn use_then_close(own f: File) effects {File.close} -> Int {
+    let n = size_of(f)
     close(f)
-    close(f)        // ERROR: f는 이미 move됨 (앞줄에서 소비)
+    n
 }
 
-// [E-move-join] 분기 병합은 보수적 합집합
+// 양쪽 분기에서 소비하면 통과한다
-pub fn conditional_close(own f: File, c: Bool) effects {File.close} {
-    if c {
-        close(f)
-    }
-    close(f)        // ERROR: f는 이 분기에서 move됨 (조건부 소비)
-}
-
-// 정당한 형태 — 양쪽 분기에서 소비하면 통과해야 한다.
 pub fn both_branches_close(own f: File, c: Bool) effects {File.close} {
     if c {
         close(f)
@@ -29,48 +41,75 @@ pub fn both_branches_close(own f: File, c: Bool) effects {File.close} {
     }
 }
 
+// 빌린 값을 다른 빌림 자리로 넘기는 것은 복제가 아니다
+pub fn borrow_twice(f: File) -> Int {
+    size_of(f) + size_of(f)
+}
+
+// affine 값을 capture한 클로저는 affine fn이다
+pub fn deferred_close(own f: File) -> affine fn() effects {File.close} {
+    fn() { close(f) }
+}
+
+// --- 여기서부터 전부 오류다 ---
+
+// [E-move-after-move] affine 값의 이중 소비
+pub fn double_close(own f: File) effects {File.close} {
+    close(f)
+    close(f)
+}
+
+// [E-move-join] 분기 병합은 보수적 합집합
+pub fn conditional_close(own f: File, c: Bool) effects {File.close} {
+    if c {
+        close(f)
+    }
+    close(f)
+}
+
 // [E-use-escape] 빌린 값의 반환
-pub fn leak_capability(pay: PaymentGateway) -> PaymentGateway {
+pub fn leak_capability(pay: Gateway) -> Gateway {
-    pay             // ERROR: 빌린 값은 반환할 수 없음 (own이 아니다)
+    pay
 }
 
 // [E-use-escape] 빌린 값의 저장
 pub struct Holder {
-    pay: PaymentGateway,
+    pay: Gateway,
 }
 
-pub fn store_capability(pay: PaymentGateway) -> Holder {
+pub fn store_capability(pay: Gateway) -> Holder {
-    Holder { pay: pay }   // ERROR: 빌린 값은 struct에 저장할 수 없음
+    Holder { pay: pay }
 }
 
-// [E-use-escape] 빌린 값을 capture한 클로저를 own 자리에 전달
+// [E-use-escape] 빌린 값을 다른 함수에 소유로 넘긴다
-pub fn register(own handler: fn()) effects {Registry.add}
+pub fn give_away(f: File) effects {File.close} {
+    close(f)
+}
 
-pub fn escape_via_closure(pay: PaymentGateway) effects {Registry.add} {
+// [E-use-escape] 빌린 값을 capture한 클로저를 own 자리에 넘긴다
-    register(fn() { pay.refund(OrderId(1)) })
+pub fn register(own h: fn() effects {Gateway.refund}) effects {Registry.add}
-    // ERROR: pay를 capture한 클로저는 빌린 값이며 own 자리에 전달할 수 없음
+
+pub fn escape_via_closure(pay: Gateway) effects {Registry.add} {
+    register(fn() { pay.refund(1) })
 }
 
 // [E-affinity-transitive] affine 필드를 가진 타입을 copyable로 선언
 pub copyable struct Box {
-    f: File,        // ERROR: affine 필드(File)와 copyable 선언은 공존할 수 없음
+    f: File,
 }
 
-// [E-callable-affinity] affine 값을 capture한 클로저를 fn 위치에 대입
+// [E-callable-affinity] affine 값을 capture한 클로저를 fn 위치에 반환
 pub fn misuse_affine_closure(own f: File) -> fn() effects {File.close} {
     fn() { close(f) }
-    // ERROR: f를 capture했으므로 타입은 affine fn()이며 fn() 위치에 대입할 수 없음
 }
 
-// [E-spawn-capture] spawn 클로저의 mutable capture
+// [E-closure-mut-capture] 클로저는 mut 바인딩을 capture할 수 없다
-pub fn spawn_mutable(sc: TaskScope, mut counter: Int) effects {TaskScope.spawn} {
+pub fn capture_mut(own f: File, pay: Gateway)
-    scope s = sc {
+    effects {File.close, Registry.add, Gateway.refund} {
-        sc.spawn(fn() { counter = counter + 1 })
+    let mut counter = 0
-        // ERROR: spawn 클로저는 mutable 참조를 capture할 수 없음
+    register(fn() {
-    }
+        counter = counter + 1
-}
+        pay.refund(counter)
-
+    })
-// [E-effect-undeclared] 선언되지 않은 effect
+    close(f)
-pub fn silent_write(log: Logger) {
-    log.write("hi")   // ERROR: effect Logger.write가 시그니처에 선언되지 않음
 }

samples/08_syntax_errors.cool

@@ -2,7 +2,9 @@
 //
 // 05와 목적이 다르다. 05는 구문은 맞지만 검사기가 거부해야 하는 파일이고,
 // 이 파일은 파서가 거부해야 하는 파일이다.
-// 아직 오류 복구가 없으므로 파서는 첫 오류에서 멈춘다 — 한 번에 하나씩 확인한다.
+// 파서는 항목 단위로 회복한다. 오류가 난 선언은 통째로 버리고 다음 선언에서
+// 다시 시작하므로, 한 항목에 오류 하나가 상한이다. 이 파일은 항목마다 하나씩
+// 심어 회복이 실제로 되는지 본다 — 아래 넷이 모두 보고되어야 한다.
 
 // [E-syntax-effect-union] 파라미터 위치의 합집합은 문법에 존재하지 않는다.
 // 검사기가 아니라 파서가 거부한다 (eff_param 프로덕션에 "|"가 없다).
@@ -19,3 +21,25 @@ pub fn classify(e: PayError) -> String {
         _ => "other",
     }
 }
+
+// [E-syntax-trailing-comma] 다중 줄 목록에는 후행 콤마가 필요하다.
+// 줄바꿈이 목록을 닫으려 하면 원인을 직접 말한다.
+pub fn missing_comma(
+    a: Int,
+    b: Int
+) -> Int
+// ERROR (parse): 다중 줄 목록에는 후행 콤마가 필요합니다
+
+// [E-syntax-scope-parent] 자식 scope는 부모를 명시해야 한다.
+// 부모 없는 작업이 생기지 않게 하는 것은 문법의 일이다.
+pub fn orphan(root: TaskScope) {
+    scope sc {
+        sc.spawn(fn() { })
+    }
+}
+// ERROR (parse): = (자식 scope의 부모를 명시해야 합니다)
+
+// 회복이 되었다는 증거: 이 마지막 선언은 정상적으로 읽혀야 한다.
+pub fn fine(n: Int) -> Int {
+    n + 1
+}

samples/10_effect_errors.cool

@@ -0,0 +1,86 @@
+// 10. effect 검사기가 거부해야 하는 코드
+//
+// 09와 같은 이유로 외부 타입이 하나도 없다. capability를 이 파일에서 정의해야
+// 메서드의 effect가 알려지고, 검사기가 실제로 판정할 수 있다.
+
+pub capability Db {
+    fn read(id: Int) effects {Db.read} -> Int
+    fn write(id: Int, v: Int) effects {Db.write}
+}
+
+pub capability Log {
+    fn write(msg: String) effects {Log.write}
+}
+
+// --- 통과해야 하는 것 ---
+
+pub fn get(db: Db, id: Int) effects {Db.read} -> Int {
+    db.read(id)
+}
+
+pub fn copy(db: Db, from: Int, to: Int) effects {Db.read, Db.write} {
+    db.write(to, db.read(from))
+}
+
+// 헬퍼를 부르면 헬퍼의 effect를 물려받는다
+pub fn get_twice(db: Db, id: Int) effects {Db.read} -> Int {
+    get(db, id) + get(db, id)
+}
+
+// effect 변수: 결정 위치의 변수가 인자의 effect로 묶인다
+pub fn twice[e: effects](f: fn() effects e) effects e {
+    f()
+    f()
+}
+
+pub fn log_twice(log: Log) effects {Log.write} {
+    twice(fn() { log.write("hi") })
+}
+
+// effect 없는 함수는 effects 절이 없다
+pub fn pure_add(a: Int, b: Int) -> Int {
+    a + b
+}
+
+// --- 여기서부터 전부 오류다 ---
+
+// [E-effect-undeclared] 선언 없이 capability 메서드를 부른다
+pub fn silent_read(db: Db) -> Int {
+    db.read(1)
+}
+
+// [E-effect-undeclared] 일부만 선언했다
+pub fn partial(db: Db, id: Int) effects {Db.read} {
+    db.write(id, db.read(id))
+}
+
+// [E-effect-undeclared] 헬퍼가 수행하는 effect도 물려받아야 한다
+pub fn via_helper(db: Db, id: Int) -> Int {
+    get(db, id)
+}
+
+// [E-effect-undeclared] 클로저를 통해 새어 나오는 effect
+pub fn via_closure(log: Log) {
+    twice(fn() { log.write("hi") })
+}
+
+// [E-effect-closure-annotated] 클로저가 선언한 것보다 많이 수행한다
+pub fn closure_lies(log: Log) effects {Log.write} {
+    twice(fn() effects {} { log.write("hi") })
+}
+
+// [E-effect-param] 파라미터가 허용한 effect를 넘는 함수를 넘긴다
+pub fn takes_pure(f: fn() effects {}) {
+    f()
+}
+
+pub fn pass_impure(log: Log) effects {Log.write} {
+    takes_pure(fn() { log.write("hi") })
+}
+
+// [E-capability-static] capability 메서드를 타입 이름으로 부른다.
+// 이것이 허용되면 capability 없이 effect를 수행할 수 있게 되어
+// "capability 없이는 effect를 수행할 수 없다"는 정리가 무너진다.
+pub fn no_instance() effects {Db.read} -> Int {
+    Db.read(1)
+}

samples/11_exhaustiveness.cool

@@ -0,0 +1,108 @@
+// 11. exhaustiveness 검사기가 거부해야 하는 코드
+//
+// 철학 1의 대표 항목이자, interface hash가 enum 정의 본문을 입력으로 삼는 이유다.
+// upstream에 variant가 하나 늘면 downstream의 match가 깨져야 하는데,
+// 이 검사가 없으면 깨질 것이 없다.
+
+pub enum Shape {
+    Circle(Int),
+    Rect(Int, Int),
+    Point,
+}
+
+// --- 통과해야 하는 것 ---
+
+pub fn area(s: Shape) -> Int {
+    match s {
+        Circle(r) => r * r,
+        Rect(w, h) => w * h,
+        Point => 0,
+    }
+}
+
+pub fn with_wildcard(s: Shape) -> Int {
+    match s {
+        Circle(r) => r,
+        _ => 0,
+    }
+}
+
+pub fn nested_full(o: Option[Shape]) -> Int {
+    match o {
+        Some(Circle(r)) => r,
+        Some(Rect(w, h)) => w * h,
+        Some(Point) => 0,
+        None => 0,
+    }
+}
+
+pub fn results(r: Result[Int, Int]) -> Int {
+    match r {
+        Ok(n) => n,
+        Err(e) => e,
+    }
+}
+
+pub fn flags(b: Bool) -> Int {
+    match b {
+        true => 1,
+        false => 0,
+    }
+}
+
+// --- 여기서부터 전부 오류다 ---
+
+// [E-match-missing] variant 하나가 빠졌다
+pub fn missing_variant(s: Shape) -> Int {
+    match s {
+        Circle(r) => r,
+        Rect(w, h) => w * h,
+    }
+}
+
+// [E-match-missing] Bool도 생성자 집합이 유한하다
+pub fn missing_false(b: Bool) -> Int {
+    match b {
+        true => 1,
+    }
+}
+
+// [E-match-missing] Option
+pub fn missing_none(o: Option[Int]) -> Int {
+    match o {
+        Some(n) => n,
+    }
+}
+
+// [E-match-missing] 중첩된 자리에서 빠진 경우도 찾는다
+pub fn missing_nested(o: Option[Shape]) -> Int {
+    match o {
+        Some(Circle(r)) => r,
+        None => 0,
+    }
+}
+
+// [E-match-missing] Int 리터럴은 생성자 집합이 무한하다
+pub fn missing_literal(n: Int) -> Int {
+    match n {
+        0 => 1,
+        1 => 2,
+    }
+}
+
+// [E-match-unreachable] 앞의 와일드카드에 가린다
+pub fn shadowed(s: Shape) -> Int {
+    match s {
+        _ => 0,
+        Point => 1,
+    }
+}
+
+// [E-match-unreachable] 같은 생성자가 두 번
+pub fn duplicated(s: Shape) -> Int {
+    match s {
+        Circle(r) => r,
+        Circle(x) => x,
+        _ => 0,
+    }
+}

samples/12_stdlib_effects.cool

@@ -0,0 +1,33 @@
+// 12. 표준 라이브러리 시그니처가 실제로 검사된다
+//
+// std가 생기기 전에는 List.each가 모르는 이름이라 조용히 통과했다.
+// "모르는 것을 틀렸다고 말하지 않는다"는 맞는 원칙이지만, 그 그늘에
+// 검사되지 않는 영역이 숨어 있었다. 이제 그늘이 없다.
+//
+// 이 파일은 세 가지 오류를 낸다.
+
+import "cool.dev/std/list" as List
+import "cool.dev/std/int" as Int
+
+pub capability Console {
+    fn print(s: String) effects {Console.print}
+}
+
+// (1) effect 다형성. e는 클로저의 시그니처에서 {Console.print}로 묶이고,
+//     그것이 이 함수의 effects 절 {}를 넘는다. effect 변수가 호출 지점에서
+//     실제로 해소된다는 증거다 — 이게 안 걸리면 규칙이 장식이다.
+pub fn leaks_effect(c: Console, xs: List[Int]) {
+    List.each(xs, fn(n) {
+        c.print(Int.show(n))
+    })
+}
+
+// (2) 인자 개수
+pub fn wrong_arity(xs: List[Int]) -> Int {
+    List.len(xs, 1)
+}
+
+// (3) 반환 타입
+pub fn wrong_type(xs: List[Int]) -> String {
+    List.len(xs)
+}

samples/13_lints.cool

@@ -0,0 +1,35 @@
+// 13. 두 lint — 미사용 import와 effect 과잉 선언
+//
+// 둘 다 취향 문제가 아니라 비용 문제다.
+//
+// 미사용 import: 쓰지도 않는 모듈의 시그니처가 바뀌면 이 모듈이 재검사된다.
+// 증분 루프의 비용을 아무 이유 없이 넓히는 선언이다.
+//
+// effect 과잉 선언: 선언한 effect를 수행하지 않으면 호출자는 하지도 않는
+// 일에 대한 의무를 진다 — 자기 effects 절을 넓히거나 capability를 받아온다.
+// 시그니처는 실제보다 좁아도 안 되고 넓어도 안 된다.
+
+import "cool.dev/std/list" as List
+// ERROR: List을(를) 가져왔지만 쓰지 않습니다
+
+pub capability Db {
+    fn read(id: Int) effects {Db.read} -> Int
+    fn write(id: Int) effects {Db.write}
+}
+
+// Db.write는 선언만 하고 수행하지 않는다.
+pub fn only_reads(db: Db, id: Int) effects {Db.read, Db.write} -> Int {
+    db.read(id)
+}
+// ERROR: only_reads은(는) Db.write을(를) 선언했지만 수행하지 않습니다
+
+// 정확히 선언하면 통과한다.
+pub fn honest(db: Db, id: Int) effects {Db.read} -> Int {
+    db.read(id)
+}
+
+// effect 변수가 있으면 판정하지 않는다. e에 무엇이 묶일지는 호출 지점이
+// 정하고, 본문만 보고는 알 수 없다 — 모르는 것을 틀렸다고 말하지 않는다.
+pub fn polymorphic[e: effects](f: fn() effects e) effects e {
+    f()
+}

samples/README.md

@@ -12,19 +12,44 @@
 | 02_higher_order_effects | effect 변수, 구문 수준 제한, 명시적 인스턴스화 |
 | 03_scope_concurrency | TaskScope, 이름 있는 scope, 중첩 시 수명 표현 |
 | 04_enum_match_interface | enum 정의 본문이 interface surface에 들어가는 경로 |
-| 05_move_errors | **에러가 나야 하는** 코드 — 진단 하나씩 |
+| 05_move_errors | **move/affinity 검사기가** 거부해야 하는 코드 (자원을 직접 정의) |
 | 06_affine_closure | callable affinity (fn vs affine fn), own과의 직교성 |
 | 07_module_interface | interface artifact가 담아야 할 것 전부 |
 | 08_syntax_errors | **파서가** 거부해야 하는 코드 |
 | 09_type_errors | **타입 검사기가** 거부해야 하는 코드 (외부 타입 0개) |
+| 10_effect_errors | **effect 검사기가** 거부해야 하는 코드 (capability를 직접 정의) |
+| 11_exhaustiveness | **exhaustiveness 검사기가** 거부해야 하는 코드 |
 
-05, 08, 09는 통과하면 안 되는 파일이다. 각 함수 주석의 `[E-...]` 태그가 기대
+05, 08, 09, 10은 통과하면 안 되는 파일이다. 각 함수 주석의 `[E-...]` 태그가
-진단이며, 셋의 목적이 다르다 — **08은 파서가, 09는 타입 검사기가, 05는 아직
+기대 진단이며, 넷의 목적이 다르다 — **08은 파서가, 09는 타입 검사기가,
-없는 move/affinity 검사가** 거부해야 한다. 단계별로 파일을 나눈 이유는
+10은 effect 검사기가, 05는 move/affinity 검사가** 거부해야 한다. 단계별로
-앞 단계가 첫 오류에서 멈추면 뒤 단계 케이스에 영영 도달하지 못하기 때문이다.
+파일을 나눈 이유는 앞 단계가 첫 오류에서 멈추면 뒤 단계 케이스에 영영
+도달하지 못하기 때문이다.
 
-09에는 외부 타입이 하나도 없다. 전부 모듈 안에서 정의되므로 검사기가
+05, 09, 10에는 외부 타입이 하나도 없다. 전부 모듈 안에서 정의되므로 검사기가
-TUnknown으로 빠져나갈 구석이 없다 — 검사기에 이빨이 있는지 보는 파일이다.
+빠져나갈 구석이 없다 — 검사기에 이빨이 있는지 보는 파일들이다. 10은
+capability를 직접 정의해야 메서드의 effect가 알려지고, 05는 affinity의 뿌리가
+capability라 자원 타입을 정의해야 affine임이 유도된다.
+
+13은 두 lint다. 미사용 import는 재검사 범위를 넓히고, effect 과잉 선언은
+호출자에게 없는 의무를 지운다 — 둘 다 취향이 아니라 비용이다. 미사용
+import는 lint이므로 뒤 단계를 막지 않는다: 같은 파일의 타입 오류가 함께
+보고된다.
+
+12는 표준 라이브러리가 생긴 뒤에야 가능해진 파일이다. std가 없을 때는
+`List.each`가 모르는 이름이라 조용히 통과했다 — "모르는 것을 틀렸다고 말하지
+않는다"는 맞는 원칙이지만 그 그늘에 검사되지 않는 영역이 있었다.
+
+01~04, 06, 07은 `coolc check`를 통과한다 (exit 0).
+
+`modules/`는 모듈 경계다. `coolc check modules/area.cool`이 import를 따라
+shapes를 먼저 검사하고, `coolc iface modules/shapes.cool`이 downstream이
+보는 표면과 그 해시를 보여준다.
+
+`run/`은 실제로 돈다. `coolc run run/hello.cool`. 이 파일들은 검사를
+통과한다가 아니라 무엇을 출력하는지까지 말한다 — 기대 출력이 주석에 있고
+같은 것을 test/가 검사한다. main이 선언한 capability만 런타임이 넘기므로,
+파라미터에서 Console을 지우면 출력할 방법이 프로그램 안에 없다.
 
 파서는 첫 오류에서 멈춘다(오류 복구 미구현). 타입 검사기는 오류를 전부 모은다.
 

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,
+    }
+}

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
+}

samples/run/control.cool

@@ -0,0 +1,57 @@
+// 실행 의미를 한 파일에 모은 것: ?, mut, struct, match, scope.
+//
+// 기대 출력:
+//   7
+//   6
+//   err
+//   in scope
+
+import "cool.dev/std/int" as Int
+
+pub capability Console {
+    fn print(s: String) effects {Console.print}
+}
+
+pub enum E {
+    Bad,
+}
+
+pub copyable struct P {
+    x: Int,
+    y: Int,
+}
+
+pub fn half(n: Int) -> Result[Int, E] {
+    if n % 2 == 0 {
+        Ok(n / 2)
+    } else {
+        Err(Bad)
+    }
+}
+
+pub fn twice(n: Int) -> Result[Int, E] {
+    let a = half(n)?
+    let b = half(a)?
+    Ok(a + b)
+}
+
+pub fn show_res(r: Result[Int, E]) -> String {
+    match r {
+        Ok(v) => Int.show(v),
+        Err(_) => "err",
+    }
+}
+
+pub fn main(c: Console, root: TaskScope) effects {Console.print} {
+    let mut total = 0
+    let p = P { x: 3, y: 4 }
+    total = total + p.x + p.y
+    c.print(Int.show(total))
+    c.print(show_res(twice(8)))
+    c.print(show_res(twice(7)))
+    scope sc = root {
+        sc.spawn(fn() {
+            c.print("in scope")
+        })
+    }
+}

samples/run/hello.cool

@@ -0,0 +1,40 @@
+// 실행되는 첫 프로그램.
+//
+// main은 자기가 선언한 capability만 받는다. Console을 파라미터에서 지우면
+// print할 방법이 프로그램 안에 없다 — ambient authority가 없다는 것의
+// 실행 시점 의미다.
+//
+// 표준 라이브러리도 명시적으로 가져온다. prelude가 없다 —
+// 암묵적으로 끌어오지 않는다는 규칙에 예외를 두지 않는다.
+//
+// 기대 출력:
+//   area = 12
+//   area = 9
+//   area = 3
+
+import "cool.dev/std/list" as List
+import "cool.dev/std/string" as String
+import "cool.dev/std/int" as Int
+
+pub capability Console {
+    fn print(s: String) effects {Console.print}
+}
+
+pub enum Shape {
+    Circle(Int),
+    Square(Int),
+}
+
+pub fn area(s: Shape) -> Int {
+    match s {
+        Circle(r) => r * r * 3,
+        Square(w) => w * w,
+    }
+}
+
+pub fn main(c: Console) effects {Console.print} {
+    let shapes = [Circle(2), Square(3), Circle(1)]
+    List.each(shapes, fn(s) {
+        c.print(String.concat("area = ", Int.show(area(s))))
+    })
+}

std/bool.cool

@@ -0,0 +1,3 @@
+// 표준 라이브러리: 불리언.
+
+pub fn show(b: Bool) -> String

std/int.cool

@@ -0,0 +1,4 @@
+// 표준 라이브러리: 정수.
+
+pub fn show(n: Int) -> String
+pub fn abs(n: Int) -> Int

std/list.cool

@@ -0,0 +1,21 @@
+// 표준 라이브러리: 리스트.
+//
+// 본문이 없다. 런타임이 구현하고, 이 파일은 그 계약을 말한다.
+// 그래서 이 파일은 구현이 아니라 시험대다 — effect 다형성이 실제로 쓸 만한지가
+// 여기서 결정된다. each와 map이 effect 변수 하나로 표현되지 않으면 규칙이
+// 틀린 것이고, 그건 v1로 미룰 수 없는 발견이다.
+//
+// e는 파라미터의 effect 슬롯에 홀로 나타난다 (결정 위치). 호출 지점에서
+// 인자의 시그니처를 읽어 묶인다 — 추론이 아니라 읽기다.
+
+pub fn len[a](xs: List[a]) -> Int
+
+pub fn each[a, e: effects](
+    xs: List[a],
+    f: fn(a) effects e,
+) effects e
+
+pub fn map[a, b, e: effects](
+    xs: List[a],
+    f: fn(a) effects e -> b,
+) effects e -> List[b]

std/string.cool

@@ -0,0 +1,4 @@
+// 표준 라이브러리: 문자열.
+
+pub fn len(s: String) -> Int
+pub fn concat(a: String, b: String) -> String

test/dune

@@ -2,4 +2,5 @@
  (name test_coollang)
  (libraries coollang)
  (deps
-  (glob_files %{workspace_root}/samples/*.cool)))
+  (glob_files %{workspace_root}/samples/*.cool)
+  (glob_files %{workspace_root}/std/*.cool)))

test/test_coollang.ml

@@ -453,14 +453,17 @@ let () =
   check "effect 집합의 capability도 표면에 든다"
     (resolve_ext "fn f() effects {Gw.pay}" = [ "Gw" ])
 
-(* --- 샘플: 01~07은 이름 해소를 통과해야 한다 --- *)
+(* --- 샘플: 오류 샘플을 뺀 나머지는 이름 해소를 통과해야 한다 --- *)
+
+(* 일부러 틀린 파일들. 무엇이 틀렸는지는 각 파일의 주석에 있다. *)
+let error_samples = [ "08_syntax_errors.cool"; "13_lints.cool" ]
 
 let () =
   let dir = "../samples" in
   let files =
     Sys.readdir dir |> Array.to_list
     |> List.filter (fun f -> Filename.check_suffix f ".cool")
-    |> List.filter (fun f -> f <> "08_syntax_errors.cool")
+    |> List.filter (fun f -> not (List.mem f error_samples))
     |> List.sort compare
   in
   List.iter
@@ -580,7 +583,17 @@ let () =
     Sys.readdir dir |> Array.to_list
     |> List.filter (fun f -> Filename.check_suffix f ".cool")
     |> List.filter (fun f ->
-        f <> "08_syntax_errors.cool" && f <> "09_type_errors.cool")
+        not
+          (List.mem f
+             [
+               "05_move_errors.cool";
+               "08_syntax_errors.cool";
+               "09_type_errors.cool";
+               "10_effect_errors.cool";
+               "11_exhaustiveness.cool";
+               "12_stdlib_effects.cool";
+               "13_lints.cool";
+             ]))
     |> List.sort compare
   in
   List.iter
@@ -593,7 +606,629 @@ let () =
             errors;
           check (f ^ " 타입 검사") false)
     ok_files;
-  match Driver.typecheck (Filename.concat dir "09_type_errors.cool") with
+  (match Driver.typecheck (Filename.concat dir "09_type_errors.cool") with
   | Ok () -> check "09는 타입 오류를 내야 한다" false
   | Error errors ->
-      check "09의 오류를 전부 모은다 (첫 오류에서 멈추지 않는다)" (List.length errors >= 18)
+      check "09의 오류를 전부 모은다 (첫 오류에서 멈추지 않는다)" (List.length errors >= 18));
+  (match Driver.typecheck (Filename.concat dir "10_effect_errors.cool") with
+  | Ok () -> check "10은 effect 오류를 내야 한다" false
+  | Error errors -> check "10의 effect 오류" (List.length errors >= 6));
+  (match Driver.typecheck (Filename.concat dir "05_move_errors.cool") with
+  | Ok () -> check "05는 move 오류를 내야 한다" false
+  | Error errors -> check "05의 move 오류" (List.length errors >= 9));
+  match Driver.typecheck (Filename.concat dir "11_exhaustiveness.cool") with
+  | Ok () -> check "11은 exhaustiveness 오류를 내야 한다" false
+  | Error errors -> check "11의 exhaustiveness 오류" (List.length errors >= 7)
+
+(* ================================================================== *)
+(* effect / capability 검사                                            *)
+(* ================================================================== *)
+
+let cap =
+  "capability Db {\n\
+  \  fn read(id: Int) effects {Db.read} -> Int\n\
+  \  fn touch(id: Int) effects {Db.read}\n\
+   }\n"
+
+(* --- 미선언 effect = compile error (철학 1) --- *)
+
+let () =
+  check "선언하면 통과"
+    (type_ok (cap ^ "fn f(db: Db) effects {Db.read} -> Int {\n  db.read(1)\n}"));
+  check "선언 없이 capability 메서드를 부르면 오류"
+    (type_has
+       (cap ^ "fn f(db: Db) -> Int {\n  db.read(1)\n}")
+       "선언되지 않은 effect Db.read");
+  check "헬퍼의 effect도 물려받는다"
+    (type_has
+       (cap
+      ^ "fn g(db: Db) effects {Db.read} -> Int {\n\
+        \  db.read(1)\n\
+         }\n\
+         fn f(db: Db) -> Int {\n\
+        \  g(db)\n\
+         }")
+       "선언되지 않은 effect Db.read");
+  check "effect 없는 함수는 절이 없어도 된다"
+    (type_ok "fn add(a: Int, b: Int) -> Int {\n  a + b\n}")
+
+(* --- 클로저의 effect는 정의한 자리가 아니라 부르는 자리에서 일어난다 --- *)
+
+let () =
+  check "클로저를 만들기만 하면 effect가 새지 않는다"
+    (type_ok
+       (cap
+      ^ "fn f(db: Db) -> fn() effects {Db.read} -> Int {\n\
+        \  fn() { db.read(1) }\n\
+         }"));
+  check "클로저가 선언한 것보다 많이 수행하면 오류"
+    (type_has
+       (cap
+      ^ "fn run(f: fn() effects {}) \n\
+         fn f(db: Db) {\n\
+        \  run(fn() effects {} { db.touch(1) })\n\
+         }")
+       "클로저가 선언하지 않은 effect Db.read");
+  check "파라미터가 허용한 범위를 넘는 함수를 넘기면 오류"
+    (type_has
+       (cap
+      ^ "fn run(f: fn() effects {})\n\
+         fn f(db: Db) {\n\
+        \  run(fn() { db.touch(1) })\n\
+         }")
+       "파라미터가 허용한 effect는 {}")
+
+(* --- effect 변수: 결정 위치에서 인자의 effect로 묶인다 --- *)
+
+let () =
+  let twice = "fn twice[e: effects](f: fn() effects e) effects e\n" in
+  check "effect 변수는 인자의 effect로 해소된다"
+    (type_ok
+       (cap ^ twice
+      ^ "fn f(db: Db) effects {Db.read} {\n  twice(fn() { db.touch(1) })\n}"));
+  check "해소된 effect가 선언에 없으면 오류"
+    (type_has
+       (cap ^ twice ^ "fn f(db: Db) {\n  twice(fn() { db.touch(1) })\n}")
+       "선언되지 않은 effect Db.read");
+  check "effect 변수를 그대로 물려주는 것은 통과"
+    (type_ok
+       (twice ^ "fn g[e: effects](f: fn() effects e) effects e {\n  twice(f)\n}"));
+  check "effect 변수를 선언하지 않고 물려주면 오류"
+    (type_has
+       (twice ^ "fn g[e: effects](f: fn() effects e) {\n  twice(f)\n}")
+       "선언되지 않은 effect e")
+
+(* --- capability 없이는 effect를 수행할 수 없다 --- *)
+
+let () =
+  check "capability 값이 없으면 메서드를 부를 수 없다"
+    (type_has
+       (cap ^ "fn f() effects {Db.read} -> Int {\n  Db.read(1)\n}")
+       "값을 통해서만")
+
+(* ================================================================== *)
+(* move / affinity 검사                                                *)
+(* ================================================================== *)
+
+let move_errs src =
+  List.map (fun (e : Move.error) -> e.msg) (Move.check (parse_ok src))
+
+let move_ok src = move_errs src = []
+
+let move_has src frag =
+  List.exists
+    (fun m ->
+      let n = String.length frag in
+      let rec go i =
+        i + n <= String.length m && (String.sub m i n = frag || go (i + 1))
+      in
+      go 0)
+    (move_errs src)
+
+let res =
+  "capability F {\n\
+  \  fn size() -> Int\n\
+   }\n\
+   fn drop(own f: F)\n\
+   fn peek(f: F) -> Int\n"
+
+(* --- 이중 소비와 분기 병합 --- *)
+
+let () =
+  check "빌리기만 하면 여러 번 써도 된다"
+    (move_ok (res ^ "fn f(x: F) -> Int {\n  peek(x) + peek(x)\n}"));
+  check "이중 소비는 오류"
+    (move_has (res ^ "fn f(own x: F) {\n  drop(x)\n  drop(x)\n}") "이미 move");
+  check "양쪽 분기에서 소비하면 통과"
+    (move_ok
+       (res
+      ^ "fn f(own x: F, c: Bool) {\n\
+        \  if c {\n\
+        \    drop(x)\n\
+        \  } else {\n\
+        \    drop(x)\n\
+        \  }\n\
+         }"));
+  check "한 분기에서만 소비해도 병합 이후는 moved (보수적 합집합)"
+    (move_has
+       (res
+      ^ "fn f(own x: F, c: Bool) {\n  if c {\n    drop(x)\n  }\n  drop(x)\n}")
+       "이미 move");
+  check "소비한 자리를 진단에 담는다"
+    (move_has (res ^ "fn f(own x: F) {\n  drop(x)\n  drop(x)\n}") "에서 소비")
+
+(* --- 빌린 값은 탈출하지 못한다 --- *)
+
+let () =
+  check "빌린 값의 반환" (move_has (res ^ "fn f(x: F) -> F {\n  x\n}") "반환할 수 없습니다");
+  check "빌린 값을 소유 자리로" (move_has (res ^ "fn f(x: F) {\n  drop(x)\n}") "빌린 값이라");
+  check "own으로 받으면 넘길 수 있다" (move_ok (res ^ "fn f(own x: F) {\n  drop(x)\n}"));
+  check "빌린 값의 struct 저장"
+    (move_has
+       (res ^ "struct H {\n  f: F,\n}\nfn g(x: F) -> H {\n  H { f: x }\n}")
+       "struct에 저장할 수 없습니다")
+
+(* --- use의 전염 --- *)
+
+let () =
+  check "빌린 값을 capture한 클로저는 빌린 값이다"
+    (move_has
+       (res ^ "fn sink(own h: fn())\nfn f(x: F) {\n  sink(fn() { peek(x) })\n}")
+       "use 값은 탈출하지 못합니다");
+  check "빌려 쓰는 자리로는 넘길 수 있다"
+    (move_ok
+       (res ^ "fn borrow(h: fn())\nfn f(x: F) {\n  borrow(fn() { peek(x) })\n}"))
+
+(* --- callable affinity --- *)
+
+let () =
+  check "affine 값을 capture하면 affine fn"
+    (move_ok (res ^ "fn f(own x: F) -> affine fn() {\n  fn() { drop(x) }\n}"));
+  check "affine 클로저를 fn 자리에 반환하면 오류"
+    (move_has
+       (res ^ "fn f(own x: F) -> fn() {\n  fn() { drop(x) }\n}")
+       "affine fn이어야 합니다");
+  check "by-move capture는 바깥에서 소비다"
+    (move_has
+       (res
+      ^ "fn f(own x: F) -> affine fn() {\n\
+        \  let g = fn() { drop(x) }\n\
+        \  drop(x)\n\
+        \  g\n\
+         }")
+       "이미 move")
+
+(* --- affinity 전이 --- *)
+
+let () =
+  check "capability를 필드로 가지면 전이적으로 affine"
+    (move_has
+       (res ^ "struct B {\n  f: F,\n}\nfn g(b: B) -> B {\n  b\n}")
+       "반환할 수 없습니다");
+  check "copyable 선언과 affine 필드는 공존할 수 없다"
+    (move_has (res ^ "copyable struct B {\n  f: F,\n}") "copyable로 선언되었지만");
+  check "affine이 없으면 copyable"
+    (move_ok "copyable struct B {\n  n: Int,\n}\nfn g(b: B) -> B {\n  b\n}");
+  check "컨테이너를 통해서도 전이된다"
+    (move_has (res ^ "fn g(x: List[F]) -> List[F] {\n  x\n}") "반환할 수 없습니다")
+
+(* --- 클로저의 mut capture 금지 --- *)
+
+let () =
+  check "클로저는 mut 바인딩을 capture할 수 없다"
+    (move_has
+       "fn sink(h: fn())\n\
+        fn f() {\n\
+       \  let mut n = 0\n\
+       \  sink(fn() { n = n + 1 })\n\
+        }"
+       "mut 바인딩");
+  check "불변 바인딩은 capture해도 된다"
+    (move_ok "fn sink(h: fn())\nfn f() {\n  let n = 0\n  sink(fn() { n })\n}")
+
+(* --- 외부 타입은 affine임을 증명할 수 없다 --- *)
+
+let () =
+  check "모르는 타입은 copyable로 본다" (move_ok "fn f(x: Widget) -> Widget {\n  x\n}")
+
+(* ================================================================== *)
+(* exhaustiveness                                                      *)
+(* ================================================================== *)
+
+let e3 = "enum E {\n  A(Int),\n  B,\n  C,\n}\n"
+
+let () =
+  check "모든 variant를 덮으면 통과"
+    (type_ok
+       (e3
+      ^ "fn f(x: E) -> Int {\n\
+        \  match x {\n\
+        \    A(n) => n,\n\
+        \    B => 1,\n\
+        \    C => 2,\n\
+        \  }\n\
+         }"));
+  check "빠진 variant를 이름으로 말한다"
+    (type_has
+       (e3
+      ^ "fn f(x: E) -> Int {\n  match x {\n    A(n) => n,\n    B => 1,\n  }\n}"
+       )
+       "빠진 경우: C");
+  check "와일드카드가 나머지를 덮는다"
+    (type_ok
+       (e3
+      ^ "fn f(x: E) -> Int {\n  match x {\n    A(n) => n,\n    _ => 0,\n  }\n}"
+       ));
+  check "Bool의 생성자 집합도 유한하다"
+    (type_has "fn f(b: Bool) -> Int {\n  match b {\n    true => 1,\n  }\n}"
+       "빠진 경우: false");
+  check "Option"
+    (type_has
+       "fn f(o: Option[Int]) -> Int {\n  match o {\n    Some(n) => n,\n  }\n}"
+       "빠진 경우: None");
+  check "Result"
+    (type_ok
+       "fn f(r: Result[Int, Int]) -> Int {\n\
+       \  match r {\n\
+       \    Ok(n) => n,\n\
+       \    Err(e) => e,\n\
+       \  }\n\
+        }");
+  check "중첩된 자리의 반례도 찾는다"
+    (type_has
+       (e3
+      ^ "fn f(o: Option[E]) -> Int {\n\
+        \  match o {\n\
+        \    Some(A(n)) => n,\n\
+        \    None => 0,\n\
+        \  }\n\
+         }")
+       "Some(B)");
+  check "Int 리터럴만으로는 완전해지지 않는다"
+    (type_has
+       "fn f(n: Int) -> Int {\n  match n {\n    0 => 1,\n    1 => 2,\n  }\n}"
+       "모든 경우를 덮지 않습니다");
+  check "와일드카드가 있으면 리터럴 match도 통과"
+    (type_ok
+       "fn f(n: Int) -> Int {\n  match n {\n    0 => 1,\n    _ => 2,\n  }\n}")
+
+let () =
+  check "와일드카드 뒤의 팔은 도달할 수 없다"
+    (type_has
+       (e3
+      ^ "fn f(x: E) -> Int {\n  match x {\n    _ => 0,\n    B => 1,\n  }\n}")
+       "도달할 수 없습니다");
+  check "같은 생성자를 두 번 쓰면 뒤가 죽는다"
+    (type_has
+       (e3
+      ^ "fn f(x: E) -> Int {\n\
+        \  match x {\n\
+        \    A(n) => n,\n\
+        \    A(m) => m,\n\
+        \    _ => 0,\n\
+        \  }\n\
+         }")
+       "도달할 수 없습니다");
+  check "생성자 집합을 모르면 검사하지 않는다"
+    (type_ok "fn f(w: Widget) -> Int {\n  match w {\n    _ => 0,\n  }\n}")
+
+(* upstream의 variant 추가가 downstream match를 깨뜨린다 —
+   interface hash가 enum 본문을 입력으로 삼는 이유 *)
+let () =
+  let two = "enum E {\n  A,\n  B,\n}\n" in
+  let three = "enum E {\n  A,\n  B,\n  C,\n}\n" in
+  let user =
+    "fn f(x: E) -> Int {\n  match x {\n    A => 0,\n    B => 1,\n  }\n}"
+  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))
+
+(* ------------------------------------------------------------------ *)
+(* 인터프리터                                                          *)
+(*                                                                     *)
+(* 샘플은 이제 "검사를 통과한다"가 아니라 "이 값을 낸다"까지 말한다.   *)
+(* 실행 가능한 명세가 되는 지점이고, v1이 백엔드를 바꿔도 남는다.      *)
+(* ------------------------------------------------------------------ *)
+
+let run_src src =
+  let dir = Filename.concat (Filename.get_temp_dir_name ()) "cool_runtest" in
+  ignore (Sys.command (Printf.sprintf "mkdir -p %s" (Filename.quote dir)));
+  let f = Filename.concat dir "m.cool" in
+  write f src;
+  (* 표준 라이브러리는 저장소의 std/. 테스트는 /tmp에서 도니 명시한다. *)
+  let st = Session.create ~root:dir ~std:"../std" () in
+  Session.run st f
+
+(* prelude가 없다. 표준 라이브러리도 명시적으로 가져온다.
+   미사용 import는 오류이므로 테스트마다 쓰는 것만 가져온다. *)
+let imports names =
+  String.concat ""
+    (List.map
+       (fun n ->
+         Printf.sprintf "import \"cool.dev/std/%s\" as %s\n"
+           (String.lowercase_ascii n) n)
+       names)
+
+let console =
+  "pub capability Console {\n\
+  \  fn print(s: String) effects {Console.print}\n\
+   }\n\n"
+
+let outputs ?(use = []) src expected =
+  match run_src (imports use ^ console ^ src) with
+  | Ok out -> out = expected
+  | Error e ->
+      Printf.printf "  (실행 오류: %s)\n" (Session.string_of_error e);
+      false
+
+let () =
+  check "산술과 출력"
+    (outputs ~use:[ "Int" ]
+       "pub fn main(c: Console) effects {Console.print} {\n\
+       \  c.print(Int.show(2 + 3 * 4))\n\
+        }"
+       "14\n");
+  check "match와 생성자"
+    (outputs ~use:[ "Int" ]
+       "pub enum S {\n\
+       \  A(Int),\n\
+       \  B,\n\
+        }\n\n\
+        pub fn f(s: S) -> Int {\n\
+       \  match s {\n\
+       \    A(n) => n + 1,\n\
+       \    B => 0,\n\
+       \  }\n\
+        }\n\n\
+        pub fn main(c: Console) effects {Console.print} {\n\
+       \  c.print(Int.show(f(A(41))))\n\
+       \  c.print(Int.show(f(B)))\n\
+        }"
+       "42\n0\n");
+  check "mut 바인딩과 대입"
+    (outputs ~use:[ "Int" ]
+       "pub fn main(c: Console) effects {Console.print} {\n\
+       \  let mut n = 1\n\
+       \  n = n + 10\n\
+       \  c.print(Int.show(n))\n\
+        }"
+       "11\n");
+  check "?는 Err에서 즉시 반환한다"
+    (outputs ~use:[ "Int" ]
+       "pub enum E {\n\
+       \  Bad,\n\
+        }\n\n\
+        pub fn half(n: Int) -> Result[Int, E] {\n\
+       \  if n % 2 == 0 { Ok(n / 2) } else { Err(Bad) }\n\
+        }\n\n\
+        pub fn twice(n: Int) -> Result[Int, E] {\n\
+       \  let a = half(n)?\n\
+       \  let b = half(a)?\n\
+       \  Ok(a + b)\n\
+        }\n\n\
+        pub fn show_res(r: Result[Int, E]) -> String {\n\
+       \  match r {\n\
+       \    Ok(v) => Int.show(v),\n\
+       \    Err(_) => \"err\",\n\
+       \  }\n\
+        }\n\n\
+        pub fn main(c: Console) effects {Console.print} {\n\
+       \  c.print(show_res(twice(8)))\n\
+       \  c.print(show_res(twice(7)))\n\
+        }"
+       "6\nerr\n");
+  check "클로저가 바깥 capability를 잡는다"
+    (outputs ~use:[ "List"; "Int" ]
+       "pub fn main(c: Console) effects {Console.print} {\n\
+       \  List.each([1, 2], fn(n) {\n\
+       \    c.print(Int.show(n))\n\
+       \  })\n\
+        }"
+       "1\n2\n");
+  check "scope 블록은 순차로 돌고 나갈 때 join한다"
+    (outputs
+       "pub fn main(c: Console, root: TaskScope) effects {Console.print} {\n\
+       \  scope sc = root {\n\
+       \    sc.spawn(fn() { c.print(\"a\") })\n\
+       \    sc.spawn(fn() { c.print(\"b\") })\n\
+       \  }\n\
+       \  c.print(\"after\")\n\
+        }"
+       "a\nb\nafter\n");
+  (* 권한은 런타임에서만 온다. main이 선언하지 않으면 존재하지 않는다. *)
+  check "선언하지 않은 capability는 실행 시점에도 없다"
+    (match run_src "pub fn main() { }" with Ok "" -> true | _ -> false);
+  check "런타임이 모르는 capability는 거절한다"
+    (match
+       run_src
+         "pub capability Db {\n\
+         \  fn read() effects {Db.read} -> Int\n\
+          }\n\n\
+          pub fn main(d: Db) effects {Db.read} -> Int { d.read() }"
+     with
+    | Error e -> has_sub e.message "제공하지 않습니다"
+    | Ok _ -> false)
+
+(* 표준 라이브러리 시그니처가 실제 검사에 쓰이는지.
+
+   std가 생기기 전에는 List.each가 모르는 이름이라 조용히 통과했다.
+   effect 다형성이 장식이 아니라는 것을 여기서 고정한다. *)
+let () =
+  let std_check src =
+    let dir = Filename.concat (Filename.get_temp_dir_name ()) "cool_stdtest" in
+    ignore (Sys.command (Printf.sprintf "mkdir -p %s" (Filename.quote dir)));
+    let f = Filename.concat dir "m.cool" in
+    write f src;
+    let st = Session.create ~root:dir ~std:"../std" () in
+    Session.load st f;
+    List.map (fun (e : Session.error) -> e.message) (Session.errors st)
+  in
+  let hdr use = imports use ^ "\n" ^ console in
+  let list_only = hdr [ "List" ] in
+  let hdr = hdr [ "List"; "Int" ] in
+  check "std 시그니처로 인자 개수를 잡는다"
+    (List.exists
+       (fun m -> has_sub m "인자 1개가 필요한데")
+       (std_check
+          (list_only ^ "pub fn f(xs: List[Int]) -> Int {\n  List.len(xs, 1)\n}")));
+  check "std 시그니처로 반환 타입을 잡는다"
+    (List.exists
+       (fun m -> has_sub m "String이(가) 필요한데 Int")
+       (std_check
+          (list_only ^ "pub fn f(xs: List[Int]) -> String {\n  List.len(xs)\n}")));
+  (* effect 변수가 호출 지점에서 실제로 해소된다 *)
+  check "List.each의 effect 변수가 클로저의 effect로 묶인다"
+    (List.exists
+       (fun m -> has_sub m "선언되지 않은 effect Console.print")
+       (std_check
+          (hdr
+         ^ "pub fn f(c: Console, xs: List[Int]) {\n\
+           \  List.each(xs, fn(n) { c.print(Int.show(n)) })\n\
+            }")));
+  check "effect를 선언하면 같은 코드가 통과한다"
+    (std_check
+       (hdr
+      ^ "pub fn f(c: Console, xs: List[Int]) effects {Console.print} {\n\
+        \  List.each(xs, fn(n) { c.print(Int.show(n)) })\n\
+         }")
+    = [])
+
+(* ------------------------------------------------------------------ *)
+(* lint 둘                                                             *)
+(*                                                                     *)
+(* 취향이 아니라 비용이다. 미사용 import는 재검사 범위를 넓히고,        *)
+(* effect 과잉 선언은 호출자에게 없는 의무를 지운다.                    *)
+(* ------------------------------------------------------------------ *)
+
+let () =
+  let msgs src =
+    let dir = Filename.concat (Filename.get_temp_dir_name ()) "cool_linttest" in
+    ignore (Sys.command (Printf.sprintf "mkdir -p %s" (Filename.quote dir)));
+    let f = Filename.concat dir "m.cool" in
+    write f src;
+    let st = Session.create ~root:dir ~std:"../std" () in
+    Session.load st f;
+    List.map (fun (e : Session.error) -> e.message) (Session.errors st)
+  in
+  let db =
+    "pub capability Db {\n\
+    \  fn read(id: Int) effects {Db.read} -> Int\n\
+    \  fn write(id: Int) effects {Db.write}\n\
+     }\n\n"
+  in
+  check "미사용 import를 잡는다"
+    (List.exists
+       (fun m -> has_sub m "가져왔지만 쓰지 않습니다")
+       (msgs
+          "import \"cool.dev/std/list\" as List\n\npub fn f() -> Int {\n  1\n}"));
+  check "쓰면 잡지 않는다"
+    (msgs
+       "import \"cool.dev/std/list\" as List\n\n\
+        pub fn f(xs: List[Int]) -> Int {\n\
+       \  List.len(xs)\n\
+        }"
+    = []);
+  check "effect 과잉 선언을 잡는다"
+    (List.exists
+       (fun m -> has_sub m "선언했지만 수행하지 않습니다")
+       (msgs
+          (db
+         ^ "pub fn f(db: Db, id: Int) effects {Db.read, Db.write} -> Int {\n\
+           \  db.read(id)\n\
+            }")));
+  check "정확히 선언하면 통과한다"
+    (msgs
+       (db
+      ^ "pub fn f(db: Db, id: Int) effects {Db.read} -> Int {\n  db.read(id)\n}"
+       )
+    = []);
+  (* 모르는 것을 틀렸다고 말하지 않는다 *)
+  check "effect 변수가 있으면 과잉 선언을 판정하지 않는다"
+    (msgs "pub fn f[e: effects](g: fn() effects e) effects e {\n  g()\n}" = []);
+  check "외부 타입이 섞이면 과잉 선언을 판정하지 않는다"
+    (msgs "pub fn f(fs: FileSystem) effects {FileSystem.read} {\n  fs.read()\n}"
+    = []);
+  (* lint는 뒤 단계를 막지 않는다 — lint 하나가 진짜 타입 오류를 가리면 안 된다 *)
+  check "미사용 import가 타입 오류를 가리지 않는다"
+    (let ms =
+       msgs
+         "import \"cool.dev/std/list\" as List\n\n\
+          pub fn f() -> String {\n\
+         \  1\n\
+          }"
+     in
+     List.exists (fun m -> has_sub m "가져왔지만 쓰지 않습니다") ms
+     && List.exists (fun m -> has_sub m "String이(가) 필요한데 Int") ms)