Oleg writes: > the real type of h is > forall t. t -> (function-of-t) > > The real type of h is not totally polymorphic : it is dependent! Ummm... that doesn't look like a dependent type to me, it looks like a functional dependency. A dependent type would be forall t. x::t -> (function-of-x) Perhaps it's not (quite) so surprising? --KW 8-)