Universe problem: AU cannot use telescopes quantified at Iris level
This is a regression from dev.2022-05-06.0.7b9f809f
to dev.2022-05-06.1.1414d84
, by !781 (merged)
The following snippet shows the problem. AU_fail
is accepted in dev.2022-05-06.0.7b9f809f
but not in dev.2022-05-06.1.1414d84
.
I tried putting Unset Universe Minimization ToSet
in bi.lib.atomic
as well as locally, but that didn't help.
Require Import stdpp.coPset.
Require Import iris.bi.telescopes.
Require Import iris.bi.lib.atomic.
Section definition.
Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset).
Definition AU_succeed (TA TB : tele) : Prop :=
⊢ ∀ (α : TA → PROP) (β Φ : TA → TB → PROP),
atomic_update Eo Ei α β Φ.
Fail Definition AU_fail : Prop :=
⊢ ∀ (TA TB : tele) (α : TA → PROP) (β Φ : TA → TB → PROP),
atomic_update Eo Ei α β Φ.
End definition.
This is the error message:
In environment
PROP : bi
H : BiFUpd PROP
TA : tele
TB : tele
Eo, Ei : coPset
TA0 : tele
TB0 : tele
α : TA0 → PROP
β : TA0 → TB0 → PROP
Φ : TA0 → TB0 → PROP
The term "α" has type "forall _ : tele_arg@{tests.62} TA0, bi_car PROP"
while it is expected to have type
"forall _ : tele_arg@{iris.bi.lib.atomic.94} ?TA, bi_car ?PROP5".
Edited by Hai Dang