Unfolding predicates with implicits tagged with default arguments

[nikswamy]

This works:

let pred (x:int) : slprop = emp
fn test (x:int)
requires pred x
ensures emp
{
  unfold pred;
}

But, this fails and the error location blamed spans part of the definition of pred2 and part of the definition of test2.
If you remove the implict argument f then it succeeds.

let gpu_array (a:Type0) (sz:nat) : Type0 = unit
let pred2 (#a:Type0)
  (#sz:nat)
  (arr : gpu_array a sz)
  (#[exact (`1.0R)] f : perm)
  (i:nat)
  (v:a)
: slprop
= emp
fn test2 #a #sz (arr:gpu_array a sz) i v
requires pred2 arr i v
ensures emp
{
  unfold pred2;
}

A smaller variant behaves similarly, but this time the error range blamed on failure is different ... it blames both the unfold and the arr:tt binder in pred3.

let tt : Type0 = unit
let pred3 
  (arr : tt)
  (#[exact (`1.0R)] f : perm)
  (i:nat)
: slprop
= emp
fn test3 (arr:tt) i
requires pred3 arr i
ensures emp
{
  unfold pred3;
}