In this talk, we will discuss some preliminary progress (and difficulties) on proving the type soundness of a merge system via semantic typing.