Merge PR #21618: Typecheck ignoring errors instead of globalize for Ltac2 Globalize

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

Author: coqbot-app[bot]

plugins/ltac2/tac2entries.ml

@@ -1599,8 +1599,9 @@ let typecheck_expr e =
 
 let globalize_expr e =
   let avoid = Id.Set.empty in
-  let e = Tac2intern.debug_globalize_allow_ext avoid e in
-  Feedback.msg_notice (Tac2print.pr_rawexpr_gen E5 ~avoid e)
+  let e, t, errors = Tac2intern.intern_accumulate_errors ~strict:false [] e in
+  (* XXX print type and errors? *)
+  Feedback.msg_notice (Tac2print.pr_glbexpr_gen E5 ~avoid e)
 
 (** Calling tactics *)
 

plugins/ltac2/tac2extravals.ml

@@ -417,7 +417,6 @@ let () =
   let pr_raw e = Genprint.PrinterBasic (fun _env _sigma ->
       let avoid = Id.Set.empty in
       (* FIXME avoid set, same as pr_glb *)
-      let e = Tac2intern.debug_globalize_allow_ext avoid e in
       Tac2print.pr_rawexpr_gen ~avoid E5 e) in
   let pr_glb (ids, e) =
     let ids =
@@ -437,7 +436,6 @@ let () =
 
 let () =
   let pr_raw e = Genprint.PrinterBasic (fun _ _ ->
-      let e = Tac2intern.debug_globalize_allow_ext Id.Set.empty e in
       Tac2print.pr_rawexpr_gen ~avoid:Id.Set.empty E5 e)
   in
   let pr_glb e = Genprint.PrinterBasic (fun _ _ -> Tac2print.pr_glbexpr ~avoid:Id.Set.empty e) in

plugins/ltac2/tac2intern.ml

@@ -1076,9 +1076,12 @@ let tycon_fun_body ?loc env tycon dom =
     let () = unify ?loc env (GTypArrow (dom,codom)) tycon in
     codom
   | GTypRef _ ->
-    CErrors.user_err ?loc
-      Pp.(str "This expression should not be a function, the expected type is" ++ spc() ++
-          pr_glbtype env tycon ++ str ".")
+    let () =
+      add_error env ?loc
+        Pp.(str "This expression should not be a function, the expected type is" ++ spc() ++
+            pr_glbtype env tycon ++ str ".")
+    in
+    GTypVar (fresh_id env)
 
 let tycon_app ?loc env ~ft t =
   match kind env t with
@@ -1093,14 +1096,16 @@ let tycon_app ?loc env ~ft t =
       | GTypArrow _ -> true
       | _ -> false
     in
-    if is_fun then
-      CErrors.user_err ?loc
+    let () = if is_fun then
+      add_error env ?loc
         Pp.(str "This function has type" ++ spc() ++ pr_glbtype env ft ++
             spc() ++ str "and is applied to too many arguments.")
     else
-      CErrors.user_err ?loc
+      add_error env ?loc
         Pp.(str "This expression has type" ++ spc() ++ pr_glbtype env ft ++ str"." ++
             spc() ++ str "It is not a function and cannot be applied.")
+    in
+    GTypVar (fresh_id env), GTypVar (fresh_id env)
 
 let warn_useless_record_with = CWarnings.create ~name:"ltac2-useless-record-with" ~default:AsError
     ~category:CWarnings.CoreCategories.ltac2
@@ -1521,29 +1526,32 @@ and intern_constructor env loc tycon kn args = match kn with
   else
     error_nargs_mismatch ?loc kn nargs (List.length args)
 | Tuple n ->
-  let () = if not (Int.equal n (List.length args)) then begin
-      if Int.equal 0 n then
-        (* parsing [() bla] produces [CTacApp (Tuple 0, [bla])] but parsing
-           [((), ()) bla] produces [CTacApp (CTacApp (Tuple 2, [(); ()]), [bla])]
-           so we only need to produce a sensible error for [Tuple 0] *)
-        let t = GTypRef (Tuple 0, []) in
-        CErrors.user_err ?loc Pp.(
-            str "This expression has type" ++ spc () ++ pr_glbtype env t ++
-            spc () ++ str "and is not a function")
-      else assert false
-    end
-  in
-  let types = List.init n (fun i -> GTypVar (fresh_id env)) in
-  let ans = GTypRef (Tuple n, types) in
-  let ans = match tycon with
-    | None -> ans
-    | Some tycon ->
-      let () = unify ?loc env ans tycon in
-      tycon
-  in
-  let map arg tpe = intern_rec_with_constraint env arg tpe in
-  let args = List.map2 map args types in
-  GTacCst (Tuple n, 0, args), ans
+  if not (Int.equal n (List.length args)) then begin
+    assert (Int.equal 0 n);
+    (* parsing [() bla] produces [CTacApp (Tuple 0, [bla])] but parsing
+         [((), ()) bla] produces [CTacApp (CTacApp (Tuple 2, [(); ()]), [bla])]
+         so we only need to produce a sensible error for [Tuple 0] *)
+    let t = GTypRef (Tuple 0, []) in
+    let () =
+      add_error env ?loc Pp.(
+        str "This expression has type" ++ spc () ++ pr_glbtype env t ++
+        spc () ++ str "and is not a function.")
+    in
+    let args = List.map (fun arg -> fst @@ intern_rec env None arg) args in
+    GTacApp (GTacCst (Tuple 0, 0, []), args), GTypVar (fresh_id env)
+  end
+  else
+    let types = List.init n (fun i -> GTypVar (fresh_id env)) in
+    let ans = GTypRef (Tuple n, types) in
+    let ans = match tycon with
+      | None -> ans
+      | Some tycon ->
+        let () = unify ?loc env ans tycon in
+        tycon
+    in
+    let map arg tpe = intern_rec_with_constraint env arg tpe in
+    let args = List.map2 map args types in
+    GTacCst (Tuple n, 0, args), ans
 
 and intern_case env loc e tycon pl =
   let e, et = intern_rec env None e in
@@ -1583,6 +1591,17 @@ let intern ~strict ctx e =
   let t = normalize env (count, vars) t in
   (e, (!count, t))
 
+let intern_accumulate_errors ~strict ctx e =
+  let env = empty_env ~strict ~accumulate_errors:true () in
+  (* XXX not doing check_unused_variables *)
+  let fold accu (id, t) = push_name (Name id) (polymorphic t) accu in
+  let env = List.fold_left fold env ctx in
+  let (e, t) = intern_rec env None e in
+  let count = ref 0 in
+  let vars = ref TVar.Map.empty in
+  let t = normalize env (count, vars) t in
+  (e, (!count, t), get_errors env)
+
 let intern_typedef self (ids, t) : glb_quant_typedef =
   let env = set_rec self (empty_env ()) in
   (* Initialize type parameters *)
@@ -1776,10 +1795,6 @@ let globalize ids tac =
   in
   globalize_gen ~tacext ids tac
 
-let debug_globalize_allow_ext ids tac =
-  let tacext ?loc (RawExt (tag,arg)) = CAst.make ?loc @@ CTacExt (tag,arg) in
-  globalize_gen ~tacext ids tac
-
 let { Goptions.get = typed_notations } =
   Goptions.declare_bool_option_and_ref
     ~key:["Ltac2";"Typed";"Notations"] ~value:true ()

plugins/ltac2/tac2intern.mli

@@ -19,6 +19,9 @@ val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quan
 val intern_open_type : raw_typexpr -> type_scheme
 val intern_notation_data : Id.Set.t -> raw_tacexpr -> Tac2env.notation_data
 
+val intern_accumulate_errors : strict:bool -> context -> raw_tacexpr ->
+  glb_tacexpr * type_scheme * Pp.t Loc.located list
+
 (** [check_unused] is default true *)
 val genintern_warn_not_unit : ?check_unused:bool ->
   Genintern.glob_sign ->
@@ -66,10 +69,6 @@ val globalize : Id.Set.t -> raw_tacexpr -> raw_tacexpr
 (** Replaces all qualified identifiers by their corresponding kernel name. The
     set represents bound variables in the context. *)
 
-val debug_globalize_allow_ext : Id.Set.t -> raw_tacexpr -> raw_tacexpr
-(** Variant of globalize which can accept CTacExt using the provided function.
-    Intended for debugging. *)
-
 (** Errors *)
 
 val error_nargs_mismatch : ?loc:Loc.t -> ltac_constructor -> int -> int -> 'a

plugins/ltac2/tac2typing_env.ml

@@ -105,6 +105,9 @@ type mix_type_scheme = int * mix_var glb_typexpr
    so instead we use mutation to detect them *)
 type used = { mutable used : bool }
 
+(* TODO delay printing? but printing depends on env which is mutable *)
+type error = Pp.t Loc.located
+
 type t = {
   env_var : (mix_type_scheme * used) Id.Map.t;
   (** Type schemes of bound variables *)
@@ -118,17 +121,30 @@ type t = {
   (** Recursive type definitions *)
   env_strict : bool;
   (** True iff in strict mode *)
+  env_errs : error list ref option;
+  (** [None] if raise on first error, [Some] if accumulate errors *)
 }
 
-let empty_env ?(strict=true) () = {
+let empty_env ?(strict=true) ?(accumulate_errors=false) () = {
   env_var = Id.Map.empty;
   env_cst = UF.create ();
   env_als = ref Id.Map.empty;
   env_opn = true;
   env_rec = Id.Map.empty;
   env_strict = strict;
+  env_errs = if accumulate_errors then Some (ref []) else None;
 }
 
+let add_error ?loc env msg =
+  match env.env_errs with
+  | None -> CErrors.user_err ?loc msg
+  | Some errs -> errs := (loc,msg) :: !errs
+
+let get_errors env =
+  match env.env_errs with
+  | None -> assert false
+  | Some errs -> !errs
+
 let env_strict env = env.env_strict
 
 let set_rec self env = { env with env_rec = self }
@@ -328,7 +344,7 @@ let rec unify0 env t1 t2 = match kind env t1, kind env t2 with
 let unify ?loc env t1 t2 =
   try unify0 env t1 t2
   with CannotUnify (u1, u2) ->
-    CErrors.user_err ?loc Pp.(str "This expression has type" ++ spc () ++ pr_glbtype env t1 ++
+    add_error env ?loc Pp.(str "This expression has type" ++ spc () ++ pr_glbtype env t1 ++
       spc () ++ str "but an expression was expected of type" ++ spc () ++ pr_glbtype env t2)
 
 let unify_arrow ?loc env ft args =
@@ -343,12 +359,17 @@ let unify_arrow ?loc env ft args =
     let () = unify ?loc env (GTypVar id) (GTypArrow (t, ft)) in
     iter ft args true
   | GTypRef _, _ :: _ ->
-    if is_fun then
-      CErrors.user_err ?loc Pp.(str "This function has type" ++ spc () ++ pr_glbtype env ft0 ++
-        spc () ++ str "and is applied to too many arguments")
-    else
-      CErrors.user_err ?loc Pp.(str "This expression has type" ++ spc () ++ pr_glbtype env ft0 ++
-        spc () ++ str "and is not a function")
+    let () =
+      if is_fun then
+        add_error env ?loc
+          Pp.(str "This function has type" ++ spc () ++ pr_glbtype env ft0 ++
+              spc () ++ str "and is applied to too many arguments")
+      else
+        add_error env ?loc
+          Pp.(str "This expression has type" ++ spc () ++ pr_glbtype env ft0 ++
+              spc () ++ str "and is not a function")
+    in
+    GTypVar (fresh_id env)
   in
   iter ft args false
 

plugins/ltac2/tac2typing_env.mli

@@ -21,8 +21,14 @@ end
 
 type t
 
-(** default strict:true *)
-val empty_env : ?strict:bool -> unit -> t
+(** default strict:true, accumulate_errors:false *)
+val empty_env : ?strict:bool -> ?accumulate_errors:bool -> unit -> t
+
+(** In accumulate mode, add the error to the list in the env. Otherwise raise UserError. *)
+val add_error : ?loc:Loc.t -> t -> Pp.t -> unit
+
+(** Get accumulated errors. Assertion failure if not in accumulate mode. *)
+val get_errors : t -> Pp.t Loc.located list
 
 val set_rec : (KerName.t * int) Id.Map.t -> t -> t
 

test-suite/output/ltac2_check_globalize.out

@@ -16,25 +16,26 @@ let x := fun x => x in
 let _ := x 1 in
 let _ := x "" in
 () : unit
-let accu := { contents := []} in
-(let x := fun x => accu.(contents) := (x :: accu.(contents)) in
- let _ := x 1 in
- let _ := x "" in
- ());
+let accu := { contents := [] } in
+let _ :=
+  let x := fun x => accu.(contents) := (x :: accu.(contents)) in
+  let _ := x 1 in
+  let _ := x "" in
+  ()
+in
 accu.(contents)
 File "./output/ltac2_check_globalize.v", line 38, characters 0-144:
 The command has indeed failed with message:
 This expression has type string but an expression was expected of type 
 int
-let (m : '__α Pattern.goal_matching) :=
-  ([(([(None, (Pattern.MatchPattern, pat:(_)))],
+let m :=
+  [(([(None, (Pattern.MatchPattern, pat:(_)))],
       (Pattern.MatchPattern, pat:(_))),
      (fun h =>
       let h := Array.get h 0 in
       fun _ => fun _ => fun _ => fun _ => Std.clear h));
-     (([], (Pattern.MatchPattern, pat:(_))),
+    (([], (Pattern.MatchPattern, pat:(_))),
       (fun _ => fun _ => fun _ => fun _ => fun _ => ()))]
-    : _ Pattern.goal_matching)
 in
-Pattern.lazy_goal_match0 false m :'__α
+Pattern.lazy_goal_match0 false m
 constr:(ltac2:(()))

test-suite/output/ltac2_typed_notations.out

@@ -2,12 +2,10 @@ File "./output/ltac2_typed_notations.v", line 5, characters 9-10:
 The command has indeed failed with message:
 This expression has type bool but an expression was expected of type 
 constr
-fun (b : bool) =>
-(let c := b in
- let (m : '__α Pattern.constr_matching) :=
-   [(Pattern.MatchPattern, pat:(true),
-     (fun _ => fun (_ : constr array) => true));
-     (Pattern.MatchPattern, pat:(false),
-      (fun _ => fun (_ : constr array) => false))]
- with (t : constr) := c in
- Pattern.one_match0 t m :'__α : bool)
+fun b =>
+let c := b in
+let m :=
+  [(Pattern.MatchPattern, pat:(true), (fun _ => fun _ => true));
+    (Pattern.MatchPattern, pat:(false), (fun _ => fun _ => false))]
+with t := c in
+Pattern.one_match0 t m