Substitution

Capture-free substitution and telescope instantiation.

substitution

Capture-free substitution and telescope instantiation for QIEC.

StaticSubstitution dataclass

StaticSubstitution(types: tuple[tuple[str, TypeExpr], ...] = (), indices: tuple[tuple[str, IndexTerm], ...] = (), effects: tuple[tuple[str, EffectRef | EffectVariable], ...] = ())

A deterministic substitution split by static namespace.

PARAMETER	DESCRIPTION
types	Bindings from type-variable names to types. TYPE: tuple[tuple[str, TypeExpr], ...] DEFAULT: ()
indices	Bindings from index-variable names to index terms. TYPE: tuple[tuple[str, IndexTerm], ...] DEFAULT: ()
effects	Bindings from effect-variable names to interface applications or other effect variables. TYPE: tuple[tuple[str, EffectRef | EffectVariable], ...] DEFAULT: ()

__post_init__

__post_init__() -> None

Reject a substitution that binds one name twice.

RAISES	DESCRIPTION
ValueError	If a name repeats within a namespace. Two bindings for one name would make the result depend on lookup order.

Source code in src/quivers/qiec/substitution.py

def __post_init__(self) -> None:
    """Reject a substitution that binds one name twice.

    Raises
    ------
    ValueError
        If a name repeats within a namespace. Two bindings for one
        name would make the result depend on lookup order.
    """
    for namespace in (self.types, self.indices, self.effects):
        names = [name for name, _ in namespace]
        if len(set(names)) != len(names):
            raise ValueError("duplicate substitution binding")

type

type(name: str) -> TypeExpr | None

What a type binder of this name is bound to.

PARAMETER	DESCRIPTION
name	The binder name. TYPE: str

RETURNS	DESCRIPTION
TypeExpr or None	The bound type, or None when this substitution says nothing about the name, in which case the variable stands.

Source code in src/quivers/qiec/substitution.py

def type(self, name: str) -> TypeExpr | None:
    """What a type binder of this name is bound to.

    Parameters
    ----------
    name : str
        The binder name.

    Returns
    -------
    TypeExpr or None
        The bound type, or None when this substitution says nothing
        about the name, in which case the variable stands.
    """
    return next((value for key, value in self.types if key == name), None)

index

index(name: str) -> IndexTerm | None

What an index binder of this name is bound to.

PARAMETER	DESCRIPTION
name	The binder name. TYPE: str

RETURNS	DESCRIPTION
IndexTerm or None	The bound index, or None when the name is unbound here.

Source code in src/quivers/qiec/substitution.py

def index(self, name: str) -> IndexTerm | None:
    """What an index binder of this name is bound to.

    Parameters
    ----------
    name : str
        The binder name.

    Returns
    -------
    IndexTerm or None
        The bound index, or None when the name is unbound here.
    """
    return next((value for key, value in self.indices if key == name), None)

effect

effect(name: str) -> EffectRef | EffectVariable | None

What an effect binder of this name is bound to.

PARAMETER	DESCRIPTION
name	The binder name. TYPE: str

RETURNS	DESCRIPTION
EffectRef or EffectVariable or None	The bound interface application or effect variable, or None when the name is unbound here.

Source code in src/quivers/qiec/substitution.py

def effect(self, name: str) -> EffectRef | EffectVariable | None:
    """What an effect binder of this name is bound to.

    Parameters
    ----------
    name : str
        The binder name.

    Returns
    -------
    EffectRef or EffectVariable or None
        The bound interface application or effect variable, or None
        when the name is unbound here.
    """
    return next((value for key, value in self.effects if key == name), None)

instantiate_telescope

instantiate_telescope(telescope: Telescope, arguments: tuple[StaticArgument, ...]) -> StaticSubstitution

Kind-check static arguments and construct their substitution.

PARAMETER	DESCRIPTION
telescope	The binders to instantiate, in order. Later binders may depend on earlier ones, so the arguments are checked left to right with the substitution built so far already applied. TYPE: Telescope
arguments	One argument per binder. TYPE: tuple[StaticArgument, ...]

RETURNS	DESCRIPTION
StaticSubstitution	The substitution carrying each binder to its argument.

RAISES	DESCRIPTION
TypeError	If an argument is of the wrong static class for its binder.
ValueError	If the counts differ, or an argument is of the wrong kind or index sort.

Source code in src/quivers/qiec/substitution.py

def instantiate_telescope(
    telescope: Telescope,
    arguments: tuple[StaticArgument, ...],
) -> StaticSubstitution:
    """Kind-check static arguments and construct their substitution.

    Parameters
    ----------
    telescope : Telescope
        The binders to instantiate, in order. Later binders may depend on
        earlier ones, so the arguments are checked left to right with the
        substitution built so far already applied.
    arguments : tuple[StaticArgument, ...]
        One argument per binder.

    Returns
    -------
    StaticSubstitution
        The substitution carrying each binder to its argument.

    Raises
    ------
    TypeError
        If an argument is of the wrong static class for its binder.
    ValueError
        If the counts differ, or an argument is of the wrong kind or
        index sort.
    """
    types, indices, effects = check_static_arguments(telescope, arguments)
    return StaticSubstitution(types, indices, effects)

substitute_index

substitute_index(term: IndexTerm, substitution: StaticSubstitution) -> IndexTerm

Substitute into an index term.

PARAMETER	DESCRIPTION
term	The index to rewrite. TYPE: IndexTerm
substitution	The bindings to apply. TYPE: StaticSubstitution

RETURNS	DESCRIPTION
IndexTerm	The rewritten index. A variable carrying an identity is rigid and is returned unchanged, which is what keeps a branch's skolem from being captured by a like-named declaration binder.

Source code in src/quivers/qiec/substitution.py

def substitute_index(term: IndexTerm, substitution: StaticSubstitution) -> IndexTerm:
    """Substitute into an index term.

    Parameters
    ----------
    term : IndexTerm
        The index to rewrite.
    substitution : StaticSubstitution
        The bindings to apply.

    Returns
    -------
    IndexTerm
        The rewritten index. A variable carrying an identity is rigid and
        is returned unchanged, which is what keeps a branch's skolem from
        being captured by a like-named declaration binder.
    """
    if isinstance(term, IndexVariable) and term.identity is None:
        return substitution.index(term.name) or term
    if isinstance(term, IndexConstructor):
        return IndexConstructor(
            term.name,
            tuple(substitute_index(arg, substitution) for arg in term.arguments),
            term.sort,
        )
    if isinstance(term, ShapeIndex):
        return ShapeIndex(
            tuple(
                substitute_index(dimension, substitution)
                for dimension in term.dimensions
            )
        )
    return term

substitute_effect

substitute_effect(effect: EffectRef, substitution: StaticSubstitution) -> EffectRef

Substitute into an interface application's static arguments.

PARAMETER	DESCRIPTION
effect	The application to rewrite. TYPE: EffectRef
substitution	The bindings to apply. TYPE: StaticSubstitution

RETURNS	DESCRIPTION
EffectRef	The application with its arguments rewritten. The declaration's identity and name are unchanged, since substitution instantiates an interface rather than selecting a different one.

Source code in src/quivers/qiec/substitution.py

def substitute_effect(effect: EffectRef, substitution: StaticSubstitution) -> EffectRef:
    """Substitute into an interface application's static arguments.

    Parameters
    ----------
    effect : EffectRef
        The application to rewrite.
    substitution : StaticSubstitution
        The bindings to apply.

    Returns
    -------
    EffectRef
        The application with its arguments rewritten. The declaration's
        identity and name are unchanged, since substitution instantiates
        an interface rather than selecting a different one.
    """
    return EffectRef(
        effect.id,
        effect.name,
        tuple(substitute_static(arg, substitution) for arg in effect.arguments),
    )

substitute_plate

substitute_plate(plate: PlateShape, substitution: StaticSubstitution) -> PlateShape

Substitute static variables in a plate's axis sizes.

PARAMETER	DESCRIPTION
plate	The plate. TYPE: PlateShape
substitution	The static substitution. TYPE: StaticSubstitution

RETURNS	DESCRIPTION
PlateShape	The plate with every axis size substituted.

Source code in src/quivers/qiec/substitution.py

def substitute_plate(plate: PlateShape, substitution: StaticSubstitution) -> PlateShape:
    """Substitute static variables in a plate's axis sizes.

    Parameters
    ----------
    plate : PlateShape
        The plate.
    substitution : StaticSubstitution
        The static substitution.

    Returns
    -------
    PlateShape
        The plate with every axis size substituted.
    """
    return PlateShape(
        tuple(
            PlateAxis(axis.name, substitute_index(axis.size, substitution))
            for axis in plate.batch
        ),
        tuple(
            PlateAxis(axis.name, substitute_index(axis.size, substitution))
            for axis in plate.event
        ),
    )

substitute_type

substitute_type(type_: TypeExpr, substitution: StaticSubstitution) -> TypeExpr

Substitute into a type expression.

PARAMETER	DESCRIPTION
type_	The type to rewrite. TYPE: TypeExpr
substitution	The bindings to apply. TYPE: StaticSubstitution

RETURNS	DESCRIPTION
TypeExpr	The rewritten type. As with indices, a variable carrying an identity is rigid and survives unchanged.

RAISES	DESCRIPTION
TypeError	If the expression is of an unknown class.

Source code in src/quivers/qiec/substitution.py

def substitute_type(type_: TypeExpr, substitution: StaticSubstitution) -> TypeExpr:
    """Substitute into a type expression.

    Parameters
    ----------
    type_ : TypeExpr
        The type to rewrite.
    substitution : StaticSubstitution
        The bindings to apply.

    Returns
    -------
    TypeExpr
        The rewritten type. As with indices, a variable carrying an
        identity is rigid and survives unchanged.

    Raises
    ------
    TypeError
        If the expression is of an unknown class.
    """
    if isinstance(type_, TypeVariable) and type_.identity is None:
        return substitution.type(type_.name) or type_
    if isinstance(type_, TypeVariable):
        return type_
    if isinstance(type_, TypeApplication):
        return TypeApplication(
            type_.constructor,
            tuple(substitute_static(arg, substitution) for arg in type_.arguments),
        )
    if isinstance(type_, FunctionType):
        return FunctionType(
            substitute_type(type_.parameter, substitution),
            substitute_type(type_.result, substitution),
        )
    if isinstance(type_, EqualityType):
        return EqualityType(
            type_.kind,
            substitute_static(type_.left, substitution),
            substitute_static(type_.right, substitution),
        )
    raise TypeError(f"unknown type term {type_!r}")

substitute_static

substitute_static(term: StaticArgument, substitution: StaticSubstitution) -> StaticArgument

Substitute into a static argument of any namespace.

PARAMETER	DESCRIPTION
term	A type, index, or effect argument. TYPE: StaticArgument
substitution	The bindings to apply. TYPE: StaticSubstitution

RETURNS	DESCRIPTION
StaticArgument	The rewritten argument, dispatched to the namespace it belongs to.

RAISES	DESCRIPTION
TypeError	If the term is of an unknown class.

Source code in src/quivers/qiec/substitution.py

def substitute_static(
    term: StaticArgument,
    substitution: StaticSubstitution,
) -> StaticArgument:
    """Substitute into a static argument of any namespace.

    Parameters
    ----------
    term : StaticArgument
        A type, index, or effect argument.
    substitution : StaticSubstitution
        The bindings to apply.

    Returns
    -------
    StaticArgument
        The rewritten argument, dispatched to the namespace it belongs
        to.

    Raises
    ------
    TypeError
        If the term is of an unknown class.
    """
    if isinstance(term, EffectVariable) and term.identity is None:
        return substitution.effect(term.name) or term
    if isinstance(term, EffectVariable):
        return term
    if isinstance(term, EffectRef):
        return substitute_effect(term, substitution)
    if isinstance(term, (IndexVariable, IndexConstructor, ShapeIndex)) or hasattr(
        term, "sort"
    ):
        return substitute_index(term, substitution)  # type: ignore[arg-type]
    return substitute_type(term, substitution)  # type: ignore[arg-type]

substitute_row

substitute_row(row: EffectRow, substitution: StaticSubstitution) -> EffectRow

Substitute into every interface application in an effect row.

PARAMETER	DESCRIPTION
row	The row to rewrite. TYPE: EffectRow
substitution	The bindings to apply. TYPE: StaticSubstitution

RETURNS	DESCRIPTION
EffectRow	The row with each entry's interface rewritten. Instance identities and the open tail are untouched: this substitutes static arguments, and a row variable is solved by unification rather than by this substitution.

Source code in src/quivers/qiec/substitution.py

def substitute_row(row: EffectRow, substitution: StaticSubstitution) -> EffectRow:
    """Substitute into every interface application in an effect row.

    Parameters
    ----------
    row : EffectRow
        The row to rewrite.
    substitution : StaticSubstitution
        The bindings to apply.

    Returns
    -------
    EffectRow
        The row with each entry's interface rewritten. Instance
        identities and the open tail are untouched: this substitutes
        static arguments, and a row variable is solved by unification
        rather than by this substitution.
    """
    return EffectRow(
        tuple(
            RowEntry(entry.instance, substitute_effect(entry.effect, substitution))
            for entry in row.entries
        ),
        row.tail,
    )

instantiate_operation

instantiate_operation(operation: OperationDef, arguments: tuple[StaticArgument, ...], outer: StaticSubstitution = StaticSubstitution()) -> tuple[tuple[TypeExpr, ...], TypeExpr]

Instantiate an operation's signature at a request site.

PARAMETER	DESCRIPTION
operation	The declared operation. TYPE: OperationDef
arguments	Static arguments for the operation's own telescope. TYPE: tuple[StaticArgument, ...]
outer	Bindings already in force from the interface's telescope. These come first, so an operation binder of the same name shadows the interface's, which is the scoping a reader expects. TYPE: StaticSubstitution DEFAULT: StaticSubstitution()

RETURNS	DESCRIPTION
tuple[tuple[TypeExpr, ...], TypeExpr]	The instantiated parameter types and result type.

RAISES	DESCRIPTION
TypeError	If an argument is of the wrong static class for its binder.
ValueError	If the argument count is wrong, or an argument is ill-kinded.

Source code in src/quivers/qiec/substitution.py

def instantiate_operation(
    operation: OperationDef,
    arguments: tuple[StaticArgument, ...],
    outer: StaticSubstitution = StaticSubstitution(),
) -> tuple[tuple[TypeExpr, ...], TypeExpr]:
    """Instantiate an operation's signature at a request site.

    Parameters
    ----------
    operation : OperationDef
        The declared operation.
    arguments : tuple[StaticArgument, ...]
        Static arguments for the operation's own telescope.
    outer : StaticSubstitution
        Bindings already in force from the interface's telescope. These
        come first, so an operation binder of the same name shadows the
        interface's, which is the scoping a reader expects.

    Returns
    -------
    tuple[tuple[TypeExpr, ...], TypeExpr]
        The instantiated parameter types and result type.

    Raises
    ------
    TypeError
        If an argument is of the wrong static class for its binder.
    ValueError
        If the argument count is wrong, or an argument is ill-kinded.
    """
    local = instantiate_telescope(operation.telescope, arguments)
    substitution = StaticSubstitution(
        (*outer.types, *local.types),
        (*outer.indices, *local.indices),
        (*outer.effects, *local.effects),
    )
    parameter_types = tuple(
        substitute_type(argument.type, substitution) for argument in operation.arguments
    )
    return parameter_types, substitute_type(operation.result_type, substitution)

substitute_evidence

substitute_evidence(evidence: EqualityEvidence, substitution: StaticSubstitution) -> EqualityEvidence

Substitute into the equality an evidence term states.

PARAMETER	DESCRIPTION
evidence	The evidence to rewrite. TYPE: EqualityEvidence
substitution	The static bindings to apply. TYPE: StaticSubstitution

RETURNS	DESCRIPTION
EqualityEvidence	Evidence of the same class stating the substituted equality. A branch given keeps its identity, since substituting into what it proves does not make it a different piece of evidence.

RAISES	DESCRIPTION
TypeError	If the evidence is of an unknown class.

Source code in src/quivers/qiec/substitution.py

def substitute_evidence(
    evidence: EqualityEvidence,
    substitution: StaticSubstitution,
) -> EqualityEvidence:
    """Substitute into the equality an evidence term states.

    Parameters
    ----------
    evidence : EqualityEvidence
        The evidence to rewrite.
    substitution : StaticSubstitution
        The static bindings to apply.

    Returns
    -------
    EqualityEvidence
        Evidence of the same class stating the substituted equality. A
        branch given keeps its identity, since substituting into what it
        proves does not make it a different piece of evidence.

    Raises
    ------
    TypeError
        If the evidence is of an unknown class.
    """
    equality = EqualityType(
        evidence.equality.kind,
        substitute_static(evidence.equality.left, substitution),
        substitute_static(evidence.equality.right, substitution),
    )
    if isinstance(evidence, Reflexivity):
        return Reflexivity(equality)
    if isinstance(evidence, BranchGiven):
        return BranchGiven(evidence.id, equality)
    raise TypeError(f"unknown equality evidence {evidence!r}")

substitute_value

substitute_value(value: Value, substitution: StaticSubstitution) -> Value

Substitute static arguments throughout a value term.

PARAMETER	DESCRIPTION
value	The value to rewrite. TYPE: Value
substitution	The static bindings to apply. TYPE: StaticSubstitution

RETURNS	DESCRIPTION
Value	The value with every type, index, and effect position substituted. Value-level structure is untouched: this rewrites the static layer, not the data.

RAISES	DESCRIPTION
TypeError	If the value is of an unknown class.

Source code in src/quivers/qiec/substitution.py

def substitute_value(value: Value, substitution: StaticSubstitution) -> Value:
    """Substitute static arguments throughout a value term.

    Parameters
    ----------
    value : Value
        The value to rewrite.
    substitution : StaticSubstitution
        The static bindings to apply.

    Returns
    -------
    Value
        The value with every type, index, and effect position
        substituted. Value-level structure is untouched: this rewrites
        the static layer, not the data.

    Raises
    ------
    TypeError
        If the value is of an unknown class.
    """
    if isinstance(value, Var):
        return Var(
            Local(value.local.name, substitute_type(value.local.type, substitution))
        )
    if isinstance(value, LiteralValue):
        return LiteralValue(value.value, substitute_type(value.type, substitution))
    if isinstance(value, ConstructorValue):
        return ConstructorValue(
            value.constructor,
            tuple(
                substitute_static(argument, substitution)
                for argument in value.static_arguments
            ),
            tuple(substitute_value(field, substitution) for field in value.fields),
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, EvidenceValue):
        return EvidenceValue(substitute_evidence(value.evidence, substitution))
    if isinstance(value, AttachmentRef):
        return AttachmentRef(
            value.attachment, substitute_type(value.type, substitution)
        )
    if isinstance(value, TransportValue):
        return TransportValue(
            substitute_evidence(value.evidence, substitution),
            substitute_value(value.value, substitution),
            substitute_type(value.target_type, substitution),
        )
    if isinstance(value, PrimitiveApplication):
        return PrimitiveApplication(
            value.primitive,
            value.name,
            tuple(substitute_value(item, substitution) for item in value.arguments),
            substitute_type(value.result_type, substitution),
            value.origin,
        )
    if isinstance(value, TupleValue):
        return TupleValue(
            tuple(substitute_value(item, substitution) for item in value.items),
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, TensorValue):
        return TensorValue(
            tuple(substitute_value(item, substitution) for item in value.items),
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, Projection):
        return Projection(
            substitute_value(value.value, substitution),
            value.position,
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, DistributionValue):
        return DistributionValue(
            value.family,
            value.name,
            tuple(
                (name, substitute_value(argument, substitution))
                for name, argument in value.arguments
            ),
            substitute_type(value.result_type, substitution),
            value.origin,
            substitute_plate(value.plate, substitution),
        )
    if isinstance(value, Gather):
        return Gather(
            substitute_value(value.value, substitution),
            substitute_value(value.index, substitution),
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, WeightSum):
        return WeightSum(substitute_value(value.value, substitution))
    if isinstance(value, SegmentSum):
        return SegmentSum(
            substitute_value(value.value, substitution),
            substitute_value(value.index, substitution),
            substitute_index(value.groups, substitution),
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, KernelMatrix):
        return KernelMatrix(
            substitute_value(value.inputs, substitution),
            value.kernel,
            value.length_scale,
            value.jitter,
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, AffineMap):
        return AffineMap(
            substitute_value(value.weight, substitution),
            substitute_value(value.bias, substitution),
            tuple(substitute_value(item, substitution) for item in value.sources),
            value.row_offset,
            value.rows,
            value.transform,
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, TableMap):
        return TableMap(
            substitute_value(value.table, substitution),
            substitute_value(value.index, substitution),
            value.row_offset,
            value.rows,
            value.transform,
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, Reduction):
        return Reduction(
            value.operator,
            substitute_value(value.value, substitution),
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, Rowwise):
        return Rowwise(
            value.operator,
            substitute_value(value.value, substitution),
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, Comprehension):
        return Comprehension(
            Local(value.binder.name, substitute_type(value.binder.type, substitution)),
            substitute_index(value.extent, substitution),
            substitute_value(value.body, substitution),
            substitute_type(value.result_type, substitution),
        )
    if isinstance(value, LogDensity):
        return LogDensity(
            substitute_value(value.sampleable, substitution),
            substitute_value(value.value, substitution),
            value.origin,
            tuple(
                PlateAxis(axis.name, substitute_index(axis.size, substitution))
                for axis in value.batch
            ),
        )
    if isinstance(value, SiteValue):
        return SiteValue(value.label, substitute_type(value.result_type, substitution))
    raise TypeError(f"unknown value term {value!r}")

substitute_request

substitute_request(request: EffectRequest, substitution: StaticSubstitution) -> EffectRequest

Substitute static arguments throughout an effect request.

PARAMETER	DESCRIPTION
request	The request to rewrite. TYPE: EffectRequest
substitution	The static bindings to apply. TYPE: StaticSubstitution

RETURNS	DESCRIPTION
EffectRequest	The request against the substituted interface application, with its own static and value arguments and result type rewritten. The instance, the operation, and the site are identities and do not move.

Source code in src/quivers/qiec/substitution.py

def substitute_request(
    request: EffectRequest,
    substitution: StaticSubstitution,
) -> EffectRequest:
    """Substitute static arguments throughout an effect request.

    Parameters
    ----------
    request : EffectRequest
        The request to rewrite.
    substitution : StaticSubstitution
        The static bindings to apply.

    Returns
    -------
    EffectRequest
        The request against the substituted interface application, with
        its own static and value arguments and result type rewritten. The
        instance, the operation, and the site are identities and do not
        move.
    """
    return EffectRequest(
        request.instance,
        substitute_effect(request.effect, substitution),
        request.operation,
        tuple(
            substitute_static(argument, substitution)
            for argument in request.static_arguments
        ),
        tuple(
            substitute_value(argument, substitution) for argument in request.arguments
        ),
        substitute_type(request.result_type, substitution),
        request.origin,
    )

substitute_computation

substitute_computation(computation: Computation, substitution: StaticSubstitution) -> Computation

Substitute static arguments throughout a computation.

Capture cannot occur, and the reason is structural rather than a freshening pass. A substitution binds declaration binders, which carry no identity and are matched by name. Every binder a computation introduces is rigid: a case branch's skolems are built with derived StaticVariableIds, and substitute_type and substitute_static return a variable carrying an identity unchanged. So a branch's own binders are invisible to substitution while references to an enclosing declaration binder inside that branch are rewritten, which is exactly the capture-avoiding behavior.

PARAMETER	DESCRIPTION
computation	The computation to rewrite. TYPE: Computation
substitution	The static bindings to apply. TYPE: StaticSubstitution

RETURNS	DESCRIPTION
Computation	The computation with every static position substituted. Identities are preserved throughout: a call still names the same callee, a handle the same handler, and an allocation the same instance.

RAISES	DESCRIPTION
TypeError	If the computation, or a term nested in it, is of an unknown class.

Source code in src/quivers/qiec/substitution.py

def substitute_computation(
    computation: Computation,
    substitution: StaticSubstitution,
) -> Computation:
    """Substitute static arguments throughout a computation.

    Capture cannot occur, and the reason is structural rather than a
    freshening pass. A substitution binds declaration binders, which
    carry no identity and are matched by name. Every binder a computation
    introduces is rigid: a case branch's skolems are built with derived
    `StaticVariableId`s, and `substitute_type` and `substitute_static`
    return a variable carrying an identity unchanged. So a branch's own
    binders are invisible to substitution while references to an
    enclosing declaration binder inside that branch are rewritten, which
    is exactly the capture-avoiding behavior.

    Parameters
    ----------
    computation : Computation
        The computation to rewrite.
    substitution : StaticSubstitution
        The static bindings to apply.

    Returns
    -------
    Computation
        The computation with every static position substituted.
        Identities are preserved throughout: a call still names the same
        callee, a handle the same handler, and an allocation the same
        instance.

    Raises
    ------
    TypeError
        If the computation, or a term nested in it, is of an unknown
        class.
    """
    if isinstance(computation, Return):
        return Return(substitute_value(computation.value, substitution))
    if isinstance(computation, Bind):
        return Bind(
            Local(
                computation.binder.name,
                substitute_type(computation.binder.type, substitution),
            ),
            substitute_computation(computation.first, substitution),
            substitute_computation(computation.then, substitution),
        )
    if isinstance(computation, Perform):
        return Perform(substitute_request(computation.request, substitution))
    if isinstance(computation, Handle):
        return Handle(
            computation.instance,
            computation.handler,
            substitute_computation(computation.computation, substitution),
            tuple(
                substitute_static(argument, substitution)
                for argument in computation.static_arguments
            ),
        )
    if isinstance(computation, Case):
        return Case(
            substitute_value(computation.scrutinee, substitution),
            CaseMotive(
                computation.motive.indices,
                substitute_type(computation.motive.result_type, substitution),
            ),
            tuple(
                CaseBranch(
                    branch.constructor,
                    tuple(
                        substitute_static(argument, substitution)
                        for argument in branch.static_arguments
                    ),
                    tuple(
                        Local(field.name, substitute_type(field.type, substitution))
                        for field in branch.fields
                    ),
                    substitute_computation(branch.body, substitution),
                    branch.scope,
                )
                for branch in computation.branches
            ),
        )
    if isinstance(computation, If):
        return If(
            substitute_value(computation.condition, substitution),
            substitute_computation(computation.then, substitution),
            substitute_computation(computation.otherwise, substitution),
        )
    if isinstance(computation, Call):
        return Call(
            computation.callee,
            computation.name,
            tuple(
                substitute_static(argument, substitution)
                for argument in computation.static_arguments
            ),
            tuple(
                substitute_value(argument, substitution)
                for argument in computation.arguments
            ),
            substitute_type(computation.result_type, substitution),
            substitute_row(computation.effects, substitution),
            computation.origin,
        )
    if isinstance(computation, Resume):
        return Resume(
            substitute_value(computation.value, substitution),
            computation.origin,
        )
    if isinstance(computation, NewInstance):
        return NewInstance(
            computation.instance,
            substitute_effect(computation.effect, substitution),
            substitute_computation(computation.body, substitution),
            computation.origin,
        )
    raise TypeError(f"unknown computation term {computation!r}")