Annotated function types with more than 3 parameters fail in non-interactive mode

[gebner]

module Problem
#lang-pulse
open Pulse

type a =
type b =
type c =
type d =
type f =

let ok (x:a) (y:b) (z:c) (w:d) (u:f) : slprop =
  emp

let ty (x:a) (y:b) (z:c) (w:d) = u:f -> stt unit emp (fun r -> ok x y z w u)

fn foo x y z w : ty x y z w  = u {
  fold ok x y z w u;
}

This is an interesting one:

• It works interactively, in vscode.
• It works after removing the w:d.
• But it fails on the command-line:

❯ fstar.exe --include $PULSE_HOME/lib/pulse Problem.fst
* Error 228 at Problem.fst(15,36-15,36):
  - Could not check term:
        x -> y -> z -> w -> u79: Problem.f
          -> Pulse.Lib.Core.stt Prims.unit
              Pulse.Lib.Core.emp
              (fun _ -> Problem.ok x y z u79 u79)

* Error 189 at Problem.fst(17,26-17,27):
  - Expected expression of type d got expression u9 of type f
  - Raised within Tactics.refl_instantiate_implicits
  - See also Problem.fst(15,34-15,35)

2 errors were reported (see above)

[gebner]

According to git bisect, this was broken by the recent gensym changes: 16b55bffd981546a19ccaa65a6da7998680aa0e5 (https://github.com/FStarLang/FStar/pull/3515)

[mtzguido]

Ouch. Looks like a name clash right? I remember some discussions about F's gensym and Pulse's gensym clashing, but I forget the exact details. Probably the stabler and smaller F gensym'd numbers now clash more easily?

[gebner]

I think you're right about the name clash. Making the Pulse vars start at 10000 lets the example pass:

diff --git a/src/checker/Pulse.Typing.Env.fst b/src/checker/Pulse.Typing.Env.fst
index c3fad92f1..c5ae01cd9 100644
--- a/src/checker/Pulse.Typing.Env.fst
+++ b/src/checker/Pulse.Typing.Env.fst
@@ -106,7 +106,7 @@ let rec max (bs:list (var & typ)) (current:var)

 let fresh g =
   match g.bs with
-  | [] -> 1
+  | [] -> 10000
   | (x, _)::bs_rest ->
     let max = max bs_rest x in
     max + 1

I'm not sure where we get the F* gensym variables from, though.

[gebner]

I'm not sure where we get the F* gensym variables from, though.

I think that was the wrong question. The question is where F is getting the Pulse gensym variables from and that is easy to answer. We're running the F type-checker on u:f -> stt unit emp (fun r -> ok x y z w u), then the F* type-checker creates a new variable to go under this binder, and this new variable clashes with the existing one previously created by Pulse.