Proposal: Improve type inference of `if`/`switch` with comptime-known operand

[topolarity]

Problem

Comptime emulation will sometimes assign different types to the same syntax as runtime code:

A. if/switch don't perform peer type resolution for comptime arguments, affecting downstream code:

comptime { // works if we comment out `comptime`
    const base: usize = 15;
    var y: union(enum) { offset: usize, unknown: void } = .{ .offset = 12 };

    const maybe_x = switch(y) {
       .offset => |off| off + base,
       .unknown => null,
    };
    if (maybe_x) |x| { // error: expected optional type, found 'usize'
        ...
    }
}

B. In a comptime context, all tuple fields are all inferred to be comptime, making them suddenly immutable:

comptime { // works if we comment out `comptime`
    var x: usize = 1;
    var y = .{ x, x + 1 };
    y = .{ 3, 4 }; // error: value stored in comptime field does not match the default value of the field
}

(A) is particularly problematic, since it means that Zig cannot improve its semantic analysis like Andrews mentions here:

... zig reserves the right to make the if static if it can prove the value is compile-time known (which it should be able to do in this example with more sophisticated semantic analysis).

Unfortunately if we don't fix this problem, improving semantic analysis is a breaking change for users.

So what can be done about it?

Proposed solution

A value is "semantically comptime" if it is:

1. a literal constant, OR
2. labeled with comptime at its declaration site, OR
3. the result of a comptime ... expression, OR
4. the result of an operator/builtin with semantically comptime inputs, OR
5. a const whose initialization expression is semantically comptime

In a runtime context, all comptime-known values are also semantically comptime. However in a comptime context, there are values that are comptime-known but not semantically comptime. For example:

const x = comptime b: { // x is both comptime-known and semantically comptime
    var y: usize = 1; // comptime-known, but not semantically comptime
    break :b y;
};

A. Branching in switch/if

When branching on a comptime-known but not semantically comptime value in a switch/if/orelse/catch or a non-inline while/for, Sema must perform "runtime-equivalent analysis" as follows:

• Semantically comptime values (from before branch entry) are treated as immutable.
• Peer type resolution is performed the same way it would be at runtime.
• In dead branches:
  • Comptime-known, but not semantically comptime values are treated as runtime values.
  • No runtime code is generated during this analysis.

B. Tuple fields

Tuple fields should only be inferred to be comptime fields if they are initialized with a semantically comptime value.

This would resolve #12261. The existing tuple semantics also accidentally make the rejected #7539 implementable in userspace, which is resolved by this proposal.

[Vexu]

Related #5401

Regarding A., I would normally expect conditionals to work identically at runtime and comptime, except that there are cases, such as throwing a @compileError, where non-taken branches are to be explicitly ignored. Maybe it would pay off in clarity if we introduce inline if and inline switch, which require a comptime-known condition and are semantically guaranteed to be replaced by the taken branch -- without peer-type resolution or any other analysis of the non-taken branches. Ordinary conditionals, on the other hand, would become completely transparent with regard to runtime/comptime status.

[topolarity]

Updated the OP with some new requirements:

• Any existing comptime var are temporarily immutable within "runtime-equivalent" control flow, just like at runtime
• Dead branches introduced by non-inline for/while loops also undergo "runtime-equivalent analysis"

The first is necessary so that the value of the comptime variable is statically determined within the dead branch. It also means we only need to do "runtime-equivalent analysis" once per semantically comptime context.

The second is needed to make the following example work:

comptime { // works if we comment out `comptime`
  var i: usize = 0;
  const maybe_x = b: while (i < 3) : (i += 1) {
    if (i == 2)
      break :b @as(usize, 1);
  } else null; // never executes, so doesn't participate in peer type resolution
  
  if (maybe_x) |x| { // error: expected optional type, found 'usize'
     ...
  }
}

[topolarity]

Maybe it would pay off in clarity if we introduce inline if and inline switch, which require a comptime-known condition and are semantically guaranteed to be replaced by the taken branch

Yeah, I can definitely see the value in clarity here. Especially since a runtime-equivalent "if" means restricting comptime mutability, inline if is a nice way to explicitly opt-in to the comptime semantics.

In a comptime context, "inline if" can also support arguments that are not semantically comptime, so that this works:

comptime {
    var x: bool = true;
    inline if(x) { // `inline if` does not need its operand to be "semantically comptime"
        ...
    } else @compileError("x should be false!");
}

That said, inline if(x) is basically just equivalent to if(comptime x)

That said, inline if(x) is basically just equivalent to if(comptime x)

Not quite. Currently, if x is const or comptime var, then there is no way to opt out of the comptime semantics, and the comptime in if (comptime x) is redundant.

Quite generally, I'd be in favor of more explicitness when it comes to comptime behavior. Inferring "semantically comptime" status based on contextual clues saves characters, but takes up head space. Especially in advanced cases, such as mixed runtime/comptime control flow in inline loops, it becomes really difficult to figure out what is supposed to happen. Even in ordinary cases there is room for confusion, because const in Zig can mean either "runtime immutable" or "semantically comptime", and you may need to consider the wider context to determine which is which, and whether it was intended as such.

[topolarity]

It's worth mentioning that "semantically comptime" is still relevant even if we separate if vs. inline if:

comptime {
   var bits: usize = 8;
   
   var x: usize = 0;
   while (true) : (x += 1) {
      const z = switch (x) { // This is a "runtime-equivalent" switch statement
         0 => @as(u16, 1),
         1, 3 => @as(std.meta.Int(.unsigned, bits), 1), // Type of this branch depends on `bits`
         2 => {
             bits = 32;
             continue;
         },
         4 => break,
         else => unreachable,
      };
      // @TypeOf(z) is not stable across loop iterations.
      // Supporting this would mean extra algorithmic effort:
      //     1. Dead branches have to be re-analyzed on every loop iteration.
      //     2. Sema must fully evaluate all operations in each branch, rather
      //        than just the semantically-comptime operations.
      //     3. Sema has to make sure to isolate comptime mutations in each branch, 
      //        and then keep only the mutations from the surviving branch.
   }
}

To avoid all of the additional complexity, this scenario is not allowed under this proposal: bits is not a comptime var so it is not semantically comptime and is effectively runtime in the branch. If it were made a comptime var, then it wouldn't be mutable in the switch. Either way, this is a compile error.

On the other hand if the switch is effectively inline, then the dead branches don't matter and this code is fine as-is.

Point taken regarding explicitness, though. I agree that an explicit inline if/switch would make it clearer how evaluation works in mixed comptime/runtime code.

@topolarity, I'm not sure I understand the idea behind this example. If we wanted to perform peer-type resolution on the switch, e.g. on the first iteration with T == void, then we'd have to unify u8, FooType(void), void and noreturn. This fails of course, but simply because the types are incompatible, not because of mutable comptime weirdness. Or am I misunderstanding something?

fixed

[topolarity]

@zzyxyzz Sorry about that, the example was quite misleading. I've revised it to have compatible types, so hopefully it's clearer now.

My original thought was that the switch would be required to have type that is stable across (non-inline) loop iterations, which is clearly impossible in this case.

After thinking about it a bit more, I think it's probably consistent to allow this type to vary across iterations after all. However, it comes at a significant cost w.r.t. performance and implementation complexity. Overall, my recommendation is that we prohibit these scenarios, especially since they have no runtime equivalent

[InKryption]

Would this code cease to be valid?

const foo: [3]u8 = blk: {
    var bar: []const u8 = "baz";
    break :blk bar[0..bar.len].*;
};

By the way,

The existing tuple semantics also accidentally make the rejected #7539 implementable in userspace, which is resolved by this proposal.

In fairness, this isn't specific to the tuple semantics, you can achieve a similar effect with the aforementioned wonky type resolution:

fn weAreInComptime() bool {
    var cond = false;
    const a = if (cond) @as(u32, 1) else null;
    return @TypeOf(a) == @TypeOf(null);
}

(Worked Last Time I Checked:tm:)

[topolarity]

Would this code cease to be valid?

const foo: [3]u8 = blk: {
    var bar: []const u8 = "baz";
    break :blk bar[0..bar.len].*;
};

Still valid - but it would behave slightly differently than today in a comptime context.

The rule of thumb is that this proposal doesn't change the comptime-ness of values in a runtime context, it just changes the behavior in a comptime context to match the runtime behavior.

In this case, the code works at runtime if you change it to break :blk bar[0..3].*;, but foo is not a comptime value. This proposal makes it behave the same way (with or without the edit) at comptime. In a comptime context, foo is compile-time-known, but not semantically comptime.