Ltac2: use preterm in exact / eexact

Fix coq#12827

The implementation uses a generalization of Constr.pretype which takes
flags (an opaque type) and a typing constraint.

Changing `refine` is left to the future as the notation takes a tactic
thunk at constr type so would be backwards incompatible.

doc/changelog/06-Ltac2-language/18157-ltac2-exact-preterm.rst

@@ -0,0 +1,6 @@
+- **Changed:**
+  Ltac2 `exact` and `eexact` elaborate their argument using the type of the goal as expected type,
+  instead of elaborating with no expected type then unifying the resulting type with the goal
+  (`#18157 <https://github.com/coq/coq/pull/18157>`_,
+  fixes `#12827 <https://github.com/coq/coq/issues/12827>`_,
+  by Gaëtan Gilbert).

plugins/ltac2/tac2core.ml

@@ -32,6 +32,18 @@ let constr_flags =
     polymorphic = false;
   }
 
+let open_constr_use_classes_flags =
+  let open Pretyping in
+  {
+  use_coercions = true;
+  use_typeclasses = Pretyping.UseTC;
+  solve_unification_constraints = true;
+  fail_evar = false;
+  expand_evars = true;
+  program_mode = false;
+  polymorphic = false;
+  }
+
 let open_constr_no_classes_flags =
   let open Pretyping in
   {
@@ -157,6 +169,12 @@ let inductive = repr_ext val_inductive
 
 let projection = repr_ext val_projection
 
+let to_expected_type : _ -> Pretyping.typing_constraint = function
+  | ValInt 0 -> IsType
+  | ValInt 1 -> WithoutTypeConstraint
+  | ValBlk (0, [|c|]) -> OfType (to_constr c)
+  | _ -> assert false
+
 (** Stdlib exceptions *)
 
 let err_notfocussed =
@@ -729,23 +747,14 @@ let () =
     throw err_notfocussed
 
 (** preterm -> constr *)
+let () = define "constr_flags" (ret (repr_ext val_pretype_flags)) constr_flags
+
+let () = define "open_constr_flags" (ret (repr_ext val_pretype_flags)) open_constr_use_classes_flags
+
 let () =
-  define "constr_pretype" (repr_ext val_preterm @-> tac constr) @@ fun c ->
-  let open Pretyping in
-  let open Ltac_pretype in
+  define "constr_pretype" (repr_ext val_pretype_flags @-> to_expected_type @--> repr_ext val_preterm @-> tac constr) @@ fun flags expected_type c ->
   let pretype env sigma =
-    (* For now there are no primitives to create preterms with a non-empty
-       closure. I do not know whether [closed_glob_constr] is really the type
-       we want but it does not hurt in the meantime. *)
-    let { closure; term } = c in
-    let vars = {
-      ltac_constrs = closure.typed;
-      ltac_uconstrs = closure.untyped;
-      ltac_idents = closure.idents;
-      ltac_genargs = closure.genargs;
-    } in
-    let flags = constr_flags in
-    let sigma, t = understand_ltac flags env sigma vars WithoutTypeConstraint term in
+    let sigma, t = Pretyping.understand_uconstr ~flags ~expected_type env sigma c in
     Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t
   in
   pf_apply ~catch_exceptions:true pretype

plugins/ltac2/tac2ffi.ml

@@ -116,6 +116,7 @@ let val_uint63 = Val.create "uint63"
 let val_float = Val.create "float"
 let val_ind_data : (Names.Ind.t * Declarations.mutual_inductive_body) Val.tag = Val.create "ind_data"
 let val_transparent_state : TransparentState.t Val.tag = Val.create "transparent_state"
+let val_pretype_flags = Val.create "pretype_flags"
 
 let extract_val (type a) (type b) (tag : a Val.tag) (tag' : b Val.tag) (v : b) : a =
 match Val.eq tag tag' with

plugins/ltac2/tac2ffi.mli

@@ -225,6 +225,7 @@ val val_free : Id.Set.t Val.tag
 val val_uint63 : Uint63.t Val.tag
 val val_float : Float64.t Val.tag
 val val_ltac1 : Geninterp.Val.t Val.tag
+val val_pretype_flags : Pretyping.inference_flags Val.tag
 
 val val_ind_data : (Names.Ind.t * Declarations.mutual_inductive_body) Val.tag
 val val_transparent_state : TransparentState.t Val.tag

test-suite/bugs/bug_12827.v

@@ -0,0 +1,17 @@
+Existing Class True.
+Existing Instance I.
+
+(* ltac1 exact works *)
+Goal True.
+  exact _.
+Qed.
+
+Require Import Ltac2.Ltac2.
+Require Import Ltac2.Notations.
+
+Goal True.
+  exact _.
+  (* was: Error: Cannot infer this placeholder of type "True" (no type class instance
+found).
+   *)
+Qed.

test-suite/bugs/bug_17233.v

@@ -1,15 +1,20 @@
 Require Import Ltac2.Ltac2.
 
+(* exact0 at the time of the bug, with eexact part removed for simplicity *)
+Ltac2 exact0 c :=
+  Control.enter (fun _ =>
+      Control.with_holes c (fun c => Control.refine (fun _ => c))).
+
 Ltac2 Eval
   let x := constr:(0) in
   Constr.pretype preterm:($x).
 (* (* uncaught Not_found *) *)
 
 Ltac2 Eval
   let x := constr:(0) in
-  Constr.pretype preterm:(ltac2:(let y () := x in exact0 false y)).
+  Constr.pretype preterm:(ltac2:(let y () := x in exact0 y)).
 (* (* anomaly unbound variable x *) *)
 
-Notation "[ x ]" := ltac2:(exact0 false (fun ()  => Constr.pretype x)).
+Notation "[ x ]" := ltac2:(exact0 (fun ()  => Constr.pretype x)).
 
-Check ltac2:(let y := constr:(0) in exact0 false (fun () => open_constr:([ $y ]))).
+Check ltac2:(let y := constr:(0) in exact0 (fun () => open_constr:([ $y ]))).

test-suite/output/PrintGenarg.out

@@ -4,7 +4,6 @@ Ltac foo := let x := open_constr:(ltac:(exact 0)) in
 Ltac2 bar : unit -> unit
       bar :=
         fun _ =>
-        let x :=
-          open_constr:(ltac2:(let c := fun _ => open_constr:(0) in
-                              exact0 false c)) in
+        let x := open_constr:(ltac2:(let c := preterm:(0) in exact1 false c))
+          in
         ()

test-suite/output/bug_17594.out

@@ -2,7 +2,7 @@
 3
 2
 3
-File "./output/bug_17594.v", line 8, characters 2-102:
+File "./output/bug_17594.v", line 12, characters 19-20:
 The command has indeed failed with message:
 The term "0" has type "nat" while it is expected to have type "True".
 1
@@ -16,7 +16,7 @@ The term "0" has type "nat" while it is expected to have type "True".
 3
 2
 3
-File "./output/bug_17594.v", line 19, characters 2-115:
+File "./output/bug_17594.v", line 23, characters 19-20:
 The command has indeed failed with message:
 The term "0" has type "nat" while it is expected to have type "True".
 1

user-contrib/Ltac2/Constr.v

@@ -139,7 +139,26 @@ Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "co
     focused goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is
     the proof built by the tactic. *)
 
-Ltac2 @ external pretype : preterm -> constr := "coq-core.plugins.ltac2" "constr_pretype".
+Module Pretype.
+  Module Flags.
+    Ltac2 Type t.
+
+    Ltac2 @ external constr_flags : t := "coq-core.plugins.ltac2" "constr_flags".
+    (** Does not allow new unsolved evars. *)
+
+    Ltac2 @ external open_constr_flags : t := "coq-core.plugins.ltac2" "open_constr_flags".
+    (** Allows new unsolved evars. *)
+  End Flags.
+
+  Ltac2 Type expected_type := [ IsType | OfType (constr) | WithoutTypeConstraint ].
+
+  Ltac2 @ external pretype : Flags.t -> expected_type -> preterm -> constr
+    := "coq-core.plugins.ltac2" "constr_pretype".
+  (** Pretype the provided preterm. Assumes the goal to be focussed. *)
+End Pretype.
+
+Ltac2 pretype (c : preterm) : constr :=
+  Pretype.pretype Pretype.Flags.constr_flags Pretype.WithoutTypeConstraint c.
 (** Pretype the provided preterm. Assumes the goal to be focussed. *)
 
 

user-contrib/Ltac2/Notations.v

@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Import Ltac2.Init.
-Require Ltac2.Control Ltac2.Option Ltac2.Pattern Ltac2.Array Ltac2.Int Ltac2.Std.
+Require Ltac2.Control Ltac2.Option Ltac2.Pattern Ltac2.Array Ltac2.Int Ltac2.Std Ltac2.Constr.
 
 (** Constr matching *)
 
@@ -460,6 +460,7 @@ Ltac2 Notation "erewrite"
 
 (** coretactics *)
 
+(** Provided for backwards compat *)
 Ltac2 exact0 ev c :=
   Control.enter (fun _ =>
     match ev with
@@ -471,8 +472,20 @@ Ltac2 exact0 ev c :=
     end
   ).
 
-Ltac2 Notation "exact" c(thunk(open_constr)) := exact0 false c.
-Ltac2 Notation "eexact" c(thunk(open_constr)) := exact0 true c.
+Ltac2 exact1 ev c :=
+  Control.enter (fun () =>
+    let c :=
+      Constr.Pretype.pretype
+        (if ev then Constr.Pretype.Flags.open_constr_flags else Constr.Pretype.Flags.constr_flags)
+        (Constr.Pretype.OfType (Control.goal()))
+        c
+    in
+    Control.refine (fun _ => c)).
+
+Ltac2 Notation "exact" c(preterm) := exact1 false c.
+
+Ltac2 Notation "eexact" c(preterm) := exact1 true c.
+(** Like [refine] but new evars are shelved instead of becoming subgoals. *)
 
 Ltac2 Notation "intro" id(opt(ident)) mv(opt(move_location)) := Std.intro id mv.
 Ltac2 Notation intro := intro.