coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] universe inconsistency on import

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] universe inconsistency on import
Date: Sun, 1 Dec 2019 09:20:57 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vzaliva AT cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-il1-f171.google.com
Ironport-phdr: 9a23:T/qyzhb7aEpBeFgZSbqiEVr/LSx+4OfEezUN459isYplN5qZoMm/bnLW6fgltlLVR4KTs6sC17ON9fm/AidZuc/JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRu7oR/MusQUj4ZuJbs9xgfUrnBVZ+lY2GRkKE6JkR3h/Mmw5plj8ypRu/Il6cFNVLjxcro7Q7JFEjkoKng568L3uxbNSwuP/WYcXX4NkhVUGQjF7Qr1UYn3vyDnq+dywiiaPcnxTbApRTSv6rpgRRH0hCsbMTMy7WfagdFygq1GuhKsvxNww4DWb4+VOvRwfb7Tc80GSmdaRMldSzZMD5mgY4cTDecMO/tToYnnp1sJqBuzHQajC/nyxT9Jg3/9wK413P4lEQHHwgwvBc8FvXPKrNT0LqgSVeG1zLfSwjjYc/xW3Cr95JLWfR88vPGBRLR9etffx0koEgPKlFSQqYr9MjOTzOsNtnaU4/N8WuKokWEotwFxriKzyccrj4nEgJ8exFPc9Shh3oo5Odm1RFR4bNOkCpdcqiCXOopsTs8/QWxkpSA3waAct5GhZigF0pEnygbfa/OZd4iI5QruVOOLLjd5gHJpYbO/hxKv/US5xO3wS8u53EtQoipKldnMsX8N1xjN5cSdVvR9+UKh1S6O1wDV9O5EPVg5mbTHJ5Ml2LI9lZoevV7eEiL3mUj6lrKae0c59uSw7uToeLTmppuSN49ujQH+N7wjmtKlDuslMwgOWnKX+OWm273n/E35Xq9Fg+Y4k6bHq5DaOd4XqbK8Aw9IyIos9QuwDyq+3NQCgXYHNE5FeA6Aj4XxJ17OJ+n4Ae6jjFSojTdk3OvLPqbhA5XINnjMiq3tfbd7605GyQo818pT55xOCuJJHPWmUUjo8dfcExURMgquwu+hBs8u+JkZXDexC6OYNevguFuJ+Otnd/eebYsUpj/VIP04ofPikClqyhcmYaC10M5POziDFfN8LhDBOCu+spI6CW4P+zEGYqnvgVyGXyRUYi/uDb0x/S19A4e7S4rPW9L02eHT7GKABpRTI1t+JBWMHHPvLdvWXv4NbGeTJpYknGVbDP6uTIgu0Rzovwj/meI+crjkvxYAvJem7+BbovXJnEBg/jlpScmRzjPVQg==

Cristian,

That’s very helpful. You suggest:

“If it is indeed failing to enforce [Helix.MSigmaHCOL.Memory.16 < Coq.FSets.FMapAVL.649], then you may get away with enforcing early that the universe for FMap contents is strictly larger than the universe for Memory contents.”

How can I enforce something like this?

I also failed to include the exact error message. Here it is:

Set Printing Universes.
Print Memory.NM_sequence.
Require Import Helix.FSigmaHCOL.ReifyDSHCOL.

Memory.NM_sequence = ...
(* {Helix.MSigmaHCOL.Memory.17 Helix.MSigmaHCOL.Memory.16 Helix.MSigmaHCOL.Memory.10 Helix.MSigmaHCOL.Memory.7 Helix.MSigmaHCOL.Memory.1} |= 
   Coq.Structures.OrderedType.4 <= Helix.MSigmaHCOL.Memory.16
   Set <= Helix.MSigmaHCOL.Memory.16
   Coq.FSets.FMapAVL.649 <= Helix.MSigmaHCOL.Memory.16
   Helix.MSigmaHCOL.Memory.1 <= Coq.FSets.FMapAVL.649
   Helix.MSigmaHCOL.Memory.1 <= Coq.FSets.FMapAVL.651
   Helix.MSigmaHCOL.Memory.17 <= Coq.FSets.FMapAVL.649
   Helix.MSigmaHCOL.Memory.17 <= Coq.FSets.FMapAVL.651
   Helix.MSigmaHCOL.Memory.17 <= Coq.FSets.FMapAVL.659
    *)

Arguments A, m, M are implicit and maximally inserted
Argument scopes are [type_scope function_scope _ _]

Error: Universe inconsistency. Cannot enforce ExtLib.Data.Monads.OptionMonad.2 =
Helix.MSigmaHCOL.Memory.17 because Helix.MSigmaHCOL.Memory.17
<= Helix.DSigmaHCOL.ReifyMSHCOL.10755 < MetaCoq.Template.TemplateMonad.Monad.1
<= ExtLib.Data.Monads.OptionMonad.14 = ExtLib.Data.Monads.OptionMonad.2.

It looks like the problem with OptionMonad.

—
Vadim Zaliva
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: +1(510)220-1060

Re: [Coq-Club] universe inconsistency on import, Vadim Zaliva, 12/01/2019
- Re: [Coq-Club] universe inconsistency on import, Christian Doczkal, 12/01/2019
  - Re: [Coq-Club] universe inconsistency on import, Vadim Zaliva, 12/01/2019
    - Re: [Coq-Club] universe inconsistency on import, Christian Doczkal, 12/02/2019
      - Re: [Coq-Club] universe inconsistency on import, Gaëtan Gilbert, 12/02/2019
        
        Re: [Coq-Club] universe inconsistency on import, Jason Gross, 12/02/2019
        
        Re: [Coq-Club] universe inconsistency on import, Vadim Zaliva, 12/02/2019