I respect that, but just to get it written down, here's what I've come up with so far:

All lambda expressions must be lambda-lifted so they're at the top level of some module. (I guess this might count as a lambda-free logical framework.)

Every function type (X -> Y) is annotated as (X -> [C] Y) with the implementation code C of that function's source module. A simple export/import of an X-to-Y function will actually bind an import variable of the type (existscode C. (SatisfiesSignature S C * (X -> [C] Y))), where S is the import signature.

If a module has access to installed implementation code C and it knows SatisfiesSignature S C and SatisfiesSignature S C', then it can conclude C = C'. It can take advantage of this knowledge to get access to fuller knowledge about how an (X -> [C'] Y) function behaves.

---

"I was (and still am) waiting for you to teach them to me :p"