Open mtzguido opened 1 year ago
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)
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)
This gives