Working with computed function types painful

[catalin-hritcu]

I'm encountering strange failures with computed function types in stlc-norm (https://github.com/yforster/stlc-norm/blob/master/StlcNormalizing.fst#L277) and since I was a bit stuck there (now not any more) I wanted to try if computed function types work in much simpler examples, and the results are quite mixed, including one Unexpected error and some regular failures too.

val t : bool -> Tot Type0
let t b = if b then int else (int -> Tot int)

(* CH: at the top level everything explodes  *)
(* val f0 : t false *)
(* let f0 n = n *)
(* Error: Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error. *)
(* Failure("Impossible! let-bound lambda Bug578.f0 = (fun n -> n@0) has a type that's not a function: ((_:Prims.int -> Tot Prims.int) : Type)\n") *)

(* CH: or just fails to work *)
(* val f1 : unit -> t false *)
(* let f1 () n = n *)
(* ./bug578.fst(13,24-14,15) : Error *)
(* Expected a term of type "(uu___:Prims.unit -> (Bug578.t false))"; *)
(* got a function "(fun uu___ n -> n@0)" (Function definition takes more arguments than expected from its annotated type) *)

(* CH: this fails too *)
(* val f2 : unit -> t false *)
(* let f2 () = (fun n -> n) *)
(* ./bug578.fst(21,24-22,24) : Error *)
(* Expected a term of type "(uu___:Prims.unit -> (Bug578.t false))"; *)
(* got a function "(fun uu___ n -> n@0)" (Function definition takes more arguments than expected from its annotated type) *)

(* CH: And when things get trickier things fail too *)
(* val f3 : b:bool -> (if b then int else int -> Tot int) *)
(* let f3 b = if b then 42 else (fun n -> n) *)
(* ./bug578.fst(29,29-29,41): Failed to resolve implicit argument of type 'Type' introduced in (?39422 b uu___) because user-provided implicit term *)

(* CH: ... and again *)
(* val f4 : b:bool -> t b *)
(* let f4 b = if b then 42 else (fun n -> n) *)
(* ./bug578.fst(31,29-31,41): Failed to resolve implicit argument of type '((fun b uu___ -> Type) b uu___)' introduced in (?17835 b uu___) because user-provided implicit term *)

(* CH: ... or they succeed with additional type annotations *)
val f5 : b:bool -> t b
let f5 b = if b then 42 else (fun (n:int) -> n)

val aux : int -> Tot int
let aux n = n
val f6 : b:bool -> t b
let f6 b = if b then 42 else aux

[catalin-hritcu]

This is as bad as before, in fact one of the things that worked (f2) now started to fail too. On the positive side, one of the explosions become a spurious error. Updated the error messages above.

[catalin-hritcu]

Discussed a bit with Nik about this and he thinks that some of the last examples (f3 and f4) are quite hopeless for the way we currently type-check match, by adding equality constraints and handing it to the SMT solver, since in this case the normalizer can't do its thing on the types. He's wondering whether it's time for a match-as-in-return variant like in Coq that one could use in such cases.

[nikswamy]

Only hopeless without annotations. With explicit ascriptions in the branches, it should be made to work. E.g. (fun n -> n) <: t false

Whether that's more palatable that the match-return syntax remains to be seen

[mtzguido]

f0, f1 and f2 now work. The situation is the same for f3 and f4 (they work with annotations).