Ah, no, that was unclear. More accurately, I should have said "it's not entirely obvious to me that it's desirable foo(value:) to ever print "P" [whenever it's called with an argument of concrete type X] under the 'separate modules' circumstance". That said, I think the only option I presented which actually prevents that is #3, which has significant limitations.
Okay, that's what I thought. Thanks for clarifying!
I view these cases as subtly different, though it was somewhat difficult to phrase why. I think it comes down to the fact that for me, dynamic casts/existentials feel like "defining features" of a protocol conformance, by which I mean that when I declare a conformance to a protocol, those are (some of) the meaningful things I wish to do with that conformance.
OTOH, the "defining features" of a class are its properties, methods, initializers etc. When I declare an internal class, I intend for these features to be hidden from other modules. I don't want clients poking my properties, calling my methods, or creating instances of me (unless through a declared inheritance which I know will expose public API).
As the author of File1.swift, if I'm using a feature that describes a declared conformance X: internal P as an "internal conformance," I similarly expect the "defining features" of that conformance to be hidden outside the module. At the very least, I would expect that I, as the author of an internal conformance, am able to control when those features are exposed to clients. I.e., I would want something like what you're doing with ConformanceXToP—without explicitly "exporting" the conformance, it doesn't leave the module.