Closures do not behave uniformly

[annenkov]

I hit the following issue when using closures in Liquidity.

The example below does not compile giving Types ((int -> int)[@closure :int]) and int -> int are not compatible

let my_map (f : int -> int) (xs : int list) =
  List.map f xs
  
let bar (i : int) (xs : int list) =
  my_map (fun (x : int) -> x + i) xs

It seems like types of closures get extra typing information about the environment wrt. which they are closed. The same problem prevents returning closures from different branches, that are supposed to have the same type:

let return_closure (x : int) : int -> int =
  if x = 0 then fun y : int -> y
  else fun y : int -> x + y

In this case, the type of the second branch is ('c4 -> int)[@closure :int], while I expected it to be of a function type.

This problem disallows many usual functional programming patterns. We are currently working on extracting verified Liquidity code from the Coq proof assistant and in several cases code didn't compile because of this issue with closures.

Would it be possible to fix closures so the types of variables didn't show up in the type of a closure?