From 43ba9f44634f2a5fda8f6ec75ae7c7f7bbfc8631 Mon Sep 17 00:00:00 2001
From: Tiago Soares <tl.soares@campus.fct.unl.pt>
Date: Sat, 28 Dec 2024 21:48:46 +0100
Subject: [PATCH 1/3] Fix bug in creation of fresh type variables

---
 src/dterm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/dterm.ml b/src/dterm.ml
index 2234e879..2a54b98d 100644
--- a/src/dterm.ml
+++ b/src/dterm.ml
@@ -249,7 +249,7 @@ let ts_of_dty = function Some dt_dty -> ts_of_dty dt_dty | None -> ts_bool
 let rec ty_of_dty_raw = function
   | Tvar { dtv_def = Some (Tty ty); _ } -> ty
   | Tvar { dtv_def = Some dty; _ } -> ty_of_dty_raw dty
-  | Tvar _ -> fresh_ty_var ~loc:Location.none "xi"
+  | Tvar _ as ty -> ty_of_dty ty
   | Tapp (ts, dl) -> ty_app ts (List.map ty_of_dty_raw dl)
   | Tty ty -> ty
 

From 80c9832df62b4b074cd2a2d6bc2f39c3600f3d09 Mon Sep 17 00:00:00 2001
From: Tiago Soares <tl.soares@campus.fct.unl.pt>
Date: Tue, 7 Jan 2025 14:49:25 +0100
Subject: [PATCH 2/3] Add test for type variables in HO functions

---
 test/typechecker/dune.inc      | 21 +++++++++++++++++++++
 test/typechecker/type_vars.mli |  3 +++
 2 files changed, 24 insertions(+)
 create mode 100644 test/typechecker/type_vars.mli

diff --git a/test/typechecker/dune.inc b/test/typechecker/dune.inc
index 8c3b6c1c..98a390e3 100644
--- a/test/typechecker/dune.inc
+++ b/test/typechecker/dune.inc
@@ -1052,6 +1052,27 @@
    (with-accepted-exit-codes 2
     (run ocamlc -c %{dep:type_arity5.mli})))))
 
+(rule
+ (deps
+  %{bin:gospel}
+  (:checker %{project_root}/test/utils/testchecker.exe))
+ (targets type_vars.gospel)
+ (action
+  (with-outputs-to type_vars.mli.output
+   (run %{checker} %{dep:type_vars.mli}))))
+
+(rule
+ (alias runtest)
+ (action
+  (diff type_vars.mli type_vars.mli.output)))
+
+(rule
+ (alias test-cmis)
+ (action
+  (chdir %{project_root}
+   ; Syntax sanity check
+   (run ocamlc -c %{dep:type_vars.mli}))))
+
 (rule
  (deps
   %{bin:gospel}
diff --git a/test/typechecker/type_vars.mli b/test/typechecker/type_vars.mli
new file mode 100644
index 00000000..db5379b2
--- /dev/null
+++ b/test/typechecker/type_vars.mli
@@ -0,0 +1,3 @@
+(*@ function f (f : 'a -> 'b) : 'a * 'b *)
+
+(*@ axiom test1 : forall x. f (fun _ -> x) = (x, x) *)

From 65c41f0987ee0c7e62a0ad0f15d1e53fe327601d Mon Sep 17 00:00:00 2001
From: Tiago Soares <tl.soares@campus.fct.unl.pt>
Date: Fri, 17 Jan 2025 16:51:58 +0100
Subject: [PATCH 3/3] Update changelog

---
 CHANGES.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index f9e135f0..25e170d8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -46,6 +46,8 @@
 
 ## Internals
 
+- Fix bug in creation of fresh type variables
+  [\#435](https://github.com/ocaml-gospel/gospel/pull/435)
 - Fix premature parsing of specification keywords in the preprocessor.
   [\#394](https://github.com/ocaml-gospel/gospel/pull/394)
 - Fix `ls_name` of `unit` logical symbol to be `()`