diff --git a/website/docs/tensor-shapes-ai-porting.mdx b/website/docs/tensor-shapes-ai-porting.mdx
index 0d4d4c3047..3b35d02c1a 100644
--- a/website/docs/tensor-shapes-ai-porting.mdx
+++ b/website/docs/tensor-shapes-ai-porting.mdx
@@ -84,7 +84,7 @@ The skill produces a `verify_port.sh` report with these key metrics:
 | **`ig` (ignore)** | `type: ignore` comments. Lower is better. Each should have a category (algebraic gap, conditional equality, stub gap). |
 | **`bs` (bare sig)** | Bare `Tensor` in function signatures. Should be 0 for well-typed modules. |
 | **`bv` (bare var)** | Bare `Tensor` in local variable annotations. Lower is better. |
-| **`sh` (shaped)** | `assert_type` calls with full shapes (e.g., `Tensor[B, D]`). Higher is better. |
+| **`sh` (shaped)** | `assert_type` calls with full shapes (e.g., `Tensor[[B, D]]`). Higher is better. |
 | **`ba` (bare assert)** | `assert_type(x, Tensor)` — tracking gaps. Lower is better. Each should have a root-cause comment. |
 | **`sm` (smoke)** | Smoke test functions. At least 1-2 per model. |
 
diff --git a/website/docs/tensor-shapes-reference.mdx b/website/docs/tensor-shapes-reference.mdx
index 1dabf5b0e6..3740f2b0a2 100644
--- a/website/docs/tensor-shapes-reference.mdx
+++ b/website/docs/tensor-shapes-reference.mdx
@@ -23,7 +23,11 @@ description: Experiment with Int operators, type-level arithmetic in shapes, and
 ## `Int[X]`
 
 `Int[X]` is a type constructor that bridges runtime integer values to
-type-level symbols. It is defined in the `shape_extensions` package.
+type-level symbols. It is defined in the `shape_extensions` package,
+alongside the other names used throughout this page: `IntVar` (the bound
+for shape type parameters), `IntTuple` (the bound for whole-shape type
+parameters), and `Elements` (splices a whole-shape type parameter into a
+`Tensor` argument list).
 
 ### Basics
 
@@ -61,11 +65,11 @@ For optional dimensions — parameters that may or may not be present — use
 `if param is not None:` to recover `Int[X]` inside the branch:
 
 ```python
-class Attention[D, RK](nn.Module):
+class Attention[D: IntVar, RK: IntVar](nn.Module):
     def __init__(self, dim: Int[D], rank_k: Int[RK] | None = None):
         ...
 
-    def forward[B, T](self, x: Tensor[B, T, D]) -> Tensor[B, T, D]:
+    def forward[B: IntVar, T: IntVar](self, x: Tensor[[B, T, D]]) -> Tensor[[B, T, D]]:
         if self.rank_k is not None:
             # rank_k is Int[RK] here
             ...
@@ -76,11 +80,11 @@ class Attention[D, RK](nn.Module):
 | Pattern | Purpose |
 |---------|---------|
 | `def __init__(self, dim: Int[D])` | Accept a dimension as a constructor parameter |
-| `class Model[D](nn.Module)` | Make a dimension a class-level type parameter |
-| `def forward[B](self, x: Tensor[B, D])` | Bind a per-call dimension |
+| `class Model[D: IntVar](nn.Module)` | Make a dimension a class-level type parameter |
+| `def forward[B: IntVar](self, x: Tensor[[B, D]])` | Bind a per-call dimension |
 | `self.head_dim = dim // n_head` | Compute a derived dimension (`Int[D // NHead]`) |
 
-## `Tensor[D1, D2, ...]`
+## `Tensor[[D1, D2, ...]]`
 
 `Tensor` with type arguments represents a tensor with a known shape. The
 type arguments are the dimensions, in order.
@@ -89,19 +93,20 @@ type arguments are the dimensions, in order.
 
 | Form | Meaning |
 |------|---------|
-| `Tensor[3, 4]` | Concrete 2D tensor with shape `(3, 4)` |
-| `Tensor[B, C, H, W]` | Generic 4D tensor with symbolic dimensions |
-| `Tensor[B, 3 * C, H // 2]` | Dimensions can contain arithmetic expressions |
-| `Tensor[*Bs, D]` | Variadic: any number of leading batch dimensions |
+| `Tensor[[3, 4]]` | Concrete 2D tensor with shape `(3, 4)` |
+| `Tensor[[B, C, H, W]]` | Generic 4D tensor with symbolic dimensions |
+| `Tensor[[B, 3 * C, H // 2]]` | Dimensions can contain arithmetic expressions |
+| `Tensor[[*Elements[Bs], D]]` | Variadic: any number of leading batch dimensions (`Bs: IntTuple`) |
 | `Tensor` (bare) | Shape unknown — tracking gap |
 
-### Variadic dimensions with `*Bs`
+### Variadic dimensions with `Elements`
 
-Use `TypeVarTuple` (or PEP 646 `*Bs` syntax) for dimensions that should be
-propagated without being enumerated:
+Use a type parameter bound to `IntTuple`, spliced into the shape list with
+`*Elements[...]`, for dimensions that should be propagated without being
+enumerated:
 
 ```python
-def forward[*Bs](self, x: Tensor[*Bs, InDim]) -> Tensor[*Bs, OutDim]:
+def forward[Bs: IntTuple](self, x: Tensor[[*Elements[Bs], InDim]]) -> Tensor[[*Elements[Bs], OutDim]]:
     ...
 ```
 
@@ -109,11 +114,12 @@ This accepts any number of leading dimensions (batch, sequence, etc.) and
 preserves them in the output.
 
 **Don't hide known class dims inside variadic params.** If the module has a
-class-level Int `D`, use `Tensor[*Bs, D]` not `Tensor[*S]`.
+class-level Int `D`, use `Tensor[[*Elements[Bs], D]]` not folding `D` into
+the variadic carrier itself.
 
 ### `.shape` and `.size()`
 
-When `x: Tensor[B, C, H, W]`:
+When `x: Tensor[[B, C, H, W]]`:
 
 - `x.shape` has type `tuple[Int[B], Int[C], Int[H], Int[W]]`
 - `x.size(0)` has type `Int[B]`
@@ -130,7 +136,7 @@ reports an error.
 
 ```python
 h = self.fc1(x)
-assert_type(h, Tensor[B, 512])  # checked by pyrefly
+assert_type(h, Tensor[[B, 512]])  # checked by pyrefly
 ```
 
 Use `assert_type` during development to verify inferred shapes as you port
@@ -161,7 +167,7 @@ Use it to understand what pyrefly infers before writing `assert_type`:
 
 ```python
 h = self.fc1(x)
-reveal_type(h)  # Revealed type: Tensor[B, 512]
+reveal_type(h)  # Revealed type: Tensor[[B, 512]]
 ```
 
 Replace `reveal_type` with `assert_type` once you know the expected type.
@@ -172,11 +178,11 @@ Annotations can contain arithmetic on type parameters and literals:
 
 | Expression | Example |
 |-----------|---------|
-| Addition | `Tensor[B, C1 + C2, H, W]` — concatenation |
-| Subtraction | `Tensor[B, T, D - 1]` |
-| Multiplication | `Tensor[B, NHead * DK]` — multi-head reshape |
-| Floor division | `Tensor[B, NHead, T, D // NHead]` |
-| Exponentiation | `Tensor[B, C * 2 ** I, H // 2 ** I]` |
+| Addition | `Tensor[[B, C1 + C2, H, W]]` — concatenation |
+| Subtraction | `Tensor[[B, T, D - 1]]` |
+| Multiplication | `Tensor[[B, NHead * DK]]` — multi-head reshape |
+| Floor division | `Tensor[[B, NHead, T, D // NHead]]` |
+| Exponentiation | `Tensor[[B, C * 2 ** I, H // 2 ** I]]` |
 
 ### Simplification rules
 
@@ -201,7 +207,7 @@ When annotating local variables, choose from most to least desirable:
 
 1. **`assert_type`** — verifies the checker's inference. Proves the system
    works, not just that you annotated correctly.
-2. **Annotation fallback** — `x: Tensor[B, C, H, W] = untracked_op(...)`.
+2. **Annotation fallback** — `x: Tensor[[B, C, H, W]] = untracked_op(...)`.
    The checker can't infer the shape, but the annotation is compatible.
    Document WHY.
 3. **`type: ignore`** — the checker produces a WRONG type (algebraic gap).
@@ -216,8 +222,8 @@ annotations as an alternative front-end:
 
 | Pyrefly native | Jaxtyping equivalent |
 |---------------|---------------------|
-| `Tensor[M, 2, M // 2]` | `Shaped[Tensor, "M 2 M//2"]` |
-| `Tensor[B, C, H, W]` | `Shaped[Tensor, "B C H W"]` |
+| `Tensor[[M, 2, M // 2]]` | `Shaped[Tensor, "M 2 M//2"]` |
+| `Tensor[[B, C, H, W]]` | `Shaped[Tensor, "B C H W"]` |
 
 Jaxtyping annotations are translated internally to generics and display
 back in jaxtyping syntax. Note that jaxtyping cannot share symbolic
diff --git a/website/docs/tensor-shapes-tutorial-advanced.mdx b/website/docs/tensor-shapes-tutorial-advanced.mdx
index 426d9c143b..7bf8b2434e 100644
--- a/website/docs/tensor-shapes-tutorial-advanced.mdx
+++ b/website/docs/tensor-shapes-tutorial-advanced.mdx
@@ -24,7 +24,7 @@ modules, make it generic so dimensions propagate through constructors:
 
 ```python
 @dataclass
-class GPTConfig[VocabSize, BlockSize, NEmbedding, NHead, NLayer]:
+class GPTConfig[VocabSize: IntVar, BlockSize: IntVar, NEmbedding: IntVar, NHead: IntVar, NLayer: IntVar]:
     block_size: Int[BlockSize]
     vocab_size: Int[VocabSize]
     n_layer: Int[NLayer]
@@ -37,17 +37,17 @@ class GPTConfig[VocabSize, BlockSize, NEmbedding, NHead, NLayer]:
 Modules extract only the type parameters they need, using `Any` for the rest:
 
 ```python
-class MLP[NEmbedding](nn.Module):
+class MLP[NEmbedding: IntVar](nn.Module):
     def __init__(self, config: GPTConfig[Any, Any, NEmbedding, Any, Any]):
         super().__init__()
         self.c_fc = nn.Linear(config.n_embd, 4 * config.n_embd)
         self.c_proj = nn.Linear(4 * config.n_embd, config.n_embd)
 
-    def forward[B, T](
-        self, x: Tensor[B, T, NEmbedding]
-    ) -> Tensor[B, T, NEmbedding]:
+    def forward[B: IntVar, T: IntVar](
+        self, x: Tensor[[B, T, NEmbedding]]
+    ) -> Tensor[[B, T, NEmbedding]]:
         h = F.gelu(self.c_fc(x))
-        assert_type(h, Tensor[B, T, 4 * NEmbedding])
+        assert_type(h, Tensor[[B, T, 4 * NEmbedding]])
         return self.c_proj(h)
 ```
 
@@ -101,7 +101,7 @@ remain grouped:
 self.fc1 = nn.Linear(dim, hidden)
 self.fc2 = nn.Linear(hidden, dim)
 
-def forward[B](self, x: Tensor[B, D]) -> Tensor[B, D]:
+def forward[B: IntVar](self, x: Tensor[[B, D]]) -> Tensor[[B, D]]:
     h = F.relu(self.fc1(x))
     return self.fc2(h)
 ```
@@ -124,16 +124,16 @@ Fix: use a class with a typed `forward` method:
 
 ```python
 # Good: class preserves shape contract
-class Block[InC, OutC](nn.Module):
+class Block[InC: IntVar, OutC: IntVar](nn.Module):
     def __init__(self, in_c: Int[InC], out_c: Int[OutC]) -> None:
         super().__init__()
         self.net = nn.Sequential(
             nn.Conv2d(in_c, 128, ...), nn.Conv2d(128, out_c, ...)
         )
 
-    def forward[B, H, W](
-        self, x: Tensor[B, InC, H, W]
-    ) -> Tensor[B, OutC, H, W]:
+    def forward[B: IntVar, H: IntVar, W: IntVar](
+        self, x: Tensor[[B, InC, H, W]]
+    ) -> Tensor[[B, OutC, H, W]]:
         return self.net(x)
 ```
 
@@ -150,7 +150,7 @@ Fix: add an explicit `Int` field to the config:
 
 ```python
 @dataclass
-class Config[K, MlpOut]:
+class Config[K: IntVar, MlpOut: IntVar]:
     num_output_features: Int[K]
     mlp_output_dim: Int[MlpOut]        # explicit — was hidden_units[-1]
     mlp_hidden_units: list[int] = field(default_factory=lambda: [512, 256])
@@ -163,7 +163,7 @@ resort is a **typed interface**: the module's `forward` signature provides
 the shape contract, and `type: ignore` narrows the internal result:
 
 ```python
-class DynamicMLP[InDim, OutDim](nn.Module):
+class DynamicMLP[InDim: IntVar, OutDim: IntVar](nn.Module):
     def __init__(self, in_dim: Int[InDim], out_dim: Int[OutDim],
                  hidden: list[int]) -> None:
         super().__init__()
@@ -175,15 +175,15 @@ class DynamicMLP[InDim, OutDim](nn.Module):
         layers.append(nn.Linear(prev, out_dim))
         self.layers = nn.ModuleList(layers)
 
-    def forward[B](self, x: Tensor[B, InDim]) -> Tensor[B, OutDim]:
+    def forward[B: IntVar](self, x: Tensor[[B, InDim]]) -> Tensor[[B, OutDim]]:
         h = x
         for layer in self.layers:
             h = layer(h)
-        result: Tensor[B, OutDim] = h  # type: ignore[bad-assignment]
+        result: Tensor[[B, OutDim]] = h  # type: ignore[bad-assignment]
         return result
 ```
 
-The caller sees a clean `Tensor[B, InDim] -> Tensor[B, OutDim]` contract.
+The caller sees a clean `Tensor[[B, InDim]] -> Tensor[[B, OutDim]]` contract.
 The `type: ignore` is localized to the module's internals.
 
 Use typed interfaces only after exhausting all restructuring options —
diff --git a/website/docs/tensor-shapes-tutorial-architectures.mdx b/website/docs/tensor-shapes-tutorial-architectures.mdx
index fd0b484a55..b98c86409b 100644
--- a/website/docs/tensor-shapes-tutorial-architectures.mdx
+++ b/website/docs/tensor-shapes-tutorial-architectures.mdx
@@ -42,27 +42,27 @@ This gives a recursive signature where `recurse` takes and returns the same
 shape:
 
 ```python
-class UNet[NChannels, NClasses](nn.Module):
-    def _encode[B, C, H, W](
-        self, x: Tensor[B, C, H, W], depth: int
-    ) -> Tensor[B, 2 * C, (H - 2) // 2 + 1, (W - 2) // 2 + 1]:
+class UNet[NChannels: IntVar, NClasses: IntVar](nn.Module):
+    def _encode[B: IntVar, C: IntVar, H: IntVar, W: IntVar](
+        self, x: Tensor[[B, C, H, W]], depth: int
+    ) -> Tensor[[B, 2 * C, (H - 2) // 2 + 1, (W - 2) // 2 + 1]]:
         idx = len(self.downs) - depth
         down: Down[C, 2 * C] = self.downs[idx]
         return down(x)
 
-    def _decode[B, C, H, W](
+    def _decode[B: IntVar, C: IntVar, H: IntVar, W: IntVar](
         self,
-        skip: Tensor[B, C, H, W],
-        deep: Tensor[B, 2 * C, (H - 2) // 2 + 1, (W - 2) // 2 + 1],
+        skip: Tensor[[B, C, H, W]],
+        deep: Tensor[[B, 2 * C, (H - 2) // 2 + 1, (W - 2) // 2 + 1]],
         depth: int,
-    ) -> Tensor[B, C, H, W]:
+    ) -> Tensor[[B, C, H, W]]:
         idx = len(self.ups) - depth
         up: Up[2 * C, C] = self.ups[idx]
         return up(deep, skip)
 
-    def recurse[I, B, C, H, W](
-        self, x: Tensor[B, C, H, W], depth: Int[I]
-    ) -> Tensor[B, C, H, W]:
+    def recurse[I: IntVar, B: IntVar, C: IntVar, H: IntVar, W: IntVar](
+        self, x: Tensor[[B, C, H, W]], depth: Int[I]
+    ) -> Tensor[[B, C, H, W]]:
         if depth == 0:
             return x
         skip = x
@@ -111,27 +111,27 @@ Use `@overload` to separate the base case from the recursive case:
 
 ```python
 class Generator(nn.Module):
-    def _apply_stage[B, C, H, W](
-        self, x: Tensor[B, C, H, W], depth: int
-    ) -> Tensor[B, C // 2, (H - 1) * 2 + 2, (W - 1) * 2 + 2]:
+    def _apply_stage[B: IntVar, C: IntVar, H: IntVar, W: IntVar](
+        self, x: Tensor[[B, C, H, W]], depth: int
+    ) -> Tensor[[B, C // 2, (H - 1) * 2 + 2, (W - 1) * 2 + 2]]:
         idx = len(self.up_stages) - depth
         stage: GenUpStage[C] = self.up_stages[idx]
         return stage(x)
 
     @overload
-    def _chain[B, C, H, W](
-        self, x: Tensor[B, C, H, W], depth: Int[1]
-    ) -> Tensor[B, C // 2, H * 2, W * 2]: ...
+    def _chain[B: IntVar, C: IntVar, H: IntVar, W: IntVar](
+        self, x: Tensor[[B, C, H, W]], depth: Int[1]
+    ) -> Tensor[[B, C // 2, H * 2, W * 2]]: ...
 
     @overload
-    def _chain[I, B, C, H, W](
-        self, x: Tensor[B, C, H, W], depth: Int[I]
-    ) -> Tensor[B, C // 2 ** I, H * 2 ** I, W * 2 ** I]: ...
-
-    def _chain[I, B, C, H, W](
-        self, x: Tensor[B, C, H, W], depth: Int[I]
-    ) -> (Tensor[B, C // 2, H * 2, W * 2]
-         | Tensor[B, C // 2 ** I, H * 2 ** I, W * 2 ** I]):
+    def _chain[I: IntVar, B: IntVar, C: IntVar, H: IntVar, W: IntVar](
+        self, x: Tensor[[B, C, H, W]], depth: Int[I]
+    ) -> Tensor[[B, C // 2 ** I, H * 2 ** I, W * 2 ** I]]: ...
+
+    def _chain[I: IntVar, B: IntVar, C: IntVar, H: IntVar, W: IntVar](
+        self, x: Tensor[[B, C, H, W]], depth: Int[I]
+    ) -> (Tensor[[B, C // 2, H * 2, W * 2]]
+         | Tensor[[B, C // 2 ** I, H * 2 ** I, W * 2 ** I]]):
         y = self._apply_stage(x, depth)
         if depth == 1:
             return y
@@ -154,11 +154,11 @@ This `_apply_stage` + `_chain` pattern separates concerns:
 The caller invokes `_chain` with a concrete depth:
 
 ```python
-def forward[B](self, input: Tensor[B, 100, 1, 1]) -> Tensor[B, 3, 64, 64]:
+def forward[B: IntVar](self, input: Tensor[[B, 100, 1, 1]]) -> Tensor[[B, 3, 64, 64]]:
     h0 = F.relu(self.project_bn(self.project(input)))
-    assert_type(h0, Tensor[B, 512, 4, 4])
+    assert_type(h0, Tensor[[B, 512, 4, 4]])
     h1 = self._chain(h0, 3)  # 512->64, 4->32
-    assert_type(h1, Tensor[B, 64, 32, 32])
+    assert_type(h1, Tensor[[B, 64, 32, 32]])
     return torch.tanh(self.output(h1))
 ```
 
diff --git a/website/docs/tensor-shapes-tutorial-basics.mdx b/website/docs/tensor-shapes-tutorial-basics.mdx
index d30dbae791..d6d58a58b8 100644
--- a/website/docs/tensor-shapes-tutorial-basics.mdx
+++ b/website/docs/tensor-shapes-tutorial-basics.mdx
@@ -64,7 +64,7 @@ Make the dimension parameters into `Int[...]` and add class-level type
 parameters:
 
 ```python
-class BaselineActor[S, A](nn.Module):
+class BaselineActor[S: IntVar, A: IntVar](nn.Module):
     def __init__(self, state_size: Int[S], action_size: Int[A]) -> None:
         super().__init__()
         self.fc1 = nn.Linear(state_size, 400)
@@ -83,7 +83,7 @@ The forward method has one dynamic dimension — **batch size** — that
 varies across calls. Make it a method-level type parameter:
 
 ```python
-def forward[B](self, state: Tensor[B, S]) -> Tensor[B, A]:
+def forward[B: IntVar](self, state: Tensor[[B, S]]) -> Tensor[[B, A]]:
     h1 = F.relu(self.fc1(state))
     h2 = F.relu(self.fc2(h1))
     return torch.tanh(self.out(h2))
@@ -97,13 +97,13 @@ method-level param (bound per call).
 Add `assert_type` after each intermediate to verify what pyrefly infers:
 
 ```python
-def forward[B](self, state: Tensor[B, S]) -> Tensor[B, A]:
+def forward[B: IntVar](self, state: Tensor[[B, S]]) -> Tensor[[B, A]]:
     h1 = F.relu(self.fc1(state))
-    assert_type(h1, Tensor[B, 400])
+    assert_type(h1, Tensor[[B, 400]])
     h2 = F.relu(self.fc2(h1))
-    assert_type(h2, Tensor[B, 400])
+    assert_type(h2, Tensor[[B, 400]])
     act = torch.tanh(self.out(h2))
-    assert_type(act, Tensor[B, A])
+    assert_type(act, Tensor[[B, A]])
     return act
 ```
 
@@ -124,12 +124,12 @@ the shape annotations are consistent end-to-end:
 def test_baseline_actor():
     actor = BaselineActor(24, 4)
     state = torch.randn(8, 24)
-    # pyrefly infers: Tensor[8, 24]
+    # pyrefly infers: Tensor[[8, 24]]
     act = actor(state)
-    # pyrefly infers: Tensor[8, 4]
+    # pyrefly infers: Tensor[[8, 4]]
 ```
 
-Use concrete dimensions in tests (`Tensor[8, 24]`, not generic `Tensor[B, S]`)
+Use concrete dimensions in tests (`Tensor[[8, 24]]`, not generic `Tensor[[B, S]]`)
 so the type checker verifies the full shape calculation.
 
 ## The complete port
@@ -146,23 +146,23 @@ import TabItem from '@theme/TabItem';
     import torch.nn as nn
     import torch.nn.functional as F
     from torch import Tensor
-    from shape_extensions import Int
+    from shape_extensions import Int, IntVar
 
 
-    class BaselineActor[S, A](nn.Module):
+    class BaselineActor[S: IntVar, A: IntVar](nn.Module):
         def __init__(self, state_size: Int[S], action_size: Int[A]) -> None:
             super().__init__()
             self.fc1 = nn.Linear(state_size, 400)
             self.fc2 = nn.Linear(400, 400)
             self.out = nn.Linear(400, action_size)
 
-        def forward[B](self, state: Tensor[B, S]) -> Tensor[B, A]:
+        def forward[B: IntVar](self, state: Tensor[[B, S]]) -> Tensor[[B, A]]:
             h1 = F.relu(self.fc1(state))
-            # pyrefly infers: Tensor[B, 400]
+            # pyrefly infers: Tensor[[B, 400]]
             h2 = F.relu(self.fc2(h1))
-            # pyrefly infers: Tensor[B, 400]
+            # pyrefly infers: Tensor[[B, 400]]
             act = torch.tanh(self.out(h2))
-            # pyrefly infers: Tensor[B, A]
+            # pyrefly infers: Tensor[[B, A]]
             return act
     ```
   </TabItem>
diff --git a/website/docs/tensor-shapes-tutorial-loops.mdx b/website/docs/tensor-shapes-tutorial-loops.mdx
index 1839dc06a9..e6c1ba0739 100644
--- a/website/docs/tensor-shapes-tutorial-loops.mdx
+++ b/website/docs/tensor-shapes-tutorial-loops.mdx
@@ -27,7 +27,7 @@ Here's a Transformer encoder that stacks `n_layers` identical
 `EncoderLayer` modules:
 
 ```python
-class Encoder[NHead, DK, DInner](nn.Module):
+class Encoder[NHead: IntVar, DK: IntVar, DInner: IntVar](nn.Module):
     def __init__(
         self,
         n_head: Int[NHead],
@@ -40,13 +40,13 @@ class Encoder[NHead, DK, DInner](nn.Module):
             [EncoderLayer(n_head, d_k, d_inner) for _ in range(n_layers)]
         )
 
-    def forward[B, T](
-        self, src_seq: Tensor[B, T, NHead * DK]
-    ) -> Tensor[B, T, NHead * DK]:
+    def forward[B: IntVar, T: IntVar](
+        self, src_seq: Tensor[[B, T, NHead * DK]]
+    ) -> Tensor[[B, T, NHead * DK]]:
         enc_output = src_seq
         for layer in self.layer_stack:
             enc_output, _attn = layer(enc_output)
-            assert_type(enc_output, Tensor[B, T, NHead * DK])
+            assert_type(enc_output, Tensor[[B, T, NHead * DK]])
         return enc_output
 ```
 
@@ -54,7 +54,7 @@ Notice that `n_layers` is `int`, not `Int` — it's an iteration count that
 doesn't flow into any tensor dimension. Only values that determine tensor
 shapes need to be `Int`.
 
-Each `EncoderLayer` takes `Tensor[B, T, NHead * DK]` and returns the same
+Each `EncoderLayer` takes `Tensor[[B, T, NHead * DK]]` and returns the same
 shape, so the loop preserves the invariant and the type checker is
 satisfied.
 
@@ -74,15 +74,15 @@ widens to a less precise type.
 The fix is to separate the first iteration:
 
 ```python
-# Problem: x widens to Tensor[B, F, D] | Tensor[B, K, D]
+# Problem: x widens to Tensor[[B, F, D]] | Tensor[[B, K, D]]
 x = input_embs
 for layer in self.layers:
     x = layer(x)
-out: Tensor[B, K, D] = x  # type: ignore[bad-assignment]
+out: Tensor[[B, K, D]] = x  # type: ignore[bad-assignment]
 
 # Solution: no union, no type: ignore
 x = self.layers[0](input_embs)        # [B, F, D] -> [B, K, D]
-assert_type(x, Tensor[B, K, D])
+assert_type(x, Tensor[[B, K, D]])
 for i in range(1, len(self.layers)):
     x = self.layers[i](x)             # [B, K, D] -> [B, K, D]
 ```
@@ -94,14 +94,15 @@ separating them, you avoid the union widening entirely.
 
 Many architectures accept an activation function as a parameter (ReLU, GELU,
 SiLU, etc.). Since each activation's forward signature is
-`Tensor[*S] -> Tensor[*S]`, you can express this with a type alias:
+`Tensor[S] -> Tensor[S]` for a whole-shape type parameter `S: IntTuple`, you
+can express this with a type alias:
 
 ```python
 ShapePreservingActivation = (
     type[nn.ReLU] | type[nn.GELU] | type[nn.SiLU] | type[nn.Tanh]
 )
 
-class ResBlock[C](nn.Module):
+class ResBlock[C: IntVar](nn.Module):
     def __init__(self, c: Int[C], act_fn: ShapePreservingActivation) -> None:
         super().__init__()
         self.net = nn.Sequential(
@@ -121,7 +122,7 @@ Multi-head attention involves reshaping tensors from `[B, T, D]` to
 directly in annotations:
 
 ```python
-class CausalSelfAttention[NEmbedding, NHead](nn.Module):
+class CausalSelfAttention[NEmbedding: IntVar, NHead: IntVar](nn.Module):
     def __init__(
         self,
         n_embd: Int[NEmbedding],
@@ -133,19 +134,19 @@ class CausalSelfAttention[NEmbedding, NHead](nn.Module):
         self.n_head = n_head
         self.n_embd = n_embd
 
-    def forward[B, T](
-        self, x: Tensor[B, T, NEmbedding]
-    ) -> Tensor[B, T, NEmbedding]:
+    def forward[B: IntVar, T: IntVar](
+        self, x: Tensor[[B, T, NEmbedding]]
+    ) -> Tensor[[B, T, NEmbedding]]:
         qkv = self.c_attn(x)
-        assert_type(qkv, Tensor[B, T, 3 * NEmbedding])
+        assert_type(qkv, Tensor[[B, T, 3 * NEmbedding]])
         q, k, v = qkv.split(self.n_embd, dim=2)
-        assert_type(q, Tensor[B, T, NEmbedding])
+        assert_type(q, Tensor[[B, T, NEmbedding]])
 
         # Reshape for multi-head: [B, T, D] -> [B, NHead, T, D // NHead]
         head_dim = self.n_embd // self.n_head
         q = q.view(q.size(0), q.size(1), self.n_head, head_dim)
         q = q.transpose(1, 2)
-        assert_type(q, Tensor[B, NHead, T, NEmbedding // NHead])
+        assert_type(q, Tensor[[B, NHead, T, NEmbedding // NHead]])
         ...
 ```
 
diff --git a/website/docs/tensor-shapes.mdx b/website/docs/tensor-shapes.mdx
index 51ad1da938..7f77648319 100644
--- a/website/docs/tensor-shapes.mdx
+++ b/website/docs/tensor-shapes.mdx
@@ -44,8 +44,8 @@ import TabItem from '@theme/TabItem';
 </Tabs>
 
 With tensor shapes enabled, Pyrefly infers and displays the shape of every
-intermediate tensor — `Tensor[B, T, NEmbedding]` for embeddings,
-`Tensor[T]` for position indices — without any manual annotations on local
+intermediate tensor — `Tensor[[B, T, NEmbedding]]` for embeddings,
+`Tensor[[T]]` for position indices — without any manual annotations on local
 variables.
 
 ```sandbox
@@ -58,7 +58,7 @@ description: See tensor shape tracking, variadic batch dimensions, and shape mis
 Pyrefly's tensor shape support is built on two extensions that work together:
 
 1. **Symbolic integer arithmetic** in the core type system — lets you write
-   `Tensor[B, C, H, W]` and have arithmetic like `D // NHead` work at the
+   `Tensor[[B, C, H, W]]` and have arithmetic like `D // NHead` work at the
    type level.
 2. **Shape transform specifications** for PyTorch operators — a library of
    shape rules that tells Pyrefly how each operator transforms shapes.
@@ -69,12 +69,15 @@ a few annotations at class and function boundaries.
 
 ### Symbolic integer arithmetic
 
-You can write tensor types with integer dimensions — `Tensor[3, 4]` is a
+You can write tensor types with integer dimensions — `Tensor[[3, 4]]` is a
 2D tensor with shape `(3, 4)`. This works for modules too: `nn.Linear[3, 4]`
-takes `Tensor[..., 3]` as input and returns `Tensor[..., 4]`.
+accepts a tensor with any number of leading dimensions followed by a `3`,
+and returns one with the same leading dimensions followed by a `4` — see
+[Variadic dimensions with `Elements`](./tensor-shapes-reference.mdx#variadic-dimensions-with-elements)
+in the Reference page for the syntax that expresses this.
 
 **`Int[X]`** bridges runtime integer values to the type level. When
-`x: Tensor[3, 4]`, then `x.shape` has type `tuple[Int[3], Int[4]]` — you
+`x: Tensor[[3, 4]]`, then `x.shape` has type `tuple[Int[3], Int[4]]` — you
 can extract dimensions from tensors and use them to construct new ones.
 Arithmetic works too: if `a: Int[3]` and `b: Int[4]`, then
 `a * b: Int[12]`.
@@ -82,16 +85,16 @@ Arithmetic works too: if `a: Int[3]` and `b: Int[4]`, then
 **Generic type parameters** let you write shape-polymorphic modules:
 
 ```python
-class Linear[N, M]:
+class Linear[N: IntVar, M: IntVar]:
     def __init__(self, n: Int[N], m: Int[M]):
         ...
 
-    def forward[*Xs](self, inp: Tensor[*Xs, N]) -> Tensor[*Xs, M]:
+    def forward[Xs: IntTuple](self, inp: Tensor[[*Elements[Xs], N]]) -> Tensor[[*Elements[Xs], M]]:
         ...
 
 linear: Linear[3, 4] = Linear(3, 4)
-inp: Tensor[2, 5, 3] = ...
-x: Tensor[2, 5, 4] = linear(inp)
+inp: Tensor[[2, 5, 3]] = ...
+x: Tensor[[2, 5, 4]] = linear(inp)
 ```
 
 `Int` encodes symbolic shapes at the type level throughout PyTorch, covering modules as well as tensors.
@@ -99,10 +102,10 @@ x: Tensor[2, 5, 4] = linear(inp)
 **Arithmetic on type variables** lets you write custom shape transforms:
 
 ```python
-def custom_rand_tensor[A, B](a: Int[A], b: Int[B]) -> Tensor[(A + B) // 2]:
+def custom_rand_tensor[A: IntVar, B: IntVar](a: Int[A], b: Int[B]) -> Tensor[[(A + B) // 2]]:
     return torch.randn((a + b) // 2)
 
-x: Tensor[3] = custom_rand_tensor(2, 4)
+x: Tensor[[3]] = custom_rand_tensor(2, 4)
 ```
 
 While these examples use type annotations for exposition, the types of local
@@ -115,7 +118,7 @@ Some PyTorch operators have simple shape signatures that can be expressed as
 standard type stubs. For example, `torch.mm`:
 
 ```python
-def mm[M, K, N](x: Tensor[M, K], y: Tensor[K, N]) -> Tensor[M, N]:
+def mm[M: IntVar, K: IntVar, N: IntVar](x: Tensor[[M, K]], y: Tensor[[K, N]]) -> Tensor[[M, N]]:
     ...
 ```
 
@@ -166,7 +169,7 @@ express tensor shapes in type annotations that other libraries like `typeguard`
 and `beartype` can check at runtime. The syntax is designed to be universal for
 array-like containers (supporting JAX, NumPy, and PyTorch), but is somewhat
 verbose — for example, `Shaped[Tensor, "M 2 M//2"]` instead of
-`Tensor[M, 2, M // 2]`.
+`Tensor[[M, 2, M // 2]]`.
 
 Pyrefly supports jaxtyping annotations as an alternative front-end to our native
 syntax; these annotations are translated internally to use generics and display