Merge pull request #435 from mrjazzybread/bugfix

Fix bug in creation of fresh type variables

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

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
 

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}

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