Ltac2: warn on unused variables

Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.

clib/cString.ml

@@ -23,6 +23,7 @@ sig
   val string_index_from : string -> int -> string -> int
   val string_contains : where:string -> what:string -> bool
   val plural : int -> string -> string
+  val lplural : _ list -> string -> string
   val conjugate_verb_to_be : int -> string
   val ordinal : int -> string
   val is_sub : string -> string -> int -> bool
@@ -140,6 +141,11 @@ let is_suffix p s =
 
 let plural n s = if n<>1 then s^"s" else s
 
+let lplural l s =
+  match l with
+  | [_] -> s
+  | _ -> s^"s"
+
 let conjugate_verb_to_be n = if n<>1 then "are" else "is"
 
 let ordinal n =

clib/cString.mli

@@ -51,6 +51,9 @@ sig
   val plural : int -> string -> string
   (** [plural n s] adds a optional 's' to the [s] when [2 <= n]. *)
 
+  val lplural : _ list -> string -> string
+  (** [lplural l s] is [plural (List.length l) s]. *)
+
   val conjugate_verb_to_be : int -> string
   (** [conjugate_verb_to_be] returns "is" when [n=1] and "are" otherwise *)
 

doc/changelog/06-Ltac2-language/18641-ltac2-warn-unused.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  warning on unused Ltac2 variables
+  (`#18641 <https://github.com/coq/coq/pull/18641>`_,
+  by Gaëtan Gilbert).

plugins/ltac2/tac2intern.ml

@@ -1098,6 +1098,19 @@ let expand_notation ?loc el kn =
     assert (Id.Map.is_empty argtys);
     CAst.make ?loc @@ CTacGlb (prms, el, body, ty)
 
+let warn_unused_variables = CWarnings.create ~name:"ltac2-unused-variable"
+    ~category:CWarnings.CoreCategories.ltac2
+    Pp.(fun ids -> str "Unused " ++ str (String.lplural ids "variable") ++ str ":" ++ spc() ++ prlist_with_sep spc Id.print ids ++ str ".")
+
+let check_unused_variables ?loc env to_name bnd =
+  let unused = List.filter_map (fun bnd -> match to_name bnd with
+      | Anonymous -> None
+      | Name id -> if is_used_var id env then None else Some id)
+      bnd
+  in
+  if CList.is_empty unused then ()
+  else warn_unused_variables ?loc unused
+
 let rec intern_rec env tycon {loc;v=e} =
   let check et = check ?loc env tycon et in
   match e with
@@ -1141,6 +1154,10 @@ let rec intern_rec env tycon {loc;v=e} =
       env, tycon) (env,tycon) nas tl
   in
   let (e, t) = intern_rec env tycon (exp e) in
+  let () =
+    (* TODO better loc? *)
+    check_unused_variables ?loc env (fun x -> x) nas
+  in
   let t = match tycon with
     | None -> List.fold_right (fun t accu -> GTypArrow (t, accu)) tl t
     | Some tycon -> tycon
@@ -1191,7 +1208,7 @@ let rec intern_rec env tycon {loc;v=e} =
         times in this matching")
   in
   let ids = List.fold_left fold Id.Set.empty el in
-  if is_rec then intern_let_rec env el tycon e
+  if is_rec then intern_let_rec env loc el tycon e
   else intern_let env loc ids el tycon e
 | CTacSyn (el, kn) ->
   let v = expand_notation ?loc el kn in
@@ -1369,10 +1386,11 @@ and intern_let env loc ids el tycon e =
   let (e, elp) = List.fold_left_map fold e el in
   let env = List.fold_left (fun accu (na, _, t) -> push_name na t accu) env elp in
   let (e, t) = intern_rec env tycon e in
+  let () = check_unused_variables ?loc env pi1 elp in
   let el = List.map (fun (na, e, _) -> na, e) elp in
   (GTacLet (false, el, e), t)
 
-and intern_let_rec env el tycon e =
+and intern_let_rec env loc el tycon e =
   let map env (pat, t, e) =
     let na = match pat.v with
     | CPatVar na -> na
@@ -1433,6 +1451,10 @@ and intern_let_rec env el tycon e =
   in
   let el = List.map map el in
   let (e, t) = intern_rec env tycon e in
+  let () =
+    (* TODO better loc? *)
+    check_unused_variables ?loc env fst el
+  in
   (GTacLet (true, el, e), t)
 
 and intern_constructor env loc tycon kn args = match kn with
@@ -1499,6 +1521,7 @@ and intern_case env loc e tycon pl =
       let patvars, pat = intern_pat env cpat et in
       let patenv = push_ids patvars env in
       let br = intern_rec_with_constraint patenv cbr rt in
+      let () = check_unused_variables ?loc patenv (fun (id,_) -> Name id) (Id.Map.bindings patvars) in
       pat, br)
       pl
   in
@@ -1511,6 +1534,7 @@ type context = (Id.t * type_scheme) list
 
 let intern ~strict ctx e =
   let env = empty_env ~strict () 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
@@ -1726,6 +1750,7 @@ let intern_notation_data ids body =
     in
     let env, argtys = Id.Set.fold fold ids (env,Id.Map.empty) in
     let body, ty = intern_rec env None body in
+    let () = check_unused_variables env (fun (id,_) -> Name id) (Id.Map.bindings argtys) in
     let count = ref 0 in
     let vars = ref TVar.Map.empty in
     let argtys = Id.Map.map (fun ty -> normalize env (count, vars) ty) argtys in
@@ -2027,6 +2052,7 @@ let () =
     let env = List.fold_left fold env ids in
     let loc = tac.loc in
     let (tac, t) = intern_rec env None tac in
+    let () = check_unused_variables ?loc env (fun x -> Name x) ids in
     let () = check_elt_unit loc env t in
     (ist, (ids, tac))
   in
@@ -2074,6 +2100,7 @@ let () =
     let ids, env = Id.Map.fold fold ntn_vars (Id.Set.empty, env) in
     let loc = tac.loc in
     let (tac, t) = intern_rec env None tac in
+    (* no check_unused_variables for notation variables *)
     let () = check_elt_unit loc env t in
     (ist, (ids, tac))
   in

plugins/ltac2/tac2typing_env.ml

@@ -101,8 +101,12 @@ type mix_var =
 
 type mix_type_scheme = int * mix_var glb_typexpr
 
+(* Changing the APIs enough to get which variables are used in random genargs seems very hard
+   so instead we use mutation to detect them *)
+type used = { mutable used : bool }
+
 type t = {
-  env_var : mix_type_scheme Id.Map.t;
+  env_var : (mix_type_scheme * used) Id.Map.t;
   (** Type schemes of bound variables *)
   env_cst : UF.elt glb_typexpr UF.t;
   (** Unification state *)
@@ -135,7 +139,14 @@ let find_rec_var id env = Id.Map.find_opt id env.env_rec
 
 let mem_var id env = Id.Map.mem id env.env_var
 
-let find_var id env = Id.Map.find id env.env_var
+let find_var id env =
+  let t, used = Id.Map.find id env.env_var in
+  used.used <- true;
+  t
+
+let is_used_var id env =
+  let _, {used} = Id.Map.find id env.env_var in
+  used
 
 let bound_vars env = Id.Map.domain env.env_var
 
@@ -196,10 +207,15 @@ let get_alias {CAst.loc;v=id} env =
 
 let push_name id t env = match id with
 | Anonymous -> env
-| Name id -> { env with env_var = Id.Map.add id t env.env_var }
+| Name id -> { env with env_var = Id.Map.add id (t, {used=false}) env.env_var }
 
 let push_ids ids env =
-  { env with env_var = Id.Map.union (fun _ x _ -> Some x) ids env.env_var }
+  let merge_fun _ fresh orig = match fresh, orig with
+    | None, None -> assert false
+    | Some x, _ -> Some (x, {used=false})
+    | None, Some x -> Some x
+  in
+  { env with env_var = Id.Map.merge merge_fun ids env.env_var }
 
 let rec subst_type subst (t : 'a glb_typexpr) = match t with
 | GTypVar id -> subst id
@@ -346,7 +362,7 @@ let fv_env env =
   | id, None -> UF.Map.add id () accu
   | _, Some t -> fv_type f t accu
   in
-  let fold_var id (_, t) accu =
+  let fold_var id ((_, t), _) accu =
     let fmix id accu = match id with
     | LVar _ -> accu
     | GVar id -> f id accu

plugins/ltac2/tac2typing_env.mli

@@ -48,6 +48,8 @@ val mem_var : Id.t -> t -> bool
 
 val find_var : Id.t -> t -> mix_type_scheme
 
+val is_used_var : Id.t -> t -> bool
+
 val bound_vars : t -> Id.Set.t
 
 val get_variable0 : (Id.t -> bool) -> tacref or_relid -> tacref Locus.or_var

test-suite/output/PrintGenarg.out

@@ -4,6 +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 := preterm:(0) in exact1 false c))
+        let _ := open_constr:(ltac2:(let c := preterm:(0) in exact1 false c))
           in
         ()

test-suite/output/PrintGenarg.v

@@ -7,7 +7,7 @@ Print foo.
 Require Import Ltac2.Ltac2.
 
 Ltac2 bar () :=
-  let x := open_constr:(ltac2:(exact 0)) in
+  let _ := open_constr:(ltac2:(exact 0)) in
   ().
 
 Print bar.

test-suite/output/bug_18138.v

@@ -4,6 +4,7 @@ Module Import M.
   Ltac2 foo := ().
 End M.
 
+#[warnings="-ltac2-unused-variable"]
 Ltac2 bar foo := M.foo.
 
 Print bar.

test-suite/output/ltac2_unused_var.out

@@ -0,0 +1,28 @@
+File "./output/ltac2_unused_var.v", line 3, characters 6-18:
+Warning: Unused variable: x. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 5, characters 16-27:
+Warning: Unused variable: y. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 5, characters 6-27:
+Warning: Unused variable: x. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 8, characters 6-19:
+Warning: Unused variable: _x. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 10, characters 0-38:
+Warning: Unused variable: x. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 16, characters 17-23:
+Warning: Unused variable: x. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 18, characters 16-40:
+Warning: Unused variable: y. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 20, characters 16-56:
+Warning: Unused variable: x. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 22, characters 16-43:
+Warning: Unused variable: b. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 24, characters 15-32:
+Warning: Unused variable: x. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 26, characters 23-26:
+Warning: Unused variables: x y. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 28, characters 23-26:
+Warning: Unused variable: y. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 30, characters 18-55:
+Warning: Unused variable: y. [ltac2-unused-variable,ltac2,default]
+File "./output/ltac2_unused_var.v", line 42, characters 37-39:
+Warning: Unused variable: x. [ltac2-unused-variable,ltac2,default]

test-suite/output/ltac2_unused_var.v

@@ -0,0 +1,46 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 foo1 x := ().
+
+Ltac2 foo2 x := fun y => ().
+
+(* we also warn on _ prefixed variable unlike ocaml *)
+Ltac2 foo3 _x := ().
+
+Ltac2 Notation "foo4" x(constr) := ().
+
+(* questionable behaviour: unused variable in untyped notation warns at notation use time *)
+Unset Ltac2 Typed Notations.
+Ltac2 Notation "foo5" x(constr) := ().
+Set Ltac2 Typed Notations.
+Ltac2 foo6 () := foo5 1.
+
+Ltac2 foo7 x := match x with y => () end.
+
+Ltac2 foo8 x := match x with Some x => 1 | None => 2 end.
+
+Ltac2 foo9 x := match x with (a,b) => a end.
+
+Ltac2 foo10 := let x := () in ().
+
+Ltac2 foo11 () := let (x,y) := (1,2) in ().
+
+Ltac2 foo12 () := let (x,y) := (1,2) in x.
+
+Ltac2 foo13 () := let rec x () := 1 with y () := 2 in x.
+
+Ltac2 foo14 () := let rec x () := y () with y () := 2 in x.
+
+(* missing warning for unused letrec (bug?) *)
+Ltac2 foo15 () := let rec x () := y () with y () := x () in ().
+
+Ltac2 mutable bar () := ().
+
+(* missing warning for unused "Set as" (bug?) *)
+Ltac2 Set bar as bar0 := fun () => ().
+
+Ltac2 foo16 () := ltac1:(ltac2:(x |- ())).
+
+(* no warning for y even though it's bound in the ltac2 context
+   (ltac2 can't tell that the notation isn't eg "ltac2:(...) + y") *)
+Notation foo17 x y := ltac2:(exact $preterm:x) (only parsing).

user-contrib/Ltac2/Array.v

@@ -75,8 +75,8 @@ Ltac2 init (l : int) (f : int->'a) :=
   end.
 
 Ltac2 make_matrix (sx : int) (sy : int) (v : 'a) :=
-  let init1 i := v in
-  let initr i := init sy init1 in
+  let init1 _ := v in
+  let initr _ := init sy init1 in
   init sx initr.
 
 Ltac2 copy a := lowlevel_sub a 0 (length a).
@@ -175,7 +175,7 @@ Ltac2 of_list (ls : 'a list) :=
     end in
   match ls with
   | [] => empty
-  | hd::tl =>
+  | hd :: _ =>
       let anew := make (list_length ls) hd in
       of_list_aux ls anew 0;
       anew

user-contrib/Ltac2/List.v

@@ -71,19 +71,19 @@ Ltac2 cons (x : 'a) (xs : 'a list) :=
 Ltac2 hd_opt (ls : 'a list) :=
   match ls with
   | [] => None
-  | x :: xs => Some x
+  | x :: _ => Some x
   end.
 
 Ltac2 hd (ls : 'a list) :=
   match ls with
   | [] => Control.throw_invalid_argument "List.hd"
-  | x :: xs => x
+  | x :: _ => x
   end.
 
 Ltac2 tl (ls : 'a list) :=
   match ls with
   | [] => []
-  | x :: xs => xs
+  | _ :: xs => xs
   end.
 
 Ltac2 dest (xs : 'a list) : 'a * 'a list :=
@@ -332,7 +332,7 @@ Ltac2 rec for_all2_aux (on_length_mismatch : 'a list -> 'b list -> bool) f xs ys
   match xs with
   | [] => match ys with
           | [] => true
-          | y :: ys' => on_length_mismatch xs ys
+          | _ :: _ => on_length_mismatch xs ys
           end
   | x :: xs'
     => match ys with
@@ -352,7 +352,7 @@ Ltac2 rec exist2 f xs ys :=
   match xs with
   | [] => match ys with
           | [] => false
-          | y :: ys' => Control.throw_invalid_argument "List.exist2"
+          | _ :: _ => Control.throw_invalid_argument "List.exist2"
           end
   | x :: xs'
     => match ys with
@@ -473,7 +473,7 @@ Ltac2 rec skipn (n : int) (ls : 'a list) :=
   | false
     => match ls with
        | [] => Control.throw_out_of_bounds "List.skipn"
-       | x :: xs
+       | _ :: xs
          => skipn (Int.sub n 1) xs
        end
   end.

user-contrib/Ltac2/Notations.v

@@ -244,7 +244,7 @@ match cl with
 end.
 
 Ltac2 pose0 ev p :=
-  enter_h ev (fun ev (na, p) => Std.pose na p) p.
+  enter_h ev (fun _ (na, p) => Std.pose na p) p.
 
 Ltac2 Notation "pose" p(thunk(pose)) :=
   pose0 false p.