val declaration + let works differently from the new let (x:t) : M b notation

[jkzinzindohoue]

In the following snippet, the first add function typechecks, but not the second while I would expect the two to be equivalent.

module Test

type new_int (z:int) = x:int{x = z}

val add:  new_int 1 -> new_int 2 -> Tot (new_int 3)
let add a b = a + b

let add' (a:new_int 1) (b:new_int 2) : Tot (new_int 3) = a + b // fails to typecheck

On add' F* returns test.fst(8,39-11,6): could not prove post-condition

[nikswamy]

Also observing that the notation has a negative impact on extraction.

This version extracts fine:

module TestExtraction 
let st_pre = int -> Type0
let st_post (a:Type) = (a * int) -> Type0
let st_wp (a:Type) = int -> st_post a -> Type0
val st_bind_wp : (a:Type) -> (b:Type) -> (f:st_wp a) -> (g:(a -> Tot (st_wp b))) -> Tot (st_wp b)
let st_bind_wp a b f g = 
    fun n0 post -> f n0 (fun x_n1 -> g (fst x_n1) (snd x_n1) post)

to

open Prims

type st_pre =
Prims.int  ->  Obj.t


type 'Aa st_post =
('Aa * Prims.int)  ->  Obj.t


type 'Aa st_wp =
Prims.int  ->  Prims.unit  ->  Obj.t


type ('Aa, 'Ax, 'An0, 'Apost) st_return_wp =
Prims.unit


type ('Aa, 'Ab, 'Af, 'Ag, 'An0, 'Apost) st_bind_wp =
'Af

However, this version gets the arity of st_bind_wp wrong after extraction.

module TestExtraction 
let st_pre = int -> Type0
let st_post (a:Type) = (a * int) -> Type0
let st_wp (a:Type) = int -> st_post a -> Type0
let st_bind_wp (a:Type) (b:Type) (f:st_wp a) (g:(a -> Tot (st_wp b))) : st_wp b = 
    fun n0 post -> f n0 (fun x_n1 -> g (fst x_n1) (snd x_n1) post)

Here it is after extraction:

open Prims

type st_pre =
Prims.int  ->  Obj.t


type 'Aa st_post =
('Aa * Prims.int)  ->  Obj.t


type 'Aa st_wp =
Prims.int  ->  Prims.unit  ->  Obj.t


type ('Aa, 'Ab, 'Af, 'Ag) st_bind_wp =
'Af

[nikswamy]

The original problem should be improved now.

However, the extraction problem remains.

Also, some very disturbing pathologies remain. The combination of pattern matching notation in the arguments of a function and this inline annotation of the result type-and-effect is badly broken.

This program fails to verify:

module Test
assume val good : int -> Type0
assume val x:int
let f () : Lemma (good x) = admit()
let g () =
  f();
  assert (good x)

Whereas this one is fine:

module Test
assume val good : int -> Type0
assume val x:int
let f (u:unit) : Lemma (good x) = admit()
let g () =
  f();
  assert (good x)

Astoundingly, in the first example, the let f () = ... is a pattern matching of that is desugared to
let f (u:unit) = match u with | () -> (admit():Lemma (good x)) The body of the function is checked to have the expected type, but then at the top-level, default effects kick in because the function appears unannotated, and f just has type unit -> Tot unit for the rest of the program.

[nikswamy]

I've fixed a few things, eliminating all the known symptoms of this bug.

1. You can no longer write stuff like:

let f (x1, x2) : Tot (y:nat{y= x1 + x2}) = x1 + x2

The combination of pattern matching on (x1, x2) with the scoping rules for effect annotations etc. was getting too complex to be sustainable. This will now fail with a desugaring error:

.\test.fst(3,6-3,14) : Error
Computation type annotations are only permitted on let-bindings without inlined patterns; replace this pattern with a variable

1. The extraction bug is fixed also. There was a missing normalization of abstractions prior to extracting type abbreviations.

Closing it. Hopefully this will not raise its ugly head anymore. Fingers crossed.