EDIT: ... or maybe I just misunderstood your example. If MyData is a statically known/defined type, then you can obviously accesss it however you want... but then I fail to see the value of HasSomeProperty returning a Type (given the reasoning below, you'd still have to have some proof object giving you the things you're interested in --- so that you wouldn't have to 'prove' the structure of the data obeys the property again.).
I don't understand how you could possibly write any non-trivial (e.g. just unit-returning) code in the body of "someProcessing" with having some sort of proof object (generated by HasSomeProperty) with which to extract whatever you'd be interested in. As the example is written you'd only have a Type, but I don't see how that's enough.
Can you explain or perhaps give an example of what a "someProcessing" function body might look like?
I don't understand how you could possibly write any non-trivial (e.g. just unit-returning) code in the body of "someProcessing" with having some sort of proof object (generated by HasSomeProperty) with which to extract whatever you'd be interested in. As the example is written you'd only have a Type, but I don't see how that's enough.
Can you explain or perhaps give an example of what a "someProcessing" function body might look like?