Crash on lambda

[mtzguido]

trafficstars

let fix_1
  (#a : Type)
  (#r : (xa:a -> Type))
  (#sz : Type)
  (m : a -> sz)
  (ff : (x1:a -> (y1:a{m y1 << m x1} -> Tot (r y1)) -> Tot (r x1)))
  : x:a -> Tot (r x)
  = let rec f x : Tot (r x) (decreases m x) =
      ff x f
    in
    f


assume val stt : Type -> Type0

let tes1 (#a : Type) (#b : a -> Type)
  (kk : ((y:a -> stt (b y)) -> x:a -> stt (b x) ))
  : x:a -> stt (b x)
  =
  fix_1 id (fun k x -> kk x k)

This gives

* Error 230 at Bug.fst(23,16-23,17):
  - Variable "x#701" not found

[mtzguido]

Side note: this program

let pk (x:int) (r : (y:int{x==0} -> int)) : Type u#a =
  y:int{x==0} -> Tot (r y)

gives:

* Error 12 at Bug.fst(9,23-9,28):
  - Expected type "Type"; but "r y" has type "Prims.int"

Verified module: Bug
2 errors were reported (see above)

which makes sense except for the count. Internally this error was raised twice, and using --print_full_names shows them both:

* Error 12 at Bug.fst(9,23-9,28):
  - Expected type "Type"; but "r7 y28" has type "Prims.int"

* Error 12 at Bug.fst(9,23-9,28):
  - Expected type "Type"; but "r72 y96" has type "Prims.int"

Verified module: Bug
2 errors were reported (see above)

[mtzguido]

Minimized a bit more

module Bug3057

let fix_1
  (#r : (nat -> Type))
  (ff : (x1:nat -> (y1:nat{y1 < x1} -> Tot (r y1)) -> Tot (r x1)))
  : Tot (r 0)
  = ff 0 (fun _ -> 0)

let tes1 
  (kk : ((y:nat -> nat) -> x:nat -> nat))
: nat
= fix_1 #_ (fun x k -> kk k x)