ifuel 0 breaks unfolding

[gebner]

The below file works if you comment out the --ifuel 0. This seems to be another instance of Pulse gratuitously re-typechecking things plus an unclear dependency on ifuel--the regular F* definition checks just fine with the same options (?!).

module UnfoldTc
open Pulse.Nolib
#lang-pulse

#push-options "--ifuel 0"

assume val foo (n: nat) : bool & s:Seq.seq bool { Seq.length s == n }

let bar (n: nat) : slprop =
  pure (Seq.index (snd (foo (n + 1))) n == false)

fn baz (n: nat)
  requires bar n
{
  unfold bar
  // Expected term of type slprop
  // got term pure (Seq.Base.index (snd (foo (n + 1))) n == false)
}