Fix #11140: Bidirectionality hints perform (surprising?) simplification

We typecheck arguments like previously, using bidirectionality hints,
but ultimately replace them with user-provided arguments on which we
replay coercion traces.

This is a fix which should be easy to backport, but there are two
directions of future work:
- Coercion traces for `Program` coercions (in these cases, we currently
use the inferred arguments)
- Separate the Coercion API in two phases: inference and application of
coercions. It will make the approach taken here cleaner, and probably
make it easier to interleave typing steps with coercion inference.

Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

1 files changed, 11 insertions, 0 deletions

diff --git a/test-suite/bugs/bug_11140.v b/test-suite/bugs/bug_11140.v
new file mode 100644
index 0000000000..ca806ea324
--- /dev/null
+++ b/test-suite/bugs/bug_11140.v
@@ -0,0 +1,11 @@
+Axiom T : nat -> Prop.
+Axiom f : forall x, T x.
+Arguments f & x.
+
+Lemma test : (f (1 + _) : T 2) = f 2.
+match goal with
+| |- (f (1 + 1) = f 2) => idtac
+| |- (f 2 = f 2) => fail (* Issue 11140 *)
+| |- _ => fail
+end.
+Abort.