This is why Turing-complete languages are evil and you should use Agda.

Yes in ML you'd have to eta-expand first:

    val id : 'a -> 'a
    fun id x = id x

You can still write x=_|_ in ML, you just have to be subtler about it.