App/Platform Return Type Not Fully Unified

[lukewilliamboswell]

Follow up from #8508

Issue: App/Platform Return Type Not Fully Unified

Summary

When an app defines main! returning a tag union (e.g., Ok({})), the function's return
type variable remains flex (unresolved) at the type-checking level, even though individual
expressions within the function body have concrete types. This causes issues during
interpreter execution when the interpreter tries to use the expected return type to
determine tag union layouts.

Reproduction

Minimal App

# hello.roc
app [main!] { pf: platform "..." }

import pf.Stdout

main! = |_args| {
    Stdout.line!("Hello, World!")
    Ok({})
}

Platform

# platform/main.roc
platform ""
    requires {} { main! : List Str => Try {} }
    exposes [Stdout]
    packages {}
    provides { main_for_host! }

main_for_host! = main!

The Issue

What Should Happen

1. Platform declares: main! : List Str => Try {}
2. App implements: main! = |_args| { ... Ok({}) }
3. Type checker should unify the lambda's return type with Try {}
4. Lambda's return type variable should resolve to Try {} (a tag union)

What Actually Happens

1. Platform declares: main! : List Str => Try {}
2. App implements: main! = |_args| { ... Ok({}) }
3. The Ok({}) expression gets type [Ok({})] (correct)
4. BUT the lambda's return type variable remains flex (unresolved)
5. When interpreter tries to use expected_rt_var (from function return type), it's flex
6. Interpreter crashes trying to get tag union layout from a flex type

Evidence

In the interpreter error message:

e_tag: expected tag_union but got rt=flex:n/a ct=structure has_expected=true for tag `Ok`

• rt=flex - The runtime type variable is flex (not resolved)
• ct=structure - The compile-time type of the expression IS correctly a structure (tag union)
• has_expected=true - An expected type WAS passed, but it's useless (flex)

Where to Investigate

1. src/check/Check.zig - Type Checking

Look at how e_lambda is type-checked (around line 3075):

• When checking a lambda, the expected type (from platform requires) should be used
• The lambda's return type should be unified with the expected function's return type
• Question: Is the platform's requires type being properly passed as expected when
  type-checking the app's main! definition?

2. src/check/Check.zig - e_lookup_required handling (around line 3035)

When the platform references main! from the app:

main_for_host! = main!  # This is e_lookup_required

• The app's main! type should be unified with the platform's declared type
• Question: Does this unification happen? Does it propagate back to the lambda's
  internal types?

3. Cross-Module Type Unification

The app and platform are separate modules. When type information crosses module boundaries:

• src/canonicalize/Can.zig - How are required values resolved?
• Question: When the app's main! is type-checked, does it know about the platform's
  expected type?

Current Workaround

In src/eval/interpreter.zig, the e_tag handler now checks if expected_rt_var is
concrete before using it:

var rt_var = blk: {
    if (expected_rt_var) |expected| {
        const expected_resolved = self.runtime_types.resolveVar(expected);
        // Use expected only if it's concrete (not flex)
        if (expected_resolved.desc.content == .structure or
            expected_resolved.desc.content == .alias)
        {
            break :blk expected;
        }
    }
    // Fall back to translating from compile-time type
    const ct_var = can.ModuleEnv.varFrom(expr_idx);
    break :blk try self.translateTypeVar(self.env, ct_var);
};

This is correct behavior (use ct_var when expected_rt_var is useless), but ideally
expected_rt_var should be concrete after proper type unification.

Why This Matters

1. Performance: Falling back to ct_var translation may be less efficient than using
   the already-translated expected_rt_var

2. Correctness for Polymorphism: In polymorphic cases like:

   identity = |x| x
   main! = identity(Ok({}))

   The call site needs to provide the concrete type - ct_var alone may not be enough.

3. Architecture: This suggests a gap in how type information flows between app and
   platform modules during type checking.

Questions for Investigation

1. When is the app type-checked relative to the platform? Are they checked in separate
   passes?

2. How does requires work? When the platform says requires { main! : T }, how does
   this constrain the app's main!?

3. Is there a unification step missing? When main_for_host! = main! is type-checked
   in the platform, does the unification propagate the concrete return type back into the
   app's lambda?

4. Is this a fundamental limitation of separate compilation? Or is there a way to
   ensure the app's types are fully resolved before the interpreter runs?

Related Files

• src/check/Check.zig - Main type checker
• src/canonicalize/Can.zig - Canonicalization, handles e_lookup_required
• src/eval/interpreter.zig - Interpreter, where the workaround was added (around line 8647)
• src/check/test/cross_module_test.zig - Existing cross-module type tests (good reference)