The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Thanks for all the advice. Let me try to make this little more concrete. I am working with FMaps indexed by natural numbers,
instantiated like this:

Module NM := FMapAVL.Make(Nat_as_OT).

I’ve traced the problem of universe inconsistency to the following function (using ExlLib):

Definition NM_sequence
           {A:Type}
           {m} {M:Monad m}
           (mv: NM.t (m A)): m (NM.t A)
  := NM.fold
       (fun k v acc =>
          v' <- v ;;
             acc' <- acc ;;
             ret (NM.add k v' acc'))
       mv
       (ret (@NM.empty A)).

The constraints for this function, reported by Print are:

{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

As a workaround I’ve replaced it with a specialized version, getting rid of monadic stuff:

Definition option_NM_sequence  {A:Type}  (mv: NM.t (option A)): option (NM.t A)
  := NM.fold
       (fun k v acc =>
          match v with
          | Some v' =>
            match acc with
            | Some acc' => Some (NM.add k v' acc')
            | None => None
            end
          | None => None
          end)
       mv
       (Some (@NM.empty A)).

This specialized version does not trigger the universe inconsistency error. The Universe constraints
for it are:

{Helix.FSigmaHCOL.ReifyDSHCOL.4} |= Coq.Structures.OrderedType.4 <= Coq.FSets.FMapAVL.659
Coq.Structures.OrderedType.4 <= Coq.Init.Datatypes.13
Helix.FSigmaHCOL.ReifyDSHCOL.4 <= Coq.FSets.FMapAVL.649
Helix.FSigmaHCOL.ReifyDSHCOL.4 <= Coq.FSets.FMapAVL.651
Helix.FSigmaHCOL.ReifyDSHCOL.4 <= Coq.Init.Datatypes.13
Set <= Coq.FSets.FMapAVL.659
Set <= Coq.Init.Datatypes.13
Coq.FSets.FMapAVL.649 <= Coq.FSets.FMapAVL.659
Coq.FSets.FMapAVL.649 <= Coq.Init.Datatypes.13

What can one deduce from these constraints and how I can proceed to resolve this?
Thanks!

Vadim

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