Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 153
    • Issues 153
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 8
    • Merge requests 8
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #461
Closed
Open
Created May 15, 2022 by Hai Dang@haidangOwner

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 May 15, 2022 by Hai Dang
Assignee
Assign to
Time tracking