Preliminary work-around to only substitute by any/empty variables that were...

Preliminary work-around to only substitute by any/empty variables that were introduced by the tallying.

types/types.ml

@@ -2800,7 +2800,7 @@ module Positive = struct
         let () = Memo.add memo (pos,v) () in
         match v.def with
         |`Type d -> ()
-        |`Variable d when Var.Set.mem d delta -> ()
+        |`Variable d when Var.Set.mem d delta || not (Var.is_internal d) -> Hashtbl.replace vars d v
         |`Variable d ->
           begin try
             let td = Hashtbl.find vars d in
@@ -3333,7 +3333,7 @@ module Tallying = struct
     let aux ((`Var v) as alpha) (s,t) acc =
       (* we cannot solve twice the same variable *)
       assert(not(CS.E.mem alpha acc));
-      let pre = Printf.sprintf "_fr_%s_" (Var.id alpha) in
+      let pre = Printf.sprintf "#fr_%s_" (Var.id alpha) in
       let b = var (Var.fresh ~pre ()) in
       (* s <= alpha <= t --> alpha = ( s v fresh ) ^ t *)
       CS.E.add alpha (cap (cup s b) t) acc

types/var.ml

@@ -27,6 +27,11 @@ end
 include VAR
 
 let id (`Var x) = x.V.id
+let is_internal (`Var x) =
+  let s = x.V.repr in
+  String.length s >= 1 && s.[0] == '#'
+;;
+
 let pp ppf (`Var x) = Format.fprintf ppf "'%s" x.V.repr
 
 let mk ?repr id = `Var (V.make_id ?repr id)

types/var.mli

@@ -11,6 +11,7 @@ val pp : Format.formatter -> var -> unit
 val mk : ?repr:string -> string -> var
 val fresh : ?pre:string -> unit -> var
 val id : var -> string
+val is_internal : var -> bool
 
 module Set : sig
   include Custom.T