In the snippet below, we want to make a list of functions of some_ty, just like f1, but trying to write this list triggers an implicit instantiation for f1 and does not check. This should not happen IMO since the expected type for that position is some_ty, which has an implicit.
open FStar.List.Tot
let some_ty = (#x:int) -> l:(list int){length l == x} -> bool
let f1 : some_ty = fun _ -> true
let funcs : list some_ty = [f1]
Workarounds are annotating f1 <: some_ty or eta expanding (fun #x -> f1 #x).
Old issue, but something I'd like to revisit now.
In the snippet below, we want to make a list of functions of
some_ty, just likef1, but trying to write this list triggers an implicit instantiation forf1and does not check. This should not happen IMO since the expected type for that position issome_ty, which has an implicit.Workarounds are annotating
f1 <: some_tyor eta expanding(fun #x -> f1 #x).