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 `()`
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
 
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) *)