typeclass resolution bug

[Alizter]

Here is a strange bug that was noticed in #1146. It seems that typeclass resolution can fail when things are eta-expanded.

Require Import Basics Types.

Context {G H : Type}.

Typeclasses eauto := debug.

Goal G <~> H <~> G = H.
Proof.
  symmetry.
Abort.

(** Works *)

Definition foo
  : G <~> H <~> G = H.
Proof.
  symmetry.
Abort.

(** Works *)

Definition foo {U : Univalence}
  : G <~> H <~> G = H.
Proof.
  symmetry.
Abort.

(** Works 
1: looking for (Symmetric Equiv) without backtracking
1.1: exact symmetric_equiv on (Symmetric Equiv), 0 subgoal(s)
*)

Definition foo {U : Univalence} {G : Type}
  : G <~> H <~> G = H.
Proof.
  symmetry.
Abort.

(** Works
1: looking for (Symmetric Equiv) without backtracking
1.1: exact symmetric_equiv on (Symmetric Equiv), 0 subgoal(s)
*)

Definition foo {U : Univalence} {G H : Type}
  : G <~> H <~> G = H.
Proof.
  symmetry.
Abort.

(* Doesn't work?!
Cannot infer this placeholder of type "Symmetric (fun A B : Type => A <~> B)" (no
type class instance found) in environment:
U : Univalence
G : Type
H : Type
1: looking for (Symmetric Equiv) without backtracking
1.1: exact symmetric_equiv on (Symmetric Equiv), 0 subgoal(s)
1: looking for (Symmetric (fun A B : Type => A <~> B)) without backtracking
1: no match for (Symmetric (fun A B : Type => A <~> B)), 3 possibilities
1: looking for (Symmetric (fun A B : Type => A <~> B)) without backtracking
1: no match for (Symmetric (fun A B : Type => A <~> B)), 3 possibilities
*)

[mikeshulman]

Bizarre!

[JasonGross]

Can you extract this into something that doesn't depend on HoTT, and then report it as a bug in Coq?

[Alizter]

@JasonGross I was trying to extract the code into something that runs in regular coq. What's weird is that it now runs.

Observe that the following works in regular coq, but doesn't work in our version. I am not sure of the specifics here.

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

*)

[JasonGross]

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]

I'm not sure why this changes things, but it at least explains the difference between our version and standard coqc, and should allow you to report this as a bug in Coq.

[Alizter]

@JasonGross Thanks for working that out!

[mikeshulman]

Since this has been reported as a bug in Coq, I don't think we need to keep it open here.

[Alizter]

This doesn't seem to be a bug in coq after returning to it. The Symmetric class forces both universe instances of Equiv@{u v} : Type@{u} -> Type@{v} -> Type@{max(u,v)} to be equal. However that means we cannot use symmetry on a goal like Equiv A B where A and B are of different universes. The solution to this is to change equiv to only have one universe variable Equiv@{u v} : Type@{u} -> Type@{u} -> Type@{u}.

@mikeshulman What do you think? When defining Equiv does it make sense to have differing universes or is it better to compare them in the same one?

[jdchristensen]

It's definitely important to be able to talk about equivalences between types in different universes. E.g. the formalization of one of my recent preprints has

Record IsSmall@{i j | } (X : Type@{j}) :=
  { smalltype : Type@{i} ;
    equiv_smalltype : smalltype <~> X
  }.

That said, maybe universe cumulativity would make this still work with Equiv having only one universe variable? Not sure.

[jdchristensen]

No, it doesn't work, since I don't want to assume i <= j or j <= i, so I would need a third universe variable u with i <= u and j <= u. In my development, I had to work really hard to keep the universe variables to a minimum, so I wouldn't want to require a third one here. (I wish coq allowed max(i,j) to be given as a universe argument.)

[jdchristensen]

I also don't see what this has to do with the error message in the initial comment in this issue. Why are the universes the same in some cases and not in others? Why doesn't using symmetry just add universe constraints in all cases?

If you want to avoid universe constraints, I think you just have to avoid using symmetry. apply equiv_inverse works, without imposing constraints.

[mikeshulman]

I wonder if we could define our symmetry tactic to sneakily notice whether it's being applied to an Equiv goal, in which case it applies equiv_inverse, and only otherwise recourses to the Symmetric typeclass. And whether that would be a good idea or too clever by half.

[mikeshulman]

I don't know about the OP, but it could be that introducing G and H in a Context or as hypotheses leads to different universe constraints. Stepping through it with Show Universes I definitely see different behavior going on, but I don't have time to puzzle out exactly what or why.

[mikeshulman]

Presumably transitivity also has this problem...

[Alizter]

Here is a more minimized version of the issue:

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.

Have a look at the type of paths. With indices matter there is one universe variable, without there are two. We are trying to unify Equiv@{u v} (A <~> B) (A = B) with a symmetry instance, but that path type forces the second argument of Equiv to necessarily be larger (not apparent when indices don't matter). The symmetry instance only allows for relations on a single type, i.e. the common universe of A and B which is strictly smaller than the universe of A = B.

[Alizter]

I kind of like Mike's idea of making symmetry clever. I have some ideas how we could make this happen, I'll try experimenting. It has annoyed me for some time that these tactics mess up the universe level.

[jdchristensen]

Since one can just type apply equiv_inverse, which is easy and clear, I don't think it's a good idea to make symmetry clever. Then a reader would have to go find that in the library to see what it does.