Notes

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)

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,9 @@ from ..type3.types import (
     TypeConstructor_Struct,
     TypeConstructor_Tuple,
 )
+from ..type5 import kindexpr as type5kindexpr
+from ..type5 import record as type5record
+from ..type5 import typeexpr as type5typeexpr
 from ..wasm import WasmType, WasmTypeInt32, WasmTypeNone
 from . import builtins
 
@@ -55,18 +58,28 @@ class MissingImplementationWarning(Warning):
 class BuildBase[G]:
     __slots__ = (
         'dynamic_array',
+        'dynamic_array_type5_constructor',
         'function',
+        'function_type5_constructor',
         'static_array',
+        'static_array_type5_constructor',
         'struct',
         'tuple_',
+        'tuple_type5_constructor_map',
 
         'none_',
+        'none_type5',
+        'unit_type5',
         'bool_',
+        'bool_type5',
+        'u8_type5',
+        'u32_type5',
 
         'type_info_map',
         'type_info_constructed',
 
         'types',
+        'type5s',
         'type_classes',
         'type_class_instances',
         'type_class_instance_methods',
@@ -84,6 +97,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 +106,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.
@@ -98,6 +115,7 @@ class BuildBase[G]:
     It should be applied with two arguments. It has a compile time
     determined length, and each argument is the same.
     """
+    static_array_type5_constructor: type5typeexpr.TypeConstructor
 
     struct: TypeConstructor_Struct
     """
@@ -113,16 +131,26 @@ class BuildBase[G]:
     determined length, and each argument can be different.
     """
 
+    tuple_type5_constructor_map: dict[int, type5typeexpr.TypeConstructor]
+
     none_: Type3
     """
     The none type, for when functions simply don't return anything. e.g., IO().
     """
+    none_type5: type5typeexpr.AtomicType
+
+    unit_type5: type5typeexpr.AtomicType
 
     bool_: Type3
     """
     The bool type, either True or False
     """
 
+    bool_type5: type5typeexpr.AtomicType
+
+    u8_type5: type5typeexpr.AtomicType
+    u32_type5: type5typeexpr.AtomicType
+
     type_info_map: dict[str, TypeInfo]
     """
     Map from type name to the info of that type
@@ -142,6 +170,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,8 +212,21 @@ class BuildBase[G]:
         self.struct = builtins.struct
         self.tuple_ = builtins.tuple_
 
+        S = type5kindexpr.Star()
+        N = type5kindexpr.Nat()
+
+        self.function_type5_constructor = type5typeexpr.TypeConstructor(kind=S >> (S >> S), name="function")
+        self.tuple_type5_constructor_map = {}
+        self.dynamic_array_type5_constructor = type5typeexpr.TypeConstructor(kind=S >> S, name="dynamic_array")
+        self.static_array_type5_constructor = type5typeexpr.TypeConstructor(kind=N >> (S >> S), name='static_array')
+
         self.bool_ = builtins.bool_
+        self.bool_type5 = type5typeexpr.AtomicType('bool')
+        self.unit_type5 = type5typeexpr.AtomicType('()')
         self.none_ = builtins.none_
+        self.none_type5 = type5typeexpr.AtomicType('None')
+        self.u8_type5 = type5typeexpr.AtomicType('u8')
+        self.u32_type5 = type5typeexpr.AtomicType('u32')
 
         self.type_info_map = {
             'None': TypeInfo('ptr', WasmTypeNone, 'unreachable', 'unreachable', 0, None),
@@ -193,6 +239,11 @@ class BuildBase[G]:
             'None': self.none_,
             'bool': self.bool_,
         }
+        self.type5s = {
+            'bool': self.bool_type5,
+            'u8': self.u8_type5,
+            'u32': self.u32_type5,
+        }
         self.type_classes = {}
         self.type_class_instances = set()
         self.type_class_instance_methods = {}
@@ -337,3 +388,178 @@ class BuildBase[G]:
             result += self.calculate_alloc_size(memtyp, is_member=True)
 
         raise Exception(f'{needle} not in {st_name}')
+
+    def type5_name(self, typ: type5typeexpr.TypeExpr) -> str:
+        func_args = self.type5_is_function(typ)
+        if func_args is not None:
+            return 'Callable[' + ', '.join(map(self.type5_name, func_args)) + ']'
+
+        tp_args = self.type5_is_tuple(typ)
+        if tp_args is not None:
+            return '(' + ', '.join(map(self.type5_name, tp_args)) + ', )'
+
+        da_arg = self.type5_is_dynamic_array(typ)
+        if da_arg is not None:
+            if da_arg == self.u8_type5:
+                return 'bytes'
+
+            return self.type5_name(da_arg) + '[...]'
+
+        sa_args = self.type5_is_static_array(typ)
+        if sa_args is not None:
+            sa_len, sa_type = sa_args
+            return f'{self.type5_name(sa_type)}[{sa_len}]'
+
+        return typ.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_make_tuple(self, args: Sequence[type5typeexpr.TypeExpr]) -> type5typeexpr.TypeApplication:
+        if not args:
+            raise TypeError("Tuples must at least one field")
+
+        arlen = len(args)
+        constructor = self.tuple_type5_constructor_map.get(arlen)
+        if constructor is None:
+            star = type5kindexpr.Star()
+
+            kind: type5kindexpr.Arrow = star >> star
+            for _ in range(len(args) - 1):
+                kind = star >> kind
+            constructor = type5typeexpr.TypeConstructor(kind=kind, name=f'tuple_{arlen}')
+            self.tuple_type5_constructor_map[arlen] = constructor
+
+        result: type5typeexpr.TypeApplication | None = None
+
+        for arg in args:
+            if result is None:
+                result = type5typeexpr.TypeApplication(
+                    constructor=constructor,
+                    argument=arg
+                )
+                continue
+
+            result = type5typeexpr.TypeApplication(
+                constructor=result,
+                argument=arg
+            )
+
+        assert result is not None  # type hint
+        result.name = '(' + ', '.join(x.name for x in args) + ', )'
+        return result
+
+    def type5_is_tuple(self, typeexpr: type5typeexpr.TypeExpr) -> list[type5typeexpr.TypeExpr] | None:
+        arg_list = []
+
+        while isinstance(typeexpr, type5typeexpr.TypeApplication):
+            arg_list.append(typeexpr.argument)
+            typeexpr = typeexpr.constructor
+
+        if not isinstance(typeexpr, type5typeexpr.TypeConstructor):
+            return None
+
+        if typeexpr not in self.tuple_type5_constructor_map.values():
+            return None
+
+        return list(reversed(arg_list))
+
+    def type5_make_record(self, name: str, fields: tuple[tuple[str, type5typeexpr.AtomicType | type5typeexpr.TypeApplication], ...]) -> type5record.Record:
+        return type5record.Record(name, fields)
+
+    def type5_is_record(self, arg: type5typeexpr.TypeExpr) -> tuple[tuple[str, type5typeexpr.AtomicType | type5typeexpr.TypeApplication], ...] | None:
+        if not isinstance(arg, type5record.Record):
+            return None
+
+        return arg.fields
+
+    def type5_make_dynamic_array(self, arg: type5typeexpr.TypeExpr) -> type5typeexpr.TypeApplication:
+        return type5typeexpr.TypeApplication(
+            constructor=self.dynamic_array_type5_constructor,
+            argument=arg,
+        )
+
+    def type5_is_dynamic_array(self, typeexpr: type5typeexpr.TypeExpr) -> type5typeexpr.TypeExpr | None:
+        """
+        Check if the given type expr is a concrete dynamic array type.
+
+        The element argument type is returned if so. Else, None is returned.
+        """
+        if not isinstance(typeexpr, type5typeexpr.TypeApplication):
+            return None
+        if typeexpr.constructor != self.dynamic_array_type5_constructor:
+            return None
+
+        return typeexpr.argument
+
+    def type5_make_static_array(self, len: int, arg: type5typeexpr.TypeExpr) -> type5typeexpr.TypeApplication:
+        return type5typeexpr.TypeApplication(
+            constructor=type5typeexpr.TypeApplication(
+                constructor=self.static_array_type5_constructor,
+                argument=type5typeexpr.TypeLevelNat(len),
+            ),
+            argument=arg,
+        )
+
+    def type5_is_static_array(self, typeexpr: type5typeexpr.TypeExpr) -> tuple[int, 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.static_array_type5_constructor:
+            return None
+
+        assert isinstance(typeexpr.constructor.argument, type5typeexpr.TypeLevelNat)  # type hint
+
+        return (
+            typeexpr.constructor.argument.value,
+            typeexpr.argument,
+        )

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)

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,
@@ -39,6 +40,8 @@ from .typeclasses import (
 
 
 class BuildDefault(BuildBase[Generator]):
+    __slots__ = ()
+
     def __init__(self) -> None:
         super().__init__()
 
@@ -82,6 +85,18 @@ class BuildDefault(BuildBase[Generator]):
             'bytes': bytes_,
         })
 
+        self.type5s.update({
+            'u16': type5typeexpr.AtomicType('u16'),
+            'u64': type5typeexpr.AtomicType('u64'),
+            'i8': type5typeexpr.AtomicType('i8'),
+            'i16': type5typeexpr.AtomicType('i16'),
+            'i32': type5typeexpr.AtomicType('i32'),
+            'i64': type5typeexpr.AtomicType('i64'),
+            'f32': type5typeexpr.AtomicType('f32'),
+            'f64': type5typeexpr.AtomicType('f64'),
+            'bytes': type5typeexpr.TypeApplication(self.dynamic_array_type5_constructor, self.u8_type5),
+        })
+
         tc_list = [
             bits,
             eq, ord,

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:
+        if isinstance(func, ourlang.StructConstructor):
-            # Builtin (-2) or auto generated (-1)
+            # Auto generated
             continue
 
         if result:
             result += '\n'
-        result += function(func)
+        result += function(inp, func)
 
     return result

phasm/compiler.py

@@ -314,7 +314,8 @@ 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['[]'])
+        assert inp.sourceref is not None  # TODO: Remove this
+        inp_as_fc = ourlang.FunctionCall(mod.build.type_classes['Subscriptable'].operators['[]'], inp.sourceref)
         inp_as_fc.type3 = inp.type3
         inp_as_fc.arguments = [inp.varref, inp.index]
 

phasm/ourlang.py

@@ -7,18 +7,44 @@ 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 record as type5record
+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
     type3: Type3 | None
+    type5: type5typeexpr.TypeExpr | None
 
-    def __init__(self) -> None:
+    def __init__(self, *, sourceref: SourceRef | None = None) -> None:
+        assert sourceref is not None  # TODO: Move to type level
+
+        self.sourceref = sourceref
         self.type3 = None
+        self.type5 = None
 
 class Constant(Expression):
     """
@@ -36,8 +62,8 @@ class ConstantPrimitive(Constant):
 
     value: Union[int, float]
 
-    def __init__(self, value: Union[int, float]) -> None:
+    def __init__(self, value: Union[int, float], sourceref: SourceRef) -> None:
-        super().__init__()
+        super().__init__(sourceref=sourceref)
         self.value = value
 
     def __repr__(self) -> str:
@@ -53,8 +79,8 @@ class ConstantMemoryStored(Constant):
 
     data_block: 'ModuleDataBlock'
 
-    def __init__(self, data_block: 'ModuleDataBlock') -> None:
+    def __init__(self, data_block: 'ModuleDataBlock', sourceref: SourceRef) -> None:
-        super().__init__()
+        super().__init__(sourceref=sourceref)
         self.data_block = data_block
 
 class ConstantBytes(ConstantMemoryStored):
@@ -65,8 +91,8 @@ class ConstantBytes(ConstantMemoryStored):
 
     value: bytes
 
-    def __init__(self, value: bytes, data_block: 'ModuleDataBlock') -> None:
+    def __init__(self, value: bytes, data_block: 'ModuleDataBlock', sourceref: SourceRef) -> None:
-        super().__init__(data_block)
+        super().__init__(data_block, sourceref=sourceref)
         self.value = value
 
     def __repr__(self) -> str:
@@ -83,8 +109,8 @@ class ConstantTuple(ConstantMemoryStored):
 
     value: List[Union[ConstantPrimitive, ConstantBytes, 'ConstantTuple', 'ConstantStruct']]
 
-    def __init__(self, value: List[Union[ConstantPrimitive, ConstantBytes, 'ConstantTuple', 'ConstantStruct']], data_block: 'ModuleDataBlock') -> None:
+    def __init__(self, value: List[Union[ConstantPrimitive, ConstantBytes, 'ConstantTuple', 'ConstantStruct']], data_block: 'ModuleDataBlock', sourceref: SourceRef) -> None:
-        super().__init__(data_block)
+        super().__init__(data_block, sourceref=sourceref)
         self.value = value
 
     def __repr__(self) -> str:
@@ -102,8 +128,8 @@ class ConstantStruct(ConstantMemoryStored):
     struct_type3: Type3
     value: List[Union[ConstantPrimitive, ConstantBytes, ConstantTuple, 'ConstantStruct']]
 
-    def __init__(self, struct_type3: Type3, value: List[Union[ConstantPrimitive, ConstantBytes, ConstantTuple, 'ConstantStruct']], data_block: 'ModuleDataBlock') -> None:
+    def __init__(self, struct_type3: Type3, value: List[Union[ConstantPrimitive, ConstantBytes, ConstantTuple, 'ConstantStruct']], data_block: 'ModuleDataBlock', sourceref: SourceRef) -> None:
-        super().__init__(data_block)
+        super().__init__(data_block, sourceref=sourceref)
         self.struct_type3 = struct_type3
         self.value = value
 
@@ -121,8 +147,8 @@ class VariableReference(Expression):
 
     variable: Union['ModuleConstantDef', 'FunctionParam'] # also possibly local
 
-    def __init__(self, variable: Union['ModuleConstantDef', 'FunctionParam']) -> None:
+    def __init__(self, variable: Union['ModuleConstantDef', 'FunctionParam'], sourceref: SourceRef) -> None:
-        super().__init__()
+        super().__init__(sourceref=sourceref)
         self.variable = variable
 
 class BinaryOp(Expression):
@@ -135,8 +161,8 @@ class BinaryOp(Expression):
     left: Expression
     right: Expression
 
-    def __init__(self, operator: Type3ClassMethod, left: Expression, right: Expression) -> None:
+    def __init__(self, operator: Type3ClassMethod, left: Expression, right: Expression, sourceref: SourceRef) -> None:
-        super().__init__()
+        super().__init__(sourceref=sourceref)
 
         self.operator = operator
         self.left = left
@@ -154,8 +180,8 @@ class FunctionCall(Expression):
     function: Union['Function', 'FunctionParam', Type3ClassMethod]
     arguments: List[Expression]
 
-    def __init__(self, function: Union['Function', 'FunctionParam', Type3ClassMethod]) -> None:
+    def __init__(self, function: Union['Function', 'FunctionParam', Type3ClassMethod], sourceref: SourceRef) -> None:
-        super().__init__()
+        super().__init__(sourceref=sourceref)
 
         self.function = function
         self.arguments = []
@@ -168,8 +194,8 @@ class FunctionReference(Expression):
 
     function: 'Function'
 
-    def __init__(self, function: 'Function') -> None:
+    def __init__(self, function: 'Function', sourceref: SourceRef) -> None:
-        super().__init__()
+        super().__init__(sourceref=sourceref)
         self.function = function
 
 class TupleInstantiation(Expression):
@@ -180,8 +206,8 @@ class TupleInstantiation(Expression):
 
     elements: List[Expression]
 
-    def __init__(self, elements: List[Expression]) -> None:
+    def __init__(self, elements: List[Expression], sourceref: SourceRef) -> None:
-        super().__init__()
+        super().__init__(sourceref=sourceref)
 
         self.elements = elements
 
@@ -195,8 +221,8 @@ class Subscript(Expression):
     varref: VariableReference
     index: Expression
 
-    def __init__(self, varref: VariableReference, index: Expression) -> None:
+    def __init__(self, varref: VariableReference, index: Expression, sourceref: SourceRef) -> None:
-        super().__init__()
+        super().__init__(sourceref=sourceref)
 
         self.varref = varref
         self.index = index
@@ -211,8 +237,8 @@ class AccessStructMember(Expression):
     struct_type3: Type3
     member: str
 
-    def __init__(self, varref: VariableReference,  struct_type3: Type3, member: str) -> None:
+    def __init__(self, varref: VariableReference,  struct_type3: Type3, member: str, sourceref: SourceRef) -> None:
-        super().__init__()
+        super().__init__(sourceref=sourceref)
 
         self.varref = varref
         self.struct_type3 = struct_type3
@@ -222,7 +248,14 @@ class Statement:
     """
     A statement within a function
     """
-    __slots__ = ()
+    __slots__ = ("sourceref", )
+
+    sourceref: SourceRef
+
+    def __init__(self, *, sourceref: SourceRef | None = None) -> None:
+        assert sourceref is not None  # TODO: Move to type level
+
+        self.sourceref = sourceref
 
 class StatementPass(Statement):
     """
@@ -230,13 +263,18 @@ class StatementPass(Statement):
     """
     __slots__ = ()
 
+    def __init__(self, sourceref: SourceRef) -> None:
+        super().__init__(sourceref=sourceref)
+
 class StatementReturn(Statement):
     """
     A return statement within a function
     """
     __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 +299,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 +319,43 @@ 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', 'struct_type5', 'sourceref', )
 
     struct_type3: Type3
-    lineno: int
+    struct_type5: type5record.Record
+    sourceref: SourceRef
 
-    def __init__(self, struct_type3: Type3, lineno: int) -> None:
+    def __init__(self, struct_type3: Type3, struct_type5: type5record.Record, sourceref: SourceRef) -> None:
         self.struct_type3 = struct_type3
-        self.lineno = lineno
+        self.struct_type5 = struct_type5
+        self.sourceref = sourceref
 
 class StructConstructor(Function):
     """
@@ -318,38 +364,44 @@ class StructConstructor(Function):
     A function will generated to instantiate a struct. The arguments
     will be the defaults
     """
-    __slots__ = ('struct_type3', )
+    __slots__ = ('struct_type3', 'struct_type5', )
 
     struct_type3: Type3
+    struct_type5: type5record.Record
 
-    def __init__(self, struct_type3: Type3) -> None:
+    def __init__(self, struct_type3: Type3, struct_type5: type5record.Record, sourceref: SourceRef) -> None:
-        super().__init__(f'@{struct_type3.name}@__init___@', -1, struct_type3)
+        super().__init__(f'@{struct_type3.name}@__init___@', sourceref, struct_type3)
 
         assert isinstance(struct_type3.application, TypeApplication_Struct)
 
+        mem_typ5_map = dict(struct_type5.fields)
+
         for mem, typ in struct_type3.application.arguments:
-            self.posonlyargs.append(FunctionParam(mem, typ, ))
+            self.posonlyargs.append(FunctionParam(mem, typ, mem_typ5_map[mem]))
             self.signature.args.append(typ)
 
         self.signature.args.append(struct_type3)
 
         self.struct_type3 = struct_type3
+        self.struct_type5 = struct_type5
 
 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 +435,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 +449,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 = {}

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
@@ -124,14 +127,16 @@ class OurVisitor[G]:
                     )
 
                 module.types[res.struct_type3.name] = res.struct_type3
-                module.functions[res.struct_type3.name] = StructConstructor(res.struct_type3)
+                module.type5s[res.struct_type5.name] = res.struct_type5
+                module.functions[res.struct_type3.name] = StructConstructor(res.struct_type3, res.struct_type5, res.sourceref)
+                module.functions[res.struct_type3.name].type5 = module.build.type5_make_function([x[1] for x in res.struct_type5.fields] + [res.struct_type5])
                 # Store that the definition was done in this module for the formatter
                 module.struct_definitions[res.struct_type3.name] = res
 
             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 +161,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, srf(module, node), 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 +183,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 +227,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
@@ -230,6 +245,7 @@ class OurVisitor[G]:
         _not_implemented(not node.decorator_list, 'ClassDef.decorator_list')
 
         members: Dict[str, Type3] = {}
+        members5: Dict[str, type5typeexpr.AtomicType | type5typeexpr.TypeApplication] = {}
 
         for stmt in node.body:
             if not isinstance(stmt, ast.AnnAssign):
@@ -249,7 +265,15 @@ 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)
+            field_type5 = self.visit_type5(module, stmt.annotation)
+            assert isinstance(field_type5, (type5typeexpr.AtomicType, type5typeexpr.TypeApplication, ))
+            members5[stmt.target.id] = field_type5
+
+        return StructDefinition(
+            module.build.struct(node.name, tuple(members.items())),
+            module.build.type5_make_record(node.name, tuple(members5.items())),
+            srf(module, node),
+        )
 
     def pre_visit_Module_AnnAssign(self, module: Module[G], node: ast.AnnAssign) -> ModuleConstantDef:
         if not isinstance(node.target, ast.Name):
@@ -262,8 +286,9 @@ class OurVisitor[G]:
 
             return ModuleConstantDef(
                 node.target.id,
-                node.lineno,
+                srf(module, node),
                 self.visit_type(module, node.annotation),
+                self.visit_type5(module, node.annotation),
                 value_data,
             )
 
@@ -275,8 +300,9 @@ class OurVisitor[G]:
             # Then return the constant as a pointer
             return ModuleConstantDef(
                 node.target.id,
-                node.lineno,
+                srf(module, node),
                 self.visit_type(module, node.annotation),
+                self.visit_type5(module, node.annotation),
                 value_data,
             )
 
@@ -288,8 +314,9 @@ class OurVisitor[G]:
             # Then return the constant as a pointer
             return ModuleConstantDef(
                 node.target.id,
-                node.lineno,
+                srf(module, node),
                 self.visit_type(module, node.annotation),
+                self.visit_type5(module, node.annotation),
                 value_data,
             )
 
@@ -328,7 +355,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),
+                srf(module, node),
             )
 
         if isinstance(node, ast.If):
@@ -349,7 +377,7 @@ class OurVisitor[G]:
             return result
 
         if isinstance(node, ast.Pass):
-            return StatementPass()
+            return StatementPass(srf(module, node))
 
         raise NotImplementedError(f'{node} as stmt in FunctionDef')
 
@@ -389,6 +417,7 @@ class OurVisitor[G]:
                 module.operators[operator],
                 self.visit_Module_FunctionDef_expr(module, function, our_locals, node.left),
                 self.visit_Module_FunctionDef_expr(module, function, our_locals, node.right),
+                srf(module, node),
             )
 
         if isinstance(node, ast.Compare):
@@ -417,6 +446,7 @@ class OurVisitor[G]:
                 module.operators[operator],
                 self.visit_Module_FunctionDef_expr(module, function, our_locals, node.left),
                 self.visit_Module_FunctionDef_expr(module, function, our_locals, node.comparators[0]),
+                srf(module, node),
             )
 
         if isinstance(node, ast.Call):
@@ -443,15 +473,15 @@ class OurVisitor[G]:
 
             if node.id in our_locals:
                 param = our_locals[node.id]
-                return VariableReference(param)
+                return VariableReference(param, srf(module, node))
 
             if node.id in module.constant_defs:
                 cdef = module.constant_defs[node.id]
-                return VariableReference(cdef)
+                return VariableReference(cdef, srf(module, node))
 
             if node.id in module.functions:
                 fun = module.functions[node.id]
-                return FunctionReference(fun)
+                return FunctionReference(fun, srf(module, node))
 
             _raise_static_error(node, f'Undefined variable {node.id}')
 
@@ -465,7 +495,7 @@ class OurVisitor[G]:
             if len(arguments) != len(node.elts):
                 raise NotImplementedError('Non-constant tuple members')
 
-            return TupleInstantiation(arguments)
+            return TupleInstantiation(arguments, srf(module, node))
 
         raise NotImplementedError(f'{node} as expr in FunctionDef')
 
@@ -490,7 +520,7 @@ class OurVisitor[G]:
 
             func = module.functions[node.func.id]
 
-        result = FunctionCall(func)
+        result = FunctionCall(func, sourceref=srf(module, node))
         result.arguments.extend(
             self.visit_Module_FunctionDef_expr(module, function, our_locals, arg_expr)
             for arg_expr in node.args
@@ -512,6 +542,7 @@ class OurVisitor[G]:
             varref,
             varref.variable.type3,
             node.attr,
+            srf(module, node),
         )
 
     def visit_Module_FunctionDef_Subscript(self, module: Module[G], function: Function, our_locals: OurLocals, node: ast.Subscript) -> Expression:
@@ -527,10 +558,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, srf(module, node))
         elif node.value.id in module.constant_defs:
             constant_def = module.constant_defs[node.value.id]
-            varref = VariableReference(constant_def)
+            varref = VariableReference(constant_def, srf(module, node))
         else:
             _raise_static_error(node, f'Undefined variable {node.value.id}')
 
@@ -538,7 +569,7 @@ class OurVisitor[G]:
             module, function, our_locals, node.slice,
         )
 
-        return Subscript(varref, slice_expr)
+        return Subscript(varref, slice_expr, srf(module, node))
 
     def visit_Module_Constant(self, module: Module[G], node: Union[ast.Constant, ast.Tuple, ast.Call]) -> Union[ConstantPrimitive, ConstantBytes, ConstantTuple, ConstantStruct]:
         if isinstance(node, ast.Tuple):
@@ -555,7 +586,7 @@ class OurVisitor[G]:
             data_block = ModuleDataBlock(tuple_data)
             module.data.blocks.append(data_block)
 
-            return ConstantTuple(tuple_data, data_block)
+            return ConstantTuple(tuple_data, data_block, srf(module, node))
 
         if isinstance(node, ast.Call):
             # Struct constant
@@ -583,18 +614,18 @@ class OurVisitor[G]:
 
             data_block = ModuleDataBlock(struct_data)
             module.data.blocks.append(data_block)
-            return ConstantStruct(struct_def.struct_type3, struct_data, data_block)
+            return ConstantStruct(struct_def.struct_type3, struct_data, data_block, srf(module, node))
 
         _not_implemented(node.kind is None, 'Constant.kind')
 
         if isinstance(node.value, (int, float, )):
-            return ConstantPrimitive(node.value)
+            return ConstantPrimitive(node.value, srf(module, node))
 
         if isinstance(node.value, bytes):
             data_block = ModuleDataBlock([])
             module.data.blocks.append(data_block)
 
-            result = ConstantBytes(node.value, data_block)
+            result = ConstantBytes(node.value, data_block, srf(module, node))
             data_block.data.append(result)
             return result
 
@@ -664,6 +695,69 @@ 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.Constant):
+            if node.value is None:
+                return module.build.none_type5
+
+            _raise_static_error(node, f'Unrecognized type {node.value}')
+
+        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
+                ])
+
+            if isinstance(node.slice, ast.Slice):
+                _raise_static_error(node, 'Must subscript using an index')
+
+            if not isinstance(node.slice, ast.Constant):
+                _raise_static_error(node, 'Must subscript using a constant index')
+
+            if node.slice.value is Ellipsis:
+                return module.build.type5_make_dynamic_array(
+                    self.visit_type5(module, node.value),
+                )
+
+            if not isinstance(node.slice.value, int):
+                _raise_static_error(node, 'Must subscript using a constant integer index')
+            if not isinstance(node.ctx, ast.Load):
+                _raise_static_error(node, 'Must be load context')
+
+            return module.build.type5_make_static_array(
+                node.slice.value,
+                self.visit_type5(module, node.value),
+            )
+
+        if isinstance(node, ast.Tuple):
+            if not isinstance(node.ctx, ast.Load):
+                _raise_static_error(node, 'Must be load context')
+
+            return module.build.type5_make_tuple(
+                [self.visit_type5(module, elt) for elt in node.elts],
+            )
+
+        raise NotImplementedError(node)
+
 def _not_implemented(check: Any, msg: str) -> None:
     if not check:
         raise NotImplementedError(msg)
@@ -672,3 +766,6 @@ def _raise_static_error(node: Union[ast.stmt, ast.expr], msg: str) -> NoReturn:
     raise StaticError(
         f'Static error on line {node.lineno}: {msg}'
     )
+
+def srf(mod: Module[Any], node: ast.stmt | ast.expr) -> SourceRef:
+    return SourceRef(mod.filename, node.lineno, node.col_offset)

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()

phasm/type5/constraints.py

@@ -0,0 +1,419 @@
+from __future__ import annotations
+
+import dataclasses
+from typing import Any, Callable, Iterable, Protocol, Sequence
+
+from ..build.base import BuildBase
+from ..ourlang import ConstantStruct, ConstantTuple, SourceRef
+from ..wasm import WasmTypeFloat32, WasmTypeFloat64, WasmTypeInt32, WasmTypeInt64
+from .kindexpr import KindExpr, Star
+from .typeexpr import (
+    TypeExpr,
+    TypeVariable,
+    is_concrete,
+    replace_variable,
+)
+from .unify import Action, 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 | None]
+
+    def __init__(self, build: BuildBase[Any]) -> None:
+        self.build = build
+        self.placeholder_update = {}
+
+    def make_placeholder(self, arg: ExpressionProtocol | None = None, kind: KindExpr = Star()) -> TypeVariable:
+        res = TypeVariable(kind, f"p_{len(self.placeholder_update)}")
+        self.placeholder_update[res] = arg
+        return res
+
+@dataclasses.dataclass
+class CheckResult:
+    _: dataclasses.KW_ONLY
+    done: bool = True
+    actions: ActionList = dataclasses.field(default_factory=ActionList)
+    new_constraints: list[ConstraintBase] = dataclasses.field(default_factory=list)
+    failures: list[Failure] = dataclasses.field(default_factory=list)
+
+    def to_str(self, type_namer: Callable[[TypeExpr], str]) -> str:
+        if not self.done and not self.actions and not self.new_constraints and not self.failures:
+            return '(skip for now)'
+
+        if self.done and not self.actions and not self.new_constraints and not self.failures:
+            return '(ok)'
+
+        if self.done and self.actions and not self.new_constraints and not self.failures:
+            return self.actions.to_str(type_namer)
+
+        if self.done and not self.actions and self.new_constraints and not self.failures:
+            return f'(got {len(self.new_constraints)} new constraints)'
+
+        if self.done and not self.actions and not self.new_constraints and self.failures:
+            return 'ERR: ' + '; '.join(x.msg for x in self.failures)
+
+        return f'{self.actions.to_str(type_namer)} {self.failures} {self.new_constraints} {self.done}'
+
+def skip_for_now() -> CheckResult:
+    return CheckResult(done=False)
+
+def new_constraints(lst: Iterable[ConstraintBase]) -> CheckResult:
+    return CheckResult(new_constraints=list(lst))
+
+def ok() -> CheckResult:
+    return CheckResult(done=True)
+
+def fail(msg: str) -> CheckResult:
+    return CheckResult(failures=[Failure(msg)])
+
+class ConstraintBase:
+    __slots__ = ("ctx", "sourceref", "comment",)
+
+    ctx: Context
+    sourceref: SourceRef
+    comment: str | None
+
+    def __init__(self, ctx: Context, sourceref: SourceRef, 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: Action) -> None:
+        if isinstance(action, ReplaceVariable):
+            self.replace_variable(action.var, action.typ)
+            return
+
+        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, 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 skip_for_now()
+
+        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 fail('Must be integer')
+
+            try:
+                self.literal.value.to_bytes(type_info.alloc_size, 'big', signed=type_info.signed)
+            except OverflowError:
+                return fail(f'Must fit in {type_info.alloc_size} byte(s)')
+
+            return ok()
+
+        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 ok()
+
+            return fail('Must be real')
+
+        da_arg = self.ctx.build.type5_is_dynamic_array(self.type)
+        if da_arg is not None:
+            if da_arg == self.ctx.build.u8_type5:
+                if not isinstance(self.literal.value, bytes):
+                    return fail('Must be bytes')
+
+                return ok()
+
+            if not isinstance(self.literal, ConstantTuple):
+                return fail('Must be tuple')
+
+            return new_constraints(
+                LiteralFitsConstraint(self.ctx, nod.sourceref, da_arg, nod)
+                for nod in self.literal.value
+            )
+
+        sa_args = self.ctx.build.type5_is_static_array(self.type)
+        if sa_args is not None:
+            sa_len, sa_typ = sa_args
+
+            if not isinstance(self.literal, ConstantTuple):
+                return fail('Must be tuple')
+
+            if len(self.literal.value) != sa_len:
+                return fail('Tuple element count mismatch')
+
+            return new_constraints(
+                LiteralFitsConstraint(self.ctx, nod.sourceref, sa_typ, nod)
+                for nod in self.literal.value
+            )
+
+        st_args = self.ctx.build.type5_is_record(self.type)
+        if st_args is not None:
+            if not isinstance(self.literal, ConstantStruct):
+                return fail('Must be struct')
+
+            if self.literal.struct_type3.name != self.type.name:  # TODO: Name based check is wonky
+                return fail('Must be right struct')
+
+            if len(self.literal.value) != len(st_args):
+                return fail('Struct member count mismatch')
+
+            return new_constraints(
+                LiteralFitsConstraint(self.ctx, nod.sourceref, nod_typ, nod)
+                for nod, (_, nod_typ) in zip(self.literal.value, st_args, strict=True)
+            )
+
+        tp_args = self.ctx.build.type5_is_tuple(self.type)
+        if tp_args is not None:
+            if not isinstance(self.literal, ConstantTuple):
+                return fail('Must be tuple')
+
+            if len(self.literal.value) != len(tp_args):
+                return fail('Tuple element count mismatch')
+
+            return new_constraints(
+                LiteralFitsConstraint(self.ctx, nod.sourceref, nod_typ, nod)
+                for nod, nod_typ in zip(self.literal.value, tp_args, strict=True)
+            )
+
+        raise NotImplementedError(self.type, 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, lft: TypeExpr, rgt: TypeExpr, *, comment: str | None = None) -> None:
+        super().__init__(ctx, sourceref, comment)
+
+        self.lft = lft
+        self.rgt = rgt
+
+    def check(self) -> CheckResult:
+        result = unify(self.lft, self.rgt)
+
+        if isinstance(result, Failure):
+            return CheckResult(failures=[result])
+
+        return CheckResult(actions=result)
+
+    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)}"
+
+class CanBeSubscriptedConstraint(ConstraintBase):
+    __slots__ = ('ret_type5', 'container_type5', 'index_type5', 'index_const', )
+
+    ret_type5: TypeExpr
+    container_type5: TypeExpr
+    index_type5: TypeExpr
+    index_const: int | None
+
+    def __init__(
+            self,
+            ctx: Context,
+            sourceref: SourceRef,
+            ret_type5: TypeExpr,
+            container_type5: TypeExpr,
+            index_type5: TypeExpr,
+            index_const: int | None,
+        ) -> None:
+        super().__init__(ctx, sourceref)
+
+        self.ret_type5 = ret_type5
+        self.container_type5 = container_type5
+        self.index_type5 = index_type5
+        self.index_const = index_const
+
+    def check(self) -> CheckResult:
+        if not is_concrete(self.container_type5):
+            return CheckResult(done=False)
+
+        da_arg = self.ctx.build.type5_is_dynamic_array(self.container_type5)
+        if da_arg is not None:
+            return new_constraints([
+                UnifyTypesConstraint(self.ctx, self.sourceref, da_arg, self.ret_type5),
+                UnifyTypesConstraint(self.ctx, self.sourceref, self.ctx.build.u32_type5, self.index_type5),
+            ])
+
+        sa_args = self.ctx.build.type5_is_static_array(self.container_type5)
+        if sa_args is not None:
+            sa_len, sa_typ = sa_args
+
+            if self.index_const is not None and (self.index_const < 0 or sa_len <= self.index_const):
+                return fail('Tuple index out of range')
+
+            return new_constraints([
+                UnifyTypesConstraint(self.ctx, self.sourceref, sa_typ, self.ret_type5),
+                UnifyTypesConstraint(self.ctx, self.sourceref, self.ctx.build.u32_type5, self.index_type5),
+            ])
+
+        tp_args = self.ctx.build.type5_is_tuple(self.container_type5)
+        if tp_args is not None:
+            if self.index_const is None:
+                return fail('Must index with integer literal')
+
+            if self.index_const < 0 or len(tp_args) <= self.index_const:
+                return fail('Tuple index out of range')
+
+            return new_constraints([
+                UnifyTypesConstraint(self.ctx, self.sourceref, tp_args[self.index_const], self.ret_type5),
+                UnifyTypesConstraint(self.ctx, self.sourceref, self.ctx.build.u32_type5, self.index_type5),
+            ])
+
+        return fail(f'Missing type class instantation: Subscriptable {self.container_type5.name}')
+
+    def replace_variable(self, var: TypeVariable, typ: TypeExpr) -> None:
+        self.ret_type5 = replace_variable(self.ret_type5, var, typ)
+        self.container_type5 = replace_variable(self.container_type5, var, typ)
+        self.index_type5 = replace_variable(self.index_type5, var, typ)
+
+    def __str__(self) -> str:
+        return f"[] :: t a -> b -> a ~ {self.ctx.build.type5_name(self.container_type5)} -> {self.ctx.build.type5_name(self.index_type5)} -> {self.ctx.build.type5_name(self.ret_type5)}"
+
+class CanAccessStructMemberConstraint(ConstraintBase):
+    __slots__ = ('ret_type5', 'struct_type5', 'member_name', )
+
+    ret_type5: TypeExpr
+    struct_type5: TypeExpr
+    member_name: str
+
+    def __init__(
+            self,
+            ctx: Context,
+            sourceref: SourceRef,
+            ret_type5: TypeExpr,
+            struct_type5: TypeExpr,
+            member_name: str,
+        ) -> None:
+        super().__init__(ctx, sourceref)
+
+        self.ret_type5 = ret_type5
+        self.struct_type5 = struct_type5
+        self.member_name = member_name
+
+    def check(self) -> CheckResult:
+        if not is_concrete(self.struct_type5):
+            return CheckResult(done=False)
+
+        st_args = self.ctx.build.type5_is_record(self.struct_type5)
+        if st_args is None:
+            return fail('Must be a struct')
+
+        member_dict = dict(st_args)
+
+        if self.member_name not in member_dict:
+            return fail('Must have a field with this name')
+
+        return UnifyTypesConstraint(self.ctx, self.sourceref, self.ret_type5, member_dict[self.member_name]).check()
+
+    def replace_variable(self, var: TypeVariable, typ: TypeExpr) -> None:
+        self.ret_type5 = replace_variable(self.ret_type5, var, typ)
+        self.struct_type5 = replace_variable(self.struct_type5, var, typ)
+
+    def __str__(self) -> str:
+        st_args = self.ctx.build.type5_is_record(self.struct_type5)
+        member_dict = dict(st_args or [])
+        member_typ = member_dict.get(self.member_name)
+
+        if member_typ is None:
+            expect = 'a -> b'
+        else:
+            expect = f'{self.ctx.build.type5_name(self.struct_type5)} -> {self.ctx.build.type5_name(member_typ)}'
+
+        return f".{self.member_name} :: {expect} ~ {self.ctx.build.type5_name(self.struct_type5)} -> {self.ctx.build.type5_name(self.ret_type5)}"
+
+class FromTupleConstraint(ConstraintBase):
+    __slots__ = ('ret_type5', 'member_type5_list', )
+
+    ret_type5: TypeExpr
+    member_type5_list: list[TypeExpr]
+
+    def __init__(
+            self,
+            ctx: Context,
+            sourceref: SourceRef,
+            ret_type5: TypeExpr,
+            member_type5_list: Sequence[TypeExpr],
+        ) -> None:
+        super().__init__(ctx, sourceref)
+
+        self.ret_type5 = ret_type5
+        self.member_type5_list = list(member_type5_list)
+
+    def check(self) -> CheckResult:
+        if not is_concrete(self.ret_type5):
+            return CheckResult(done=False)
+
+        da_arg = self.ctx.build.type5_is_dynamic_array(self.ret_type5)
+        if da_arg is not None:
+            return CheckResult(new_constraints=[
+                UnifyTypesConstraint(self.ctx, self.sourceref, da_arg, x)
+                for x in self.member_type5_list
+            ])
+
+        sa_args = self.ctx.build.type5_is_static_array(self.ret_type5)
+        if sa_args is not None:
+            sa_len, sa_typ = sa_args
+            if sa_len != len(self.member_type5_list):
+                return fail('Tuple element count mismatch')
+
+            return CheckResult(new_constraints=[
+                UnifyTypesConstraint(self.ctx, self.sourceref, sa_typ, x)
+                for x in self.member_type5_list
+            ])
+
+        tp_args = self.ctx.build.type5_is_tuple(self.ret_type5)
+        if tp_args is not None:
+            if len(tp_args) != len(self.member_type5_list):
+                return fail('Tuple element count mismatch')
+
+            return CheckResult(new_constraints=[
+                UnifyTypesConstraint(self.ctx, self.sourceref, act_typ, exp_typ)
+                for act_typ, exp_typ in zip(tp_args, self.member_type5_list, strict=True)
+            ])
+
+        raise NotImplementedError(self.ret_type5)
+
+    def replace_variable(self, var: TypeVariable, typ: TypeExpr) -> None:
+        self.ret_type5 = replace_variable(self.ret_type5, var, typ)
+        self.member_type5_list = [
+            replace_variable(x, var, typ)
+            for x in self.member_type5_list
+        ]
+
+    def __str__(self) -> str:
+        args = ', '.join(self.ctx.build.type5_name(x) for x in self.member_type5_list)
+        return f'FromTuple {self.ctx.build.type5_name(self.ret_type5)} ~ ({args}, )'

phasm/type5/fromast.py

@@ -0,0 +1,270 @@
+from typing import Any, Generator
+
+from .. import ourlang
+from ..type3 import functions as type3functions
+from ..type3 import typeclasses as type3classes
+from ..type3 import types as type3types
+from .constraints import (
+    CanAccessStructMemberConstraint,
+    CanBeSubscriptedConstraint,
+    ConstraintBase,
+    Context,
+    FromTupleConstraint,
+    LiteralFitsConstraint,
+    UnifyTypesConstraint,
+)
+from .kindexpr import Star
+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_binary_operator(ctx: Context, inp: ourlang.BinaryOp, phft: TypeVariable) -> ConstraintGenerator:
+    yield from expression_function_call(
+        ctx,
+        _binary_op_to_function(ctx, inp),
+        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 isinstance(inp.function, type3classes.Type3ClassMethod):
+        func_type = _signature_to_type5(ctx, inp.function.signature)
+    else:
+        assert isinstance(inp.function.type5, TypeExpr)
+        func_type = inp.function.type5
+
+    expr_type = ctx.build.type5_make_function(arg_typ_list + [phft])
+
+    yield UnifyTypesConstraint(ctx, inp.sourceref, func_type, 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_tuple_instantiation(ctx: Context, inp: ourlang.TupleInstantiation, phft: TypeVariable) -> ConstraintGenerator:
+    arg_typ_list = []
+    for arg in inp.elements:
+        arg_tv = ctx.make_placeholder(arg)
+        yield from expression(ctx, arg, arg_tv)
+        arg_typ_list.append(arg_tv)
+
+    yield FromTupleConstraint(ctx, inp.sourceref, phft, arg_typ_list)
+
+def expression_subscript(ctx: Context, inp: ourlang.Subscript, phft: TypeVariable) -> ConstraintGenerator:
+    varref_phft = ctx.make_placeholder(inp.varref)
+    index_phft = ctx.make_placeholder(inp.index)
+
+    yield from expression(ctx, inp.varref, varref_phft)
+    yield from expression(ctx, inp.index, index_phft)
+
+    if isinstance(inp.index, ourlang.ConstantPrimitive) and isinstance(inp.index.value, int):
+        yield CanBeSubscriptedConstraint(ctx, inp.sourceref, phft, varref_phft, index_phft, inp.index.value)
+    else:
+        yield CanBeSubscriptedConstraint(ctx, inp.sourceref, phft, varref_phft, index_phft, None)
+
+def expression_access_struct_member(ctx: Context, inp: ourlang.AccessStructMember, phft: TypeVariable) -> ConstraintGenerator:
+    varref_phft = ctx.make_placeholder(inp.varref)
+
+    yield from expression_variable_reference(ctx, inp.varref, varref_phft)
+
+    yield CanAccessStructMemberConstraint(ctx, inp.sourceref, phft, varref_phft, inp.member)
+
+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.BinaryOp):
+        yield from expression_binary_operator(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
+
+    if isinstance(inp, ourlang.TupleInstantiation):
+        yield from expression_tuple_instantiation(ctx, inp, phft)
+        return
+
+    if isinstance(inp, ourlang.Subscript):
+        yield from expression_subscript(ctx, inp, phft)
+        return
+
+    if isinstance(inp, ourlang.AccessStructMember):
+        yield from expression_access_struct_member(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 from expression(ctx, inp.value, phft)
+    yield UnifyTypesConstraint(ctx, inp.sourceref, type5, phft)
+
+def statement_if(ctx: Context, fun: ourlang.Function, inp: ourlang.StatementIf) -> ConstraintGenerator:
+    test_phft = ctx.make_placeholder(inp.test)
+
+    yield from expression(ctx, inp.test, test_phft)
+
+    yield UnifyTypesConstraint(ctx, inp.test.sourceref, test_phft, ctx.build.bool_type5)
+
+    for stmt in inp.statements:
+        yield from statement(ctx, fun, stmt)
+
+    for stmt in inp.else_statements:
+        yield from statement(ctx, fun, stmt)
+
+def statement(ctx: Context, fun: ourlang.Function, inp: ourlang.Statement) -> ConstraintGenerator:
+    if isinstance(inp, ourlang.StatementReturn):
+        yield from statement_return(ctx, fun, inp)
+        return
+
+    if isinstance(inp, ourlang.StatementIf):
+        yield from statement_if(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?
+
+def _binary_op_to_function(ctx: Context, inp: ourlang.BinaryOp) -> ourlang.FunctionCall:
+    """
+    Temporary method while migrating from type3 to type5
+    """
+    opr = inp.operator
+    fun = ourlang.Function(opr.name, ourlang.SourceRef("(generated)", -1, -1), ctx.build.none_)
+    fun.type5 = _signature_to_type5(ctx, opr.signature)
+
+    assert inp.sourceref is not None  # TODO: sourceref required
+    call = ourlang.FunctionCall(fun, inp.sourceref)
+    call.arguments = [inp.left, inp.right]
+    return call
+
+class TypeVarMap:
+    __slots__ = ('ctx', 'cache', )
+
+    ctx: Context
+    cache: dict[type3functions.TypeVariable, TypeVariable | TypeApplication]
+
+    def __init__(self, ctx: Context):
+        self.ctx = ctx
+        self.cache = {}
+
+    def __getitem__(self, var: type3functions.TypeVariable) -> TypeVariable | TypeApplication:
+        exists = self.cache.get(var)
+        if exists is not None:
+            return exists
+
+        if isinstance(var.application, type3functions.TypeVariableApplication_Nullary):
+            res_var = self.ctx.make_placeholder()
+            self.cache[var] = res_var
+            return res_var
+
+        if isinstance(var.application, type3functions.TypeVariableApplication_Unary):
+            # TODO: t a -> t a
+            # solve by caching var.application.constructor in separate map
+            cvar = self.ctx.make_placeholder(kind=Star() >> Star())
+            avar = self.__getitem__(var.application.arguments)
+            res_app = TypeApplication(constructor=cvar, argument=avar)
+            self.cache[var] = res_app
+            return res_app
+
+        raise NotImplementedError(var)
+
+def _signature_to_type5(ctx: Context, signature: type3functions.FunctionSignature) -> TypeExpr:
+    """
+    Temporary hack while migrating from type3 to type5
+    """
+    tv_map = TypeVarMap(ctx)
+
+    args: list[TypeExpr] = []
+    for t3arg in signature.args:
+        if isinstance(t3arg, type3types.Type3):
+            args.append(ctx.build.type5s[t3arg.name])
+            continue
+
+        if isinstance(t3arg, type3functions.TypeVariable):
+            args.append(tv_map[t3arg])
+            continue
+
+        if isinstance(t3arg, type3functions.FunctionArgument):
+            func_t3arg_list: list[TypeExpr] = []
+            for func_t3arg in t3arg.args:
+                if isinstance(func_t3arg, type3types.Type3):
+                    func_t3arg_list.append(ctx.build.type5s[t3arg.name])
+                    continue
+
+                if isinstance(func_t3arg, type3functions.TypeVariable):
+                    func_t3arg_list.append(tv_map[func_t3arg])
+                    continue
+
+                raise NotImplementedError
+
+            args.append(ctx.build.type5_make_function(func_t3arg_list))
+            continue
+
+        raise NotImplementedError(t3arg)
+
+    return ctx.build.type5_make_function(args)

phasm/type5/kindexpr.py

@@ -0,0 +1,57 @@
+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 Nat:
+    def __rshift__(self, other: KindExpr) -> Arrow:
+        return Arrow(self, other)
+
+    def __str__(self) -> str:
+        return "Nat"
+
+    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 | Nat
+    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 | Nat | Arrow

phasm/type5/record.py

@@ -0,0 +1,43 @@
+from dataclasses import dataclass
+
+from .kindexpr import Star
+from .typeexpr import AtomicType, TypeApplication, is_concrete
+
+
+@dataclass
+class Record(AtomicType):
+    """
+    Records are a fundamental type. But we need to store some extra info.
+    """
+    fields: tuple[tuple[str, AtomicType | TypeApplication], ...]
+
+    def __init__(self, name: str, fields: tuple[tuple[str, AtomicType | TypeApplication], ...]) -> None:
+        for field_name, field_type in fields:
+            if field_type.kind != Star():
+                raise TypeError(f"Record fields must not be constructors ({field_name} :: {field_type})")
+
+            if not is_concrete(field_type):
+                raise TypeError("Record field types must be concrete types ({field_name} :: {field_type})")
+
+        super().__init__(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(TypeConstructor):
+#     """
+#     TODO.
+
+#     i.e.:
+#     ```
+#     class Foo[T, R]:
+#         lft: T
+#         rgt: R
+#     """
+#     name: str

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

phasm/type5/solver.py

@@ -0,0 +1,117 @@
+from typing import Any
+
+from ..ourlang import Module
+from .constraints import ConstraintBase, Context
+from .fromast import phasm_type5_generate_constraints
+from .typeexpr import TypeExpr, TypeVariable
+from .unify import ReplaceVariable
+
+MAX_RESTACK_COUNT = 10 # 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:
+                print(f"{constraint.sourceref!s}  {constraint!s}")
+            print()
+
+        new_constraint_list: list[ConstraintBase] = []
+        while constraint_list:
+            constraint = constraint_list.pop(0)
+            result = constraint.check()
+
+            if verbose:
+                print(f"{constraint.sourceref!s}  {constraint!s}")
+                print(f"{constraint.sourceref!s}  => {result.to_str(inp.build.type5_name)}")
+
+            if not result:
+                # None or empty list
+                # Means it checks out and we don't need do anything
+                continue
+
+            while result.actions:
+                action = result.actions.pop(0)
+
+                if isinstance(action, ReplaceVariable):
+                    action_var: TypeExpr = action.var
+                    while isinstance(action_var, TypeVariable) and action_var in placeholder_types:
+                        action_var = placeholder_types[action_var]
+
+                    action_typ: TypeExpr = action.typ
+                    while isinstance(action_typ, TypeVariable) and action_typ in placeholder_types:
+                        action_typ = placeholder_types[action_typ]
+
+                    # print(inp.build.type5_name(action_var), ':=', inp.build.type5_name(action_typ))
+
+                    if action_var == action_typ:
+                        continue
+
+                    if not isinstance(action_var, TypeVariable) and isinstance(action_typ, TypeVariable):
+                        action_typ, action_var = action_var, action_typ
+
+                    if isinstance(action_var, TypeVariable):
+                        placeholder_types[action_var] = action_typ
+
+                        for oth_const in new_constraint_list + constraint_list:
+                            if oth_const is constraint and result.done:
+                                continue
+
+                            old_str = str(oth_const)
+                            oth_const.replace_variable(action_var, action_typ)
+                            new_str = str(oth_const)
+
+                            if verbose and old_str != new_str:
+                                print(f"{oth_const.sourceref!s}  => - {old_str!s}")
+                                print(f"{oth_const.sourceref!s}  => + {new_str!s}")
+                        continue
+
+                    error_list.append((str(constraint.sourceref), str(constraint), "Not the same type", ))
+                    if verbose:
+                        print(f"{constraint.sourceref!s}  => ERR: Conflict in applying {action.to_str(inp.build.type5_name)}")
+                    continue
+
+                # Action of unsupported type
+                raise NotImplementedError(action)
+
+            for failure in result.failures:
+                error_list.append((str(constraint.sourceref), str(constraint), failure.msg, ))
+
+            new_constraint_list.extend(result.new_constraints)
+
+            if result.done:
+                continue
+
+            new_constraint_list.append(constraint)
+
+        if error_list:
+            raise Type5SolverException(error_list)
+
+        if not new_constraint_list:
+            break
+
+        if verbose:
+            print()
+            print('New round')
+
+        constraint_list = new_constraint_list
+
+    if new_constraint_list:
+        raise Type5SolverException('Was unable to complete typing this program')
+
+    for placeholder, expression in ctx.placeholder_update.items():
+        if expression is None:
+            continue
+
+        expression.type5 = placeholder_types[placeholder]

phasm/type5/typeexpr.py

@@ -0,0 +1,147 @@
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import Callable, Sequence
+
+from .kindexpr import Arrow, KindExpr, Nat, 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 TypeLevelNat(TypeExpr):
+    value: int
+
+    def __init__(self, nat: int) -> None:
+        assert 0 <= nat
+
+        super().__init__(Nat(), str(nat))
+
+        self.value = nat
+
+@dataclass
+class TypeVariable(TypeExpr):
+    """
+    A placeholder in a type expression
+    """
+    constraints: Sequence[Callable[[TypeExpr], bool]] = ()
+
+    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 isinstance(constructor.kind, Nat):
+            raise TypeError("A constructor cannot be a number")
+
+        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, TypeLevelNat):
+        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:
+    assert var.kind == rep_expr.kind, (var, rep_expr, )
+
+    if isinstance(expr, AtomicType):
+        # Nothing to replace
+        return expr
+
+    if isinstance(expr, TypeLevelNat):
+        # Nothing to replace
+        return expr
+
+    if isinstance(expr, TypeVariable):
+        if expr == var:
+            return rep_expr
+        return expr
+
+    if isinstance(expr, TypeConstructor):
+        # Nothing to replace
+        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

phasm/type5/unify.py

@@ -0,0 +1,120 @@
+from dataclasses import dataclass
+from typing import Callable
+
+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:
+    def to_str(self, type_namer: Callable[[TypeExpr], str]) -> str:
+        raise NotImplementedError
+
+class ActionList(list[Action]):
+    def to_str(self, type_namer: Callable[[TypeExpr], str]) -> str:
+        return '{' + ', '.join((x.to_str(type_namer) for x in self)) + '}'
+
+UnifyResult = Failure | ActionList
+
+@dataclass
+class ReplaceVariable(Action):
+    var: TypeVariable
+    typ: TypeExpr
+
+    def to_str(self, type_namer: Callable[[TypeExpr], str]) -> str:
+        return f'{self.var.name} := {type_namer(self.typ)}'
+
+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')

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:

tests/integration/test_lang/generator.md

@@ -61,15 +61,9 @@ CONSTANT: (u32, ) = $VAL0
 
 ```py
 if TYPE_NAME.startswith('tuple_') or TYPE_NAME.startswith('static_array_') or TYPE_NAME.startswith('dynamic_array_'):
-    expect_type_error(
+    expect_type_error('Tuple element count mismatch')
-        'Tuple element count mismatch',
-        'The given literal must fit the expected type',
-    )
 else:
-    expect_type_error(
+    expect_type_error('Must be tuple')
-        'Must be tuple',
-        'The given literal must fit the expected type',
-    )
 ```
 
 # function_result_is_literal_ok
@@ -114,20 +108,11 @@ def testEntry() -> i32:
 
 ```py
 if TYPE_NAME.startswith('tuple_') or TYPE_NAME.startswith('static_array_') or TYPE_NAME.startswith('dynamic_array_'):
-    expect_type_error(
+    expect_type_error('Tuple element count mismatch')
-        'Mismatch between applied types argument count',
-        'The type of a tuple is a combination of its members',
-    )
 elif TYPE_NAME.startswith('struct_'):
-    expect_type_error(
+    expect_type_error('Not the same type')
-        TYPE + ' must be (u32, ) instead',
-        'The type of the value returned from function constant should match its return type',
-    )
 else:
-    expect_type_error(
+    expect_type_error('Must be tuple')
-        'Must be tuple',
-        'The given literal must fit the expected type',
-    )
 ```
 
 # function_result_is_module_constant_ok
@@ -175,16 +160,7 @@ def testEntry() -> i32:
 ```
 
 ```py
-if TYPE_NAME.startswith('tuple_') or TYPE_NAME.startswith('static_array_') or TYPE_NAME.startswith('dynamic_array_') or TYPE_NAME.startswith('struct_'):
+expect_type_error('Not the same type')
-    expect_type_error(
-        TYPE + ' must be (u32, ) instead',
-        'The type of the value returned from function constant should match its return type',
-    )
-else:
-    expect_type_error(
-        TYPE_NAME + ' must be (u32, ) instead',
-        'The type of the value returned from function constant should match its return type',
-    )
 ```
 
 # function_result_is_arg_ok
@@ -226,16 +202,7 @@ def select(x: $TYPE) -> (u32, ):
 ```
 
 ```py
-if TYPE_NAME.startswith('tuple_') or TYPE_NAME.startswith('static_array_') or TYPE_NAME.startswith('dynamic_array_') or TYPE_NAME.startswith('struct_'):
+expect_type_error('Not the same type')
-    expect_type_error(
-        TYPE + ' must be (u32, ) instead',
-        'The type of the value returned from function select should match its return type',
-    )
-else:
-    expect_type_error(
-        TYPE_NAME + ' must be (u32, ) instead',
-        'The type of the value returned from function select should match its return type',
-    )
 ```
 
 # function_arg_literal_ok
@@ -274,21 +241,11 @@ def testEntry() -> i32:
 
 ```py
 if TYPE_NAME.startswith('tuple_') or TYPE_NAME.startswith('static_array_') or TYPE_NAME.startswith('dynamic_array_'):
-    expect_type_error(
+    expect_type_error('Tuple element count mismatch')
-        'Mismatch between applied types argument count',
-        # FIXME: Shouldn't this be the same as for the else statement?
-        'The type of a tuple is a combination of its members',
-    )
 elif TYPE_NAME.startswith('struct_'):
-    expect_type_error(
+    expect_type_error('Not the same type')
-        TYPE + ' must be (u32, ) instead',
-        'The type of the value passed to argument 0 of function helper should match the type of that argument',
-    )
 else:
-    expect_type_error(
+    expect_type_error('Must be tuple')
-        'Must be tuple',
-        'The given literal must fit the expected type',
-    )
 ```
 
 # function_arg_module_constant_def_ok
@@ -330,14 +287,8 @@ def testEntry() -> i32:
 ```
 
 ```py
-if TYPE_NAME.startswith('tuple_') or TYPE_NAME.startswith('static_array_') or TYPE_NAME.startswith('dynamic_array_') or TYPE_NAME.startswith('struct_'):
+if TYPE_NAME.startswith('tuple_') or TYPE_NAME.startswith('static_array_') or TYPE_NAME.startswith('dynamic_array_'):
-    expect_type_error(
+    expect_type_error('Not the same type constructor')
-        TYPE + ' must be (u32, ) instead',
-        'The type of the value passed to argument 0 of function helper should match the type of that argument',
-    )
 else:
-    expect_type_error(
+    expect_type_error('Not the same type')
-        TYPE_NAME + ' must be (u32, ) instead',
-        'The type of the value passed to argument 0 of function helper should match the type of that argument',
-    )
 ```

tests/integration/test_lang/generator.py

@@ -41,11 +41,9 @@ def generate_assertion_expect(result, arg, given=None):
     result.append('result = Suite(code_py).run_code(' + ', '.join(repr(x) for x in given) + ')')
     result.append(f'assert {repr(arg)} == result.returned_value')
 
-def generate_assertion_expect_type_error(result, error_msg, error_comment = None):
+def generate_assertion_expect_type_error(result, error_msg):
-    result.append('with pytest.raises(Type3Exception) as exc_info:')
+    result.append(f'with pytest.raises(Type5SolverException, match={error_msg!r}):')
     result.append('    Suite(code_py).run_code()')
-    result.append(f'assert {repr(error_msg)} == exc_info.value.args[0][0].msg')
-    result.append(f'assert {repr(error_comment)} == exc_info.value.args[0][0].comment')
 
 def json_does_not_support_byte_or_tuple_values_fix(inp: Any):
     if isinstance(inp, (int, float, )):
@@ -98,7 +96,7 @@ def generate_code(markdown, template, settings):
     print('"""')
     print('import pytest')
     print()
-    print('from phasm.type3.entry import Type3Exception')
+    print('from phasm.type5.solver import Type5SolverException')
     print()
     print('from ..helpers import Suite')
     print()

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 = """

tests/integration/test_lang/test_if.py

@@ -1,5 +1,7 @@
 import pytest
 
+from phasm.type5.solver import Type5SolverException
+
 from ..helpers import Suite
 
 
@@ -70,3 +72,30 @@ def testEntry(a: i32, b: i32) -> i32:
     assert 2 == suite.run_code(20, 10).returned_value
     assert 1 == suite.run_code(10, 20).returned_value
     assert 0 == suite.run_code(10, 10).returned_value
+
+@pytest.mark.integration_test
+def test_if_type_invalid():
+    code_py = """
+@exported
+def testEntry(a: i32) -> i32:
+    if a:
+        return 1
+
+    return 0
+"""
+
+    with pytest.raises(Type5SolverException, match='i32 ~ bool'):
+        Suite(code_py).run_code(1)
+
+@pytest.mark.integration_test
+def test_if_type_ok():
+    code_py = """
+@exported
+def testEntry(a: bool) -> i32:
+    if a:
+        return 1
+
+    return 0
+"""
+
+    assert 1 == Suite(code_py).run_code(1).returned_value

tests/integration/test_lang/test_imports.py

@@ -1,6 +1,6 @@
 import pytest
 
-from phasm.type3.entry import Type3Exception
+from phasm.type5.solver import Type5SolverException
 
 from ..helpers import Suite
 
@@ -69,7 +69,7 @@ def testEntry(x: u32) -> u8:
     def helper(mul: int) -> int:
         return 4238 * mul
 
-    with pytest.raises(Type3Exception, match=r'u32 must be u8 instead'):
+    with pytest.raises(Type5SolverException, match='Not the same type'):
         Suite(code_py).run_code(
             imports={
                 'helper': helper,

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()

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, [^]]+\]'
+    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]+, [^]]+\]'
+    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,34 @@ 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)
+"""
+
+    with pytest.raises(Type5SolverException, match='f32 ~ i32'):
+        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]+, [^]]+\]'
+    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_not_enough_args_use():
-def test_sof_wrong_not_enough_args_call():
     code_py = """
 def add(left: i32, right: i32) -> i32:
     return left + right
@@ -126,11 +162,11 @@ def testEntry() -> i32:
     return action(add, 13)
 """
 
-    with pytest.raises(Type3Exception, match=r'f32 must be i32 instead'):
+    with pytest.raises(Type5SolverException, match='Not the same type'):
         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 +179,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]+, p_[0-9]+\]'
+    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_too_many_args_use():
-def test_sof_wrong_too_many_args_call():
     code_py = """
 def thirteen() -> i32:
     return 13
@@ -161,22 +197,24 @@ def testEntry() -> i32:
     return action(thirteen, 13)
 """
 
-    with pytest.raises(Type3Exception, match=r'f32 must be i32 instead'):
+    match = r'Callable\[i32\] ~ Callable\[i32, p_[0-9]+\]'
-        Suite(code_py).run_code()
+    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]+, p_[0-9]+\]'
+    with pytest.raises(Type5SolverException, match=match):
         Suite(code_py).run_code()

tests/integration/test_lang/test_static_array.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() -> i32:
     return 0
 """
 
-    with pytest.raises(Type3Exception, match='Member count mismatch'):
+    with pytest.raises(Type5SolverException, match='Tuple element count mismatch'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -28,7 +28,7 @@ def testEntry() -> i32:
     return 0
 """
 
-    with pytest.raises(Type3Exception, match='Member count mismatch'):
+    with pytest.raises(Type5SolverException, match='Tuple element count mismatch'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test

tests/integration/test_lang/test_struct.py

@@ -1,7 +1,7 @@
 import pytest
 
 from phasm.exceptions import StaticError
-from phasm.type3.entry import Type3Exception
+from phasm.type5.solver import Type5SolverException
 
 from ..helpers import Suite
 
@@ -76,7 +76,7 @@ class CheckedValueRed:
 CONST: CheckedValueBlue = CheckedValueRed(1)
 """
 
-    with pytest.raises(Type3Exception, match='CheckedValueBlue must be CheckedValueRed instead'):
+    with pytest.raises(Type5SolverException, match='Must be right struct'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -91,7 +91,20 @@ class CheckedValueRed:
 CONST: (CheckedValueBlue, u32, ) = (CheckedValueRed(1), 16, )
 """
 
-    with pytest.raises(Type3Exception, match='CheckedValueBlue must be CheckedValueRed instead'):
+    with pytest.raises(Type5SolverException, match='Must be right struct'):
+        Suite(code_py).run_code()
+
+@pytest.mark.integration_test
+def test_type_mismatch_struct_call_arg_count():
+    code_py = """
+class CheckedValue:
+    value1: i32
+    value2: i32
+
+CONST: CheckedValue = CheckedValue(1)
+"""
+
+    with pytest.raises(Type5SolverException, match='Struct member count mismatch'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -105,7 +118,7 @@ def testEntry(arg: Struct) -> (i32, i32, ):
     return arg.param
 """
 
-    with pytest.raises(Type3Exception, match=type_ + r' must be \(i32, i32, \) instead'):
+    with pytest.raises(Type5SolverException, match='Not the same type'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -132,7 +145,6 @@ class f32:
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
-@pytest.mark.skip(reason='FIXME: See constraintgenerator.py for AccessStructMember')
 def test_struct_not_accessible():
     code_py = """
 @exported
@@ -140,7 +152,67 @@ def testEntry(x: u8) -> u8:
     return x.y
 """
 
-    with pytest.raises(Type3Exception, match='u8 is not struct'):
+    with pytest.raises(Type5SolverException, match='Must be a struct'):
+        Suite(code_py).run_code()
+
+@pytest.mark.integration_test
+def test_struct_does_not_have_field():
+    code_py = """
+class CheckedValue:
+    value: i32
+
+@exported
+def testEntry(x: CheckedValue) -> u8:
+    return x.y
+"""
+
+    with pytest.raises(Type5SolverException, match='Must have a field with this name'):
+        Suite(code_py).run_code()
+
+@pytest.mark.integration_test
+def test_struct_literal_does_not_fit():
+    code_py = """
+class CheckedValue:
+    value: i32
+
+@exported
+def testEntry() -> CheckedValue:
+    return 14
+"""
+
+    with pytest.raises(Type5SolverException, match='Must be struct'):
+        Suite(code_py).run_code()
+
+@pytest.mark.integration_test
+def test_struct_wrong_struct():
+    code_py = """
+class CheckedValue:
+    value: i32
+
+class MessedValue:
+    value: i32
+
+@exported
+def testEntry() -> CheckedValue:
+    return MessedValue(14)
+"""
+
+    with pytest.raises(Type5SolverException, match='Not the same type'):
+        Suite(code_py).run_code()
+
+@pytest.mark.integration_test
+def test_struct_wrong_arg_count():
+    code_py = """
+class CheckedValue:
+    value1: i32
+    value2: i32
+
+@exported
+def testEntry() -> CheckedValue:
+    return CheckedValue(14)
+"""
+
+    with pytest.raises(Type5SolverException, match='Not the same type'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test

tests/integration/test_lang/test_subscriptable.py

@@ -1,7 +1,7 @@
 import pytest
 import wasmtime
 
-from phasm.type3.entry import Type3Exception
+from phasm.type5.solver import Type5SolverException
 
 from ..helpers import Suite
 
@@ -71,7 +71,7 @@ def testEntry(f: {type_}) -> u32:
     return f[0]
 """
 
-    with pytest.raises(Type3Exception, match='u32 must be u8 instead'):
+    with pytest.raises(Type5SolverException, match='Not the same type'):
         Suite(code_py).run_code(in_put)
 
 @pytest.mark.integration_test
@@ -82,7 +82,7 @@ def testEntry(x: (u8, u32, u64), y: u8) -> u64:
     return x[y]
 """
 
-    with pytest.raises(Type3Exception, match='Must index with integer literal'):
+    with pytest.raises(Type5SolverException, match='Must index with integer literal'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -93,7 +93,7 @@ def testEntry(x: (u8, u32, u64)) -> u64:
     return x[0.0]
 """
 
-    with pytest.raises(Type3Exception, match='Must index with integer literal'):
+    with pytest.raises(Type5SolverException, match='Must index with integer literal'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -109,7 +109,7 @@ def testEntry(x: {type_}) -> u8:
     return x[-1]
 """
 
-    with pytest.raises(Type3Exception, match='Tuple index out of range'):
+    with pytest.raises(Type5SolverException, match='Tuple index out of range'):
         Suite(code_py).run_code(in_put)
 
 @pytest.mark.integration_test
@@ -120,7 +120,7 @@ def testEntry(x: (u8, u32, u64)) -> u64:
     return x[4]
 """
 
-    with pytest.raises(Type3Exception, match='Tuple index out of range'):
+    with pytest.raises(Type5SolverException, match='Tuple index out of range'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -147,5 +147,5 @@ def testEntry(x: u8) -> u8:
     return x[0]
 """
 
-    with pytest.raises(Type3Exception, match='Missing type class instantation: Subscriptable u8'):
+    with pytest.raises(Type5SolverException, match='Missing type class instantation: Subscriptable u8'):
         Suite(code_py).run_code()

tests/integration/test_lang/test_tuple.py

@@ -1,6 +1,6 @@
 import pytest
 
-from phasm.type3.entry import Type3Exception
+from phasm.type5.solver import Type5SolverException
 
 from ..helpers import Suite
 
@@ -41,7 +41,7 @@ def test_assign_to_tuple_with_tuple():
 CONSTANT: (u32, ) = 0
 """
 
-    with pytest.raises(Type3Exception, match='Must be tuple'):
+    with pytest.raises(Type5SolverException, match='Must be tuple'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -50,7 +50,7 @@ def test_tuple_constant_too_few_values():
 CONSTANT: (u32, u8, u8, ) = (24, 57, )
 """
 
-    with pytest.raises(Type3Exception, match='Tuple element count mismatch'):
+    with pytest.raises(Type5SolverException, match='Tuple element count mismatch'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -59,7 +59,7 @@ def test_tuple_constant_too_many_values():
 CONSTANT: (u32, u8, u8, ) = (24, 57, 1, 1, )
 """
 
-    with pytest.raises(Type3Exception, match='Tuple element count mismatch'):
+    with pytest.raises(Type5SolverException, match='Tuple element count mismatch'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -68,7 +68,7 @@ def test_tuple_constant_type_mismatch():
 CONSTANT: (u32, u8, u8, ) = (24, 4000, 1, )
 """
 
-    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

tests/integration/test_typeclasses/test_eq.py

@@ -1,6 +1,6 @@
 import pytest
 
-from phasm.type3.entry import Type3Exception
+from phasm.type5.solver import Type5SolverException
 
 from ..helpers import Suite
 
@@ -25,11 +25,11 @@ class Foo:
     val: i32
 
 @exported
-def testEntry(x: Foo, y: Foo) -> Foo:
+def testEntry(x: Foo, y: Foo) -> bool:
     return x == y
 """
 
-    with pytest.raises(Type3Exception, match='Missing type class instantation: Eq Foo'):
+    with pytest.raises(Type5SolverException, match='Missing type class instantation: Eq Foo'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -107,11 +107,11 @@ class Foo:
     val: i32
 
 @exported
-def testEntry(x: Foo, y: Foo) -> Foo:
+def testEntry(x: Foo, y: Foo) -> bool:
     return x != y
 """
 
-    with pytest.raises(Type3Exception, match='Missing type class instantation: Eq Foo'):
+    with pytest.raises(Type5SolverException, match='Missing type class instantation: Eq Foo'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test

tests/integration/test_typeclasses/test_foldable.py

@@ -1,6 +1,6 @@
 import pytest
 
-from phasm.type3.entry import Type3Exception
+from phasm.type5.solver import Type5SolverException
 
 from ..helpers import Suite
 from .test_natnum import FLOAT_TYPES, INT_TYPES
@@ -36,7 +36,7 @@ def testEntry(x: Foo[4]) -> Foo:
     return sum(x)
 """
 
-    with pytest.raises(Type3Exception, match='Missing type class instantation: NatNum Foo'):
+    with pytest.raises(Type5SolverException, match='Missing type class instantation: NatNum Foo'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -129,7 +129,7 @@ def testEntry(b: i32[{typ_arg}]) -> i32:
 """
     suite = Suite(code_py)
 
-    result = suite.run_code(tuple(in_put), with_traces=True, do_format_check=False)
+    result = suite.run_code(tuple(in_put))
     assert exp_result == result.returned_value
 
 @pytest.mark.integration_test
@@ -168,9 +168,12 @@ def testEntry(x: {in_typ}, y: i32, z: i64[3]) -> i32:
     return foldl(x, y, z)
 """
 
-    r_in_typ = in_typ.replace('[', '\\[').replace(']', '\\]')
+    match = {
+        'i8': 'Type shape mismatch',
+        'i8[3]': 'Kind mismatch',
+    }
 
-    with pytest.raises(Type3Exception, match=f'{r_in_typ} must be a function instead'):
+    with pytest.raises(Type5SolverException, match=match[in_typ]):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -184,7 +187,7 @@ def testEntry(i: i64, l: i64[3]) -> i64:
     return foldr(foo, i, l)
 """
 
-    with pytest.raises(Type3Exception, match=r'Callable\[i64, i64, i64\] must be Callable\[i32, i64, i64\] instead'):
+    with pytest.raises(Type5SolverException, match='Not the same type'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -195,7 +198,7 @@ def testEntry(x: i32[5]) -> f64:
     return sum(x)
 """
 
-    with pytest.raises(Type3Exception, match='f64 must be i32 instead'):
+    with pytest.raises(Type5SolverException, match='Not the same type'):
         Suite(code_py).run_code((4, 5, 6, 7, 8, ))
 
 @pytest.mark.integration_test
@@ -206,16 +209,16 @@ def testEntry(x: i32) -> i32:
     return sum(x)
 """
 
-    with pytest.raises(Type3Exception, match='Missing type class instantation: Foldable i32.*i32 must be a constructed type instead'):
+    with pytest.raises(Type5SolverException, match='Type shape mismatch'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
 def test_foldable_not_foldable():
     code_py = """
 @exported
-def testEntry(x: (i32, u32, )) -> i32:
+def testEntry(x: (u32, i32, )) -> i32:
     return sum(x)
 """
 
-    with pytest.raises(Type3Exception, match='Missing type class instantation: Foldable tuple'):
+    with pytest.raises(Type5SolverException, match='Missing type class instantation: Foldable tuple'):
         Suite(code_py).run_code()