Interesting post will spend a little time reading it late,in the meantime a quick Q, this

D = P(x,y) ← Q(x,z) % z is not shared with head(D)

throws me a bit, isn't it equivalent (as z is unused) to

D = P(x,y) ← Q(x)

which makes me wonder what y is doing. Would that leave y unbound, and if so is that why it's disallowed?

TIA