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.

[gebner]

Options:

• extend the attribute [@@erasable (fun _ -> ())]
• extend the attribute with the arity [@@erasable 1] (defaulting to zero) (maybe let erasable = erasable_at 0 or something)

TODO: erase must_erase_for_extraction as well

[gebner]

After giving this some more thought, I don't think we can make the arity version of the attribute work. Knowing the arity is enough to detect this issue, but not to produce the right code. During extraction, we still need to know which type to erase to: i.e., should we replace x: t by fun (x: unit) -> () or by fun (x: int) -> (). (ML expressions are typed after all.)

I only see two approaches left:

1. Specify the erasure replacement in the attribute, i.e., [@@erasable_to (fun (x: unit) -> ())]. You can always avoid the extra boilerplate with an explicit erased.
2. Enforce CMI extraction, we could then unfold the implementation type. Though we'd still need to fix extraction to erase to fun (x: unit) -> () instead of ().

[nikswamy]

There's a third option. Generate fun (x:Obj.t) -> (). ML expressions can be pretty weakly typed.