Extraction preserves GTot predicates as type argument

[jroesch]

Bad.fst:

module Bad

open FStar.HyperStack.ST
module HS =  FStar.HyperStack

val do_while:
   inv:(unit -> GTot Type0) ->
    Stack unit (fun _ -> True) (fun _ _ _ -> True)
let rec do_while inv = ()

Bad.ml:

open Prims
let rec do_while : 'Ainv . Prims.unit = ()

It seems that extraction preserves predicates of this form when they are the first argument to a function, for example consider Okay.fst

In Okay.ml we can see the argument has been erased to a unit argument, which can be optimized by later Kremlin passes if my understanding is correct.

module Okay

open FStar.HyperStack.ST
module HS =  FStar.HyperStack

val do_while:
   other:int ->
   inv:(unit -> GTot Type0) ->
    Stack unit (fun _ -> True) (fun _ _ _ -> True)
let rec do_while other inv = ()

open Prims
let rec do_while : Prims.int -> Prims.unit -> Prims.unit =
  fun other  -> fun inv  -> () %

To further elaborate this works fine in ML, but is problematic when being plumbed through later passed to Kremlin because it creates a type application that is unusable by monomorphization, ater triggering an error in Kremlin. The predicate should be erased, so this kind of code can be compiled as a monomorphic function.

[jroesch]

F* 0.9.4.3
platform=Darwin_x86_64
compiler=OCaml 4.04.0
date=2017-07-21T10:22:16-07:00
commit=d3acbe6b8 (dirty)

[jroesch]

cc @nikswamy @protz

[jroesch]

One more comment for debugging, I believe that this issue was not due to my changes for monomorphization, because the type applications generated come directly from the type schemes we build for functions, and the type scheme seems to have left this argument as a type parameter.