Inconsistent subtyping with covariance

[gebner]

This is an MWE extracted from the issue I had in the thunk module I showed yesterday. There are three types here, r is a subtype of s, which is in turn a subtype of t.

module Subtyping

let t = unit -> Dv nat
let s = unit -> Dv (n:nat { n >= 42 })
let f (x: nat) : s = fun _ -> x + 42
let p (g: t) = exists x. f x == g
let r = x:t { p x }

let does_work_1 (x: s) : t = x
let does_work_2 (x: r) : t = x
[@@expect_failure] let should_work_3 (x: r) : s = x

let elim_subtype #a (#b:_ { subtype_of a b }) (x: a) : b = x

[@@expect_failure] let should_work_4 (x: s) : t = elim_subtype x
let does_work_5 (x: r) : t = elim_subtype x
let does_work_6 (x: r) : s = elim_subtype x

[@@expect_failure] let should_work_7 : squash (subtype_of s t) = ()
let does_work_8 : squash (subtype_of r t) = ()
let does_work_9 : squash (subtype_of r s) = ()

If we replace Dv by Tot, then 4 and 7 work but 3 still fails.