clean the new implementation of variable

Expose the flags to avoid having the possibility to have
two variables with the same id but different flags.

lib/common/Type.ml

@@ -316,7 +316,8 @@ let rec refresh_variables bdgs env (t : t) =
   match t with
   | Var v ->
     let v' =
-      Variable.HMap.get_or_add bdgs ~f:(fun _ -> Variable.Gen.gen env.Env.var_gen) ~k:v
+      Variable.HMap.get_or_add bdgs
+        ~f:(fun _ -> Variable.(Gen.gen Flags.empty env.Env.var_gen)) ~k:v
     in
     var env v'
   | Constr (lid, t) -> constr env lid (Array.map (refresh_variables bdgs env) t)
@@ -413,12 +414,12 @@ let outcome_of_string (str : String.t) =
   parse_to_outcome parse_ty
 
 let generate_var bdgs (env : Env.t) = function
-  | None -> var env @@ Variable.Gen.gen env.var_gen
+  | None -> var env @@ Variable.(Gen.gen Flags.empty env.var_gen)
   | Some name -> (
       match String.HMap.get bdgs name with
       | Some v -> var env v
       | None ->
-          let v = Variable.Gen.gen env.var_gen in
+          let v = Variable.(Gen.gen Flags.empty env.var_gen) in
           String.HMap.add bdgs name v;
           var env v)
 

lib/common/Variable.ml

@@ -39,12 +39,10 @@ let compare v1 v2 = CCInt.compare v1.id v2.id
 let equal v1 v2 =
   if CCInt.equal v1.id v2.id then (assert (Flags.equal v1.flags v2.flags); true) else false
 
-let set_non_arrow v = {v with flags = Flags.(set non_arrow v.flags)}
 let is_non_arrow v = Flags.(get non_arrow v.flags)
 
 let merge_flags v1 v2 gen =
-  let {id; _} = gen () in
-  {id; flags = Flags.union v1.flags v2.flags}
+  gen (Flags.union v1.flags v2.flags)
 
 module Map = CCMap.Make (struct
     type nonrec t = t
@@ -76,8 +74,8 @@ module Gen  = struct
   let make () =
     ref 0
 
-  let gen t =
-    { id = CCRef.get_then_incr t; flags = Flags.empty }
+  let gen flags t =
+    { id = CCRef.get_then_incr t; flags }
 
 end
 

lib/common/Variable.mli

@@ -1,17 +1,28 @@
+module Flags : sig
+  type t
+  type field
+
+  val empty : t
+  val non_arrow : field
+
+  val set : field -> t -> t
+
+  val union : t -> t -> t
+end
+
 type t
 type var = t
 
 val as_int : t -> int 
 val equal : t CCEqual.t
 val compare : t CCOrd.t
 
-val set_non_arrow : t -> t
 val is_non_arrow : t -> bool
 
 (** [merge v1 v2 gen] merge the flags of v1 v2 into a fresh variable
     created by gen. 
  *)
-val merge_flags : t -> t -> ( unit -> t) -> t
+val merge_flags : t -> t -> ( Flags.t -> t) -> t
 
 module Map : CCMap.S with type key = t
 module HMap : CCHashtbl.S with type key = t
@@ -33,7 +44,7 @@ module Gen : sig
   type t
 
   val make : unit -> t
-  val gen : t -> var
+  val gen : Flags.t -> t -> var
 
 end
 

lib/unification/AC.ml

@@ -296,7 +296,7 @@ end = struct
   let dioph2env env ({System. nb_atom; assoc_type; first_var; _} as system) sol =
     let symb, start_i =
       if first_var = 0 then
-        Type.var (Env.tyenv env) (Env.gen env), 0
+        Type.var (Env.tyenv env) (Env.gen Variable.Flags.empty env), 0
       else get_first_assoc_type sol system
     in
     let env = Env.copy env in

lib/unification/Env.ml

@@ -26,7 +26,7 @@ let copy { tyenv ; vars ; tuples ; arrows; partials ; orig_vars } =
 
 let vars e = e.vars
 let tyenv t = t.tyenv
-let gen e : Variable.t = Variable.Gen.gen e.tyenv.var_gen
+let gen flags e : Variable.t = Variable.Gen.gen flags e.tyenv.var_gen
 
 let add e v ty = e.vars <- Subst.add v ty e.vars
 

lib/unification/Env.mli

@@ -4,7 +4,7 @@ type t
 
 val make : tyenv:Type.Env.t -> orig_vars:Variable.Set.t -> t
 val copy : t -> t
-val gen : t -> Variable.t
+val gen : Variable.Flags.t -> t -> Variable.t
 val vars : t -> Subst.t
 
 val tyenv : t -> Type.Env.t

lib/unification/Syntactic.ml

@@ -197,15 +197,18 @@ and non_proper env stack (x : Variable.t) (y : Variable.t) =
      Env.representative env y) with
   | (V x' | E (x', _)), (V y' | E (y', _)) when Variable.equal x' y' -> process_stack env stack
   | V x', V y' ->
-      let t = Type.var (Env.tyenv env) (Variable.merge_flags x' y' (fun () -> Env.gen env)) in
+      let t =
+        Type.var (Env.tyenv env)
+          (Variable.merge_flags x' y' (fun flags -> Env.gen flags env))
+      in
       let* () = attach env x' t in
       let* () = attach env y' t in
       process_stack env stack
   | V x', E (_, t) | E (_, t), V x' ->
       let* () = attach env x' t in
       process_stack env stack
   | E (x', s), E (y', t) ->
-      let z' = Variable.merge_flags x' y' (fun () -> Env.gen env) in
+      let z' = Variable.merge_flags x' y' (fun flags -> Env.gen flags env) in
       let tv = Type.var (Env.tyenv env) z' in
       let* () = attach env x' tv in
       let* () = attach env y' tv in

lib/unification/Unification.ml

@@ -38,7 +38,7 @@ and solve_arrow_problem env0 { ArrowTerm.left; right } =
         ("Right", `String (CCFormat.sprintf "%a" ArrowTerm.pp right));
       ])
     @@
-  let ret_type = Type.var (Env.tyenv env0) (Env.gen env0 |> Variable.set_non_arrow) in
+  let ret_type = Type.var (Env.tyenv env0) (Env.gen Variable.Flags.(set non_arrow empty) env0) in
   let potentials =
     [
       (* TODO: When doing AL = AR if they are both tuples of size 1 it is useless  *)
@@ -57,7 +57,7 @@ and solve_arrow_problem env0 { ArrowTerm.left; right } =
           *)
           Trace.with_span ~__FUNCTION__ ~__FILE__ ~__LINE__
             "AL * αL ≡? AR  ∧  BL ≡? αL -> BR" (fun _sp ->
-              let var_arg_left = Env.gen env in
+              let var_arg_left = Env.gen Variable.Flags.empty env in
               Env.push_tuple env
                 (ACTerm.add left.args (Type.var (Env.tyenv env) var_arg_left))
                 right.args;
@@ -73,7 +73,7 @@ and solve_arrow_problem env0 { ArrowTerm.left; right } =
           *)
           Trace.with_span ~__FUNCTION__ ~__FILE__ ~__LINE__
             "AL ≡? AR * αR  ∧  αR -> BL ≡? BR" (fun _sp ->
-              let var_arg_right = Env.gen env in
+              let var_arg_right = Env.gen Variable.Flags.empty env in
               Env.push_tuple env left.args
                 (ACTerm.add right.args (Type.var (Env.tyenv env) var_arg_right));
               let* () = insert env ret_type left.ret in
@@ -89,8 +89,8 @@ and solve_arrow_problem env0 { ArrowTerm.left; right } =
           *)
           Trace.with_span ~__FUNCTION__ ~__FILE__ ~__LINE__
             "AL * αL ≡? AR * αR  ∧  BL ≡? αL -> β  ∧  αR -> β ≡? BR" (fun _sp ->
-              let var_arg_left = Env.gen env in
-              let var_arg_right = Env.gen env in
+              let var_arg_left = Env.gen Variable.Flags.empty env in
+              let var_arg_right = Env.gen Variable.Flags.empty env in
               (* TOCHECK *)
               Env.push_tuple env
                 (ACTerm.add left.args (Type.var (Env.tyenv env) var_arg_left))