1. **Implement Parsing for `(union ...)` Type Specifiers:** * Modify `Til.Typer.ExpressionTyper.resolve_type_specifier_node` to recognize and parse S-expressions like `(union integer string)`. * This will involve recursively resolving the inner type specifiers and constructing a raw union type definition. The existing interning and subtyping logic for unions can then be leveraged. * Add tests for type checking expressions annotated with these explicit union types, e.g., `(the (union integer string) some-expression)`. 3. **Implement Parsing for Basic Function Type Specifiers:** * Modify `Til.Typer.ExpressionTyper.resolve_type_specifier_node` to parse function type specifiers, e.g., `(function (Arg1Type Arg2Type ...) ReturnType)`. * Add interning support for function types in `Til.Typer.Interner`. * Implement basic subtyping rules for function types in `Til.Typer.SubtypeChecker` (initially, arity checking; then contravariant arguments, covariant return). 4. **Implement Basic Function Definition (e.g., `def` or `lambda`):** * Define syntax (e.g., `(def my-fn (param1 param2) body-expr)`). * Add parser support for this syntax. * Typer: * For this initial step, infer a basic function type (e.g., based on arity, with `any` for parameter and return types if not annotated). * Add the function name and its inferred type to the environment. 5. **Implement Basic Function Calls:** * Extend `Til.Typer.ExpressionTyper.infer_s_expression_type` for function calls: * When the operator of an S-expression is a symbol, look up its type in the environment. * If it's a function type (from step 4), perform an arity check against the provided arguments. * The inferred type of the call would be the function's (currently basic) return type. 6. **Enhance Function Definitions with Type Annotations:** * Extend the function definition syntax to support type annotations for parameters and return types (e.g., `(def my-fn ((p1 P1Type) (p2 P2Type)) :: ReturnType body-expr)`). * Update the parser for this extended syntax. * Typer: * Use these annotations to construct a more precise function type. * When typing the function body, use the annotated parameter types in the local environment. * Verify that the inferred type of the function body is a subtype of the annotated return type. * Update function call typing (from step 5) to use these precise function types for argument type checking and to determine the call's return type. 7. **Implement Type Inference for Core Map Operation: `(map-get map key)`:** * Define the S-expression syntax `(map-get map-expr key-expr)`. * In `Til.Typer.ExpressionTyper`, implement type inference rules for `map-get` based on the logic outlined in `todo.md`. This includes: * Typing `map-expr` and `key-expr`. * Handling cases where `key-expr`'s type is a literal (allowing lookup in `known_elements`). * Handling cases where `key-expr`'s type is a general type (using `index_signature` and potentially unioning types from `known_elements`). 8. **Improve User-Facing Type Error Messages:** * For common errors like `type_annotation_mismatch` or function call argument mismatches, enhance the error reporting. * Develop a utility to pretty-print type definitions (from their internal map representation or ID) for inclusion in error messages, making them more readable than raw type IDs or structures. * Ensure source locations (file, line, column) are clearly associated with type errors. 9. **Implement Parsing for `(intersection ...)` Type Specifiers:** * Similar to union types, update `Til.Typer.ExpressionTyper.resolve_type_specifier_node` for intersection type S-expressions. * Add interning and subtyping rules for intersection types in `Til.Typer.Interner` and `Til.Typer.SubtypeChecker`. 10. **Implement Simple Type Aliases (e.g., `deftype`):** * Define syntax for non-generic type aliases (e.g., `(deftype PositiveInteger (refinement integer ...))` or `(deftype UserMap (map atom any))`). * Add parser support. * Typer: * Store these alias definitions. * Modify `Til.Typer.ExpressionTyper.resolve_type_specifier_node` to recognize and expand these aliases when they are used in type annotations.