diff --git a/docs/grammar.ebnf b/docs/grammar.ebnf
index 2f90802..7efa1b8 100644
--- a/docs/grammar.ebnf
+++ b/docs/grammar.ebnf
@@ -197,7 +197,10 @@ if_expr        = "if" , expr_ns , block , [ "else" , ( block | if_expr ) ] ;
 match_expr     = "match" , expr_ns , "{" , { arm } , "}" ;
 arm            = pattern , "=>" , ( expr | block ) , { NEWLINE } ,
                  [ "," , { NEWLINE } ] ;
-scope_expr     = "scope" , ident , block ;
+scope_expr     = "scope" , ident , "=" , ident , block ;
+(* scope 자식 = 부모 { ... }
+ * 부모를 구문에 적는다. 적지 않으면 자식의 부모가 "가장 가까운 스코프"가 되어
+ * 정확히 ambient authority가 된다 — 이 언어가 배제하는 것 *)
 
 (* expr_ns = struct_lit로 시작하지 않는 expr.
  * if/match/scope의 머리 자리에서 "{"가 블록의 시작인지 struct 리터럴인지
diff --git a/docs/thesis.md b/docs/thesis.md
index 0083f24..952b40f 100644
--- a/docs/thesis.md
+++ b/docs/thesis.md
@@ -119,13 +119,15 @@ Affinity 전이 (보안 주장의 필수 전제):
   ※ v0는 affine 미소비(누수)를 허용하므로 handle 기반 보장은 애초에 불가능하다.
      실행 의미로 옮겨야 그 허점이 사라진다
 - 루트 TaskScope는 main에 주입 → ambient authority 없이 권한 사슬이 main부터 닫힌다
-- scope는 이름을 갖는다: scope sc { sc.spawn(...) }. 암묵 바인딩은 채택하지 않는다
-  ※ 중첩 시 결정적이다. scope outer { scope inner { ... } }에서 안쪽 블록이
-     바깥 스코프에 spawn하는 것(수명이 다른 태스크를 의도적으로 부모에 붙이는
-     정당한 패턴)이 암묵 바인딩으로는 표현 불가이거나 섀도잉 규칙이라는
-     새 복잡성을 부른다. 이름이 있으면 outer.spawn / inner.spawn으로 그냥 갈린다
+- scope는 자식을 만들고 부모를 구문에 적는다: scope inner = outer { ... }
+  ※ 부모를 적지 않으면 자식의 부모가 "가장 가까운 스코프"가 되는데, 그것이
+     정확히 ambient authority다. 권한 사슬이 main의 루트 TaskScope부터
+     끊기지 않고 이어지려면 모든 자식이 부모를 이름으로 지목해야 한다
+  ※ 중첩이 결정적이다. 안쪽 블록에서 바깥 스코프에 붙이는 것(수명이 다른
+     태스크를 의도적으로 부모에 붙이는 정당한 패턴)이 outer.spawn /
+     inner.spawn으로 그냥 갈린다
   ※ "어느 스코프에 붙는 태스크인가"가 리뷰어 눈에 보이는 것 자체가 이 언어가
-     파는 물건이다. 축약형은 체감 불만이 실제로 쌓이면 v1에서 검토
+     파는 물건이다. 타이핑을 줄이려고 여기서 깎으면 팔 물건이 없어진다
 
 Effect 다형성 (철학 2,5에서 파생):
 - effect 변수는 타입 파라미터와 정확히 같은 규율을 따른다:
@@ -243,6 +245,8 @@ Generics (철학 2에서 파생):
   ※ 가드가 붙는 순간 그 분기가 패턴 전체를 덮는다고 말할 수 없어 exhaustiveness가
      흐려지고, SMT 없이는 보수적으로 _ 분기를 강요하게 된다. 철학 1의 대표 항목을
      문법 편의와 바꾸지 않는다. 필요하면 분기 본문에서 if를 쓴다
+- 타입 이름은 그 타입에 딸린 함수의 이름공간이다: String.len(s), File.close(f).
+  별도의 정적 메서드 문법을 두지 않는다
 - ?는 Result 전용으로 하드코딩한다 (trait solver가 없으므로 일반화 경로가 없다)
   ※ 조기 탈출도 블록 종료이므로 scope의 join/cancel은 ? 경로에서도 실행된다
   ※ v1에서 linear를 넣으면 ?의 조기 탈출 경로마다 해제가 필요해진다.
@@ -261,6 +265,9 @@ Generics (철학 2에서 파생):
 
 포함 (되돌리기 비싼 것 전부):
 - parse → name resolution → type check → effect/capability check
+  ※ 각 단계는 그 단계가 소유한 성질만 판정한다. 예: affinity는 타입 동등성이
+     아니라 substructural 성질이므로 타입 검사가 아니라 move 검사가 소유한다.
+     단계가 서로의 결론을 앞지르면 진단이 엉뚱한 곳에서 난다
 - move/affinity 검사, capability use 규칙, affinity 전이
 - effect 변수 (effect 다형성)
 - interface artifact + hash 기반 incremental invalidation
diff --git a/lib/ast.ml b/lib/ast.ml
index 6b41afb..8940e40 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -55,7 +55,7 @@ type expr =
   | E_closure of closure
   | E_if of { cond : expr; then_ : block; else_ : expr option; pos : pos }
   | E_match of { scrutinee : expr; arms : arm list; pos : pos }
-  | E_scope of { name : string; body : block; pos : pos }
+  | E_scope of { name : string; parent : string; body : block; pos : pos }
   | E_block of block
   | E_call of { callee : expr; args : expr list; pos : pos }
   | E_field of { obj : expr; name : string; pos : pos }
@@ -285,8 +285,8 @@ let rec buf_expr b = function
           Buffer.add_char b ')')
         arms;
       Buffer.add_char b ')'
-  | E_scope { name; body; _ } ->
-      Buffer.add_string b ("(scope " ^ name ^ " ");
+  | E_scope { name; parent; body; _ } ->
+      Buffer.add_string b ("(scope " ^ name ^ " = " ^ parent ^ " ");
       buf_block b body;
       Buffer.add_char b ')'
   | E_block bl -> buf_block b bl
diff --git a/lib/driver.ml b/lib/driver.ml
index b313c10..0529fb5 100644
--- a/lib/driver.ml
+++ b/lib/driver.ml
@@ -56,6 +56,33 @@ let resolve (file : string) : (Resolve.info, error list) result =
                  { file; line = e.pos.line; col = e.pos.col; message = e.msg })
                errors))
 
+let typecheck (file : string) : (unit, error list) result =
+  match parse_file file with
+  | Error e -> Error [ e ]
+  | Ok m -> (
+      let _, rerrors = Resolve.resolve m in
+      match rerrors with
+      | _ :: _ ->
+          Error
+            (List.map
+               (fun (e : Resolve.error) ->
+                 { file; line = e.pos.line; col = e.pos.col; message = e.msg })
+               rerrors)
+      | [] -> (
+          match Typecheck.check m with
+          | [] -> Ok ()
+          | terrors ->
+              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
   | [] ->
@@ -63,16 +90,13 @@ let check (files : string list) : (unit, error list) result =
   | _ ->
       let errors =
         List.filter_map
-          (fun f ->
-            match resolve f with
-            | Ok _ -> None
-            | Error (e :: _) -> Some e
-            | Error [] -> None)
+          (fun f -> match typecheck f with Ok _ -> None | Error es -> Some es)
           files
+        |> List.concat
       in
       if errors <> [] then Error errors
       else
-        (* 이름 해소는 통과했다. 통과했다고 말하지 않는다 — 파이프라인의
+        (* 타입 검사는 통과했다. 통과했다고 말하지 않는다 — 파이프라인의
            나머지가 아직 없으므로 검사되지 않은 것이다. *)
         Error
           (List.map
@@ -81,7 +105,8 @@ let check (files : string list) : (unit, error list) result =
                  file = f;
                  line = 0;
                  col = 0;
-                 message = "구문 분석까지 통과. 이름 해소가 아직 구현되지 않았습니다";
+                 message =
+                   "타입 검사까지 통과. effect/capability 검사와 move 검사가 아직 구현되지 않았습니다";
                })
              files)
 
diff --git a/lib/parser.ml b/lib/parser.ml
index ba60301..86aaa36 100644
--- a/lib/parser.ml
+++ b/lib/parser.ml
@@ -385,9 +385,11 @@ and parse_primary st =
   | Token.Kw_match -> parse_match st
   | Token.Kw_scope ->
       adv st;
-      let name = ident st "scope 이름" in
+      let name = ident st "새 scope 이름" in
+      expect st Token.Eq "= (자식 scope의 부모를 명시해야 합니다)";
+      let parent = ident st "부모 scope 이름" in
       let body = parse_block st in
-      E_scope { name; body; pos = p }
+      E_scope { name; parent; body; pos = p }
   | Token.Ident n ->
       adv st;
       if (not st.no_struct) && kind st = Token.LBrace then
diff --git a/lib/resolve.ml b/lib/resolve.ml
index b709ed8..70c62ea 100644
--- a/lib/resolve.ml
+++ b/lib/resolve.ml
@@ -139,6 +139,8 @@ let rec resolve_expr st = function
         if Hashtbl.mem st.items n then ()
         else if List.mem n builtin_values then ()
         else if Hashtbl.mem st.ctors n then ()
+        else if List.mem n builtin_types then ()
+          (* 타입 이름은 그 타입에 딸린 함수의 이름공간이다: String.len *)
         else external_ref st n pos
   | E_list (xs, _) -> List.iter (resolve_expr st) xs
   | E_struct { name; fields; pos } ->
@@ -171,16 +173,20 @@ let rec resolve_expr st = function
           resolve_expr st a.arm_body;
           pop st)
         arms
-  | E_scope { name; body; pos } ->
-      (* TaskScope는 use 값이라 모듈 수준에 있을 수 없다. scope의 머리는
-         반드시 지역 바인딩(파라미터 포함)이어야 한다. *)
-      if lookup_local st name = None then
+  | E_scope { name; parent; body; pos } ->
+      (* 부모는 이미 가진 TaskScope여야 한다. TaskScope는 use 값이라 모듈
+         수준에 있을 수 없으므로 반드시 지역 바인딩(파라미터 포함)이다.
+         자식 scope 이름은 블록 안에서만 산다. *)
+      if lookup_local st parent = None then
         error st pos
           (Printf.sprintf
-             "scope 이름 %s이(가) 지역 바인딩이 아닙니다 (TaskScope는 use 값이라 파라미터나 상위 블록에서 \
+             "부모 scope %s이(가) 지역 바인딩이 아닙니다 (TaskScope는 use 값이라 파라미터나 상위 블록에서 \
               와야 합니다)"
-             name);
-      resolve_block_scoped st body
+             parent);
+      push st;
+      bind st pos name false;
+      resolve_block st body;
+      pop st
   | E_block b -> resolve_block_scoped st b
   | E_call { callee; args; _ } ->
       resolve_expr st callee;
diff --git a/lib/typecheck.ml b/lib/typecheck.ml
new file mode 100644
index 0000000..591034e
--- /dev/null
+++ b/lib/typecheck.ml
@@ -0,0 +1,604 @@
+(* 타입 검사.
+
+   범위: 이 모듈 안에서 아는 것만 검사한다. 외부 이름은 TUnknown이 되어
+   무엇과도 맞는다 — 모르는 것을 틀렸다고 말하지 않는다.
+
+   제네릭 해소는 호출 지점의 지역 unification이다. 함수 하나를 넘어가지
+   않으므로 전역 추론이 아니다. *)
+
+open Ast
+module T = Types
+
+type error = { pos : Token.pos; msg : string }
+
+type scheme = {
+  s_gen : string list; (* 타입 파라미터 이름 (effect 파라미터는 제외) *)
+  s_params : T.t list;
+  s_ret : T.t;
+}
+
+type env = {
+  structs : (string, string list * (string * T.t) list) Hashtbl.t;
+  enums : (string, string list * (string * T.t list) list) Hashtbl.t;
+  caps : (string, (string * scheme) list) Hashtbl.t;
+  fns : (string, scheme) Hashtbl.t;
+  consts : (string, T.t) Hashtbl.t;
+  ctors : (string, string) Hashtbl.t; (* variant -> enum *)
+  mutable locals : (string * T.t) list list;
+  mutable ret : T.t; (* 현재 함수의 선언된 반환 타입 *)
+  mutable errors : error list;
+}
+
+let err env pos msg = env.errors <- { pos; msg } :: env.errors
+
+let mismatch env pos expected got what =
+  err env pos
+    (Printf.sprintf "%s: %s이(가) 필요한데 %s입니다" what (T.show expected) (T.show got))
+
+let push env = env.locals <- [] :: env.locals
+let pop env = match env.locals with _ :: r -> env.locals <- r | [] -> ()
+
+let bind env n t =
+  match env.locals with
+  | s :: r -> env.locals <- ((n, t) :: s) :: r
+  | [] -> env.locals <- [ [ (n, t) ] ]
+
+let lookup env n =
+  let rec go = function
+    | [] -> None
+    | s :: r -> (
+        match List.assoc_opt n s with Some t -> Some t | None -> go r)
+  in
+  go env.locals
+
+(* ------------------------------------------------------------------ *)
+(* Ast.ty -> Types.t                                                   *)
+(* ------------------------------------------------------------------ *)
+
+let rec conv env (gen : string list) (t : Ast.ty) : T.t =
+  match t with
+  | T_named { 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
+      else
+        match name with
+        | "Int" -> T.TInt
+        | "Bool" -> T.TBool
+        | "String" -> T.TString
+        | "Unit" -> T.TUnit
+        | "List" | "Option" | "Result" -> T.TCon (name, args)
+        | _ ->
+            if
+              Hashtbl.mem env.structs name
+              || Hashtbl.mem env.enums name || Hashtbl.mem env.caps name
+            then T.TCon (name, args)
+            else T.TUnknown)
+  | T_fn { affine; params; ret; _ } ->
+      T.TFn
+        {
+          affine;
+          params = List.map (conv env gen) params;
+          ret = (match ret with None -> T.TUnit | Some r -> conv env gen r);
+        }
+
+let scheme_of env (d : fn_decl) : scheme =
+  let gen =
+    List.filter_map
+      (fun g -> if g.gp_effect then None else Some g.gp_name)
+      d.fn_gen
+  in
+  {
+    s_gen = gen;
+    s_params = List.map (fun p -> conv env gen p.p_ty) d.fn_params;
+    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 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 builtin_ctor = function
+  | "Ok" ->
+      let a = T.fresh () and b = T.fresh () in
+      Some ([ a ], T.TCon ("Result", [ a; b ]))
+  | "Err" ->
+      let a = T.fresh () and b = T.fresh () in
+      Some ([ b ], T.TCon ("Result", [ a; b ]))
+  | "Some" ->
+      let a = T.fresh () in
+      Some ([ a ], T.TCon ("Option", [ a ]))
+  | _ -> None
+
+(* ------------------------------------------------------------------ *)
+(* 식                                                                  *)
+(* ------------------------------------------------------------------ *)
+
+let rec infer env (e : expr) : T.t =
+  match e with
+  | E_lit (L_int _, _) -> T.TInt
+  | E_lit (L_str _, _) -> T.TString
+  | E_lit (L_bool _, _) -> T.TBool
+  | E_ident (n, _) -> (
+      match lookup env n with
+      | Some t -> t
+      | None -> (
+          match Hashtbl.find_opt env.consts n with
+          | Some t -> t
+          | None -> (
+              match n with
+              | "unit" -> T.TUnit
+              | "None" -> T.TCon ("Option", [ T.fresh () ])
+              | _ -> (
+                  match Hashtbl.find_opt env.fns n with
+                  | Some s ->
+                      let params, ret = instantiate s in
+                      T.TFn { affine = false; params; ret }
+                  | None -> (
+                      match Hashtbl.find_opt env.ctors n with
+                      | Some enum -> nullary_ctor env enum n
+                      | None -> T.TUnknown)))))
+  | E_list (xs, pos) ->
+      let elem = T.fresh () in
+      List.iter
+        (fun x ->
+          let t = infer env x in
+          if not (T.unify elem t) then
+            mismatch env pos elem t "리스트 원소의 타입이 서로 다릅니다")
+        xs;
+      T.TCon ("List", [ elem ])
+  | E_struct { name; fields; pos } -> infer_struct env name fields pos
+  | E_closure c -> infer_closure env c None
+  | E_if { cond; then_; else_; pos } -> (
+      let c = infer env cond in
+      if not (T.unify c T.TBool) then mismatch env pos T.TBool c "if의 조건";
+      let t1 = infer_block env then_ in
+      match else_ with
+      | None ->
+          if not (T.unify t1 T.TUnit) then
+            err env pos "else가 없는 if의 본문은 값을 남길 수 없습니다";
+          T.TUnit
+      | Some e2 ->
+          let t2 = infer env e2 in
+          if not (T.unify t1 t2) then mismatch env pos t1 t2 "if의 두 분기 타입이 다릅니다";
+          t1)
+  | E_match { scrutinee; arms; pos } ->
+      let s = infer env scrutinee in
+      let result = T.fresh () in
+      List.iter
+        (fun a ->
+          push env;
+          check_pattern env s a.arm_pat;
+          let t = infer env a.arm_body in
+          if not (T.unify result t) then
+            mismatch env a.arm_pos result t "match 팔의 타입이 서로 다릅니다";
+          pop env)
+        arms;
+      if arms = [] then err env pos "match에 팔이 없습니다";
+      result
+  | E_scope { name; parent; body; pos } ->
+      (match lookup env parent with
+      | Some t when not (T.unify t (T.TCon ("TaskScope", []))) ->
+          if T.resolve t <> T.TUnknown then
+            mismatch env pos (T.TCon ("TaskScope", [])) t "scope의 부모"
+      | _ -> ());
+      push env;
+      bind env name (T.TCon ("TaskScope", []));
+      let t = infer_block env body in
+      pop env;
+      t
+  | E_block b ->
+      push env;
+      let t = infer_block env b in
+      pop env;
+      t
+  | E_call { callee; args; pos } -> infer_call env callee args pos
+  | E_field { obj; name; pos } -> infer_field env obj name pos
+  | E_inst { callee; args; pos } -> infer_inst env callee args pos
+  | E_try { inner; pos } -> (
+      let t = infer env inner in
+      match T.resolve t with
+      | T.TUnknown -> T.TUnknown
+      | T.TCon ("Result", [ ok; _ ]) ->
+          (match T.resolve env.ret with
+          | T.TCon ("Result", _) | T.TUnknown -> ()
+          | r ->
+              err env pos
+                (Printf.sprintf "?는 Result를 반환하는 함수 안에서만 쓸 수 있습니다 (현재 반환 타입 %s)"
+                   (T.show r)));
+          ok
+      | other ->
+          err env pos
+            (Printf.sprintf "?는 Result에만 쓸 수 있습니다 (%s에 쓰였습니다)" (T.show other));
+          T.TUnknown)
+  | E_unary { op; operand; pos } ->
+      let t = infer env operand in
+      let want = match op with U_not -> T.TBool | U_neg -> T.TInt in
+      if not (T.unify t want) then mismatch env pos want t "단항 연산자의 피연산자";
+      want
+  | E_binary { op; lhs; rhs; pos } -> (
+      let a = infer env lhs and b = infer env rhs in
+      match op with
+      | B_or | B_and ->
+          if not (T.unify a T.TBool) then mismatch env pos T.TBool a "논리 연산자";
+          if not (T.unify b T.TBool) then mismatch env pos T.TBool b "논리 연산자";
+          T.TBool
+      | B_add | B_sub | B_mul | B_div | B_rem ->
+          if not (T.unify a T.TInt) then mismatch env pos T.TInt a "산술 연산자";
+          if not (T.unify b T.TInt) then mismatch env pos T.TInt b "산술 연산자";
+          T.TInt
+      | B_lt | B_le | B_gt | B_ge ->
+          if not (T.unify a T.TInt) then mismatch env pos T.TInt a "비교 연산자";
+          if not (T.unify b T.TInt) then mismatch env pos T.TInt b "비교 연산자";
+          T.TBool
+      | B_eq | B_ne ->
+          if not (T.unify a b) then mismatch env pos a b "같은 타입끼리만 비교할 수 있습니다";
+          T.TBool)
+
+and nullary_ctor env enum name =
+  match Hashtbl.find_opt env.enums enum with
+  | None -> T.TUnknown
+  | Some (gen, variants) -> (
+      let sub = List.map (fun v -> (v, T.fresh ())) gen in
+      match List.assoc_opt name variants with
+      | Some [] -> T.TCon (enum, List.map snd sub)
+      | _ -> T.TCon (enum, List.map snd sub))
+
+and infer_struct env name fields pos =
+  match Hashtbl.find_opt env.structs name with
+  | None ->
+      List.iter (fun (_, e) -> ignore (infer env e)) fields;
+      T.TUnknown
+  | Some (gen, decl_fields) ->
+      let sub = List.map (fun v -> (v, T.fresh ())) gen in
+      List.iter
+        (fun (fname, fe) ->
+          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 got = infer env fe in
+              if not (T.unify want got) then
+                mismatch env pos want got (Printf.sprintf "%s.%s 필드" name fname))
+        fields;
+      List.iter
+        (fun (fname, _) ->
+          if not (List.mem_assoc fname fields) then
+            err env pos (Printf.sprintf "%s의 %s 필드가 빠졌습니다" name fname))
+        decl_fields;
+      T.TCon (name, List.map snd sub)
+
+and infer_closure env (c : closure) (expected : T.t option) =
+  let expected_params, expected_ret =
+    match Option.map T.resolve expected with
+    | Some (T.TFn { params; ret; _ })
+      when List.length params = List.length c.cl_params ->
+        (List.map Option.some params, Some ret)
+    | _ -> (List.map (fun _ -> None) c.cl_params, None)
+  in
+  push env;
+  let param_tys =
+    List.map2
+      (fun (n, ann) exp ->
+        let t =
+          match ann with
+          | Some a -> conv env [] a
+          | None -> ( match exp with Some t -> t | None -> T.TUnknown)
+        in
+        bind env n t;
+        t)
+      c.cl_params expected_params
+  in
+  let declared_ret = Option.map (conv env []) c.cl_ret in
+  let saved = env.ret in
+  env.ret <-
+    (match declared_ret with
+    | Some t -> t
+    | None -> ( match expected_ret with Some t -> t | None -> T.TUnknown));
+  let body = infer_block env c.cl_body 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;
+  pop env;
+  T.TFn { affine = false; params = param_tys; ret }
+
+and infer_call env callee args pos =
+  let fn_ty =
+    match callee with
+    | E_ident (n, _) when lookup env n = None -> (
+        match Hashtbl.find_opt env.ctors n with
+        | Some enum -> Some (ctor_fn env enum n)
+        | None -> (
+            match builtin_ctor n with
+            | Some (params, ret) -> Some (T.TFn { affine = false; params; ret })
+            | None -> (
+                match Hashtbl.find_opt env.fns n with
+                | Some s ->
+                    let params, ret = instantiate s in
+                    Some (T.TFn { affine = false; params; ret })
+                | None -> None)))
+    | _ -> (
+        match T.resolve (infer env callee) with
+        | T.TFn _ as t -> Some t
+        | _ -> None)
+  in
+  match fn_ty with
+  | None ->
+      List.iter (fun a -> ignore (infer env a)) args;
+      T.TUnknown
+  | Some (T.TFn { params; ret; _ }) ->
+      if List.length params <> List.length args then (
+        err env pos
+          (Printf.sprintf "인자 %d개가 필요한데 %d개가 주어졌습니다" (List.length params)
+             (List.length args));
+        List.iter (fun a -> ignore (infer env a)) args)
+      else
+        List.iter2
+          (fun p a ->
+            let got =
+              match a with
+              | 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 "인자")
+          params args;
+      ret
+  | Some _ -> T.TUnknown
+
+and ctor_fn env enum name =
+  match Hashtbl.find_opt env.enums enum with
+  | None -> T.TUnknown
+  | Some (gen, variants) ->
+      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
+        | None -> []
+      in
+      T.TFn { affine = false; params; ret = T.TCon (enum, List.map snd sub) }
+
+and infer_field env obj name pos =
+  let t = infer env obj in
+  match T.resolve t with
+  | T.TUnknown -> T.TUnknown
+  | T.TCon (cname, args) -> (
+      match Hashtbl.find_opt env.structs cname with
+      | Some (gen, fields) -> (
+          let sub = List.map2 (fun v a -> (v, a)) gen (adjust gen args) in
+          match List.assoc_opt name fields with
+          | Some ft -> T.subst sub ft
+          | None ->
+              err env pos (Printf.sprintf "%s에 %s 필드가 없습니다" cname name);
+              T.TUnknown)
+      | None -> (
+          match Hashtbl.find_opt env.caps cname with
+          | Some methods -> (
+              match List.assoc_opt name methods with
+              | Some s ->
+                  let params, ret = instantiate s in
+                  T.TFn { affine = false; params; 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
+  let rec take k xs =
+    if k = 0 then []
+    else
+      match xs with
+      | [] -> T.fresh () :: take (k - 1) []
+      | x :: r -> x :: take (k - 1) r
+  in
+  take n args
+
+and infer_inst env callee args pos =
+  let tys =
+    List.filter_map
+      (function TA_ty t -> Some (conv env [] t) | TA_eff _ -> None)
+      args
+  in
+  match callee with
+  | E_ident (n, _) when lookup env n = None -> (
+      match Hashtbl.find_opt env.fns n with
+      | None -> T.TUnknown
+      | Some s ->
+          if List.length tys <> List.length s.s_gen then (
+            err env pos
+              (Printf.sprintf "타입 인자 %d개가 필요한데 %d개가 주어졌습니다"
+                 (List.length s.s_gen) (List.length tys));
+            T.TUnknown)
+          else
+            let params, ret = instantiate_with s tys in
+            T.TFn { affine = false; params; ret })
+  | _ -> T.TUnknown
+
+and check_pattern env (scrutinee : T.t) (p : pattern) =
+  match p with
+  | P_wild _ -> ()
+  | P_lit (l, pos) ->
+      let t =
+        match l with
+        | L_int _ -> T.TInt
+        | L_str _ -> T.TString
+        | L_bool _ -> T.TBool
+      in
+      if not (T.unify scrutinee t) then mismatch env pos scrutinee t "패턴의 리터럴"
+  | P_bind (n, _) -> (
+      match Hashtbl.find_opt env.ctors n with
+      | Some enum ->
+          check_ctor env scrutinee enum n [] Token.{ line = 0; col = 0 }
+      | None -> bind env n scrutinee)
+  | P_ctor { name; args; pos } -> (
+      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)
+
+and check_ctor env scrutinee enum name args pos =
+  match Hashtbl.find_opt env.enums enum with
+  | None -> ()
+  | Some (gen, variants) ->
+      let sub = List.map (fun v -> (v, T.fresh ())) gen in
+      let ety = T.TCon (enum, List.map snd sub) in
+      if not (T.unify scrutinee ety) then
+        mismatch env pos scrutinee ety "패턴이 match 대상과 다른 타입입니다";
+      let fields =
+        match List.assoc_opt name variants with Some ts -> ts | None -> []
+      in
+      if List.length fields = List.length args then
+        List.iter2
+          (fun ft ap -> check_pattern env (T.subst sub ft) ap)
+          fields args
+
+(* ------------------------------------------------------------------ *)
+(* 문과 블록                                                           *)
+(* ------------------------------------------------------------------ *)
+
+and infer_block env (b : block) : T.t =
+  let rec go = function
+    | [] -> T.TUnit
+    | [ S_expr e ] -> infer env e
+    | s :: rest ->
+        check_stmt env s;
+        go rest
+  in
+  go b.stmts
+
+and check_stmt env = function
+  | S_let { pat; ty; value; pos; _ } ->
+      let declared = Option.map (conv env []) ty in
+      let got =
+        match (value, declared) with
+        | E_closure c, Some t -> infer_closure env c (Some t)
+        | _ -> infer env value
+      in
+      let t =
+        match declared with
+        | None -> got
+        | Some d ->
+            if not (T.unify d got) then mismatch env pos d got "let의 타입 주석";
+            d
+      in
+      check_pattern env t pat
+  | S_return { value; pos } ->
+      let got = match value with None -> T.TUnit | Some e -> infer env e in
+      if not (T.unify env.ret got) then mismatch env pos env.ret got "return의 값"
+  | S_assign { place; value; pos } ->
+      let p = infer env place in
+      let v = infer env value in
+      if not (T.unify p v) then mismatch env pos p v "대입"
+  | S_expr e -> ignore (infer env e)
+
+(* ------------------------------------------------------------------ *)
+(* 모듈                                                                *)
+(* ------------------------------------------------------------------ *)
+
+let check_fn env (d : fn_decl) =
+  match d.fn_body with
+  | None -> ()
+  | Some body ->
+      let gen =
+        List.filter_map
+          (fun g -> if g.gp_effect then None else Some g.gp_name)
+          d.fn_gen
+      in
+      push env;
+      List.iter (fun p -> bind env p.p_name (conv env gen p.p_ty)) d.fn_params;
+      let declared =
+        match d.fn_ret with None -> T.TUnit | Some r -> conv env gen r
+      in
+      env.ret <- declared;
+      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);
+      pop env
+
+let check (m : modul) : error list =
+  let env =
+    {
+      structs = Hashtbl.create 16;
+      enums = Hashtbl.create 16;
+      caps = Hashtbl.create 16;
+      fns = Hashtbl.create 16;
+      consts = Hashtbl.create 16;
+      ctors = Hashtbl.create 16;
+      locals = [];
+      ret = T.TUnit;
+      errors = [];
+    }
+  in
+  (* 1차: 타입과 생성자 이름부터 (선언 순서에 의존하지 않는다) *)
+  List.iter
+    (fun it ->
+      match it with
+      | I_struct { name; gen; _ } ->
+          Hashtbl.replace env.structs name
+            (List.map (fun g -> g.gp_name) gen, [])
+      | I_enum { name; gen; variants; _ } ->
+          Hashtbl.replace env.enums name (List.map (fun g -> g.gp_name) gen, []);
+          List.iter (fun v -> Hashtbl.replace env.ctors v.v_name name) variants
+      | I_capability { name; _ } -> Hashtbl.replace env.caps name []
+      | _ -> ())
+    m.items;
+  (* 2차: 본문을 채운다 *)
+  List.iter
+    (fun it ->
+      match it with
+      | I_struct { name; gen; fields; _ } ->
+          let g = List.map (fun x -> x.gp_name) gen in
+          Hashtbl.replace env.structs name
+            (g, List.map (fun f -> (f.f_name, conv env g f.f_ty)) fields)
+      | I_enum { name; gen; variants; _ } ->
+          let g = List.map (fun x -> x.gp_name) gen in
+          Hashtbl.replace env.enums name
+            ( g,
+              List.map
+                (fun v -> (v.v_name, List.map (conv env g) v.v_args))
+                variants )
+      | I_capability { name; methods; _ } ->
+          Hashtbl.replace env.caps name
+            (List.map (fun d -> (d.fn_name, scheme_of env d)) methods)
+      | I_fn { decl; _ } ->
+          Hashtbl.replace env.fns decl.fn_name (scheme_of env decl)
+      | I_const { name; ty; _ } ->
+          Hashtbl.replace env.consts name (conv env [] ty)
+      | _ -> ())
+    m.items;
+  (* 3차: 본문 검사 *)
+  List.iter
+    (fun it ->
+      env.locals <- [];
+      match it with
+      | I_fn { decl; _ } -> check_fn env decl
+      | I_const { ty; value; pos; _ } ->
+          let want = conv env [] ty in
+          let got = infer env value in
+          if not (T.unify want got) then mismatch env pos want got "상수의 값"
+      | _ -> ())
+    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 env.errors)
diff --git a/lib/types.ml b/lib/types.ml
new file mode 100644
index 0000000..d418ffc
--- /dev/null
+++ b/lib/types.ml
@@ -0,0 +1,93 @@
+(* 타입 표현과 지역 unification.
+
+   TUnknown이 핵심이다. 외부 모듈에서 오는 이름은 모듈 로딩이 없는 v0에서
+   해소할 수 없다. 그런 타입은 TUnknown이 되고 무엇과도 맞는다 — 모르는 것을
+   틀렸다고 말하지 않기 위해서다. 아는 범위에서만 검사한다.
+
+   TMeta는 호출 지점에서 제네릭을 인스턴스화할 때 생기는 미지수다. 함수 하나
+   범위에서만 살고 전역으로 흐르지 않는다 (철학 2: 전역 추론 없음). *)
+
+type t =
+  | TUnknown
+  | TInt
+  | TBool
+  | TString
+  | TUnit
+  | TVar of string
+  | TCon of string * t list
+  | TFn of { affine : bool; params : t list; ret : t }
+  | TMeta of meta ref
+
+and meta = Unbound of int | Bound of t
+
+let counter = ref 0
+
+let fresh () =
+  incr counter;
+  TMeta (ref (Unbound !counter))
+
+let rec resolve t =
+  match t with TMeta { contents = Bound u } -> resolve u | _ -> t
+
+let rec show t =
+  match resolve t with
+  | TUnknown -> "?"
+  | TInt -> "Int"
+  | TBool -> "Bool"
+  | TString -> "String"
+  | TUnit -> "Unit"
+  | TVar v -> v
+  | TCon (n, []) -> n
+  | TCon (n, args) -> n ^ "[" ^ String.concat ", " (List.map show args) ^ "]"
+  | TFn { affine; params; ret } -> (
+      (if affine then "affine fn(" else "fn(")
+      ^ String.concat ", " (List.map show params)
+      ^ ")"
+      ^ match resolve ret with TUnit -> "" | r -> " -> " ^ show r)
+  | TMeta { contents = Unbound n } -> Printf.sprintf "_%d" n
+  | TMeta { contents = Bound _ } -> "?"
+
+let rec occurs r t =
+  match resolve t with
+  | TMeta r' -> r == r'
+  | TCon (_, args) -> List.exists (occurs r) args
+  | TFn { params; ret; _ } -> List.exists (occurs r) params || occurs r ret
+  | _ -> false
+
+(* 성공하면 true. 실패해도 예외를 던지지 않는다 — 호출자가 위치를 알고
+   진단을 만든다. *)
+let rec unify a b =
+  match (resolve a, resolve b) with
+  | TUnknown, _ | _, TUnknown -> true
+  | TMeta r, TMeta r' when r == r' -> true
+  | TMeta r, t | t, TMeta r ->
+      if occurs r t then false
+      else (
+        r := Bound t;
+        true)
+  | TInt, TInt | TBool, TBool | TString, TString | TUnit, TUnit -> true
+  | TVar x, TVar y -> x = y
+  | TCon (n, xs), TCon (m, ys) ->
+      n = m && List.length xs = List.length ys && List.for_all2 unify xs ys
+  | TFn f, TFn g ->
+      (* affinity는 타입 동등성의 일부가 아니다. 값이 affine인지는 무엇을
+         capture했는지로 정해지는 substructural 성질이고, move/affinity 검사가
+         소유한다. 여기서 섞으면 두 검사가 서로의 결론을 앞질러 버린다. *)
+      List.length f.params = List.length g.params
+      && List.for_all2 unify f.params g.params
+      && unify f.ret g.ret
+  | _ -> false
+
+(* 제네릭 인스턴스화: TVar를 주어진 대입으로 바꾼다 *)
+let rec subst env t =
+  match resolve t with
+  | TVar v -> ( match List.assoc_opt v env with Some u -> u | None -> TVar v)
+  | TCon (n, args) -> TCon (n, List.map (subst env) args)
+  | TFn f ->
+      TFn
+        {
+          affine = f.affine;
+          params = List.map (subst env) f.params;
+          ret = subst env f.ret;
+        }
+  | u -> u
diff --git a/samples/03_scope_concurrency.cool b/samples/03_scope_concurrency.cool
index 6718a97..d4c6f93 100644
--- a/samples/03_scope_concurrency.cool
+++ b/samples/03_scope_concurrency.cool
@@ -1,21 +1,22 @@
 // 03. TaskScope capability와 이름 있는 scope
 //
-// scope는 이름을 갖는다. 중첩 시 어느 스코프에 붙는 태스크인지가 코드에 보인다.
+// scope 자식 = 부모 { ... }. 부모를 구문에 적는 이유는 하나다 —
+// 적지 않으면 자식의 부모가 "가장 가까운 스코프"가 되고, 그것이 ambient authority다.
 
 import "cool.dev/std/list" as List
 
 pub fn main(
-    sc: TaskScope,
+    root: TaskScope,
     fs: FileSystem,
     log: Logger,
 ) effects {TaskScope.spawn, FileSystem.read, Logger.write} {
     let paths = [Path("a.txt"), Path("b.txt"), Path("c.txt")]
 
     // 블록 종료 시 런타임이 자식 전원을 join한다. handle 소비에 의존하지 않는다.
-    scope sc {
+    scope work = root {
         List.each(paths, fn(p) {
-            sc.spawn(fn() {
-                let body = fs.read(p)
+            work.spawn(fn() {
+                fs.read(p)
                 log.write("read: ", p)
             })
         })
@@ -24,37 +25,32 @@ pub fn main(
     log.write("all done")
 }
 
-// 중첩 — 아직 표현할 수 없다. 열린 결정 하나가 걸려 있다.
-//
-// scope X { } 의 X가 "이미 가진 TaskScope를 쓴다"인지 "새 자식 스코프를 만들어
-// X로 묶는다"인지가 정해지지 않았다. 전자면 아래 inner가 어디서도 오지 않고,
-// 후자면 자식의 부모가 무엇인지 구문에 없다(= ambient authority).
-// 이름 해소가 이 구멍을 잡았다. 결정 전까지 주석으로 둔다.
-//
-// pub fn fan_out(
-//     outer: TaskScope,
-//     fs: FileSystem,
-//     log: Logger,
-//     groups: List[List[Path]],
-// ) effects {TaskScope.spawn, FileSystem.read, Logger.write} {
-//     List.each(groups, fn(g) {
-//         scope inner {
-//             List.each(g, fn(p) {
-//                 inner.spawn(fn() { fs.read(p) })
-//             })
-//             outer.spawn(fn() { log.write("group done") })
-//         }
-//     })
-// }
+// 중첩. 부모가 이름으로 지목되므로 어느 스코프에 붙는 태스크인지가 코드에 보인다.
+pub fn fan_out(
+    outer: TaskScope,
+    fs: FileSystem,
+    log: Logger,
+    groups: List[List[Path]],
+) effects {TaskScope.spawn, FileSystem.read, Logger.write} {
+    List.each(groups, fn(g) {
+        scope inner = outer {
+            List.each(g, fn(p) {
+                inner.spawn(fn() { fs.read(p) })
+            })
+            // 이 태스크는 inner가 아니라 outer의 수명을 따른다.
+            outer.spawn(fn() { log.write("group done") })
+        }
+    })
+}
 
 // spawn 클로저는 by-move 또는 immutable capture만 가능하다.
 pub fn broadcast(
-    sc: TaskScope,
+    root: TaskScope,
     log: Logger,
     msg: String,
 ) effects {TaskScope.spawn, Logger.write} {
-    scope sc {
-        sc.spawn(fn() { log.write(msg) })
-        sc.spawn(fn() { log.write(msg) })
+    scope s = root {
+        s.spawn(fn() { log.write(msg) })
+        s.spawn(fn() { log.write(msg) })
     }
 }
diff --git a/samples/05_move_errors.cool b/samples/05_move_errors.cool
index 51ed26a..000a3d7 100644
--- a/samples/05_move_errors.cool
+++ b/samples/05_move_errors.cool
@@ -64,7 +64,7 @@ pub fn misuse_affine_closure(own f: File) -> fn() effects {File.close} {
 
 // [E-spawn-capture] spawn 클로저의 mutable capture
 pub fn spawn_mutable(sc: TaskScope, mut counter: Int) effects {TaskScope.spawn} {
-    scope sc {
+    scope s = sc {
         sc.spawn(fn() { counter = counter + 1 })
         // ERROR: spawn 클로저는 mutable 참조를 capture할 수 없음
     }
diff --git a/samples/09_type_errors.cool b/samples/09_type_errors.cool
new file mode 100644
index 0000000..bd10df2
--- /dev/null
+++ b/samples/09_type_errors.cool
@@ -0,0 +1,131 @@
+// 09. 타입 검사기가 거부해야 하는 코드
+//
+// 이 파일에는 외부 타입이 하나도 없다. 전부 이 모듈 안에서 정의되므로
+// 검사기가 TUnknown으로 빠져나갈 구석이 없다 — 이빨이 있는지 보는 파일이다.
+
+pub enum Shape {
+    Circle(Int),
+    Rect(Int, Int),
+    Point,
+}
+
+pub copyable struct Box {
+    width: Int,
+    label: String,
+}
+
+pub fn area(s: Shape) -> Int {
+    match s {
+        Circle(r) => r * r,
+        Rect(w, h) => w * h,
+        Point => 0,
+    }
+}
+
+// --- 여기서부터 전부 오류다 ---
+
+// [E-type-if-cond] if의 조건은 Bool이어야 한다
+pub fn bad_cond(n: Int) -> Int {
+    if n {
+        1
+    } else {
+        2
+    }
+}
+
+// [E-type-if-branches] 두 분기의 타입이 달라서는 안 된다
+pub fn bad_branches(c: Bool) -> Int {
+    if c {
+        1
+    } else {
+        "둘"
+    }
+}
+
+// [E-type-return] 본문이 남기는 값이 선언된 반환 타입과 달라서는 안 된다
+pub fn bad_return(n: Int) -> String {
+    n + 1
+}
+
+// [E-type-arity] 인자 개수
+pub fn bad_arity(s: Shape) -> Int {
+    area(s, s)
+}
+
+// [E-type-arg] 인자 타입
+pub fn bad_arg(b: Box) -> Int {
+    area(b)
+}
+
+// [E-type-arith] 산술의 피연산자는 Int
+pub fn bad_arith(b: Box) -> Int {
+    b.width + b.label
+}
+
+// [E-type-field] 없는 필드
+pub fn bad_field(b: Box) -> Int {
+    b.height
+}
+
+// [E-type-struct-missing] 빠진 필드
+pub fn bad_struct_missing() -> Box {
+    Box { width: 1 }
+}
+
+// [E-type-struct-unknown] 없는 필드에 대입
+pub fn bad_struct_unknown() -> Box {
+    Box { width: 1, label: "a", depth: 2 }
+}
+
+// [E-type-struct-field] 필드 타입
+pub fn bad_struct_field() -> Box {
+    Box { width: "넓이", label: "a" }
+}
+
+// [E-type-match-arms] match 팔의 타입이 서로 달라서는 안 된다
+pub fn bad_arms(s: Shape) -> Int {
+    match s {
+        Circle(_) => 1,
+        Rect(_, _) => "둘",
+        Point => 3,
+    }
+}
+
+// [E-type-pattern] 패턴이 match 대상과 다른 타입
+pub fn bad_pattern(b: Box) -> Int {
+    match b {
+        Circle(r) => r,
+        _ => 0,
+    }
+}
+
+// [E-type-let] let의 타입 주석
+pub fn bad_let() -> Int {
+    let x: Int = "하나"
+    x
+}
+
+// [E-type-assign] 대입의 타입
+pub fn bad_assign() -> Int {
+    let mut x = 1
+    x = "하나"
+    x
+}
+
+// [E-type-try] ?는 Result에만
+pub fn bad_try(n: Int) -> Int {
+    n?
+}
+
+// [E-type-eq] 다른 타입끼리의 비교
+pub fn bad_eq(n: Int, s: String) -> Bool {
+    n == s
+}
+
+// [E-type-list] 리스트 원소의 타입이 서로 다름
+pub fn bad_list() -> List[Int] {
+    [1, "둘", 3]
+}
+
+// [E-type-const] 상수의 값
+pub const LIMIT: Int = "많이"
diff --git a/samples/README.md b/samples/README.md
index a121781..aaecdbe 100644
--- a/samples/README.md
+++ b/samples/README.md
@@ -16,13 +16,17 @@
 | 06_affine_closure | callable affinity (fn vs affine fn), own과의 직교성 |
 | 07_module_interface | interface artifact가 담아야 할 것 전부 |
 | 08_syntax_errors | **파서가** 거부해야 하는 코드 |
+| 09_type_errors | **타입 검사기가** 거부해야 하는 코드 (외부 타입 0개) |
 
-05와 08은 통과하면 안 되는 파일이다. 각 함수 주석의 `[E-...]` 태그가 기대
-진단이다. 둘의 목적이 다르다 — **05는 구문은 맞지만 검사기가 거부해야 하고,
-08은 파서가 거부해야 한다.** 그래서 파일을 나눴다: 한 파일에 섞으면 파서가
-첫 오류에서 멈춰 검사기 케이스에 영영 도달하지 못한다.
+05, 08, 09는 통과하면 안 되는 파일이다. 각 함수 주석의 `[E-...]` 태그가 기대
+진단이며, 셋의 목적이 다르다 — **08은 파서가, 09는 타입 검사기가, 05는 아직
+없는 move/affinity 검사가** 거부해야 한다. 단계별로 파일을 나눈 이유는
+앞 단계가 첫 오류에서 멈추면 뒤 단계 케이스에 영영 도달하지 못하기 때문이다.
 
-오류 복구는 아직 없다. 파서는 첫 오류에서 멈춘다.
+09에는 외부 타입이 하나도 없다. 전부 모듈 안에서 정의되므로 검사기가
+TUnknown으로 빠져나갈 구석이 없다 — 검사기에 이빨이 있는지 보는 파일이다.
+
+파서는 첫 오류에서 멈춘다(오류 복구 미구현). 타입 검사기는 오류를 전부 모은다.
 
 ## 확정된 표기
 
@@ -41,5 +45,7 @@
 - 문 구분은 줄바꿈 (Go식 자동 삽입)
 - 블록은 식. 마지막 식이 값이고 `return`은 조기 탈출 전용
 - `if`와 `match`는 식. `match` 가드 없음
+- scope: `scope inner = outer { ... }` — 부모를 구문에 명시
+- 타입 이름은 그 타입의 함수 이름공간: `String.len(s)`, `File.close(f)`
 - 리스트 리터럴 `[a, b, c]`, 빈 리터럴은 타입 주석 필요
 - 오류 전파 `?`는 `Result` 전용
diff --git a/test/test_coollang.ml b/test/test_coollang.ml
index d0b5e90..f75eb9d 100644
--- a/test/test_coollang.ml
+++ b/test/test_coollang.ml
@@ -306,9 +306,10 @@ let () =
   check "match"
     (one "fn f() {\n  match e {\n    A(_) => 1,\n    _ => 2,\n  }\n}"
     = "(fn f () (block (match e ((A _) => 1) (_ => 2))))");
-  check "scope"
-    (one "fn f() {\n  scope sc {\n    sc.spawn(g)\n  }\n}"
-    = "(fn f () (block (scope sc (block (call (. sc spawn) g)))))");
+  check "scope는 부모를 명시한다"
+    (one "fn f(root: TaskScope) {\n  scope sc = root {\n    sc.spawn(g)\n  }\n}"
+    = "(fn f (root:TaskScope) (block (scope sc = root (block (call (. sc \
+       spawn) g)))))");
   check "struct 리터럴"
     (one "fn f() {\n  H { a: 1 }\n}" = "(fn f () (block (struct H (a 1))))")
 
@@ -411,10 +412,15 @@ let () =
 (* --- scope 머리는 지역 바인딩이어야 한다 --- *)
 
 let () =
-  check "지역 바인딩이 아닌 scope 이름"
-    (has_err "fn f() {\n  scope sc {\n    sc\n  }\n}" "지역 바인딩이 아닙니다");
-  check "파라미터로 온 scope는 통과"
-    (resolve_errs "fn f(sc: TaskScope) {\n  scope sc {\n    sc\n  }\n}" = [])
+  check "부모 scope가 지역 바인딩이 아니면 오류"
+    (has_err "fn f() {\n  scope s = root {\n    s\n  }\n}" "지역 바인딩이 아닙니다");
+  check "파라미터로 온 부모는 통과"
+    (resolve_errs "fn f(root: TaskScope) {\n  scope s = root {\n    s\n  }\n}"
+    = []);
+  check "자식 scope 이름은 블록 안에서만 산다"
+    (resolve_ext
+       "fn f(root: TaskScope) {\n  scope s = root {\n    s\n  }\n  s\n}"
+    = [ "TaskScope"; "s" ])
 
 (* --- variant는 구문이 아니라 이름 해소가 판정한다 --- *)
 
@@ -468,3 +474,126 @@ let () =
             errors;
           check (f ^ " 이름 해소") false)
     files
+
+(* ================================================================== *)
+(* 타입 검사                                                           *)
+(* ================================================================== *)
+
+let type_errs src =
+  List.map (fun (e : Typecheck.error) -> e.msg) (Typecheck.check (parse_ok src))
+
+let type_ok src = type_errs src = []
+
+let type_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)
+    (type_errs src)
+
+(* --- 제네릭은 호출 지점에서 지역 unification으로 풀린다 --- *)
+
+let () =
+  check "제네릭 인스턴스화" (type_ok "fn id[a](x: a) -> a\nfn f() -> Int {\n  id(1)\n}");
+  check "제네릭 결과가 반환 타입과 안 맞으면 오류"
+    (type_has "fn id[a](x: a) -> a\nfn f() -> String {\n  id(1)\n}" "String");
+  check "명시적 인스턴스화의 인자 개수"
+    (type_has "fn id[a](x: a) -> a\nfn f() -> Int {\n  id[Int, Int](1)\n}"
+       "타입 인자 1개가 필요한데 2개");
+  check "고차 함수의 클로저 파라미터 타입은 기대 타입에서 온다"
+    (type_ok
+       "fn map[a, b](xs: List[a], f: fn(a) -> b) -> List[b]\n\
+        fn g(xs: List[Int]) -> List[Int] {\n\
+       \  map(xs, fn(x) { x + 1 })\n\
+        }");
+  check "클로저 본문의 타입 오류는 잡힌다"
+    (type_has
+       "fn map[a, b](xs: List[a], f: fn(a) -> b) -> List[b]\n\
+        fn g(xs: List[Int]) -> List[Int] {\n\
+       \  map(xs, fn(x) { x + \"1\" })\n\
+        }"
+       "산술 연산자")
+
+(* --- Result와 ? --- *)
+
+let () =
+  check "?는 Result를 벗긴다"
+    (type_ok
+       "fn f(x: Result[Int, String]) -> Result[Int, String] {\n\
+       \  let a = x?\n\
+       \  Ok(a)\n\
+        }");
+  check "?는 Result 반환 함수 안에서만"
+    (type_has "fn f(x: Result[Int, String]) -> Int {\n  x?\n}"
+       "Result를 반환하는 함수 안에서만")
+
+(* --- enum과 struct --- *)
+
+let () =
+  let e = "enum E {\n  A(Int),\n  B,\n}\n" in
+  check "생성자 호출" (type_ok (e ^ "fn f() -> E {\n  A(1)\n}"));
+  check "생성자 인자 타입" (type_has (e ^ "fn f() -> E {\n  A(\"x\")\n}") "인자");
+  check "인자 없는 생성자" (type_ok (e ^ "fn f() -> E {\n  B\n}"));
+  check "match는 값을 낸다"
+    (type_ok
+       (e
+      ^ "fn f(x: E) -> Int {\n  match x {\n    A(n) => n,\n    B => 0,\n  }\n}"
+       ));
+  check "제네릭 struct 필드"
+    (type_ok "struct P[a] {\n  v: a,\n}\nfn f(p: P[Int]) -> Int {\n  p.v\n}");
+  check "제네릭 struct 필드 타입 오류"
+    (type_has "struct P[a] {\n  v: a,\n}\nfn f(p: P[Int]) -> String {\n  p.v\n}"
+       "String")
+
+(* --- capability 메서드 --- *)
+
+let () =
+  let c = "capability G {\n  fn pay(n: Int) -> Bool\n}\n" in
+  check "capability 메서드 타입"
+    (type_ok (c ^ "fn f(g: G) -> Bool {\n  g.pay(1)\n}"));
+  check "없는 메서드"
+    (type_has (c ^ "fn f(g: G) -> Bool {\n  g.nope(1)\n}") "메서드가 없습니다");
+  check "메서드 인자 타입"
+    (type_has (c ^ "fn f(g: G) -> Bool {\n  g.pay(\"x\")\n}") "인자")
+
+(* --- 외부 이름은 검사를 막지 않는다 --- *)
+
+let () =
+  check "모르는 타입은 무엇과도 맞는다"
+    (type_ok "fn f(w: Widget) -> Int {\n  w.anything(1, 2)\n}");
+  check "모르는 것을 틀렸다고 말하지 않는다" (type_ok "fn f(w: Widget) -> Widget {\n  w\n}")
+
+(* --- affinity는 타입 검사가 소유하지 않는다 --- *)
+
+let () =
+  check "affine fn과 fn은 타입 동등성에서 구분되지 않는다"
+    (type_ok "fn f() -> affine fn() {\n  fn() {\n    unit\n  }\n}")
+
+(* --- 샘플 --- *)
+
+let () =
+  let dir = "../samples" in
+  let ok_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" && f <> "09_type_errors.cool")
+    |> List.sort compare
+  in
+  List.iter
+    (fun f ->
+      match Driver.typecheck (Filename.concat dir f) with
+      | Ok () -> ()
+      | Error errors ->
+          List.iter
+            (fun e -> Printf.printf "  %s\n" (Driver.string_of_error e))
+            errors;
+          check (f ^ " 타입 검사") false)
+    ok_files;
+  match Driver.typecheck (Filename.concat dir "09_type_errors.cool") with
+  | Ok () -> check "09는 타입 오류를 내야 한다" false
+  | Error errors ->
+      check "09의 오류를 전부 모은다 (첫 오류에서 멈추지 않는다)" (List.length errors >= 18)