From 1e2fa3a3a0ce3c5be93287ee034fc1fddc82d733 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 20 Jun 2014 14:15:02 +0200 Subject: Bug 27 closed now that universe contexts can be refined during the proof, here instantiating a flexible level with Set. --- test-suite/bugs/closed/HoTT_coq_027.v | 94 +++++++++++++++++++++++++++++++++++ test-suite/bugs/opened/HoTT_coq_027.v | 94 ----------------------------------- 2 files changed, 94 insertions(+), 94 deletions(-) create mode 100644 test-suite/bugs/closed/HoTT_coq_027.v delete mode 100644 test-suite/bugs/opened/HoTT_coq_027.v diff --git a/test-suite/bugs/closed/HoTT_coq_027.v b/test-suite/bugs/closed/HoTT_coq_027.v new file mode 100644 index 0000000000..27834cc486 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_027.v @@ -0,0 +1,94 @@ +Set Implicit Arguments. +Generalizable All Variables. +Set Asymmetric Patterns. +Set Universe Polymorphism. + +Record Category (obj : Type) := { Morphism : obj -> obj -> Type }. + +Record Functor `(C : Category objC) `(D : Category objD) := + { ObjectOf :> objC -> objD; + MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d) }. + +Definition TypeCat : @Category Type := @Build_Category Type (fun s d => s -> d). +Definition SetCat : @Category Set := @Build_Category Set (fun s d => s -> d). + +Definition FunctorToSet `(C : @Category objC) := Functor C SetCat. +Definition FunctorToType `(C : @Category objC) := Functor C TypeCat. + +(* Removing the following line, as well as the [Definition] and [Identity Coercion] immediately following it, makes the file go through *) +Identity Coercion FunctorToType_Id : FunctorToType >-> Functor. + +Set Printing Universes. +Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C) +: FunctorToType C. + refine (@Build_Functor _ C _ TypeCat + (fun x => F.(ObjectOf) x) + (fun s d m => F.(MorphismOf) _ _ m)). +(* ??? Toplevel input, characters 8-148: +Error: +In environment +objC : Type{Top.100} +C : Category@{Top.100 Top.101} objC +F : FunctorToSet@{Top.100 Top.101 Top.99} C +The term + "{| + ObjectOf := fun x : objC => F x; + MorphismOf := fun (s d : objC) (m : Morphism@{Top.100 Top.101} C s d) => + MorphismOf@{Top.100 Top.101 Top.99 Set} F s d m |}" has type + "Functor@{Top.104 Top.105 Top.106 Top.107} C TypeCat@{Top.108 Top.109 + Top.110}" while it is expected to have type + "FunctorToType@{Top.100 Top.101 Top.102 Top.103} C" +(Universe inconsistency: Cannot enforce Set = Top.103)). + *) +Defined. (* Toplevel input, characters 0-8: +Error: +The term + "fun (objC : Type) (C : Category objC) (F : FunctorToSet C) => + {| + ObjectOf := fun x : objC => F x; + MorphismOf := fun (s d : objC) (m : Morphism C s d) => MorphismOf F s d m |}" +has type + "forall (objC : Type) (C : Category objC), + FunctorToSet C -> Functor C TypeCat" while it is expected to have type + "forall (objC : Type) (C : Category objC), FunctorToSet C -> FunctorToType C". + *) + +Coercion FunctorTo_Set2Type : FunctorToSet >-> FunctorToType. + +Record GrothendieckPair `(C : @Category objC) (F : Functor C TypeCat) := + { GrothendieckC : objC; + GrothendieckX : F GrothendieckC }. + +Record SetGrothendieckPair `(C : @Category objC) (F' : Functor C SetCat) := + { SetGrothendieckC : objC; + SetGrothendieckX : F' SetGrothendieckC }. + +Section SetGrothendieckCoercion. + Context `(C : @Category objC). + Variable F : Functor C SetCat. + Let F' := (F : FunctorToSet _) : FunctorToType _. (* The command has indeed failed with message: +=> Anomaly: apply_coercion_args: mismatch between arguments and coercion. +Please report. *) + + Set Printing Universes. + Definition SetGrothendieck2Grothendieck (G : SetGrothendieckPair F) : GrothendieckPair F' + := {| GrothendieckC := G.(SetGrothendieckC); GrothendieckX := G.(SetGrothendieckX) : F' _ |}. + (* Toplevel input, characters 0-187: +Error: Illegal application: +The term "ObjectOf (* Top.8375 Top.8376 Top.8379 Set *)" of type + "forall (objC : Type (* Top.8375 *)) + (C : Category (* Top.8375 Top.8376 *) objC) (objD : Type (* Top.8379 *)) + (D : Category (* Top.8379 Set *) objD), + Functor (* Top.8375 Top.8376 Top.8379 Set *) C D -> objC -> objD" +cannot be applied to the terms + "objC" : "Type (* Top.8375 *)" + "C" : "Category (* Top.8375 Top.8376 *) objC" + "Type (* Set *)" : "Type (* Set+1 *)" + "TypeCat (* Top.8379 Set *)" : "Category (* Top.8379 Set *) Set" + "F'" : "FunctorToType (* Top.8375 Top.8376 Top.8379 Set *) C" + "SetGrothendieckC (* Top.8375 Top.8376 Top.8379 *) G" : "objC" +The 5th term has type "FunctorToType (* Top.8375 Top.8376 Top.8379 Set *) C" +which should be coercible to + "Functor (* Top.8375 Top.8376 Top.8379 Set *) C TypeCat (* Top.8379 Set *)". + *) +End SetGrothendieckCoercion. diff --git a/test-suite/bugs/opened/HoTT_coq_027.v b/test-suite/bugs/opened/HoTT_coq_027.v deleted file mode 100644 index 7f283237a1..0000000000 --- a/test-suite/bugs/opened/HoTT_coq_027.v +++ /dev/null @@ -1,94 +0,0 @@ -Set Implicit Arguments. -Generalizable All Variables. -Set Asymmetric Patterns. -Set Universe Polymorphism. - -Record Category (obj : Type) := { Morphism : obj -> obj -> Type }. - -Record Functor `(C : Category objC) `(D : Category objD) := - { ObjectOf :> objC -> objD; - MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d) }. - -Definition TypeCat : @Category Type := @Build_Category Type (fun s d => s -> d). -Definition SetCat : @Category Set := @Build_Category Set (fun s d => s -> d). - -Definition FunctorToSet `(C : @Category objC) := Functor C SetCat. -Definition FunctorToType `(C : @Category objC) := Functor C TypeCat. - -(* Removing the following line, as well as the [Definition] and [Identity Coercion] immediately following it, makes the file go through *) -Identity Coercion FunctorToType_Id : FunctorToType >-> Functor. - -Set Printing Universes. -Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C) -: FunctorToType@{Type Type Type Set} C. - refine (@Build_Functor _ C _ TypeCat - (fun x => F.(ObjectOf) x) - (fun s d m => F.(MorphismOf) _ _ m)). -(* ??? Toplevel input, characters 8-148: -Error: -In environment -objC : Type{Top.100} -C : Category@{Top.100 Top.101} objC -F : FunctorToSet@{Top.100 Top.101 Top.99} C -The term - "{| - ObjectOf := fun x : objC => F x; - MorphismOf := fun (s d : objC) (m : Morphism@{Top.100 Top.101} C s d) => - MorphismOf@{Top.100 Top.101 Top.99 Set} F s d m |}" has type - "Functor@{Top.104 Top.105 Top.106 Top.107} C TypeCat@{Top.108 Top.109 - Top.110}" while it is expected to have type - "FunctorToType@{Top.100 Top.101 Top.102 Top.103} C" -(Universe inconsistency: Cannot enforce Set = Top.103)). - *) -Defined. (* Toplevel input, characters 0-8: -Error: -The term - "fun (objC : Type) (C : Category objC) (F : FunctorToSet C) => - {| - ObjectOf := fun x : objC => F x; - MorphismOf := fun (s d : objC) (m : Morphism C s d) => MorphismOf F s d m |}" -has type - "forall (objC : Type) (C : Category objC), - FunctorToSet C -> Functor C TypeCat" while it is expected to have type - "forall (objC : Type) (C : Category objC), FunctorToSet C -> FunctorToType C". - *) - -Coercion FunctorTo_Set2Type : FunctorToSet >-> FunctorToType. - -Record GrothendieckPair `(C : @Category objC) (F : Functor C TypeCat) := - { GrothendieckC : objC; - GrothendieckX : F GrothendieckC }. - -Record SetGrothendieckPair `(C : @Category objC) (F' : Functor C SetCat) := - { SetGrothendieckC : objC; - SetGrothendieckX : F' SetGrothendieckC }. - -Section SetGrothendieckCoercion. - Context `(C : @Category objC). - Variable F : Functor C SetCat. - Let F' := (F : FunctorToSet _) : FunctorToType _. (* The command has indeed failed with message: -=> Anomaly: apply_coercion_args: mismatch between arguments and coercion. -Please report. *) - - Set Printing Universes. - Definition SetGrothendieck2Grothendieck (G : SetGrothendieckPair F) : GrothendieckPair F' - := {| GrothendieckC := G.(SetGrothendieckC); GrothendieckX := G.(SetGrothendieckX) : F' _ |}. - (* Toplevel input, characters 0-187: -Error: Illegal application: -The term "ObjectOf (* Top.8375 Top.8376 Top.8379 Set *)" of type - "forall (objC : Type (* Top.8375 *)) - (C : Category (* Top.8375 Top.8376 *) objC) (objD : Type (* Top.8379 *)) - (D : Category (* Top.8379 Set *) objD), - Functor (* Top.8375 Top.8376 Top.8379 Set *) C D -> objC -> objD" -cannot be applied to the terms - "objC" : "Type (* Top.8375 *)" - "C" : "Category (* Top.8375 Top.8376 *) objC" - "Type (* Set *)" : "Type (* Set+1 *)" - "TypeCat (* Top.8379 Set *)" : "Category (* Top.8379 Set *) Set" - "F'" : "FunctorToType (* Top.8375 Top.8376 Top.8379 Set *) C" - "SetGrothendieckC (* Top.8375 Top.8376 Top.8379 *) G" : "objC" -The 5th term has type "FunctorToType (* Top.8375 Top.8376 Top.8379 Set *) C" -which should be coercible to - "Functor (* Top.8375 Top.8376 Top.8379 Set *) C TypeCat (* Top.8379 Set *)". - *) -End SetGrothendieckCoercion. -- cgit v1.2.3