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.