Incorrect erasure of function types

[gebner]

(Following up on the discussion we just had.)

F* treats function types with an erasable codomain as erasable themselves. For example, Type -> Type is erasable. If such a function type is hidden behind an interface, then F* will replace values of that function type by () which is incompatible with polymorphism. (In the same file, values of that type are erased to fun _ -> () which is fine.)

//==> FunErasureHelper.fsti <==
module FunErasureHelper

[@@must_erase_for_extraction]
val t : Type u#1

val x : t

val f : t * nat -> nat

//==> FunErasureHelper.fst <==
module FunErasureHelper

let t = Type0 -> Type0

let x = list

let generic_apply #a #b (f: (a -> b) * nat) (x: a) : b * nat =
  (f._1 x, f._2)

let f (x: t * nat) =
  (generic_apply x nat)._2

//==> FunErasure.fst <==
module FunErasure
open FunErasureHelper

let _ = f (x, 42) // <- crash

The last definition will crash, because x is incorrectly erased to (), and generic_apply then treats it as a function and calls it.