Handle ExtensionSet type parameters in inference

[croyzor]

No description provided.

[acl-cqc]

@croyzor is this just "deal with them when we find them" or the broader "use extension typevars instead of the current notion of variables in inference"? If the former, do we have an issue for the latter?

[croyzor]

I think it's probably the former. I don't think there's a separate issue for the latter yet

[acl-cqc]

Ok, so I think there are two possibilities here:

• Track the location, specifically the number of enclosing binders, for each Meta (created from a Hugr location). When copying a solution (which must come from a Meta - you could pick any if there are several, all solutions must be equivalent) to another Meta, renumber any variables in the solution according to the difference in the #binders with the Meta to which the solution is copied.
• Whenever new binders are found (which basically means function definitions), recursively solve the problem within those binders (within the function) separately from (and before) the outer problem. The input/output extensions of the FuncDefn node itself should not depend upon those variables (that's an error) - said variables only appear in the (function type of the) static output of the FuncDefn node. This is used at call nodes, but only after instantiation, i.e. the type-args to the Call give us ExtensionSets to substitute in for those variables.

TBH I think the latter is saner, and probably easier.

[acl-cqc]

...particularly given the nested FuncDefn cannot depend on TypeParams declared by any enclosing FuncDefn, e.g.

hugr/quantinuum-hugr/src/hugr/validate.rs

Lines 591 to 597 in a2e4d05

	// For FuncDefn's, only the type variables declared by the FuncDefn can be referred to by nodes
	// inside the function. (The same would be true for FuncDecl's, but they have no child nodes.)
	let var_decls = if let OpType::FuncDefn(FuncDefn { signature, .. }) = op_type {
	signature.params()
	} else {
	var_decls
	};

[acl-cqc]

I think it's probably the former. I don't think there's a separate issue for the latter yet

Sorry, I've missed this in my last two comments above - this now is the latter ("use extensionset typevars instead of the current notion of variables in inference"). However, maybe we don't need to do anything just to deal with these, at least after #906 - at that point there will be no nested binders, so (within the scope of a binder, i.e. a FuncDefn) the same DeBruijn index always means the same type variable. We probably should check that ExtensionSet TypeVars don't "escape" their binders (and one way, though not the only way, to do that would be to solve recursively, as suggested) - but perhaps the same solution does both "deal with them when we find them" and the broader "use extension typevars instead of variables"...

[acl-cqc]

Further discussion - in theory it should be possible to define a Hugr with:

• A FuncDefn polymorphic over an ExtensionSet.
  • Given it is difficult to put an ExtensionSet-typevar into a Lift node (at least without refactor: Generalise Lift nodes to ExtensionSets #819), this might have to be something higher-order, e.g. apply_twice<E: Extensions>(in: Tuple[int,int], f: int --E-->int) --E--> Tuple[int,int]
• A call to that function with a concrete ExtensionSet argument
• extension-delta for the whole Hugr equal to that concrete ExtensionSet argument

If that all works then we may not need anything more

[acl-cqc]

Tests in previous

Further discussion - in theory it should be possible to define a Hugr with:

• A FuncDefn polymorphic over an ExtensionSet.

  • Given it is difficult to put an ExtensionSet-typevar into a Lift node (at least without refactor: Generalise Lift nodes to ExtensionSets #819), this might have to be something higher-order, e.g. apply_twice<E: Extensions>(in: Tuple[int,int], f: int --E-->int) --E--> Tuple[int,int]

• A call to that function with a concrete ExtensionSet argument

• extension-delta for the whole Hugr equal to that concrete ExtensionSet argument

If that all works then we may not need anything more

These tests added in #939 and #1003.

Further work in #709 should handle the rest