SyntaxExtension: handle ticks in declarations

share/pulse/examples/Test.GenOrder2.A.fsti

@@ -0,0 +1,10 @@
+module Test.GenOrder2.A
+
+#lang-pulse
+open Pulse
+
+val foo : int -> int -> slprop
+
+fn flip ()
+  requires foo 'x 'y
+  ensures  foo 'y 'x

share/pulse/examples/Test.GenOrder2.B.fst

@@ -0,0 +1,12 @@
+module Test.GenOrder2.B
+
+#lang-pulse
+open Pulse
+open Test.GenOrder2.A
+
+fn test ()
+  requires foo 1 2
+  ensures  foo 2 1
+{
+  flip () #1 #2;
+}

src/syntax_extension/PulseSyntaxExtension.Desugar.fst

@@ -858,6 +858,13 @@ and desugar_decl (env:env_t)
 
   | Sugar.FnDecl { id; binders; ascription=Inl ascription; range } ->
     let! env, bs, bvs = desugar_binders env binders in
+
+    (* Process ticks *)
+    let fvs = free_vars_comp env ascription in
+    let! env, bs', bvs' = idents_as_binders env fvs in
+    let bs = bs@bs' in
+    let bvs = bvs@bvs' in
+
     let! comp = desugar_computation_type env ascription in
     let! qbs = map2 faux bs bvs in
     let comp = close_comp_bvs comp (List.Tot.map (fun (_,_,bv) -> bv) qbs) in