_forced

Forced-argument analysis helpers for datatype constructors; consumed by datatype elaboration and tests that inspect recoverable constructor fields.

forcedFieldNames

McBride-forced subset of a constructor's fields: a field is forced iff its sentinel marker occurs in targetIdx prevFull or in fieldTyOf f_j prev_<j for some j > i. Returns field names in declaration order.

{ fields : [Field]; targetIdx : Prev -> Hoas; fieldTyOf : ?Field -> Prev -> Hoas } -> [String]

forcedFieldSet

forcedFieldNames re-keyed as { <name> = true; } for O(1) membership.

{ fields; targetIdx; fieldTyOf? } -> { <name> = true; }

isFieldForced

Predicate form: whether the named field appears in the forced set.

{ fields; targetIdx; fieldTyOf? } -> String -> Bool

mentionsOf

Collect _signatureField marker names occurring in a HOAS term. Binder bodies are descended by applying their closure to a forced-probe sentinel.

Hoas -> [String]