[Bug]: comptime function type checks but returns typing error on compilation

[bhayat-quantinuum]

Description

from typing import Callable
from guppylang import guppy

from guppylang.std.builtins import array, qubit, owned, comptime

n_qubits = 0
n_predicates = 0
predicates = []

@guppy.comptime
def comptime_predicates() -> array[
    tuple[
        Callable[[array[qubit, comptime(n_qubits)]], qubit],
        Callable[
            [array[qubit, comptime(n_qubits)], qubit @ owned],
            None,
        ],
    ],
    comptime(n_predicates),
]:
    result : array[
        tuple[
            Callable[[array[qubit, comptime(n_qubits)]], qubit],
            Callable[
                [array[qubit, comptime(n_qubits)], qubit @ owned],
                None,
            ],
        ],
        comptime(n_predicates),
    ] = array(predicate
     for predicate in predicates)
    return result

comptime_predicates.check()
comptime_predicates.compile()

The code above type checks, but then raises a typing error at compilation time.

Steps to Reproduce

Run code above

Expected Behaviour

Should fail at type checking or pass compilation.

Ideally, if it does fail type checking, the error message should be clearer.

Actual Behaviour

Passes type checking, but fails compilation.

Component

No response

Environment

- guppylang version: 0.21.16
- Python version: 3.13

Additional Context

No response

[ss2165]

This is expected behaviour I think - comptime functions are only traced (python evaluated) at compile time, so type errors inferrable only after tracing are only catchable then. We likely need to improve our comptime documentation around this.