diff --git a/TODO.md b/TODO.md
index 0757ab3..88c672d 100644
--- a/TODO.md
+++ b/TODO.md
@@ -22,3 +22,25 @@
 - Try to implement the min and max functions using select
 
 - Read https://bytecodealliance.org/articles/multi-value-all-the-wasm
+
+
+- GRose :: (* -> *) -> * -> *
+- skolem => variable that cannot be unified
+
+
+Limitations (for now):
+- no type level nats
+- only support first order kinds
+  Do not support yet:
+  ```
+  data Record f = Record {
+    field: f Int
+  }
+  Record :: (* -> *) -> *
+  ```
+  (Nested arrows)
+- only support rank 1 types
+  ```
+  mapRecord :: forall f g. (forall a. f a -> f b) -> Record f -> Record g
+  ```
+  (Nested forall)
diff --git a/phasm/type4/__init__.py b/phasm/type4/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/phasm/type4/classes.py b/phasm/type4/classes.py
new file mode 100644
index 0000000..8c3ae12
--- /dev/null
+++ b/phasm/type4/classes.py
@@ -0,0 +1,131 @@
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import TypeAlias
+
+## Kind * (part 1)
+
+@dataclass
+class Atomic:
+    """
+    Atomic (or base or fundamental) type - it doesn't construct anything and wasn't constructed
+    """
+    name: str
+
+class Struct(Atomic):
+    """
+    Structs are a fundamental type. But we need to store some extra info.
+    """
+    fields: list[tuple[str, Type4]]
+
+@dataclass
+class Variable:
+    """
+    Type variable of kind *.
+    """
+    name: str
+
+@dataclass
+class Nat:
+    """
+    Some type constructors take a natural number as argument, rather than a type.
+    """
+    value: int
+
+    @property
+    def name(self) -> str:
+        return str(self.value)
+
+## Kind * -> *
+
+@dataclass
+class ConcreteConSS:
+    """
+    An concrete type construtor of kind * -> *, like dynamic array.
+    """
+    name: str
+
+@dataclass
+class VariableConSS:
+    """
+    A type variable of kind * -> *.
+    """
+    name: str
+
+@dataclass
+class AppliedConSS:
+    """
+    An application of a type constructor of kind * -> *.
+
+    The result is a type of kind *.
+    """
+    con: ConcreteConSS | VariableConSS | AppliedConSSS | AppliedConNSS
+    arg: Type4
+
+    @property
+    def name(self) -> str:
+        return f'{self.con.name} {self.arg.name}'
+
+## Kind * -> * -> *
+
+@dataclass
+class ConcreteConSSS:
+    """
+    An concrete type construtor of kind * -> * -> *, like function, tuple or Either.
+    """
+    name: str
+
+@dataclass
+class VariableConSSS:
+    """
+    A type variable of kind * -> * -> *.
+    """
+    name: str
+
+@dataclass
+class AppliedConSSS:
+    """
+    An application of a type constructor of kind * -> * -> *.
+
+    The result is a type construtor of kind * -> *.
+    """
+    con: ConcreteConSSS | VariableConSSS
+    arg: Type4
+
+    @property
+    def name(self) -> str:
+        return f'{self.con.name} {self.arg.name}'
+
+## Kind Nat -> * -> *
+
+@dataclass
+class ConcreteConNSS:
+    """
+    An concrete type construtor of kind Nat -> * -> *, like static array.
+    """
+    name: str
+
+@dataclass
+class VariableConNSS:
+    """
+    A type variable of kind Nat -> * -> *.
+    """
+    name: str
+
+@dataclass
+class AppliedConNSS:
+    """
+    An application of a type constructor of kind Nat -> * -> *.
+
+    The result is a type construtor of kind * -> *.
+    """
+    con: ConcreteConNSS | VariableConNSS
+    arg: Nat
+
+    @property
+    def name(self) -> str:
+        return f'{self.con.name} {self.arg.name}'
+
+# Kind * (part 2)
+
+Type4: TypeAlias = Atomic | Variable | AppliedConSS
diff --git a/phasm/type4/unify.py b/phasm/type4/unify.py
new file mode 100644
index 0000000..7cdde15
--- /dev/null
+++ b/phasm/type4/unify.py
@@ -0,0 +1,202 @@
+from dataclasses import dataclass
+
+from .classes import (
+    AppliedConNSS,
+    AppliedConSS,
+    AppliedConSSS,
+    Atomic,
+    ConcreteConNSS,
+    ConcreteConSS,
+    ConcreteConSSS,
+    Type4,
+    Variable,
+    VariableConNSS,
+    VariableConSS,
+    VariableConSSS,
+)
+
+
+@dataclass
+class Failure:
+    """
+    Both types are already different - cannot be unified.
+    """
+    msg: str
+
+@dataclass
+class Action:
+    pass
+
+UnifyResult = Failure | list[Action]
+
+@dataclass
+class SetTypeForVariable(Action):
+    var: Variable
+    type: Atomic | AppliedConSS
+
+@dataclass
+class SetTypeForConSSVariable(Action):
+    var: VariableConSS
+    type: ConcreteConSS | AppliedConSSS | AppliedConNSS
+
+@dataclass
+class SetTypeForConSSSVariable(Action):
+    var: VariableConSSS
+    type: ConcreteConSSS
+
+@dataclass
+class ReplaceVariable(Action):
+    before: Variable
+    after: Variable
+
+@dataclass
+class ReplaceConSSVariable(Action):
+    before: VariableConSS
+    after: VariableConSS
+
+def unify(lft: Type4, rgt: Type4) -> UnifyResult:
+    """
+    Tries to unify the given two types.
+    """
+    if isinstance(lft, Atomic) and isinstance(rgt, Atomic):
+        if lft == rgt:
+            return []
+
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, Atomic) and isinstance(rgt, Variable):
+        return [SetTypeForVariable(rgt, lft)]
+
+    if isinstance(lft, Atomic) and isinstance(rgt, AppliedConSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, Variable) and isinstance(rgt, Atomic):
+        return [SetTypeForVariable(lft, rgt)]
+
+    if isinstance(lft, Variable) and isinstance(rgt, Variable):
+        return [ReplaceVariable(lft, rgt)]
+
+    if isinstance(lft, Variable) and isinstance(rgt, AppliedConSS):
+        return [SetTypeForVariable(lft, rgt)]
+
+    if isinstance(lft, AppliedConSS) and isinstance(rgt, Atomic):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, AppliedConSS) and isinstance(rgt, Variable):
+        return [SetTypeForVariable(rgt, lft)]
+
+    if isinstance(lft, AppliedConSS) and isinstance(rgt, AppliedConSS):
+        con_res = unify_con_ss(lft.con, rgt.con)
+        if isinstance(con_res, Failure):
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        arg_res = unify(lft.arg, rgt.arg)
+        if isinstance(arg_res, Failure):
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        return con_res + arg_res
+
+    raise NotImplementedError
+
+def unify_con_ss(
+        lft: ConcreteConSS | VariableConSS | AppliedConSSS | AppliedConNSS,
+        rgt: ConcreteConSS | VariableConSS | AppliedConSSS | AppliedConNSS,
+    ) -> UnifyResult:
+    """
+    Tries to unify the given two constuctors of kind * -> *.
+    """
+    if isinstance(lft, ConcreteConSS) and isinstance(rgt, ConcreteConSS):
+        if lft == rgt:
+            return []
+
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, ConcreteConSS) and isinstance(rgt, VariableConSS):
+        return [SetTypeForConSSVariable(rgt, lft)]
+
+    if isinstance(lft, ConcreteConSS) and isinstance(rgt, AppliedConSSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, ConcreteConSS) and isinstance(rgt, AppliedConNSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, VariableConSS) and isinstance(rgt, ConcreteConSS):
+        return [SetTypeForConSSVariable(lft, rgt)]
+
+    if isinstance(lft, VariableConSS) and isinstance(rgt, VariableConSS):
+        return [ReplaceConSSVariable(lft, rgt)]
+
+    if isinstance(lft, VariableConSS) and isinstance(rgt, AppliedConSSS):
+        return [SetTypeForConSSVariable(lft, rgt)]
+
+    if isinstance(lft, VariableConSS) and isinstance(rgt, AppliedConNSS):
+        return [SetTypeForConSSVariable(lft, rgt)]
+
+    if isinstance(lft, AppliedConSSS) and isinstance(rgt, ConcreteConSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, AppliedConSSS) and isinstance(rgt, VariableConSS):
+        return [SetTypeForConSSVariable(rgt, lft)]
+
+    if isinstance(lft, AppliedConSSS) and isinstance(rgt, AppliedConSSS):
+        con_res = unify_con_sss(lft.con, rgt.con)
+        if isinstance(con_res, Failure):
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        arg_res = unify(lft.arg, rgt.arg)
+        if isinstance(arg_res, Failure):
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        return con_res + arg_res
+
+    if isinstance(lft, AppliedConSSS) and isinstance(rgt, AppliedConNSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, AppliedConNSS) and isinstance(rgt, ConcreteConSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, AppliedConNSS) and isinstance(rgt, VariableConSS):
+        return [SetTypeForConSSVariable(rgt, lft)]
+
+    if isinstance(lft, AppliedConNSS) and isinstance(rgt, AppliedConSSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, AppliedConNSS) and isinstance(rgt, AppliedConNSS):
+        con_res = unify_con_nss(lft.con, rgt.con)
+        if isinstance(con_res, Failure):
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        if lft.arg.value != rgt.arg.value:
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        return con_res
+
+    raise NotImplementedError
+
+def unify_con_sss(
+        lft: ConcreteConSSS | VariableConSSS,
+        rgt: ConcreteConSSS | VariableConSSS,
+    ) -> UnifyResult:
+    """
+    Tries to unify the given two constuctors of kind * -> * -> *.
+    """
+    if isinstance(lft, ConcreteConSSS) and isinstance(rgt, ConcreteConSSS):
+        if lft == rgt:
+            return []
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    raise NotImplementedError
+
+def unify_con_nss(
+        lft: ConcreteConNSS | VariableConNSS,
+        rgt: ConcreteConNSS | VariableConNSS,
+    ) -> UnifyResult:
+    """
+    Tries to unify the given two constuctors of kind * -> * -> *.
+    """
+    if isinstance(lft, ConcreteConNSS) and isinstance(rgt, ConcreteConNSS):
+        if lft == rgt:
+            return []
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    raise NotImplementedError
diff --git a/phasm/type5/__init__.py b/phasm/type5/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/phasm/type5/__main__.py b/phasm/type5/__main__.py
new file mode 100644
index 0000000..98adf30
--- /dev/null
+++ b/phasm/type5/__main__.py
@@ -0,0 +1,93 @@
+from .kindexpr import Star
+from .record import Record
+from .typeexpr import AtomicType, TypeApplication, TypeConstructor, TypeVariable
+from .unify import unify
+
+
+def main() -> None:
+    S = Star()
+
+    a_var = TypeVariable(name="a", kind=S)
+    b_var = TypeVariable(name="b", kind=S)
+    t_var = TypeVariable(name="t", kind=S >> S)
+    r_var = TypeVariable(name="r", kind=S >> S)
+    print(a_var)
+    print(b_var)
+    print(t_var)
+    print(r_var)
+    print()
+
+    u32_type = AtomicType(name="u32")
+    f64_type = AtomicType(name="f64")
+    print(u32_type)
+    print(f64_type)
+    print()
+
+    maybe_constructor = TypeConstructor(name="Maybe", kind=S >> S)
+    maybe_a_type = TypeApplication(constructor=maybe_constructor, argument=a_var)
+    maybe_u32_type = TypeApplication(constructor=maybe_constructor, argument=u32_type)
+    print(maybe_constructor)
+    print(maybe_a_type)
+    print(maybe_u32_type)
+    print()
+
+    either_constructor = TypeConstructor(name="Either", kind=S >> (S >> S))
+    either_a_constructor = TypeApplication(constructor=either_constructor, argument=a_var)
+    either_a_a_type = TypeApplication(constructor=either_a_constructor, argument=a_var)
+    either_u32_constructor = TypeApplication(constructor=either_constructor, argument=u32_type)
+    either_u32_f64_type = TypeApplication(constructor=either_u32_constructor, argument=f64_type)
+    either_u32_a_type = TypeApplication(constructor=either_u32_constructor, argument=a_var)
+    print(either_constructor)
+    print(either_a_constructor)
+    print(either_a_a_type)
+    print(either_u32_constructor)
+    print(either_u32_f64_type)
+    print(either_u32_a_type)
+    print()
+
+    t_a_type = TypeApplication(constructor=t_var, argument=a_var)
+    t_u32_type = TypeApplication(constructor=t_var, argument=u32_type)
+    print(t_a_type)
+    print(t_u32_type)
+    print()
+
+
+    shape_record = Record("Shape", [
+        ("width", u32_type),
+        ("height", either_u32_f64_type),
+    ])
+    print('shape_record', shape_record)
+    print()
+
+    values = [
+        a_var,
+        b_var,
+        u32_type,
+        f64_type,
+        t_var,
+        t_a_type,
+        r_var,
+        maybe_constructor,
+        maybe_u32_type,
+        maybe_a_type,
+        either_u32_constructor,
+        either_u32_a_type,
+        either_u32_f64_type,
+    ]
+
+    seen_exprs: set[str] = set()
+    for lft in values:
+        for rgt in values:
+            expr = f"{lft.name} ~ {rgt.name}"
+            if expr in seen_exprs:
+                continue
+
+            print(expr.ljust(40) + " => " + str(unify(lft, rgt)))
+
+            inv_expr = f"{rgt.name} ~ {lft.name}"
+            seen_exprs.add(inv_expr)
+
+        print()
+
+if __name__ == '__main__':
+    main()
diff --git a/phasm/type5/kindexpr.py b/phasm/type5/kindexpr.py
new file mode 100644
index 0000000..cd3ae05
--- /dev/null
+++ b/phasm/type5/kindexpr.py
@@ -0,0 +1,40 @@
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import TypeAlias
+
+
+@dataclass
+class Star:
+    def __rshift__(self, other: KindExpr) -> Arrow:
+        return Arrow(self, other)
+
+    def __str__(self) -> str:
+        return "*"
+
+@dataclass
+class Arrow:
+    """
+    Represents an arrow kind `K1 -> K2`.
+
+    To create K1 -> K2 -> K3, pass an Arrow for result_kind.
+    For now, we do not support Arrows as arguments (i.e.,
+    no higher order kinds).
+    """
+    arg_kind: Star
+    result_kind: KindExpr
+
+    def __str__(self) -> str:
+        if isinstance(self.arg_kind, Star):
+            arg_kind = "*"
+        else:
+            arg_kind = f"({str(self.arg_kind)})"
+
+        if isinstance(self.result_kind, Star):
+            result_kind = "*"
+        else:
+            result_kind = f"({str(self.result_kind)})"
+
+        return f"{arg_kind} -> {result_kind}"
+
+KindExpr: TypeAlias = Star | Arrow
diff --git a/phasm/type5/record.py b/phasm/type5/record.py
new file mode 100644
index 0000000..1cee24e
--- /dev/null
+++ b/phasm/type5/record.py
@@ -0,0 +1,42 @@
+from dataclasses import dataclass
+
+from .kindexpr import Star
+from .typeexpr import AtomicType, TypeApplication, TypeExpr
+
+
+@dataclass
+class Record(TypeExpr):
+    """
+    Records are a fundamental type. But we need to store some extra info.
+    """
+    fields: list[tuple[str, AtomicType | TypeApplication]]
+
+    def __init__(self, name: str, fields: list[tuple[str, AtomicType | TypeApplication]]) -> None:
+        for field_name, field_type in fields:
+            if field_type.kind == Star():
+                continue
+
+            raise TypeError(f"Record fields must be concrete types ({field_name} :: {field_type})")
+
+        super().__init__(Star(), name)
+        self.fields = fields
+
+    def __str__(self) -> str:
+        args = ", ".join(
+            f"{field_name} :: {field_type}"
+            for field_name, field_type in self.fields
+        )
+        return f"{self.name} {{{args}}} :: {self.kind}"
+
+@dataclass
+class RecordConstructor(TypeExpr):
+    """
+    TODO.
+
+    i.e.:
+    ```
+    class Foo[T, R]:
+        lft: T
+        rgt: R
+    """
+    name: str
diff --git a/phasm/type5/typeexpr.py b/phasm/type5/typeexpr.py
new file mode 100644
index 0000000..3e1ac5f
--- /dev/null
+++ b/phasm/type5/typeexpr.py
@@ -0,0 +1,52 @@
+from __future__ import annotations
+
+from dataclasses import dataclass
+
+from .kindexpr import Arrow, KindExpr, Star
+
+
+@dataclass
+class TypeExpr:
+    kind: KindExpr
+    name: str
+
+    def __str__(self) -> str:
+        return f"{self.name} :: {self.kind}"
+
+@dataclass
+class AtomicType(TypeExpr):
+    def __init__(self, name: str) -> None:
+        super().__init__(Star(), name)
+
+@dataclass
+class TypeVariable(TypeExpr):
+    """
+    A placeholder in a type expression
+    """
+
+@dataclass
+class TypeConstructor(TypeExpr):
+    name: str
+
+    def __init__(self, kind: Arrow, name: str) -> None:
+        super().__init__(kind, name)
+
+@dataclass
+class TypeApplication(TypeExpr):
+    constructor: TypeConstructor | TypeApplication | TypeVariable
+    argument: TypeExpr
+
+    def __init__(self, constructor: TypeConstructor | TypeApplication | TypeVariable, argument: TypeExpr) -> None:
+        if isinstance(constructor.kind, Star):
+            raise TypeError("A constructor cannot be a concrete type")
+
+        if constructor.kind.arg_kind != argument.kind:
+            raise TypeError("Argument does match construtor's expectations")
+
+        super().__init__(
+            constructor.kind.result_kind,
+            f"{constructor.name} {argument.name}",
+        )
+
+        self.constructor = constructor
+        self.argument = argument
diff --git a/phasm/type5/unify.py b/phasm/type5/unify.py
new file mode 100644
index 0000000..61f5a42
--- /dev/null
+++ b/phasm/type5/unify.py
@@ -0,0 +1,157 @@
+from dataclasses import dataclass
+
+from .typeexpr import (
+    AtomicType,
+    TypeApplication,
+    TypeConstructor,
+    TypeExpr,
+    TypeVariable,
+)
+
+
+@dataclass
+class Failure:
+    """
+    Both types are already different - cannot be unified.
+    """
+    msg: str
+
+@dataclass
+class Action:
+    pass
+
+class ActionList(list[Action]):
+    def __str__(self) -> str:
+        return '{' + ', '.join(map(str, self)) + '}'
+
+UnifyResult = Failure | ActionList
+
+@dataclass
+class ReplaceVariable(Action):
+    var: TypeVariable
+    typ: TypeExpr
+
+    def __str__(self) -> str:
+        return f'{self.var.name} := {self.typ.name}'
+
+def unify(lft: TypeExpr, rgt: TypeExpr) -> UnifyResult:
+    if lft == rgt:
+        return ActionList()
+
+    if lft.kind != rgt.kind:
+        return Failure("Kind mismatch")
+
+
+
+    if isinstance(lft, AtomicType) and isinstance(rgt, AtomicType):
+        return Failure("Not the same type")
+
+    if isinstance(lft, AtomicType) and isinstance(rgt, TypeVariable):
+        return ActionList([ReplaceVariable(rgt, lft)])
+
+    if isinstance(lft, AtomicType) and isinstance(rgt, TypeConstructor):
+        raise NotImplementedError  # Should have been caught by kind check above
+
+    if isinstance(lft, AtomicType) and isinstance(rgt, TypeApplication):
+        if is_concrete(rgt):
+            return Failure("Not the same type")
+
+        return Failure("Type shape mismatch")
+
+
+
+    if isinstance(lft, TypeVariable) and isinstance(rgt, AtomicType):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeVariable) and isinstance(rgt, TypeVariable):
+        return ActionList([ReplaceVariable(lft, rgt)])
+
+    if isinstance(lft, TypeVariable) and isinstance(rgt, TypeConstructor):
+        return ActionList([ReplaceVariable(lft, rgt)])
+
+    if isinstance(lft, TypeVariable) and isinstance(rgt, TypeApplication):
+        if occurs(lft, rgt):
+            return Failure("One type occurs in the other")
+
+        return ActionList([ReplaceVariable(lft, rgt)])
+
+
+
+    if isinstance(lft, TypeConstructor) and isinstance(rgt, AtomicType):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeConstructor) and isinstance(rgt, TypeVariable):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeConstructor) and isinstance(rgt, TypeConstructor):
+        return Failure("Not the same type constructor")
+
+    if isinstance(lft, TypeConstructor) and isinstance(rgt, TypeApplication):
+        return Failure("Not the same type constructor")
+
+
+
+    if isinstance(lft, TypeApplication) and isinstance(rgt, AtomicType):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeApplication) and isinstance(rgt, TypeVariable):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeApplication) and isinstance(rgt, TypeConstructor):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeApplication) and isinstance(rgt, TypeApplication):
+        con_res = unify(lft.constructor, rgt.constructor)
+        if isinstance(con_res, Failure):
+            return con_res
+
+        arg_res = unify(lft.argument, rgt.argument)
+        if isinstance(arg_res, Failure):
+            return arg_res
+
+        return ActionList(con_res + arg_res)
+
+
+
+    return Failure('Not implemented')
+
+def occurs(lft: TypeVariable, rgt: TypeApplication) -> bool:
+    """
+    Checks whether the given variable occurs in the given application.
+    """
+    if lft == rgt.constructor:
+        return True
+
+    if lft == rgt.argument:
+        return True
+
+    if isinstance(rgt.argument, TypeApplication):
+        return occurs(lft, rgt.argument)
+
+    return False
+
+def is_concrete(lft: TypeExpr) -> bool:
+    """
+    A concrete type has no variables in it.
+
+    This is also known as a monomorphic type.
+    """
+    if isinstance(lft, AtomicType):
+        return True
+
+    if isinstance(lft, TypeVariable):
+        return False
+
+    if isinstance(lft, TypeConstructor):
+        return True
+
+    if isinstance(lft, TypeApplication):
+        return is_concrete(lft.constructor) and is_concrete(lft.argument)
+
+    raise NotImplementedError
+
+def is_polymorphic(lft: TypeExpr) -> bool:
+    """
+    A polymorphic type has one or more variables in it.
+    """
+    return not is_concrete(lft)
diff --git a/tests/integration/test_type4/__init__.py b/tests/integration/test_type4/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/tests/integration/test_type4/test_unify.py b/tests/integration/test_type4/test_unify.py
new file mode 100644
index 0000000..ed4a7cb
--- /dev/null
+++ b/tests/integration/test_type4/test_unify.py
@@ -0,0 +1,113 @@
+import pytest
+
+from phasm.type4 import classes
+from phasm.type4 import unify as sut
+
+
+class TestNamespace:
+    ## Kind * (part 1)
+    u32 = classes.Atomic('u32')
+    f64 = classes.Atomic('f64')
+
+    a = classes.Variable('a')
+    b = classes.Variable('b')
+
+    ## Kind * -> *
+    dynamic_array = classes.ConcreteConSS('dynamic_array')
+    maybe = classes.ConcreteConSS('maybe')
+    f = classes.VariableConSS('f')
+    t = classes.VariableConSS('t')
+
+    ## Kind * -> * -> *
+    function = classes.ConcreteConSSS('function')
+    either = classes.ConcreteConSSS('either')
+
+    ## Kind Nat -> * -> *
+    static_array = classes.ConcreteConNSS('static_array')
+
+    ## Kind * -> * (part 2)
+    function_u32 = classes.AppliedConSSS(function, u32)
+    function_f64 = classes.AppliedConSSS(function, f64)
+    either_u32 = classes.AppliedConSSS(either, u32)
+    either_f64 = classes.AppliedConSSS(either, f64)
+    static_array_4 = classes.AppliedConNSS(static_array, classes.Nat(4))
+    static_array_8 = classes.AppliedConNSS(static_array, classes.Nat(8))
+
+    ## Kind * (part 2)
+    dynamic_array_u32 = classes.AppliedConSS(dynamic_array, u32)
+    dynamic_array_f64 = classes.AppliedConSS(dynamic_array, f64)
+    maybe_u32 = classes.AppliedConSS(maybe, u32)
+    maybe_f64 = classes.AppliedConSS(maybe, f64)
+    t_u32 = classes.AppliedConSS(t, u32)
+    t_f64 = classes.AppliedConSS(t, f64)
+    f_u32 = classes.AppliedConSS(f, u32)
+    f_f64 = classes.AppliedConSS(f, f64)
+    function_f64_u32 = classes.AppliedConSS(function_f64, u32)
+    either_f64_u32 = classes.AppliedConSS(either_f64, u32)
+    static_array_4_u32 = classes.AppliedConSS(static_array_4, u32)
+    static_array_8_u32 = classes.AppliedConSS(static_array_8, u32)
+
+    TEST_LIST: list[tuple[classes.Type4, classes.Type4, sut.UnifyResult]] = [
+        # Atomic / Atomic
+        (u32, u32, []),
+        (u32, f64, sut.Failure('Cannot unify u32 and f64')),
+        # Atomic / Variable
+        (u32, a, [sut.SetTypeForVariable(a, u32)]),
+        # Atomic / AppliedConSS
+        (u32, t_f64, sut.Failure('Cannot unify u32 and t f64')),
+
+        # Variable / Atomic
+        (a, u32, [sut.SetTypeForVariable(a, u32)]),
+        # Variable / Variable
+        (a, b, [sut.ReplaceVariable(a, b)]),
+        # Variable / AppliedConSS
+        (a, t_f64, [sut.SetTypeForVariable(a, t_f64)]),
+
+        # AppliedConSS / Atomic
+        (t_f64, u32, sut.Failure('Cannot unify t f64 and u32')),
+        # AppliedConSS / Variable
+        (t_f64, a, [sut.SetTypeForVariable(a, t_f64)]),
+
+        # AppliedConSS ConcreteConSS / AppliedConSS ConcreteConSS
+        (dynamic_array_u32, dynamic_array_u32, []),
+        (dynamic_array_u32, maybe_u32, sut.Failure('Cannot unify dynamic_array u32 and maybe u32')),
+        # AppliedConSS ConcreteConSS / AppliedConSS VariableConSS
+        (dynamic_array_u32, t_u32, [sut.SetTypeForConSSVariable(t, dynamic_array)]),
+        # AppliedConSS ConcreteConSS / AppliedConSS AppliedConSSS
+        (dynamic_array_u32, function_f64_u32, sut.Failure('Cannot unify dynamic_array u32 and function f64 u32')),
+        # AppliedConSS ConcreteConSS / AppliedConSS AppliedConNSS
+        (dynamic_array_u32, static_array_4_u32, sut.Failure('Cannot unify dynamic_array u32 and static_array 4 u32')),
+
+        # AppliedConSS VariableConSS / AppliedConSS ConcreteConSS
+        (t_u32, dynamic_array_u32, [sut.SetTypeForConSSVariable(t, dynamic_array)]),
+        # AppliedConSS VariableConSS / AppliedConSS VariableConSS
+        (t_u32, f_u32, [sut.ReplaceConSSVariable(t, f)]),
+        # AppliedConSS VariableConSS / AppliedConSS AppliedConSSS
+        (t_u32, function_f64_u32, [sut.SetTypeForConSSVariable(t, function_f64)]),
+        # AppliedConSS VariableConSS / AppliedConSS AppliedConNSS
+        (t_u32, static_array_4_u32, [sut.SetTypeForConSSVariable(t, static_array_4)]),
+
+        # AppliedConSS AppliedConSSS / AppliedConSS ConcreteConSS
+        (function_f64_u32, dynamic_array_u32, sut.Failure('Cannot unify function f64 u32 and dynamic_array u32')),
+        # AppliedConSS AppliedConSSS / AppliedConSS VariableConSS
+        (function_f64_u32, t_u32, [sut.SetTypeForConSSVariable(t, function_f64)]),
+        # AppliedConSS AppliedConSSS / AppliedConSS AppliedConSSS
+        # (function_f64_u32, function_f64_u32, []),
+        (function_f64_u32, either_f64_u32, sut.Failure('Cannot unify function f64 u32 and either f64 u32')),
+        # AppliedConSS AppliedConSSS / AppliedConSS AppliedConNSS
+        (function_f64_u32, static_array_4_u32, sut.Failure('Cannot unify function f64 u32 and static_array 4 u32')),
+
+        # AppliedConSS AppliedConNSS / AppliedConSS ConcreteConSS
+        (static_array_4_u32, dynamic_array_u32, sut.Failure('Cannot unify static_array 4 u32 and dynamic_array u32')),
+        # AppliedConSS AppliedConNSS / AppliedConSS VariableConSS
+        (static_array_4_u32, t_u32, [sut.SetTypeForConSSVariable(t, static_array_4)]),
+        # AppliedConSS AppliedConNSS / AppliedConSS AppliedConSSS
+        (static_array_4_u32, function_f64_u32, sut.Failure('Cannot unify static_array 4 u32 and function f64 u32')),
+        # AppliedConSS AppliedConNSS / AppliedConSS AppliedConNSS
+        (static_array_4_u32, static_array_4_u32, []),
+        (static_array_4_u32, static_array_8_u32, sut.Failure('Cannot unify static_array 4 u32 and static_array 8 u32')),
+    ]
+
+@pytest.mark.parametrize('lft,rgt,exp_out', TestNamespace.TEST_LIST)
+def test_unify(lft: classes.Type4, rgt: classes.Type4, exp_out: sut.UnifyResult) -> None:
+    assert exp_out == sut.unify(lft, rgt)