GitLab

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".