There are a few methods in the "chalk integration" impl that have the job of "instantiating" canonical things with inference variables and the like. Actually, these methods have a somewhat bigger job: they are also supposed to create the surrounding inference context.
There are two such methods:
PR #54858 introduces a enter_with_canonical method that is more-or-less exactly what we need here (link). Hopefully that will land soon.
For reference, the implementations of these methods from the chalk project are here.
There are a few methods in the "chalk integration" impl that have the job of "instantiating" canonical things with inference variables and the like. Actually, these methods have a somewhat bigger job: they are also supposed to create the surrounding inference context.
There are two such methods:
instantiate_ucanonical_goalinstantiate_ex_clausePR #54858 introduces a
enter_with_canonicalmethod that is more-or-less exactly what we need here (link). Hopefully that will land soon.For reference, the implementations of these methods from the chalk project are here.