coollang/lib/typecheck.ml

(* 타입 검사.

   범위: 이 모듈 안에서 아는 것만 검사한다. 외부 이름은 TUnknown이 되어
   무엇과도 맞는다 — 모르는 것을 틀렸다고 말하지 않는다.

   제네릭 해소는 호출 지점의 지역 unification이다. 함수 하나를 넘어가지
   않으므로 전역 추론이 아니다. *)

open Ast
module T = Types

type error = { pos : Token.pos; msg : string }

type scheme = {
  s_gen : string list; (* 타입 파라미터 *)
  s_eff_gen : string list; (* effect 파라미터 *)
  (* (own, 타입). 무표기는 빌림 *)
  s_params : (bool * T.t) list;
  s_eff : T.eff; (* 이 함수를 부르면 수행되는 effect *)
  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 *)
  (* 가져온 모듈의 별칭. `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;
}

let err env pos msg = env.errors <- { pos; msg } :: env.errors

let expr_pos (e : expr) : Token.pos =
  match e with
  | E_lit (_, p)
  | E_ident (_, p)
  | E_list (_, p)
  | E_struct { pos = p; _ }
  | E_if { pos = p; _ }
  | E_match { pos = p; _ }
  | E_scope { pos = p; _ }
  | E_call { pos = p; _ }
  | E_field { pos = p; _ }
  | E_inst { pos = p; _ }
  | E_try { pos = p; _ }
  | E_unary { pos = p; _ }
  | E_binary { pos = p; _ }
  | E_crash { pos = p; _ } ->
      p
  | E_closure c -> c.cl_pos
  | E_block b -> b.block_pos

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 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 { modl; name; args; _ } -> (
      let args =
        List.filter_map
          (function TA_ty t -> Some (conv env gen t) | TA_eff _ -> None)
          args
      in
      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 if modl = None then name else "" 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; eff; ret; _ } ->
      T.TFn
        {
          affine;
          params =
            List.map
              (fun (p : fn_param_ty) -> (p.pt_own, conv env gen p.pt_ty))
              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);
        }

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
  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 -> (p.p_own, 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
  let esub = List.map (fun v -> (v, T.fresh_eff ())) s.s_eff_gen in
  ( List.map (fun (o, t) -> (o, T.subst sub esub t)) 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
  let esub = List.map (fun v -> (v, T.fresh_eff ())) s.s_eff_gen in
  ( List.map (fun (o, t) -> (o, T.subst sub esub t)) s.s_params,
    T.subst_eff esub s.s_eff,
    T.subst sub esub 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
  (* crash는 돌아오지 않는다. 타입은 Never이고 어떤 자리에도 놓인다 *)
  | E_crash { msg; pos } ->
      let t = infer env msg in
      if not (T.unify t T.TString) then
        mismatch env pos T.TString t "crash의 메시지";
      T.TNever
  | 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, eff, ret = instantiate s in
                      T.TFn { affine = false; params; eff; ret }
                  | None -> (
                      match Hashtbl.find_opt env.ctors n with
                      | Some enum -> nullary_ctor env enum n
                      | None ->
                          env.saw_unknown <- true;
                          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에 팔이 없습니다";
      check_exhaustive env s arms pos;
      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)

(* 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
  | 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 (fun (o, t) -> Some (o, t)) params, Some ret)
    | _ -> (List.map (fun _ -> None) c.cl_params, None)
  in
  push env;
  let param_tys =
    List.map2
      (fun (p : cl_param) exp ->
        let t =
          match p.cp_ty with
          | Some a -> conv env [] a
          | None -> ( match exp with Some (_, t) -> t | None -> T.TUnknown)
        in
        (* 기대 타입이 소유를 말하는데 리터럴이 안 적었으면 오류다.
           반대도 오류다 — 빌리는 자리에 소유를 주장하면 빌린 값을 소비한다.
           방향을 다루려면 부분 타입이 필요하고 우리에겐 없다. *)
        (match exp with
        | Some (o, _) when o <> p.cp_own ->
            err env c.cl_pos
              (Printf.sprintf "클로저 파라미터 %s의 소유권이 기대와 다릅니다 (기대: %s, 적힌 것: %s)"
                 p.cp_name
                 (if o then "own" else "빌림")
                 (if p.cp_own then "own" else "빌림"))
        | _ -> ());
        bind env p.cp_name t;
        (p.cp_own, t))
      c.cl_params expected_params
  in
  let declared_ret = Option.map (conv env []) c.cl_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_ret;
  pop env;
  T.TFn { affine = false; params = param_tys; eff; 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 = List.map (fun t -> (false, t)) params;
                       eff = [];
                       ret;
                     })
            | None -> (
                match Hashtbl.find_opt env.fns n with
                | Some s ->
                    let params, eff, ret = instantiate s in
                    Some (T.TFn { affine = false; params; eff; ret })
                | None -> None)))
    | _ -> (
        match T.resolve (infer env callee) with
        | T.TFn _ as t -> Some t
        | _ -> None)
  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; 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)
             (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
            (* 먼저 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

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 (fun t -> (false, T.subst sub [] t)) ts
        | None -> []
      in
      T.TFn
        {
          affine = false;
          params;
          eff = [];
          ret = T.TCon (enum, List.map snd sub);
        }

and infer_field env obj name pos =
  (* capability 메서드는 값을 통해서만 부를 수 있다. 타입 이름으로 부를 수 있으면
     capability 없이 effect를 수행하게 되어 보안 정리 (i)이 무너진다. *)
  (match obj with
  | E_ident (n, _) when lookup env n = None && Hashtbl.mem env.caps n ->
      err env pos
        (Printf.sprintf
           "capability %s의 메서드는 값을 통해서만 부를 수 있습니다 (%s를 파라미터로 받아야 합니다)" n n)
  | _ -> ());
  match obj with
  | E_ident (a, _) when lookup env a = None && List.mem a env.aliases -> (
      (* 모듈 별칭을 통한 접근. 가져온 표면은 "Alias.name" 키로 들어와 있다. *)
      let key = a ^ "." ^ name in
      let unknown () =
        err env pos (Printf.sprintf "%s에 %s이(가) 없습니다" a name);
        T.TUnknown
      in
      match Hashtbl.find_opt env.consts key with
      | Some t -> t
      | None -> (
          match Hashtbl.find_opt env.fns key with
          | Some s ->
              let params, eff, ret = instantiate s in
              T.TFn { affine = false; params; eff; ret }
          | None -> (
              match Hashtbl.find_opt env.ctors key with
              | Some enum -> (
                  match Hashtbl.find_opt env.enums enum with
                  | Some (_, variants)
                    when List.assoc_opt key variants = Some [] ->
                      nullary_ctor env enum key
                  | Some _ -> ctor_fn env enum key
                  | None -> T.TUnknown)
              | None -> unknown ())))
  | _ -> (
      let t = infer env obj in
      match T.resolve t with
      | T.TUnknown -> T.TUnknown
      | T.TCon (cname, args) -> (
          match Hashtbl.find_opt env.structs cname with
          | Some (gen, fields) -> (
              let sub = List.map2 (fun v a -> (v, a)) gen (adjust gen args) in
              match List.assoc_opt name fields with
              | Some ft -> T.subst sub [] ft
              | None ->
                  err env pos (Printf.sprintf "%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, 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
  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, eff, ret = instantiate_with s tys in
            T.TFn { affine = false; params; eff; 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 { 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)

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
  (* 꼬리가 아닌 자리의 식은 값을 남기면 안 된다. 남긴 값은 버려지는데,
     그 값이 Result면 실패가 조용히 사라진다 — 철학 1과 정면으로 부딪힌다.
     일부러 버리려면 let _ = 로 적는다. 버린다는 사실이 코드에 보여야 한다. *)
  | S_expr e -> (
      let t = infer env e in
      match T.resolve t with
      | T.TUnit | T.TUnknown | T.TNever -> ()
      | other ->
          err env (expr_pos e)
            (Printf.sprintf "이 식이 남기는 %s이(가) 버려집니다 (일부러 버리려면 let _ = 로 적으십시오)"
               (T.show other)))
  | 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 "대입"

(* ------------------------------------------------------------------ *)
(* 모듈                                                                *)
(* ------------------------------------------------------------------ *)

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;
      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 ?(imports : item list = []) (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;
      (* 표면을 실제로 받아온 별칭만 안다. 해소되지 않은 모듈(예: 아직 가져오지
         못한 패키지)의 별칭은 모르는 것이므로 그 아래 이름을 틀렸다고 말하지
         않는다. *)
      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
  (* 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 []
      | _ -> ())
    (imports @ 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)
      | _ -> ())
    (imports @ 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 "상수의 값"
      (* 테스트는 파라미터 없고 effect 없는 함수와 같다. 검사도 같다 —
         일반 코드와 다른 규칙을 주면 테스트만 통과하는 코드가 생긴다 *)
      | I_test { name; body; pos } ->
          env.locals <- [];
          push env;
          env.ret <- T.TUnit;
          env.performed <- [];
          env.saw_unknown <- false;
          let got = infer_block env body in
          if not (T.unify T.TUnit got) then
            mismatch env pos T.TUnit got (Printf.sprintf "테스트 \"%s\"의 본문" name);
          List.iter
            (fun (a, apos) ->
              err env apos
                (Printf.sprintf
                   "테스트는 effect를 수행할 수 없습니다 (%s) — 테스트는 capability를 받지 않습니다"
                   (T.atom_show a)))
            (List.rev (T.eff_resolve (List.map fst env.performed))
            |> List.map (fun a -> (a, pos)));
          env.performed <- [];
          pop env
      | _ -> ())
    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)