MLF is a type system that seamlessly merges ML-style implicit but second-class polymorphism with System-F explicit first-class polymorphism. We present xMLF, a Church-style version of MLF with full type information that can easily be maintained during reduction. All parameters of functions are explicitly typed and both type abstraction and type instantiation are explicit. However, type instantiation in xMLF is more general than type application in System-F. We give xMLF a small-step reduction semantics where reduction is allowed in any context and show that reduction is confluent and type-preserving. We also show that both subject reduction and progress hold for weak-reduction strategies, including the call-by-value with the value-restriction. There is a type preserving encoding of MLF into F (which we will not describe), which ensures type soundness for the most general version of MLF.