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 => ...`)

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

plugins/ltac2/tac2intern.ml

@@ -1108,6 +1108,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 variables:" ++ 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
@@ -1151,6 +1164,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
@@ -1201,7 +1218,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
@@ -1379,10 +1396,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
@@ -1443,6 +1461,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
@@ -1509,6 +1531,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
@@ -1521,6 +1544,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
@@ -2037,6 +2061,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
@@ -2084,6 +2109,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
+    let () = check_unused_variables ?loc env (fun x -> Name x) (Id.Set.elements ids) in
     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

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

@@ -246,7 +246,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.