Ltac2: named type variables can't be defined

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

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

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