Universe inconsistencies depend oddly on the stdlib (polyproj)

[JasonGross]

Here is some code that works on HoTT/coq trunk, fails on pose (@isequiv_apD10 H (Lift A)). with polyproj, and fails on exact t' with polyproj when we replace the standard library with the one from HoTT/HoTT.

(* File reduced by coq-bug-finder from 1920 lines to 66 lines. *)

Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.

Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
  : forall x, f x = g x
  := fun x => match h with idpath => idpath end.

Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.

Section local.
  Let type_cast_up_type : Type.
  Proof.
    let U0 := constr:(Type) in
    let U1 := constr:(Type) in
    let unif := constr:(U0 : U1) in
    exact (U0 -> U1).
  Defined.
  Definition Lift : type_cast_up_type
    := fun T => T.
End local.

Lemma Funext_downward_closed `{H : Funext} : Funext.
Proof.
  constructor.
  intros A P.
  Set Printing All.
  Set Printing Universes.
  pose (@isequiv_apD10 H (Lift A)).  (* On coqtop without a -coqlib argument:
Toplevel input, characters 39-45:
Error:
In environment
H : Funext
A : Type (* Top.15 *)
P : forall _ : A, Type (* Top.16 *)
The term "Lift A" has type "Type (* Top.21 *)"
while it is expected to have type "Type (* Top.15 *)"
(Universe inconsistency: Cannot enforce Top.21 <= Top.15 because Top.15
<= Top.20 < Top.21)). *)
  let t := constr:(@isequiv_apD10 H (Lift A) (fun a => Lift (P a))) in
  let t' := (eval compute [Lift] in t) in
  exact t'. (* On coqtop with -coqlib:
Toplevel input, characters 139-141:
Error:
In environment
H : Funext (* Top.40 Top.41 Top.42 *)
A : Type (* Top.45 *)
P : forall _ : A, Type (* Top.44 *)
i := @isequiv_apD10 (* Top.40 Top.41 Top.42 *) H
       (Lift (* Top.52 Top.53 Top.54 *) A)
  : forall
      (P : forall _ : Lift (* Top.52 Top.53 Top.54 *) A, Type (* Top.41 *))
      (f g : forall x : Lift (* Top.52 Top.53 Top.54 *) A, P x),
    @IsEquiv (* Top.40 Top.40 *)
      (@paths (* Top.40 *)
         (forall x : Lift (* Top.52 Top.53 Top.54 *) A, P x) f g)
      (forall x : Lift (* Top.52 Top.53 Top.54 *) A,
       @paths (* Top.41 *) (P x) (f x) (g x))
      (@apD10 (* Top.41 Top.42 Top.40 *) (Lift (* Top.52 Top.53 Top.54 *) A)
         P f g)
The term "@isequiv_apD10 (* Top.40 Top.41 Top.42 *) H A (fun a : A => P a)"
has type
 "forall f g : forall x : A, P x,
  @IsEquiv (* Top.40 Top.40 *) (@paths (* Top.40 *) (forall x : A, P x) f g)
    (forall x : A, @paths (* Top.41 *) (P x) (f x) (g x))
    (@apD10 (* Top.41 Top.42 Top.40 *) A (fun a : A => P a) f g)"
while it is expected to have type
 "forall f g : forall x : A, P x,
  @IsEquiv (* Top.43 Top.43 *) (@paths (* Top.43 *) (forall x : A, P x) f g)
    (forall x : A, @paths (* Top.44 *) (P x) (f x) (g x))
    (@apD10 (* Top.44 Top.45 Top.43 *) A P f g)"
(Universe inconsistency: Cannot enforce Top.41 = Top.44 because Top.44
<= Top.71 < Top.70 <= Top.41)). *)

[JasonGross]

Here is code that used to be accepted, but is no longer, which hopefully explicates the problem. I think it is valid (and useful); do I think incorrectly? (It seems that now you require universes in inductive types to match exactly, whereas before, you required only inequality.)

Set Printing All.
Set Printing Implicit.
Set Printing Universes.
Set Universe Polymorphism.

Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
Arguments idpath {A a} , [A] a.

Notation "x = y" := (@paths _ x y) : type_scope.

Section lift.
  Let lift_type : Type.
  Proof.
    let U0 := constr:(Type) in
    let U1 := constr:(Type) in
    let unif := constr:(U0 : U1) in
    exact (U0 -> U1).
  Defined.

  Definition Lift : lift_type := fun A => A.
End lift.

Goal forall (A : Type) (x y : A), @paths A x y -> @paths (Lift A) x y.
intros A x y p.
compute in *.
exact p.

[JasonGross]

I suspect the dependence on the stdlib was actually a dependence on Set Universe Polymorphism.

[mattam82]

Indeed, equality of the levels is required for consistency in general, so you need to do an eta expansion of the paths value here. It is true that for some inductives like equality, we should be able to not require this, but the details are still unclear. — Matthieu

On 1 avr. 2014, at 22:33, Jason Gross notifications@github.com wrote:

Here is code that used to be accepted, but is no longer, which hopefully explicates the problem. I think it is valid (and useful); do I think incorrectly? (It seems that now you require universes in inductive types to match exactly, whereas before, you required only inequality.)

Set Printing All. Set Printing Implicit. Set Printing Universes. Set Universe Polymorphism.

Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. Arguments idpath {A a} , [A] a.

Notation "x = y" := (@paths _ x y) : type_scope.

Section lift.

Let lift_type : Type.

Proof.

let U0 := constr:(Type) in

let U1 := constr:(Type) in

let unif := constr:(U0 : U1) in

exact (U0 -> U1).

Defined.

Definition Lift : lift_type := fun A => A. End lift.

Goal forall (A : Type) (x y : A), @paths A x y -> @paths (Lift A) x y. intros A x y p. compute in *. exact p. — Reply to this email directly or view it on GitHub.

[JasonGross]

Here is one way to implement this rule: add half-eta-expansion for all inductive types which refreshes universes in the return type to the conversion machinery, and trigger this on universe inconsistency in the appropriate places. That is, if we have p : @paths (* U_i *) A x y, say that p is convertible with

match p in (@paths _ _ y') return (@paths (* U_k *) A x y') with
  | eq_refl => eq_refl
end

where U_k is a fresh universe, constrained only by whatever constraints normally get added to matches.

[mattam82]

I'm thinking this could maybe be handled simply at pretyping time using the existing coercion mechanism. Do you need this "deeper" like in unification? -- Matthieu

On May 2, 2014, at 16:06, Jason Gross notifications@github.com wrote:

Here is one way to implement this rule: add half-eta-expansion for all inductive types which refreshes universes in the return type to the conversion machinery, and trigger this on universe inconsistency in the appropriate places. That is, if we have p : @paths (* U_i *) A x y, say that p is convertible with

match p in (@paths y') return (@paths (* U_k *) A x y') with | eq_refl => eq_refl end where U_k is a fresh universe, constrained only by whatever constraints normally get added to matches.

— Reply to this email directly or view it on GitHub.

[JasonGross]

If you can make this go through at pretyping time, then I think you're good:

Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.

Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
  : forall x, f x = g x
  := fun x => match h with idpath => idpath end.

Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.

Section local.
  Let type_cast_up_type : Type.
  Proof.
    let U0 := constr:(Type) in
    let U1 := constr:(Type) in
    let unif := constr:(U0 : U1) in
    exact (U0 -> U1).
  Defined.
  Definition Lift : type_cast_up_type
    := fun T => T.
End local.

Set Printing All.
Set Printing Universes.

Lemma Funext_downward_closed `{H : Funext} : Funext.
Proof.
  constructor.
  intros A P.
  exact (@isequiv_apD10 H (Lift A) (fun a => Lift (P a))).
Defined.

But I think you need this in unification, because the paths live inside the equiv type, and under lambdas, and then you need to talk about equalities of such paths given equalities of the original ones. But maybe you don't? Do you have an example of how you'd use the coercion mechanism?