Improper handling of the $ qualifier on function arguments

[mtzguido]

Probably an F* issue

(Error 339) Internal error: unexpected unresolved (universe) uvar in deep_compress: 16
Domains.fst(47,51-47,58): (Error 12) Expected type "$f: Prims.unit
  -> Pulse.Steel.Wrapper.stt Prims.nat Steel.Effect.Common.emp (fun _ -> Steel.Effect.Common.emp)"; but "pth n" has type "_fret: Prims.unit
  -> Pulse.Steel.Wrapper.stt Prims.nat Steel.Effect.Common.emp (fun _ -> Steel.Effect.Common.emp)"
Domains.fst(47,13-47,58): (Error) Could not infer implicit arguments in Domains.spawn (Domains.pth n)
proof-state: State dump @ depth 12 (at the time of failure):
Location: Pulse.Typing.Env.fst(350,2-350,31)
Domains.fst(36,8-36,8): (Error 228) user tactic failed: `Pulse checker failed` (see also Pulse.Typing.Env.fst(350,2-350,31))

    module Domains
    
    open Pulse.Main
    open Pulse.Steel.Wrapper
    open Steel.Effect.Common
    
    assume val domain : a:Type -> (a -> vprop) -> Type
    
    assume val spawn :
     (#a:Type) -> (#pre : vprop) -> (#post : (a -> vprop)) ->
     ($f : unit -> stt a pre post) ->
     stt (domain a post) pre (fun _ -> emp)
    
    assume val join :
      (#a:Type) -> (#post : (a -> vprop)) ->
      domain a post ->
      stt a emp post
    
    let rec fib0 (n:nat) : nat =
      if n < 2 then n
      else fib0 (n-1) + fib0 (n-2)
    
    let just #a (x:a) : stt a emp (fun _ -> emp) =
      sub_stt _ _ (magic()) (magic ()) (return_stt x (fun _ -> emp))
    
    ```pulse
    fn pth (n:pos) (_:unit)
      requires emp
      returns n:nat
      ensures emp
    {
      fib0 (n-1)
    }
    ```
    
    ```pulse
    fn pfib (n:nat)
      requires emp
      returns n:nat
      ensures emp
    {
      if (n < 20) {
        fib0 n
      } else {
        //let c = (fun () -> just #_ (fib0 (n-1))) <: unit -> stt nat emp (fun _ -> emp);
        // let th = spawn #nat #emp #(fun _ -> emp) c;
        let th = spawn #nat #emp #(fun (n:nat) -> emp) (pth n);
        let r = 123; // fib (n-2) + join th;
        r
      }
    }
    ```

[nikswamy]

This now fails with a localized error on spawn (pth n), saying "Elaborated term has unresolved implicits". If you turn on print_implicits and print_universes you see

Bug45.spawn u#_ u#_ #Prims.nat #Pulse.Lib.Core.emp #(fun _ -> Pulse.Lib.Core.emp) (Bug45.pth n)

I'm not sure why we can't resolve at least the first universe var to 0.

If you make domain singly universe polymorphic:

assume val domain : a:Type u#a -> (a -> vprop) -> Type u#a

Then the universe inference works out, but the example still fails with

Expected type "$f: unit -> Prims.Tot (stt u#0 nat emp (fun _ -> emp))"; but "pth n" has type "_fret: unit -> Prims.Tot (stt u#0 nat emp (fun _ -> emp))"

not handling the $ qualifier correctly. Changing the title accordingly.