Complete session types inference with progress guarantees for ML