I think I've proven it, now. It required tweaking the typechecking algorithm. I was sitting in Sam's alternating between trying to find a counterexample, trying to prove it, and taking bites of the sandwich. I paused for bit to think about soundness, and realized that for it I only needed the types of an irrelevant function and its argument to match up in the promoted context, because I can type-convert to the `good' type in that context, and then fall back down into the irrelevant typing judgment. So I tried proving completeness for the weaker assumption that the types are equal in the stronger context (whee, contravariance) and succeeded! Assuming I didn't fuck anything up, anyway. I should ask Frank to proofread my, uh proof, probably.
...make lemma-nade.
I think I've proven it, now. It required tweaking the typechecking algorithm. I was sitting in Sam's alternating between trying to find a counterexample, trying to prove it, and taking bites of the sandwich. I paused for bit to think about soundness, and realized that for it I only needed the types of an irrelevant function and its argument to match up in the promoted context, because I can type-convert to the `good' type in that context, and then fall back down into the irrelevant typing judgment. So I tried proving completeness for the weaker assumption that the types are equal in the stronger context (whee, contravariance) and succeeded! Assuming I didn't fuck anything up, anyway. I should ask Frank to proofread my, uh proof, probably.
- Post a new comment
- 0 comments
- Post a new comment
- 0 comments
