This global switch enables or disables the anti-frame rule.
When the anti-frame rule is enabled, the value restriction must be enabled
as well. Indeed, the combination of hidden state and unrestricted
polymorphism is unsound. This is evident in the fact that it is impossible
to extrude THide out of TTyAbs -- the type of the hidden state might
mention the bound type variable.
As a result, when the anti-frame rule is enabled, the construct TTyAbs is
disabled. The coercion CoDistrib is also disabled, because its soundness
argument relies on the presence of TTyAbs.
It is important to understand that the switch remains abstract, so that all
proofs are carried out simultaneously for *both* values of the switch.
Parameter anti_frame_switch :
bool.
Definition anti_frame_enabled :=
(
match anti_frame_switch with true =>
True |
false =>
False end).
Definition anti_frame_disabled :=
(
match anti_frame_switch with true =>
False |
false =>
True end).
Lemma anti_frame_switch_contradiction:
forall P :
Prop,
anti_frame_enabled ->
anti_frame_disabled ->
P.
Proof.
unfold anti_frame_enabled,
anti_frame_disabled.
destruct anti_frame_switch;
tauto.
Qed.