With Coq master, we otherwise fail to infer instances with subG_savedAnythingΣ, which leads to goals like

> looking for (subG
>                       (@savedAnythingΣ (@ofe_funCF val (fun _ : val => laterCF idCF))
>                          ?cFunctorContractive0) Σ)