Subtyping between propositions could be improved, especially when mixing positive and
negative type propositions.
Take the following function.
The subtyping test for the {then} proposition fails because
is not a subtype of
However in the context of the current lexical environment,
combined with the actual then proposition
implies
.
Every {FilterSet} should also carry the {PropEnv} in which it was created. (We should take care that this
environment is substituted properly when we eg. substitute function parameters for de Bruijn indices).
Then we can check to see if the contained environment for the actual proposition set satisfies the
supertype proposition.
Test case:
This test case should pass: let-filter-unscoping-test.
Code review:
Patch:
Very vague, would require something like refinement types which is a huge job.