Incorrect extraction of GTot-subtyping

[gebner]

F* admits a subtyping rule for effectful functions such that a -> b is a subtype of a -> GTot b. However this rule implies that a function f can have both the type a -> b and the type a -> GTot b, even though one extracts to a function while the other is erased.

We can use this rule to easily convert an erased ghost function to a total function and then call it:

module GTotSub

let t = nat -> nat
let f : t = fun x -> x + 42

let s = nat -> GTot nat
let g : s = f

irreducible let force_smt (x:Type) : y:Type { x == y } = x
let h : t = (g <: force_smt t)

let uhoh = h 42

Extracting this module predictably results in an OCaml program that crashes when run:

open Prims
type t = Prims.nat -> Prims.nat
let (f : t) = fun x -> x + (Prims.of_int (42))
type s = unit

type 'x force_smt = 'x
let (h : t) = Obj.magic ()
let (uhoh : Prims.nat) = h (Prims.of_int (42))

[mtzguido]

Interesting. Slight minimization:

let t = nat -> nat
let s = nat -> GTot nat

let f : t = (fun n -> n)
let g : s = f

let _ = assert (has_type g t)

This is accepted from (roughly) HasType f t and (= g f) in the encoding. Reminds me of #2069, a similar issue where the lack of universes in the encoding produces more equalities than there should be.

[mtzguido]

#1390 is another related issue. We reject subeffecting a -> Tot b into a -> Tac b since we need some internal marker to make sure the tactics normalize properly. Instead one can eta-expand (we also considered using coercive subtyping so the typechecker would automatically do it, but did not implement it).

I would imagine without that patch we run into the issue for tactics (reifiable effects in general). And also forbidding subeffecting of Tot arrows into GTot arrows, without eta expanding, would avoid this issue I think (but it would probably be painful for users).