Interesting, I have no authority on type theory, I had a similar thought also. I do wonder how would inline work with say a complex pattern match it may look a bit too noisy versus the out-of-band look, you make a good point with dx is it possible both can be implemented and one is just syntax sugar of the other etc?
