Construct fixed size Vec with a list literal

docs/internal/SCOREBOARD.md

@@ -29,7 +29,7 @@ compaction, above it is not.
 | surface AST      |    2,125 |     1,502 |       363 |        205 |  0.14 |
 | syntax codecs    |     none |      none |     2,996 |      2,456 |   n/a |
 | lint             |     none |      none |     1,190 |        866 |   n/a |
-| checker          |   12,726 |    10,049 |     4,239 |      3,390 |  0.34 |
+| checker          |   12,813 |    10,093 |     4,239 |      3,390 |  0.34 |
 
 What each row counts:
 

docs/src/spec.md

@@ -457,6 +457,8 @@ The third ground kind is **`Nat`**, inhabited by type-level natural numbers, the
 
 Dimensions unify **by equality only**: two literals unify when they are equal (`3` with `3`), a variable unifies with whatever dimension it meets, and a clash is a compile error naming both lengths (zipping a `Vec(Int, 3)` with a `Vec(Int, 4)` reports `expected length 3, but got length 4`). There is deliberately no successor structure and no arithmetic on dimensions: `n + m` and `n + 1` in a dimension position are declined at the parser with a pointed message, and this is a decision, not a gap.
 
+A dimension's reach is not only a constraint on types but the way its values are written. A **list literal in a `Vec` position takes its length from the literal's own element count**, so `[1, 2, 3]` in a `Vec(Int, 3)` position is a length-three vector and `[]` is the empty one; a count that disagrees with a literal dimension is a compile error naming both lengths, and a count meeting a variable dimension solves it. The spelling is the ordinary list syntax, resolved by the expected type in the way a bare integer literal adopts a `Float` context and a literal's elements adopt the lane of a known `List(T)`. The form is offered for `Data.Vec` and nothing else, and deliberately so: a dimension is erased before Core, so no criterion can tell a `Nat` that measures a container from one that means something else, and a rule keyed on a declaration's shape would offer the form to any type with a `Nat` in it — including one whose author meant it as something other than a length. `Vec` is the one type where the offer is worth making, because `MkVec` is hidden, so outside its module a literal is the only route to a value and the count it carries is the only thing holding the length honest. A general mechanism would be additive — a class a type conforms to, with `Vec` as its first instance — rather than a widening of this rule. Writing a literal is thus not a way around the absent arithmetic: it can write a longer vector than a constructor at length `0` or `1` could, but it cannot compute a length.
+
 The consequence is stated honestly rather than worked around: an operation whose correctness needs an arithmetic relation between dimensions cannot be given a length-precise type. A length-changing `cons` of type `(a, Vec(a, n)) -> Vec(a, n + 1)` is therefore not expressible, and a `head` over `Vec(a, n)` cannot statically exclude the empty vector (which would require `n` to be a successor `m + 1`); such a `head` accepts any length and faults, or ranges over `Fail`, on the empty case. Equality-only dimension unification is exactly the reach that shape indexing needs (fixed-length containers, matching-length zips) without importing a dependent-arithmetic decision procedure into the frozen core.
 
 Dimensions are erased before the Core IR and never reach code generation, so a `Nat` index is a purely static fact: it constrains what type-checks but is invisible to every backend and to the determinism contract, exactly like a phantom parameter. An unannotated parameter still defaults to `Type`, so `Nat` is opt-in.

lib/std/Data/Vec.pr

@@ -3,10 +3,20 @@
 -- `Vec(a, n)` is a list of `a` whose length `n` is a type-level natural. The
 -- `Nat` kind unifies dimensions by equality of literals and variables only:
 -- there is no successor structure and no arithmetic, and `n + m` in a dimension
--- position is declined at the parser. This module therefore ships exactly the
--- operations that equality-only indexing can type honestly:
+-- position is declined at the parser.
 --
---   - `vempty` and `vsingle` pin a literal length (`0`, `1`).
+-- A vector is written as a list literal, and the literal's own element count is
+-- what fixes the length: in a `Vec(Int, 3)` position `[1, 2, 3]` is a
+-- length-three vector and `[]` is the empty one, while a count that disagrees is
+-- a compile error naming both lengths. The count is read from the literal rather
+-- than required of it, so this reaches every length, and a literal in a position
+-- whose length is a variable solves that variable. The constructor below is an
+-- implementation detail of that spelling and is not exported.
+--
+-- This module ships the operations that equality-only indexing can type honestly:
+--
+--   - `vempty` and `vsingle` pin a literal length (`0`, `1`), though a literal is
+--     usually the plainer way to say the same thing.
 --   - `vmap` preserves the length (`n` appears on both sides).
 --   - `vzip` requires equal lengths (both `n`); a length clash is a compile
 --     error that names both lengths.
@@ -15,7 +25,9 @@
 -- expressible under equality-only unification: a length-changing
 -- `vcons : (a, Vec(a, n)) -> Vec(a, n + 1)` and an append
 -- `(Vec(a, n), Vec(a, m)) -> Vec(a, n + m)`. That is the declined line; writing
--- either `n + 1` produces a pointed rejection rather than a bare parse error.
+-- either `n + 1` produces a pointed rejection rather than a bare parse error. A
+-- literal is no way around it either: it can write a longer vector than the
+-- constructors here can, but it cannot compute one.
 --
 -- `vhead` accepts any length, so it cannot statically forbid the empty vector
 -- (ruling it out needs `n = m + 1`, again arithmetic). On an empty vector it

src/core/elaborate/expr.rs

@@ -926,7 +926,32 @@ impl Elab<'_> {
                         Box::new(Comp::Bind(Box::new(acc), vrest.into(), Box::new(cons))),
                     );
                 }
-                acc
+                // A literal checked against a shape-indexed type is that type's own
+                // constructor applied to the element chain above — `[1, 2, 3]` in a
+                // `Vec(Int, 3)` position is a `MkVec` over the three-element list. The
+                // dimension is erased before Core, so the constructor is the whole of
+                // what elaboration needs to know, and checking recorded which one
+                // against this node because the expected type is not visible here.
+                let wrap = match self.hir.res(e.id) {
+                    Some(NodeRes::ShapeIndexed(ctor)) => Some(*ctor),
+                    _ => None,
+                };
+                match wrap {
+                    Some(ctor) => {
+                        let vlist = self.fresh();
+                        let tag = self.ctors.get(ctor.as_str()).map_or(0, |c| c.tag);
+                        Comp::Bind(
+                            Box::new(acc),
+                            vlist.clone().into(),
+                            Box::new(Comp::Return(Value::Ctor(
+                                ctor,
+                                tag,
+                                vec![Value::Var(vlist.into())],
+                            ))),
+                        )
+                    }
+                    _ => acc,
+                }
             }
             Expr::FieldAccess(recv, field) => self.field_access(e.id, recv, field, locals)?,
             Expr::RecordCreate(ctor_name, field_exprs) => {

src/driver/dump.rs

@@ -1316,6 +1316,10 @@ enum HirRes {
     },
     #[serde(rename = "unboxed")]
     Unboxed { index: usize, arity: usize },
+    // A list literal that constructs a shape-indexed type: the constructor
+    // elaboration wraps its element chain in.
+    #[serde(rename = "shape_indexed")]
+    ShapeIndexed { ctor: String },
     #[serde(rename = "paths")]
     Paths { chains: Vec<Vec<HirStep>> },
 }
@@ -1414,6 +1418,9 @@ fn render_res(res: &NodeRes) -> HirRes {
             index: *index,
             arity: *arity,
         },
+        NodeRes::ShapeIndexed(ctor) => HirRes::ShapeIndexed {
+            ctor: ctor.as_str().to_string(),
+        },
         NodeRes::Paths(chains) => HirRes::Paths {
             chains: chains
                 .iter()

src/hir/lint.rs

@@ -121,7 +121,7 @@ pub fn lint_hir(hir: &CheckedHir<'_>) -> Vec<HirViolation> {
     };
     for (i, fact) in hir.facts.res.iter().enumerate() {
         match fact {
-            None => {}
+            None | Some(NodeRes::ShapeIndexed(_)) => {}
             Some(NodeRes::Field(field)) => {
                 if let Some(msg) = check_step(field) {
                     push(&mut out, i, msg);

src/hir/mod.rs

@@ -41,6 +41,12 @@ pub enum NodeRes {
     /// A record update path `e { p.q = v }`: one rebuild chain per path, one
     /// [`FieldRef`] step per path segment.
     Paths(Vec<Vec<FieldRef>>),
+    /// A list literal checked against a shape-indexed expected type: the
+    /// constructor to wrap the literal's element chain in, so `[1, 2, 3]` in a
+    /// `Vec(Int, 3)` position elaborates to that type's own constructor applied
+    /// to the list. The dimension itself is erased before Core, so the
+    /// constructor is the whole of what elaboration needs to know.
+    ShapeIndexed(Sym),
 }
 
 /// Operation-local residual evidence for one checked handler expression.
@@ -332,6 +338,7 @@ impl NodeFacts {
     pub(crate) fn from_tables(
         field_res: BTreeMap<NodeId, FieldRef>,
         unboxed_field: BTreeMap<NodeId, (usize, usize)>,
+        shape_indexed: BTreeMap<NodeId, Sym>,
         path_res: PathRes,
         fixed: BTreeMap<NodeId, Type>,
         span_types: BTreeMap<NodeId, Type>,
@@ -355,6 +362,9 @@ impl NodeFacts {
         for (id, (idx, arity)) in unboxed_field {
             place(&mut res, id, NodeRes::UnboxedField(idx, arity));
         }
+        for (id, ctor) in shape_indexed {
+            place(&mut res, id, NodeRes::ShapeIndexed(ctor));
+        }
         for (id, chains) in path_res {
             place(&mut res, id, NodeRes::Paths(chains));
         }

src/repl/mod.rs

@@ -1730,6 +1730,7 @@ mod tests {
                 BTreeMap::new(),
                 BTreeMap::new(),
                 BTreeMap::new(),
+                BTreeMap::new(),
                 BTreeSet::new(),
                 BTreeMap::new(),
                 BTreeSet::new(),

src/tc/infer.rs

@@ -16,9 +16,9 @@ use crate::names;
 use crate::sym::Sym;
 use crate::syntax::ast::{self, Core, Expr, Grade, HandlerArm, HandlerMode, NodeId, S};
 use crate::syntax::desugar::referenced_names;
-use crate::types::ty::{EffRow, Label, Type, LIST, NUM_CLASS, SHOW_CLASS};
+use crate::types::ty::{EffRow, Kind, Label, Type, LIST, NUM_CLASS, SHOW_CLASS};
 use crate::types::EffOpInfo;
-use crate::wired::Indexable;
+use crate::wired::{self, Indexable};
 
 // Red zone / segment size for the checker's per-node recursion, matching the
 // desugar and typed-Core-builder guards.
@@ -273,6 +273,49 @@ impl Tc<'_> {
         handled
     }
 
+    /// The constructor a list literal should build when its expected type is the
+    /// standard library's vector, as `(element position, dimension position,
+    /// constructor)`, or `None` for every other type.
+    ///
+    /// **This is `Data.Vec.Vec` and nothing else, deliberately.** A dimension is an
+    /// erased phantom, so no criterion can tell a `Nat` that measures a container
+    /// from one that means something else. Recognising a type by its declared kinds
+    /// — which an earlier version of this did — offers the form to any declaration
+    /// with a `Nat` in it, whatever its author meant by it, and it cannot check the
+    /// value it builds either.
+    ///
+    /// `Vec` is the one type where the offer is worth making, because `MkVec` is
+    /// `opaque` and pinned hidden by `stdlib_invariant_constructors_are_hidden`, so
+    /// outside its module a literal is the *only* route to a value and the count it
+    /// carries is the only thing holding the length honest. A user's own
+    /// `Grid(a, n : Nat)` has the same shape but keeps its constructor visible, so
+    /// nothing is checked there either way and the form would only appear to
+    /// promise something.
+    ///
+    /// A general mechanism would be additive rather than a widening of this: a class
+    /// a type conforms to, as Swift's builder conformance works, with `Vec` as its
+    /// first instance.
+    fn shape_indexed_ctor(&self, head: &Sym, args: &[Type]) -> Option<(usize, usize, Sym)> {
+        if head.as_str() != wired::TY_VEC || args.len() != 2 {
+            return None;
+        }
+        // A sanity check on a type whose declaration is known rather than a way of
+        // recognising it: `Vec` has one constructor, and the form is retired rather
+        // than guessed if that ever stops being true. The positions below are the
+        // library's declaration order — element first, dimension second — and are
+        // read from the kinds rather than assumed, so a re-declaration that swapped
+        // them retires the form instead of misreading it.
+        let info = self.data.get(head.as_str())?;
+        if info.ctors.len() != 1 {
+            return None;
+        }
+        let kinds = info.param_kinds();
+        let elem_i = kinds.iter().position(|k| *k == Kind::Type)?;
+        let nat_i = kinds.iter().position(|k| *k == Kind::Nat)?;
+        let ctor = Sym::from(info.ctors[0].as_str());
+        Some((elem_i, nat_i, ctor))
+    }
+
     fn check(&mut self, env: &Env, e: &S<Expr<Core>>, ty: &Type) -> Result<(), TypeError> {
         self.with_tooltip_row(e.id, e.span, |tc| tc.check_node(env, e, ty))
     }
@@ -444,6 +487,39 @@ impl Tc<'_> {
                 }
                 Ok(())
             }
+            // A list literal against `Vec` takes its length from the literal's own
+            // element count, so `[1, 2, 3]` in a `Vec(Int, 3)` position is a
+            // length-3 vector with no construction function in sight. It descends
+            // from the tuple arm above, which takes an arity from its shape, and
+            // from the `Float` adoption below, which lets an expected type steer a
+            // literal. The predicate says why this is `Vec` alone.
+            (Expr::List(elems), Type::Con(head, args))
+                if self.shape_indexed_ctor(head, args).is_some() =>
+            {
+                let (elem_i, nat_i, ctor) =
+                    self.shape_indexed_ctor(head, args).expect("guarded above");
+                let elem_ty = self.apply(&args[elem_i]);
+                for elem in elems {
+                    self.check(env, elem, &elem_ty)?;
+                }
+                // The dimension is unified rather than merely compared, so a literal
+                // against a variable length solves it, a clash names both lengths in
+                // the wording dimension unification already uses, and a rigid
+                // dimension is refused rather than forced.
+                let want = self.apply(&args[nat_i]);
+                let got = Type::Nat(u64::try_from(elems.len()).unwrap_or(u64::MAX));
+                self.subtype(&got, &want).map_err(|e| {
+                    e.or(TypeError::TypeMismatch {
+                        span,
+                        expected: want.show(),
+                        found: got.show(),
+                    })
+                })?;
+                // Elaboration cannot see the expected type, so the constructor it
+                // must wrap the element chain in is recorded against this node.
+                self.shape_indexed.insert(id, ctor);
+                Ok(())
+            }
             // A list literal against a known `List(T)` pushes `T` into each
             // element, so the tower's polymorphic literals reach through the
             // aggregate: `[1, 2, 3] : List(I64)` needs no per-element suffix, the

src/tc/mod.rs

@@ -365,6 +365,7 @@ fn check_seeded_mode(
     }
     let field_res;
     let unboxed_field;
+    let shape_indexed;
     let path_res;
     let fixed;
     let span_types;
@@ -386,6 +387,7 @@ fn check_seeded_mode(
             eff_ops: &eff_ops,
             field_res: BTreeMap::new(),
             unboxed_field: BTreeMap::new(),
+            shape_indexed: BTreeMap::new(),
             path_res: PathRes::new(),
             fixed: BTreeMap::new(),
             span_types: BTreeMap::new(),
@@ -508,6 +510,7 @@ fn check_seeded_mode(
         tc.check_or_null_sites()?;
         field_res = tc.field_res;
         unboxed_field = tc.unboxed_field;
+        shape_indexed = tc.shape_indexed;
         path_res = tc.path_res;
         fixed = tc.fixed;
         span_types = tc.span_types;
@@ -543,6 +546,7 @@ fn check_seeded_mode(
         facts: NodeFacts::from_tables(
             field_res,
             unboxed_field,
+            shape_indexed,
             path_res,
             fixed,
             span_types,
@@ -704,6 +708,7 @@ fn infer_expr_full(
         eff_ops: &checked.defs.eff_ops,
         field_res: BTreeMap::new(),
         unboxed_field: BTreeMap::new(),
+        shape_indexed: BTreeMap::new(),
         path_res: PathRes::new(),
         fixed: BTreeMap::new(),
         span_types: BTreeMap::new(),
@@ -757,6 +762,7 @@ fn infer_expr_full(
     let facts = NodeFacts::from_tables(
         tc.field_res,
         tc.unboxed_field,
+        tc.shape_indexed,
         tc.path_res,
         tc.fixed,
         tc.span_types,
@@ -791,6 +797,7 @@ fn query_tc(seed: &TypecheckSeed) -> Tc<'_> {
         eff_ops: seed.effect_operations(),
         field_res: BTreeMap::new(),
         unboxed_field: BTreeMap::new(),
+        shape_indexed: BTreeMap::new(),
         path_res: PathRes::new(),
         fixed: BTreeMap::new(),
         span_types: BTreeMap::new(),

src/tc/session.rs

@@ -134,6 +134,9 @@ pub(super) struct Tc<'a> {
     pub(super) eff_ops: &'a BTreeMap<String, EffOpInfo>,
     pub(super) field_res: BTreeMap<NodeId, FieldRef>,
     pub(super) unboxed_field: BTreeMap<NodeId, (usize, usize)>,
+    /// A list literal checked against a shape-indexed expected type, keyed by the
+    /// literal's node id: the constructor elaboration wraps its element chain in.
+    pub(super) shape_indexed: BTreeMap<NodeId, Sym>,
     pub(super) path_res: PathRes,
     pub(super) fixed: BTreeMap<NodeId, Type>,
     pub(super) span_types: BTreeMap<NodeId, Type>,

src/tc/subsume.rs

@@ -892,6 +892,7 @@ mod tests {
             field_res: BTreeMap::new(),
             body_witness: BTreeMap::new(),
             unboxed_field: BTreeMap::new(),
+            shape_indexed: BTreeMap::new(),
             path_res: PathRes::new(),
             fixed: BTreeMap::new(),
             span_types: BTreeMap::new(),

src/wired.rs

@@ -19,6 +19,14 @@ use crate::types::Type;
 const TY_HASHMAP: &str = "HashMap";
 const TY_TENSOR: &str = "Tensor";
 
+/// The standard library's fixed-length vector, `Data.Vec.Vec`.
+///
+/// Unlike the containers above, this one is matched on its **qualified** name.
+/// Those are the only declarations of their name, so a bare name is enough for
+/// them; a user is free to declare a `Vec` of their own, and the list-literal
+/// rule that reads this must not catch it.
+pub(crate) const TY_VEC: &str = "Data.Vec.Vec";
+
 /// A container the `e[k]` / `e[k] := v` index sugar supports.
 ///
 /// Classifying a receiver type once, here, is what lets the typing rule

tests/frontend.rs

@@ -69,6 +69,7 @@ mod module_self_import;
 mod modules;
 #[path = "language/num_tower.rs"]
 mod num_tower;
+
 #[path = "language/ordered_witness.rs"]
 mod ordered_witness;
 #[path = "language/param_annot.rs"]
@@ -81,6 +82,8 @@ mod query;
 mod reflect;
 #[path = "language/rigid_sig_vars.rs"]
 mod rigid_sig_vars;
+#[path = "language/shape_indexed_literal.rs"]
+mod shape_indexed_literal;
 #[path = "language/skolem_escape.rs"]
 mod skolem_escape;
 #[path = "language/soundness.rs"]