diff --git a/toy-impl/README.md b/toy-impl/README.md
index 8a61b41..5e289a2 100644
--- a/toy-impl/README.md
+++ b/toy-impl/README.md
@@ -37,7 +37,83 @@ Here is the list of files and their purpose:
     python AST.
 * `type_def.py`: python class for various types.
 
-## Type Check Implementation
+## Variable Scope
+There is no shadowing in Python, so we decided that variables with the same name
+in a function must have the same type. For example, the following is not
+allowed:
+```python
+if foo():
+    a = 1
+else:
+    a = None
+```
+
+Also, as variables has to be well typed, they must be initialized before using
+them. If a variable could be not initialized in some code path, then it is not
+readable. The following is also not allowed:
+```python
+if foo():
+    a = 1
+a = a + 1
+```
+## Generics
+Generics are supported via type variables.
+
+* Generic type variable:
+    ```python
+    A = TypeVar('A')
+    ```
+* Bounded type variable (`A` can either be `T1` or `T2` or ...):
+    ```python
+    A = TypeVar('A', T1, T2, ...)
+    ```
+> Note:
+>
+> 1. In normal python, the *bound* of a type variable is actually about class
+>    inheritance. However, our type variable would be invariant and would not
+>    deal with subtyping.
+> 2. Type variables cannot contain any type variable in their bound. For
+>    example, `B = TypeVar('B', A, T3)` is not allowed.
+> 3. I did not really check the difference between the variable name and the
+>    name parameter of `TypeVar`, so idk what would happen if they are
+>    different. Please don't do that right now, would be fixed in later more
+>    serious implementations.
+
+For generic type variables, you can't really do much with them, other than
+passing them around in parameters, dealing with their list, etc.
+
+For bounded type variables, if an operation is supported by all the possible
+values of the variable, we can use that directly:
+```python
+A = TypeVar('A', int32, int64)
+
+def add(a: A, b: A) -> A:
+    return a + b
+```
+
+If an operation is supported by some possible values, we can use type guard:
+```python
+A = TypeVar('A', int32, list[int32])
+def add2(a: int32, b: A) -> a:
+    if type(b) == int32:
+        # b is int32 here
+        return a + b
+    else:
+        # b is list[int32] here
+        for x in b:
+            a = a + b
+        return a
+```
+
+Note that we only support very simple kinds of type guards in this toy
+implementation. More specifically, the type guard has to meet the following
+conditions:
+1. The if statement must be of the form `type(*) == **` or `type(*) != **`.
+   For example, `if type(b) == int32 or type(b) == list[int32]` is not allowed.
+2. The type of `*` must be a type variable. For example, `list[X]` is not
+   allowed.
+
+### Substitution
 The crucial constraint and assumption in our system is that, every
 (sub-)expressions must have their types fully determined, and cannot depend on
 statements/expressions after them.  Hence, in a function call, every arguments
@@ -81,7 +157,7 @@ def sum_of_heads(a: list[Y], b: list[Y]) -> Y:
 
 In this example, `a` has type `list[Y]`, so the algorithm would give a
 substitution `X -> Y` for the call `head(a)`, and similarly for `b`.
-As `Y` can only range over `int32` and `int64`, in the two valuations of `Y`,
+As `Y` can only range over `int32` and `int64`, in the two instances of `Y`,
 the return statement would have type
 * `int32 + int32 : int32 : Y` under `Y -> int32`, and
 * `int64 + int64 : int64 : Y` under `Y -> int64`.
@@ -96,6 +172,7 @@ def add(a: int32, b: I) -> int32:
     if type(b) == int32:
         return a + b
     else:
+        # b must be list[int32] in this branch.
         for x in b:
             a = add(a, x)
         return a
@@ -105,7 +182,21 @@ add(1, [1, 2, 3])
 This one should type check. `I -> list[int32]` only affects 1 call,
 and the recursion inside could substitute `I -> int32`.
 
-## Variable Scoping
+Example of a failure case:
+```python
+A = TypeVar('A')
+B = TypeVar('B')
+
+def foo(a: A, b: A):
+    pass
+
+def bar(a: A, b: B):
+    foo(a, b)
+```
+
+This would fail. From the first argument, we have `A -> A`, and from the second
+argument we need `A -> B`. In general, we may have `A != B`, so there is no
+substitution that meets the requirement and the type check failed.
 
 ## Operator Override