Updated documentation and type_check test

README.md

@@ -78,7 +78,7 @@ class Foo(EnvExperiment):
         return a == b
 ```
 
-* Type variables can only be used in functions/methods, but not in class fields.
+* Type variables can only be used in functions/methods, but not in classes.
 * Type variable can be limited to a fixed set of types. A shorthand for one-time
   type variable limited to a fixed set of types is [union type & optional type](https://docs.python.org/3/library/typing.html#typing.Union).
   e.g. `def run(self, a: Union[int, str])`
@@ -99,6 +99,7 @@ class Foo(EnvExperiment):
 * Generics are instantiated at compile time, all the type checks like
   `type(x) == int` would be evaluated as constants. Type checks are not allowed
   in area outside generics.
+* Type variable and union cannot occur alone in the result type.
 
 ## Dynamic Dispatch
 Type annotations are invariant, so subtype (derived types) cannot be used

type_check.py

@@ -3,7 +3,7 @@ def is_variable(b):
 
 def unify(ctx, a, b):
     """
-    a is the concrete type
+    a is the more specific type
     b is the type with parameter
     lower case means primitive type
     upper case means type variable
@@ -18,6 +18,9 @@ def unify(ctx, a, b):
         else:
             ctx[b] = a
             return ctx
+    else:
+        if is_variable(a):
+            return f"{a} is less specific then {b}"
 
     if isinstance(a, list) and isinstance(b, list):
         return unify(ctx, a[0], b[0])
@@ -37,6 +40,8 @@ def check_eq(a, b):
     print(f"{a} <- {b}\n{unifier}\n")
 
 check_eq('a', 'A')
+check_eq('A', 'B')
+check_eq('A', 'a')
 check_eq(['a'], 'A')
 check_eq(['a'], ['A'])
 check_eq(['a'], ['b'])