> for any x and y, your type annotation does not induce anything about the 
> instantiation of g's variable 'a. The following is perfectly legal:
>
>  g ("hello" : int t) true
>
> The compiler just infers the most general type.

two things :

first

# type 'a t=string;;
type 'a t = string
# let g (x : 'a) (y : 'a t)=();;
val g : 'a -> 'a t -> unit = <fun>
# g 3;;
- : int t -> unit = <fun>

here we should have int t=string='_a t ...

second :

I strongly disaggree with the fact that the compiler infered the most 
general type in this case.

Because I specified it.

when you write (let f=fun (x : 'a) (y : 'a) -> (x,y)), you force the type 
of x 
and y to be equal.
It would be a problem if one could write (f true 3).

J

PS : The behavior with abstract types is the one expected and my example 
in the previous mail was irrelevant (sorry about that).