Universe minimization failure during typeclass search

[Alizter]

Description of the problem

We noticed the following in the HoTT library in HoTT/Coq-HoTT#1153.

The following code fails when compiling with -indices-matter:

Set Universe Polymorphism.
Local Set Typeclasses Strict Resolution.
Local Unset Elimination Schemes.
Global Set Keyed Unification.
Global Unset Strict Universe Declaration.
Global Unset Universe Minimization ToSet.
Global Set Default Goal Selector "!".
Global Set Printing Primitive Projection Parameters.

(** Relations *)

Definition Relation (A : Type) := A -> A -> Type.

Class Symmetric {A} (R : Relation A) :=
  symmetry : forall x y, R x y -> R y x.

Arguments symmetry {A R _} / _ _ _.

Ltac symmetry :=
  let R := match goal with |- ?R ?x ?y => constr:(R) end in
  let x := match goal with |- ?R ?x ?y => constr:(x) end in
  let y := match goal with |- ?R ?x ?y => constr:(y) end in
  let pre_proof_term_head := constr:(@symmetry _ R _) in
  let proof_term_head := (eval cbn in pre_proof_term_head) in
  refine (proof_term_head y x _); change (R y x).

(** Paths *)

Cumulative Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.

Arguments idpath {A a} , [A] a.

Scheme paths_ind := Induction for paths Sort Type.
Arguments paths_ind [A] a P f y p.
Scheme paths_rec := Minimality for paths Sort Type.
Arguments paths_rec [A] a P f y p.

Register idpath as core.identity.refl.

(* See comment above about the tactic [induction]. *)
Definition paths_rect := paths_ind.

Register paths_rect as core.identity.ind.

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

Notation "1" := idpath.

Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
  := match p with idpath => idpath end.

(** Equivalences *)

Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
  forall x : A, r (s x) = x.

Global Arguments Sect {A B}%type_scope / (s r)%function_scope.

(** A typeclass that includes the data making [f] into an adjoint equivalence. *)
Cumulative Class IsEquiv {A B : Type} (f : A -> B) := {
  equiv_inv : B -> A ;
  eisretr : Sect equiv_inv f;
  eissect : Sect f equiv_inv;
  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
}.

Arguments eisretr {A B}%type_scope f%function_scope {_} _.
Arguments eissect {A B}%type_scope f%function_scope {_} _.
Arguments eisadj {A B}%type_scope f%function_scope {_} _.
Arguments IsEquiv {A B}%type_scope f%function_scope.

Cumulative Record Equiv A B := {
  equiv_fun : A -> B ;
  equiv_isequiv : IsEquiv equiv_fun
}.

Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.
Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.

(** The inverse of an equivalence is an equivalence. *)
Section EquivInverse.

  Context {A B : Type} (f : A -> B) {feq : IsEquiv f}.

  Theorem other_adj (b : B) : eissect f (f^-1 b) = ap f^-1 (eisretr f b).
  Proof.
  Admitted.

  Global Instance isequiv_inverse : IsEquiv f^-1 | 10000
    := Build_IsEquiv B A f^-1 f (eissect f) (eisretr f) other_adj.
End EquivInverse.

Hint Extern 0 (IsEquiv _^-1) => apply @isequiv_inverse : typeclass_instances.

Coercion equiv_fun : Equiv >-> Funclass.

Global Existing Instance equiv_isequiv.

Theorem equiv_inverse {A B : Type} : (A <~> B) -> (B <~> A).
Proof.
  intro e.
  exists (e^-1).
  apply isequiv_inverse.
Defined.

Notation "e ^-1" := (@equiv_inverse _ _ e).

Global Instance symmetric_equiv : Symmetric Equiv | 0 := @equiv_inverse.


(** Bug *)

Context {A B : Type}.

Typeclasses eauto := debug.

Goal (A <~> B) <~> (A = B).
Proof.
  symmetry.
Abort.
(** Works *)


Definition foo
(*   {A B : Type} *)
  : A <~> B <~> A = B.
Proof.
  symmetry.
Abort.
(** Works
1: looking for (Symmetric Equiv) without backtracking
1.1: exact symmetric_equiv on (Symmetric Equiv), 0 subgoal(s)
*)


Definition foo
  {A B : Type}
  : A <~> B <~> A = B.
Proof.
  symmetry.
Abort.

(** Fails

Cannot infer this placeholder of type "Symmetric (fun A B : Type => A <~> B)" (no
type class instance found) in environment:
A : Type
B : Type
1: looking for (Symmetric (fun A B : Type => A <~> B)) without backtracking
1: no match for (Symmetric (fun A B : Type => A <~> B)), 0 possibilities
1: looking for (Symmetric (fun A B : Type => A <~> B)) without backtracking
1: no match for (Symmetric (fun A B : Type => A <~> B)), 0 possibilities


*)

Jason observed the following:
The thing you are missing is -indices-matter. If I add

Set Printing Universes.
Print paths.
Print Equiv.
Print IsEquiv.

and put this all in bar.v then with coqc -q bar.v I get

Inductive
paths@{bar.9 bar.10} (A : Type@{bar.9}) (a : A) : A -> Type@{bar.10} :=
    idpath : a = a
(* *bar.9 *bar.10 |=  *)

For paths: Argument A is implicit and maximally inserted
For idpath, when applied to no arguments:
  Arguments A, a are implicit and maximally inserted
For idpath, when applied to 1 argument:
  Argument A is implicit
For paths: Argument scopes are [type_scope _ _]
For idpath: Argument scopes are [type_scope _]
Record Equiv (A : Type@{bar.51}) (B : Type@{bar.52})
  : Type@{max(bar.51,bar.52,bar.55,bar.56,bar.57)} := Build_Equiv
  { equiv_fun : A -> B;
    equiv_isequiv : IsEquiv@{bar.51 bar.52 bar.55 bar.56 bar.57} equiv_fun }
(* *bar.51 *bar.52 *bar.55 *bar.56 *bar.57 |=  *)

For Equiv: Argument scopes are [type_scope type_scope]
For Build_Equiv: Argument scopes are [type_scope type_scope function_scope _]
Record IsEquiv (A : Type@{bar.33}) (B : Type@{bar.34})
(f : A -> B) : Type@{max(bar.33,bar.34,bar.38,bar.43,bar.46)}
  := Build_IsEquiv
  { equiv_inv : B -> A;
    eisretr : Sect@{bar.34 bar.33 bar.38} equiv_inv f;
    eissect : Sect@{bar.33 bar.34 bar.46} f equiv_inv;
    eisadj : forall x : A,
             eisretr (f x) = ap@{bar.33 bar.34 bar.46 bar.38} f (eissect x) }
(* *bar.33 *bar.34 *bar.38 *bar.43 *bar.46 |=  *)

For IsEquiv: Arguments A, B are implicit and maximally inserted
For IsEquiv: Argument scopes are [type_scope type_scope function_scope]
For Build_IsEquiv: Argument scopes are [type_scope type_scope function_scope
                     function_scope _ _ function_scope]

and no error at the bottom, while with coqc -q -indices-matter bar.v I get

Inductive paths@{bar.9} (A : Type@{bar.9}) (a : A) : A -> Type@{bar.9} :=
    idpath : a = a
(* *bar.9 |=  *)

For paths: Argument A is implicit and maximally inserted
For idpath, when applied to no arguments:
  Arguments A, a are implicit and maximally inserted
For idpath, when applied to 1 argument:
  Argument A is implicit
For paths: Argument scopes are [type_scope _ _]
For idpath: Argument scopes are [type_scope _]
Record Equiv (A : Type@{bar.39}) (B : Type@{bar.40})
  : Type@{max(bar.39,bar.40)} := Build_Equiv
  { equiv_fun : A -> B;  equiv_isequiv : IsEquiv@{bar.39 bar.40} equiv_fun }
(* *bar.39 *bar.40 |=  *)

For Equiv: Argument scopes are [type_scope type_scope]
For Build_Equiv: Argument scopes are [type_scope type_scope function_scope _]
Record IsEquiv (A : Type@{bar.26}) (B : Type@{bar.27})
(f : A -> B) : Type@{max(bar.26,bar.27)} := Build_IsEquiv
  { equiv_inv : B -> A;
    eisretr : Sect@{bar.27 bar.26} equiv_inv f;
    eissect : Sect@{bar.26 bar.27} f equiv_inv;
    eisadj : forall x : A, eisretr (f x) = ap@{bar.26 bar.27} f (eissect x) }
(* *bar.26 *bar.27 |=  *)

For IsEquiv: Arguments A, B are implicit and maximally inserted
For IsEquiv: Argument scopes are [type_scope type_scope function_scope]
For Build_IsEquiv: Argument scopes are [type_scope type_scope function_scope
                     function_scope _ _ function_scope]

Coq Version

The Coq Proof Assistant, version 8.11+alpha (November 2019)
compiled on Nov 21 2019 23:35:31 with OCaml 4.05.0

[Alizter]

Here is a more minimized version of this bug, doesn't seem to have anything to do with indices-matter specifically, just the number of universe variables that gives.

Set Universe Polymorphism.

(** Relations *)

Definition Relation (A : Type) := A -> A -> Type.

Class Symmetric {A} (R : Relation A) :=
  symmetry : forall x y, R x y -> R y x.

(** Paths *)

Axiom paths_indmat@{u} : forall {A : Type@{u}}, A -> A -> Type@{u}.
Axiom paths@{u v} : forall {A : Type@{u}}, A -> A -> Type@{v}. 

Axiom Equiv@{u v} : Type@{u} -> Type@{v} -> Type@{max(u,v)}.

Global Instance symmetric_equiv : Symmetric Equiv | 0. Proof. Admitted.

(** Bug *)

Set Typeclasses Debug.

Axiom A : Type.
Axiom B : Type.

(** Indices don't matter *)

Goal Equiv A (paths A B).
Proof.
(*     symmetry. *)
  let R := match goal with |- ?R ?x ?y => constr:(R) end in
  let x := match goal with |- ?R ?x ?y => constr:(x) end in
  let y := match goal with |- ?R ?x ?y => constr:(y) end in
  let t := constr:(@symmetry _ R _) in
  let t' := (eval cbn in t) in
  refine (t' y x _); change (R y x).
Abort.

Definition foo {X Y : Type}
  : Equiv X (paths X Y).
Proof.
(*   symmetry. *)
  let R := match goal with |- ?R ?x ?y => constr:(R) end in
  let x := match goal with |- ?R ?x ?y => constr:(x) end in
  let y := match goal with |- ?R ?x ?y => constr:(y) end in
  let t := constr:(@symmetry _ R _) in
  let t' := (eval cbn in t) in
  refine (t' y x _); change (R y x).
Abort.

(** Indices do matter *)


Goal Equiv A (paths_indmat A B).
Proof.
(*     symmetry. *)
  let R := match goal with |- ?R ?x ?y => constr:(R) end in
  let x := match goal with |- ?R ?x ?y => constr:(x) end in
  let y := match goal with |- ?R ?x ?y => constr:(y) end in
  let t := constr:(@symmetry _ R _) in
  let t' := (eval cbn in t) in
  refine (t' y x _); change (R y x).
Abort.

Definition foo {X Y : Type}
  : Equiv X (paths_indmat X Y).
Proof.
(*   symmetry. *)
  let R := match goal with |- ?R ?x ?y => constr:(R) end in
  let x := match goal with |- ?R ?x ?y => constr:(x) end in
  let y := match goal with |- ?R ?x ?y => constr:(y) end in
  let t := constr:(@symmetry _ R _) in
  let t' := (eval cbn in t) in
  refine (t' y x _); change (R y x).
Abort.

[Alizter]

Hmm but after minimizing this a bit more, it seems that it is really an issue of design then a bug. Having Equiv@{u v} : Type@{u} -> Type@{v} -> Type@{max(u,v)} might seem like a good idea, but makes little sense in general since you really want to lift the arguments before comparing them.

[SkySkimmer]

Hmm but after minimizing this a bit more, it seems that it is really an issue of design then a bug. Having Equiv@{u v} : Type@{u} -> Type@{v} -> Type@{max(u,v)} might seem like a good idea, but makes little sense in general since you really want to lift the arguments before comparing them.

What's the failure exactly?

[Alizter]

The Symmetric class forces both universes in Equiv@{u v} : Type@{u} -> Type@{v} -> Type@{max(u,v)} to be equal, therefore the symmetry instances can't be applied to a goal Equiv A B where A and B are different universes.

[SkySkimmer]

Why can't the univs be unified?

[Alizter]

In general they can, but in this example there was a constraint causing one to be larger than the other. A = B lives in a strictly larger universe than A or B since the path type is in the universe of A (or B).