Hmm… I’m not sure if it conveys the idea better, but I’ll break down how the type of the function is interpreted by the compiler to see if it helps understanding why the type itself is problematic.
The type we’re starting from is:
?c:'a container -> unit -> 'a
Let’s first remove the optional argument and replace it with an option, and remove the unit:
'a container option -> 'a
This is a bit simpler and shows the same problem.
One thing that is important is that this type is given to a toplevel binding. Either in a module signature, like in my example, or just by typing the let-binding in your original example. This means that the type variable 'a is interpreted as universally quantified (“for all alpha …”), and the type is actually:
'a . 'a container option -> 'a
Or equivalently, if you prefer local types:
type t. t container option -> t (* Note: this version is not valid syntax in signatures *)
I think it is a bit unfortunate that quantification is not more explicit in OCaml; here are a few more examples where this is felt:
type 'a r = {
id1 : 'a -> 'a; (* monomorphic function, whose type is linked to the type parameter *)
id2 : 'a. 'a -> 'a; (* polymorphic function, independent of the type parameter *)
}
module M = struct
let g : 'a -> 'a = fun x -> x (* variable bound at the definition of g, and generalized *)
let v = (g 0, g false) (* works, as g is polymorphic *)
end
let v =
let g : 'a -> 'a = fun x -> x in (* variable bound at the definition of v, not generalizable *)
(g 0, g false) (* compilation error, as g is not polymorphic *)
let v =
let g : 'a. 'a -> 'a = fun x -> x in (* Explicit polymorphic annotation *)
(g 0, g false) (* works, as g is polymorphic *)
Anyway, back to our initial problem.
Since its type is polymorphic, you can use the function with any instantiation of the type variable. So the following are all valid:
let f : type t. t container option -> t = ...
let f_int : int container option -> int = f
let f_bool : bool container option -> bool = f
let f_string : string container option -> string = f
Something already looks fishy: the bool and string versions return booleans and strings, even though you expected the default case to return an integer. But the following is also allowed, and more obviously wrong:
let f_float : float container option -> float = f
You don’t expect f_float to actually return a floating point number, and you don’t want your function to raise an exception or loop infinitely, so the only hope is that it is impossible to actually create a value of type float container option. If you don’t have the option, it works: the GADT constraints actually ensure that such inputs don’t exist. You can try it with the unbox function:
let unbox : type t. t container -> t = ...
let unbox_float : float container -> float = unbox
It compiles, but you will never be able to get a float out of unbox_float because you cannot create a value of type float container to pass to it.
But with the option, it doesn’t work anymore: None can have type t option for any t, including types for which no value exists like float container. You cannot constraint the option type to only allow None at some specific types, which is what your initial example seems to be trying to do (when given None, you function returns an integer, so it means that you should only allow None at type int container option).
And here we link back to @octachron’s answer: he showed you how to define your own option-like type where you can put restrictions on the type of None, and with these restrictions your code becomes correct (although as he said, you cannot overload the syntax for optional arguments with custom option types so it’s more cumbersome to use).
If you wanted something a bit less fancy, you could have defined the custom option type like this:
type _ container_option =
| None : int container_option
| Some : 'a container -> 'a container_option
let unbox_default (type t) (c: t container_option): t =
let opt : t container = match c with
| None -> Int 1
| Some c -> c
in
match opt with
| Int i -> i
| String s -> s
| Bool b -> b
Typing for optional arguments is done using the pre-defined option type and constructors, not the option type or Some/None constructors currently in scope, so overriding the constructors and the type still doesn’t allow you to use optional argument syntax.