More troubles with type inference and [Prop]

[JasonGross]

This code fails in HoTT/Coq, but does not if I remove the change (present_obj) or intros lines:

Set Implicit Arguments.

Generalizable All Variables.

Set Asymmetric Patterns.

Polymorphic Record Category (obj : Type) :=
  Build_Category {
      Object :> _ := obj;
      Morphism : obj -> obj -> Type;

      Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
    }.

Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=
  { ObjectOf :> objC -> objD }.

Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := objC) C (objD := objD) D) :=
  { ComponentsOf' :> forall c, D.(Morphism) (F.(ObjectOf) c) (G.(ObjectOf) c);
    Commutes' : forall s d (m : C.(Morphism) s d), ComponentsOf' s = ComponentsOf' s }.

Ltac present_obj from to :=
  repeat match goal with
           | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in *
           | [ |- appcontext[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in *
         end.

Section NaturalTransformationComposition.
  Context `(C : @Category objC).
  Context `(D : @Category objD).
  Context `(E : @Category objE).
  Variables F F' F'' : Functor C D.

  Polymorphic Definition NTComposeT (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F') :
    NaturalTransformation F F''.
    exists (fun c => Compose _ _ _ _ (T' c) (T c)).
    progress present_obj @Morphism @Morphism. (* removing this line makes the error go away *)
    intros. (* removing this line makes the error go away *)
    admit.
  Defined.
End NaturalTransformationComposition.


Polymorphic Definition FunctorCategory objC (C : Category objC) objD (D : Category objD) :
  @Category (Functor C D)
  := @Build_Category (Functor C D)
                     (NaturalTransformation (C := C) (D := D))
                     (NTComposeT (C := C) (D := D)).

Definition Cat0 : Category Empty_set
  := @Build_Category Empty_set
                     (@eq _)
                     (fun x => match x return _ with end).

Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C
  := Build_Functor Cat0 C (fun x => match x with end).

Section Law0.
  Variable objC : Type.
  Variable C : Category objC.

  Set Printing All.
  Set Printing Universes.
  Set Printing Existential Instances.

  Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf : Object (FunctorCategory Cat0 C).
    hnf.
    refine (@FunctorFrom0 _ _).
    (* Toplevel input, characters 23-40:
Error:
In environment
objC : Type (* Top.61069 *)
C : Category (* Top.61069 Top.61071 *) objC
The term
 "@FunctorFrom0 (* Top.61077 Top.61078 *) ?69 (* [objC, C] *)
    ?70 (* [objC, C] *)" has type
 "@Functor (* Set Prop Top.61077 Top.61078 *) Empty_set Cat0
    ?69 (* [objC, C] *) ?70 (* [objC, C] *)"
 while it is expected to have type
 "@Functor (* Set Prop Set Prop *) Empty_set Cat0 objC C".
*)

[mattam82]

This is due to lowering of a universe variable (here 61078) to Prop being forbidden in the current implementation (lines 283-286 of pretyping/evd.ml). Not that typechecking forced objC to be in Set already here (in type constraint @Functor (* Set Prop Set Prop *) Empty_set Cat0 objC C), which you certainly don't want! I have been working on an improved version of inference/unification with universes, generating less universe variables and giving you more precise types that handles this and many more cases better. I'm hoping to have it ready in the next few weeks.

[mattam82]

Fixed in latest version.

[mattam82]

In the current trunk, the present_obj tactic forces C and D to be at the same level in FunctorCategory and this now makes the definition of ExponentialLaw0Functor_Inverse_ObjectOf' fail because objC is not a Set there. So, should I change the semantics of change so that it doesn't allow this conversion? That seems reasonable to me.

[JasonGross]

Why does present_obj force C and D to be at the same level?

Is it possible to see the local universe graph in the middle of a proof?

Also, would it be possible to make it so that definitions don't have constraints like Top.a = Top.b? That is, collapse all equality constraints that refer to universes introduced in that definition?

[mattam82]

By equating all the Morphism instances in the goal it unifies their universe instances. I'll add a command to do that. For the last point, yes, I can improve there,

[JasonGross]

I think my preferred default semantics for change are "introduce fresh universes wherever needed, and equate as needed afterwards". Perhaps change <new type> should not do this, and change ... with ... at n should not refresh universes, either. But I generally use change a with b in * to mean "do so polymorphically".

[JasonGross]

(My general motto being "I shouldn't have to think about universes unless I'm being evil; otherwise, they should just work, as generally as possible, unless making them just work is too slow".)

[mattam82]

The problem is it's impossible to get the behavior you hope for in this case. You're asking all terms that match "Morphism@{i' j'} ?C ?D" to convert to the same term "@Morphism@{i j} C D" right at the call to the tactic, so the instances at applications of Morphism for both objD and objC are converted. [repeat progress present_obj @Morphism @Morphism], without a repeat in present_obj does what you expect.

[JasonGross]

This will still unify universes though, right? For example, if I have Contr_internal showing up in a bunch of places at various universe levels, and I do change Contr_internal with Contr in *, then all of my universes will be unified? I'd prefer change not unify universes when aggregating the instances that it applies to. (I'm fine with having to do repeat change Contr_internal with Contr in * to get all of the instances changed.)

[mattam82]

It will still unify with the first occurrence as you will likely have flexible universes in @f when you write change @f with t.

Le 16 juin 2014 à 15:44, Jason Gross [email protected] a écrit :

This will still unify universes though, right? For example, if I have Contr_internal showing up in a bunch of places at various universe levels, and I do change Contr_internal with Contr in *, then all of my universes will be unified? I'd prefer change not unify universes when aggregating the instances that it applies to. (I'm fine with having to do repeat change Contr_internal with Contr in * to get all of the instances changed.)

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

[JasonGross]

change seems broken in trunk (https://coq.inria.fr/bugs/show_bug.cgi?id=3387):

Goal Type@{i} = Type@{j}.
Proof.
  (* 1 subgoals
, subgoal 1 (ID 3)

  ============================
   Type@{Top.368} = Type@{Top.370}
(dependent evars:) *)
  let x := constr:(Type) in
  let y := constr:(Obj set_cat) in
  unify x y. (* success *)
  let x := constr:(Type) in
  let y := constr:(Obj set_cat) in
  first [ unify x y | fail 2 "no unify" ];
    change x with y. (* Error: Not convertible. *)
  change Type@{i} with (Obj set_cat@{i}).

Here is a file that I want to succeed, as stated:

Set Universe Polymorphism.
Set Printing Universes.
Record Cat := { Obj : Type }.
Definition set_cat := {| Obj := Type |}.

Module Failure.
  Goal Type@{i} = Type@{j}.
  Proof.
    change (Obj set_cat@{i j} = Obj set_cat@{i j}).
    compute.
    Fail let x := match goal with |- ?x = ?y => constr:(x) end in
         let y := match goal with |- ?x = ?y => constr:(y) end in
         let unif := constr:(x : y) in pose unif.
    (* The command has indeed failed with message:
=> Error:
The term "Type@{Top.41}" has type "Type@{Top.41+1}"
while it is expected to have type "Type@{Top.41}". *)
    admit.
  Defined.
End Failure.

Module Success.
  Goal Type@{i} = Type@{j}.
  Proof.
    progress repeat change Type with (Obj set_cat).
    compute.
    let x := match goal with |- ?x = ?y => constr:(x) end in
    let y := match goal with |- ?x = ?y => constr:(y) end in
    let unif := constr:(x : y) in pose unif.
    admit.
  Defined.
End Success.