diff --git a/.gitignore b/.gitignore
index ff0165c..d9d67bd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,6 @@
 .DS_Store
 target/
 .mooncakes/
-.moonagent/
\ No newline at end of file
+.moonagent/
+
+*.zip
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000..59ed047
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "contest-2025-data"]
+	path = contest-2025-data
+	url = https://github.com/moonbitlang/contest-2025-data.git
diff --git a/batch_run.py b/batch_run.py
new file mode 100644
index 0000000..2f9380b
--- /dev/null
+++ b/batch_run.py
@@ -0,0 +1,39 @@
+import os
+import asyncio
+
+
+async def check_file(filepath):
+    proc = await asyncio.create_subprocess_exec(
+        "moon",
+        "run",
+        "src/bin/main.mbt",
+        "--",
+        "--typecheck",
+        filepath,
+        stdout=asyncio.subprocess.PIPE,
+        stderr=asyncio.subprocess.PIPE,
+    )
+    stdout, stderr = await proc.communicate()
+    if proc.returncode != 0:
+        print(f"""
+[{proc.returncode}] Error in file {filepath}:
+======== STDOUT ========
+{stdout.decode()}
+======== STDERR ========
+{stderr.decode()}
+""")
+    else:
+        print(f"File {filepath} compiled successfully.")
+
+
+async def main():
+    tasks = []
+    for file in os.listdir("contest-2025-data/test_cases/mbt"):
+        if file.endswith(".mbt"):
+            filepath = os.path.join("contest-2025-data/test_cases/mbt", file)
+            tasks.append(check_file(filepath))
+    await asyncio.gather(*tasks)
+
+
+if __name__ == "__main__":
+    asyncio.run(main())
diff --git a/contest-2025-data b/contest-2025-data
new file mode 160000
index 0000000..b296c16
--- /dev/null
+++ b/contest-2025-data
@@ -0,0 +1 @@
+Subproject commit b296c1620353bf96d135a123533ba5d2698893e7
diff --git a/src/bin/main.mbt b/src/bin/main.mbt
index b9281a9..83bd70a 100644
--- a/src/bin/main.mbt
+++ b/src/bin/main.mbt
@@ -1,6 +1,22 @@
+///|
+fn[T] println_panic(msg : String) -> T {
+  println("[FTL] \{msg}")
+  @sys.exit(1)
+  panic()
+}
+
+///|
+fn println_debug(msg : String) -> Unit {
+  println("[DBG] \{msg}")
+}
+
 ///|
 fn main {
-  let argv = @sys.get_cli_args()
+  guard @sys.get_cli_args() is [_, .. argv] else {
+    println_panic("Failed to get CLI arguments")
+  }
+  let argv = argv.to_array()
+  println_debug("CLI arguments: \{argv}")
   let typecheck_only = Ref::new(false)
   let mut in_file = None
   let out_file = Ref::new("a.s")
@@ -15,44 +31,55 @@ fn main {
       (
         "--output",
         "-o",
-        @ArgParser.String(s => out_file.val = s),
+        @ArgParser.Set_string(out_file),
         "Output file (default: a.s)",
       ),
     ],
     fn(s) {
       if !in_file.is_empty() {
-        abort("multiple files are given")
+        println_panic("multiple files are given")
       }
       in_file = Some(s)
     },
     (
       #|Lilunar: Lil-Ran's experimental MiniMoonBit to RISC-V compiler for MGPIC-2025.
       #|
-      #|Usage: lilunar [options] <input-file>
-      #|
-      #|Options:
-      #|  --typecheck          Only run type checking
-      #|  -o, --output <file>  Output file (default: a.s)
+      #| usage: lilunar [options] <input-file>
       #|
     ),
     argv,
   ) catch {
-    e => abort("Argument parsing error: \{e}")
+    @ArgParser.ErrorMsg(msg) => println_panic("Argument parsing error: \{msg}")
+    e => println_panic("Unknown error during argument parsing: \{e}")
   }
-  let file = in_file.unwrap_or_else(abort("no input file provided"))
+  let file = in_file.unwrap_or_else(() => println_panic(
+    "no input file provided",
+  ))
+  println_debug("Compiling file: \{file}")
   let contents = @fs.read_file_to_string(file) catch {
-    e => abort("Failed to read file \{file}: \{e}")
+    @fs.IOError(msg) => println_panic("Failed to read file \{file}: \{msg}")
   }
+  println_debug(
+    (
+      #|
+      #|================================
+      $|\{contents}
+      #|================================
+    ),
+  )
   let program = try
     contents
     |> @parser.tokenize()
     |> @parser.parse_program()
     |> @typecheck.typecheck()
   catch {
-    e => abort("Parsing or type checking error: \{e}")
+    @parser.TokenizeError(msg) => println_panic("Tokenization error: \{msg}")
+    @parser.ParseError(msg) => println_panic("Parse error: \{msg}")
+    @typecheck.TypeCheckError(msg) => println_panic("Type check error: \{msg}")
+    _ => println_panic("Unknown error during compilation")
   }
   if typecheck_only.val {
-    println("Type checking passed.")
+    println_debug("Type checking passed.")
     return
   }
 
diff --git a/src/typecheck/program.mbt b/src/typecheck/program.mbt
index 4691d2d..398c064 100644
--- a/src/typecheck/program.mbt
+++ b/src/typecheck/program.mbt
@@ -98,56 +98,63 @@ pub fn Context::check_program(
   self : Context,
   program : @parser.Program,
 ) -> Program raise TypeCheckError {
-  self.collect_struct_names(program)
-  self.collect_function_types(program)
-  let struct_defs : Map[String, StructDef] = Map::new()
-  for name, struct_def in program.struct_defs {
-    let checked_struct_def = self.check_struct_def(struct_def)
-    struct_defs.set(name, checked_struct_def)
-    self.struct_defs.set(name, checked_struct_def)
-  }
-  let top_functions : Map[String, TopFunction] = Map::new()
-  for name, func in program.top_functions {
-    let checked_func = self.check_top_function(func)
-    top_functions.set(name, checked_func)
-    self.func_types.set(
-      name,
-      Function(checked_func.param_list.map(p => p.ty), checked_func.ret_ty),
-    )
-  }
-  let top_lets : Map[String, TopLet] = Map::new()
-  for name, let_def in program.top_lets {
-    let checked_let = self.check_top_let(let_def)
-    top_lets.set(name, checked_let)
-    self.type_env.set(name, checked_let.ty)
-  }
-  { top_lets, top_functions, struct_defs }
-}
-
-///|
-pub fn Context::collect_struct_names(
-  self : Context,
-  program : @parser.Program,
-) -> Unit raise TypeCheckError {
+  // 收集结构体名称
   for name, _ in program.struct_defs {
     if self.struct_defs.contains(name) {
       raise TypeCheckError("Duplicate struct definition: \{name}")
     }
     self.struct_defs.set(name, { name, fields: [] })
   }
+  // 此时除泛型外，所有存在的类型都已确定
+  // 收集结构体定义
+  let struct_defs : Map[String, StructDef] = Map::new()
+  for name, struct_def in program.struct_defs {
+    let checked_struct_def = self.check_struct_def(struct_def)
+    struct_defs.set(name, checked_struct_def)
+    self.struct_defs.set(name, checked_struct_def)
+  }
+  // 收集顶层函数声明
+  for name, func in program.top_functions {
+    self.func_types.set(name, self.check_top_function_type_decl(func))
+  }
+  // 补充内建函数类型
+  self.add_intrinsic_functions()
+  // 此时顶层变量初始化表达式可引用的类型都已确定
+  // 收集顶层变量类型和表达式
+  let top_lets : Map[String, TopLet] = Map::new()
+  for name, let_def in program.top_lets {
+    let checked_let = self.check_top_let(let_def)
+    top_lets.set(name, checked_let)
+    self.type_env.set(name, checked_let.ty)
+  }
+  // 此时所有顶层标识符的类型都已确定
+  // 检查顶层函数定义
+  let top_functions : Map[String, TopFunction] = Map::new()
+  for name, func in program.top_functions {
+    top_functions.set(name, self.check_top_function_body(func))
+  }
+  { top_lets, top_functions, struct_defs }
 }
 
 ///|
-pub fn Context::collect_function_types(
-  self : Context,
-  program : @parser.Program,
-) -> Unit {
-  for name, _ in program.top_functions {
-    let func_type = self.new_type_var()
-    self.func_types.set(name, func_type)
-  }
-  for name, _ in program.top_lets {
-    let let_type = self.new_type_var()
-    self.type_env.set(name, { kind: let_type, mutable: false })
+pub fn Context::add_intrinsic_functions(self : Context) -> Unit {
+  let map = Map::of([
+    ("read_int", Function([], Int)),
+    ("print_int", Function([Int], Unit)),
+    ("read_char", Function([], Int)),
+    ("print_char", Function([Int], Unit)),
+    ("print_endline", Function([], Unit)),
+    ("int_of_float", Function([Double], Int)),
+    ("float_of_int", Function([Int], Double)),
+    ("truncate", Function([Double], Int)),
+    ("floor", Function([Double], Double)),
+    ("abs_float", Function([Double], Double)),
+    ("sqrt", Function([Double], Double)),
+    ("sin", Function([Double], Double)),
+    ("cos", Function([Double], Double)),
+    ("atan", Function([Double], Double)),
+  ])
+  for name, ty in map {
+    self.type_env.set(name, { kind: ty, mutable: false })
   }
 }
diff --git a/src/typecheck/top_function.mbt b/src/typecheck/top_function.mbt
index db8c3e6..0a65b27 100644
--- a/src/typecheck/top_function.mbt
+++ b/src/typecheck/top_function.mbt
@@ -13,51 +13,78 @@ pub(all) struct TopFunction {
 } derive(Show)
 
 ///|
-pub fn Context::check_top_function(
+pub fn Context::check_top_function_body(
   self : Context,
   func : @parser.Function,
 ) -> TopFunction raise TypeCheckError {
   // XXX: 目前的泛型不是真正的泛型，只是只能归一成单个类型的类型变量
   if func.user_defined_type is Some(UserDefined(udt)) {
-    self.type_env.set("$Generic$\{udt}", {
-      kind: self.new_type_var(),
-      mutable: false,
-    })
-  }
-  //
-  let param_list : Array[Param] = func.params.map(param => {
-    let (param_name, param_type) = param
-    match param_type {
-      Some(ty) => { name: param_name, ty: self.check_parser_type(ty).kind }
-      None => { name: param_name, ty: self.new_type_var() }
+    guard self.type_env.get("$GenericFunc$\{func.id}$\{udt}") is Some(tv) else {
+      raise TypeCheckError(
+        "Internal error: generic type variable for function '\{func.id}' not found.",
+      )
     }
-  })
-  let ret_ty = match func.return_type {
-    Some(ty) => self.check_parser_type(ty).kind
-    None => self.new_type_var()
+    self.type_env.set("$Generic$\{udt}", tv)
   }
-  let func_type = Function(param_list.map(p => p.ty), ret_ty)
-  self.type_env.set(func.id, { kind: func_type, mutable: false })
-  //
+  let param_names = func.params.map(param => param.0)
+  let param_list = []
+  guard self.func_types.get(func.id) is Some(Function(param_types, ret_ty)) else {
+    raise TypeCheckError("Function type for '\{func.id}' not found.")
+  }
+  self.type_env.set(func.id, {
+    kind: Function(param_types, ret_ty),
+    mutable: false,
+  })
   self.enter_scope()
   self.current_func_ret_ty = Some(ret_ty)
-  //
-  for param in param_list {
-    let { name, ty } = param
-    self.type_env.set(name, { kind: ty, mutable: false })
+  for i in 0..<param_names.length() {
+    self.type_env.set(param_names[i], { kind: param_types[i], mutable: false })
+    param_list.push(Param::{ name: param_names[i], ty: param_types[i] })
   }
-  //
   let checked_body = self.check_block_expr(Block(func.body))
   if !self.is_type_compatible(checked_body.ty, ret_ty) {
     raise TypeCheckError(
       "Function '\{func.id}' return type mismatch: expected \{ret_ty}, got \{checked_body.ty}",
     )
   }
-  //
   self.exit_scope()
   if func.user_defined_type is Some(UserDefined(udt)) {
     self.type_env.local_.remove("$Generic$\{udt}")
   }
-  //
   { fname: func.id, param_list, ret_ty, body: checked_body }
 }
+
+///|
+pub fn Context::check_top_function_type_decl(
+  self : Context,
+  func : @parser.Function,
+) -> TypeKind raise TypeCheckError {
+  // XXX: 目前的泛型不是真正的泛型，只是只能归一成单个类型的类型变量
+  if func.user_defined_type is Some(UserDefined(udt)) {
+    let generic_type = { kind: self.new_type_var(), mutable: false }
+    // 用于函数内类型查找
+    self.type_env.set("$Generic$\{udt}", generic_type)
+    // 用于稍后检查函数体时能使用同一个 type_var
+    self.type_env.set("$GenericFunc$\{func.id}$\{udt}", generic_type)
+  }
+  let param_list : Array[Param] = func.params.map(param => {
+    let (param_name, param_type) = param
+    let ty = param_type.or_error(
+      TypeCheckError(
+        "Parameter type annotation is required for top function; found none for '\{param_name}' in function '\{func.id}'.",
+      ),
+    )
+    { name: param_name, ty: self.check_parser_type(ty).kind }
+  })
+  let ret_ty = func.return_type.or_error(
+    TypeCheckError(
+      "Return type annotation is required for top function; found none in function '\{func.id}'.",
+    ),
+  )
+  let ret_ty = self.check_parser_type(ret_ty).kind
+  let func_type = Function(param_list.map(p => p.ty), ret_ty)
+  if func.user_defined_type is Some(UserDefined(udt)) {
+    self.type_env.local_.remove("$Generic$\{udt}")
+  }
+  func_type
+}
diff --git a/src/typecheck/typecheck_test.mbt b/src/typecheck/typecheck_test.mbt
index 5e3d0d6..3f81b48 100644
--- a/src/typecheck/typecheck_test.mbt
+++ b/src/typecheck/typecheck_test.mbt
@@ -759,7 +759,7 @@ test "Top Function TypeCheck Test" {
   // parse
   let tokens = @parser.tokenize(code)
   let program = @parser.parse_program(tokens)
-  let _ = ctx.check_top_function(program.top_functions["fib"])
+  let _ = ctx.check_top_function_body(program.top_functions["fib"])
 
 }
 
diff --git a/src/typecheck/typechecker.mbt b/src/typecheck/typechecker.mbt
index 7aaa1ce..7bf364c 100644
--- a/src/typecheck/typechecker.mbt
+++ b/src/typecheck/typechecker.mbt
@@ -3,10 +3,10 @@ pub fn typecheck(program : @parser.Program) -> Program raise TypeCheckError {
   let ctx = Context::new()
   let checked_program = ctx.check_program(program)
   let result = ctx.substitute_type_var(checked_program)
-
-  // XXX: do not to_string
-  if result.to_string().contains("TypeVar") {
-    raise TypeCheckError("unsubstituted type variable remains")
+  for v in ctx.type_vars.values() {
+    if ctx.deref_type_var(v) is TypeVar(_) {
+      raise TypeCheckError("unsubstituted type variable remains")
+    }
   }
   result
 }