Reject multi-qubit arms under controlled(par)

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<Expr>) -> Option<SimpleSpan> {
+    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<Expr>) -> Option<SimpleSpan> {
+    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<Expr>) -> 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<Expr>,
     ) -> Result<Ty, TypeError> {
         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)),

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"

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]

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::<Vec<_>>()
         .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}"
     );
 }
 

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.