Legacy unification (apply) + Polymorphic Inductive Cumulativity results in confusing and suspicious differences between evar and evar-free behavior

[JasonGross]

Description of the problem

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-R" "src" "QuickChick" "-I" "plugin" "-top" "QuickChick.Instances" "-Q" "/home/jgross/.local64/coq/coq-8.16.0+17325/lib/coq/user-contrib/Equations" "Equations" "-Q" "/home/jgross/.local64/coq/coq-8.16.0+17325/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/home/jgross/.local64/coq/coq-8.16.0+17325/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/home/jgross/.local64/coq/coq-8.16.0+17325/lib/coq/user-contrib/SimpleIO" "SimpleIO" "-Q" "/home/jgross/.local64/coq/coq-8.16.0+17325/lib/coq/user-contrib/mathcomp" "mathcomp") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 817 lines to 20 lines, then from 33 lines to 943 lines, then from 941 lines to 32 lines, then from 45 lines to 1419 lines, then from 1409 lines to 1658 lines, then from 1625 lines to 21 lines, then from 34 lines to 919 lines, then from 922 lines to 21 lines, then from 34 lines to 1268 lines, then from 1262 lines to 21 lines, then from 26 lines to 21 lines, then from 35 lines to 21 lines, then from 34 lines to 71 lines, then from 76 lines to 21 lines, then from 34 lines to 153 lines, then from 158 lines to 29 lines, then from 34 lines to 29 lines *)
(* coqc version 8.16.0 compiled with OCaml 4.11.2
   coqtop version 8.16.0
   Expected coqc runtime on this file: 0.069 sec *)
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
{ ret : forall {t : Type@{d}}, t -> m t
; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u
}.
Opaque ret.
Set Printing Universes.
Set Printing All.
Section __.
  Polymorphic Universes GTu0 MGu0 Pu0 Pu1 RSu0.
  Lemma foo
    : forall (A : Type@{_}) (s : nat) (a : A)
             (T : forall _ : Type@{GTu0}, Type@{max(Set,RSu0,GTu0)})
             (m : Monad@{GTu0 MGu0} T) (s0 : forall (_ : T (option A)) (_ : nat), option A -> Prop)
             (H3 : s0 (@ret@{GTu0 MGu0} T m (option A) (@None A)) s (@Some A a)) (k : Prop),
    exists a', forall
      (_ : forall _ : s0 (@ret@{Pu0 Pu1} T m (option A) (@None A)) s (@Some A a'), k), True.
    intros ?????? H3; eexists; intro H4.
    assert_succeeds (pose (H4 H3)).
    Fail apply H4 in H3.
    (* The command has indeed failed with message:
Unable to apply lemma of type "forall _ : s0 (@ret@{Pu0 Pu1} T m (option A) (@None A)) s (@Some A ?a'), k"
on hypothesis of type "s0 (@ret@{GTu0 MGu0} T m (option A) (@None A)) s (@Some A a)".
*)
    instantiate (1:=a) in H4.
    apply H4 in H3. (* success *)
    exact I.
  Defined.
End __.

Note that pose succeeds both with and without cumulativity, and apply succeeds in the evar-free case with cumulativity and in both cases without cumulativity. I think this is probably a bug in apply and it should succeed also in the with-evar case in the presence of cumulativity.

cc ... @SkySkimmer ?

Coq Version

8.16

[SkySkimmer]

Old unification only understands inductive cumulativity in the syntactic equality fast path IIRC #14758

[JasonGross]

Can the situation be improved? Or can #17565 be granted?