Merge PR #10049: [elaboration] Bidirectionality hints

Ack-by: RalfJung
Reviewed-by: SkySkimmer
Reviewed-by: gares
Ack-by: maximedenes

10 files changed, 346 insertions, 52 deletions

diff --git a/doc/changelog/02-specification-language/10049-bidi-app.rst b/doc/changelog/02-specification-language/10049-bidi-app.rst
new file mode 100644
index 0000000000..79678c5242
--- /dev/null
+++ b/doc/changelog/02-specification-language/10049-bidi-app.rst
@@ -0,0 +1,6 @@
+- New annotation in `Arguments` for bidirectionality hints: it is now possible
+  to tell type inference to use type information from the context once the `n`
+  first arguments of an application are known. The syntax is:
+  `Arguments foo x y & z`.
+  `#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with
+  help from Enrico Tassi
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index c1af4d067f..8c5ad785e4 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2448,3 +2448,45 @@ types and functions of a :g:`Uint63` module. Said module is not produced by
 extraction. Instead, it has to be provided by the user (if they want to compile
 or execute the extracted code). For instance, an implementation of this module
 can be taken from the kernel of Coq.
+
+Bidirectionality hints
+----------------------
+
+When type-checking an application, Coq normally does not use information from
+the context to infer the types of the arguments. It only checks after the fact
+that the type inferred for the application is coherent with the expected type.
+Bidirectionality hints make it possible to specify that after type-checking the
+first arguments of an application, typing information should be propagated from
+the context to help inferring the types of the remaining arguments.
+
+.. cmd:: Arguments @qualid {* @ident__1 } & {* @ident__2}
+   :name: Arguments (bidirectionality hints)
+
+   This commands tells the typechecking algorithm, when type-checking
+   applications of :n:`@qualid`, to first type-check the arguments in
+   :n:`@ident__1` and then propagate information from the typing context to
+   type-check the remaining arguments (in :n:`@ident__2`).
+
+.. example::
+
+   In a context where a coercion was declared from ``bool`` to ``nat``:
+
+   .. coqtop:: in reset
+
+      Definition b2n (b : bool) := if b then 1 else 0.
+      Coercion b2n : bool >-> nat.
+
+   Coq cannot automatically coerce existential statements over ``bool`` to
+   statements over ``nat``, because the need for inserting a coercion is known
+   only from the expected type of a subterm:
+
+   .. coqtop:: all
+
+      Fail Check (ex_intro _ true _ : exists n : nat, n > 0).
+
+   However, a suitable bidirectionality hint makes the example work:
+
+   .. coqtop:: all
+
+      Arguments ex_intro _ _ & _ _.
+      Check (ex_intro _ true _ : exists n : nat, n > 0).
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f2b8671a48..c7b657f96c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -52,6 +52,18 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
 let (!!) env = GlobEnv.env env
 
+let bidi_hints =
+  Summary.ref (GlobRef.Map.empty : int GlobRef.Map.t) ~name:"bidirectionalityhints"
+
+let add_bidirectionality_hint gr n =
+  bidi_hints := GlobRef.Map.add gr n !bidi_hints
+
+let get_bidirectionality_hint gr =
+  GlobRef.Map.find_opt gr !bidi_hints
+
+let clear_bidirectionality_hint gr =
+  bidi_hints := GlobRef.Map.remove gr !bidi_hints
+
 (************************************************************************)
 (* This concerns Cases *)
 open Inductive
@@ -635,24 +647,36 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env :
     let sigma, fj = pretype empty_tycon env sigma f in
     let floc = loc_of_glob_constr f in
     let length = List.length args in
+    let nargs_before_bidi =
+      (* if `f` is a global, we retrieve bidirectionality hints *)
+      try
+        let (gr,_) = destRef sigma fj.uj_val in
+        Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints
+      with DestKO ->
+        length
+    in
     let candargs =
-	(* Bidirectional typechecking hint: 
-	   parameters of a constructor are completely determined
-	   by a typing constraint *)
+      (* Bidirectional typechecking hint:
+         parameters of a constructor are completely determined
+         by a typing constraint *)
+      (* This bidirectionality machinery is the one of `Program` for
+         constructors and is orthogonal to bidirectionality hints. However, we
+         could probably factorize both by providing default bidirectionality hints
+         for constructors corresponding to their number of parameters. *)
       if program_mode && length > 0 && isConstruct sigma fj.uj_val then
-	match tycon with
-	| None -> []
-	| Some ty ->
+        match tycon with
+        | None -> []
+        | Some ty ->
           let ((ind, i), u) = destConstruct sigma fj.uj_val in
           let npars = inductive_nparams !!env ind in
-	    if Int.equal npars 0 then []
-	    else
-	      try
-                let IndType (indf, args) = find_rectype !!env sigma ty in
-	  	let ((ind',u'),pars) = dest_ind_family indf in
-	  	  if eq_ind ind ind' then List.map EConstr.of_constr pars
-	  	  else (* Let the usual code throw an error *) []
-	      with Not_found -> []
+          if Int.equal npars 0 then []
+          else
+            try
+              let IndType (indf, args) = find_rectype !!env sigma ty in
+              let ((ind',u'),pars) = dest_ind_family indf in
+              if eq_ind ind ind' then List.map EConstr.of_constr pars
+              else (* Let the usual code throw an error *) []
+            with Not_found -> []
       else []
     in
     let app_f = 
@@ -662,20 +686,29 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env :
         let p = Projection.make p false in
         let npars = Projection.npars p in
         fun n ->
-          if n == npars + 1 then fun _ v -> mkProj (p, v)
+          if Int.equal n npars then fun _ v -> mkProj (p, v)
           else fun f v -> applist (f, [v])
       | _ -> fun _ f v -> applist (f, [v])
     in
-    let rec apply_rec env sigma n resj candargs = function
-      | [] -> sigma, resj
+    let rec apply_rec env sigma n resj candargs bidiargs = function
+      | [] -> sigma, resj, List.rev bidiargs
       | c::rest ->
+        let bidi = n >= nargs_before_bidi in
         let argloc = loc_of_glob_constr c in
         let sigma, resj = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in
         let resty = whd_all !!env sigma resj.uj_type in
         match EConstr.kind sigma resty with
         | Prod (na,c1,c2) ->
           let tycon = Some c1 in
-          let sigma, hj = pretype tycon env sigma c in
+          let (sigma, hj), bidiargs =
+            if bidi && Option.has_some tycon then
+              (* We want to get some typing information from the context before
+              typing the argument, so we replace it by an existential
+              variable *)
+              let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in
+              (sigma, make_judge c_hole c1), (c_hole, c) :: bidiargs
+            else pretype tycon env sigma c, bidiargs
+          in
           let sigma, candargs, ujval =
             match candargs with
             | [] -> sigma, [], j_val hj
@@ -687,30 +720,45 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env :
                   sigma, args, nf_evar sigma (j_val hj)
               end
           in
-            let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in
-            let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
-	    let j = { uj_val = value; uj_type = typ } in
-            apply_rec env sigma (n+1) j candargs rest
-	  | _ ->
-            let sigma, hj = pretype empty_tycon env sigma c in
-	      error_cant_apply_not_functional
-                ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|]
+          let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in
+          let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
+          let j = { uj_val = value; uj_type = typ } in
+          apply_rec env sigma (n+1) j candargs bidiargs rest
+        | _ ->
+          let sigma, hj = pretype empty_tycon env sigma c in
+          error_cant_apply_not_functional
+            ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|]
     in
-    let sigma, resj = apply_rec env sigma 1 fj candargs args in
+    let sigma, resj, bidiargs = apply_rec env sigma 0 fj candargs [] args in
     let sigma, resj =
       match EConstr.kind sigma resj.uj_val with
       | App (f,args) ->
-          if Termops.is_template_polymorphic_ind !!env sigma f then
-	    (* Special case for inductive type applications that must be 
-	       refreshed right away. *)
-            let c = mkApp (f, args) in
-            let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in
-            let t = Retyping.get_type_of !!env sigma c in
-            sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t
-          else sigma, resj
+        if Termops.is_template_polymorphic_ind !!env sigma f then
+          (* Special case for inductive type applications that must be
+             refreshed right away. *)
+          let c = mkApp (f, args) in
+          let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in
+          let t = Retyping.get_type_of !!env sigma c in
+          sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t
+        else sigma, resj
       | _ -> sigma, resj
     in
-    inh_conv_coerce_to_tycon ?loc env sigma resj tycon
+    let sigma, t = inh_conv_coerce_to_tycon ?loc env sigma resj tycon in
+    let refine_arg sigma (newarg,origarg) =
+      (* Refine an argument (originally `origarg`) represented by an evar
+         (`newarg`) to use typing information from the context *)
+      (* Recover the expected type of the argument *)
+      let ty = Retyping.get_type_of !!env sigma newarg in
+      (* Type the argument using this expected type *)
+      let sigma, j = pretype (Some ty) env sigma origarg in
+      (* Unify the (possibly refined) existential variable with the
+      (typechecked) original value *)
+      Evarconv.unify_delay !!env sigma newarg (j_val j)
+    in
+    (* We now refine any arguments whose typing was delayed for
+       bidirectionality *)
+    let sigma = List.fold_left refine_arg sigma bidiargs in
+    (sigma, t)
 
   | GLambda(name,bk,c1,c2) ->
     let sigma, tycon' =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 1037cf6cc5..c0a95e73c6 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -14,12 +14,22 @@
    into elementary ones, insertion of coercions and resolution of
    implicit arguments. *)
 
+open Names
 open Environ
 open Evd
 open EConstr
 open Glob_term
 open Ltac_pretype
 
+val add_bidirectionality_hint : GlobRef.t -> int -> unit
+(** A bidirectionality hint `n` for a global `g` tells the pretyper to use
+    typing information from the context after typing the `n` for arguments of an
+    application of `g`. *)
+
+val get_bidirectionality_hint : GlobRef.t -> int option
+
+val clear_bidirectionality_hint : GlobRef.t -> unit
+
 val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
   glob_level -> Univ.Level.t
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fca33a24bf..f55bfb504f 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -304,6 +304,12 @@ let print_inductive_argument_scopes =
   print_args_data_of_inductive_ids
     Notation.find_arguments_scope (Option.has_some) print_argument_scopes
 
+let print_bidi_hints gr =
+  match Pretyping.get_bidirectionality_hint gr with
+  | None -> []
+  | Some nargs ->
+    [str "Using typing information from context after typing the " ++ int nargs ++ str " first arguments"]
+
 (*********************)
 (* "Locate" commands *)
 
@@ -841,7 +847,8 @@ let print_about_any ?loc env sigma k udecl =
 	print_name_infos ref @
 	(if Pp.ismt rb then [] else [rb]) @
 	print_opacity ref @
-	[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
+  print_bidi_hints ref @
+  [hov 0 (str "Expands to: " ++ pr_located_qualid k)])
   | Syntactic kn ->
     let () = match Syntax_def.search_syntactic_definition kn with
     | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref
diff --git a/test-suite/success/BidirectionalityHints.v b/test-suite/success/BidirectionalityHints.v
new file mode 100644
index 0000000000..284cdc871b
--- /dev/null
+++ b/test-suite/success/BidirectionalityHints.v
@@ -0,0 +1,114 @@
+From Coq Require Import Utf8.
+Set Default Proof Using "Type".
+
+Module SimpleExamples.
+
+Axiom c : bool -> nat.
+Coercion c : bool >-> nat.
+Inductive Boxed A := Box (a : A).
+Arguments Box {A} & a.
+Check Box true : Boxed nat.
+
+(* Here we check that there is no regression due e.g. to refining arguments
+   in the wrong order *)
+Axiom f : forall b : bool, (if b then bool else nat) -> Type.
+Check f true true : Type.
+Arguments f & _ _.
+Check f true true : Type.
+
+End SimpleExamples.
+
+Module Issue7910.
+
+Local Set Universe Polymorphism.
+
+(** Telescopes *)
+Inductive tele : Type :=
+  | TeleO : tele
+  | TeleS {X} (binder : X → tele) : tele.
+
+Arguments TeleS {_} _.
+
+(** The telescope version of Coq's function type *)
+Fixpoint tele_fun (TT : tele) (T : Type) : Type :=
+  match TT with
+  | TeleO => T
+  | TeleS b => ∀ x, tele_fun (b x) T
+  end.
+
+Notation "TT -t> A" :=
+  (tele_fun TT A) (at level 99, A at level 200, right associativity).
+
+(** An eliminator for elements of [tele_fun].
+    We use a [fix] because, for some reason, that makes stuff print nicer
+    in the proofs in iris:bi/lib/telescopes.v *)
+Definition tele_fold {X Y} {TT : tele} (step : ∀ {A : Type}, (A → Y) → Y) (base : X → Y)
+  : (TT -t> X) → Y :=
+  (fix rec {TT} : (TT -t> X) → Y :=
+     match TT as TT return (TT -t> X) → Y with
+     | TeleO => λ x : X, base x
+     | TeleS b => λ f, step (λ x, rec (f x))
+     end) TT.
+Arguments tele_fold {_ _ !_} _ _ _ /.
+
+(** A sigma-like type for an "element" of a telescope, i.e. the data it
+  takes to get a [T] from a [TT -t> T]. *)
+Inductive tele_arg : tele → Type :=
+| TargO : tele_arg TeleO
+(* the [x] is the only relevant data here *)
+| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder).
+
+Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T :=
+  λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T :=
+     match a in tele_arg TT return (TT -t> T) → T with
+     | TargO => λ t : T, t
+     | TargS x a => λ f, rec a (f x)
+     end) TT a f.
+Arguments tele_app {!_ _} & _ !_ /.
+
+Coercion tele_arg : tele >-> Sortclass.
+Coercion tele_app : tele_fun >-> Funclass.
+
+(** Operate below [tele_fun]s with argument telescope [TT]. *)
+Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U :=
+  match TT as TT return (TT → U) → TT -t> U with
+  | TeleO => λ F, F TargO
+  | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *)
+                  tele_bind (λ a, F (TargS x a))
+  end.
+Arguments tele_bind {_ !_} _ /.
+
+(** Telescopic quantifiers *)
+Definition tforall {TT : tele} (Ψ : TT → Prop) : Prop :=
+  tele_fold (λ (T : Type) (b : T → Prop), ∀ x : T, b x) (λ x, x) (tele_bind Ψ).
+Arguments tforall {!_} _ /.
+Definition texist {TT : tele} (Ψ : TT → Prop) : Prop :=
+  tele_fold ex (λ x, x) (tele_bind Ψ).
+Arguments texist {!_} _ /.
+
+Notation "'∀..' x .. y , P" := (tforall (λ x, .. (tforall (λ y, P)) .. ))
+  (at level 200, x binder, y binder, right associativity,
+  format "∀..  x  ..  y ,  P").
+Notation "'∃..' x .. y , P" := (texist (λ x, .. (texist (λ y, P)) .. ))
+  (at level 200, x binder, y binder, right associativity,
+  format "∃..  x  ..  y ,  P").
+
+(** The actual test case *)
+Definition test {TT : tele} (t : TT → Prop) : Prop :=
+  ∀.. x, t x ∧ t x.
+
+Notation "'[TEST' x .. z , P ']'" :=
+  (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)))
+        (tele_app (λ x, .. (λ z, P) ..)))
+  (x binder, z binder).
+Notation "'[TEST2' x .. z , P ']'" :=
+  (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)))
+        (tele_app (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)))
+                  (λ x, .. (λ z, P) ..)))
+  (x binder, z binder).
+
+Check [TEST (x y : nat), x = y].
+
+Check [TEST2 (x y : nat), x = y].
+
+End Issue7910.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 7c8c2b10ab..5eec8aed1e 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -752,6 +752,7 @@ GRAMMAR EXTEND Gram
         mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] ->
          { let mods = match mods with None -> [] | Some l -> List.flatten l in
          let slash_position = ref None in
+         let ampersand_position = ref None in
          let rec parse_args i = function
            | [] -> []
            | `Id x :: args -> x :: parse_args (i+1) args
@@ -760,10 +761,15 @@ GRAMMAR EXTEND Gram
                 (slash_position := Some i; parse_args i args)
               else
                 user_err Pp.(str "The \"/\" modifier can occur only once")
+           | `Ampersand :: args ->
+             if Option.is_empty !ampersand_position then
+               (ampersand_position := Some i; parse_args i args)
+             else
+               user_err Pp.(str "The \"&\" modifier can occur only once")
          in
          let args = parse_args 0 (List.flatten args) in
          let more_implicits = Option.default [] more_implicits in
-         VernacArguments (qid, args, more_implicits, !slash_position, mods) }
+         VernacArguments (qid, args, more_implicits, !slash_position, !ampersand_position, mods) }
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->
 	   { VernacReserve bl }
@@ -785,6 +791,7 @@ GRAMMAR EXTEND Gram
       | IDENT "default"; IDENT "implicits" -> { [`DefaultImplicits] }
       | IDENT "clear"; IDENT "implicits" -> { [`ClearImplicits] }
       | IDENT "clear"; IDENT "scopes" -> { [`ClearScopes] }
+      | IDENT "clear"; IDENT "bidirectionality"; IDENT "hint" -> { [`ClearBidiHint] }
       | IDENT "rename" -> { [`Rename] }
       | IDENT "assert" -> { [`Assert] }
       | IDENT "extra"; IDENT "scopes" -> { [`ExtraScopes] }
@@ -810,6 +817,7 @@ GRAMMAR EXTEND Gram
              notation_scope=notation_scope;
              implicit_status = NotImplicit}] }
     | "/" -> { [`Slash] }
+    | "&" -> { [`Ampersand] }
     | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
        { let f x = match sc, x with
          | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 2e97a169cc..e307c0c268 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1047,7 +1047,7 @@ open Pputils
                 | Some Flags.Current -> [SetOnlyParsing]
                 | Some v -> [SetCompatVersion v]))
         )
-      | VernacArguments (q, args, more_implicits, nargs, mods) ->
+      | VernacArguments (q, args, more_implicits, nargs, nargs_before_bidi, mods) ->
         return (
           hov 2 (
             keyword "Arguments" ++ spc() ++
@@ -1058,22 +1058,23 @@ open Pputils
                 | Impargs.Implicit -> str "[" ++ x ++ str "]"
                 | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}"
                 | Impargs.NotImplicit -> x in
-              let rec print_arguments n l =
-                match n, l with
-                  | Some 0, l -> spc () ++ str"/" ++ print_arguments None l
-                  | _, [] -> mt()
-                  | n, { name = id; recarg_like = k;
+              let rec print_arguments n nbidi l =
+                match n, nbidi, l with
+                  | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l
+                  | _, Some 0, l -> spc () ++ str"|" ++ print_arguments n None l
+                  | _, _, [] -> mt()
+                  | n, nbidi, { name = id; recarg_like = k;
                          notation_scope = s;
                          implicit_status = imp } :: tl ->
                     spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++
-                      print_arguments (Option.map pred n) tl
+                    print_arguments (Option.map pred n) (Option.map pred nbidi) tl
               in
               let rec print_implicits = function
                 | [] -> mt ()
                 | (name, impl) :: rest ->
                    spc() ++ pr_br impl (Name.print name) ++ print_implicits rest
               in
-              print_arguments nargs args ++
+              print_arguments nargs nargs_before_bidi args ++
                 if not (List.is_empty more_implicits) then
                   prlist (fun l -> str"," ++ print_implicits l) more_implicits
                 else (mt ()) ++
@@ -1086,7 +1087,8 @@ open Pputils
                     | `Assert -> keyword "assert"
                     | `ExtraScopes -> keyword "extra scopes"
                     | `ClearImplicits -> keyword "clear implicits"
-                    | `ClearScopes -> keyword "clear scopes")
+                    | `ClearScopes -> keyword "clear scopes"
+                    | `ClearBidiHint -> keyword "clear bidirectionality hint")
                   mods)
         )
       | VernacReserve bl ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5ae572541e..22427621e6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1204,6 +1204,36 @@ let vernac_syntactic_definition ~module_local lid x y =
   Dumpglob.dump_definition lid false "syndef";
   Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y
 
+let cache_bidi_hints (_name, (gr, ohint)) =
+  match ohint with
+  | None -> Pretyping.clear_bidirectionality_hint gr
+  | Some nargs -> Pretyping.add_bidirectionality_hint gr nargs
+
+let load_bidi_hints _ r =
+  cache_bidi_hints r
+
+let subst_bidi_hints (subst, (gr, ohint as orig)) =
+  let gr' = subst_global_reference subst gr in
+  if gr == gr' then orig else (gr', ohint)
+
+let discharge_bidi_hints (_name, (gr, ohint)) =
+  if isVarRef gr && Lib.is_in_section gr then None
+  else
+    let vars = Lib.variable_section_segment_of_reference gr in
+    let n = List.length vars in
+    Some (gr, Option.map ((+) n) ohint)
+
+let inBidiHints =
+  let open Libobject in
+  declare_object { (default_object "BIDIRECTIONALITY-HINTS" ) with
+                   load_function = load_bidi_hints;
+                   cache_function = cache_bidi_hints;
+                   classify_function = (fun o -> Substitute o);
+                   subst_function = subst_bidi_hints;
+                   discharge_function = discharge_bidi_hints;
+                 }
+
+
 let warn_arguments_assert =
   CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
          (fun sr ->
@@ -1216,7 +1246,7 @@ let warn_arguments_assert =
 (* [nargs_for_red] is the number of arguments required to trigger reduction,
    [args] is the main list of arguments statuses,
    [more_implicits] is a list of extra lists of implicit statuses  *)
-let vernac_arguments ~section_local reference args more_implicits nargs_for_red flags =
+let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let assert_flag = List.mem `Assert flags in
@@ -1227,6 +1257,7 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
   let default_implicits_flag = List.mem `DefaultImplicits flags in
   let never_unfold_flag = List.mem `ReductionNeverUnfold flags in
   let nomatch_flag = List.mem `ReductionDontExposeCase flags in
+  let clear_bidi_hint = List.mem `ClearBidiHint flags in
 
   let err_incompat x y =
     user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in
@@ -1285,6 +1316,9 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
   if Option.cata (fun n -> n > num_args) false nargs_for_red then
     user_err Pp.(str "The \"/\" modifier should be put before any extra scope.");
 
+  if Option.cata (fun n -> n > num_args) false nargs_before_bidi then
+    user_err Pp.(str "The \"&\" modifier should be put before any extra scope.");
+
   let scopes_specified = List.exists Option.has_some scopes in
   
   if scopes_specified && clear_scopes_flag then
@@ -1396,6 +1430,12 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
 
   let red_modifiers_specified = Option.has_some red_behavior in
 
+  let bidi_hint_specified = Option.has_some nargs_before_bidi in
+
+  if bidi_hint_specified && clear_bidi_hint then
+    err_incompat "clear bidirectionality hint" "&";
+
+
   (* Actions *)
 
   if renaming_specified then begin
@@ -1428,10 +1468,26 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
               strbrk "are relevant for constants only.")
   end;
 
+  if bidi_hint_specified then begin
+    let n = Option.get nargs_before_bidi in
+    if section_local then
+      Pretyping.add_bidirectionality_hint sr n
+    else
+      Lib.add_anonymous_leaf (inBidiHints (sr, Some n))
+    end;
+
+  if clear_bidi_hint then begin
+    if section_local then
+      Pretyping.clear_bidirectionality_hint sr
+    else
+      Lib.add_anonymous_leaf (inBidiHints (sr, None))
+  end;
+
  if not (renaming_specified ||
          implicits_specified ||
          scopes_specified ||
-         red_modifiers_specified) && (List.is_empty flags) then
+         red_modifiers_specified ||
+         bidi_hint_specified) && (List.is_empty flags) then
     warn_arguments_assert sr
 
 let default_env () = {
@@ -2437,8 +2493,8 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
   | VernacSyntacticDefinition (id,c,b) ->
     with_module_locality ~atts vernac_syntactic_definition id c b;
     pstate
-  | VernacArguments (qid, args, more_implicits, nargs, flags) ->
-    with_section_locality ~atts vernac_arguments qid args more_implicits nargs flags;
+  | VernacArguments (qid, args, more_implicits, nargs, nargs_before_bidi, flags) ->
+    with_section_locality ~atts vernac_arguments qid args more_implicits nargs nargs_before_bidi flags;
     pstate
   | VernacReserve bl ->
     unsupported_attributes atts;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index f946e0596e..df1d08ad0f 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -362,8 +362,9 @@ type nonrec vernac_expr =
       vernac_argument_status list (* Main arguments status list *) *
         (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
       int option (* Number of args to trigger reduction *) *
+      int option (* Number of args before bidirectional typing *) *
         [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
-          `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
+          `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `ClearBidiHint |
           `DefaultImplicits ] list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of (lident list) option