It’s cool! You are passing ~why_does_this_work:() to x, which you unpacked from the option. You guarantee that the option is non-empty by having failwith in the None branch.

My brain is still twisted. Can someone explain how f ~why_does_this_work:() is desugared?

It seems that the argument ~why_does_this_work:() is interpreted as Some g where g has type (why_does_this_work:unit -> 'a) option -> 'a. I can’t see by what rule it arrives at that?

The closest I got was:

let g =
function
| None -> failwith ""
| Some (x:(why_does_this_work:unit -> 'a)) -> ((failwith ""):'a)
in
f (Some g)

This is not desugaring. But it would compute the equivalent result. f ~why_does_this_work:() →
from definition of f: (function Some x -> x | None -> failwith "is none") ~why_does_this_work:() →
equivalent syntax that will be more convenient later: (fun z -> match z with Some x -> x | None -> failwith "is none") ~why_does_this_work:() →
eta expansion: (fun z ~why_does_this_work -> match z with Some x -> x ~why_does_this_work | None -> failwith "is none" ~why_does_this_work) ~why_does_this_work:() →
beta reduction: fun z -> match z with Some x -> x ~why_does_this_work:() | None -> failwith "is none" ~why_does_this_work:() →
equivalent syntax: function Some x -> x ~why_does_this_work:() | None -> failwith "is none" ~why_does_this_work:()

I guess what is surprising here is that the same example doesn’t work with a non-labelled argument, e.g.

# f ~why_does_this_work:();;
> (why_does_this_work:unit -> 'a) option -> 'a = <fun>
# f ();;
Error: This variant expression is expected to have type 'a option
There is no constructor () within type option

I didn’t fully realize labelled argument compilation did so much work under the hood.

edit: from a typing perspective, the compiler unifies why_does_this_work:unit -> 'b with 'a option -> 'a. The most general solution is to unify 'a with why_does_this_work:unit -> 'b, which after application of the labelled argument yields the result type.

This always confuses me too.
I think the rules are in this paper but I don’t really understand it. I remember reading a more understandable explanation of how this worked, but I can’t find it again…

(Then I had the same unification explanation that @igarnier gives)

I think that this is confusing when it happens involuntarily, and I’m not sure in which case it is useful, but I don’t know if it would be possible to have a warning for this, since it does make sense…

Edit: To give an example where this can be misleading, you can mistype a label and get some weird type error down the line.

# let f ~longlabel1 = function | Some x -> longlabel1 x | None -> failwith "is none";;
# f ~longlabel1:((+) 1) (Some 2);;
- : int = 3
# f ~longlabel2:((+) 1) (Some 2);;
- : longlabel1:(int -> longlabel2:(int -> int) -> '_weak1) -> '_weak1 = <fun>

This is because the labeled argument can be applied out-of-order. The eta-expansion in my explanation introduces the labeled parameter on the function side so that the labeled argument can be applied even though the non-labeled argument is still missing.