Expressions of the form

let f x : t2 = e1 <: refinedtype     // x not free in e1
let g (x : t1) : t2 = e2 <: refinedtype     // x may be free in e1

where refinedtype is a refinement type (e.g. b:bool{false}) appear to ignore the refinements on the type ascription. For example, the following bindings are unexpectedly not rejected:

let f x : bool = true <: (b:bool{false})
let g (x : bool) : bool = x <: (b:bool{false})

Note that the ascription isn't totally ignored, it just seems to be the refinement: if it is a refinement of a different type altogether then it still fails (e.g. b:int{false} when bool is expected). The refinement is also still used for type inference, as such the following fails as expected when checking q

let h x : bool = x <: (b:bool{false})
let q = f true

Note also, that this doesn't seem to occur for non-parameterised lets: the following fails as expected:

let z : bool = true <: (b:bool{false})

Tested on fstar_2021.06.06_Windows_x64 (from the website) and fstar_2022.02.12_Windows_x64 (latest pre-release from GitHub)

Still occurring in 2025.02.06 (Windows x64)