Fixes

- Moved the three ConstraintBase functions into one, as it was
  giving trouble calculating everything
- Gave each constraint the option to have a comment
- SameTypeConstraint now can have multiple arguments
- Redid the infinite loop detection
- Implemented some more basic operators
- Redid the division by zero for floats, it wasn't giving the
  right results.
- Also postponed the updating the AST type3 until afterwards
- Various linting fixes

phasm/codestyle.py

@@ -3,7 +3,7 @@ This module generates source code based on the parsed AST
 
 It's intented to be a "any color, as long as it's black" kind of renderer
 """
-from typing import Generator, Optional
+from typing import Generator
 
 from . import ourlang
 from .type3.types import TYPE3_ASSERTION_ERROR, Type3, Type3OrPlaceholder

phasm/compiler.py

@@ -410,7 +410,7 @@ def expression_fold(wgn: WasmGenerator, inp: ourlang.Fold) -> None:
         raise NotImplementedError(expression, inp, inp.iter.type)
 
     wgn.add_statement('nop', comment='acu :: u8')
-    acu_var = wgn.temp_var_u8(f'fold_{codestyle.type_(inp.type)}_acu')
+    acu_var = wgn.temp_var_u8(f'fold_{codestyle.type3(inp.type3)}_acu')
     wgn.add_statement('nop', comment='adr :: bytes*')
     adr_var = wgn.temp_var_i32('fold_i32_adr')
     wgn.add_statement('nop', comment='len :: i32')
@@ -430,7 +430,7 @@ def expression_fold(wgn: WasmGenerator, inp: ourlang.Fold) -> None:
     wgn.local.set(len_var)
 
     wgn.add_statement('nop', comment='i = 0')
-    idx_var = wgn.temp_var_i32(f'fold_{codestyle.type_(inp.type)}_idx')
+    idx_var = wgn.temp_var_i32(f'fold_{codestyle.type3(inp.type3)}_idx')
     wgn.i32.const(0)
     wgn.local.set(idx_var)
 
@@ -765,7 +765,7 @@ def _generate_struct_constructor(wgn: WasmGenerator, inp: ourlang.StructConstruc
     # Return the allocated address
     wgn.local.get(tmp_var)
 
-def _calculate_alloc_size(type3: Union[type3types.StructType3, type3types.Type3]) -> int:
+def _calculate_alloc_size(typ: Union[type3types.StructType3, type3types.Type3]) -> int:
     return 0 # FIXME: Stub
 
 def _calculate_member_offset(struct_type3: type3types.StructType3, member: str) -> int:

phasm/type3/constraints.py

@@ -3,13 +3,19 @@ This module contains possible constraints generated based on the AST
 
 These need to be resolved before the program can be compiled.
 """
-from typing import Dict, Tuple, Union
+from typing import Dict, Optional, List, Tuple, Union
 
 from .. import ourlang
 
 from . import types
 
 class Error:
+    """
+    An error returned by the check functions for a contraint
+
+    This means the programmer has to make some kind of chance to the
+    typing of their program before the compiler can do its thing.
+    """
     def __init__(self, msg: str) -> None:
         self.msg = msg
 
@@ -17,12 +23,18 @@ class Error:
         return f'Error({repr(self.msg)})'
 
 class RequireTypeSubstitutes:
-    pass
+    """
+    Returned by the check function for a contraint if they do not have all
+    their types substituted yet.
 
-CheckResult = Union[None, Error, RequireTypeSubstitutes]
+    Hopefully, another constraint will give the right information about the
+    typing of the program, so this constraint can be updated.
+    """
 
 SubstitutionMap = Dict[types.PlaceholderForType, types.Type3]
 
+CheckResult = Union[None, SubstitutionMap, Error, RequireTypeSubstitutes]
+
 HumanReadableRet = Tuple[str, Dict[str, Union[str, ourlang.Expression, types.Type3, types.PlaceholderForType]]]
 
 class Context:
@@ -36,28 +48,39 @@ class ConstraintBase:
     """
     Base class for constraints
     """
-    __slots__ = ()
+    __slots__ = ('comment', )
 
-    def check(self) -> CheckResult:
+    comment: Optional[str]
+    """
+    A comment to help the programmer with debugging the types in their program
+    """
+
+    def __init__(self, comment: Optional[str] = None) -> None:
+        self.comment = comment
+
+    def check(self, smap: SubstitutionMap) -> CheckResult:
         """
-        Checks if the constraint hold, returning an error if it doesn't
+        Checks if the constraint hold
+
+        smap will contain a mapping from placeholders to types, for
+        placeholders discovered from either other constraints or from
+        earlier calls to check in this constraint.
+
+        This function can return an error, if the constraint does not hold,
+        which indicates an error in the typing of the input program.
+
+        This function can return RequireTypeSubstitutes(), if we cannot deduce
+        all the types yet.
+
+        This function can return a SubstitutionMap, if during the evaluation
+        of the contraint we discovered new types. In this case, the constraint
+        is expected to hold.
+
+        This function can return None, if the constraint holds, but no new
+        information was deduced from evaluating this constraint.
         """
         raise NotImplementedError
 
-    def get_new_placeholder_substitutes(self) -> SubstitutionMap:
-        """
-        Returns any new placeholders that can be substituted for actual types
-        """
-        return {}
-
-    def substitute_placeholders(self, smap: SubstitutionMap) -> None:
-        """
-        Called with type substitutes, so you can update any placeholders
-        you may have with the known types. Note that this does not guarantee
-        that all types are known, you may still have some placeholders left.
-        """
-        raise NotImplementedError(self, self.substitute_placeholders)
-
     def human_readable(self) -> HumanReadableRet:
         """
         Returns a more human readable form of this constraint
@@ -66,71 +89,61 @@ class ConstraintBase:
 
 class SameTypeConstraint(ConstraintBase):
     """
-    Verifies that an expression has an expected type
+    Verifies that a number of types all are the same type
     """
-    __slots__ = ('expected', 'actual', 'message', )
+    __slots__ = ('type_list', )
 
-    expected: types.Type3OrPlaceholder
+    type_list: List[types.Type3OrPlaceholder]
-    actual: types.Type3OrPlaceholder
-    message: str
 
-    def __init__(self, expected: types.Type3OrPlaceholder, actual: types.Type3OrPlaceholder, message: str) -> None:
+    def __init__(self, *type_list: types.Type3OrPlaceholder, comment: Optional[str] = None) -> None:
-        self.expected = expected
+        super().__init__(comment=comment)
-        self.actual = actual
-        self.message = message
 
-    def check(self) -> CheckResult:
+        assert len(type_list) > 1
-        if isinstance(self.expected, types.PlaceholderForType) or isinstance(self.actual, types.PlaceholderForType):
+        self.type_list = [*type_list]
+
+    def check(self, smap: SubstitutionMap) -> CheckResult:
+        known_types = []
+        placeholders = []
+        for typ in self.type_list:
+            if isinstance(typ, types.Type3):
+                known_types.append(typ)
+                continue
+
+            if typ in smap:
+                known_types.append(smap[typ])
+                continue
+
+            placeholders.append(typ)
+
+        if not known_types:
             return RequireTypeSubstitutes()
 
-        if self.expected is self.actual:
+        first_type = known_types[0]
+        for typ in known_types[1:]:
+            if typ is not first_type:
+                return Error(f'{typ:s} must be {first_type:s} instead')
+
+        if not placeholders:
             return None
 
-        return Error(f'{self.expected:s} must be {self.actual:s} instead')
+        return {
-
+            typ: first_type
-    def get_new_placeholder_substitutes(self) -> SubstitutionMap:
+            for typ in placeholders
-        result: SubstitutionMap = {}
+        }
-
-        if isinstance(self.expected, types.Type3) and isinstance(self.actual, types.PlaceholderForType):
-            result = {
-                self.actual: self.expected
-            }
-
-            self.actual.get_substituted(self.expected)
-            self.actual = self.expected
-
-
-        if isinstance(self.actual, types.Type3) and isinstance(self.expected, types.PlaceholderForType):
-            result = {
-                self.expected: self.actual
-            }
-
-            self.expected.get_substituted(self.actual)
-            self.expected = self.actual
-
-        return result
-
-    def substitute_placeholders(self, smap: SubstitutionMap) -> None:
-        if isinstance(self.expected, types.PlaceholderForType) and self.expected in smap: # FIXME: Check recursive?
-            self.expected.get_substituted(smap[self.expected])
-            self.expected = smap[self.expected]
-
-        if isinstance(self.actual, types.PlaceholderForType) and self.actual in smap: # FIXME: Check recursive?
-            self.actual.get_substituted(smap[self.actual])
-            self.actual = smap[self.actual]
 
     def human_readable(self) -> HumanReadableRet:
         return (
-            '{expected} == {actual}',
+            ' == '.join('{t' + str(idx) + '}' for idx in range(len(self.type_list))),
             {
-                'expected': self.expected,
+                't' + str(idx): typ
-                'actual': self.actual,
+                for idx, typ in enumerate(self.type_list)
-                'comment': self.message,
             },
         )
 
     def __repr__(self) -> str:
-        return f'SameTypeConstraint({repr(self.expected)}, {repr(self.actual)}, {repr(self.message)})'
+        args = ', '.join(repr(x) for x in self.type_list)
+
+        return f'SameTypeConstraint({args}, comment={repr(self.comment)})'
 
 class MustImplementTypeClassConstraint(ConstraintBase):
     """
@@ -141,23 +154,31 @@ class MustImplementTypeClassConstraint(ConstraintBase):
     type_class3: str
     type3: types.Type3OrPlaceholder
 
-    def __init__(self, type_class3: str, type3: types.Type3OrPlaceholder) -> None:
+    def __init__(self, type_class3: str, type3: types.Type3OrPlaceholder, comment: Optional[str] = None) -> None:
+        super().__init__(comment=comment)
+
         self.type_class3 = type_class3
         self.type3 = type3
 
-    def substitute_placeholders(self, smap: SubstitutionMap) -> None:
+    def check(self, smap: SubstitutionMap) -> CheckResult:
-        if isinstance(self.type3, types.PlaceholderForType) and self.type3 in smap: # FIXME: Check recursive?
+        typ = self.type3
-            self.type3.get_substituted(smap[self.type3])
+        if isinstance(typ, types.PlaceholderForType) and typ in smap:
-            self.type3 = smap[self.type3]
+            typ = smap[typ]
 
-    def check(self) -> CheckResult:
+        if isinstance(typ, types.PlaceholderForType):
-        if isinstance(self.type3, types.PlaceholderForType):
             return RequireTypeSubstitutes()
 
-        if 'BitWiseOr' == self.type_class3 and (self.type3 is types.u8 or self.type3 is types.u32 or self.type3 is types.u64):
+        if 'BitWiseOperation' == self.type_class3 and (typ is types.u8 or typ is types.u32 or typ is types.u64):
             return None
 
-        return Error(f'{self.type3.name} does not implement the {self.type_class3} type class')
+        if 'BasicMathOperation' == self.type_class3 and (
+                typ is types.u8 or typ is types.u32 or typ is types.u64
+                or typ is types.i32 or typ is types.i64
+                or typ is types.f32 or typ is types.f64
+            ):
+            return None
+
+        return Error(f'{typ.name} does not implement the {self.type_class3} type class')
 
     def human_readable(self) -> HumanReadableRet:
         return (
@@ -169,7 +190,7 @@ class MustImplementTypeClassConstraint(ConstraintBase):
         )
 
     def __repr__(self) -> str:
-        return f'MustImplementTypeClassConstraint({repr(self.type_class3)}, {repr(self.type3)})'
+        return f'MustImplementTypeClassConstraint({repr(self.type_class3)}, {repr(self.type3)}, comment={repr(self.comment)})'
 
 class LiteralFitsConstraint(ConstraintBase):
     """
@@ -180,11 +201,13 @@ class LiteralFitsConstraint(ConstraintBase):
     type3: types.Type3OrPlaceholder
     literal: Union[ourlang.ConstantPrimitive, ourlang.ConstantTuple]
 
-    def __init__(self, type3: types.Type3OrPlaceholder, literal: Union[ourlang.ConstantPrimitive, ourlang.ConstantTuple]) -> None:
+    def __init__(self, type3: types.Type3OrPlaceholder, literal: Union[ourlang.ConstantPrimitive, ourlang.ConstantTuple], comment: Optional[str] = None) -> None:
+        super().__init__(comment=comment)
+
         self.type3 = type3
         self.literal = literal
 
-    def check(self) -> CheckResult:
+    def check(self, smap: SubstitutionMap) -> CheckResult:
         int_table: Dict[str, Tuple[int, bool]] = {
             'u8': (1, False),
             'u32': (4, False),
@@ -201,7 +224,10 @@ class LiteralFitsConstraint(ConstraintBase):
 
         def _check(type3: types.Type3OrPlaceholder, literal: Union[ourlang.ConstantPrimitive, ourlang.ConstantTuple]) -> CheckResult:
             if isinstance(type3, types.PlaceholderForType):
-                return RequireTypeSubstitutes()
+                if type3 not in smap:
+                    return RequireTypeSubstitutes()
+
+                type3 = smap[type3]
 
             val = literal.value
 
@@ -249,11 +275,6 @@ class LiteralFitsConstraint(ConstraintBase):
 
         return _check(self.type3, self.literal)
 
-    def substitute_placeholders(self, smap: SubstitutionMap) -> None: # FIXME: Duplicate code
-        if isinstance(self.type3, types.PlaceholderForType) and self.type3 in smap: # FIXME: Check recursive?
-            self.type3.get_substituted(smap[self.type3])
-            self.type3 = smap[self.type3]
-
     def human_readable(self) -> HumanReadableRet:
         return (
             '{literal} : {type3}',
@@ -264,7 +285,7 @@ class LiteralFitsConstraint(ConstraintBase):
         )
 
     def __repr__(self) -> str:
-        return f'LiteralFitsConstraint({repr(self.type3)}, {repr(self.literal)})'
+        return f'LiteralFitsConstraint({repr(self.type3)}, {repr(self.literal)}, comment={repr(self.comment)})'
 
 class CanBeSubscriptedConstraint(ConstraintBase):
     """
@@ -276,42 +297,45 @@ class CanBeSubscriptedConstraint(ConstraintBase):
     index: ourlang.Expression
     index_type3: types.Type3OrPlaceholder
 
-    def __init__(self, type3: types.Type3OrPlaceholder, index: ourlang.Expression) -> None:
+    def __init__(self, type3: types.Type3OrPlaceholder, index: ourlang.Expression, comment: Optional[str] = None) -> None:
+        super().__init__(comment=comment)
+
         self.type3 = type3
         self.index = index
         self.index_type3 = index.type3
 
-    def check(self) -> CheckResult:
+    def check(self, smap: SubstitutionMap) -> CheckResult:
-        if isinstance(self.type3, types.PlaceholderForType):
+        raise NotImplementedError
-            return RequireTypeSubstitutes()
+    #     if isinstance(self.type3, types.PlaceholderForType):
-
+    #         return RequireTypeSubstitutes()
-        if isinstance(self.index_type3, types.PlaceholderForType):
+    #
-            return RequireTypeSubstitutes()
+    #     if isinstance(self.index_type3, types.PlaceholderForType):
-
+    #         return RequireTypeSubstitutes()
-        if not isinstance(self.type3, types.AppliedType3):
+    #
-            return Error(f'Cannot subscript {self.type3:s}')
+    #     if not isinstance(self.type3, types.AppliedType3):
-
+    #         return Error(f'Cannot subscript {self.type3:s}')
-        if self.type3.base is types.tuple:
+    #
-            return None
+    #     if self.type3.base is types.tuple:
-
+    #         return None
-        raise NotImplementedError(self.type3)
+    #
-
+    #     raise NotImplementedError(self.type3)
-    def get_new_placeholder_substitutes(self) -> SubstitutionMap:
+    #
-        if isinstance(self.type3, types.AppliedType3) and self.type3.base is types.tuple and isinstance(self.index_type3, types.PlaceholderForType):
+    # def get_new_placeholder_substitutes(self) -> SubstitutionMap:
-            return {
+    #     if isinstance(self.type3, types.AppliedType3) and self.type3.base is types.tuple and isinstance(self.index_type3, types.PlaceholderForType):
-                self.index_type3: types.u32,
+    #         return {
-            }
+    #             self.index_type3: types.u32,
-
+    #         }
-        return {}
+    #
-
+    #     return {}
-    def substitute_placeholders(self, smap: SubstitutionMap) -> None: # FIXME: Duplicate code
+    #
-        if isinstance(self.type3, types.PlaceholderForType) and self.type3 in smap: # FIXME: Check recursive?
+    # def substitute_placeholders(self, smap: SubstitutionMap) -> None: # FIXME: Duplicate code
-            self.type3.get_substituted(smap[self.type3])
+    #     if isinstance(self.type3, types.PlaceholderForType) and self.type3 in smap: # FIXME: Check recursive?
-            self.type3 = smap[self.type3]
+    #         self.type3.get_substituted(smap[self.type3])
-
+    #         self.type3 = smap[self.type3]
-        if isinstance(self.index_type3, types.PlaceholderForType) and self.index_type3 in smap: # FIXME: Check recursive?
+    #
-            self.index_type3.get_substituted(smap[self.index_type3])
+    #     if isinstance(self.index_type3, types.PlaceholderForType) and self.index_type3 in smap: # FIXME: Check recursive?
-            self.index_type3 = smap[self.index_type3]
+    #         self.index_type3.get_substituted(smap[self.index_type3])
+    #         self.index_type3 = smap[self.index_type3]
 
     def human_readable(self) -> HumanReadableRet:
         return (
@@ -323,4 +347,4 @@ class CanBeSubscriptedConstraint(ConstraintBase):
         )
 
     def __repr__(self) -> str:
-        return f'CanBeSubscriptedConstraint({repr(self.type3)}, {repr(self.index)})'
+        return f'CanBeSubscriptedConstraint({repr(self.type3)}, {repr(self.index)}, comment={repr(self.comment)})'

phasm/type3/constraintsgenerator.py

@@ -33,30 +33,41 @@ def expression(ctx: Context, inp: ourlang.Expression) -> Generator[ConstraintBas
         return
 
     if isinstance(inp, ourlang.VariableReference):
-        yield SameTypeConstraint(inp.variable.type3, inp.type3, f'The type of a variable reference is the same as the type of variable {inp.variable.name}')
+        yield SameTypeConstraint(inp.variable.type3, inp.type3,
+            comment=f'typeOf("{inp.variable.name}") == typeOf({inp.variable.name})')
         return
 
     if isinstance(inp, ourlang.BinaryOp):
-        if '|' == inp.operator:
+        if inp.operator in ('|', '&', '^', ):
             yield from expression(ctx, inp.left)
             yield from expression(ctx, inp.right)
 
-            yield MustImplementTypeClassConstraint('BitWiseOr', inp.left.type3)
+            yield MustImplementTypeClassConstraint('BitWiseOperation', inp.left.type3)
-            yield SameTypeConstraint(inp.right.type3, inp.left.type3, '(|) :: a -> a -> a')
+            yield SameTypeConstraint(inp.left.type3, inp.right.type3, inp.type3,
-            yield SameTypeConstraint(inp.type3, inp.right.type3, '(|) :: a -> a -> a')
+                comment=f'({inp.operator}) :: a -> a -> a')
+            return
+
+        if inp.operator in ('+', '-', '*', '/', ):
+            yield from expression(ctx, inp.left)
+            yield from expression(ctx, inp.right)
+
+            yield MustImplementTypeClassConstraint('BasicMathOperation', inp.left.type3)
+            yield SameTypeConstraint(inp.left.type3, inp.right.type3, inp.type3,
+                comment=f'({inp.operator}) :: a -> a -> a')
             return
 
         raise NotImplementedError(expression, inp)
 
     if isinstance(inp, ourlang.FunctionCall):
-        yield SameTypeConstraint(inp.function.returns_type3, inp.type3, f'The type of a function call to {inp.function.name} is the same as the type that the function returns')
+        yield SameTypeConstraint(inp.function.returns_type3, inp.type3,
+            comment=f'The type of a function call to {inp.function.name} is the same as the type that the function returns')
 
         assert len(inp.arguments) == len(inp.function.posonlyargs) # FIXME: Make this a Constraint
 
         for fun_arg, call_arg in zip(inp.function.posonlyargs, inp.arguments):
             yield from expression(ctx, call_arg)
             yield SameTypeConstraint(fun_arg.type3, call_arg.type3,
-                f'The type of the value passed to argument {fun_arg.name} of function {inp.function.name} should match the type of that argument')
+                comment=f'The type of the value passed to argument {fun_arg.name} of function {inp.function.name} should match the type of that argument')
 
         return
 
@@ -69,7 +80,7 @@ def expression(ctx: Context, inp: ourlang.Expression) -> Generator[ConstraintBas
 
     if isinstance(inp, ourlang.AccessStructMember):
         yield SameTypeConstraint(inp.struct_type3.members[inp.member], inp.type3,
-            f'The type of a struct member reference is the same as the type of struct member {inp.struct_type3.name}.{inp.member}')
+            comment=f'The type of a struct member reference is the same as the type of struct member {inp.struct_type3.name}.{inp.member}')
         return
 
     raise NotImplementedError(expression, inp)
@@ -83,11 +94,13 @@ def function(ctx: Context, inp: ourlang.Function) -> Generator[ConstraintBase, N
 
     yield from expression(ctx, inp.statements[0].value)
 
-    yield SameTypeConstraint(inp.returns_type3, inp.statements[0].value.type3, f'The type of the value returned from function {inp.name} should match its return type')
+    yield SameTypeConstraint(inp.returns_type3, inp.statements[0].value.type3,
+        comment=f'The type of the value returned from function {inp.name} should match its return type')
 
 def module_constant_def(ctx: Context, inp: ourlang.ModuleConstantDef) -> Generator[ConstraintBase, None, None]:
     yield from constant(ctx, inp.constant)
-    yield SameTypeConstraint(inp.type3, inp.constant.type3, f'The type of the value for module constant definition {inp.name} should match the type of that constant')
+    yield SameTypeConstraint(inp.type3, inp.constant.type3,
+        comment=f'The type of the value for module constant definition {inp.name} should match the type of that constant')
 
 def module(ctx: Context, inp: ourlang.Module) -> Generator[ConstraintBase, None, None]:
     for cdef in inp.constant_defs.values():

phasm/type3/entry.py

@@ -24,48 +24,74 @@ def phasm_type3(inp: ourlang.Module, verbose: bool = False) -> None:
     placeholder_substitutes: Dict[PlaceholderForType, Type3] = {}
     placeholder_id_map: Dict[int, str] = {}
 
-    restack_counter = 0
-
     error_list: List[Error] = []
-    while constraint_list:
+    for _ in range(MAX_RESTACK_COUNT):
         if verbose:
             print()
             print_constraint_list(placeholder_id_map, constraint_list, placeholder_substitutes)
 
-        constraint = constraint_list.pop(0)
+        old_constraint_ids = {id(x) for x in constraint_list}
+        old_placeholder_substitutes_len = len(placeholder_substitutes)
 
-        constraint.substitute_placeholders(placeholder_substitutes)
+        new_constraint_list = []
-        placeholder_substitutes.update(constraint.get_new_placeholder_substitutes())
+        for constraint in constraint_list:
+            check_result = constraint.check(placeholder_substitutes)
+            if check_result is None:
+                if verbose:
+                    print_constraint(placeholder_id_map, constraint)
+                    print('-> Constraint checks out')
+                continue
 
-        check_result = constraint.check()
+            if isinstance(check_result, dict):
-        if check_result is None:
+                placeholder_substitutes.update(check_result)
-            if verbose:
-                print('Constraint checks out')
-            continue
 
-        if isinstance(check_result, Error):
+                if verbose:
-            error_list.append(check_result)
+                    print_constraint(placeholder_id_map, constraint)
-            if verbose:
+                    print('-> Constraint checks out, and gave us new information')
-                print('Got an error')
+                continue
-            continue
 
-        if isinstance(check_result, RequireTypeSubstitutes):
+            if isinstance(check_result, Error):
-            # FIXME: How to detect infinite loop? Is that necessary?
+                error_list.append(check_result)
-            restack_counter += 1
+                if verbose:
-            if restack_counter > MAX_RESTACK_COUNT:
+                    print_constraint(placeholder_id_map, constraint)
-                raise Exception('This looks like an infinite loop', constraint_list)
+                    print('-> Got an error')
+                continue
 
-            constraint_list.append(constraint)
+            if isinstance(check_result, RequireTypeSubstitutes):
-            if verbose:
+                new_constraint_list.append(constraint)
-                print('Back on the todo list')
-            continue
 
-        raise NotImplementedError(constraint, check_result)
+                if verbose:
+                    print_constraint(placeholder_id_map, constraint)
+                    print('-> Back on the todo list')
+                continue
+
+            raise NotImplementedError(constraint, check_result)
+
+        if not new_constraint_list:
+            constraint_list = new_constraint_list
+            break
+
+        # Infinite loop detection
+        new_constraint_ids = {id(x) for x in new_constraint_list}
+        new_placeholder_substitutes_len = len(placeholder_substitutes)
+
+        if old_constraint_ids == new_constraint_ids and old_placeholder_substitutes_len == new_placeholder_substitutes_len:
+            raise Exception('Cannot type this program - not enough information')
+
+        constraint_list = new_constraint_list
+
+    if constraint_list:
+        raise Exception(f'Cannot type this program - tried {MAX_RESTACK_COUNT} iterations')
 
     if error_list:
         raise Type3Exception(error_list)
 
-    # TODO: Implement type substitution on the AST
+    # FIXME: This doesn't work with e.g. `:: [a] -> a`, as the placeholder is inside a type
+    for plh, typ in placeholder_substitutes.items():
+        for expr in plh.update_on_substitution:
+            assert expr.type3 is plh
+
+            expr.type3 = typ
 
 def print_constraint(placeholder_id_map: Dict[int, str], constraint: ConstraintBase) -> None:
     txt, fmt = constraint.human_readable()
@@ -88,15 +114,15 @@ def print_constraint(placeholder_id_map: Dict[int, str], constraint: ConstraintB
 
         act_fmt[fmt_key] = fmt_val
 
-    if 'comment' in act_fmt:
+    if constraint.comment is not None:
-        print('- ' + txt.format(**act_fmt).ljust(40) + '; ' + act_fmt['comment'])
+        print('- ' + txt.format(**act_fmt).ljust(40) + '; ' + constraint.comment)
     else:
         print('- ' + txt.format(**act_fmt))
 
 def print_constraint_list(placeholder_id_map: Dict[int, str], constraint_list: List[ConstraintBase], placeholder_substitutes: SubstitutionMap) -> None:
     print('=== v type3 constraint_list v === ')
     for psk, psv in placeholder_substitutes.items():
-        print_constraint(placeholder_id_map, SameTypeConstraint(psk, psv, 'Deduced type'))
+        print_constraint(placeholder_id_map, SameTypeConstraint(psk, psv, comment='Deduced type'))
 
     for constraint in constraint_list:
         print_constraint(placeholder_id_map, constraint)

phasm/type3/types.py

@@ -67,21 +67,6 @@ class PlaceholderForType:
     def __init__(self, update_on_substitution: Iterable[ExpressionProtocol]) -> None:
         self.update_on_substitution = [*update_on_substitution]
 
-    def get_substituted(self, result_type: Type3) -> None:
-        """
-        Informs this Placeholder that it's getting substituted
-
-        This will also clear the update_on_substitution list
-        """
-        for uos in self.update_on_substitution:
-            uos.type3 = result_type
-
-        self.update_on_substitution = []
-
-    @property
-    def name(self) -> str:
-        return f'T{id(self)}'
-
     def __repr__(self) -> str:
         uos = ', '.join(repr(x) for x in self.update_on_substitution)
 

tests/integration/test_lang/test_primitives.py

@@ -151,7 +151,7 @@ def testEntry() -> f64:
     return 10.0 | 3.0
 """
 
-    with pytest.raises(Type3Exception, match='f64 does not implement the BitWiseOr type class'):
+    with pytest.raises(Type3Exception, match='f64 does not implement the BitWiseOperation type class'):
         Suite(code_py).run_code()
 
 @pytest.mark.integration_test
@@ -297,17 +297,33 @@ def testEntry() -> {type_}:
     assert TYPE_MAP[type_] == type(result.returned_value)
 
 @pytest.mark.integration_test
-@pytest.mark.parametrize('type_', COMPLETE_NUMERIC_TYPES)
+@pytest.mark.parametrize('type_', COMPLETE_INT_TYPES)
-def test_division_zero_let_it_crash(type_):
+def test_division_zero_let_it_crash_int(type_):
     code_py = f"""
 @exported
 def testEntry() -> {type_}:
     return 10 / 0
 """
 
+    # WebAssembly dictates that integer division is a partial operator (e.g. unreachable for 0)
+    # https://www.w3.org/TR/wasm-core-1/#-hrefop-idiv-umathrmidiv_u_n-i_1-i_2
     with pytest.raises(Exception):
         Suite(code_py).run_code()
 
+@pytest.mark.integration_test
+@pytest.mark.parametrize('type_', ALL_FLOAT_TYPES)
+def test_division_zero_let_it_crash_float(type_):
+    code_py = f"""
+@exported
+def testEntry() -> {type_}:
+    return 10.0 / 0.0
+"""
+
+    # WebAssembly dictates that float division follows the IEEE rules
+    # https://www.w3.org/TR/wasm-core-1/#-hrefop-fdivmathrmfdiv_n-z_1-z_2
+    result = Suite(code_py).run_code()
+    assert float('+inf') == result.returned_value
+
 @pytest.mark.integration_test
 @pytest.mark.parametrize('type_', ['f32', 'f64'])
 def test_builtins_sqrt(type_):