controlled(par{...}) target-count mismatch between typechecker and surface @ syntax

[arniber21]

This was generated by AI during triage.

Context

Split out of #368 during triage — a follow-up defect found by adversarial review of a par/qinit/formatter fix diff, distinct in scope and triage state from #368's init_one/init_plus gap.

controlled(par { ... }) target-count mismatch (pre-existing, widened by the par { c1, c2 } tensor form)

controlled(c) @ (control, target) is elaborated via decompose_controlled, which distributes control over Compose/CircuitBlock/Par/ParN arms. That elaboration path is correct. But the typechecker rejects controlled(par { H @0, H @0 }) @ (0, (1, 2)) with "this gate acts on 3 qubit(s), but 2 target(s) were given" — because controlled(c: Circuit<k,k,d,C>) is typed as Circuit<k+1, k+1, ...> (one control wire), so a 2-qubit par under control expects 3 targets, but the surface @(control, target) syntax only provides a single target (the 2-tuple (control, (t1, t2)) parses as 2 targets, not 3).

This is pre-existing for controlled(par { c } * k) (the repeated-body form) too; the par { c1, c2 } tensor form (ParN) makes it more reachable since it's a natural way to write multi-qubit bodies under control.

Demonstrated

fn ctrl_layer(): Circuit<3, 3, 2, Clifford> = circuit {
    (controlled(par { H @0, H @0 })) @(0, (1, 2))   -- type error: 3 qubits expected, 2 given
}

Why this needs a human, not an agent

This is a design decision with two divergent, both-valid resolutions:

1. Reconcile the typechecker's controlled target-counting with the surface @ syntax so multi-qubit bodies under controlled(...) typecheck as written (a language-design change to how @ arity is counted for controlled circuits).
2. Leave the typing rule as-is and instead reject controlled(par{...}) explicitly at parse/typecheck time with a clear diagnostic, documenting it as unsupported.

These have different implications for the surface language (option 1 changes what programs are accepted; option 2 forecloses a pattern users may reasonably expect to work) and should be decided by whoever owns the type system's design, not inferred by an agent. Whichever direction is chosen also needs to be coordinated with the existing controlled(par { c } * k) partial-support note, since the Par (repeat) arm in decompose_controlled has the same underlying issue.

Severity

Low-urgency: not hit by the documented par/qubit examples (all of which now compile end-to-end and are lit-tested). A forward-looking gap that will bite as par/controlled composition sees broader use.

Dependency note

At triage time, the ParN AST node and the decompose_controlled ParN arm this issue references exist only as uncommitted changes on main (not yet on any pushed branch or committed history) — this is not blocking triage, but whoever picks this up should confirm that work has landed first, since the repro depends on it.

References

• Investigation report: VQE H2 ground-state calculation (O'Malley 2016 parity-mapped Hamiltonian) — surfaced par/qinit/formatter gaps.
• Adversarial review of the fix diff.
• Split from init_one()/init_plus() typecheck but do not lower #368.