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/build/base.py b/phasm/build/base.py
index 579c147..eb38e9b 100644
--- a/phasm/build/base.py
+++ b/phasm/build/base.py
@@ -3,7 +3,7 @@ The base class for build environments.
 
 Contains nothing but the explicit compiler builtins.
 """
-from typing import Any, Callable, NamedTuple, Type
+from typing import Any, Callable, NamedTuple, Sequence, Type
 from warnings import warn
 
 from ..type3.functions import (
@@ -27,6 +27,8 @@ from ..type3.types import (
     TypeConstructor_Struct,
     TypeConstructor_Tuple,
 )
+from ..type5 import kindexpr as type5kindexpr
+from ..type5 import typeexpr as type5typeexpr
 from ..wasm import WasmType, WasmTypeInt32, WasmTypeNone
 from . import builtins
 
@@ -55,18 +57,22 @@ class MissingImplementationWarning(Warning):
 class BuildBase[G]:
     __slots__ = (
         'dynamic_array',
+        'dynamic_array_type5_constructor',
         'function',
+        'function_type5_constructor',
         'static_array',
         'struct',
         'tuple_',
 
         'none_',
+        'unit_type5',
         'bool_',
 
         'type_info_map',
         'type_info_constructed',
 
         'types',
+        'type5s',
         'type_classes',
         'type_class_instances',
         'type_class_instance_methods',
@@ -84,6 +90,8 @@ class BuildBase[G]:
     determined length, and each argument is the same.
     """
 
+    dynamic_array_type5_constructor: type5typeexpr.TypeConstructor
+
     function: TypeConstructor_Function
     """
     This is a function.
@@ -91,6 +99,8 @@ class BuildBase[G]:
     It should be applied with one or more arguments. The last argument is the 'return' type.
     """
 
+    function_type5_constructor: type5typeexpr.TypeConstructor
+
     static_array: TypeConstructor_StaticArray
     """
     This is a fixed length piece of memory.
@@ -118,6 +128,8 @@ class BuildBase[G]:
     The none type, for when functions simply don't return anything. e.g., IO().
     """
 
+    unit_type5: type5typeexpr.TypeExpr
+
     bool_: Type3
     """
     The bool type, either True or False
@@ -142,6 +154,11 @@ class BuildBase[G]:
     Types that are available without explicit import.
     """
 
+    type5s: dict[str, type5typeexpr.TypeExpr]
+    """
+    Types that are available without explicit import.
+    """
+
     type_classes: dict[str, Type3Class]
     """
     Type classes that are available without explicit import.
@@ -179,7 +196,13 @@ class BuildBase[G]:
         self.struct = builtins.struct
         self.tuple_ = builtins.tuple_
 
+        S = type5kindexpr.Star()
+
+        self.function_type5_constructor = type5typeexpr.TypeConstructor(kind=S >> (S >> S), name="function")
+        self.dynamic_array_type5_constructor = type5typeexpr.TypeConstructor(kind=S >> S, name="dynamic_array")
+
         self.bool_ = builtins.bool_
+        self.unit_type5 = type5typeexpr.AtomicType('()')
         self.none_ = builtins.none_
 
         self.type_info_map = {
@@ -193,6 +216,7 @@ class BuildBase[G]:
             'None': self.none_,
             'bool': self.bool_,
         }
+        self.type5s = {}
         self.type_classes = {}
         self.type_class_instances = set()
         self.type_class_instance_methods = {}
@@ -337,3 +361,61 @@ class BuildBase[G]:
             result += self.calculate_alloc_size(memtyp, is_member=True)
 
         raise Exception(f'{needle} not in {st_name}')
+
+    def type5_make_function(self, args: Sequence[type5typeexpr.TypeExpr]) -> type5typeexpr.TypeExpr:
+        if not args:
+            raise TypeError("Functions must at least have a return type")
+
+        if len(args) == 1:
+            # Functions always take an argument
+            # To distinguish between a function without arguments and a value
+            # of the type, we have a unit type
+            # This type has one value so it can always be called
+            args = [self.unit_type5, *args]
+
+        res_type5 = None
+
+        for arg_type5 in reversed(args):
+            if res_type5 is None:
+                res_type5 = arg_type5
+                continue
+
+            res_type5 = type5typeexpr.TypeApplication(
+                constructor=type5typeexpr.TypeApplication(
+                    constructor=self.function_type5_constructor,
+                    argument=arg_type5,
+                ),
+                argument=res_type5,
+            )
+
+        assert res_type5 is not None  # type hint
+
+        return res_type5
+
+    def type5_is_function(self, typeexpr: type5typeexpr.TypeExpr) -> list[type5typeexpr.TypeExpr] | None:
+        if not isinstance(typeexpr, type5typeexpr.TypeApplication):
+            return None
+        if not isinstance(typeexpr.constructor, type5typeexpr.TypeApplication):
+            return None
+        if typeexpr.constructor.constructor != self.function_type5_constructor:
+            return None
+
+        arg0 = typeexpr.constructor.argument
+        if arg0 is self.unit_type5:
+            my_args = []
+        else:
+            my_args = [arg0]
+
+        arg1 = typeexpr.argument
+        more_args = self.type5_is_function(arg1)
+        if more_args is None:
+            return my_args + [arg1]
+
+        return my_args + more_args
+
+    def type5_name(self, typ: type5typeexpr.TypeExpr) -> str:
+        func_args = self.type5_is_function(typ)
+        if func_args is None:
+            return typ.name
+
+        return 'Callable[' + ', '.join(map(self.type5_name, func_args)) + ']'
diff --git a/phasm/build/builtins.py b/phasm/build/builtins.py
index 5dd65d5..7aeb532 100644
--- a/phasm/build/builtins.py
+++ b/phasm/build/builtins.py
@@ -14,6 +14,8 @@ from ..type3.types import (
     TypeConstructor_Struct,
     TypeConstructor_Tuple,
 )
+from ..type5.kindexpr import Star
+from ..type5.typeexpr import TypeConstructor as Type5Constructor
 
 dynamic_array = TypeConstructor_DynamicArray('dynamic_array')
 function = TypeConstructor_Function('function')
@@ -24,3 +26,6 @@ tuple_ = TypeConstructor_Tuple('tuple')
 bool_ = Type3('bool', TypeApplication_Nullary(None, None))
 none_ = Type3('None', TypeApplication_Nullary(None, None))
 
+s = Star()
+
+static_array5 = Type5Constructor(name="static_array", kind=s >> s)
diff --git a/phasm/build/default.py b/phasm/build/default.py
index 2cbcd8f..6426af2 100644
--- a/phasm/build/default.py
+++ b/phasm/build/default.py
@@ -11,6 +11,7 @@ from ..type3.types import (
     Type3,
     TypeApplication_Nullary,
 )
+from ..type5 import typeexpr as type5typeexpr
 from ..wasm import (
     WasmTypeFloat32,
     WasmTypeFloat64,
@@ -82,6 +83,14 @@ class BuildDefault(BuildBase[Generator]):
             'bytes': bytes_,
         })
 
+        u8_5 = type5typeexpr.AtomicType('u8')
+        self.type5s.update({
+            'u8': u8_5,
+            'i32': type5typeexpr.AtomicType('i32'),
+            'f32': type5typeexpr.AtomicType('f32'),
+            'bytes': type5typeexpr.TypeApplication(self.dynamic_array_type5_constructor, u8_5),
+        })
+
         tc_list = [
             bits,
             eq, ord,
diff --git a/phasm/codestyle.py b/phasm/codestyle.py
index 1209c70..446e8b6 100644
--- a/phasm/codestyle.py
+++ b/phasm/codestyle.py
@@ -7,6 +7,7 @@ from typing import Any, Generator
 
 from . import ourlang
 from .type3.types import Type3, TypeApplication_Struct
+from .type5 import typeexpr as type5typeexpr
 
 
 def phasm_render(inp: ourlang.Module[Any]) -> str:
@@ -23,6 +24,12 @@ def type3(inp: Type3) -> str:
     """
     return inp.name
 
+def type5(mod: ourlang.Module[Any], inp: type5typeexpr.TypeExpr) -> str:
+    """
+    Render: type's name
+    """
+    return mod.build.type5_name(inp)
+
 def struct_definition(inp: ourlang.StructDefinition) -> str:
     """
     Render: TypeStruct's definition
@@ -128,7 +135,7 @@ def statement(inp: ourlang.Statement) -> Statements:
 
     raise NotImplementedError(statement, inp)
 
-def function(inp: ourlang.Function) -> str:
+def function(mod: ourlang.Module[Any], inp: ourlang.Function) -> str:
     """
     Render: Function body
 
@@ -142,7 +149,7 @@ def function(inp: ourlang.Function) -> str:
         result += '@imported\n'
 
     args = ', '.join(
-        f'{p.name}: {type3(p.type3)}'
+        f'{p.name}: {type5(mod, p.type5)}'
         for p in inp.posonlyargs
     )
 
@@ -175,12 +182,12 @@ def module(inp: ourlang.Module[Any]) -> str:
         result += constant_definition(cdef)
 
     for func in inp.functions.values():
-        if func.lineno < 0:
-            # Builtin (-2) or auto generated (-1)
+        if func.sourceref is None:
+            # Builtin or auto generated
             continue
 
         if result:
             result += '\n'
-        result += function(func)
+        result += function(inp, func)
 
     return result
diff --git a/phasm/compiler.py b/phasm/compiler.py
index 439828a..ca9893a 100644
--- a/phasm/compiler.py
+++ b/phasm/compiler.py
@@ -314,7 +314,7 @@ def expression(wgn: WasmGenerator, mod: ourlang.Module[WasmGenerator], inp: ourl
             expression_subscript_tuple(wgn, mod, inp)
             return
 
-        inp_as_fc = ourlang.FunctionCall(mod.build.type_classes['Subscriptable'].operators['[]'])
+        inp_as_fc = ourlang.FunctionCall(mod.build.type_classes['Subscriptable'].operators['[]'])  # type: ignore  # TODO
         inp_as_fc.type3 = inp.type3
         inp_as_fc.arguments = [inp.varref, inp.index]
 
diff --git a/phasm/ourlang.py b/phasm/ourlang.py
index 5bd5597..435ee1d 100644
--- a/phasm/ourlang.py
+++ b/phasm/ourlang.py
@@ -7,18 +7,41 @@ from .build.base import BuildBase
 from .type3.functions import FunctionSignature, TypeVariableContext
 from .type3.typeclasses import Type3ClassMethod
 from .type3.types import Type3, TypeApplication_Struct
+from .type5 import typeexpr as type5typeexpr
 
 
+class SourceRef:
+    __slots__ = ('filename', 'lineno', 'colno', )
+
+    filename: str | None
+    lineno: int | None
+    colno: int | None
+
+    def __init__(self, filename: str | None, lineno: int | None = None, colno: int | None = None) -> None:
+        self.filename = filename
+        self.lineno = lineno
+        self.colno = colno
+
+    def __repr__(self) -> str:
+        return f"SourceRef({self.filename!r}, {self.lineno!r}, {self.colno!r})"
+
+    def __str__(self) -> str:
+        return f"{self.filename}:{self.lineno:>4}:{self.colno:<3}"
+
 class Expression:
     """
     An expression within a statement
     """
-    __slots__ = ('type3', )
+    __slots__ = ('type3', 'type5', 'sourceref', )
 
+    sourceref: SourceRef | None
     type3: Type3 | None
+    type5: type5typeexpr.TypeExpr | None
 
-    def __init__(self) -> None:
+    def __init__(self, *, sourceref: SourceRef | None = None) -> None:
+        self.sourceref = sourceref
         self.type3 = None
+        self.type5 = None
 
 class Constant(Expression):
     """
@@ -36,8 +59,8 @@ class ConstantPrimitive(Constant):
 
     value: Union[int, float]
 
-    def __init__(self, value: Union[int, float]) -> None:
-        super().__init__()
+    def __init__(self, value: Union[int, float], sourceref: SourceRef) -> None:
+        super().__init__(sourceref=sourceref)
         self.value = value
 
     def __repr__(self) -> str:
@@ -121,8 +144,8 @@ class VariableReference(Expression):
 
     variable: Union['ModuleConstantDef', 'FunctionParam'] # also possibly local
 
-    def __init__(self, variable: Union['ModuleConstantDef', 'FunctionParam']) -> None:
-        super().__init__()
+    def __init__(self, variable: Union['ModuleConstantDef', 'FunctionParam'], sourceref: SourceRef) -> None:
+        super().__init__(sourceref=sourceref)
         self.variable = variable
 
 class BinaryOp(Expression):
@@ -154,8 +177,8 @@ class FunctionCall(Expression):
     function: Union['Function', 'FunctionParam', Type3ClassMethod]
     arguments: List[Expression]
 
-    def __init__(self, function: Union['Function', 'FunctionParam', Type3ClassMethod]) -> None:
-        super().__init__()
+    def __init__(self, function: Union['Function', 'FunctionParam', Type3ClassMethod], sourceref: SourceRef) -> None:
+        super().__init__(sourceref=sourceref)
 
         self.function = function
         self.arguments = []
@@ -222,7 +245,12 @@ class Statement:
     """
     A statement within a function
     """
-    __slots__ = ()
+    __slots__ = ("sourceref", )
+
+    sourceref: SourceRef | None
+
+    def __init__(self, *, sourceref: SourceRef | None = None) -> None:
+        self.sourceref = sourceref
 
 class StatementPass(Statement):
     """
@@ -236,7 +264,9 @@ class StatementReturn(Statement):
     """
     __slots__ = ('value', )
 
-    def __init__(self, value: Expression) -> None:
+    def __init__(self, value: Expression, sourceref: SourceRef) -> None:
+        super().__init__(sourceref=sourceref)
+
         self.value = value
 
     def __repr__(self) -> str:
@@ -261,14 +291,18 @@ class FunctionParam:
     """
     A parameter for a Function
     """
-    __slots__ = ('name', 'type3', )
+    __slots__ = ('name', 'type3', 'type5', )
 
     name: str
     type3: Type3
+    type5: type5typeexpr.TypeExpr
+
+    def __init__(self, name: str, type3: Type3, type5: type5typeexpr.TypeExpr) -> None:
+        assert type5typeexpr.is_concrete(type5)
 
-    def __init__(self, name: str, type3: Type3) -> None:
         self.name = name
         self.type3 = type3
+        self.type5 = type5
 
     def __repr__(self) -> str:
         return f'FunctionParam({self.name!r}, {self.type3!r})'
@@ -277,39 +311,41 @@ class Function:
     """
     A function processes input and produces output
     """
-    __slots__ = ('name', 'lineno', 'exported', 'imported', 'statements', 'signature', 'returns_type3', 'posonlyargs', )
+    __slots__ = ('name', 'sourceref', 'exported', 'imported', 'statements', 'signature', 'returns_type3', 'type5', 'posonlyargs', )
 
     name: str
-    lineno: int
+    sourceref: SourceRef
     exported: bool
     imported: Optional[str]
     statements: List[Statement]
     signature: FunctionSignature
     returns_type3: Type3
+    type5: type5typeexpr.TypeExpr | None
     posonlyargs: List[FunctionParam]
 
-    def __init__(self, name: str, lineno: int, returns_type3: Type3) -> None:
+    def __init__(self, name: str, sourceref: SourceRef, returns_type3: Type3) -> None:
         self.name = name
-        self.lineno = lineno
+        self.sourceref = sourceref
         self.exported = False
         self.imported = None
         self.statements = []
         self.signature = FunctionSignature(TypeVariableContext(), [])
         self.returns_type3 = returns_type3
+        self.type5 = None
         self.posonlyargs = []
 
 class StructDefinition:
     """
     The definition for a struct
     """
-    __slots__ = ('struct_type3', 'lineno', )
+    __slots__ = ('struct_type3', 'sourceref', )
 
     struct_type3: Type3
-    lineno: int
+    sourceref: SourceRef
 
-    def __init__(self, struct_type3: Type3, lineno: int) -> None:
+    def __init__(self, struct_type3: Type3, sourceref: SourceRef) -> None:
         self.struct_type3 = struct_type3
-        self.lineno = lineno
+        self.sourceref = sourceref
 
 class StructConstructor(Function):
     """
@@ -323,12 +359,12 @@ class StructConstructor(Function):
     struct_type3: Type3
 
     def __init__(self, struct_type3: Type3) -> None:
-        super().__init__(f'@{struct_type3.name}@__init___@', -1, struct_type3)
+        super().__init__(f'@{struct_type3.name}@__init___@', -1, struct_type3)  # type: ignore # TODO
 
         assert isinstance(struct_type3.application, TypeApplication_Struct)
 
         for mem, typ in struct_type3.application.arguments:
-            self.posonlyargs.append(FunctionParam(mem, typ, ))
+            self.posonlyargs.append(FunctionParam(mem, typ))  # type: ignore # TODO
             self.signature.args.append(typ)
 
         self.signature.args.append(struct_type3)
@@ -339,17 +375,19 @@ class ModuleConstantDef:
     """
     A constant definition within a module
     """
-    __slots__ = ('name', 'lineno', 'type3', 'constant', )
+    __slots__ = ('name', 'sourceref', 'type3', 'type5', 'constant', )
 
     name: str
-    lineno: int
+    sourceref: SourceRef
     type3: Type3
+    type5: type5typeexpr.TypeExpr
     constant: Constant
 
-    def __init__(self, name: str, lineno: int, type3: Type3, constant: Constant) -> None:
+    def __init__(self, name: str, sourceref: SourceRef, type3: Type3, type5: type5typeexpr.TypeExpr, constant: Constant) -> None:
         self.name = name
-        self.lineno = lineno
+        self.sourceref = sourceref
         self.type3 = type3
+        self.type5 = type5
         self.constant = constant
 
 class ModuleDataBlock:
@@ -383,11 +421,13 @@ class Module[G]:
     """
     A module is a file and consists of functions
     """
-    __slots__ = ('build', 'data', 'types',  'struct_definitions', 'constant_defs', 'functions', 'methods', 'operators', 'functions_table', )
+    __slots__ = ('build', 'filename', 'data', 'types', 'type5s', 'struct_definitions', 'constant_defs', 'functions', 'methods', 'operators', 'functions_table', )
 
     build: BuildBase[G]
+    filename: str
     data: ModuleData
     types: dict[str, Type3]
+    type5s: dict[str, type5typeexpr.TypeExpr]
     struct_definitions: Dict[str, StructDefinition]
     constant_defs: Dict[str, ModuleConstantDef]
     functions: Dict[str, Function]
@@ -395,11 +435,13 @@ class Module[G]:
     operators: Dict[str, Type3ClassMethod]
     functions_table: dict[Function, int]
 
-    def __init__(self, build: BuildBase[G]) -> None:
+    def __init__(self, build: BuildBase[G], filename: str) -> None:
         self.build = build
+        self.filename = filename
 
         self.data = ModuleData()
         self.types = {}
+        self.type5s = {}
         self.struct_definitions = {}
         self.constant_defs = {}
         self.functions = {}
diff --git a/phasm/parser.py b/phasm/parser.py
index a182822..fb7659d 100644
--- a/phasm/parser.py
+++ b/phasm/parser.py
@@ -22,6 +22,7 @@ from .ourlang import (
     Module,
     ModuleConstantDef,
     ModuleDataBlock,
+    SourceRef,
     Statement,
     StatementIf,
     StatementPass,
@@ -34,6 +35,7 @@ from .ourlang import (
 )
 from .type3.typeclasses import Type3ClassMethod
 from .type3.types import IntType3, Type3
+from .type5 import typeexpr as type5typeexpr
 from .wasmgenerator import Generator
 
 
@@ -96,11 +98,12 @@ class OurVisitor[G]:
         self.build = build
 
     def visit_Module(self, node: ast.Module) -> Module[G]:
-        module = Module(self.build)
+        module = Module(self.build, "-")
 
         module.methods.update(self.build.methods)
         module.operators.update(self.build.operators)
         module.types.update(self.build.types)
+        module.type5s.update(self.build.type5s)
 
         _not_implemented(not node.type_ignores, 'Module.type_ignores')
 
@@ -112,7 +115,7 @@ class OurVisitor[G]:
             if isinstance(res, ModuleConstantDef):
                 if res.name in module.constant_defs:
                     raise StaticError(
-                        f'{res.name} already defined on line {module.constant_defs[res.name].lineno}'
+                        f'{res.name} already defined on line {module.constant_defs[res.name].sourceref.lineno}'
                     )
 
                 module.constant_defs[res.name] = res
@@ -131,7 +134,7 @@ class OurVisitor[G]:
             if isinstance(res, Function):
                 if res.name in module.functions:
                     raise StaticError(
-                        f'{res.name} already defined on line {module.functions[res.name].lineno}'
+                        f'{res.name} already defined on line {module.functions[res.name].sourceref.lineno}'
                     )
 
                 module.functions[res.name] = res
@@ -156,15 +159,20 @@ class OurVisitor[G]:
         raise NotImplementedError(f'{node} on Module')
 
     def pre_visit_Module_FunctionDef(self, module: Module[G], node: ast.FunctionDef) -> Function:
-        function = Function(node.name, node.lineno, self.build.none_)
+        function = Function(node.name, SourceRef(module.filename, node.lineno, node.col_offset), self.build.none_)
 
         _not_implemented(not node.args.posonlyargs, 'FunctionDef.args.posonlyargs')
 
+        arg_type5_list = []
+
         for arg in node.args.args:
             if arg.annotation is None:
                 _raise_static_error(node, 'Must give a argument type')
 
             arg_type = self.visit_type(module, arg.annotation)
+            arg_type5 = self.visit_type5(module, arg.annotation)
+
+            arg_type5_list.append(arg_type5)
 
             # FIXME: Allow TypeVariable in the function signature
             # This would also require FunctionParam to accept a placeholder
@@ -173,6 +181,7 @@ class OurVisitor[G]:
             function.posonlyargs.append(FunctionParam(
                 arg.arg,
                 arg_type,
+                arg_type5,
             ))
 
         _not_implemented(not node.args.vararg, 'FunctionDef.args.vararg')
@@ -216,9 +225,13 @@ class OurVisitor[G]:
         if node.returns is None: # Note: `-> None` would be a ast.Constant
             _raise_static_error(node, 'Must give a return type')
         return_type = self.visit_type(module, node.returns)
+        arg_type5_list.append(self.visit_type5(module, node.returns))
+
         function.signature.args.append(return_type)
         function.returns_type3 = return_type
 
+        function.type5 = module.build.type5_make_function(arg_type5_list)
+
         _not_implemented(not node.type_comment, 'FunctionDef.type_comment')
 
         return function
@@ -249,7 +262,10 @@ class OurVisitor[G]:
 
             members[stmt.target.id] = self.visit_type(module, stmt.annotation)
 
-        return StructDefinition(module.build.struct(node.name, tuple(members.items())), node.lineno)
+        return StructDefinition(
+            module.build.struct(node.name, tuple(members.items())),
+            SourceRef(module.filename, node.lineno, node.col_offset),
+        )
 
     def pre_visit_Module_AnnAssign(self, module: Module[G], node: ast.AnnAssign) -> ModuleConstantDef:
         if not isinstance(node.target, ast.Name):
@@ -262,8 +278,9 @@ class OurVisitor[G]:
 
             return ModuleConstantDef(
                 node.target.id,
-                node.lineno,
+                SourceRef(module.filename, node.lineno, node.col_offset),
                 self.visit_type(module, node.annotation),
+                self.visit_type5(module, node.annotation),
                 value_data,
             )
 
@@ -275,8 +292,9 @@ class OurVisitor[G]:
             # Then return the constant as a pointer
             return ModuleConstantDef(
                 node.target.id,
-                node.lineno,
+                SourceRef(module.filename, node.lineno, node.col_offset),
                 self.visit_type(module, node.annotation),
+                self.visit_type5(module, node.annotation),
                 value_data,
             )
 
@@ -288,8 +306,9 @@ class OurVisitor[G]:
             # Then return the constant as a pointer
             return ModuleConstantDef(
                 node.target.id,
-                node.lineno,
+                SourceRef(module.filename, node.lineno, node.col_offset),
                 self.visit_type(module, node.annotation),
+                self.visit_type5(module, node.annotation),
                 value_data,
             )
 
@@ -328,7 +347,8 @@ class OurVisitor[G]:
                 _raise_static_error(node, 'Return must have an argument')
 
             return StatementReturn(
-                self.visit_Module_FunctionDef_expr(module, function, our_locals, node.value)
+                self.visit_Module_FunctionDef_expr(module, function, our_locals, node.value),
+                SourceRef(module.filename, node.lineno, node.col_offset),
             )
 
         if isinstance(node, ast.If):
@@ -443,11 +463,11 @@ class OurVisitor[G]:
 
             if node.id in our_locals:
                 param = our_locals[node.id]
-                return VariableReference(param)
+                return VariableReference(param, SourceRef(module.filename, node.lineno, node.col_offset))
 
             if node.id in module.constant_defs:
                 cdef = module.constant_defs[node.id]
-                return VariableReference(cdef)
+                return VariableReference(cdef, SourceRef(module.filename, node.lineno, node.col_offset))
 
             if node.id in module.functions:
                 fun = module.functions[node.id]
@@ -490,7 +510,7 @@ class OurVisitor[G]:
 
             func = module.functions[node.func.id]
 
-        result = FunctionCall(func)
+        result = FunctionCall(func, sourceref=SourceRef(module.filename, node.lineno, node.col_offset))
         result.arguments.extend(
             self.visit_Module_FunctionDef_expr(module, function, our_locals, arg_expr)
             for arg_expr in node.args
@@ -527,10 +547,10 @@ class OurVisitor[G]:
         varref: VariableReference
         if node.value.id in our_locals:
             param = our_locals[node.value.id]
-            varref = VariableReference(param)
+            varref = VariableReference(param, SourceRef(module.filename, node.lineno, node.col_offset))
         elif node.value.id in module.constant_defs:
             constant_def = module.constant_defs[node.value.id]
-            varref = VariableReference(constant_def)
+            varref = VariableReference(constant_def, SourceRef(module.filename, node.lineno, node.col_offset))
         else:
             _raise_static_error(node, f'Undefined variable {node.value.id}')
 
@@ -588,7 +608,7 @@ class OurVisitor[G]:
         _not_implemented(node.kind is None, 'Constant.kind')
 
         if isinstance(node.value, (int, float, )):
-            return ConstantPrimitive(node.value)
+            return ConstantPrimitive(node.value, SourceRef(module.filename, node.lineno, node.col_offset))
 
         if isinstance(node.value, bytes):
             data_block = ModuleDataBlock([])
@@ -664,6 +684,34 @@ class OurVisitor[G]:
 
         raise NotImplementedError(f'{node} as type')
 
+    def visit_type5(self, module: Module[G], node: ast.expr) -> type5typeexpr.TypeExpr:
+        if isinstance(node, ast.Name):
+            if not isinstance(node.ctx, ast.Load):
+                _raise_static_error(node, 'Must be load context')
+
+            if node.id in module.type5s:
+                return module.type5s[node.id]
+
+            _raise_static_error(node, f'Unrecognized type {node.id}')
+
+        if isinstance(node, ast.Subscript):
+            if isinstance(node.value, ast.Name) and node.value.id == 'Callable':
+                func_arg_types: list[ast.expr]
+
+                if isinstance(node.slice, ast.Name):
+                    func_arg_types = [node.slice]
+                elif isinstance(node.slice, ast.Tuple):
+                    func_arg_types = node.slice.elts
+                else:
+                    _raise_static_error(node, 'Must subscript using a list of types')
+
+                return module.build.type5_make_function([
+                    self.visit_type5(module, e)
+                    for e in func_arg_types
+                ])
+
+        raise NotImplementedError
+
 def _not_implemented(check: Any, msg: str) -> None:
     if not check:
         raise NotImplementedError(msg)
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/constraints.py b/phasm/type5/constraints.py
new file mode 100644
index 0000000..857324f
--- /dev/null
+++ b/phasm/type5/constraints.py
@@ -0,0 +1,145 @@
+from typing import Any, Protocol
+
+from ..build.base import BuildBase
+from ..ourlang import SourceRef
+from ..wasm import WasmTypeFloat32, WasmTypeFloat64, WasmTypeInt32, WasmTypeInt64
+from .kindexpr import KindExpr, Star
+from .typeexpr import (
+    TypeApplication,
+    TypeExpr,
+    TypeVariable,
+    is_concrete,
+    replace_variable,
+)
+from .unify import ActionList, Failure, ReplaceVariable, unify
+
+
+class ExpressionProtocol(Protocol):
+    """
+    A protocol for classes that should be updated on substitution
+    """
+
+    type5: TypeExpr | None
+    """
+    The type to update
+    """
+
+class Context:
+    __slots__ = ("build", "placeholder_update", )
+
+    build: BuildBase[Any]
+    placeholder_update: dict[TypeVariable, ExpressionProtocol]
+
+    def __init__(self, build: BuildBase[Any]) -> None:
+        self.build = build
+        self.placeholder_update = {}
+
+    def make_placeholder(self, arg: ExpressionProtocol, kind: KindExpr = Star()) -> TypeVariable:
+        res = TypeVariable(kind, f"p_{len(self.placeholder_update)}")
+        self.placeholder_update[res] = arg
+        return res
+
+class SkipForNow:
+    def __str__(self) -> str:
+        return '(skip for now)'
+
+CheckResult = None | ActionList | Failure | SkipForNow
+
+class ConstraintBase:
+    __slots__ = ("ctx", "sourceref", "comment",)
+
+    ctx: Context
+    sourceref: SourceRef | None
+    comment: str | None
+
+    def __init__(self, ctx: Context, sourceref: SourceRef | None, comment: str | None = None) -> None:
+        self.ctx = ctx
+        self.sourceref = sourceref
+        self.comment = comment
+
+    def check(self) -> CheckResult:
+        raise NotImplementedError(self)
+
+    def apply(self, action_list: ActionList) -> None:
+        for action in action_list:
+            if isinstance(action, ReplaceVariable):
+                self.replace_variable(action.var, action.typ)
+                continue
+
+            raise NotImplementedError(action)
+
+    def replace_variable(self, var: TypeVariable, typ: TypeExpr) -> None:
+        pass
+
+
+class LiteralFitsConstraint(ConstraintBase):
+    __slots__ = ("type", "literal",)
+
+    def __init__(self, ctx: Context, sourceref: SourceRef | None, type: TypeExpr, literal: Any, *, comment: str | None = None) -> None:
+        super().__init__(ctx, sourceref, comment)
+
+        self.type = type
+        self.literal = literal
+
+    def check(self) -> CheckResult:
+        if not is_concrete(self.type):
+            return SkipForNow()
+
+        type_info = self.ctx.build.type_info_map.get(self.type.name)
+
+        if type_info is not None and (type_info.wasm_type is WasmTypeInt32 or type_info.wasm_type is WasmTypeInt64):
+            assert type_info.signed is not None
+
+            if not isinstance(self.literal.value, int):
+                return Failure('Must be integer')
+
+            try:
+                self.literal.value.to_bytes(type_info.alloc_size, 'big', signed=type_info.signed)
+            except OverflowError:
+                return Failure(f'Must fit in {type_info.alloc_size} byte(s)')
+
+            return None
+
+        if type_info is not None and (type_info.wasm_type is WasmTypeFloat32 or type_info.wasm_type is WasmTypeFloat64):
+            if isinstance(self.literal.value, float):
+                # FIXME: Bit check
+
+                return None
+
+            return Failure('Must be real')
+
+        if isinstance(self.type, TypeApplication) and self.type.constructor == self.ctx.build.dynamic_array_type5_constructor:
+            if self.type.argument == self.ctx.build.type5s['u8']:
+                if not isinstance(self.literal.value, bytes):
+                    return Failure('Must be bytes')
+
+                return None
+
+            raise NotImplementedError(type_info)
+
+        raise NotImplementedError(type_info)
+
+    def replace_variable(self, var: TypeVariable, typ: TypeExpr) -> None:
+        self.type = replace_variable(self.type, var, typ)
+
+    def __str__(self) -> str:
+        return f"{self.ctx.build.type5_name(self.type)} can contain {self.literal!r}"
+
+class UnifyTypesConstraint(ConstraintBase):
+    __slots__ = ("lft", "rgt",)
+
+    def __init__(self, ctx: Context, sourceref: SourceRef | None, lft: TypeExpr, rgt: TypeExpr, *, comment: str | None = None) -> None:
+        super().__init__(ctx, sourceref, comment)
+
+        self.lft = lft
+        self.rgt = rgt
+
+    def check(self) -> CheckResult:
+        return unify(self.lft, self.rgt)
+
+    def replace_variable(self, var: TypeVariable, typ: TypeExpr) -> None:
+        self.lft = replace_variable(self.lft, var, typ)
+        self.rgt = replace_variable(self.rgt, var, typ)
+
+    def __str__(self) -> str:
+        return f"{self.ctx.build.type5_name(self.lft)} ~ {self.ctx.build.type5_name(self.rgt)}"
diff --git a/phasm/type5/fromast.py b/phasm/type5/fromast.py
new file mode 100644
index 0000000..0d4df1f
--- /dev/null
+++ b/phasm/type5/fromast.py
@@ -0,0 +1,114 @@
+from typing import Any, Generator
+
+from .. import ourlang
+from .constraints import (
+    ConstraintBase,
+    Context,
+    LiteralFitsConstraint,
+    UnifyTypesConstraint,
+)
+from .typeexpr import TypeApplication, TypeExpr, TypeVariable
+
+ConstraintGenerator = Generator[ConstraintBase, None, None]
+
+
+def phasm_type5_generate_constraints(ctx: Context, inp: ourlang.Module[Any]) -> list[ConstraintBase]:
+    return [*module(ctx, inp)]
+
+def expression_constant(ctx: Context, inp: ourlang.Constant, phft: TypeVariable) -> ConstraintGenerator:
+    if isinstance(inp, (ourlang.ConstantPrimitive, ourlang.ConstantBytes, ourlang.ConstantTuple, ourlang.ConstantStruct)):
+        yield LiteralFitsConstraint(
+            ctx, inp.sourceref, phft, inp,
+            comment='The given literal must fit the expected type'
+        )
+        return
+
+    raise NotImplementedError(inp)
+
+def expression_variable_reference(ctx: Context, inp: ourlang.VariableReference, phft: TypeVariable) -> ConstraintGenerator:
+    yield UnifyTypesConstraint(ctx, inp.sourceref, inp.variable.type5, phft)
+
+def expression_function_call(ctx: Context, inp: ourlang.FunctionCall, phft: TypeVariable) -> ConstraintGenerator:
+    arg_typ_list = []
+    for arg in inp.arguments:
+        arg_tv = ctx.make_placeholder(arg)
+        yield from expression(ctx, arg, arg_tv)
+        arg_typ_list.append(arg_tv)
+
+    if not hasattr(inp.function, 'type5'):
+        raise NotImplementedError
+
+    assert isinstance(inp.function.type5, TypeExpr)
+
+    expr_type = ctx.build.type5_make_function(arg_typ_list + [phft])
+
+    yield UnifyTypesConstraint(ctx, inp.sourceref, inp.function.type5, expr_type)
+
+def expression_function_reference(ctx: Context, inp: ourlang.FunctionReference, phft: TypeVariable) -> ConstraintGenerator:
+    assert inp.function.type5 is not None  # Todo: Make not nullable
+
+    yield UnifyTypesConstraint(ctx, inp.sourceref, inp.function.type5, phft)
+
+def expression(ctx: Context, inp: ourlang.Expression, phft: TypeVariable) -> ConstraintGenerator:
+    if isinstance(inp, ourlang.Constant):
+        yield from expression_constant(ctx, inp, phft)
+        return
+
+    if isinstance(inp, ourlang.VariableReference):
+        yield from expression_variable_reference(ctx, inp, phft)
+        return
+
+    if isinstance(inp, ourlang.FunctionCall):
+        yield from expression_function_call(ctx, inp, phft)
+        return
+
+    if isinstance(inp, ourlang.FunctionReference):
+        yield from expression_function_reference(ctx, inp, phft)
+        return
+
+    raise NotImplementedError(inp)
+
+def statement_return(ctx: Context, fun: ourlang.Function, inp: ourlang.StatementReturn) -> ConstraintGenerator:
+    phft = ctx.make_placeholder(inp.value)
+
+    if fun.type5 is None:
+        raise NotImplementedError("Deducing function type - you'll have to annotate it.")
+
+    if isinstance(fun.type5, TypeApplication):
+        args = ctx.build.type5_is_function(fun.type5)
+        assert args is not None
+        type5 = args[-1]
+    else:
+        type5 = fun.type5
+
+    yield UnifyTypesConstraint(ctx, inp.sourceref, type5, phft)
+    yield from expression(ctx, inp.value, phft)
+
+def statement(ctx: Context, fun: ourlang.Function, inp: ourlang.Statement) -> ConstraintGenerator:
+    if isinstance(inp, ourlang.StatementReturn):
+        yield from statement_return(ctx, fun, inp)
+        return
+
+    raise NotImplementedError(inp)
+
+def function(ctx: Context, inp: ourlang.Function) -> ConstraintGenerator:
+    for stmt in inp.statements:
+        yield from statement(ctx, inp, stmt)
+
+def module_constant_def(ctx: Context, inp: ourlang.ModuleConstantDef) -> ConstraintGenerator:
+    phft = ctx.make_placeholder(inp.constant)
+
+    yield from expression_constant(ctx, inp.constant, phft)
+    yield UnifyTypesConstraint(ctx, inp.sourceref, inp.type5, phft)
+
+def module(ctx: Context, inp: ourlang.Module[Any]) -> ConstraintGenerator:
+    for cdef in inp.constant_defs.values():
+        yield from module_constant_def(ctx, cdef)
+
+    for func in inp.functions.values():
+        if func.imported:
+            continue
+
+        yield from function(ctx, func)
+
+        # TODO: Generalize?
diff --git a/phasm/type5/kindexpr.py b/phasm/type5/kindexpr.py
new file mode 100644
index 0000000..34558c2
--- /dev/null
+++ b/phasm/type5/kindexpr.py
@@ -0,0 +1,46 @@
+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 "*"
+
+    def __hash__(self) -> int:
+        return 0  # All Stars are the same
+
+@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}"
+
+    def __hash__(self) -> int:
+        return hash((self.arg_kind, self.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/router.py b/phasm/type5/router.py
new file mode 100644
index 0000000..b12d1b1
--- /dev/null
+++ b/phasm/type5/router.py
@@ -0,0 +1,8 @@
+from typing import Callable
+
+from .typeexpr import TypeExpr
+
+
+class TypeRouter[S, R]:
+    def add(self, typ: TypeExpr, mtd: Callable[[S, TypeExpr], R]) -> None:
+        raise NotImplementedError
diff --git a/phasm/type5/solver.py b/phasm/type5/solver.py
new file mode 100644
index 0000000..27ce80c
--- /dev/null
+++ b/phasm/type5/solver.py
@@ -0,0 +1,75 @@
+from typing import Any
+
+from ..ourlang import Module, SourceRef
+from .constraints import Context, SkipForNow
+from .fromast import phasm_type5_generate_constraints
+from .typeexpr import TypeExpr, TypeVariable
+from .unify import ActionList, Failure, ReplaceVariable
+
+MAX_RESTACK_COUNT = 100
+
+class Type5SolverException(Exception):
+    pass
+
+def phasm_type5(inp: Module[Any], verbose: bool = False) -> None:
+    ctx = Context(inp.build)
+
+    constraint_list = phasm_type5_generate_constraints(ctx, inp)
+    assert constraint_list
+
+    placeholder_types: dict[TypeVariable, TypeExpr] = {}
+
+    error_list: list[tuple[str, str, str]] = []
+
+    for _ in range(MAX_RESTACK_COUNT):
+        if verbose:
+            for constraint in constraint_list:
+                sourceref = constraint.sourceref or SourceRef("?", 0, 0)
+                print(f"{sourceref!s}  {constraint!s:<20}")
+            print()
+
+        new_constraint_list = []
+        for constraint in constraint_list:
+            result = constraint.check()
+
+            sourceref = constraint.sourceref or SourceRef("?", 0, 0)
+
+            if verbose:
+                print(f"{sourceref!s}  {constraint!s:<30} {result}")
+
+            if not result:
+                # None or empty list
+                # Means it checks out and we don't need do anything
+                continue
+
+            if isinstance(result, SkipForNow):
+                new_constraint_list.append(constraint)
+                continue
+
+            if isinstance(result, Failure):
+                error_list.append((str(sourceref), str(constraint), result.msg, ))
+                continue
+
+            if isinstance(result, ActionList):
+                for action in result:
+                    if isinstance(action, ReplaceVariable):
+                        assert action.var not in placeholder_types
+                        placeholder_types[action.var] = action.typ
+                        continue
+
+                for constraint in constraint_list:
+                    constraint.apply(result)
+                continue
+
+            raise NotImplementedError(result)
+
+        if error_list:
+            raise Type5SolverException(error_list)
+
+        if not new_constraint_list:
+            break
+
+        constraint_list = new_constraint_list
+
+    for placeholder, expression in ctx.placeholder_update.items():
+        expression.type5 = placeholder_types[placeholder]
diff --git a/phasm/type5/typeexpr.py b/phasm/type5/typeexpr.py
new file mode 100644
index 0000000..0bd1c7f
--- /dev/null
+++ b/phasm/type5/typeexpr.py
@@ -0,0 +1,121 @@
+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
+    """
+
+    def __hash__(self) -> int:
+        return hash((self.kind, self.name))
+
+@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
+
+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)
+
+def replace_variable(expr: TypeExpr, var: TypeVariable, rep_expr: TypeExpr) -> TypeExpr:
+    if isinstance(expr, AtomicType):
+        # Nothing to replace
+        return expr
+
+    if isinstance(expr, TypeVariable):
+        if expr == var:
+            return rep_expr
+        return expr
+
+    if isinstance(expr, TypeConstructor):
+        return expr
+
+    if isinstance(expr, TypeApplication):
+        new_constructor = replace_variable(expr.constructor, var, rep_expr)
+
+        assert isinstance(new_constructor, TypeConstructor | TypeApplication | TypeVariable)  # type hint
+
+        return TypeApplication(
+            constructor=new_constructor,
+            argument=replace_variable(expr.argument, var, rep_expr),
+        )
+
+    raise NotImplementedError
diff --git a/phasm/type5/unify.py b/phasm/type5/unify.py
new file mode 100644
index 0000000..3f832a4
--- /dev/null
+++ b/phasm/type5/unify.py
@@ -0,0 +1,118 @@
+from dataclasses import dataclass
+
+from .typeexpr import (
+    AtomicType,
+    TypeApplication,
+    TypeConstructor,
+    TypeExpr,
+    TypeVariable,
+    is_concrete,
+    occurs,
+)
+
+
+@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')
diff --git a/tests/integration/runners.py b/tests/integration/runners.py
index 20681de..a355f35 100644
--- a/tests/integration/runners.py
+++ b/tests/integration/runners.py
@@ -11,6 +11,7 @@ from phasm.compiler import phasm_compile
 from phasm.optimise.removeunusedfuncs import removeunusedfuncs
 from phasm.parser import phasm_parse
 from phasm.type3.entry import phasm_type3
+from phasm.type5.solver import phasm_type5
 from phasm.wasmgenerator import Generator as WasmGenerator
 
 Imports = Optional[Dict[str, Callable[[Any], Any]]]
@@ -39,6 +40,7 @@ class RunnerBase:
         Parses the Phasm code into an AST
         """
         self.phasm_ast = phasm_parse(self.phasm_code)
+        phasm_type5(self.phasm_ast, verbose=verbose)
         phasm_type3(self.phasm_ast, verbose=verbose)
 
     def compile_ast(self) -> None:
diff --git a/tests/integration/test_lang/test_function_calls.py b/tests/integration/test_lang/test_function_calls.py
index 475b658..004e23b 100644
--- a/tests/integration/test_lang/test_function_calls.py
+++ b/tests/integration/test_lang/test_function_calls.py
@@ -3,6 +3,21 @@ import pytest
 from ..helpers import Suite
 
 
+@pytest.mark.integration_test
+def test_call_nullary():
+    code_py = """
+def helper() -> i32:
+    return 3
+
+@exported
+def testEntry() -> i32:
+    return helper()
+"""
+
+    result = Suite(code_py).run_code()
+
+    assert 3 == result.returned_value
+
 @pytest.mark.integration_test
 def test_call_pre_defined():
     code_py = """
diff --git a/tests/integration/test_lang/test_literals.py b/tests/integration/test_lang/test_literals.py
index 5593341..c0b8539 100644
--- a/tests/integration/test_lang/test_literals.py
+++ b/tests/integration/test_lang/test_literals.py
@@ -1,6 +1,6 @@
 import pytest
 
-from phasm.type3.entry import Type3Exception
+from phasm.type5.solver import Type5SolverException
 
 from ..helpers import Suite
 
@@ -15,7 +15,7 @@ def testEntry() -> u8:
     return CONSTANT
 """
 
-    with pytest.raises(Type3Exception, match=r'Must fit in 1 byte\(s\)'):
+    with pytest.raises(Type5SolverException, match=r'Must fit in 1 byte\(s\)'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -26,5 +26,5 @@ def testEntry() -> u8:
     return 1000
 """
 
-    with pytest.raises(Type3Exception, match=r'Must fit in 1 byte\(s\)'):
+    with pytest.raises(Type5SolverException, match=r'Must fit in 1 byte\(s\)'):
         Suite(code_py).run_code()
diff --git a/tests/integration/test_lang/test_second_order_functions.py b/tests/integration/test_lang/test_second_order_functions.py
index 395d804..343624e 100644
--- a/tests/integration/test_lang/test_second_order_functions.py
+++ b/tests/integration/test_lang/test_second_order_functions.py
@@ -1,6 +1,6 @@
 import pytest
 
-from phasm.type3.entry import Type3Exception
+from phasm.type5.solver import Type5SolverException
 
 from ..helpers import Suite
 
@@ -78,11 +78,29 @@ def testEntry() -> i32:
     assert 42 == result.returned_value
 
 @pytest.mark.integration_test
-def test_sof_wrong_argument_type():
+def test_sof_function_with_wrong_argument_type_use():
     code_py = """
-def double(left: f32) -> f32:
+def double(left: i32) -> i32:
     return left * 2
 
+def action(applicable: Callable[i32, i32], left: f32) -> i32:
+    return applicable(left)
+
+@exported
+def testEntry() -> i32:
+    return action(double, 13.0)
+"""
+
+    match = r'Callable\[i32, i32\] ~ Callable\[f32, i32\]'
+    with pytest.raises(Type5SolverException, match=match):
+        Suite(code_py).run_code()
+
+@pytest.mark.integration_test
+def test_sof_function_with_wrong_argument_type_pass():
+    code_py = """
+def double(left: f32) -> i32:
+    return truncate(left) * 2
+
 def action(applicable: Callable[i32, i32], left: i32) -> i32:
     return applicable(left)
 
@@ -91,11 +109,12 @@ def testEntry() -> i32:
     return action(double, 13)
 """
 
-    with pytest.raises(Type3Exception, match=r'Callable\[f32, f32\] must be Callable\[i32, i32\] instead'):
+    match = r'Callable\[Callable\[i32, i32\], i32, i32\] ~ Callable\[Callable\[f32, i32\], p_[0-9]+, i32\]'
+    with pytest.raises(Type5SolverException, match=match):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
-def test_sof_wrong_return():
+def test_sof_function_with_wrong_return_type_use():
     code_py = """
 def double(left: i32) -> i32:
     return left * 2
@@ -103,17 +122,35 @@ def double(left: i32) -> i32:
 def action(applicable: Callable[i32, i32], left: i32) -> f32:
     return applicable(left)
 
+@exported
+def testEntry() -> f32:
+    return action(double, 13)
+"""
+
+    match = r'Callable\[i32, i32\] ~ Callable\[i32, f32\]'
+    with pytest.raises(Type5SolverException, match=match):
+        Suite(code_py).run_code()
+
+@pytest.mark.integration_test
+def test_sof_function_with_wrong_return_type_pass():
+    code_py = """
+def double(left: i32) -> f32:
+    return convert(left) * 2
+
+def action(applicable: Callable[i32, i32], left: i32) -> i32:
+    return applicable(left)
+
 @exported
 def testEntry() -> i32:
     return action(double, 13)
 """
 
-    with pytest.raises(Type3Exception, match=r'f32 must be i32 instead'):
+    match = r'Callable\[Callable\[i32, i32\], i32, i32\] ~ Callable\[Callable\[i32, f32\], p_[0-9]+, i32\]'
+    with pytest.raises(Type5SolverException, match=match):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
-@pytest.mark.skip('FIXME: Probably have the remainder be the a function type')
-def test_sof_wrong_not_enough_args_call():
+def test_sof_not_enough_args_use():
     code_py = """
 def add(left: i32, right: i32) -> i32:
     return left + right
@@ -126,11 +163,12 @@ def testEntry() -> i32:
     return action(add, 13)
 """
 
-    with pytest.raises(Type3Exception, match=r'f32 must be i32 instead'):
+    match = r'Callable\[i32, i32, i32\] ~ Callable\[i32, i32\]'
+    with pytest.raises(Type5SolverException, match=match):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
-def test_sof_wrong_not_enough_args_refere():
+def test_sof_not_enough_args_pass():
     code_py = """
 def double(left: i32) -> i32:
     return left * 2
@@ -143,12 +181,12 @@ def testEntry() -> i32:
     return action(double, 13, 14)
 """
 
-    with pytest.raises(Type3Exception, match=r'Callable\[i32, i32\] must be Callable\[i32, i32, i32\] instead'):
+    match = r'Callable\[Callable\[i32, i32, i32\], i32, i32, i32\] ~ Callable\[Callable\[i32, i32\], p_[0-9]+, p_[0-9]+, i32\]'
+    with pytest.raises(Type5SolverException, match=match):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
-@pytest.mark.skip('FIXME: Probably have the remainder be the a function type')
-def test_sof_wrong_too_many_args_call():
+def test_sof_too_many_args_use():
     code_py = """
 def thirteen() -> i32:
     return 13
@@ -161,22 +199,24 @@ def testEntry() -> i32:
     return action(thirteen, 13)
 """
 
-    with pytest.raises(Type3Exception, match=r'f32 must be i32 instead'):
-        Suite(code_py).run_code()
+    match = r'Callable\[i32\] ~ Callable\[i32, i32\]'
+    with pytest.raises(Type5SolverException, match=match):
+        Suite(code_py).run_code(verbose=True)
 
 @pytest.mark.integration_test
-def test_sof_wrong_too_many_args_refere():
+def test_sof_too_many_args_pass():
     code_py = """
 def double(left: i32) -> i32:
     return left * 2
 
-def action(applicable: Callable[i32]) -> i32:
+def action(applicable: Callable[i32], left: i32, right: i32) -> i32:
     return applicable()
 
 @exported
 def testEntry() -> i32:
-    return action(double)
+    return action(double, 13, 14)
 """
 
-    with pytest.raises(Type3Exception, match=r'Callable\[i32, i32\] must be Callable\[i32\] instead'):
+    match = r'Callable\[Callable\[i32\], i32, i32, i32\] ~ Callable\[Callable\[i32, i32\], p_[0-9]+, p_[0-9]+, i32\]'
+    with pytest.raises(Type5SolverException, match=match):
         Suite(code_py).run_code()
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)