Extracting higher-order calls
The following program satisfies Why3’s type checker:
let f (g: unit -> 'a) : 'a = g ()
let g (_:unit) = ()
let good = f (fun x -> g x)
let bad = f g
But the extracted OCaml program contains a spurious ()
in line 7 resulting in type error
(characters 12-18: Error: This expression has type unit but an expression was expected of type unit -> 'a
):
let f (g: unit -> 'a) : 'a = g ()
let g (_: unit) : unit = ()
let good = f (fun (x: unit) -> g x)
let bad = f (g ())