`change` seems to break polymorphism, gives a universe inconsistency #36

Open
JasonGross opened this Issue May 6, 2013 · 4 comments

Projects

None yet

2 participants

The following code works in coq 8.4, but not in HoTT/coq:

Set Implicit Arguments.
Set Universe Polymorphism.
Generalizable All Variables.

Record SpecializedCategory (obj : Type) :=
  {
    Object :> _ := obj
  }.

Record > Category :=
  {
    CObject : Type;
    UnderlyingCategory :> @SpecializedCategory CObject
  }.

Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
  {
    ObjectOf :> objC -> objD
  }.

Definition Functor (C D : Category) := SpecializedFunctor C D.

Parameter TerminalCategory : SpecializedCategory unit.

Definition focus A (_ : A) := True.

Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
  assert (Hf : focus ((S tt) = (S tt))) by constructor.
  progress change CObject with (fun C => @Object (CObject C) C) in *;
    simpl in *.
  match type of Hf with
    | focus ?V => exact V
  end.
Defined.

Definition Build_SliceCategory (A : Category) (F : Functor TerminalCategory A) := @Build_SpecializedCategory (CommaCategory_Object F).
Parameter SetCat : @SpecializedCategory Set.

Set Printing Universes.
Check (fun (A : Category) (F : Functor TerminalCategory A) => @Build_SpecializedCategory (CommaCategory_Object F)) SetCat.
(* (fun (A : Category (* Top.68 *))
   (F : Functor (* Set Top.68 *) TerminalCategory A) =>
 {|  |}) SetCat (* Top.68 *)
     : forall
         F : Functor (* Set Top.68 *) TerminalCategory SetCat (* Top.68 *),
       let Object := CommaCategory_Object (* Top.68 Top.69 Top.68 *) F in
       SpecializedCategory (* Top.69 *)
         (CommaCategory_Object (* Top.68 Top.69 Top.68 *) F) *)
Check @Build_SliceCategory SetCat. (* Toplevel input, characters 0-34:
Error: Universe inconsistency (cannot enforce Top.51 <= Set because Set
< Top.51). *)

Here's a slightly smaller version

Set Implicit Arguments.
Set Universe Polymorphism.

Record SpecializedCategory (obj : Type) :=
  {
    Object : _ := obj
  }.

Record > Category :=
  {
    CObject : Type;
    UnderlyingCategory :> @SpecializedCategory CObject
  }.

Parameter TerminalCategory : SpecializedCategory unit.

Definition focus A (_ : A) := True.
Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
                             (objD : Type) (D : SpecializedCategory objD), Prop.
Definition CommaCategory_Object (A : Category) : Type.
  assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
  progress change CObject with (fun C => @Object (CObject C) C) in *;
    simpl in *.
  match type of Hf with
    | focus ?V => exact V
  end.
Defined.

Definition Build_SliceCategory := @CommaCategory_Object.
Parameter SetCat : @SpecializedCategory Set.

Set Printing Universes.
Check @Build_SliceCategory SetCat.

I think what's happening here is that the change picks a single new universe for CObject C to live in when instantiating the universe for @Object, and therefore forces Set to be unified with the universe level of CObject A, which becomes CObject SetCat (which reduces to the type of Set, which is not Set).

Interestingly, I found a case where Definition foo := bar. causes foo baz to create a universe inconsistency, even when bar baz does not:

Set Implicit Arguments.
Set Universe Polymorphism.

Record SpecializedCategory (obj : Type) :=
  {
    Object : _ := obj
  }.

Record > Category :=
  {
    CObject : Type;
    UnderlyingCategory :> @SpecializedCategory CObject
  }.

Parameter TerminalCategory : SpecializedCategory unit.

Definition focus A (_ : A) := True.

Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
                             (objD : Type) (D : SpecializedCategory objD), Prop.
Definition CommaCategory_Object (A : Category) : Type.
  assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
  progress change CObject with (fun C => @Object (CObject C) C) in *;
    simpl in *.
  match type of Hf with
    | focus ?V => exact V
  end.
Defined.

Parameter SetCat : @SpecializedCategory Set.

Set Printing Universes.
Definition Build_SliceCategory := @CommaCategory_Object.
Check @CommaCategory_Object SetCat.
(* CommaCategory_Object (* Top.43 Top.44 Top.43 *) SetCat (* Top.43 *)
     : Type (* Top.44 *) *)
Check @Build_SliceCategory SetCat.
(* Toplevel input, characters 0-34:
Error: Universe inconsistency (cannot enforce Top.36 <= Set because Set
< Top.36). *)
@mattam82 mattam82 added a commit that referenced this issue May 8, 2013
@mattam82 mattam82 Fix [change] forgeting about universes in the right-hand-side (#36) a…
…nd better fix for #35 and #37,

disallowing only Set/Set+1 <= Prop constraints.
3745dba
Member

The question is again what should be the semantics of change p with c in presence of universes, as the pattern p doesn't carry universes it matches all instances. One way to make this work without introducing additional constraints would be to retypecheck c at each occurence of p.

I would be in favor of retypechecking c at each occurance of p.

-Jason
On Jun 23, 2014 11:07 AM, "Matthieu Sozeau" notifications@github.com
wrote:

The question is again what should be the semantics of change p with c in
presence of universes, as the pattern p doesn't carry universes it matches
all instances. One way to make this work without introducing additional
constraints would be to retypecheck c at each occurence of p.


Reply to this email directly or view it on GitHub
#36 (comment).

Or, at least, in refreshing the universes at each occurance.

-Jason
On Jun 23, 2014 11:22 AM, "Jason Gross" jasongross9@gmail.com wrote:

I would be in favor of retypechecking c at each occurance of p.

-Jason
On Jun 23, 2014 11:07 AM, "Matthieu Sozeau" notifications@github.com
wrote:

The question is again what should be the semantics of change p with c in
presence of universes, as the pattern p doesn't carry universes it matches
all instances. One way to make this work without introducing additional
constraints would be to retypecheck c at each occurence of p.


Reply to this email directly or view it on GitHub
#36 (comment).

@JasonGross JasonGross added a commit to CategoricalData/catdb that referenced this issue Jan 28, 2015
@JasonGross JasonGross Work around one last bug in HoTT/coq
This is HoTT/coq#36 and
HoTT/coq#45.

Now, everything compiles with HoTT/coq!!!
a4c4c2d
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment