Skip to content

Runtime-rank parameterized ADT decreases measures (per-instantiation size helpers) #1177

Description

@aallan

The #1172 guard ranks an ADT termination measure by structural size via a generated $dec_size_<T> helper — but only when the measure's type and its reachable fields are fully concrete. A parameterized measure (decreases(@List<Int>.0)), or a concrete type whose recursion rides through a parameterized field (Link(Tuple<Chain, Int>)), gets no guard: the registered layout describes the generic shape while concrete construction recomputes offsets from the actual type arguments, so a rank walk over the generic offsets reads a payload as a pointer (both failure modes were hit and regression-pinned during #1172 — a frozen rank false-trapping ch02_adt_recursive, and a wild walk on the base-name variant).

The fix is the $eq_<type> pattern: per-instantiation helpers ($dec_size_List_Int) whose field offsets are computed from the substituted concrete field types, generated from the parameterized comparison-site name exactly as structural Eq derivation does (#773/#912 machinery). Until then such measures stay statically checked (Tier 1 where provable) and honestly Tier-3-disclosed, with the scope stated in spec §5.6.1 and SKILL.md.

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions