Validation for graphs with resource variables

[croyzor]

Currently, extension validation assumes that hugrs should be extensions-closed. Which is to say that every node in the hugr should have concrete extensions for its incoming and outgoing edges. This makes sense for a static function definition, but may be needlessly restrictive for other types of hugrs.

Concretely, in the below diagram, input0 could have an open extension variable as its input extensions. Extension inference could conclude that the rest of the graph makes sense given any value for this variable, but validation would complain that DFG0's input doesn't have a concrete extension set!

flowchart
    direction TB
    subgraph DFG0
        direction TB
        subgraph DFG1
            direction TB
            Input1 --> op0
            op0 --> op1
            op1 --> Output1
        end
        Input0 --> DFG1
        Input1 --> DFG1
        DFG1 --> Output0
    end

Loading

The workaround for this lack of more permissive extension validation as introduced by #456 is for extension inference to return a closure -- a mapping of solutions for extension sets in the graph which depend on open variables which it then passes to validation, allowing validation to operate on an extension-closed hugr.

I.e. extension inference checks that there is a solution given any value for the remaining extension variables, and for validation it sets their values to the empty extension set.

[acl-cqc]

Update: there are a few other issues relevant here:

• Handle ExtensionSet type parameters in inference #713
• refactor: Combine ExtensionSolutions (no separate closure) #884 with validate_with_extension_closure
• No polymorphic closures #904

Also note that we already validate that

• type-variables (including ExtensionSet ones) appearing in TypeArgs are declared
• similarly for all port kinds

Thus, we think the only things remaining are:

• the first match might want to include other LeafOps that can include Types (e.g. Noop). However, given Move Noop, MakeTuple, UnpackTuple, Tag to prelude extension #816, this may be unnecessary
• as well as validating the port-kinds of each node's signature, we should also validate the extension-delta

[acl-cqc]

New approach using extension typevars should let us do something similar to this following #709