application of binders and it's syntax sugar are not equivalent
i.e.
type boolean
type st<_>
type out<_>
type controlFlow<a,b> =
| ReturnControl b
| ContinueControl a
term cf_out<b,c> : st<controlFlow<(), b>> -> (b -> c) -> st<c>
term ass1<a,b> : boolean -> (boolean -> st<controlFlow<a, out<b>>>) -> st<controlFlow<a, out<b>>>
term ass2<a,b> : boolean -> (boolean -> st<controlFlow<a, out<b>>>) -> st<controlFlow<a, out<b>>>
term ret<b> : b -> st<controlFlow<(), out<b>>>
term test : (v : boolean) -> st<out<boolean>> =
let%cf_out res =
v;%ass1
v;%ass2
ret<boolean> v
in res
This gives this error:
This skeleton has type boolean but is expected to have type st<controlFlow<a, out<b>>>.
But if I do
term test : (v : boolean) -> st<out<boolean>> =
let%cf_out res =
v;%ass1
let%ass2 _ = v in
ret<boolean> v
in res
everything goes smoothly. Everything is good also in this case:
term test : (v : boolean) -> st<out<boolean>> =
let%cf_out res =
let%ass1 _ = v in
let%ass2 _ = v in
ret<boolean> v
in res