not-outside-in checksum

[ivoysey]

constructability only says that we have enough type rules. it doesn't say that we've made good on our "not outside in claim". i wonder if there's a metatheorem that would act as a checksum on that. (and therefore would catch stuff like the case rules we missed in sums and @cyrus- found last last week)

[cyrus-]

maybe it's "if you can do an action in the synthetic position at the top level, you should be able to do it anywhere". not true for the current calculus, but aspirational. I think you need funny judgements about "does not analyze" and "does not have matched arrow type" and so on to really get this to work.

[ivoysey]

migrating this to the issue tracker repo.