Refinement subtypes being discarded

[amosr]

Hi, I came across a bug which allowed me to use integer division in a context that required a function of type int -> int -> int. This should be a type error because the rhs of the division is not nonzero.

I've tried to minimise it, so the concepts might not make much sense, but I think they're required to make a complex result type that eventually normalises to int -> int -> int. The last four lines show the inconsistency. The unminimised version is here: https://github.com/songlarknet/pipit/blob/submit/ecoop24/src/Pipit.Prim.Vanilla.fst

module Test.Div

type funty (valty: Type) =
 | FTVal: t: valty -> funty valty
 | FTFun: t: valty -> rest: funty valty -> funty valty

let rec funty_sem (#ty: Type) (ty_sem: ty -> eqtype) (ft: funty ty) =
  match ft with
  | FTVal t -> ty_sem t
  | FTFun t r -> (ty_sem t -> funty_sem ty_sem r)

type valtype =
 | TInt:  valtype

let ty_sem (t: valtype): eqtype = match t with
 | TInt  -> int

type prim_arith =
 | P'A'Div

let prim_arith_ty (p: prim_arith) (at: valtype): funty valtype = match p with
 | P'A'Div -> FTFun at (FTFun at (FTVal at))

let prim_arith_sem (p: prim_arith): funty_sem ty_sem (prim_arith_ty p TInt) =
  fun x y -> x / y

let div_is_int_to_int: int -> int -> int =
  prim_arith_sem P'A'Div