[benjohnbarnes]

Constructing Vec with a list literal

This is just an initial proposal, not a finished patch. It is offered so the idea can be validated before anything is polished. It type-checks and has a test suite, but some points are Outstanding at the end.

The problem

Vec(a, n : Nat) exists and dimensions unify by equality, but nothing can build a vector longer than
one. MkVec is opaque and pinned hidden by stdlib_invariant_constructors_are_hidden; vempty and
vsingle pin lengths 0 and 1; vmap and vzip preserve or demand equality; and a length-changing
vcons needs n + 1, which dimension arithmetic declines. The index is therefore habitable in
principle and unreachable in practice.

The change

A list literal in a Vec position takes its length from the literal's own element count. Nothing new is
spelled — these are ordinary list literals, and the position's type is what gives each one its length.

These compile.

fn takes3(v : Vec(Int, 3)) : Int = 0
fn fixed() : Int = takes3([1, 2, 3])            -- the count is the length

fn takes0(v : Vec(Int, 0)) : Int = 0
fn empty() : Int = takes0([])                   -- and this is the empty vector

fn first(v : Vec(Int, n)) : Int = vhead(v)      -- a variable length takes any count
fn any_length() : Int = first([1]) + first([1, 2]) + first([1, 2, 3])

fn same(v : Vec(a, n)) : Vec(a, n) = vmap(\(x) -> x, v)   -- and a variable element type
fn kept() : Vec(Int, 2) = same([1, 2])

fn count(v : Vec(a, n)) : Int = 0
fn open_element() : Int = count([])   -- compiles: the count solves n, and nothing needs to solve a

These do not compile.

fn takes3(v : Vec(Int, 3)) : Int = 0
fn takes2(v : Vec(Int, 2)) : Int = 0
fn from_list() : List(Int) = [1, 2, 3]

fn wrong_count() : Int = takes3([1, 2])                -- expected length 3, but got length 2
fn a_list() : Int = takes3(from_list())                -- expected Vec(Int, 3), got List(Int)
fn bound_first() : Int =
  let v = [1, 2, 3]
  takes3(v)                                            -- v is a List(Int) before the position is known
fn rigid(v : Vec(Int, n)) : Vec(Int, n) = [1, 2, 3]    -- expected n, got 3
fn mixed() : Int = takes2([1, true])                   -- expected Int, got Bool

fn shown(v : Vec(a, n)) : String = show(vto_list(v))
-- an unsolved element type is fine until something needs an instance of it, and then the
-- message names it: cannot discharge constraint Show(a); add `given Show(a)` to the
-- enclosing function

And these, because the rule is Vec's alone. A user's own type of the same shape — and even one that
spells the same name — is not offered the form:

type Grid(a, n : Nat) = MkGrid(List(a))
fn takes(v : Grid(Int, 3)) : Int = 0
fn user_type() : Int = takes([1, 2, 3])   -- expected Grid(Int, 3), got List(Int)

A size written in the literal still does not parse, which is the alternative this proposal does not
take:

fn sized_literal() : Vec(Int, 3) = [1, 2, 3; 3]   -- unexpected token
fn sized_type(v : [Int; 3]) : Int = 0             -- unexpected token
fn unboxed_type(v : #[Int, 3]) : Int = 0          -- unexpected '[', expected '(', '{'

Why Vec, and what a generalisation could be

Primarily because it is the only type where the check is real. MkVec is opaque and pinned hidden, so
outside its module a literal is the only route to a value — which makes the count the only thing holding
the length honest. The predicate therefore names Data.Vec.Vec, matched on its qualified name in
wired.rs beside the compiler's other standard-library hooks.

Potentially Prism could in future have a more general feature to allow other types to construct from a list (and refuse this at compile time if the list is not a valid length). Swift has ExpressibleByArrayLiteral for this sort of thing. A generalisation like this would hopefully then be additive.

What it touches

One arm in check; one predicate, an identity test on Vec; one per-node fact for elaboration
(NodeRes::ShapeIndexed, following the unboxed_field precedent); and one wrapper in the existing
Expr::List elaboration arm, since the representation is a single List(a) field. Nothing reaches
Core — dimensions are erased before it, so there is no representation or codegen change.

Tests

tests/language/shape_indexed_literal.rs, wired into tests/frontend.rs: sixteen cases — lengths 0,
1, 2, 3 and 12; a length clash asserted on its wording; a variable length solved from the count;
a rigid length refused; the element lane adopted; both directions of the list/vector boundary; a
user-declared type of the same shape being refused rather than offered the form; and a literal bound
before its position being inferred as a List rather than a vector.

Two of them are runtime cases, and they exist because vto_list destructures the vector's own
constructor: a bare list would fail to match rather than quietly resemble one. That is the property a
checking-only change would get wrong, so it is a committed test rather than a probe.

Outstanding

Nothing below is outstanding any more. Each is kept as the record of what it was, and the branch
carries the fix.

• docs/src/stdlib/data-vec.md is regenerated rather than hand-edited: prism docs --stdlib --check --out docs/src/stdlib is green on this branch with LLVM 22, and it reported data-vec.md
  as the only page that had gone stale. prism docs --stdlib --test is green with it — 566 doctests
  and 538 expectations, none failed.
• The suite runs by its committed target. cargo test --test frontend shape_indexed is green on
  this branch — sixteen cases, the two that reach the vector's own constructor included.
• The double shape_indexed_ctor call is gone: the rule is decided before the match, so the
  predicate is computed once rather than tested by a guard and re-run by the body.

Not part of this

• Dynamic containers. Bytes and Tensor already have list constructors; making a literal build
  those is a class plus instances plus elaboration, is not about the size at all, and would be
  unchecked by nature.
• Arithmetic on dimensions. vcons and append stay declined. A literal can write a longer vector
  than the present constructors can; it cannot compute one.

[sdiehl]

Let me have a think about this, not sure I'm in love with having qualified literals as wired in types. I think this probably belongs in the desugaring pass.

[sdiehl]

The lean fuzzer seems like some upstream network timeout unrelated to this PR.

The scoreboard issue can be fixed with just scoreboard and then commit the updated version.