Function subtyping at depth with "enhancements"

[catalin-hritcu]

The following code works, I'm basically just giving another name to Cons:

val push : int -> list int -> Tot (s:(list int){Cons? s})
let push x xs = Cons x xs

One would of course expect to be able to eta reduce the definition of push and just write

let push = Cons

But that fails with:

Subtyping check failed; expected type (uu___:int -> uu___:(list int) -> Tot (s#4309:(list int){(b2t (uu___is_Cons s@0))})); got type (hd:int -> tl:(list int) -> Tot (list int))

Same issue if I write something in between:

let push x = Cons x

[catalin-hritcu]

Similar problem with projectors actually:

val pop : s1:(list int){length s1 > 0} ->
  Tot (s2:(list int){length s2 = length s1 - 1})
let pop = Cons?.tl

leads to

Subtyping check failed; expected type (s1:(s1#3729:(list int){(b2t (op_GreaterThan (length s1@0) 0))}) -> Tot (s2#3813:(list int){(b2t (op_Equality (length s2@0) (op_Subtraction (length s1@1) 1)))})); got type (projectee:(uu___#7083:(list int){(b2t (uu___is_Cons uu___@0))}) -> Tot (list int))

[mtzguido]

AFAICT this is unrelated to projectors/constructors and is more of a lack of subtyping at depth. See for instance:

(* Renaming Cons *)
val push : int -> list int -> Tot (list int)
let push x xs = Cons x xs

(* Trying to refine it *)
val push' : int -> list int -> Tot (x:list int{Cons? x})
let push' = push

The first bit works, but the second fails to prove a subtyping. Or a simpler example:

let f x = x + 1

val g : x:int -> y:int{y == f x}
let g = f (* fails without eta *)

[catalin-hritcu]

@mtzguido And is subtyping in depth supposed to not work for function types?

[mtzguido]

It could work, but I don't think this is easy. It's also not just subtyping, since int -> list int -> list int is clearly not a subtype of int -> list int -> x:list int{Cons? x}, even if Cons does indeed have both types. Same for g in my example.

Maybe @nikswamy has more insight.