Referring to `comptime let` values in non-comptime code results in ICE

[TomAFrench]

I would expect that I would be able to reference a comptime let value in non-comptime code as below.

fn main() {
    comptime let comptime_bool: bool = true;

    assert(comptime_bool)
}

Compiling this program fails with the result

$ nargo compile
error: ICE: Variable not found during monomorphization
  ┌─ src/main.nr:4:12
  │
4 │     assert(comptime_bool)
  │            -------------
  │
  = Call stack:
    1. src/main.nr:4:12

Aborting due to 1 previous error

[asterite]

I think in this case the compiler should error? For example as a comptime value you can have Quoted:

fn main() {
    comptime let x: Quoted = quote { 1 };
}

but it's an error to have Quoted in runtime code:

fn main() {
    let x: Quoted = quote { 1 };
}

error:

error: Comptime-only type `Quoted` cannot be used in runtime code
  ┌─ src/main.nr:2:12
  │
2 │     let x: Quoted = quote { 1 };
  │            ------ Comptime-only type used here

So my understanding is that comptime lets should only be visible at comptime, never at runtime. @jfecher is that the intention?

[TomAFrench]

Yeah, I wasn't entirely sure on whether we wanted to allow comptime let of valid runtime types to be used in a runtime context.

I think in the case where we don't want this to be possible then we should improve the error message from an ICE to something akin to what we get when attempting to use a runtime value in a comptime block.

[jfecher]

Runtime code referring to a comptime let variable should be fine, we just need to ensure the value goes through lowering. We do this already for the values returned by comptime blocks so it looks like we're just missing a check on comptime variables to do the same there.

I'd expect Tom's program to work and Ary's to still error since we can't lower a Quoted value without a macro. That should be something we test for as well. I'm not actually sure if we have a test that ensures comptime { quote[1] } errors correctly instead of inlining 1 as a macro.

[asterite]

Should this program be valid? If so, what's the output?

fn main() {
    comptime let mut x = 1;

    println(x);

    comptime {
        x += 1;
    }

    println(x);
}

[TomAFrench]

I would expect this program to be valid and produce the output

2
2

All comptime code should be resolved before we process the runtime printlns so they all receive the final value of x

[asterite]

Out of curiosity, what's the purpose of comptime let? I can't see it being used in the standard library nor in Aztec-Packages. Of course that doesn't mean it's not useful, but I wonder what's the point of having that when you can do let ... = comptime { ... } to compute a value at comptime. I can imagine maybe you could use a comptime let for an array length? Though if you are in a comptime context I think you could always unquote a comptime value inside an array, like quote { [0; $length] }.

[jfecher]

I'd expect that program to output 1, 2 since we don't resolve all comptime code before runtime code. It's true that the actual printlns are executed at runtime but we resolve a function's body in order and execute a comptime block whenever we see it.

When you change it to this program:

fn main() {
    comptime let mut x = 1;

    println(comptime { x });

    comptime {
        x += 1;
    }

    println(comptime { x });
}

It works and does print 1 then 2

[jfecher]

Out of curiosity, what's the purpose of comptime let?

We support a few comptime <keyword>s that are generally just sugar for comptime { <keyword> .. }, possibly with a few changes. E.g. comptime global and comptime for.

I think the only case where comptime let differs from let _ = comptime { ... } is in the case Tom mentioned where it is mutated at comptime.

[asterite]

I also think it's easier for the output to be 1, then 2. Looking at the code, whenever a comptime value is used at runtime (like the result of a comptime block) the value is immediately inlined into the final program. Otherwise we'd have to inline a reference to the comptime value and just use the final value at the end.