Bad interaction between `apply:` and typeclass solver

[Tragicus]

It seems that apply: calls the typeclass solver on the goal it produces and somehow accepts a partial solution from elpi's typeclass solver. I am surprised both by the fact that the typeclass solver gives a partial answer and that apply: accepts it.

From Corelib Require Import ssreflect.

Class A := {}.

Goal (nat -> A) -> A.
Proof.
move=> hyp.
apply: id.
(* Goal : A *)
Abort.

From elpi Require Import tc.

Class B := {}.

Goal (nat -> B) -> B.
Proof.
move=> hyp.
apply: id.
(* Goal : nat *)
Abort.

Also, if I replace B by A in the last Goal, the apply: id command fails, which is even weirder.

Goal (nat -> A) -> A.
Proof.
move=> hyp.
Fail apply: id.

[gares]

Would you be so nice to attach the output of Set Debug Typeclasses for the first run? I suspect it runs, solves it using hyp, but then we toss the result as inconclusive. Maybe because the nat goal is not shelved.

And there is clearly some bug...

[Tragicus]

Sure

Calling typeclass resolution with flags: depth = ∞,unique = false,fail = false

1: looking for A without backtracking

1.1: simple apply hyp on A, 1 subgoal(s)

1.1-1 : nat

1.1-1: looking for nat without backtracking

1.1-1: no match for nat, 0 possibilities

With Set Typeclasses Debug Verbosity 2, the log ends with

1.1: simple apply hyp failed with: Proof-search failed.

Goal 1 has no more solutions, returning exception: Proof-search failed.