pub fn refine_inference_and_verify(
    compilation_env: &mut CompilationEnv,
    struct_declared_abilities: &UniqueMap<ModuleIdent, UniqueMap<StructName, AbilitySet>>,
    signature: &FunctionSignature,
    acquires: &BTreeMap<StructName, Loc>,
    locals: &UniqueMap<Var, SingleType>,
    cfg: &mut BlockCFG<'_>,
    infinite_loop_starts: &BTreeSet<Label>
)