teach the unifier how to create new variables on the fly

I am in the process of rebasing the GADT work of Olivier. One thing that is needed is to sometimes create new unification nodes on the fly during unification. For example, maybe you want to unify the locally abstract structure a with some arrow type X -> Y, in a context of GADT equations where a is equal to int -> bool. At this point you want to synthesize new (flexible) nodes for the rigid graph fragment int -> bool, and then continue the unification with X -> Y.

I was proud of having found a minimal way to add this to the interface boundary between Unifier and Generalize, where the conjunction function, which currently takes an equate : ('a -> 'a -> unit) parameter to let users recursively unify the leaves of the current structures, gets a new parameter make : ('a structure -> 'a). This is what is proposed in the present MR. @x-AOBrie then kindly reminded me that he already implemented exactly this as part of !50, and I had just forgotten about it. Clearly we should have merged !50 long ago, but in the meantime getting this small feature in would be a good idea, as it makes my life easier and is also a part of !50.