coq
coq copied to clipboard
HoTT
`change` seems to break polymorphism, gives a universe inconsistency
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). *)
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" [email protected] 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 https://github.com/HoTT/coq/issues/36#issuecomment-46826353.
Or, at least, in refreshing the universes at each occurance.
-Jason On Jun 23, 2014 11:22 AM, "Jason Gross" [email protected] wrote:
I would be in favor of retypechecking c at each occurance of p.
-Jason On Jun 23, 2014 11:07 AM, "Matthieu Sozeau" [email protected] 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 https://github.com/HoTT/coq/issues/36#issuecomment-46826353.