Note: the reason why you get _weak type variables (which are not polymorphic, just not-inferred-yet) is that the type-checker cannot detect that (z // (fun () -> ...)) is a value: it would have to unfold the call to (//) for this, which it doesn't do in general, and here certainly could not do given that its definition is hidden behind an abstraction boundary.
I would recommend experimenting *without* the module interface and the auxiliary function, with the constructors directly, you would get slightly better types.
# S(S(Z, (fun () -> Int32.zero)), (fun () -> ""));;
- : (int32 -> string -> 'a, 'a) t = S (S (Z, <fun>), <fun>)
Historically we have used module interfaces to implement "phantom types" -- because the type information there is only present in the interface, not in the definition. With GADTs, the type constraints are built into the definition itself, which is precisely what makes them more powerful; no need for an abstract interface on top.
The first part of your question is about understanding how the type-inference work (how variables are manipulated by the type-checker and then "propagated back up"). This sounds like a difficult way to understand GADTs: you want to learn the typing rules *and* the type-inference algorithm at once. But only the first part is necessary to use the feature productively (with a few tips on when to use annotations, which are easy to explain and in fact explained in the manual:
http://caml.inria.fr/pub/docs/manual-ocaml/manual033.html ). So instead of asking: "how did the compiler get this type?", I would ask: "why is this the right type"? I think you could convince yourself that (1) it is a correct type and (2) any other valid type would be a specialization of this type, there is no simpler solution.
The second part: you wrote:
let rec bind : type f r. f -> (f, r) t -> r = fun f -> function
| Z ->
f
| S (t, v) ->
bind (f (v ())) t
Let's focus on the second clause:
| S (t, v) ->
we know that (f : f) holds, and that the pattern-matching is on a value of type (f, r) t, and we must return r.
When pattern-matching on S (t, v), we learn extra type information from the typing rule of S:
| S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t
if r has type (f, r) t, then (t, v) has type ((f, a -> r) t * (unit -> a)) for *some* unknown/existential type a. So within the branch we have
bind : type f r. f -> (f, r) t -> r
f : (f, a -> r) t
v : unit -> a
expected return type: r
f does *not* have a function type here, so your idea of applying (f (v ())) cannot work (v does have a function type, so (v ()) is valid).
The only thing you can do on f is call (bind) recursively (with what arguments?), and then you will get an (a -> r) as result.
Do you see how to write a correct program from there?