Inference with nested refinements

[nikswamy]

Nested refinement types are not inferred correctly in Pulse, requiring additional annotation

module BugRealRefinement
#lang-pulse
open Pulse.Lib.Pervasives

assume
val p (#a:Type0) (_:(option perm & a)) : slprop

[@@expect_failure]
fn test (#a:Type0) (x:a)
requires emp
ensures p (Some 1.0R, x) //this fails
{
  admit()
}

fn test (#a:Type0) (x:a)
requires emp
ensures p (Some #perm 1.0R, x) //needs a #perm annotation
{
  admit()
}


let full #a (x:a) : (option perm & a) = (Some 1.0R, x)
fn test2 (#a:Type0) (x:a)
requires emp
ensures p (full x) //or an indirection
{
  admit()
}