`PURE` effect produce error: expected type Type0; got type Type0

[ayanamists]

I'm now reading Dijkstra Monad for free and try this code :

val f (x:int) : PURE int (fun post -> forall y. y >= 0 ==> post y)
let f x = op_Multiply x x

fstar.exe output:

(Error 19) Subtyping check failed; expected type Type0; got type Type0; The SMT solver could not prove the query. Use --query_stats for more details. (see also prims.fst(326,38-326,60))

It seems to complain that int should be Type0 but got Type0 (For me, this error is confusing)

Do I make any mistake ? Or fstar prevent user from using PURE effect directly ?

The version info of fstar.exe

❯ fstar.exe --version
F* 2022.11.07~dev
platform=Linux_x86_64
compiler=OCaml 4.13.1
date=2022-11-15 11:31:09 +0530 
commit=255906d3ecffc3d321c5cdc84ffe430ae5ac5245

[aseemr]

Hi @ayanamists, the error message is confusing here. The issue is regarding the monotonicity property of the wp argument of PURE.

We don't normally use PURE directly but rather use its Hoare-style variant Pure; it is more readable and also gets past this monotonicity requirement.

let g (x:int) : Pure int (requires True) (ensures fun y -> y >= 0) = op_Multiply x x

To convince F* that the wp written in your example is monotonic (you can see the definition of monotonicity in ulib/prims.fst), we need to use the as_pure_wp combinator from ulib/FStar.Monotonic.Pure:

val f (x:ℤ) : PURE ℤ (as_pure_wp (λ post → ∀ y. y ≥ 0 ⟹ post y))
let f x = op_Multiply x x

But we should fix the error message in any case.

[ayanamists]

Hi @ayanamists, the error message is confusing here. The issue is regarding the monotonicity property of the wp argument of PURE.

We don't normally use PURE directly but rather use its Hoare-style variant Pure; it is more readable and also gets past this monotonicity requirement.

let g (x:int) : Pure int (requires True) (ensures fun y -> y >= 0) = op_Multiply x x

To convince F* that the wp written in your example is monotonic (you can see the definition of monotonicity in ulib/prims.fst), we need to use the as_pure_wp combinator from ulib/FStar.Monotonic.Pure:

val f (x:ℤ) : PURE ℤ (as_pure_wp (λ post → ∀ y. y ≥ 0 ⟹ post y))
let f x = op_Multiply x x

But we should fix the error message in any case.

I got it. Thank you for your reply!

[aseemr]

I have pushed a small fix so that the error message is now:

Test.fst(4,38-4,65): (Error 19) Subtyping check failed; expected type wp: Prims.pure_wp' Prims.int {Prims.pure_wp_monotonic Prims.int wp}; got type post: (_: Prims.int -> Prims.logical) -> Prims.logical; The SMT solver could not prove the query. Use --query_stats for more details. (see also prims.fst(326,38-326,60))

And it highlights the wp body.

Thanks again for the report.