diff --git a/.github/workflows/test-compiler.yml b/.github/workflows/test-compiler.yml
index ea44e80..4a89833 100644
--- a/.github/workflows/test-compiler.yml
+++ b/.github/workflows/test-compiler.yml
@@ -14,21 +14,13 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v5
-    - uses: actions/checkout@v5
-      with:
-        ref: main
-        path: main-src
     - name: Download casac release binary
       run: |
         curl --silent --location --fail \
           --output casac-release \
           "https://github.com/frendsick/casa/releases/latest/download/casac"
         chmod +x casac-release
-    - name: Bootstrap stage0 compiler from main
-      run: |
-        cd main-src
-        ../casac-release -L lib casa.casa -o ../casac-main
     - name: Bootstrap stage1 compiler from branch
-      run: ./casac-main -L lib casa.casa -o casac-stage1
+      run: ./casac-release -L lib casa.casa -o casac-stage1
     - name: Run compiler tests
       run: ./tests/test_compiler.sh ./casac-stage1
diff --git a/.github/workflows/test-examples.yml b/.github/workflows/test-examples.yml
index 22263e0..b9e0d8f 100644
--- a/.github/workflows/test-examples.yml
+++ b/.github/workflows/test-examples.yml
@@ -14,21 +14,13 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v5
-    - uses: actions/checkout@v5
-      with:
-        ref: main
-        path: main-src
     - name: Download casac release binary
       run: |
         curl --silent --location --fail \
           --output casac-release \
           "https://github.com/frendsick/casa/releases/latest/download/casac"
         chmod +x casac-release
-    - name: Bootstrap stage0 compiler from main
-      run: |
-        cd main-src
-        ../casac-release -L lib casa.casa -o ../casac-main
     - name: Bootstrap stage1 compiler from branch
-      run: ./casac-main -L lib casa.casa -o casac-stage1
+      run: ./casac-release -L lib casa.casa -o casac-stage1
     - name: Test example programs
       run: ./tests/test_examples.sh ./casac-stage1
diff --git a/compiler/common.casa b/compiler/common.casa
index 98fed51..5ac8500 100644
--- a/compiler/common.casa
+++ b/compiler/common.casa
@@ -725,6 +725,7 @@ struct CasaTrait {
     name:        str
     type_params: List[str]
     methods:     List[TraitMethod]
+    supertraits: List[TraitBound]
     location:    Location
 }
 
@@ -831,7 +832,8 @@ struct Program {
 # Constants
 # ============================================================================
 "_start" = GLOBAL_SCOPE_LABEL
-"any" = ANY_TYPE
+"?" = TYPE_UNKNOWN
+"<missing>" = TYPE_MISSING
 "_" = MATCH_WILDCARD
 "self" = TRAIT_SELF_TYPE
 8 = WORD_SIZE
@@ -966,7 +968,6 @@ fn is_builtin_type typ:str -> bool {
     "str" typ == ||
     "ptr" typ == ||
     "array" typ == ||
-    "any" typ == ||
 }
 
 # ============================================================================
@@ -1057,7 +1058,7 @@ fn signature_matches sig_a:Signature sig_b:Signature -> bool {
     while index sig_a Signature::parameters.length > do
         index sig_a Signature::parameters.get Parameter::typ = type_a
         index sig_b Signature::parameters.get Parameter::typ = type_b
-        if type_a type_b != ANY_TYPE type_a != && ANY_TYPE type_b != && then
+        if type_a type_b != TYPE_UNKNOWN type_a != && TYPE_UNKNOWN type_b != && then
             type_b extract_generic_base = base_b
             type_a extract_generic_base = base_a
             if base_b.is_some type_a base_b.unwrap_or "" == && ! then
@@ -1073,7 +1074,7 @@ fn signature_matches sig_a:Signature sig_b:Signature -> bool {
     while index sig_a Signature::return_types.length > do
         index sig_a Signature::return_types.get = return_a
         index sig_b Signature::return_types.get = return_b
-        if return_a return_b != ANY_TYPE return_a != && ANY_TYPE return_b != && then
+        if return_a return_b != TYPE_UNKNOWN return_a != && TYPE_UNKNOWN return_b != && then
             return_b extract_generic_base = return_base_b
             return_a extract_generic_base = return_base_a
             if return_base_b.is_some return_base_a.is_some && return_base_b.unwrap return_base_a.unwrap == && then
@@ -1090,8 +1091,8 @@ fn signature_matches sig_a:Signature sig_b:Signature -> bool {
                             param_index params_b.get = param_b
                             if
                             param_a param_b !=
-                            ANY_TYPE param_a != &&
-                            ANY_TYPE param_b != &&
+                            TYPE_UNKNOWN param_a != &&
+                            TYPE_UNKNOWN param_b != &&
                             param_a.length 1 != &&
                             param_b.length 1 != &&
                             then
@@ -1493,7 +1494,6 @@ fn symbol_store_new -> SymbolStore {
     "cstr" builtins.add = builtins
     "ptr" builtins.add = builtins
     "array" builtins.add = builtins
-    "any" builtins.add = builtins
 
     builtins
     Map::new(Map[str CasaTrait])
diff --git a/compiler/syntax.casa b/compiler/syntax.casa
index a283b40..7dc0989 100644
--- a/compiler/syntax.casa
+++ b/compiler/syntax.casa
@@ -192,7 +192,7 @@ fn parse_type cursor:TokenCursor -> str {
     cursor.peek = peek_opt
     if peek_opt.is_none then
         empty_location "Expected type" ErrorKind::UnexpectedToken raise_error
-        "any" return
+        "" return
     fi
     peek_opt.unwrap = peek
 
@@ -285,6 +285,7 @@ fn get_op_type_cast cursor:TokenCursor -> Op {
     close_token Token::location Location::span Span::offset = close_offset
     close_offset open_offset - 1 + = length
     length open_offset open_token Token::location Location::file make_location = loc
+
     loc cast_type OpValue::TypeCast make_op
 }
 
@@ -868,6 +869,37 @@ fn parse_signature cursor:TokenCursor -> Signature {
 # Bounds whose trait is not registered in the store are silently skipped,
 # matching the pre-extraction behavior of both call sites.
 
+fn collect_trait_methods_into
+    seen:Set[str]
+    result:List[TraitMethod]
+    parser:Parser
+    trait_def:CasaTrait
+-> Set[str] {
+    for ctm_method in trait_def CasaTrait::methods.iter do
+        if ctm_method TraitMethod::name seen.has ! then
+            ctm_method TraitMethod::name seen.add = seen
+            ctm_method result.push
+        fi
+    done
+    for ctm_super in trait_def CasaTrait::supertraits.iter do
+        ctm_super TraitBound::name parser.store.traits.get = ctm_super_opt
+        if ctm_super_opt.is_some then
+            ctm_super_opt.unwrap parser result seen collect_trait_methods_into = seen
+        fi
+    done
+    seen
+}
+# Returns all methods (abstract + default) from `trait_def` and its
+# transitive supertraits, deduplicated by name. The trait's own methods
+# come first; supertrait methods follow in declaration order.
+
+fn collect_trait_methods parser:Parser trait_def:CasaTrait -> List[TraitMethod] {
+    List::new(List[TraitMethod]) = result
+    Set::new(Set[str]) = seen
+    trait_def parser result seen collect_trait_methods_into drop
+    result
+}
+
 fn build_hidden_trait_methods
     parser:Parser
     trait_bounds:Map[str TraitBound]
@@ -891,7 +923,7 @@ fn build_hidden_trait_methods
                     1 += bhtm_sub_index
                 done
             fi
-            for bound_method in bound_trait CasaTrait::methods.iter do
+            for bound_method in bound_trait parser collect_trait_methods.iter do
                 # Skip default methods — only abstract methods need hidden fn ptrs
                 if 0 bound_method TraitMethod::default_ops.length == then
                     f"__trait_{bound_type_var}_{bound_method TraitMethod::name}" = hidden_name
@@ -1288,6 +1320,35 @@ fn parse_trait parser:Parser cursor:TokenCursor -> CasaTrait {
         "trait" cursor parse_simple_type_vars = type_params
     fi
 
+    List::new(List[TraitBound]) = supertraits
+    cursor.peek = colon_opt
+    if colon_opt.is_some ":" colon_opt.unwrap Token::value == && then
+        cursor.pop drop
+        true = parse_super_loop
+        while parse_super_loop do
+            TokenKind::Identifier cursor expect_token_kind = super_token
+            super_token Token::value = super_name
+            super_name parser.store.traits.get = super_def_opt
+            if super_def_opt.is_none then
+                super_token Token::location f"Supertrait `{super_name}` is not defined" ErrorKind::UndefinedName raise_error
+            fi
+            super_token cursor parse_bound_type_args = super_args
+            if super_def_opt.is_some then
+                super_def_opt.unwrap CasaTrait::type_params = super_params
+                if super_args.length super_params.length != then
+                    super_token Token::location f"Supertrait `{super_name}` expects {super_params.length} type argument(s), got {super_args.length}" ErrorKind::Syntax raise_error
+                fi
+            fi
+            super_args super_name TraitBound supertraits.push
+            cursor.peek = plus_opt
+            if plus_opt.is_some "+" plus_opt.unwrap Token::value == && then
+                cursor.pop drop
+            else
+                false = parse_super_loop
+            fi
+        done
+    fi
+
     List::new(List[TraitMethod]) = methods
     "{" cursor expect_token_value drop
 
@@ -1329,7 +1390,7 @@ fn parse_trait parser:Parser cursor:TokenCursor -> CasaTrait {
         fi
     done
 
-    name_token Token::location methods type_params name_token Token::value CasaTrait
+    name_token Token::location supertraits methods type_params name_token Token::value CasaTrait
 }
 
 # ============================================================================
diff --git a/compiler/typechecker.casa b/compiler/typechecker.casa
index 75ffe85..209e4a2 100644
--- a/compiler/typechecker.casa
+++ b/compiler/typechecker.casa
@@ -130,19 +130,23 @@ fn make_match_context match_type:str -> MatchContext {
 # ============================================================================
 
 struct TypeChecker {
-    live:                TypedStack
-    parameters:          List[Parameter]
-    return_types:        TypedStack
-    has_return_types:    bool
-    branched_stacks:     List[BranchFrame]
-    current_location:    Location
-    current_op_context:  str
-    current_expect_ctx:  str
-    in_branch_condition: bool
-    store:               SymbolStore
+    live:                       TypedStack
+    parameters:                 List[Parameter]
+    return_types:               TypedStack
+    has_return_types:           bool
+    branched_stacks:            List[BranchFrame]
+    current_location:           Location
+    current_op_context:         str
+    current_expect_ctx:         str
+    in_branch_condition:        bool
+    store:                      SymbolStore
+    param_cap:                  int
+    underflow_reported_this_op: bool
 }
 
 fn make_typechecker store:SymbolStore -> TypeChecker {
+    false # underflow_reported_this_op
+    -1 # param_cap (-1 = unlimited until type_check_ops sets a real cap)
     store # store
     false # in_branch_condition
     "" # current_expect_ctx
@@ -155,6 +159,11 @@ fn make_typechecker store:SymbolStore -> TypeChecker {
     TypedStack::new # live
     TypeChecker
 }
+
+fn within_param_cap tc:TypeChecker -> bool {
+    if -1 tc TypeChecker::param_cap == then true return fi
+    tc TypeChecker::param_cap tc TypeChecker::parameters.length <
+}
 # Raise a TypeMismatch error at the type checker's current location.
 
 fn raise_type_mismatch tc:TypeChecker message:str {
@@ -175,17 +184,39 @@ fn stack_push_origin tc:TypeChecker typ:str origin:Location {
     origin tc TypeChecker::live TypedStack::origins.push
 }
 
+fn report_stack_underflow tc:TypeChecker message:str {
+    if tc TypeChecker::underflow_reported_this_op then return fi
+    tc TypeChecker::current_location message ErrorKind::StackUnderflow add_error
+    true tc TypeChecker::set_underflow_reported_this_op
+}
+
+fn stack_underflow_message tc:TypeChecker -> str {
+    tc TypeChecker::current_expect_ctx = expect_what
+    if "" expect_what == then
+        "Stack underflow: expected a value but stack is empty" return
+    fi
+    f"Stack underflow: expected {expect_what} but stack is empty"
+}
+
 fn stack_peek tc:TypeChecker -> str {
     if 0 tc TypeChecker::live TypedStack::types.length == then
-        ANY_TYPE return
+        if tc within_param_cap then
+            TYPE_UNKNOWN return
+        fi
+        tc stack_underflow_message tc report_stack_underflow
+        TYPE_MISSING return
     fi
     tc TypeChecker::live TypedStack::types.length 1 - tc TypeChecker::live TypedStack::types.get
 }
 
 fn stack_pop tc:TypeChecker -> str {
     if 0 tc TypeChecker::live TypedStack::types.length == then
-        ANY_TYPE make_param tc TypeChecker::parameters.push
-        ANY_TYPE return
+        if tc within_param_cap then
+            TYPE_UNKNOWN make_param tc TypeChecker::parameters.push
+            TYPE_UNKNOWN return
+        fi
+        tc stack_underflow_message tc report_stack_underflow
+        TYPE_MISSING return
     fi
     tc TypeChecker::live TypedStack::origins.pop drop
     tc TypeChecker::live TypedStack::types.pop
@@ -193,8 +224,12 @@ fn stack_pop tc:TypeChecker -> str {
 
 fn expect_type tc:TypeChecker expected:str -> str {
     if 0 tc TypeChecker::live TypedStack::types.length == then
-        expected make_param tc TypeChecker::parameters.push
-        expected return
+        if tc within_param_cap then
+            expected make_param tc TypeChecker::parameters.push
+            expected return
+        fi
+        f"Stack underflow: expected `{expected}` but stack is empty" tc report_stack_underflow
+        TYPE_MISSING return
     fi
     tc TypeChecker::live TypedStack::origins.pop = et_origin
     tc TypeChecker::live TypedStack::types.pop = et_actual
@@ -220,8 +255,10 @@ fn expect_type tc:TypeChecker expected:str -> str {
 
 fn types_match expected:str actual:str -> bool {
     if expected actual == then true return fi
-    if ANY_TYPE expected == then true return fi
-    if ANY_TYPE actual == then true return fi
+    if TYPE_UNKNOWN expected == then true return fi
+    if TYPE_UNKNOWN actual == then true return fi
+    if TYPE_MISSING expected == then true return fi
+    if TYPE_MISSING actual == then true return fi
     # Check fn type matching
     if "fn" expected == then
         if actual is_fn_type then true return fi
@@ -259,10 +296,53 @@ fn types_match expected:str actual:str -> bool {
     false
 }
 
+fn base_type_exists base:str function_opt:Option[Function] -> bool {
+    if base is_builtin_type then true return fi
+    if base DEFAULT_PARSER.store.structs.get.is_some then true return fi
+    if base DEFAULT_PARSER.store.enums.get.is_some then true return fi
+    if function_opt Option::Some(check_fn) is then
+        if base check_fn Function::signature Signature::type_vars.has then true return fi
+    fi
+    false
+}
+
+fn type_exists_recursive typ:str function_opt:Option[Function] -> bool {
+    if typ.length 0 == then false return fi
+
+    if typ is_fn_type then
+        typ extract_fn_signature_str = function_inner_opt
+        if function_inner_opt Option::Some(function_inner) is then
+            for function_token in function_inner split_type_tokens.iter do
+                if "->" function_token != then
+                    if function_opt function_token type_exists_recursive ! then false return fi
+                fi
+            done
+        fi
+        true return
+    fi
+
+    typ extract_generic_base = base_opt
+    if base_opt Option::Some(generic_base) is then
+        generic_base.length = base_length
+        typ.length base_length - 2 - = inner_length
+        typ base_length 1 + inner_length str::substring split_type_tokens = generic_params
+        for generic_param in generic_params.iter do
+            if function_opt generic_param type_exists_recursive ! then false return fi
+        done
+        function_opt generic_base base_type_exists return
+    fi
+
+    function_opt typ base_type_exists
+}
+
+fn validate_type_exists typ:str function_opt:Option[Function] location:Location {
+    if function_opt typ type_exists_recursive then return fi
+    location f"type `{typ}` does not exist" ErrorKind::Syntax raise_error
+}
+
 fn is_type_variable typ:str -> bool {
     # Check if the type is a type variable (single uppercase letter or
     # registered as a type var in a generic enum/struct)
-    if ANY_TYPE typ == then true return fi
     if typ.length 0 == then false return fi
     # Single uppercase letter is a type variable
     if typ.length 1 == then
@@ -309,8 +389,8 @@ fn types_match_params expected:str actual:str -> bool {
         index actual_params.get = actual_param
         if expected_param actual_param != then
             if
-            ANY_TYPE expected_param !=
-            ANY_TYPE actual_param != &&
+            TYPE_UNKNOWN expected_param !=
+            TYPE_UNKNOWN actual_param != &&
             expected_param type_vars.has ! &&
             actual_param type_vars.has ! &&
             expected_param is_type_variable ! &&
@@ -350,8 +430,8 @@ fn unify_generic_params type_a:str type_b:str -> str {
 
 fn unify_type type_a:str type_b:str -> str {
     if type_a type_b == then type_a return fi
-    if ANY_TYPE type_a == then type_b return fi
-    if ANY_TYPE type_b == then type_a return fi
+    if TYPE_UNKNOWN type_a == then type_b return fi
+    if TYPE_UNKNOWN type_b == then type_a return fi
     # Enum type variables unify with concrete types
     if type_a is_enum_type_var then type_b return fi
     if type_b is_enum_type_var then type_a return fi
@@ -448,17 +528,17 @@ fn bind_type_var tc:TypeChecker bindings:Map[str str] type_var:str actual:str ->
     fi
     existing.unwrap = bound
     if
-    ANY_TYPE bound ==
+    TYPE_UNKNOWN bound ==
     bound is_enum_type_var ||
     bound is_type_variable ||
-    ANY_TYPE actual != &&
+    TYPE_UNKNOWN actual != &&
     then
         type_var actual bindings.set return
     fi
     if
     actual bound !=
-    ANY_TYPE actual != &&
-    ANY_TYPE bound != &&
+    TYPE_UNKNOWN actual != &&
+    TYPE_UNKNOWN bound != &&
     actual is_enum_type_var ! &&
     then
         f"Type variable `{type_var}` bound to `{bound}` but got `{actual}`" tc raise_type_mismatch
@@ -474,6 +554,19 @@ fn is_enum_type_var typ:str -> bool {
         false
     fi
 }
+# True when typ has TYPE_UNKNOWN inside any parametric position. Used to
+# detect empty array literals whose element type was never constrained by an
+# annotation, cast, or surrounding use.
+
+fn type_has_unresolved typ:str -> bool {
+    typ extract_generic_params = params_opt
+    if params_opt.is_none then false return fi
+    for param in params_opt.unwrap.iter do
+        if TYPE_UNKNOWN param == then true return fi
+        if param type_has_unresolved then true return fi
+    done
+    false
+}
 
 fn bind_generic_param
     tc:TypeChecker
@@ -519,10 +612,10 @@ fn bind_generic_param
             "Type mismatch" tc raise_type_mismatch
         fi
     fi
-    if base actual == ANY_TYPE actual == || then
+    if base actual == TYPE_UNKNOWN actual == || then
         for expected_param in expected_params.iter do
             if expected_param sig Signature::type_vars.has then
-                ANY_TYPE expected_param bindings tc bind_type_var = bindings
+                TYPE_UNKNOWN expected_param bindings tc bind_type_var = bindings
             fi
         done
         true return
@@ -547,10 +640,10 @@ fn bind_fn_param tc:TypeChecker bindings:Map[str str] expected:Parameter sig:Sig
     if has_type_var ! then false return fi
 
     tc stack_pop = actual
-    if ANY_TYPE actual == then
+    if TYPE_UNKNOWN actual == then
         for type_var2 in type_var_list.iter do
             if fn_sig_str type_var2 str::find 0 <= then
-                ANY_TYPE type_var2 bindings tc bind_type_var = bindings
+                TYPE_UNKNOWN type_var2 bindings tc bind_type_var = bindings
             fi
         done
         true return
@@ -671,38 +764,109 @@ fn check_arithmetic tc:TypeChecker op:Op {
 # ============================================================================
 # Check comparison operations
 # ============================================================================
+# Primitive types whose `==`/`<` etc. are emitted as direct bytecode rather
+# than dispatched through Eq/Ord trait methods. `str` is handled separately
+# because it only supports `==`/`!=` and carries a type annotation.
+
+fn is_primitive_compare_type typ:str -> bool {
+    "int" typ ==
+    "bool" typ == ||
+    "char" typ == ||
+    "cstr" typ == ||
+    "ptr" typ == ||
+}
+
+fn comparison_method_name cmp_value:OpValue -> str {
+    if cmp_value OpValue::Eq is then "eq" return fi
+    if cmp_value OpValue::Ne is then "ne" return fi
+    if cmp_value OpValue::Lt is then "lt" return fi
+    if cmp_value OpValue::Le is then "le" return fi
+    if cmp_value OpValue::Gt is then "gt" return fi
+    "ge"
+}
+
+fn comparison_op_str cmp_value:OpValue -> str {
+    if cmp_value OpValue::Eq is then "==" return fi
+    if cmp_value OpValue::Ne is then "!=" return fi
+    if cmp_value OpValue::Lt is then "<" return fi
+    if cmp_value OpValue::Le is then "<=" return fi
+    if cmp_value OpValue::Gt is then ">" return fi
+    ">="
+}
 
-fn check_comparison tc:TypeChecker op:Op {
+fn check_comparison
+    tc:TypeChecker
+    op:Op
+    ops:List[Op]
+    op_index:int
+    function_opt:Option[Function]
+-> int {
+    op.value = cmp_value
+    cmp_value OpValue::Eq is cmp_value OpValue::Ne is || = is_eq_op
+    if is_eq_op then "Eq" else "Ord" fi = trait_name
+    f"value with trait `{trait_name}`" tc TypeChecker::set_current_expect_ctx
     tc stack_pop = type1
     tc stack_pop = type2
+    # Stack-underflow placeholder on either side: defer to caller-level
+    # inference (lambda param synthesis, generic body deferral). Skip both
+    # the same-type rule and the trait-bound check.
+    if
+    TYPE_UNKNOWN type1 ==
+    TYPE_UNKNOWN type2 == ||
+    TYPE_MISSING type1 == ||
+    TYPE_MISSING type2 == ||
+    then
+        "bool" tc stack_push
+        op_index return
+    fi
     type1 resolve_match_type = base1
     type2 resolve_match_type = base2
     base1 tc.store.enums.get.is_some = is_enum1
     base2 tc.store.enums.get.is_some = is_enum2
+    # Same-type rule applies before any specialization.
+    if type1 type2 != then
+        f"Cannot compare `{type2}` with `{type1}`" tc raise_type_mismatch
+        "bool" tc stack_push
+        op_index return
+    fi
+    # Enums: tag comparison via bytecode; data-carrying variants need annotation.
     if is_enum1 is_enum2 || then
-        if type1 type2 != then
-            f"Cannot compare `{type2}` with `{type1}`" tc raise_type_mismatch
-        fi
-        # Annotate for bytecode: data-carrying enums need heap tag comparison
         if is_enum1 then
             base1 tc.store.enums.get.unwrap = casa_enum
             if casa_enum has_inner_values then
                 base1 op Op::set_type_annotation
             fi
         fi
-    elif "str" type1 == "str" type2 == || then
-        if type1 type2 != then
-            f"Cannot compare `{type2}` with `{type1}`" tc raise_type_mismatch
-        fi
-        if
-        op.value OpValue::Eq is !
-        op.value OpValue::Ne is ! &&
-        then
+        "bool" tc stack_push
+        op_index return
+    fi
+    # str: only ==/!=, annotated for the bytecode emitter.
+    if "str" type1 == then
+        if is_eq_op ! then
             "Type `str` only supports `==` and `!=` comparison" tc raise_type_mismatch
         fi
         "str" op Op::set_type_annotation
+        "bool" tc stack_push
+        op_index return
     fi
-    "bool" tc stack_push
+    # Other primitives: bytecode handles the comparison directly.
+    if type1 is_primitive_compare_type then
+        "bool" tc stack_push
+        op_index return
+    fi
+    # User-defined types must satisfy Eq (or Ord) explicitly.
+    if function_opt trait_name type1 type_satisfies_trait ! then
+        cmp_value comparison_op_str = cmp_str
+        op Op::location f"Type `{type1}` cannot be compared with `{cmp_str}`: does not satisfy trait `{trait_name}`" ErrorKind::MissingTraitMethod add_error
+        "bool" tc stack_push
+        op_index return
+    fi
+    # Lower the operator to the corresponding trait method call.
+    cmp_value comparison_method_name = method_name
+    type2 tc stack_push
+    type1 tc stack_push
+    method_name OpValue::MethodCall op Op::set_value
+    function_opt op_index ops op tc check_method_call
 }
 
 # ============================================================================
@@ -749,25 +913,34 @@ fn check_bitwise tc:TypeChecker op:Op {
 fn check_stack_ops tc:TypeChecker op:Op {
     op.value = stack_value
     if stack_value OpValue::Drop is then
+        "value for `drop`" tc TypeChecker::set_current_expect_ctx
         tc stack_pop drop
     elif stack_value OpValue::Dup is then
+        "value for `dup`" tc TypeChecker::set_current_expect_ctx
         tc stack_pop = typ
         typ tc stack_push
         typ tc stack_push
     elif stack_value OpValue::Swap is then
+        "argument 1 of `swap`" tc TypeChecker::set_current_expect_ctx
         tc stack_pop = type1
+        "argument 2 of `swap`" tc TypeChecker::set_current_expect_ctx
         tc stack_pop = type2
         type1 tc stack_push
         type2 tc stack_push
     elif stack_value OpValue::Over is then
+        "argument 1 of `over`" tc TypeChecker::set_current_expect_ctx
         tc stack_pop = type1
+        "argument 2 of `over`" tc TypeChecker::set_current_expect_ctx
         tc stack_pop = type2
         type2 tc stack_push
         type1 tc stack_push
         type2 tc stack_push
     elif stack_value OpValue::Rot is then
+        "argument 1 of `rot`" tc TypeChecker::set_current_expect_ctx
         tc stack_pop = type1
+        "argument 2 of `rot`" tc TypeChecker::set_current_expect_ctx
         tc stack_pop = type2
+        "argument 3 of `rot`" tc TypeChecker::set_current_expect_ctx
         tc stack_pop = type3
         type2 tc stack_push
         type1 tc stack_push
@@ -778,8 +951,37 @@ fn check_stack_ops tc:TypeChecker op:Op {
 # ============================================================================
 # Check memory operations
 # ============================================================================
+# Returns true if `bound` names `Word` directly or transitively via supertraits.
 
-fn check_memory tc:TypeChecker op:Op {
+fn bound_implies_word bound:TraitBound -> bool {
+    bound TraitBound::name = bound_name
+    if "Word" bound_name == then true return fi
+    bound_name DEFAULT_PARSER.store.traits.get = bound_trait_opt
+    if bound_trait_opt.is_none then false return fi
+    for super_bound in bound_trait_opt.unwrap CasaTrait::supertraits.iter do
+        if super_bound bound_implies_word then true return fi
+    done
+    false
+}
+# Validate that `type_name` satisfies the `Word` marker trait at the given op
+# location. Concrete single-slot types always satisfy `Word` in current Casa.
+# A type variable from the enclosing function satisfies `Word` only when its
+# declared bound is `Word` itself or a trait that extends `Word`. An unbounded
+# type variable is allowed; the concrete type bound at the call site will
+# satisfy `Word` automatically.
+
+fn assert_word_bound tc:TypeChecker op:Op type_name:str function_opt:Option[Function] {
+    if type_name TYPE_UNKNOWN == then return fi
+    if function_opt.is_none then return fi
+    function_opt.unwrap Function::signature = word_sig
+    if type_name word_sig Signature::type_vars.has ! then return fi
+    type_name word_sig Signature::trait_bounds.get = word_bound_opt
+    if word_bound_opt.is_none then return fi
+    if word_bound_opt.unwrap bound_implies_word then return fi
+    op Op::location f"Type variable `{type_name}` does not satisfy `Word` bound; add `[{type_name}: Word]` (or a trait that extends `Word`) to the function's type parameters" ErrorKind::TypeMismatch raise_error
+}
+
+fn check_memory tc:TypeChecker op:Op function_opt:Option[Function] {
     op.value = mem_value
     if
     mem_value OpValue::Load8 is
@@ -796,7 +998,8 @@ fn check_memory tc:TypeChecker op:Op {
     mem_value OpValue::Store64 is ||
     then
         "ptr" tc expect_type drop
-        tc stack_pop drop
+        tc stack_pop = stored_type
+        function_opt stored_type op tc assert_word_bound
     elif mem_value OpValue::HeapAlloc is then
         "int" tc expect_type drop
         "ptr" tc stack_push
@@ -813,7 +1016,7 @@ fn unify_variable_assignment op:Op variable:Variable effective_type:str scope:st
     variable Variable::name = var_name
     if
     "" variable Variable::typ ==
-    ANY_TYPE variable Variable::typ == effective_type ANY_TYPE != && ||
+    TYPE_UNKNOWN variable Variable::typ == effective_type TYPE_UNKNOWN != && ||
     then
         effective_type variable Variable::set_typ
     fi
@@ -840,6 +1043,9 @@ fn check_assignment tc:TypeChecker op:Op function_opt:Option[Function] {
     if has_annotation then
         op Op::type_annotation = effective_type
     fi
+    if has_annotation ! stack_type type_has_unresolved && then
+        op Op::location f"Cannot infer element type of empty array literal assigned to `{var_name}`; add a type annotation (e.g. `= {var_name}:array[int]`) or an explicit cast (e.g. `[] (array[int])`)." ErrorKind::TypeMismatch raise_error
+    fi
 
     # Try local variables first
     if function_opt.is_some then
@@ -884,7 +1090,7 @@ fn simulate_trait_exec tc:TypeChecker function:Function var_name:str {
     trait_bound_opt.unwrap TraitBound::name tc.store.traits.get = trait_def_opt
     if trait_def_opt.is_none then return fi
     trait_def_opt.unwrap = trait_def
-    for trait_method_entry in trait_def CasaTrait::methods.iter do
+    for trait_method_entry in trait_def DEFAULT_PARSER collect_trait_methods.iter do
         if trait_method_name trait_method_entry TraitMethod::name == then
             tc stack_pop drop
             trait_type_var trait_method_entry TraitMethod::signature resolve_trait_sig = resolved_exec_sig
@@ -907,7 +1113,7 @@ fn check_push_var tc:TypeChecker op:Op function_opt:Option[Function] {
                 fi
             fi
         fi
-        ANY_TYPE tc stack_push
+        TYPE_UNKNOWN tc stack_push
         return
     fi
 
@@ -924,7 +1130,7 @@ fn check_push_var tc:TypeChecker op:Op function_opt:Option[Function] {
             if "" local_type != then
                 local_type tc stack_push
             else
-                ANY_TYPE tc stack_push
+                TYPE_UNKNOWN tc stack_push
             fi
             if is_trait_exec then
                 var_name function tc simulate_trait_exec
@@ -940,7 +1146,7 @@ fn check_push_var tc:TypeChecker op:Op function_opt:Option[Function] {
         if "" global_type != then
             global_type tc stack_push
         else
-            ANY_TYPE tc stack_push
+            TYPE_UNKNOWN tc stack_push
         fi
         return
     fi
@@ -1124,7 +1330,7 @@ fn type_satisfies_trait type_name:str trait_name:str function_opt:Option[Functio
             if trait_name bound_opt.unwrap trait_bound_to_str == then true return fi
         fi
     fi
-    for method in trait_def CasaTrait::methods.iter do
+    for method in trait_def DEFAULT_PARSER collect_trait_methods.iter do
         f"{type_name}::{method TraitMethod::name}" = fn_name
         fn_name DEFAULT_PARSER.store.functions.get = fn_opt
         false = via_generic_base
@@ -1165,8 +1371,8 @@ fn type_satisfies_trait type_name:str trait_name:str function_opt:Option[Functio
             param_index resolved Signature::parameters.get Parameter::typ = expected_param
             if
             actual_param expected_param !=
-            ANY_TYPE actual_param != &&
-            ANY_TYPE expected_param != &&
+            TYPE_UNKNOWN actual_param != &&
+            TYPE_UNKNOWN expected_param != &&
             then
                 false return
             fi
@@ -1178,8 +1384,8 @@ fn type_satisfies_trait type_name:str trait_name:str function_opt:Option[Functio
             return_index resolved Signature::return_types.get = expected_return
             if
             actual_return expected_return !=
-            ANY_TYPE actual_return != &&
-            ANY_TYPE expected_return != &&
+            TYPE_UNKNOWN actual_return != &&
+            TYPE_UNKNOWN expected_return != &&
             then
                 false return
             fi
@@ -1420,11 +1626,12 @@ fn inject_trait_fn_ptrs
             fi
         fi
 
+        trait_def DEFAULT_PARSER collect_trait_methods = expanded_methods
         if is_forwarding then
             # Forward hidden fn ptrs from calling function (abstract methods only)
-            trait_def CasaTrait::methods.length 1 - = method_index
+            expanded_methods.length 1 - = method_index
             while 0 method_index >= do
-                method_index trait_def CasaTrait::methods.get = method
+                method_index expanded_methods.get = method
                 if 0 method TraitMethod::default_ops.length == then
                     f"__trait_{concrete}_{method TraitMethod::name}" = hidden_var
                     location hidden_var OpValue::PushVar make_op = push_op
@@ -1443,32 +1650,27 @@ fn inject_trait_fn_ptrs
             fi
             # Inject FN_PUSH for each abstract method (reversed)
             # Skip default methods — they are instantiated on demand
-            trait_def CasaTrait::methods.length 1 - = method_index
+            expanded_methods.length 1 - = method_index
             while 0 method_index >= do
-                method_index trait_def CasaTrait::methods.get = method
-                if 0 method TraitMethod::default_ops.length != then
-                    method_index 1 - = method_index
-                    # Use continue-safe pattern (avoid nested loop break/continue bug)
-                fi
+                method_index expanded_methods.get = method
                 if 0 method TraitMethod::default_ops.length == then
                     f"{concrete}::{method TraitMethod::name}" = fn_name
                     fn_name tc.store.functions.get = global_fn_opt
-                    if global_fn_opt.is_none then
+                    if global_fn_opt.is_some then
+                        global_fn_opt.unwrap = global_fn
+                        if global_fn Function::is_used ! then
+                            true global_fn Function::set_is_used
+                            global_fn global_fn Function::ops resolve_identifiers global_fn Function::set_ops
+                        fi
+                        global_fn ensure_typechecked
+                        location fn_name OpValue::FnPush make_op = push_op
+                        insert_pos push_op ops.insert
+                        1 += insert_pos
+                        1 += inserted
+                        f"fn[{global_fn Function::signature signature_to_str}]" tc stack_push
+                    else
                         location f"Function `{fn_name}` required by trait `{trait_name}` not found" ErrorKind::TypeMismatch raise_error
-                        method_index 1 - = method_index
-                        continue
                     fi
-                    global_fn_opt.unwrap = global_fn
-                    if global_fn Function::is_used ! then
-                        true global_fn Function::set_is_used
-                        global_fn global_fn Function::ops resolve_identifiers global_fn Function::set_ops
-                    fi
-                    global_fn ensure_typechecked
-                    location fn_name OpValue::FnPush make_op = push_op
-                    insert_pos push_op ops.insert
-                    1 += insert_pos
-                    1 += inserted
-                    f"fn[{global_fn Function::signature signature_to_str}]" tc stack_push
                 fi
                 method_index 1 - = method_index
             done
@@ -1504,7 +1706,7 @@ fn check_function_ops
         fi
     elif fn_value OpValue::FnExec is then
         tc stack_peek = fn_ptr_type
-        if ANY_TYPE fn_ptr_type == then "fn" = fn_ptr_type fi
+        if TYPE_UNKNOWN fn_ptr_type == then "fn" = fn_ptr_type fi
         fn_ptr_type tc expect_type drop
         if "fn" fn_ptr_type != then
             fn_ptr_type extract_fn_signature_str = sig_str_opt
@@ -1544,7 +1746,7 @@ fn check_function_ops
 # Check literal push operations
 # ============================================================================
 
-fn check_literals tc:TypeChecker op:Op {
+fn check_literals tc:TypeChecker op:Op function_opt:Option[Function] {
     op.value = literal_value
     if literal_value OpValue::PushInt is then
         "int" tc stack_push
@@ -1554,9 +1756,29 @@ fn check_literals tc:TypeChecker op:Op {
         "bool" tc stack_push
     elif literal_value OpValue::PushChar is then
         "char" tc stack_push
-    elif literal_value OpValue::PushArray is then
-        # Array literals: pop N items of same type
-        "array[any]" tc stack_push
+    elif literal_value OpValue::PushArray(items) is then
+        if 0 items.length == then
+            List::new(List[str]) = empty_params
+            TYPE_UNKNOWN empty_params.push
+            empty_params "array" build_parameterized_type tc stack_push
+        else
+            function_opt items tc run_type_check_ops
+            TYPE_UNKNOWN = elem_type
+            0 = items_idx
+            while items_idx items.length > do
+                tc stack_pop = item_type
+                elem_type item_type unify_type = unified
+                if "" unified == then
+                    op Op::location f"Heterogeneous array literal: cannot unify `{elem_type}` and `{item_type}`" ErrorKind::TypeMismatch raise_error
+                else
+                    unified = elem_type
+                fi
+                1 += items_idx
+            done
+            List::new(List[str]) = item_params
+            elem_type item_params.push
+            item_params "array" build_parameterized_type tc stack_push
+        fi
     elif literal_value OpValue::FstringConcat(count) is then
         0 = index
         while index count > do
@@ -1571,19 +1793,48 @@ fn check_literals tc:TypeChecker op:Op {
 # Check print dispatch
 # ============================================================================
 
-fn check_io tc:TypeChecker op:Op {
-    tc stack_pop = typ
+fn check_io tc:TypeChecker op:Op ops:List[Op] op_index:int function_opt:Option[Function] -> int {
+    "value with trait `Display`" tc TypeChecker::set_current_expect_ctx
+    tc stack_peek = typ
     if "str" typ == then
+        tc stack_pop drop
         OpValue::PrintStr op Op::set_value
-    elif "bool" typ == then
+        op_index return
+    fi
+    if "bool" typ == then
+        tc stack_pop drop
         OpValue::PrintBool op Op::set_value
-    elif "char" typ == then
+        op_index return
+    fi
+    if "char" typ == then
+        tc stack_pop drop
         OpValue::PrintChar op Op::set_value
-    elif "cstr" typ == then
+        op_index return
+    fi
+    if "cstr" typ == then
+        tc stack_pop drop
         OpValue::PrintCstr op Op::set_value
-    else
+        op_index return
+    fi
+    if "int" typ == then
+        tc stack_pop drop
         OpValue::PrintInt op Op::set_value
+        op_index return
     fi
+    if TYPE_MISSING typ == then
+        tc stack_pop drop
+        op_index return
+    fi
+    if function_opt "Display" typ type_satisfies_trait ! then
+        op Op::location f"Type `{typ}` cannot be printed: does not satisfy trait `Display`" ErrorKind::MissingTraitMethod add_error
+        tc stack_pop drop
+        op_index return
+    fi
+    "to_str" OpValue::MethodCall op Op::set_value
+    function_opt op_index ops op tc check_method_call = new_index
+    op Op::location OpValue::Print make_op = print_op
+    new_index print_op ops.insert
+    new_index
 }
 
 # ============================================================================
@@ -1600,7 +1851,7 @@ fn check_typeof tc:TypeChecker op:Op {
 # Check syscalls
 # ============================================================================
 
-fn check_syscalls tc:TypeChecker op:Op {
+fn check_syscalls tc:TypeChecker op:Op function_opt:Option[Function] {
     op.value match
         OpValue::Syscall0 => 0
         OpValue::Syscall1 => 1
@@ -1614,7 +1865,8 @@ fn check_syscalls tc:TypeChecker op:Op {
     "int" tc expect_type drop
     0 = index
     while index arg_count > do
-        tc stack_pop drop
+        tc stack_pop = arg_type
+        function_opt arg_type op tc assert_word_bound
         1 += index
     done
     "int" tc stack_push
@@ -1754,14 +2006,17 @@ fn check_match tc:TypeChecker op:Op function_opt:Option[Function] {
     op.value = match_value
     if match_value OpValue::MatchStart is then
         if 0 tc TypeChecker::live TypedStack::types.length == then
-            true = inferring_signature
+            tc within_param_cap = inferring_signature
             if function_opt.is_some then
-                "None -> None" function_opt.unwrap Function::signature signature_to_str == = inferring_signature
+                if function_opt.unwrap Function::name "lambda__" str::starts_with ! then
+                    false = inferring_signature
+                fi
             else
                 false = inferring_signature
             fi
             if inferring_signature ! then
                 op Op::location "`match` requires a subject value on the stack" ErrorKind::StackUnderflow add_error
+                true tc TypeChecker::set_underflow_reported_this_op
             fi
         fi
         tc stack_pop = match_type
@@ -1941,41 +2196,6 @@ fn check_struct_literal tc:TypeChecker op:Op {
     name tc stack_push
 }
 
-# ============================================================================
-# Find method by name (for any-typed receivers)
-# ============================================================================
-
-fn find_method_by_name method_name:str -> Option[str] {
-    f"::{method_name}" = suffix
-    DEFAULT_PARSER.store.functions.keys = keys
-    "" = found
-    "" = found_with_traits
-    for key in keys.iter do
-        if key suffix str::ends_with then
-            if key "lambda__" str::starts_with ! then
-                key DEFAULT_PARSER.store.functions.get.unwrap = function
-                if 0 function Function::signature Signature::trait_bounds.keys.length == then
-                    if "" found == then
-                        key = found
-                    fi
-                else
-                    if "" found_with_traits == then
-                        key = found_with_traits
-                    fi
-                fi
-            fi
-        fi
-    done
-    # Prefer non-trait-bounded matches
-    if "" found != then
-        found Option::Some
-    elif "" found_with_traits != then
-        found_with_traits Option::Some
-    else
-        Option::None
-    fi
-}
-
 # ============================================================================
 # Instantiate default trait method for a concrete type
 # ============================================================================
@@ -2007,7 +2227,7 @@ fn find_trait_for_method method_name:str -> Option[CasaTrait] {
 }
 
 fn check_abstract_methods_present receiver:str trait_def:CasaTrait -> bool {
-    for cam_method in trait_def CasaTrait::methods.iter do
+    for cam_method in trait_def DEFAULT_PARSER collect_trait_methods.iter do
         if 0 cam_method TraitMethod::default_ops.length == then
             f"{receiver}::{cam_method TraitMethod::name}" DEFAULT_PARSER.store.functions.get = cam_fn_opt
             if cam_fn_opt.is_none then
@@ -2199,7 +2419,7 @@ fn check_method_call
                         1 += constraint_index
                     done
                 fi
-                for trait_method in trait_def CasaTrait::methods.iter do
+                for trait_method in trait_def DEFAULT_PARSER collect_trait_methods.iter do
                     if method_name trait_method TraitMethod::name == then
                         f"__trait_{receiver}_{method_name}" = hidden_var
                         tc stack_pop drop
@@ -2230,17 +2450,6 @@ fn check_method_call
         fi
     fi
 
-    # Try any-typed receiver: search all methods by name
-    if fn_opt.is_none then
-        if ANY_TYPE receiver == then
-            method_name find_method_by_name = any_match_opt
-            if any_match_opt.is_some then
-                any_match_opt.unwrap = fn_name
-                fn_name tc.store.functions.get = fn_opt
-            fi
-        fi
-    fi
-
     # Try instantiating a default trait method
     if fn_opt.is_none then
         receiver method_name function_opt instantiate_default_trait_method = default_inst_opt
@@ -2280,10 +2489,16 @@ fn check_fstring_to_str
     op_index:int
     function_opt:Option[Function]
 -> int {
+    "value with trait `Display`" tc TypeChecker::set_current_expect_ctx
     tc stack_peek = fstring_type
     if "str" fstring_type == then
         op_index return
     fi
+    if TYPE_MISSING fstring_type == then
+        tc stack_pop drop
+        "str" tc stack_push
+        op_index return
+    fi
     if function_opt "Display" fstring_type type_satisfies_trait ! then
         op Op::location f"Type `{fstring_type}` cannot be used in f-string: does not satisfy trait `Display`" ErrorKind::MissingTraitMethod add_error
         tc stack_pop drop
@@ -2320,6 +2535,7 @@ fn run_type_check_ops checker:TypeChecker ops:List[Op] function_opt:Option[Funct
         1 += op_index
         current_op Op::location checker TypeChecker::set_current_location
         "" checker TypeChecker::set_current_expect_ctx
+        false checker TypeChecker::set_underflow_reported_this_op
         current_op.value = op_value
         # Arithmetic
         if
@@ -2342,7 +2558,7 @@ fn run_type_check_ops checker:TypeChecker ops:List[Op] function_opt:Option[Funct
         op_value OpValue::Gt is ||
         op_value OpValue::Ge is ||
         then
-            current_op checker check_comparison
+            function_opt op_index ops current_op checker check_comparison = op_index
             continue
         fi
 
@@ -2393,7 +2609,7 @@ fn run_type_check_ops checker:TypeChecker ops:List[Op] function_opt:Option[Funct
         op_value OpValue::Store64 is ||
         op_value OpValue::HeapAlloc is ||
         then
-            current_op checker check_memory
+            function_opt current_op checker check_memory
             continue
         fi
 
@@ -2460,13 +2676,13 @@ fn run_type_check_ops checker:TypeChecker ops:List[Op] function_opt:Option[Funct
         op_value OpValue::PushArray is ||
         op_value OpValue::FstringConcat is ||
         then
-            current_op checker check_literals
+            function_opt current_op checker check_literals
             continue
         fi
 
         # IO
         if op_value OpValue::Print is then
-            current_op checker check_io
+            function_opt op_index ops current_op checker check_io = op_index
             continue
         fi
 
@@ -2486,7 +2702,7 @@ fn run_type_check_ops checker:TypeChecker ops:List[Op] function_opt:Option[Funct
         op_value OpValue::Syscall5 is ||
         op_value OpValue::Syscall6 is ||
         then
-            current_op checker check_syscalls
+            function_opt current_op checker check_syscalls
             continue
         fi
 
@@ -2548,6 +2764,7 @@ fn run_type_check_ops checker:TypeChecker ops:List[Op] function_opt:Option[Funct
 
         # Type cast
         if op_value OpValue::TypeCast(cast_type) is then
+            current_op Op::location function_opt cast_type validate_type_exists
             checker stack_pop drop
             cast_type checker stack_push
             continue
@@ -2578,6 +2795,14 @@ fn run_type_check_ops checker:TypeChecker ops:List[Op] function_opt:Option[Funct
 
 fn type_check_ops ops:List[Op] function_opt:Option[Function] -> Signature {
     DEFAULT_PARSER.store make_typechecker = checker
+    -1 = budget
+    if function_opt.is_some then
+        function_opt.unwrap = the_function
+        if the_function Function::name "lambda__" str::starts_with ! then
+            the_function Function::signature Signature::parameters.length = budget
+        fi
+    fi
+    budget checker TypeChecker::set_param_cap
     ERRORS.length = errors_before_ops
     function_opt ops checker run_type_check_ops
 
diff --git a/docs/STYLE.md b/docs/STYLE.md
index cf39784..91d3f6b 100644
--- a/docs/STYLE.md
+++ b/docs/STYLE.md
@@ -168,9 +168,6 @@ without a type-name prefix is acceptable.
   # Required: bare Option needs narrowing
   Option::None = empty:Option[int]
 
-  # Required: narrowing any to a concrete type
-  42 (any) = x:int
-
   # MUST NOT: inference works fine, annotation is noise
   42 = x:int
   ```
diff --git a/docs/control-flow.md b/docs/control-flow.md
index b6ce2ad..9f3714b 100644
--- a/docs/control-flow.md
+++ b/docs/control-flow.md
@@ -80,7 +80,7 @@ fi
 # result type: Option[int]
 ```
 
-The same applies to bare `array` and `array[T]`, and to `any` with any concrete type.
+The same applies to bare `array` and `array[T]`.
 
 If there is no `else` branch, the `if`/`elif` branches must not change the stack at all (since the "no match" path leaves the stack unchanged).
 
diff --git a/docs/errors.md b/docs/errors.md
index e057a3a..013f7c4 100644
--- a/docs/errors.md
+++ b/docs/errors.md
@@ -124,6 +124,29 @@ fn outer {
 error[INVALID_SCOPE]: Implementation blocks should be defined in the global scope
 ```
 
+### `STACK_UNDERFLOW`
+
+An operation tried to consume a value (or values) from the stack but the stack was empty.
+
+```casa
+fn foo { print rot }
+```
+
+```
+error[STACK_UNDERFLOW]: Stack underflow: expected value with trait `Display` but stack is empty
+error[STACK_UNDERFLOW]: Stack underflow: expected argument 1 of `rot` but stack is empty
+```
+
+The expectation phrase identifies what the operation needed:
+
+- `value with trait `T`` — operations that dispatch on a trait (e.g. `print`, `==`, `<`)
+- `argument N of `op`` — stack intrinsics that consume more than one value (`swap`, `over`, `rot`); `N` counts from the top of the stack (1 = topmost)
+- `value for `op`` — single-value stack intrinsics (`drop`, `dup`)
+- `parameter N of `name`` — function call missing arguments
+- `value` — generic fallback when no operation-specific context is available
+
+When a slot cannot be filled, downstream operations may show `<missing>` for the absent value. See [Cascade Errors](#cascade-errors).
+
 ### `TYPE_MISMATCH`
 
 A type does not match what was expected.
@@ -137,6 +160,8 @@ fn bad[T] T T -> T T { }
 error[TYPE_MISMATCH]: Type variable `T` bound to `str` but got `int`
 ```
 
+If `got` shows `<missing>`, an earlier error left the slot without a real type — fix the earlier error first. See [Cascade Errors](#cascade-errors).
+
 ### `STACK_MISMATCH`
 
 Branches of a conditional or loop leave the stack in inconsistent states. The error shows each branch's stack signature so you can see which branch diverges.
@@ -157,12 +182,12 @@ error[STACK_MISMATCH]: Branches have incompatible stack effects
    |
 27 |     fi
    |     ^^
-  Note: `if` branch has signature `any -> any int int`
+  Note: `if` branch has signature `? -> ? int int`
   --> examples/multi_error.casa:23:5
    |
 23 |     if dup then
    |     ^^
-  Note: `else` branch has signature `any -> any int`
+  Note: `else` branch has signature `? -> ? int`
   --> examples/multi_error.casa:25:5
    |
 25 |     else
@@ -181,7 +206,7 @@ bad
 ```
 error[SIGNATURE_MISMATCH]: Invalid signature for function `bad`
   Expected: int -> str
-  Inferred: any -> int
+  Inferred: ? -> int
 ```
 
 ### `INVALID_VARIABLE`
@@ -210,6 +235,25 @@ if true then
 error[UNMATCHED_BLOCK]: `if` without matching `fi`
 ```
 
+## Cascade Errors
+
+When the compiler reports an error that consumes a value from the stack — most commonly `STACK_UNDERFLOW` — the affected slot is tagged with the placeholder type `<missing>` so type checking can keep going. If a later operation reads that slot, you may see `<missing>` in its diagnostic:
+
+```casa
+fn two_generics[T] a:T b:T { }
+fn foo {
+    print           # underflow: nothing to print
+    2 two_generics  # this also fails because the underflow tainted the stack
+}
+```
+
+```
+error[STACK_UNDERFLOW]: Stack underflow: expected value with trait `Display` but stack is empty
+error[TYPE_MISMATCH]: Type variable `T` bound to `int` but got `<missing>`
+```
+
+The second error is a *cascade* — its real cause is the underflow above. Fix the upstream error first; the cascade error usually disappears on its own. `<missing>` is distinct from `?` (an unconstrained type that the compiler is still inferring).
+
 ## Multi-Error Collection
 
 The compiler collects as many errors as possible within each compilation phase before stopping. For example, the identifier resolution phase will report all undefined names at once rather than stopping at the first one.
diff --git a/docs/functions-and-lambdas.md b/docs/functions-and-lambdas.md
index fcbc1d2..9dbd5bc 100644
--- a/docs/functions-and-lambdas.md
+++ b/docs/functions-and-lambdas.md
@@ -147,6 +147,18 @@ fn first[T1 T2] a:T1 b:T2 -> T1 { a }
 fn wrap[T] T -> T int { 42 }
 ```
 
+The built-in stack intrinsics use the same generic surface syntax:
+
+```casa
+# drop[T]         T -> None
+# dup[T]          T -> T T
+# swap[T1 T2]     T1 T2 -> T2 T1
+# over[T1 T2]     T1 T2 -> T2 T1 T2
+# rot[T1 T2 T3]   T1 T2 T3 -> T3 T1 T2
+fn keep_top[T1 T2] T1 T2 -> T1 { swap drop }
+42 "kept" keep_top         # "kept" (deeper int dropped, top str kept)
+```
+
 The type checker enforces consistency — if the same type variable appears multiple times in the parameters, all occurrences must bind to the same type:
 
 ```casa
@@ -178,7 +190,7 @@ Multiple type variables are separated by commas. Variables without a `:` have no
 
 Every type variable must appear in at least one parameter (return-only type variables are not allowed).
 
-Type variable names must not collide with built-in types (`int`, `bool`, `char`, `cstr`, `str`, `ptr`, `array`, `any`) or user-defined struct names:
+Type variable names must not collide with built-in types (`int`, `bool`, `char`, `cstr`, `str`, `ptr`, `array`) or user-defined struct names:
 
 ```casa
 fn bad[int] int -> int { }     # ERROR: shadows built-in type
@@ -234,10 +246,9 @@ A variable's type is set on first assignment and cannot change:
 "hi" = x     # ERROR: cannot assign str to int variable
 ```
 
-The `= name:type` form annotates the variable type explicitly. The type checker verifies the stack value is compatible and uses the annotated type for the variable. This is useful for narrowing `any` or bare `Option` to a concrete type:
+The `= name:type` form annotates the variable type explicitly. The type checker verifies the stack value is compatible and uses the annotated type for the variable. This is useful for narrowing a bare `Option` (or other unresolved generic) to a concrete type:
 
 ```casa
-42 (any) = x:int            # narrow any to int
 Option::None = empty:Option[int]    # narrow bare Option to Option[int]
 ```
 
diff --git a/docs/intrinsics.md b/docs/intrinsics.md
index af188cf..eb48e78 100644
--- a/docs/intrinsics.md
+++ b/docs/intrinsics.md
@@ -6,13 +6,16 @@ Intrinsics are operations built into the compiler. They are available in every C
 
 Operations for manipulating the stack directly.
 
-| Intrinsic | Stack Effect | Description |
-|-----------|-------------|-------------|
-| `drop` | `a ->` | Discard top of stack |
-| `dup` | `a -> a a` | Duplicate top of stack |
-| `swap` | `a b -> b a` | Swap top two values |
-| `over` | `a b -> a b a` | Copy second value to top |
-| `rot` | `a b c -> b c a` | Rotate top three values |
+| Intrinsic | Generic signature | Description |
+|-----------|-------------------|-------------|
+| `drop` | `[T] T -> None` | Discard top of stack |
+| `dup` | `[T] T -> T T` | Duplicate top of stack |
+| `swap` | `[T1 T2] T1 T2 -> T2 T1` | Swap top two values |
+| `over` | `[T1 T2] T1 T2 -> T2 T1 T2` | Copy second value to top |
+| `rot` | `[T1 T2 T3] T1 T2 T3 -> T3 T1 T2` | Rotate top three values |
+
+Type variables resolve at the call site, so the same intrinsic works on any value type:
+`42 dup` produces two `int`s on the stack, `"hi" dup` produces two `str`s.
 
 ### Examples
 
@@ -37,13 +40,13 @@ See [`examples/stack_operations.casa`](../examples/stack_operations.casa).
 
 ### `print`
 
-Prints the top of the stack to stdout.
+Prints the top of the stack to stdout. Requires the value's type to implement the `Display` trait.
 
-**Signature:** `print a:any`
+**Signature:** `print[T: Display] a:T`
 
 **Stack effect:** `a -> None`
 
-Integers print as decimal numbers. Booleans print as `true` or `false`. Strings, characters, and C strings print as text.
+The primitives `int`, `bool`, `char`, `str`, and `cstr` already implement `Display` and are emitted through specialized output instructions. Other types must implement `Display` (a `to_str self -> str` method); the compiler lowers `value print` to `value to_str` followed by a string print.
 
 ```casa
 42 print                    # 42
@@ -58,7 +61,7 @@ true print                  # true
 
 Consumes the top of the stack and prints its type name to stdout.
 
-**Signature:** `typeof a:any`
+**Signature:** `[T] T -> str`
 
 **Stack effect:** `a -> None`
 
@@ -81,10 +84,12 @@ Low-level byte-addressed memory access for building data structures. All load/st
 | `load16` | `ptr -> int` | Load 16-bit value from address (zero-extended) |
 | `load32` | `ptr -> int` | Load 32-bit value from address (zero-extended) |
 | `load64` | `ptr -> int` | Load 64-bit value from address |
-| `store8` | `any ptr -> None` | Store 8-bit value to address |
-| `store16` | `any ptr -> None` | Store 16-bit value to address |
-| `store32` | `any ptr -> None` | Store 32-bit value to address |
-| `store64` | `any ptr -> None` | Store 64-bit value to address |
+| `store8` | `[T: Word] T ptr -> None` | Store 8-bit value to address |
+| `store16` | `[T: Word] T ptr -> None` | Store 16-bit value to address |
+| `store32` | `[T: Word] T ptr -> None` | Store 32-bit value to address |
+| `store64` | `[T: Word] T ptr -> None` | Store 64-bit value to address |
+
+The value type must satisfy the [`Word`](traits.md#word) marker trait, which constrains it to a single-slot value. Every primitive, enum variant, struct reference, and array reference satisfies `Word` automatically.
 
 ### Examples
 
@@ -104,17 +109,17 @@ Values are addressed by byte offset. Use pointer arithmetic (`+`) to access diff
 
 ## Syscall Intrinsics
 
-Direct Linux system call access. Each intrinsic pops N+1 values from the stack (the syscall number on top, then arguments in order) and pushes the kernel return value as `int`. The syscall number must be `int`. Arguments have no type constraints.
+Direct Linux system call access. Each intrinsic pops N+1 values from the stack (the syscall number on top, then arguments in order) and pushes the kernel return value as `int`. The syscall number must be `int`. Each argument must satisfy the [`Word`](traits.md#word) marker trait so that exactly one register-sized value lands in the corresponding syscall register.
 
 | Intrinsic | Stack Effect | Description |
 |-----------|-------------|-------------|
 | `syscall0` | `nr -> int` | Syscall with 0 args |
-| `syscall1` | `a1 nr -> int` | Syscall with 1 arg |
-| `syscall2` | `a2 a1 nr -> int` | Syscall with 2 args |
-| `syscall3` | `a3 a2 a1 nr -> int` | Syscall with 3 args |
-| `syscall4` | `a4 a3 a2 a1 nr -> int` | Syscall with 4 args |
-| `syscall5` | `a5 a4 a3 a2 a1 nr -> int` | Syscall with 5 args |
-| `syscall6` | `a6 a5 a4 a3 a2 a1 nr -> int` | Syscall with 6 args |
+| `syscall1` | `[A1: Word] A1 nr -> int` | Syscall with 1 arg |
+| `syscall2` | `[A1: Word A2: Word] A2 A1 nr -> int` | Syscall with 2 args |
+| `syscall3` | `[A1: Word A2: Word A3: Word] A3 A2 A1 nr -> int` | Syscall with 3 args |
+| `syscall4` | `[A1: Word ... A4: Word] A4 A3 A2 A1 nr -> int` | Syscall with 4 args |
+| `syscall5` | `[A1: Word ... A5: Word] A5 A4 A3 A2 A1 nr -> int` | Syscall with 5 args |
+| `syscall6` | `[A1: Word ... A6: Word] A6 A5 A4 A3 A2 A1 nr -> int` | Syscall with 6 args |
 
 ### Register Mapping
 
diff --git a/docs/language-server.md b/docs/language-server.md
index 7c739be..6f823f9 100644
--- a/docs/language-server.md
+++ b/docs/language-server.md
@@ -78,7 +78,7 @@ Hover over a symbol to see type and signature information in a code block.
 | Integer, string, bool, or char literal | Type and value (e.g. `(int) 42`) |
 | Assignment | `= name: type` (with inferred type) |
 | Operator | Name and stack effect (e.g. `+: int int -> int`) |
-| Intrinsic | Name and stack effect (e.g. `drop: any -> None`) |
+| Intrinsic | Name and stack effect (e.g. `drop: [T] T -> None`) |
 
 All operators and intrinsics show their stack effects on hover, including arithmetic, comparison, boolean, bitwise, stack manipulation, memory, syscall, and IO operations.
 
diff --git a/docs/operators.md b/docs/operators.md
index 568aaab..39b65fb 100644
--- a/docs/operators.md
+++ b/docs/operators.md
@@ -83,16 +83,18 @@ buf (ptr) 8 + load64 print  # 42
 
 ## Comparison
 
-All comparison operators consume two values and push a `bool`.
+All comparison operators consume two values of the same type and push a `bool`. Equality operators require the operand type to satisfy the `Eq` trait; ordering operators require `Ord`.
 
 | Operator | Stack Effect | Description |
 |----------|-------------|-------------|
-| `==` | `any any -> bool` | Equal |
-| `!=` | `any any -> bool` | Not equal |
-| `<`  | `any any -> bool` | Less than |
-| `<=` | `any any -> bool` | Less than or equal |
-| `>`  | `any any -> bool` | Greater than |
-| `>=` | `any any -> bool` | Greater than or equal |
+| `==` | `[T: Eq] T T -> bool` | Equal |
+| `!=` | `[T: Eq] T T -> bool` | Not equal |
+| `<`  | `[T: Ord] T T -> bool` | Less than |
+| `<=` | `[T: Ord] T T -> bool` | Less than or equal |
+| `>`  | `[T: Ord] T T -> bool` | Greater than |
+| `>=` | `[T: Ord] T T -> bool` | Greater than or equal |
+
+Built-in primitives (`int`, `bool`, `char`, `cstr`, `ptr`) and enums get direct bytecode comparison. User-defined types must provide `impl T { fn eq ... }` (and `fn lt ...` for ordering); the operator then lowers to the corresponding trait method call. See [traits.md](traits.md) for `Eq` and `Ord`.
 
 ```casa
 1 1 == print    # 1 (true)
@@ -115,9 +117,9 @@ String `==` and `!=` compare by content (byte-by-byte), not by pointer identity.
 
 | Operator | Stack Effect | Description |
 |----------|-------------|-------------|
-| `&&` | `any any -> bool` | Logical AND |
-| `\|\|` | `any any -> bool` | Logical OR |
-| `!`  | `any -> bool` | Logical NOT |
+| `&&` | `bool bool -> bool` | Logical AND |
+| `\|\|` | `bool bool -> bool` | Logical OR |
+| `!`  | `bool -> bool` | Logical NOT |
 
 ```casa
 true true && print    # 1
@@ -149,7 +151,6 @@ The `= name:type` form lets you annotate the type of a variable at assignment ti
 ```casa
 42 = x:int                  # explicit int annotation
 Option::None = empty:Option[int]    # narrow bare Option to Option[int]
-42 (any) = val:int          # narrow any to int
 ```
 
 Variables are created on first assignment. See [Functions and Lambdas -- Variables](functions-and-lambdas.md#variables) for scoping rules.
diff --git a/docs/standard-library.md b/docs/standard-library.md
index 34fd5ec..6e8ae4e 100644
--- a/docs/standard-library.md
+++ b/docs/standard-library.md
@@ -380,6 +380,19 @@ Use `match` with destructuring to handle Result values:
 end
 ```
 
+## Built-in Traits
+
+The standard library declares traits with primitive implementations. See [Traits](traits.md) for details.
+
+| Trait | Required | Defaults | Built-in impls |
+|-------|----------|----------|----------------|
+| `Eq` | `eq self other -> bool` | `ne` | `int`, `bool`, `char`, `str`, `cstr`, `ptr` |
+| `Ord` | `lt self other -> bool` | `le`, `gt`, `ge` | `int`, `char` |
+| `Display: Word` | `to_str self -> str` (extends `Word`) | -- | `int`, `bool`, `char`, `str`, `cstr`, `ptr`, `array[T]`, `List[T]`, `Option[T]`, `Result[T E]` |
+| `Word` | (marker) | -- | every single-slot type |
+| `Hashable: Eq + Word` | `hash self -> int` (extends `Eq`, `Word`) | -- | `int`, `str`, payload-free enums (auto-derived) |
+| `Iterable[T]` | `next self -> Option[T]` | `collect`, `map`, `filter`, `fold`, `count`, `any`, `all`, `find` | `Iter[T]` |
+
 ## See Also
 
 - [Collections](collections.md) -- List, Map, Set, and StringBuilder
diff --git a/docs/traits.md b/docs/traits.md
index 7bf6e06..5dd3454 100644
--- a/docs/traits.md
+++ b/docs/traits.md
@@ -160,29 +160,73 @@ Map::new (Map[str int]) = m
 
 The compiler sees that `Map::new` requires `[K: Hashable, V]`, determines `K=str` from the type cast `(Map[str int])`, verifies that `str` satisfies `Hashable`, and injects `&str::hash` and `&str::eq` behind the scenes.
 
+## Built-in Trait: `Eq`
+
+Equality comparison. The required method is `eq`; the trait provides a default `ne` implemented as `!eq`.
+
+```casa
+trait Eq {
+    fn eq self:self other:self -> bool
+    fn ne self:self other:self -> bool { other self.eq ! }
+}
+```
+
+Built-in implementations: `int`, `bool`, `char`, `str`, `cstr`, `ptr`.
+
+A type satisfies `Eq` by providing `Type::eq self:Type other:Type -> bool`. The `ne` default is auto-instantiated for any satisfying type, so `x.ne y` works without writing it.
+
+The `==` and `!=` operators are bounded by `Eq`. Built-in primitives and enums get direct bytecode comparison, but a user-defined struct used with `==` must provide `impl T { fn eq ... }`; the operator then lowers to `T::eq`. Comparing values whose type does not satisfy `Eq` is a compile-time error.
+
+## Built-in Trait: `Ord`
+
+Total ordering. The required method is `lt`; the defaults `le`, `gt`, and `ge` are derived from it.
+
+```casa
+trait Ord {
+    fn lt self:self other:self -> bool
+    fn le self:self other:self -> bool { self other.lt ! }
+    fn gt self:self other:self -> bool { self other.lt }
+    fn ge self:self other:self -> bool { other self.lt ! }
+}
+```
+
+Built-in implementations: `int`, `char`. Lexicographic ordering for `str` is intentionally out of scope.
+
+The `<`, `<=`, `>`, and `>=` operators are bounded by `Ord`. Built-in primitives (excluding `str`) and enums use direct bytecode ordering; user-defined types must provide `impl T { fn lt ... }` and the operator lowers to the corresponding trait method (`lt`, `le`, `gt`, `ge`). A type with `impl Eq` but no `impl Ord` is rejected at compile time when used with an ordering operator.
+
+## Built-in Trait: `Word`
+
+Marker trait for register-sized values that fit in one stack slot. It declares no methods:
+
+```casa
+trait Word { }
+```
+
+It is used as a bound on builtins that require single-slot operands (for example, syscall and `store*` arguments). Primitive types, enums, struct refs, and array refs satisfy `Word`; multi-slot value types do not.
+
+`Hashable` and `Display` both extend `Word` as supertraits, so any type that satisfies one of them automatically satisfies `Word`.
+
 ## Built-in Trait: `Hashable`
 
-The standard library defines the `Hashable` trait and provides implementations for `str` and `int`:
+The standard library defines the `Hashable` trait as an extension of `Eq` and `Word`. Any `Hashable` type therefore also satisfies both `Eq` and `Word` (see [Supertraits](#supertraits)). The trait declares only `hash`; equality is reused from `Eq`:
 
 ```casa
-trait Hashable {
+trait Hashable: Eq + Word {
     fn hash self:self -> int
-    fn eq self:self other:self -> bool
 }
 ```
 
 Built-in implementations:
 - `str::hash` uses the djb2 hash algorithm (via `str_hash`)
-- `str::eq` compares strings by content
 - `int::hash` returns the absolute value (via `int_hash`)
-- `int::eq` compares integers with `==`
+- `Eq::eq` for `str` and `int` is provided by their respective `impl` blocks
 
 ## Built-in Trait: `Display`
 
-The standard library defines a `Display` trait used by f-string interpolation to convert values to strings:
+The standard library defines a `Display` trait used by f-string interpolation to convert values to strings. `Display` extends `Word`, so any displayable type also satisfies `Word`:
 
 ```casa
-trait Display {
+trait Display: Word {
     fn to_str self:self -> str
 }
 ```
@@ -204,6 +248,28 @@ impl Point {
 f"origin = {origin}\n" print    # origin = Point(1, 2)
 ```
 
+## Supertraits
+
+A trait can require its implementors to also satisfy one or more *supertraits*. Declare supertraits with `:` after the trait name (and optional type parameters), separating multiple supertraits with `+`:
+
+```casa
+trait Eq {
+    fn eq self:self other:self -> bool
+}
+
+trait Word { }
+
+trait Hashable: Eq + Word {
+    fn hash self:self -> int
+}
+```
+
+Multiple supertraits are listed with `+`. A type satisfies `Hashable` only if it satisfies every supertrait (here `Eq` and `Word`) in addition to providing `Hashable`'s own required methods. Concretely, the type's `impl` block must contain `eq` (from `Eq`) and `hash` (from `Hashable`); `Word` is a marker with no required methods, so its satisfaction is automatic.
+
+Trait-bounded code may call methods declared by any supertrait directly. For example, inside a function bounded by `K: Hashable`, both `K::hash` and `K::eq` resolve correctly.
+
+Supertraits are checked at the trait's declaration site: each supertrait must already be defined.
+
 ## Default Methods
 
 Traits can provide default method implementations. A default method has a body in the trait definition and is automatically available to any type that satisfies the trait (i.e. implements the required methods). Default methods can call the required methods using `self`.
diff --git a/docs/types-and-literals.md b/docs/types-and-literals.md
index 81e6485..d64c4ff 100644
--- a/docs/types-and-literals.md
+++ b/docs/types-and-literals.md
@@ -201,10 +201,17 @@ All items must have the same type. Heterogeneous arrays are compile-time errors:
 [1, "hello"]        # TYPE_MISMATCH error
 ```
 
-An empty array has type `array[any]`:
+An empty array literal has an unresolved element type. The compiler infers it from the first constraining use — an explicit cast or a typed binding:
 
 ```casa
-[]                  # type: array[any]
+[] (array[int])               # explicit cast resolves element type
+[] = xs:array[str]            # type annotation on the binding resolves it
+```
+
+If the inference frame closes without resolution, the compiler emits a `TYPE_MISMATCH` error:
+
+```casa
+[] = xs xs drop               # error: cannot infer element type of empty array
 ```
 
 Arrays can be nested. The element type is inferred recursively:
@@ -226,7 +233,7 @@ Function type representing a lambda or function reference. The signature inside
 ```casa
 { 2 * }           # type: fn[int -> int]
 { 1 + }           # type: fn[int -> int]
-{ drop "hi" }     # type: fn[any -> str]
+{ drop "hi" }     # type: fn[T -> str]
 ```
 
 Call a function value with `exec`:
@@ -308,17 +315,17 @@ Result type representing either a success value (`Result::Ok`) or an error value
 enum Result[T E] { Error(E) Ok(T) }
 ```
 
-`Result::Ok` wraps the top-of-stack value into a result. The resulting type is `Result[T any]` where `T` is the type of the wrapped value.
+`Result::Ok` wraps the top-of-stack value into a result. The resulting type is `Result[T E]` where `T` is the type of the wrapped value and `E` remains an unbound type variable until constrained by a use site or annotation.
 
-**Stack effect:** `T -> Result[T any]`
+**Stack effect:** `T -> Result[T E]`
 
-`Result::Error` wraps the top-of-stack value into an error result. The resulting type is `Result[any E]` where `E` is the type of the error value.
+`Result::Error` wraps the top-of-stack value into an error result. The resulting type is `Result[T E]` where `E` is the type of the error value and `T` remains unbound.
 
-**Stack effect:** `E -> Result[any E]`
+**Stack effect:** `E -> Result[T E]`
 
 ```casa
-42 Result::Ok            # type: Result[int any]
-"not found" Result::Error # type: Result[any str]
+42 Result::Ok            # type: Result[int E]
+"not found" Result::Error # type: Result[T str]
 ```
 
 At runtime, a result is heap-allocated as 16 bytes: `[tag, value]` where each field is 8 bytes. The tag is `1` for `Ok` and `0` for `Error`.
@@ -326,8 +333,8 @@ At runtime, a result is heap-allocated as 16 bytes: `[tag, value]` where each fi
 Results stored in variables retain their type:
 
 ```casa
-42 Result::Ok = x                    # x has type Result[int any]
-"not found" Result::Error = y        # y has type Result[any str]
+42 Result::Ok = x                    # x has type Result[int E]
+"not found" Result::Error = y        # y has type Result[T str]
 ```
 
 Type annotations can narrow the type to specify both type parameters:
@@ -340,7 +347,7 @@ A bare `Result` type matches any `Result[T E]` in function signatures, similar t
 
 ```casa
 fn check res:Result -> bool { true }
-42 Result::Ok check    # works: Result[int any] matches bare Result
+42 Result::Ok check    # works: Result[int E] matches bare Result
 ```
 
 `Result::Ok` and `Result::Error` can appear in different branches of a conditional. The type checker unifies them to the more specific `Result[T E]`:
@@ -406,16 +413,6 @@ fn hash_key[K: Hashable] key:K -> int {
 
 Type variables are purely compile-time, including trait bounds. See [Functions and Lambdas — Generic Functions](functions-and-lambdas.md#generic-functions) and [Traits](traits.md) for details.
 
-## The `any` Type
-
-`any` is a special wildcard type that matches any other type. It is used as an escape hatch when the type system cannot determine a precise type.
-
-```casa
-32 alloc = buffer
-42 buffer (ptr) store64
-buffer (ptr) load64    # type: int
-```
-
 ## Type Casting
 
 The `(TypeName)` syntax casts the top of the stack to the given type. This is a compile-time annotation only — no runtime check is performed.
@@ -426,7 +423,17 @@ The `(TypeName)` syntax casts the top of the stack to the given type. This is a
 buffer (ptr) load64 (int)    # cast int -> int (no-op here, but useful for generic data)
 ```
 
-This is useful when working with generic data structures that return `any`.
+## Printing Values
+
+`print` requires the value's type to implement the [`Display` trait](traits.md). The primitives `int`, `bool`, `char`, `str`, and `cstr` are dispatched directly to specialized output instructions; user types must provide a `to_str self -> str` method, which the compiler invokes before printing the resulting string.
+
+```casa
+struct Point { x: int y: int }
+impl Point {
+    fn to_str self:Point -> str { f"({self.x}, {self.y})" }
+}
+1 2 Point print    # (1, 2)
+```
 
 ## Comments
 
diff --git a/examples/dynamic_list.casa b/examples/dynamic_list.casa
index e1de54f..846a98f 100644
--- a/examples/dynamic_list.casa
+++ b/examples/dynamic_list.casa
@@ -14,7 +14,7 @@ impl List {
     fn print_items self:List {
         0 = i
         while i self.length > do
-            i self.get print "\n" print
+            i self.get (int) print "\n" print
             1 += i
         done
     }
diff --git a/examples/enum.casa b/examples/enum.casa
index 3d05c72..abc277f 100644
--- a/examples/enum.casa
+++ b/examples/enum.casa
@@ -2,6 +2,7 @@
 #
 # Variants are accessed with EnumName::VariantName syntax.
 # Match provides exhaustive pattern matching.
+import "std"
 
 enum Color {
     Red
@@ -9,6 +10,17 @@ enum Color {
     Blue
 }
 
+# `print` requires Display; provide `to_str` so we can render variants.
+
+impl Color {
+    fn to_str c:Color -> str {
+        c match
+            Color::Red => "0"
+            Color::Green => "1"
+            Color::Blue => "2"
+        end
+    }
+}
 # Variant constructors push an enum value onto the stack
 Color::Green = color
 # Print outputs the ordinal (0-based)
diff --git a/examples/generics.casa b/examples/generics.casa
index 96d555f..acc7e46 100644
--- a/examples/generics.casa
+++ b/examples/generics.casa
@@ -22,6 +22,13 @@ fn second[T1 T2] a:T1 b:T2 -> T2 { b }
 
 42 "hello" first print "\n" print # hello
 42 "hello" second print "\n" print # 42
+# stack-shaped polymorphic helper: drop the deeper arg, keep the topmost
+# (T1 is the topmost / first RPN arg per the stack convention)
+
+fn keep_top[T1 T2] T1 T2 -> T1 { swap drop }
+
+42 "kept" keep_top print "\n" print # kept
+"discarded" 99 keep_top print "\n" print # 99
 # mixing generic and concrete types
 
 fn tag[T] T -> T str { "tagged" }
diff --git a/examples/outputs/generics.out b/examples/outputs/generics.out
index 6beacca..72fcf72 100644
--- a/examples/outputs/generics.out
+++ b/examples/outputs/generics.out
@@ -4,6 +4,8 @@ hello
 2
 hello
 42
+kept
+99
 tagged
 99
 20
diff --git a/examples/parser.casa b/examples/parser.casa
index d4d9331..e07d688 100644
--- a/examples/parser.casa
+++ b/examples/parser.casa
@@ -12,8 +12,8 @@ cursor.advance drop
 cursor.peek.unwrap print "\n" print
 # take_while: collect matching characters
 "abc123" Cursor::new = tw_cursor
-{ .is_alpha } tw_cursor.take_while = letters
-{ .is_digit } tw_cursor.take_while = digits
+&char::is_alpha tw_cursor.take_while = letters
+&char::is_digit tw_cursor.take_while = digits
 "letters: " print letters print "\n" print
 "digits: " print digits print "\n" print
 # save and restore for backtracking
@@ -22,7 +22,7 @@ sr_cursor.save = saved_pos
 &is_ident_char sr_cursor.take_while = full_token
 "full: " print full_token print "\n" print
 saved_pos sr_cursor.restore
-{ .is_alpha } sr_cursor.take_while = alpha_part
+&char::is_alpha sr_cursor.take_while = alpha_part
 "alpha only: " print alpha_part print "\n" print
 # skip_whitespace
 "   hello" Cursor::new = ws_cursor
diff --git a/examples/result.casa b/examples/result.casa
index 6d27271..55bbed4 100644
--- a/examples/result.casa
+++ b/examples/result.casa
@@ -40,7 +40,7 @@ if zero_div.is_error then
     zero_div.unwrap_error print "\n" print
 fi
 # Match on result
-5 Result::Ok match
+5 Result::Ok(Result[int str]) match
     Result::Ok(value) => value print "\n" print
     Result::Error(err) => err print "\n" print
 end
diff --git a/examples/type_annotations.casa b/examples/type_annotations.casa
index 8462e9c..0b48755 100644
--- a/examples/type_annotations.casa
+++ b/examples/type_annotations.casa
@@ -1,7 +1,7 @@
 # Type annotations on variable assignments
 #
 # The = name:type syntax allows explicit type annotation when assigning variables.
-# This is useful for narrowing 'any' or bare 'option' types to concrete types.
+# This is useful for narrowing inferred or bare 'option' types to concrete types.
 import "std"
 
 # Basic type annotations
diff --git a/examples/vec.casa b/examples/vec.casa
index 49b4e76..1c8ab56 100644
--- a/examples/vec.casa
+++ b/examples/vec.casa
@@ -6,7 +6,7 @@ import "std"
 
 # Create empty list and push elements
 "=== List::new and push ===" print "\n" print
-List::new = v
+List::new(List[int]) = v
 10 v.push
 20 v.push
 30 v.push
diff --git a/lib/parser.casa b/lib/parser.casa
index c45e3d2..a1f2176 100644
--- a/lib/parser.casa
+++ b/lib/parser.casa
@@ -162,7 +162,7 @@ fn is_ident_char character:char -> bool {
 # ---------------------------------------------------------------------------
 
 fn skip_whitespace cursor:Cursor {
-    { .is_space } cursor.skip_while
+    &char::is_space cursor.skip_while
 }
 
 fn parse_int cursor:Cursor -> Result[int ParseError] {
@@ -174,7 +174,7 @@ fn parse_int cursor:Cursor -> Result[int ParseError] {
             cursor.advance drop
         fi
     fi
-    { .is_digit } cursor.take_while = digits
+    &char::is_digit cursor.take_while = digits
     if digits.length 0 == then
         start cursor.restore
         start "expected integer" ParseError Result::Error
diff --git a/lib/std.casa b/lib/std.casa
index dc6aa75..8deec74 100644
--- a/lib/std.casa
+++ b/lib/std.casa
@@ -141,6 +141,8 @@ impl bool {
     fn to_str b:bool -> str {
         if b then "true" else "false" fi
     }
+
+    fn eq self:bool other:bool -> bool { self other == }
 }
 
 impl str {
@@ -353,6 +355,25 @@ impl str {
 }
 
 impl cstr {
+    fn eq self:cstr other:cstr -> bool {
+        true = result
+        true = scanning
+        0 = scan_index
+        while scanning do
+            self (ptr) scan_index + load8 = byte_a
+            other (ptr) scan_index + load8 = byte_b
+            if byte_a byte_b != then
+                false = result
+                false = scanning
+            elif 0 byte_a == then
+                false = scanning
+            else
+                1 += scan_index
+            fi
+        done
+        result
+    }
+
     fn to_str s:cstr -> str {
         # Find length by scanning for null byte
         0 = source_length
@@ -516,10 +537,15 @@ impl char {
     fn is_space c:char -> bool {
         c ' ' == c '\t' == || c '\n' == || c '\r' == ||
     }
+
+    fn eq self:char other:char -> bool { self other == }
+    fn lt self:char other:char -> bool { other self < }
 }
 
 impl ptr {
     fn to_str p:ptr -> str { p (int).to_str }
+
+    fn eq self:ptr other:ptr -> bool { self other == }
 }
 
 # ---------------------------------------------------------------------------
@@ -590,13 +616,37 @@ impl Result {
 # Traits
 # ---------------------------------------------------------------------------
 
-trait Hashable {
-    fn hash self:self -> int
-
+trait Eq {
     fn eq self:self other:self -> bool
+
+    fn ne self:self other:self -> bool {
+        other self.eq !
+    }
+}
+
+trait Ord {
+    fn lt self:self other:self -> bool
+
+    fn le self:self other:self -> bool {
+        self other.lt !
+    }
+
+    fn gt self:self other:self -> bool {
+        self other.lt
+    }
+
+    fn ge self:self other:self -> bool {
+        other self.lt !
+    }
+}
+
+trait Word { }
+
+trait Hashable: Eq + Word {
+    fn hash self:self -> int
 }
 
-trait Display {
+trait Display: Word {
     fn to_str self:self -> str
 }
 
@@ -734,6 +784,7 @@ impl str {
 impl int {
     fn hash self:int -> int { self int_hash }
     fn eq self:int other:int -> bool { self other == }
+    fn lt self:int other:int -> bool { other self < }
 }
 
 # ---------------------------------------------------------------------------
diff --git a/lsp.casa b/lsp.casa
index 969bb71..685ff24 100644
--- a/lsp.casa
+++ b/lsp.casa
@@ -2114,27 +2114,27 @@ fn op_value_stack_effect op_value:OpValue -> Option[str] {
         OpValue::BitXor => "^: int int -> int" Option::Some
         OpValue::BitNot => "~: int -> int" Option::Some
         OpValue::Not => "!: bool -> bool" Option::Some
-        OpValue::Eq => "==: any any -> bool" Option::Some
-        OpValue::Ne => "!=: any any -> bool" Option::Some
-        OpValue::Lt => "<: any any -> bool" Option::Some
-        OpValue::Le => "<=: any any -> bool" Option::Some
-        OpValue::Gt => ">: any any -> bool" Option::Some
-        OpValue::Ge => ">=: any any -> bool" Option::Some
+        OpValue::Eq => "==: [T: Eq] T T -> bool" Option::Some
+        OpValue::Ne => "!=: [T: Eq] T T -> bool" Option::Some
+        OpValue::Lt => "<: [T: Ord] T T -> bool" Option::Some
+        OpValue::Le => "<=: [T: Ord] T T -> bool" Option::Some
+        OpValue::Gt => ">: [T: Ord] T T -> bool" Option::Some
+        OpValue::Ge => ">=: [T: Ord] T T -> bool" Option::Some
         OpValue::And => "&&: bool bool -> bool" Option::Some
         OpValue::Or => "||: bool bool -> bool" Option::Some
-        OpValue::Drop => "drop: any -> None" Option::Some
-        OpValue::Dup => "dup: any -> any any" Option::Some
-        OpValue::Swap => "swap: any any -> any any" Option::Some
-        OpValue::Over => "over: any any -> any any any" Option::Some
-        OpValue::Rot => "rot: any any any -> any any any" Option::Some
-        OpValue::Print => "print: any -> None" Option::Some
-        OpValue::PrintInt => "print: any -> None" Option::Some
-        OpValue::PrintStr => "print: any -> None" Option::Some
-        OpValue::PrintBool => "print: any -> None" Option::Some
-        OpValue::PrintChar => "print: any -> None" Option::Some
-        OpValue::PrintCstr => "print: any -> None" Option::Some
+        OpValue::Drop => "drop[T]: T -> None" Option::Some
+        OpValue::Dup => "dup[T]: T -> T T" Option::Some
+        OpValue::Swap => "swap[T1 T2]: T1 T2 -> T2 T1" Option::Some
+        OpValue::Over => "over[T1 T2]: T1 T2 -> T2 T1 T2" Option::Some
+        OpValue::Rot => "rot[T1 T2 T3]: T1 T2 T3 -> T3 T1 T2" Option::Some
+        OpValue::Print => "print: [T: Display] T -> None" Option::Some
+        OpValue::PrintInt => "print: [T: Display] T -> None" Option::Some
+        OpValue::PrintStr => "print: [T: Display] T -> None" Option::Some
+        OpValue::PrintBool => "print: [T: Display] T -> None" Option::Some
+        OpValue::PrintChar => "print: [T: Display] T -> None" Option::Some
+        OpValue::PrintCstr => "print: [T: Display] T -> None" Option::Some
         OpValue::FnExec => "exec: fn[sig] -> ..." Option::Some
-        OpValue::Typeof => "typeof: any -> str" Option::Some
+        OpValue::Typeof => "typeof: [T] T -> str" Option::Some
         OpValue::AssignDec(_) => "-=: int -> None" Option::Some
         OpValue::AssignInc(_) => "+=: int -> None" Option::Some
         OpValue::HeapAlloc => "alloc: int -> ptr" Option::Some
@@ -2142,17 +2142,17 @@ fn op_value_stack_effect op_value:OpValue -> Option[str] {
         OpValue::Load16 => "load16: ptr -> int" Option::Some
         OpValue::Load32 => "load32: ptr -> int" Option::Some
         OpValue::Load64 => "load64: ptr -> int" Option::Some
-        OpValue::Store8 => "store8: any ptr -> None" Option::Some
-        OpValue::Store16 => "store16: any ptr -> None" Option::Some
-        OpValue::Store32 => "store32: any ptr -> None" Option::Some
-        OpValue::Store64 => "store64: any ptr -> None" Option::Some
+        OpValue::Store8 => "store8[T: Word]: T ptr -> None" Option::Some
+        OpValue::Store16 => "store16[T: Word]: T ptr -> None" Option::Some
+        OpValue::Store32 => "store32[T: Word]: T ptr -> None" Option::Some
+        OpValue::Store64 => "store64[T: Word]: T ptr -> None" Option::Some
         OpValue::Syscall0 => "syscall0: int -> int" Option::Some
-        OpValue::Syscall1 => "syscall1: any int -> int" Option::Some
-        OpValue::Syscall2 => "syscall2: any any int -> int" Option::Some
-        OpValue::Syscall3 => "syscall3: any any any int -> int" Option::Some
-        OpValue::Syscall4 => "syscall4: any any any any int -> int" Option::Some
-        OpValue::Syscall5 => "syscall5: any any any any any int -> int" Option::Some
-        OpValue::Syscall6 => "syscall6: any any any any any any int -> int" Option::Some
+        OpValue::Syscall1 => "syscall1[A1: Word]: A1 int -> int" Option::Some
+        OpValue::Syscall2 => "syscall2[A1: Word A2: Word]: A1 A2 int -> int" Option::Some
+        OpValue::Syscall3 => "syscall3[A1: Word A2: Word A3: Word]: A1 A2 A3 int -> int" Option::Some
+        OpValue::Syscall4 => "syscall4[A1: Word A2: Word A3: Word A4: Word]: A1 A2 A3 A4 int -> int" Option::Some
+        OpValue::Syscall5 => "syscall5[A1: Word A2: Word A3: Word A4: Word A5: Word]: A1 A2 A3 A4 A5 int -> int" Option::Some
+        OpValue::Syscall6 => "syscall6[A1: Word A2: Word A3: Word A4: Word A5: Word A6: Word]: A1 A2 A3 A4 A5 A6 int -> int" Option::Some
         OpValue::Argc => "argc: None -> int" Option::Some
         OpValue::Argv => "argv: None -> ptr" Option::Some
         _ => Option::None(Option[str])
diff --git a/tests/compiler/test_common.casa b/tests/compiler/test_common.casa
index 4e6c56d..477e8fe 100644
--- a/tests/compiler/test_common.casa
+++ b/tests/compiler/test_common.casa
@@ -114,9 +114,9 @@ fn test_signature_matches {
     "str -> bool" signature_from_str = sig4
     "different params don't match" sig4 sig3 signature_matches ! assert_true
 
-    "any -> bool" signature_from_str = sig5
+    f"{TYPE_UNKNOWN} -> bool" signature_from_str = sig5
     "int -> bool" signature_from_str = sig6
-    "any matches int" sig6 sig5 signature_matches assert_true
+    "TYPE_UNKNOWN matches int" sig6 sig5 signature_matches assert_true
 }
 
 fn test_is_builtin_type {
diff --git a/tests/compiler/test_compare.casa b/tests/compiler/test_compare.casa
new file mode 100644
index 0000000..b937bc7
--- /dev/null
+++ b/tests/compiler/test_compare.casa
@@ -0,0 +1,142 @@
+import "../../compiler/common.casa"
+import "../../compiler/error.casa"
+import "../../compiler/lexer.casa"
+import "../../compiler/syntax.casa"
+import "../../compiler/typechecker.casa"
+import "../../lib/test.casa"
+
+# ============================================================================
+# Constants
+# ============================================================================
+"trait Eq {\n    fn eq self:self other:self -> bool\n\n    fn ne self:self other:self -> bool {\n        other self.eq !\n    }\n}\n\ntrait Ord {\n    fn lt self:self other:self -> bool\n\n    fn le self:self other:self -> bool {\n        self other.lt !\n    }\n\n    fn gt self:self other:self -> bool {\n        self other.lt\n    }\n\n    fn ge self:self other:self -> bool {\n        other self.lt !\n    }\n}\n" = EQ_ORD_TRAITS
+
+# ============================================================================
+# Helpers
+# ============================================================================
+
+fn compare_test_typecheck code:str -> Signature {
+    clear_global_state
+    "test" code lex_source = tokens
+    tokens DEFAULT_PARSER parse_ops = ops
+    ops DEFAULT_PARSER resolve_identifiers_global = ops
+    Option::None(Option[Function]) ops type_check_ops
+}
+
+fn compare_test_typecheck_ops code:str -> List[Op] {
+    clear_global_state
+    "test" code lex_source = tokens
+    tokens DEFAULT_PARSER parse_ops = ops
+    ops DEFAULT_PARSER resolve_identifiers_global = ops
+    Option::None(Option[Function]) ops type_check_ops drop
+    ops
+}
+
+fn compare_test_typecheck_error code:str -> Signature {
+    enable_test_mode
+    clear_errors
+    clear_global_state
+    "test" code lex_source = tokens
+    tokens DEFAULT_PARSER parse_ops = ops
+    ops DEFAULT_PARSER resolve_identifiers_global = ops
+    Option::None(Option[Function]) ops type_check_ops
+}
+
+# ============================================================================
+# Primitives: bytecode equality keeps working without trait declarations
+# ============================================================================
+
+fn test_eq_primitive_int_passes {
+    "eq_primitive_int_passes" test_start
+    "1 2 == drop" compare_test_typecheck drop
+    "no errors for int ==" assert_no_errors
+}
+
+fn test_lt_primitive_int_passes {
+    "lt_primitive_int_passes" test_start
+    "1 2 < drop" compare_test_typecheck drop
+    "no errors for int <" assert_no_errors
+}
+
+# ============================================================================
+# Enums: tag comparison keeps working
+# ============================================================================
+
+fn test_enum_with_eq_compares {
+    "enum_with_eq_compares" test_start
+    EQ_ORD_TRAITS "enum Color { Red Green Blue }\nimpl Color { fn eq self:Color other:Color -> bool { self other == } }\nColor::Red Color::Green == drop\n" str::concat compare_test_typecheck drop
+    "no errors for enum with impl Eq ==" assert_no_errors
+}
+
+# ============================================================================
+# User struct: == lowers to MethodCall when impl Eq exists
+# ============================================================================
+
+fn test_user_struct_with_eq_lowers_to_method_call {
+    "user_struct_with_eq_lowers_to_method_call" test_start
+    EQ_ORD_TRAITS "struct Tag { val: int }\nimpl Tag { fn eq self:Tag other:Tag -> bool { self.val other.val == } }\n1 Tag = a\n2 Tag = b\na b == drop\n" str::concat compare_test_typecheck_ops = ops
+    "no errors for struct with impl Eq" assert_no_errors
+    0 = i
+    0 = fn_call_count
+    while i ops.length > do
+        if i ops.get.value OpValue::FnCall(callee) is then
+            if "Tag::eq" callee == then
+                1 += fn_call_count
+            fi
+        fi
+        1 += i
+    done
+    "exactly one Tag::eq call" 1 fn_call_count assert_eq
+}
+
+# ============================================================================
+# User struct without impl Eq: == fails with Eq-bound error
+# ============================================================================
+
+fn test_user_struct_without_eq_fails {
+    "user_struct_without_eq_fails" test_start
+    EQ_ORD_TRAITS "struct NoEq { val: int }\n1 NoEq = a\n2 NoEq = b\na b == drop\n" str::concat compare_test_typecheck_error drop
+    "has errors" assert_has_errors
+    "error mentions Eq trait" "Eq" assert_error_contains
+    "missing trait method error kind" ErrorKind::MissingTraitMethod assert_error_kind
+    clear_errors
+    disable_test_mode
+}
+
+# ============================================================================
+# User struct with impl Eq but no impl Ord: < fails with Ord-bound error
+# ============================================================================
+
+fn test_user_struct_with_eq_but_no_ord_fails_lt {
+    "user_struct_with_eq_but_no_ord_fails_lt" test_start
+    EQ_ORD_TRAITS "struct Tag { val: int }\nimpl Tag { fn eq self:Tag other:Tag -> bool { self.val other.val == } }\n1 Tag = a\n2 Tag = b\na b < drop\n" str::concat compare_test_typecheck_error drop
+    "has errors" assert_has_errors
+    "error mentions Ord trait" "Ord" assert_error_contains
+    "missing trait method error kind" ErrorKind::MissingTraitMethod assert_error_kind
+    clear_errors
+    disable_test_mode
+}
+
+# ============================================================================
+# Same-type rule preserved: comparing different types still fails
+# ============================================================================
+
+fn test_eq_different_types_fails {
+    "eq_different_types_fails" test_start
+    "42 \"hello\" == drop" compare_test_typecheck_error drop
+    "has errors" assert_has_errors
+    "type mismatch error kind" ErrorKind::TypeMismatch assert_error_kind
+    clear_errors
+    disable_test_mode
+}
+
+# ============================================================================
+# Run all tests
+# ============================================================================
+test_eq_primitive_int_passes
+test_lt_primitive_int_passes
+test_enum_with_eq_compares
+test_user_struct_with_eq_lowers_to_method_call
+test_user_struct_without_eq_fails
+test_user_struct_with_eq_but_no_ord_fails_lt
+test_eq_different_types_fails
+test_summary
diff --git a/tests/compiler/test_display.casa b/tests/compiler/test_display.casa
index 658a94b..a502902 100644
--- a/tests/compiler/test_display.casa
+++ b/tests/compiler/test_display.casa
@@ -35,6 +35,15 @@ fn display_test_typecheck code:str -> Signature {
     Option::None(Option[Function]) ops type_check_ops
 }
 
+fn display_test_typecheck_ops code:str -> List[Op] {
+    clear_global_state
+    "test" code lex_source = tokens
+    tokens DEFAULT_PARSER parse_ops = ops
+    ops DEFAULT_PARSER resolve_identifiers_global = ops
+    Option::None(Option[Function]) ops type_check_ops drop
+    ops
+}
+
 fn display_test_typecheck_error code:str -> Signature {
     enable_test_mode
     clear_errors
@@ -216,6 +225,65 @@ fn test_fstring_mixed_types {
     "no errors for mixed primitive f-string" assert_no_errors
 }
 
+# ============================================================================
+# Typechecker: print routes primitives to existing specialized ops
+# ============================================================================
+
+fn test_print_int_dispatches_to_print_int {
+    "print_int_dispatches_to_print_int" test_start
+    "42 print\n" display_test_typecheck_ops = ops
+    "no errors for int print" assert_no_errors
+    "int print resolves to PrintInt" 1 ops.get.value OpValue::PrintInt is assert_true
+}
+
+fn test_print_str_dispatches_to_print_str {
+    "print_str_dispatches_to_print_str" test_start
+    "\"hi\" print\n" display_test_typecheck_ops = ops
+    "no errors for str print" assert_no_errors
+    "str print resolves to PrintStr" 1 ops.get.value OpValue::PrintStr is assert_true
+}
+
+# ============================================================================
+# Typechecker: print on user struct with Display lowers to a method call
+# ============================================================================
+
+fn test_print_struct_with_display_lowers_to_method_call {
+    "print_struct_with_display_lowers_to_method_call" test_start
+    DISPLAY_TRAIT "struct Tag { val: int }\nimpl Tag { fn to_str self:Tag -> str { \"tag\" } }\n1 Tag = t\nt print\n" str::concat display_test_typecheck_ops = ops
+    "no errors for Display struct print" assert_no_errors
+    0 = lower_index
+    0 = fn_call_count
+    0 = print_str_count
+    while lower_index ops.length > do
+        lower_index ops.get.value = lower_value
+        if lower_value OpValue::FnCall(callee) is then
+            if "Tag::to_str" callee == then
+                1 += fn_call_count
+            fi
+        fi
+        if lower_value OpValue::PrintStr is then
+            1 += print_str_count
+        fi
+        1 += lower_index
+    done
+    "exactly one Tag::to_str call" 1 fn_call_count assert_eq
+    "exactly one PrintStr after lowering" 1 print_str_count assert_eq
+}
+
+# ============================================================================
+# Typechecker: print on user struct without Display raises a clear error
+# ============================================================================
+
+fn test_print_struct_without_display_raises {
+    "print_struct_without_display_raises" test_start
+    DISPLAY_TRAIT "struct NoDisplay { val: int }\n1 NoDisplay = n\nn print\n" str::concat display_test_typecheck_error drop
+    "has errors" assert_has_errors
+    "error mentions Display trait" "Display" assert_error_contains
+    "missing trait method error kind" ErrorKind::MissingTraitMethod assert_error_kind
+    clear_errors
+    disable_test_mode
+}
+
 # ============================================================================
 # Run all tests
 # ============================================================================
@@ -239,4 +307,9 @@ test_type_satisfies_trait_no_fallback_method
 test_trait_exec_pushes_return_type
 # Multi-type-parameter trait bound ordering
 test_multi_trait_bound_ordering
+# print dispatch
+test_print_int_dispatches_to_print_int
+test_print_str_dispatches_to_print_str
+test_print_struct_with_display_lowers_to_method_call
+test_print_struct_without_display_raises
 test_summary
diff --git a/tests/compiler/test_enum.casa b/tests/compiler/test_enum.casa
index 2096f02..dfd54a8 100644
--- a/tests/compiler/test_enum.casa
+++ b/tests/compiler/test_enum.casa
@@ -94,6 +94,8 @@ fn is_jump_ne_inst value:InstValue -> bool { value InstValue::JumpNe is }
 
 fn is_print_int_inst value:InstValue -> bool { value InstValue::PrintInt is }
 
+fn is_print_str_inst value:InstValue -> bool { value InstValue::PrintStr is }
+
 fn is_heap_alloc_inst value:InstValue -> bool { value InstValue::HeapAlloc is }
 
 fn is_store64_inst value:InstValue -> bool { value InstValue::Store64 is }
@@ -381,7 +383,7 @@ fn test_enum_as_return_type {
 
 fn test_enum_print {
     "enum_print" test_start
-    "enum Color { Red Green Blue }\nColor::Red print" tc_enum = sig
+    "trait Display { fn to_str self:self -> str }\nenum Color { Red Green Blue }\nimpl Color { fn to_str c:Color -> str { \"red\" } }\nColor::Red print" tc_enum = sig
     "no returns" 0 sig Signature::return_types.length assert_eq
 }
 
@@ -511,10 +513,10 @@ fn test_match_compiles_to_dup_eq_jump_pattern {
     "has JUMP_NE" 0 &is_jump_ne_inst prog Program::bytecode count_insts != assert_true
 }
 
-fn test_enum_print_compiles_to_print_int {
-    "enum_print_compiles_to_print_int" test_start
-    "enum Color { Red Green Blue }\nColor::Red print\n" compile_enum = prog
-    "has PRINT_INT" &is_print_int_inst prog Program::bytecode has_inst_kind assert_true
+fn test_enum_print_compiles_via_display {
+    "enum_print_compiles_via_display" test_start
+    "trait Display { fn to_str self:self -> str }\nenum Color { Red Green Blue }\nimpl Color { fn to_str c:Color -> str { \"red\" } }\nColor::Red print\n" compile_enum = prog
+    "has PRINT_STR" &is_print_str_inst prog Program::bytecode has_inst_kind assert_true
 }
 
 fn test_data_enum_variant_compiles_to_heap_alloc {
@@ -1122,7 +1124,7 @@ test_enum_variant_compiles_to_push_ordinal_0
 test_enum_variant_compiles_to_push_ordinal_1
 test_enum_variant_compiles_to_push_ordinal_2
 test_match_compiles_to_dup_eq_jump_pattern
-test_enum_print_compiles_to_print_int
+test_enum_print_compiles_via_display
 test_data_enum_variant_compiles_to_heap_alloc
 test_data_enum_stores_ordinal
 # Match parsing
diff --git a/tests/compiler/test_generic_structs.casa b/tests/compiler/test_generic_structs.casa
index 76e95d4..9e6d55b 100644
--- a/tests/compiler/test_generic_structs.casa
+++ b/tests/compiler/test_generic_structs.casa
@@ -185,7 +185,7 @@ fn test_typecheck_generic_struct_in_function {
 fn test_resolve_generic_struct_new {
     "resolve_generic_struct_new" test_start
     "struct Box[T] { value: T }\n42 Box" resolve_gs = ops
-    OpValue::StructNew ops find_ops_by_kind = struct_new_ops
+    List::new(List[str]) empty_location List::new(List[Member]) "" CasaStruct OpValue::StructNew ops find_ops_by_kind = struct_new_ops
     "has struct new op" 1 struct_new_ops.length assert_eq
 }
 
diff --git a/tests/compiler/test_lsp.casa b/tests/compiler/test_lsp.casa
index a62ee7b..bb6adbb 100644
--- a/tests/compiler/test_lsp.casa
+++ b/tests/compiler/test_lsp.casa
@@ -565,7 +565,7 @@ fn test_compute_hover_drop {
     "42 drop" lsp_test_state = state
     3 0 state compute_hover = result
     "is some" result.is_some assert_true
-    "contains drop effect" 0 result.unwrap HoverContent::content "drop: any -> None" str::find >= assert_true
+    "contains drop effect" 0 result.unwrap HoverContent::content "drop[T]: T -> None" str::find >= assert_true
 }
 
 fn test_compute_hover_dup {
@@ -573,7 +573,7 @@ fn test_compute_hover_dup {
     "42 dup drop drop" lsp_test_state = state
     3 0 state compute_hover = result
     "is some" result.is_some assert_true
-    "contains dup effect" 0 result.unwrap HoverContent::content "dup: any -> any any" str::find >= assert_true
+    "contains dup effect" 0 result.unwrap HoverContent::content "dup[T]: T -> T T" str::find >= assert_true
 }
 
 fn test_compute_hover_swap {
@@ -581,7 +581,23 @@ fn test_compute_hover_swap {
     "1 2 swap drop drop" lsp_test_state = state
     4 0 state compute_hover = result
     "is some" result.is_some assert_true
-    "contains swap effect" 0 result.unwrap HoverContent::content "swap: any any -> any any" str::find >= assert_true
+    "contains swap effect" 0 result.unwrap HoverContent::content "swap[T1 T2]: T1 T2 -> T2 T1" str::find >= assert_true
+}
+
+fn test_compute_hover_over {
+    "compute_hover_over" test_start
+    "1 2 over drop drop drop" lsp_test_state = state
+    4 0 state compute_hover = result
+    "is some" result.is_some assert_true
+    "contains over effect" 0 result.unwrap HoverContent::content "over[T1 T2]: T1 T2 -> T2 T1 T2" str::find >= assert_true
+}
+
+fn test_compute_hover_rot {
+    "compute_hover_rot" test_start
+    "1 2 3 rot drop drop drop" lsp_test_state = state
+    6 0 state compute_hover = result
+    "is some" result.is_some assert_true
+    "contains rot effect" 0 result.unwrap HoverContent::content "rot[T1 T2 T3]: T1 T2 T3 -> T3 T1 T2" str::find >= assert_true
 }
 
 fn test_compute_hover_not {
@@ -597,7 +613,7 @@ fn test_compute_hover_eq {
     "1 2 == drop" lsp_test_state = state
     4 0 state compute_hover = result
     "is some" result.is_some assert_true
-    "contains eq effect" 0 result.unwrap HoverContent::content "==: any any -> bool" str::find >= assert_true
+    "contains eq effect" 0 result.unwrap HoverContent::content "==: [T: Eq] T T -> bool" str::find >= assert_true
 }
 
 fn test_compute_hover_print {
@@ -605,7 +621,7 @@ fn test_compute_hover_print {
     "42 print" lsp_test_state = state
     3 0 state compute_hover = result
     "is some" result.is_some assert_true
-    "contains print effect" 0 result.unwrap HoverContent::content "print: any -> None" str::find >= assert_true
+    "contains print effect" 0 result.unwrap HoverContent::content "print: [T: Display] T -> None" str::find >= assert_true
 }
 
 fn test_compute_hover_exec {
@@ -1211,6 +1227,8 @@ test_compute_hover_assign_variable
 test_compute_hover_drop
 test_compute_hover_dup
 test_compute_hover_swap
+test_compute_hover_over
+test_compute_hover_rot
 test_compute_hover_not
 test_compute_hover_eq
 test_compute_hover_print
diff --git a/tests/compiler/test_match_underflow.casa b/tests/compiler/test_match_underflow.casa
index de242e3..b696b0c 100644
--- a/tests/compiler/test_match_underflow.casa
+++ b/tests/compiler/test_match_underflow.casa
@@ -65,8 +65,7 @@ fn test_match_without_subject_in_declared_fn_body_errors {
 }
 
 # ============================================================================
-# Inference contexts (undeclared fn, lambda) keep pre-fix behavior:
-# empty stack at `match` synthesizes an inferred parameter, no error.
+# Lambda still infers from caller-pushed values; non-lambda functions never do.
 # ============================================================================
 
 fn test_lambda_match_subject_inferred {
@@ -80,13 +79,14 @@ fn test_lambda_match_subject_inferred {
     disable_test_mode
 }
 
-fn test_undeclared_fn_match_subject_inferred {
-    "undeclared_fn_match_subject_inferred" test_start
+fn test_undeclared_fn_match_subject_errors {
+    "undeclared_fn_match_subject_errors" test_start
     enable_test_mode
     clear_global_state
     clear_errors
     "fn f { match 1 => 1 _ => 2 end drop }\n42 f\n" tc_mu drop
-    "no errors" assert_no_errors
+    "has errors" assert_has_errors
+    "stack underflow kind" ErrorKind::StackUnderflow assert_error_kind
     clear_errors
     disable_test_mode
 }
@@ -113,6 +113,6 @@ test_top_level_match_without_subject_errors
 test_match_underflow_message_names_construct
 test_match_without_subject_in_declared_fn_body_errors
 test_lambda_match_subject_inferred
-test_undeclared_fn_match_subject_inferred
+test_undeclared_fn_match_subject_errors
 test_well_formed_match_still_passes
 test_summary
diff --git a/tests/compiler/test_traits.casa b/tests/compiler/test_traits.casa
index 5e6ee2e..e7f19a1 100644
--- a/tests/compiler/test_traits.casa
+++ b/tests/compiler/test_traits.casa
@@ -390,6 +390,26 @@ fn test_undefined_trait_returns_false {
     clear_global_state
     "does not satisfy" Option::None(Option[Function]) "Nonexistent" "int" type_satisfies_trait ! assert_true
 }
+# Primitive Eq impls must satisfy a structurally-matching Eq trait.
+
+fn test_int_satisfies_eq_trait {
+    "int_satisfies_eq_trait" test_start
+    "trait Eq { fn eq self:self other:self -> bool }\nimpl int { fn eq self:int other:int -> bool { self other == } }\n" trait_test_resolve drop
+    "satisfies" Option::None(Option[Function]) "Eq" "int" type_satisfies_trait assert_true
+}
+
+fn test_int_satisfies_ord_trait {
+    "int_satisfies_ord_trait" test_start
+    "trait Ord { fn lt self:self other:self -> bool }\nimpl int { fn lt self:int other:int -> bool { other self < } }\n" trait_test_resolve drop
+    "satisfies" Option::None(Option[Function]) "Ord" "int" type_satisfies_trait assert_true
+}
+
+fn test_empty_word_trait_satisfied_by_any_type {
+    "empty_word_trait_satisfied_by_any_type" test_start
+    "trait Word { }\n" trait_test_resolve drop
+    "int satisfies" Option::None(Option[Function]) "Word" "int" type_satisfies_trait assert_true
+    "str satisfies" Option::None(Option[Function]) "Word" "str" type_satisfies_trait assert_true
+}
 
 # ============================================================================
 # extract_generic_params
@@ -814,6 +834,52 @@ fn test_trait_bounded_fn_with_conflicting_type_var_raises {
     disable_test_mode
 }
 
+# ============================================================================
+# Supertraits
+# ============================================================================
+
+fn test_trait_with_supertrait_parses {
+    "trait_with_supertrait_parses" test_start
+    "trait Eq { fn eq self:self other:self -> bool }\ntrait Hashable: Eq { fn hash self:self -> int }\n" trait_test_parse drop
+    "Hashable" DEFAULT_PARSER.store.traits.get.unwrap = hashable
+    "supertrait count" 1 hashable CasaTrait::supertraits.length assert_eq
+    "supertrait name" "Eq" 0 hashable CasaTrait::supertraits.get TraitBound::name assert_str_eq
+}
+
+fn test_trait_with_undefined_supertrait_raises {
+    "trait_with_undefined_supertrait_raises" test_start
+    enable_test_mode
+    clear_errors
+    "trait Hashable: Bogus { fn hash self:self -> int }\n" trait_test_parse drop
+    "has errors" assert_has_errors
+    "undefined supertrait" ErrorKind::UndefinedName assert_error_kind
+    clear_errors
+    disable_test_mode
+}
+
+fn test_supertrait_method_required_for_satisfaction {
+    "supertrait_method_required_for_satisfaction" test_start
+    "trait Eq { fn eq self:self other:self -> bool }\ntrait Hashable: Eq { fn hash self:self -> int }\nstruct Bare { v: int }\nimpl Bare { fn hash self:Bare -> int { self Bare::v } }\n" trait_test_resolve drop
+    "Hashable not satisfied without Eq impl" Option::None(Option[Function]) "Hashable" "Bare" type_satisfies_trait ! assert_true
+}
+
+fn test_supertrait_satisfaction_with_full_impl {
+    "supertrait_satisfaction_with_full_impl" test_start
+    "trait Eq { fn eq self:self other:self -> bool }\ntrait Hashable: Eq { fn hash self:self -> int }\nstruct Full { v: int }\nimpl Full { fn hash self:Full -> int { self Full::v } fn eq self:Full other:Full -> bool { self Full::v other Full::v == } }\n" trait_test_resolve drop
+    "Hashable satisfied with Eq impl" Option::None(Option[Function]) "Hashable" "Full" type_satisfies_trait assert_true
+}
+
+fn test_supertrait_negative_typecheck_raises {
+    "supertrait_negative_typecheck_raises" test_start
+    enable_test_mode
+    clear_errors
+    "trait Eq { fn eq self:self other:self -> bool }\ntrait Hashable: Eq { fn hash self:self -> int }\nstruct Bare { v: int }\nimpl Bare { fn hash self:Bare -> int { self Bare::v } }\nfn use_hash[K: Hashable] k:K -> int { k .hash }\n1 Bare = b\nb use_hash drop\n" trait_test_typecheck drop
+    "has errors" assert_has_errors
+    "missing Eq for Hashable bound" ErrorKind::TypeMismatch assert_error_kind
+    clear_errors
+    disable_test_mode
+}
+
 # ============================================================================
 # Parse map type in signature
 # ============================================================================
@@ -906,6 +972,9 @@ test_partial_impl_does_not_satisfy
 test_struct_satisfies_generic_trait_concrete_int
 test_struct_does_not_satisfy_generic_trait_wrong_inner
 test_undefined_trait_returns_false
+test_int_satisfies_eq_trait
+test_int_satisfies_ord_trait
+test_empty_word_trait_satisfied_by_any_type
 # Multi-param generics
 test_map_kv_type_params
 test_set_k_type_params
@@ -945,6 +1014,12 @@ test_generic_trait_bound_structural_mismatch_raises
 test_type_var_arg_generic_trait_bound_happy_path
 test_type_var_arg_bound_conflict_with_param_raises
 test_type_var_arg_bound_structural_mismatch_raises
+# Supertraits
+test_trait_with_supertrait_parses
+test_trait_with_undefined_supertrait_raises
+test_supertrait_method_required_for_satisfaction
+test_supertrait_satisfaction_with_full_impl
+test_supertrait_negative_typecheck_raises
 # Parse map type
 test_parse_map_type_in_signature
 test_summary
diff --git a/tests/compiler/test_type_annotations.casa b/tests/compiler/test_type_annotations.casa
index c449553..9ede822 100644
--- a/tests/compiler/test_type_annotations.casa
+++ b/tests/compiler/test_type_annotations.casa
@@ -155,7 +155,7 @@ fn test_annotation_char {
 fn test_no_annotation_on_increment {
     "no_annotation_on_increment" test_start
     "42 = x 1 += x" test_parse = ops
-    OpValue::AssignInc ops find_ops_by_kind = inc_ops
+    "" OpValue::AssignInc ops find_ops_by_kind = inc_ops
     "count" 1 inc_ops.length assert_eq
     "annotation empty" "" 0 inc_ops.get Op::type_annotation assert_str_eq
 }
@@ -163,7 +163,7 @@ fn test_no_annotation_on_increment {
 fn test_no_annotation_on_decrement {
     "no_annotation_on_decrement" test_start
     "42 = x 1 -= x" test_parse = ops
-    OpValue::AssignDec ops find_ops_by_kind = dec_ops
+    "" OpValue::AssignDec ops find_ops_by_kind = dec_ops
     "count" 1 dec_ops.length assert_eq
     "annotation empty" "" 0 dec_ops.get Op::type_annotation assert_str_eq
 }
@@ -196,24 +196,54 @@ fn test_tc_annotation_matches_stack {
     "return type" "int" 0 sig Signature::return_types.get assert_str_eq
 }
 
-fn test_tc_narrow_any_to_int {
-    "tc_narrow_any_to_int" test_start
-    "42 (any) = x:int x" tc_code = sig
+fn test_tc_annotation_to_int {
+    "tc_annotation_to_int" test_start
+    "42 = x:int x" tc_code = sig
     "return type" "int" 0 sig Signature::return_types.get assert_str_eq
 }
 
-fn test_tc_narrow_any_to_str {
-    "tc_narrow_any_to_str" test_start
-    "\"hello\" (any) = x:str x" tc_code = sig
+fn test_tc_annotation_to_str {
+    "tc_annotation_to_str" test_start
+    "\"hello\" = x:str x" tc_code = sig
     "return type" "str" 0 sig Signature::return_types.get assert_str_eq
 }
 
-fn test_tc_narrow_any_to_option {
-    "tc_narrow_any_to_option" test_start
-    OPTION_ENUM "Option::None (any) = x:Option[T] x" str::concat tc_code = sig
+fn test_tc_annotation_to_option {
+    "tc_annotation_to_option" test_start
+    OPTION_ENUM "Option::None = x:Option[T] x" str::concat tc_code = sig
     "return type" "Option[T]" 0 sig Signature::return_types.get assert_str_eq
 }
 
+fn assert_cast_rejected_as_unknown_type source:str expected_type:str {
+    enable_test_mode
+    clear_global_state
+    clear_errors
+    "test" source lex_source = tokens
+    tokens DEFAULT_PARSER parse_ops = ops
+    ops DEFAULT_PARSER resolve_identifiers_global = ops
+    Option::None(Option[Function]) ops type_check_ops drop
+    "has errors" assert_has_errors
+    "syntax error" ErrorKind::Syntax assert_error_kind
+    "type message" f"type `{expected_type}` does not exist" assert_error_contains
+    clear_errors
+    disable_test_mode
+}
+
+fn test_tc_reject_unknown_cast {
+    "tc_reject_unknown_cast" test_start
+    "foo" "42 (foo)" assert_cast_rejected_as_unknown_type
+}
+
+fn test_tc_reject_unknown_uppercase_cast {
+    "tc_reject_unknown_uppercase_cast" test_start
+    "T" "42 (T)" assert_cast_rejected_as_unknown_type
+}
+
+fn test_tc_reject_unknown_generic_param_cast {
+    "tc_reject_unknown_generic_param_cast" test_start
+    "List[Foo]" "42 (List[Foo])" assert_cast_rejected_as_unknown_type
+}
+
 fn test_tc_reassignment_keeps_annotated_type {
     "tc_reassignment_keeps_annotated_type" test_start
     "42 = x:int 99 = x x" tc_code = sig
@@ -232,9 +262,9 @@ fn test_tc_annotation_in_function_body {
     "return type" "int" 0 sig Signature::return_types.get assert_str_eq
 }
 
-fn test_tc_narrow_any_in_function {
-    "tc_narrow_any_in_function" test_start
-    "fn foo -> int { 42 (any) = x:int x } foo" tc_code = sig
+fn test_tc_annotation_in_function_explicit {
+    "tc_annotation_in_function_explicit" test_start
+    "fn foo -> int { 42 = x:int x } foo" tc_code = sig
     "return type" "int" 0 sig Signature::return_types.get assert_str_eq
 }
 
@@ -315,10 +345,10 @@ fn test_warn_no_warn_matching_types {
     "no warnings" 0 assert_warning_count
 }
 
-fn test_warn_no_warn_narrowing_any {
-    "warn_no_warn_narrowing_any" test_start
+fn test_warn_no_warn_annotation_match {
+    "warn_no_warn_annotation_match" test_start
     clear_warnings
-    "42 (any) = x:int" tc_code drop
+    "42 = x:int" tc_code drop
     "no warnings" 0 assert_warning_count
 }
 
@@ -344,13 +374,16 @@ test_tc_annotation_int
 test_tc_annotation_str
 test_tc_annotation_bool
 test_tc_annotation_matches_stack
-test_tc_narrow_any_to_int
-test_tc_narrow_any_to_str
-test_tc_narrow_any_to_option
+test_tc_annotation_to_int
+test_tc_annotation_to_str
+test_tc_annotation_to_option
+test_tc_reject_unknown_cast
+test_tc_reject_unknown_uppercase_cast
+test_tc_reject_unknown_generic_param_cast
 test_tc_reassignment_keeps_annotated_type
 test_tc_without_annotation
 test_tc_annotation_in_function_body
-test_tc_narrow_any_in_function
+test_tc_annotation_in_function_explicit
 test_tc_annotation_with_struct
 test_tc_option_int_with_some
 # Typechecker errors: mismatch (currently no validation in self-hosted)
@@ -360,5 +393,5 @@ test_tc_mismatch_bool_as_str
 test_tc_reassignment_type_mismatch
 # Warnings: lossy annotation (currently no warnings in self-hosted)
 test_warn_no_warn_matching_types
-test_warn_no_warn_narrowing_any
+test_warn_no_warn_annotation_match
 test_summary
diff --git a/tests/compiler/test_typechecker.casa b/tests/compiler/test_typechecker.casa
index d267997..3c78406 100644
--- a/tests/compiler/test_typechecker.casa
+++ b/tests/compiler/test_typechecker.casa
@@ -43,7 +43,9 @@ fn tc_check ops:List[Op] -> TypeChecker {
         helper_kind OpValue::Gt is ||
         helper_kind OpValue::Ge is ||
         then
-            helper_op helper_tc check_comparison
+            1 += helper_i
+            Option::None(Option[Function]) helper_i ops helper_op helper_tc check_comparison = helper_i
+            continue
             # Boolean
         elif
         helper_kind OpValue::And is
@@ -82,10 +84,12 @@ fn tc_check ops:List[Op] -> TypeChecker {
         helper_kind OpValue::Store64 is ||
         helper_kind OpValue::HeapAlloc is ||
         then
-            helper_op helper_tc check_memory
+            Option::None(Option[Function]) helper_op helper_tc check_memory
             # Print
         elif helper_kind OpValue::Print is then
-            helper_op helper_tc check_io
+            1 += helper_i
+            Option::None(Option[Function]) helper_i ops helper_op helper_tc check_io = helper_i
+            continue
             # Typeof
         elif helper_kind OpValue::Typeof is then
             helper_op helper_tc check_typeof
@@ -103,7 +107,7 @@ fn tc_check ops:List[Op] -> TypeChecker {
         helper_kind OpValue::Syscall5 is ||
         helper_kind OpValue::Syscall6 is ||
         then
-            helper_op helper_tc check_syscalls
+            Option::None(Option[Function]) helper_op helper_tc check_syscalls
             # Argc / Argv
         elif helper_kind OpValue::Argc is then
             "int" helper_tc stack_push
@@ -393,7 +397,7 @@ fn test_print_dispatch {
 }
 
 # ============================================================================
-# Tests: Typeof pops any, pushes str
+# Tests: Typeof pops a generic value, pushes str
 # ============================================================================
 
 fn test_typeof_effect {
@@ -474,8 +478,8 @@ fn test_argc_argv {
 fn test_types_match {
     "types_match" test_start
     "same types" "int" "int" types_match assert_true
-    "any matches int" "int" "any" types_match assert_true
-    "int matches any" "any" "int" types_match assert_true
+    "TYPE_UNKNOWN matches int" "int" TYPE_UNKNOWN types_match assert_true
+    "int matches TYPE_UNKNOWN" TYPE_UNKNOWN "int" types_match assert_true
     "different types" "str" "int" types_match ! assert_true
     "fn base matches fn type" "fn[int -> int]" "fn" types_match assert_true
     "generic base matches" "List[int]" "List" types_match assert_true
@@ -488,8 +492,8 @@ fn test_types_match {
 fn test_unify_type {
     "unify_type" test_start
     "same" "int" "int" "int" unify_type assert_str_eq
-    "any + int" "int" "int" "any" unify_type assert_str_eq
-    "int + any" "int" "any" "int" unify_type assert_str_eq
+    "unknown + int" "int" "int" TYPE_UNKNOWN unify_type assert_str_eq
+    "int + unknown" "int" TYPE_UNKNOWN "int" unify_type assert_str_eq
     "incompatible" "" "str" "int" unify_type assert_str_eq
 }
 
@@ -1007,7 +1011,7 @@ fn test_tc_pipeline_div_mod {
 
 fn test_types_match_extended {
     "types_match_extended" test_start
-    "both any" "any" "any" types_match assert_true
+    "both unknown" TYPE_UNKNOWN TYPE_UNKNOWN types_match assert_true
     "str str" "str" "str" types_match assert_true
     "bool bool" "bool" "bool" types_match assert_true
     "ptr ptr" "ptr" "ptr" types_match assert_true
@@ -1016,17 +1020,17 @@ fn test_types_match_extended {
 }
 
 # ============================================================================
-# Tests: stacks_compatible with any type
+# Tests: stacks_compatible with TYPE_UNKNOWN sentinel
 # ============================================================================
 
-fn test_stacks_compatible_with_any {
-    "stacks_compatible_with_any" test_start
+fn test_stacks_compatible_with_unknown {
+    "stacks_compatible_with_unknown" test_start
     List::new(List[str]) = stack_a
     "int" stack_a.push
     List::new(List[str]) = stack_b
-    "any" stack_b.push
+    TYPE_UNKNOWN stack_b.push
     stack_b stack_a stacks_compatible = result
-    "any matches int" 1 result.length assert_eq
+    "TYPE_UNKNOWN matches int" 1 result.length assert_eq
 }
 
 fn test_stacks_compatible_empty {
@@ -1204,6 +1208,79 @@ fn test_error_syscall3_non_int_number {
     disable_test_mode
 }
 
+# ============================================================================
+# Tests: Word-bound on syscall and store builtins
+# ============================================================================
+
+fn tc_full code:str {
+    clear_global_state
+    enable_test_mode
+    clear_errors
+    "test" code lex_source = tokens
+    tokens DEFAULT_PARSER parse_ops = ops
+    ops DEFAULT_PARSER resolve_identifiers_global = ops
+    Option::None(Option[Function]) ops type_check_ops drop
+    type_check_functions
+}
+
+fn test_error_syscall_non_word_bound_type_var {
+    "error_syscall_non_word_bound_type_var" test_start
+    "trait Word { } trait NotWord { } fn fail_syscall[T: NotWord] arg:T -> int { arg 1 syscall1 } 42 fail_syscall drop" tc_full
+    "has errors" assert_has_errors
+    "mentions Word" "Word" assert_error_contains
+    clear_errors
+    disable_test_mode
+}
+
+fn test_syscall_word_bound_explicit_passes {
+    "syscall_word_bound_explicit_passes" test_start
+    "trait Word { } fn ok_syscall[T: Word] arg:T -> int { arg 1 syscall1 } 42 ok_syscall drop" tc_full
+    "no errors" 0 ERRORS.length assert_eq
+    clear_errors
+    disable_test_mode
+}
+
+fn test_syscall_unbound_type_var_passes {
+    "syscall_unbound_type_var_passes" test_start
+    "trait Word { } fn deferred_syscall[T] arg:T -> int { arg 1 syscall1 } 42 deferred_syscall drop" tc_full
+    "no errors" 0 ERRORS.length assert_eq
+    clear_errors
+    disable_test_mode
+}
+
+fn test_error_store64_non_word_bound_type_var {
+    "error_store64_non_word_bound_type_var" test_start
+    "trait Word { } trait NotWord { } fn fail_store[T: NotWord] destination:ptr value:T -> None { value destination store64 } 42 1 alloc fail_store" tc_full
+    "has errors" assert_has_errors
+    "mentions Word" "Word" assert_error_contains
+    clear_errors
+    disable_test_mode
+}
+
+fn test_store64_word_bound_explicit_passes {
+    "store64_word_bound_explicit_passes" test_start
+    "trait Word { } fn ok_store[T: Word] destination:ptr value:T -> None { value destination store64 } 42 1 alloc ok_store" tc_full
+    "no errors" 0 ERRORS.length assert_eq
+    clear_errors
+    disable_test_mode
+}
+
+fn test_store64_unbound_type_var_passes {
+    "store64_unbound_type_var_passes" test_start
+    "trait Word { } fn deferred_store[T] destination:ptr value:T -> None { value destination store64 } 42 1 alloc deferred_store" tc_full
+    "no errors" 0 ERRORS.length assert_eq
+    clear_errors
+    disable_test_mode
+}
+
+fn test_store64_supertrait_word_passes {
+    "store64_supertrait_word_passes" test_start
+    "trait Word { } trait Inner: Word { } fn super_store[T: Inner] destination:ptr value:T -> None { value destination store64 } 42 1 alloc super_store" tc_full
+    "no errors" 0 ERRORS.length assert_eq
+    clear_errors
+    disable_test_mode
+}
+
 # ============================================================================
 # Tests: Syscall op-level stack effects
 # ============================================================================
@@ -1509,18 +1586,22 @@ fn test_types_match_array_types {
 }
 
 # ============================================================================
-# Tests: Print dispatch for ptr (falls to print_int)
+# Tests: Print dispatch on a non-Display type adds an error
 # ============================================================================
 
-fn test_print_dispatch_ptr {
-    "print_dispatch_ptr" test_start
+fn test_print_dispatch_no_display {
+    "print_dispatch_no_display" test_start
+    enable_test_mode
+    clear_errors
     List::new(List[Op]) = ops
     empty_location 10 OpValue::PushInt make_op ops.push
     empty_location OpValue::HeapAlloc make_op ops.push
     empty_location OpValue::Print make_op ops.push
     ops tc_check drop
-    # ptr falls through to print_int
-    "print ptr resolved" 2 ops.get.value OpValue::PrintInt is assert_true
+    "ptr without Display impl raises an error" assert_has_errors
+    "error mentions Display trait" "Display" assert_error_contains
+    clear_errors
+    disable_test_mode
 }
 
 # ============================================================================
@@ -1667,7 +1748,7 @@ fn test_branch_while_empty_body {
 
 fn test_branch_frame_kind_dispatch {
     "branch_frame_kind_dispatch" test_start
-    make_typechecker = tc
+    DEFAULT_PARSER.store make_typechecker = tc
     List::new(List[Op]) = ops
     empty_location OpValue::IfStart make_op ops.push
     0 = bd_i
@@ -1702,11 +1783,70 @@ fn test_branch_frame_kind_dispatch {
     fi
     "mutation persists through binding" default_present_after assert_true
 }
+
+# ============================================================================
+# Tests: Array literal element-type inference
+# ============================================================================
+
+fn test_array_literal_int_inference {
+    "array_literal_int_inference" test_start
+    "[1 2 3]" tc_string = sig
+    "one return" 1 sig Signature::return_types.length assert_eq
+    "array[int]" "array[int]" 0 sig Signature::return_types.get assert_str_eq
+}
+
+fn test_array_literal_str_inference {
+    "array_literal_str_inference" test_start
+    "[\"a\" \"b\"]" tc_string = sig
+    "array[str]" "array[str]" 0 sig Signature::return_types.get assert_str_eq
+}
+
+fn test_array_literal_bool_inference {
+    "array_literal_bool_inference" test_start
+    "[true false]" tc_string = sig
+    "array[bool]" "array[bool]" 0 sig Signature::return_types.get assert_str_eq
+}
+
+fn test_array_literal_empty {
+    "array_literal_empty" test_start
+    "[] (array[int])" tc_string = sig
+    "explicit cast resolves" "array[int]" 0 sig Signature::return_types.get assert_str_eq
+}
+
+fn test_array_literal_empty_with_annotation {
+    "array_literal_empty_with_annotation" test_start
+    "[] = xs:array[int] xs" tc_string = sig
+    "annotation resolves" "array[int]" 0 sig Signature::return_types.get assert_str_eq
+}
+
+fn test_array_literal_empty_with_cast_then_assign {
+    "array_literal_empty_with_cast_then_assign" test_start
+    "[] (array[str]) = xs xs" tc_string = sig
+    "cast then assign" "array[str]" 0 sig Signature::return_types.get assert_str_eq
+}
+
+fn test_error_array_literal_heterogeneous {
+    "error_array_literal_heterogeneous" test_start
+    "[1 \"a\"]" tc_string_error drop
+    "has errors" assert_has_errors
+    "type mismatch" ErrorKind::TypeMismatch assert_error_kind
+    clear_errors
+    disable_test_mode
+}
+
+fn test_error_array_literal_unresolved_assignment {
+    "error_array_literal_unresolved_assignment" test_start
+    "[] = xs xs drop" tc_string_error drop
+    "has errors" assert_has_errors
+    "type mismatch" ErrorKind::TypeMismatch assert_error_kind
+    clear_errors
+    disable_test_mode
+}
 # OpFnReturn inside a branch restores live from the frame's `before` snapshot.
 
 fn test_branch_return_inside_if_restores_live {
     "branch_return_inside_if_restores_live" test_start
-    make_typechecker = tc
+    DEFAULT_PARSER.store make_typechecker = tc
     # Seed the live stack with a single `int`.
     "int" tc stack_push
     # Begin an `if true then` block.
@@ -1723,7 +1863,7 @@ fn test_branch_return_inside_if_restores_live {
         OpValue::IfCondition br_kind == ||
         then
             br_op tc check_if_block
-        elif OpValue::PushBool br_kind == then
+        elif 0 OpValue::PushBool br_kind == then
             "bool" tc stack_push
         fi
         1 += br_i
@@ -1808,7 +1948,7 @@ test_tc_pipeline_bitshift
 test_tc_pipeline_syscall_remaining
 test_tc_pipeline_div_mod
 test_types_match_extended
-test_stacks_compatible_with_any
+test_stacks_compatible_with_unknown
 test_stacks_compatible_empty
 test_error_arithmetic_str_int
 test_error_arithmetic_bool_int
@@ -1821,6 +1961,13 @@ test_error_store_non_ptr
 test_error_syscall_non_int_number
 test_error_syscall1_non_int_number
 test_error_syscall3_non_int_number
+test_error_syscall_non_word_bound_type_var
+test_syscall_word_bound_explicit_passes
+test_syscall_unbound_type_var_passes
+test_error_store64_non_word_bound_type_var
+test_store64_word_bound_explicit_passes
+test_store64_unbound_type_var_passes
+test_store64_supertrait_word_passes
 test_store_accepts_any_value_type
 test_memory_store64
 test_syscall_any_arg_type
@@ -1847,7 +1994,7 @@ test_tc_pipeline_print_pops
 test_stacks_compatible_different_types
 test_types_match_fn_types
 test_types_match_array_types
-test_print_dispatch_ptr
+test_print_dispatch_no_display
 test_typeof_annotation
 test_type_cast_str_to_int
 test_type_cast_bool_to_int
@@ -1860,4 +2007,12 @@ test_branch_if_end_pops_frame
 test_branch_while_empty_body
 test_branch_frame_kind_dispatch
 test_branch_return_inside_if_restores_live
+test_array_literal_int_inference
+test_array_literal_str_inference
+test_array_literal_bool_inference
+test_array_literal_empty
+test_array_literal_empty_with_annotation
+test_array_literal_empty_with_cast_then_assign
+test_error_array_literal_heterogeneous
+test_error_array_literal_unresolved_assignment
 test_summary
diff --git a/tests/compiler/test_typeof.casa b/tests/compiler/test_typeof.casa
index ef10a70..eebc683 100644
--- a/tests/compiler/test_typeof.casa
+++ b/tests/compiler/test_typeof.casa
@@ -139,6 +139,13 @@ fn test_typecheck_typeof_ptr {
     "returns str" "str" 0 sig Signature::return_types.get assert_str_eq
 }
 
+fn test_typecheck_typeof_array {
+    "typecheck_typeof_array" test_start
+    "[1 2 3] typeof" tc_typeof = sig
+    "one return" 1 sig Signature::return_types.length assert_eq
+    "returns str" "str" 0 sig Signature::return_types.get assert_str_eq
+}
+
 # ============================================================================
 # Bytecode tests
 # ============================================================================
@@ -164,6 +171,12 @@ fn test_bytecode_typeof_str {
     "str in strings" "str" prog Program::strings string_table_contains assert_true
 }
 
+fn test_bytecode_typeof_array {
+    "bytecode_typeof_array" test_start
+    "[1 2 3] typeof" compile_typeof = prog
+    "array[int] in strings" "array[int]" prog Program::strings string_table_contains assert_true
+}
+
 fn test_bytecode_typeof_instruction_sequence {
     "bytecode_typeof_instruction_sequence" test_start
     "42 typeof" compile_typeof = prog
@@ -221,9 +234,11 @@ test_typecheck_typeof_returns_str_for_char
 test_typecheck_typeof_no_params
 test_typecheck_typeof_chained
 test_typecheck_typeof_ptr
+test_typecheck_typeof_array
 test_bytecode_typeof_int
 test_bytecode_typeof_bool
 test_bytecode_typeof_str
+test_bytecode_typeof_array
 test_bytecode_typeof_instruction_sequence
 test_emit_typeof_int
 test_emit_typeof_bool
diff --git a/tests/compiler/test_underflow_messages.casa b/tests/compiler/test_underflow_messages.casa
new file mode 100644
index 0000000..1c31b60
--- /dev/null
+++ b/tests/compiler/test_underflow_messages.casa
@@ -0,0 +1,95 @@
+import "../../compiler/common.casa"
+import "../../compiler/error.casa"
+import "../../compiler/lexer.casa"
+import "../../compiler/syntax.casa"
+import "../../compiler/typechecker.casa"
+import "../../lib/test.casa"
+
+# ============================================================================
+# Helper: lex + parse + resolve + typecheck a source string
+# ============================================================================
+
+fn tc_um code:str -> Signature {
+    clear_global_state
+    "test" code lex_source = tokens
+    tokens DEFAULT_PARSER parse_ops = ops
+    ops DEFAULT_PARSER resolve_identifiers_global = ops
+    Option::None(Option[Function]) ops type_check_ops
+}
+
+# ============================================================================
+# `print` underflow names the trait expectation as a value, not the trait
+# itself.
+# ============================================================================
+
+fn test_print_underflow_message_names_value_with_trait {
+    "print_underflow_message_names_value_with_trait" test_start
+    enable_test_mode
+    clear_global_state
+    clear_errors
+    "fn foo { print }\nfoo\n" tc_um drop
+    "has errors" assert_has_errors
+    "stack underflow kind" ErrorKind::StackUnderflow assert_error_kind
+    "names value with trait" "value with trait `Display`" assert_error_contains
+    clear_errors
+    disable_test_mode
+}
+
+# ============================================================================
+# `rot` underflow names the slot index of the missing argument.
+# ============================================================================
+
+fn test_rot_underflow_message_names_argument_slot {
+    "rot_underflow_message_names_argument_slot" test_start
+    enable_test_mode
+    clear_global_state
+    clear_errors
+    "fn foo { rot }\nfoo\n" tc_um drop
+    "has errors" assert_has_errors
+    "stack underflow kind" ErrorKind::StackUnderflow assert_error_kind
+    "names argument slot" "argument 1 of `rot`" assert_error_contains
+    clear_errors
+    disable_test_mode
+}
+
+# ============================================================================
+# `drop` underflow uses the singular "value for" phrasing.
+# ============================================================================
+
+fn test_drop_underflow_message_uses_singular_phrase {
+    "drop_underflow_message_uses_singular_phrase" test_start
+    enable_test_mode
+    clear_global_state
+    clear_errors
+    "fn foo { drop }\nfoo\n" tc_um drop
+    "has errors" assert_has_errors
+    "stack underflow kind" ErrorKind::StackUnderflow assert_error_kind
+    "names value for drop" "value for `drop`" assert_error_contains
+    clear_errors
+    disable_test_mode
+}
+
+# ============================================================================
+# Cascade slots show as `<missing>`, never the internal `<error>` token.
+# ============================================================================
+
+fn test_cascade_slot_renders_as_missing_token {
+    "cascade_slot_renders_as_missing_token" test_start
+    enable_test_mode
+    clear_global_state
+    clear_errors
+    "fn two_generics[T] a:T b:T {}\nfn foo { print 2 two_generics }\nfoo\n" tc_um drop
+    "has errors" assert_has_errors
+    "renders missing token" "<missing>" assert_error_contains
+    clear_errors
+    disable_test_mode
+}
+
+# ============================================================================
+# Run all tests
+# ============================================================================
+test_print_underflow_message_names_value_with_trait
+test_rot_underflow_message_names_argument_slot
+test_drop_underflow_message_uses_singular_phrase
+test_cascade_slot_renders_as_missing_token
+test_summary