Ltac2: named type variables can't be defined

If we want to build doc from code we need the annotated types to be
accurate.

Notice how in the stdlib we had a couple less than accurate type annotations.

This differs from how ocaml does things but TBH I strongly dislike how
ocaml does things in this case.

doc/changelog/06-Ltac2-language/18118-ltac2-rigid-typ-var.rst

@@ -0,0 +1,6 @@
+- **Changed:**
+  explicit type variables are rigid, such that annotations like
+  `Ltac2 id (x:'a) := ...` ensure that `id` will be polymorphic.
+  Previously for instance `Ltac2 bad_id (x:'a) : 'b := x.` would be accepted
+  (`#18118 <https://github.com/coq/coq/pull/18118>`_,
+  by Gaëtan Gilbert).

plugins/ltac2/tac2typing_env.ml

@@ -21,10 +21,10 @@ type elt
 type 'a t
 val equal : elt -> elt -> bool
 val create : unit -> 'a t
-val fresh : 'a t -> elt
+val fresh : rigid:bool -> 'a t -> elt
 val find : elt -> 'a t -> (elt * 'a option)
-val union : elt -> elt -> 'a t -> unit
-val set : elt -> 'a -> 'a t -> unit
+val union : elt -> elt -> 'a t -> bool
+val set : elt -> 'a -> 'a t -> bool
 module Map : CSig.MapS with type key = elt
 end
 =
@@ -33,8 +33,13 @@ type elt = int
 let equal = Int.equal
 module Map = Int.Map
 
+type 'a value =
+| Unset
+| Set of 'a
+| Rigid
+
 type 'a node =
-| Canon of int * 'a option
+| Canon of int * 'a value
 | Equiv of elt
 
 type 'a t = {
@@ -52,10 +57,10 @@ let resize p =
 
 let create () = { uf_data = [||]; uf_size = 0 }
 
-let fresh p =
+let fresh ~rigid p =
   resize p;
   let n = p.uf_size in
-  p.uf_data.(n) <- (Canon (1, None));
+  p.uf_data.(n) <- (Canon (1, if rigid then Rigid else Unset));
   p.uf_size <- n + 1;
   n
 
@@ -69,23 +74,32 @@ let rec lookup n p =
     res
 
 let find n p =
-  let (x, _, v) = lookup n p in (x, v)
+  let (x, _, v) = lookup n p in
+  let v = match v with Rigid | Unset -> None | Set v -> Some v in
+  (x, v)
 
 let union x y p =
   let ((x, size1, _) as xcan) = lookup x p in
   let ((y, size2, _) as ycan) = lookup y p in
   let xcan, ycan = if size1 < size2 then xcan, ycan else ycan, xcan in
   let x, _, xnode = xcan in
   let y, _, ynode = ycan in
-  assert (Option.is_empty xnode);
-  assert (Option.is_empty ynode);
-  p.uf_data.(x) <- Equiv y;
-  p.uf_data.(y) <- Canon (size1 + size2, None)
+  match xnode, ynode with
+  | Set _, _ | _, Set _ -> assert false
+  | Rigid, Rigid -> false
+  | Unset, node | node, Unset ->
+    p.uf_data.(x) <- Equiv y;
+    p.uf_data.(y) <- Canon (size1 + size2, node);
+    true
 
 let set x v p =
   let (x, s, v') = lookup x p in
-  assert (Option.is_empty v');
-  p.uf_data.(x) <- Canon (s, Some v)
+  match v' with
+  | Set _ -> assert false
+  | Rigid -> false
+  | Unset ->
+    p.uf_data.(x) <- Canon (s, Set v);
+    true
 
 end
 
@@ -183,13 +197,13 @@ let env_name env =
       let () = vars := UF.Map.add n ans !vars in
       ans
 
-let fresh_id env = UF.fresh env.env_cst
+let fresh_id env = UF.fresh ~rigid:false env.env_cst
 
 let get_alias {CAst.loc;v=id} env =
   try Id.Map.find id env.env_als.contents
   with Not_found ->
     if env.env_opn then
-      let n = fresh_id env in
+      let n = UF.fresh ~rigid:true env.env_cst in
       let () = env.env_als := Id.Map.add id n env.env_als.contents in
       n
     else CErrors.user_err ?loc Pp.(str "Unbound type parameter " ++ Id.print id)
@@ -285,11 +299,13 @@ exception CannotUnify of TVar.t glb_typexpr * TVar.t glb_typexpr
 
 let unify_var env id t = match kind env t with
 | GTypVar id' ->
-  if not (TVar.equal id id') then UF.union id id' env.env_cst
+  if not (TVar.equal id id') then begin
+    if not (UF.union id id' env.env_cst) then raise (CannotUnify (GTypVar id, t))
+  end
 | GTypArrow _ | GTypRef _ ->
   try
     let () = occur_check env id t in
-    UF.set id t env.env_cst
+    if not (UF.set id t env.env_cst) then raise (CannotUnify (GTypVar id, t))
   with Occur -> raise (CannotUnify (GTypVar id, t))
 
 let eq_or_tuple eq t1 t2 = match t1, t2 with

test-suite/ltac2/typing.v

@@ -70,3 +70,8 @@ Print Ltac2 tuple0.
 Fail Ltac2 not_a_value := { contents := 0 }.
 Fail Ltac2 not_a_value := "nope".
 Fail Ltac2 not_a_value := list_length [].
+
+(** Named type variables can't be defined. *)
+
+Fail Ltac2 foo (x:'a) : 'b := x.
+Fail Ltac2 foo (x:'a) : int := x.

user-contrib/Ltac2/List.v

@@ -487,7 +487,7 @@ Ltac2 init (len : int) (f : int -> 'a) :=
   Control.assert_valid_argument "List.init" (Int.ge len 0);
   map f (seq 0 1 len).
 
-Ltac2 repeat (x : 'a) (n : 'int) :=
+Ltac2 repeat (x : 'a) (n : int) :=
   init n (fun _ => x).
 
 Ltac2 assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) :=
@@ -538,7 +538,7 @@ Ltac2 enumerate (ls : 'a list) :=
   combine (seq 0 1 (length ls)) ls.
 
 (* from Coq stdlib *)
-Ltac2 rec merge (cmp : 'a -> 'a -> int) (l1 : 'a list) (l2 : 'b list) :=
+Ltac2 rec merge (cmp : 'a -> 'a -> int) (l1 : 'a list) (l2 : 'a list) :=
   let rec merge_aux l2 :=
       match l1 with
       | [] => l2