implement "instantiation" methods in chalk integration impl #55098

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_goal
• instantiate_ex_clause

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.