BoxSeq collision when composites have Seq fields of different element types #1101

Summary

HeapParameterization's Box datatype has a single BoxSeq constructor
whose wrapped-value type is the specific TSeq X of whatever field
triggers it. When a program has composites with Seq<T> fields for two
different T, the pipeline produces two BoxSeq constructor entries with
the same name but different argument types. Deduplication by name keeps
only one, and Core type-checking fails downstream with:

Impossible to unify (arrow (Sequence int) Box) with (arrow (Sequence bool) $__ty99).
First mismatch: int with bool.

Minimal repro

composite IntBox {
  var data: Seq<int>
}

composite BoolBox {
  var data: Seq<bool>
}

procedure useBoth() {
  var ib: IntBox := new IntBox;
  ib#data := [1, 2, 3];
  var bb: BoolBox := new BoolBox;
  bb#data := [true, false];
  assert Sequence.length(ib#data) == 3;
  assert Sequence.length(bb#data) == 2
};

Where the bug lives

Strata/Languages/Laurel/HeapParameterization.lean, in three parallel
functions:

• boxConstructorName — maps .TSeq _ to "BoxSeq" (no element-type
  discrimination)
• boxDestructorName — maps .TSeq _ to "Box..SeqVal!" (same)
• boxConstructorDef — emits { name := "BoxSeq", args := [{ name := "SeqVal", type := ⟨ty, none⟩ }] } where ty is the specific
  TSeq X of the field being boxed

A single Box datatype can only carry one BoxSeq constructor, and the
usedBoxConstructors dedup in heapParameterization keeps the first
by name.

Fix sketch

Mirror the existing per-primitive approach (BoxInt, BoxBool,
BoxFloat64, etc.) and derive an element-type-specific name from the
Seq element type:

• TSeq TInt → "BoxSeq_int" / "Box..SeqVal_int!"
• TSeq TBool → "BoxSeq_bool" / "Box..SeqVal_bool!"
• TSeq (UserDefined X) → "BoxSeq_X" / "Box..SeqVal_X!"

Needs to handle nested cases (TSeq (TSeq TInt)) — flatten into a
stable name or use a hash/encoding.

Alternative: erase the element type in the box's arg type (e.g. use
TCore "Sequence" or some opaque wrapper). Cleaner but leans on Core's
polymorphism in a way that may or may not compose with the existing
Box datatype machinery.

Impact

Not triggered by the Seq/Array feature in isolation — Array<int> uses
a single $data: Seq<int> field and Arrays of other types are rejected
by the validator. The bug only fires when two user-defined composites
have Seq fields of different element types. Before the Seq/Array feature
landed this pattern was expressible through direct composite declaration,
but the BoxSeq handling is new, so in practice the bug is newly
exercisable.

Not blocking the Seq/Array feature

The Seq/Array PR (#1073) doesn't introduce this, and a working fix is
more invasive than the rest of the PR. Filing this separately so the
feature can land.