diff --git a/TODO.md b/TODO.md
index 82abaf61..08cd91a0 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,8 +1,3 @@
-top level env has checking -- for top level `Compose`
-
-- begin-type.error.i
-- begin-type-nested.error.i
-
 # books
 
 反应网编程
diff --git a/src/lang/mod/Mod.ts b/src/lang/mod/Mod.ts
index 4ab20f06..89a52d81 100644
--- a/src/lang/mod/Mod.ts
+++ b/src/lang/mod/Mod.ts
@@ -1,4 +1,5 @@
 import { Loader } from "../../loader"
+import { Checking } from "../checking"
 import { Definition } from "../definition"
 import { Env } from "../env/Env.js"
 import { Rule } from "../rule"
@@ -7,6 +8,7 @@ import { Stmt } from "../stmt/Stmt.js"
 export type Mod = {
   loader: Loader
   env: Env
+  checking: Checking
   url: URL
   text: string
   stmts: Array<Stmt>
diff --git a/src/lang/mod/createMod.ts b/src/lang/mod/createMod.ts
index 38196575..e8153792 100644
--- a/src/lang/mod/createMod.ts
+++ b/src/lang/mod/createMod.ts
@@ -1,5 +1,6 @@
 import { Loader } from "../../loader"
 import { defineBuiltinOperators } from "../builtins/defineBuiltinOperators"
+import { createChecking } from "../checking/createChecking"
 import { createEnv } from "../env/createEnv.js"
 import { Stmt } from "../stmt/Stmt.js"
 import { Mod } from "./Mod"
@@ -21,6 +22,7 @@ export function createMod(options: {
   } as Mod
 
   mod.env = createEnv(mod)
+  mod.checking = createChecking()
 
   defineBuiltinOperators(mod)
 
diff --git a/src/lang/stmts/Compose.ts b/src/lang/stmts/Compose.ts
index 96655b1a..8847d4e6 100644
--- a/src/lang/stmts/Compose.ts
+++ b/src/lang/stmts/Compose.ts
@@ -14,7 +14,9 @@ export class Compose implements Stmt {
 
   async execute(mod: Mod): Promise<void> {
     try {
-      compose(mod, mod.env, this.word, {})
+      compose(mod, mod.env, this.word, {
+        checking: mod.checking,
+      })
     } catch (error) {
       throw appendReport(error, {
         message: [
diff --git a/tests/checking/begin-type-nested.error.i b/tests/checking/begin-type-nested.error.i
index f86c94ea..02d57ce6 100644
--- a/tests/checking/begin-type-nested.error.i
+++ b/tests/checking/begin-type-nested.error.i
@@ -16,5 +16,3 @@ node cons
 end
 
 sole sole cons
-
-TODO
diff --git a/tests/checking/begin-type-nested.error.i.err b/tests/checking/begin-type-nested.error.i.err
index e48a617d..92814a68 100644
--- a/tests/checking/begin-type-nested.error.i.err
+++ b/tests/checking/begin-type-nested.error.i.err
@@ -1,25 +1,24 @@
-[lookupDefinitionOrFail] I meet undefined name.
+[unifyTypes] I fail to unify types.
 
-  name: TODO
+  left: Trivial
+  right: Trivial List
 
 [compose] I fail compose word.
 
-  word: TODO
+  word: cons
 
+ 15 |  'A List :value!
  16 |end
  17 |
  18 |sole sole cons
  19 |
- 20 |TODO
- 21 |
 
 [Compose.execute] I fail to compose word.
 
-  word: TODO
+  word: cons
 
+ 15 |  'A List :value!
  16 |end
  17 |
  18 |sole sole cons
  19 |
- 20 |TODO
- 21 |
diff --git a/tests/checking/begin-type.error.i b/tests/checking/begin-type.error.i
index edbda2b4..806f2577 100644
--- a/tests/checking/begin-type.error.i
+++ b/tests/checking/begin-type.error.i
@@ -6,5 +6,3 @@ type Trivial -- Type end
 node sole -- Trivial :value! end
 
 sole add1
-
-TODO
diff --git a/tests/checking/begin-type.error.i.err b/tests/checking/begin-type.error.i.err
index c32b4f8c..7a4088ac 100644
--- a/tests/checking/begin-type.error.i.err
+++ b/tests/checking/begin-type.error.i.err
@@ -1,25 +1,24 @@
-[lookupDefinitionOrFail] I meet undefined name.
+[unifyTypes] I fail to unify types.
 
-  name: TODO
+  left: Trivial
+  right: Nat
 
 [compose] I fail compose word.
 
-  word: TODO
+  word: add1
 
+  5 |type Trivial -- Type end
   6 |node sole -- Trivial :value! end
   7 |
   8 |sole add1
   9 |
- 10 |TODO
- 11 |
 
 [Compose.execute] I fail to compose word.
 
-  word: TODO
+  word: add1
 
+  5 |type Trivial -- Type end
   6 |node sole -- Trivial :value! end
   7 |
   8 |sole add1
   9 |
- 10 |TODO
- 11 |