ocaml-gospel/gospel

Gospel does not parse `fun` type annotations as OCaml

Closed this issue · 2 comments

shym commented

The following code is accepted by the OCaml type checker:

  fun true : int -> 12

(besides the obviously non-exhaustive pattern true), meaning that the int is the return type but the Gospel typechecker accepts the following:

val f : int list -> int
(*@ y = f xs
    ensures List.for_all (fun x : int -> true) xs *)

where int is interpreted as the type for the argument x.

shym commented

#309 will change that situation:

val f : int list -> int
(*@ y = f xs
    ensures List.for_all (fun x : int -> true) xs *)

will now report a syntax error at : int as the type annotation is not handled by the parser.

Fixed by #309