diff --git a/frontend/src/typecheck/circuit.rs b/frontend/src/typecheck/circuit.rs index 08f9a79..ad8f736 100644 --- a/frontend/src/typecheck/circuit.rs +++ b/frontend/src/typecheck/circuit.rs @@ -198,6 +198,87 @@ fn controlled_placement<'a>( })) } +/// A multi-qubit gate inside a `par` arm of `controlled`. +/// +/// `controlled_named_gate` rejects a tuple target with +/// `controlled() of a multi-qubit gate`. Width-1 arms (`H @0`) are not +/// reported here. +fn par_arm_multiqubit_gate(expr: &Sp) -> Option { + match &expr.0 { + Expr::Par(body, _) => multiqubit_gate(body), + Expr::ParN(elems) => elems.iter().find_map(multiqubit_gate), + Expr::Compose(lhs, rhs) => { + par_arm_multiqubit_gate(lhs).or_else(|| par_arm_multiqubit_gate(rhs)) + } + Expr::Adjoint(inner) => par_arm_multiqubit_gate(inner), + Expr::CircuitBlock(stmts) => stmts.iter().find_map(|stmt| match &stmt.0 { + Stmt::Expr(e) | Stmt::Let { rhs: e, .. } | Stmt::Bind { rhs: e, .. } => { + par_arm_multiqubit_gate(e) + } + }), + Expr::Let { rhs, body, .. } => { + par_arm_multiqubit_gate(rhs).or_else(|| par_arm_multiqubit_gate(body)) + } + _ => None, + } +} + +/// A surface gate that occupies more than one qubit, or a placement whose +/// target list does. +fn multiqubit_gate(expr: &Sp) -> Option { + match &expr.0 { + Expr::GateApp { gate, qubits } => { + let targets = match &qubits.0 { + Expr::Tuple(items) => items.len(), + _ => 1, + }; + if gate_surface_arity(gate) > 1 || targets > 1 { + Some(qubits.1) + } else { + None + } + } + Expr::Var(name) => { + surface_gate(name).and_then(|info| if info.arity > 1 { Some(expr.1) } else { None }) + } + Expr::App(f, x) => { + let (head, _) = flatten_app(f, x); + match &head.0 { + Expr::Var(name) if surface_gate(name).is_some_and(|info| info.arity > 1) => { + Some(expr.1) + } + _ => None, + } + } + Expr::Compose(lhs, rhs) => multiqubit_gate(lhs).or_else(|| multiqubit_gate(rhs)), + Expr::Adjoint(inner) | Expr::Controlled(inner) => multiqubit_gate(inner), + Expr::Par(body, _) => multiqubit_gate(body), + Expr::ParN(elems) => elems.iter().find_map(multiqubit_gate), + Expr::CircuitBlock(stmts) => stmts.iter().find_map(|stmt| match &stmt.0 { + Stmt::Expr(e) | Stmt::Let { rhs: e, .. } | Stmt::Bind { rhs: e, .. } => { + multiqubit_gate(e) + } + }), + Expr::Let { rhs, body, .. } => multiqubit_gate(rhs).or_else(|| multiqubit_gate(body)), + _ => None, + } +} + +fn gate_surface_arity(gate: &Sp) -> usize { + let name = match &gate.0 { + Expr::Var(name) => name.as_str(), + Expr::App(f, x) => { + let (head, _) = flatten_app(f, x); + let Expr::Var(name) = &head.0 else { + return 1; + }; + name.as_str() + } + _ => return 1, + }; + surface_gate(name).map(|info| info.arity).unwrap_or(1) +} + impl super::TypeChecker { /// View `ty` as a circuit, returning its four indices. fn as_circuit( @@ -567,6 +648,12 @@ impl super::TypeChecker { c: &Sp, ) -> Result { let ct = self.synth(env, delta, c)?; + // A multi-qubit gate in a `par` arm (`CNOT @(0, 1)`) has a matching wire + // count, so placement succeeds, then `controlled_named_gate` rejects the + // tuple target. Report that error here. + if let Some(span) = par_arm_multiqubit_gate(c) { + return Err(TypeError::ControlledMultiQubitGate { span }); + } let (n, m, d, cl) = self.as_circuit(&ct, c.1)?; Ok(Ty::Circuit { n: n.seq(DepthExpr::Nat(1)), diff --git a/frontend/src/typecheck/error.rs b/frontend/src/typecheck/error.rs index b80712a..d8b3f21 100644 --- a/frontend/src/typecheck/error.rs +++ b/frontend/src/typecheck/error.rs @@ -206,6 +206,10 @@ pub enum TypeError { /// `start + i` is bounds-checked, and elaboration only shifts `Expr::Int`. /// A symbolic start would leave every arm on `start` and skip the width check. NonLiteralControlledStart { span: SimpleSpan }, + /// A `par` arm under `controlled` is a multi-qubit gate. Elaboration's + /// `controlled_named_gate` rejects that shape; the checker reports the same + /// diagnostic so the program does not typecheck and then fail later. + ControlledMultiQubitGate { span: SimpleSpan }, /// A construct that belongs to the linear/quantum fragment (issues #10–#15) was /// encountered while type-checking the classical fragment. Unsupported { @@ -256,6 +260,7 @@ impl TypeError { | TypeError::QecCtorRequiresDistance { span, .. } | TypeError::NonLiteralQecDistance { span } | TypeError::NonLiteralControlledStart { span } + | TypeError::ControlledMultiQubitGate { span } | TypeError::Unsupported { span, .. } => *span, } } @@ -303,6 +308,7 @@ impl TypeError { TypeError::QecCtorRequiresDistance { .. } => DiagnosticCode::QEC_CTOR_REQUIRES_DISTANCE, TypeError::NonLiteralQecDistance { .. } => DiagnosticCode::QEC_NON_LITERAL_DISTANCE, TypeError::NonLiteralControlledStart { .. } => DiagnosticCode::CIRCUIT_GATE_TARGET, + TypeError::ControlledMultiQubitGate { .. } => DiagnosticCode::UNSUPPORTED_QUANTUM, TypeError::Unsupported { .. } => DiagnosticCode::UNSUPPORTED_QUANTUM, } } @@ -534,6 +540,11 @@ impl fmt::Display for TypeError { f, "controlled(par) @(control, start) requires a non-negative literal start index" ), + // Same wording as `ElabError` for `controlled_named_gate`'s tuple target. + TypeError::ControlledMultiQubitGate { .. } => write!( + f, + "elaboration is not implemented for `controlled() of a multi-qubit gate`" + ), TypeError::Unsupported { construct, .. } => write!( f, "`{construct}` is part of the linear/quantum fragment and is not yet type-checked" diff --git a/frontend/src/typecheck/tests.rs b/frontend/src/typecheck/tests.rs index dd4e23c..bc4f24c 100644 --- a/frontend/src/typecheck/tests.rs +++ b/frontend/src/typecheck/tests.rs @@ -833,14 +833,33 @@ fn controlled_par_start_past_register_is_out_of_bounds() { } #[test] -fn controlled_par_multiqubit_arm_typechecks() { - // Width matches (control + the CNOT's two wires), so the checker accepts - // it. Elaboration still rejects the multi-qubit arm; see lower.rs. - accepts( +fn controlled_par_multiqubit_arm_is_rejected() { + // Same diagnostic `controlled_named_gate` raises for a tuple target. + // The wire count matches, so this used to typecheck and fail in elaboration. + let err = reject_err( "fn f(): Circuit<3, 3, 2, Clifford> = circuit {\n\ controlled(par { CNOT @(0, 1) }) @(0, (1, 2))\n\ }", ); + assert!( + matches!(err, TypeError::ControlledMultiQubitGate { .. }), + "got {err:?}" + ); + let msg = err.to_string(); + assert!(msg.contains("controlled() of a multi-qubit gate"), "{msg}"); +} + +#[test] +fn controlled_par_repeat_multiqubit_arm_is_rejected() { + let err = reject_err( + "fn f(): Circuit<5, 5, 2, Clifford> = circuit {\n\ + controlled(par { CNOT @(0, 1) } * 2) @(0, (1, 2, 3, 4))\n\ + }", + ); + assert!( + matches!(err, TypeError::ControlledMultiQubitGate { .. }), + "got {err:?}" + ); } #[test] diff --git a/frontend/tests/lower.rs b/frontend/tests/lower.rs index 5caa158..6a58091 100644 --- a/frontend/tests/lower.rs +++ b/frontend/tests/lower.rs @@ -217,6 +217,8 @@ fn controlled_par_nested_targets_lower() { #[test] fn controlled_par_multiqubit_arm_does_not_lower() { + // Rejected at typecheck with the same diagnostic `controlled_named_gate` + // uses, so lowering never sees the multi-qubit arm. let src = "\ fn f(): Circuit<3, 3, 2, Clifford> = circuit { controlled(par { CNOT @(0, 1) }) @(0, (1, 2)) @@ -230,8 +232,8 @@ fn f(): Circuit<3, 3, 2, Clifford> = circuit { .collect::>() .join("\n"); assert!( - text.contains("multi-qubit"), - "expected a multi-qubit elaboration failure, got {text}" + text.contains("controlled() of a multi-qubit gate"), + "expected the controlled_named_gate diagnostic, got {text}" ); } diff --git a/website/src/content/docs/reference/support-matrix.md b/website/src/content/docs/reference/support-matrix.md index 20b8b89..41c49bc 100644 --- a/website/src/content/docs/reference/support-matrix.md +++ b/website/src/content/docs/reference/support-matrix.md @@ -62,7 +62,7 @@ issue's original framing. | `adjoint(c)` | ✓ | ✓ | ✓ | ✓ | — | `qc::adjoint` of zero-arg callees | | `repeat(k, c)` (concrete & symbolic count) | ✓ | ✓ | ✓ | ✓ | — | Grover/QFT fixtures | | `controlled(named_gate)` / `controlled(Rz(θ))` | ✓ | ✓ | ✓ | ✓ | — | Distributed via `decompose_controlled` | -| `controlled(par { … })` / `controlled(par { c } * k)` | ✓ | ◐ | ◐ | ◐ | — | Width-1 arms with a literal start lower to MLIR only; no lit or neutral-atom fixture. Multi-qubit arms typecheck, then fail elaboration. See [#369](#known-limitations) | +| `controlled(par { … })` / `controlled(par { c } * k)` | ✓ | ◐ | ◐ | ◐ | — | Width-1 arms with a literal start lower to MLIR only; no lit or neutral-atom fixture. A multi-qubit arm is a type error (`controlled() of a multi-qubit gate`). See [#369](#known-limitations) | | `controlled(user_parametric_circuit)` | ✓ | ✓ | ✗ | ✗ | — | Elaboration not implemented; see [#374](#known-limitations) | | Parametric circuits (`Nat` params, `for`, `match`) | ✓ | ✓ | ✓ | ✓ | — | Specialized at call sites | @@ -460,8 +460,9 @@ the only documentation — the row above states the current behavior. Those lower to `quantum.circ` (`frontend/tests/lower.rs`). There is no `test/lit` OpenQASM fixture and no neutral-atom fixture, so QASM and NA stay partial. A multi-qubit arm such as - `controlled(par { CNOT @(0, 1) }) @(0, (1, 2))` typechecks and then fails - elaboration (`controlled() of a multi-qubit gate`). A non-literal start is + `controlled(par { CNOT @(0, 1) }) @(0, (1, 2))` is rejected at typecheck + with the same diagnostic as `controlled_named_gate`: + `controlled() of a multi-qubit gate`. A non-literal start is rejected: implied wires would not be bounds-checked, and elaboration only shifts integer literals.