HoTT does not build with trunk

[JasonGross]

We get

File "./theories/Modalities/Modality.v", line 325, characters 0-33:
Error: Signature components for label hprop_inO do not match:
polymorphic universe instances do not match.

Anybody (@mikeshulman? @mattam82?) want to take a look at this?

[JasonGross]

When printed, we get

  Set Printing Universes.
  Print Modalities.
(*    Parameter hprop_inO :
     Funext ->
     forall (O : Modality@{Var(0) Var(1)}) (T : Type@{Var(2)}),
     IsHProp (In@{Var(0) Var(1) Var(2)} O T).
     (* Top.60
        Top.61
        Top.62 |= Set < Var(1)
                  Set < Var(2)
                  Var(1) < Var(0)
                  Var(1) <= Var(2)
                   *)
*)
  Print hprop_inO. (* hprop_inO =
fun (H : Funext) (O : Modality@{Top.343 Top.344}) (T : Type@{Top.345}) =>
hprop_isequiv@{Top.345 Top.345 Top.349 Top.345 Top.345 Top.345}
  (to@{Top.343 Top.344 Top.345} O T)
     : Funext ->
       forall (O : Modality@{Top.343 Top.344}) (T : Type@{Top.345}),
       IsHProp (In@{Top.343 Top.344 Top.345} O T)
(* Top.343
   Top.344
   Top.345
   Top.349 |= Set < Top.344
              Set < Top.345
              Top.344 < Top.343
              Top.344 <= Top.345
               *)

hprop_inO is universe polymorphic
Argument H is implicit and maximally inserted
Argument scopes are [_ _ type_scope]
 *)

(What's with these Var(*), @mattam82?) So it seems that we acquired an extra floating universe somewhere?

[mikeshulman]

Looks like bug 3797 still isn't fixed. I'll look into the extra universe.

[mikeshulman]

Looks like the extra universes comes from contr_paths_contr: it has two universe parameters but the second one appears totally unused; even with Set Printing All I don't see it anywhere in the term. @mattam82, any idea where that universe is coming from?

[JasonGross]

It has something to do with Instance; if you change Instance to Definition (and strip off | 10000), then it has only one universe.

[mikeshulman]

That sounds like a bug to me; I can't think of any valid reason for that.

[JasonGross]

Bug 4121

[mikeshulman]

The Hint Extern is necessary to reproduce the behavior? That's extremely odd.

[JasonGross]

The Hint Extern is necessary for the definitions to typecheck at all.

[JasonGross]

But, uh, yes, that Hint Extern is needed to reproduce the behavior (see comments on bug thread).

[mikeshulman]

I see that bug 4121 was fixed; can we close this issue?