>         let x = (let y = fun x -> x in ref y, y)
>                  : ('a -> 'a) ref * ('a -> 'a)

Indeed, as Michel Mauny pointed out to me, this expression would have type:

          let x = (let y = fun x -> x in ref y, y)
                   : ('a -> 'a) ref * ('b -> 'b)

thus 'b appearing only in a non-expansive expression could be also
generalized here. (BTW, the context "let x = v in [ ]" is non-expansive
whenever v is)

I meant to create the situation where a type variable appears on both
side of a product, when one side is expansive, this other is not, and the
context of the product is non-expansive. But I can't think of a ``natural''
example of this. The usual trick: 

          let x = (fun (y : 'a) -> ref y, y) (fun x -> x)
                   : ('a -> 'a) ref * ('a -> 'a)

does not work, because the whole expression becomes an application and is
expansive. I can only think of using an artifial typing constraint:

          let x = (let y = fun x -> x in ref (y : 'a), (y : 'a))
                   : ('a -> 'a) ref * ('a -> 'a)

> Here 'a appears both in an outer expansive expansive expression and in a
> non-expansive expressions. Hence it is dangerous can cannot be generalized. 

Funny! it is so difficult to stop type generalization...

        Didier