From d6ce38cc3aa469446bad73dea3915ed9443751bd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 20 Jun 2014 15:06:47 +0200 Subject: Fixed some HoTT bugs, provide a proper error message when giving an ill-formed universe instance. --- library/universes.ml | 11 +++++++--- pretyping/pretyping.ml | 17 ++++++++++----- test-suite/bugs/closed/3374.v | 51 +++++++++++++++++++++++++++++++++++++++++++ test-suite/bugs/closed/3375.v | 48 ++++++++++++++++++++++++++++++++++++++++ test-suite/bugs/opened/3372.v | 2 +- test-suite/bugs/opened/3373.v | 15 ------------- test-suite/bugs/opened/3374.v | 50 ------------------------------------------ test-suite/bugs/opened/3375.v | 48 ---------------------------------------- 8 files changed, 120 insertions(+), 122 deletions(-) create mode 100644 test-suite/bugs/closed/3374.v create mode 100644 test-suite/bugs/closed/3375.v delete mode 100644 test-suite/bugs/opened/3373.v delete mode 100644 test-suite/bugs/opened/3374.v delete mode 100644 test-suite/bugs/opened/3375.v diff --git a/library/universes.ml b/library/universes.ml index e2a3901bae..0699326c54 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -244,9 +244,14 @@ let fresh_instance ctx = let existing_instance ctx inst = let s = ref LMap.empty in let () = - Array.iter2 (fun u v -> - s := LMap.add v u !s) - (Instance.to_array inst) (Instance.to_array (UContext.instance ctx)) + let a1 = Instance.to_array inst + and a2 = Instance.to_array (UContext.instance ctx) in + let len1 = Array.length a1 and len2 = Array.length a2 in + if not (len1 == len2) then + Errors.errorlabstrm "Universes" + (str "Polymorphic constant expected " ++ int len2 ++ + str" levels but was given " ++ int len1) + else Array.iter2 (fun u v -> s := LMap.add v u !s) a1 a2 in LSet.empty, !s, inst let fresh_instance_from ctx inst = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1520e1a7e7..2c16c2eb35 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -275,14 +275,21 @@ let interp_universe_level_name evd = function | GSet -> evd, Univ.Level.set | GType s -> interp_universe_name evd s -let pretype_global rigid env evd gr us = +let pretype_global loc rigid env evd gr us = let evd, instance = match us with | None -> evd, None | Some l -> - let evd, l' = List.fold_left (fun (evd, univs) l -> - let evd, l = interp_universe_level_name evd l in - (evd, l :: univs)) (evd, []) l + let _, ctx = Universes.unsafe_constr_of_global gr in + let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in + let len = Array.length arr in + if len != List.length l then + user_err_loc (loc, "pretype", + str "Universe instance should have length " ++ int len) + else + let evd, l' = List.fold_left (fun (evd, univs) l -> + let evd, l = interp_universe_level_name evd l in + (evd, l :: univs)) (evd, []) l in evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) in @@ -302,7 +309,7 @@ let pretype_ref loc evdref env ref us = variables *) Pretype_errors.error_var_not_found_loc loc id) | ref -> - let evd, c = pretype_global univ_flexible env !evdref ref us in + let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in let ty = Retyping.get_type_of env evd c in make_judge c ty diff --git a/test-suite/bugs/closed/3374.v b/test-suite/bugs/closed/3374.v new file mode 100644 index 0000000000..3c67703a2b --- /dev/null +++ b/test-suite/bugs/closed/3374.v @@ -0,0 +1,51 @@ +(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 331 lines to 59 lines *) + +Set Universe Polymorphism. +Axiom admit : forall {T}, T. +Notation paths := identity . +Definition UU := Set. +Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) . +Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) . +Definition hProp := sigT (fun X : Type => admit). +Definition hProptoType := @projT1 _ _ : hProp -> Type . +Coercion hProptoType: hProp >-> Sortclass. +Definition UU' := Type. +Definition hSet:= sigT (fun X : UU' => admit) . +Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type. +Coercion pr1hSet: hSet >-> Sortclass. +Axiom hsubtypes : UU -> Type. +Definition hrel ( X : UU ) := X -> X -> hProp. +Axiom hreldirprod : forall { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ), hrel ( dirprod X Y ) . +Axiom iseqclass : forall { X : UU } ( R : hrel X ) ( A : hsubtypes X ), Type. +Definition setquot { X : UU } ( R : hrel X ) : Type := sigT (fun A => iseqclass R A). +Axiom dirprodtosetquot : forall { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ), + setquot ( hreldirprod RX RY ). +Definition iscomprelfun2 { X Y : UU } ( R : hrel X ) ( f : X -> X -> Y ) + := forall x x' x0 x0' : X , R x x' -> R x0 x0' -> paths ( f x x0 ) ( f x' x0' ) . +Axiom setquotuniv : forall { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> Y ) ( c : setquot R ), Y . +Definition setquotuniv2 { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> X -> Y ) ( is : iscomprelfun2 R f ) ( c c0 : setquot R ) +: Y . +Proof. + intros . + set ( RR := hreldirprod R R ) . + apply (setquotuniv RR Y admit). + apply (dirprodtosetquot R R). + apply dirprodpair; [ exact c | exact c0 ]. + Undo. + exact (dirprodpair c c0). +Defined. + (* Toplevel input, characters 39-40: +Error: +In environment +X : UU +R : hrel X +Y : hSet +f : X -> X -> Y +is : iscomprelfun2 R f +c : setquot R +c0 : setquot R +RR := hreldirprod R R : hrel (dirprod X X) +The term "c" has type "setquot R" while it is expected to have type +"?42" (unable to find a well-typed instantiation for +"?42": cannot unify"Type" and "UU"). + *) diff --git a/test-suite/bugs/closed/3375.v b/test-suite/bugs/closed/3375.v new file mode 100644 index 0000000000..fe323fcb28 --- /dev/null +++ b/test-suite/bugs/closed/3375.v @@ -0,0 +1,48 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-impredicative-set") -*- *) +(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 330 lines to 45 lines *) + +Set Universe Polymorphism. +Axiom admit : forall {T}, T. +Definition UU := Set. +Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) . +Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) . +Definition hProp := sigT (fun X : Type => admit). +Axiom hProppair : forall ( X : UU ) ( is : admit ), hProp. +Definition hProptoType := @projT1 _ _ : hProp -> Type . +Coercion hProptoType: hProp >-> Sortclass. +Definition ishinh_UU ( X : UU ) : UU := forall P: Set, ( ( X -> P ) -> P ). +Definition ishinh ( X : UU ) : hProp := hProppair ( ishinh_UU X ) admit. +Definition hsubtypes ( X : UU ) : Type := X -> hProp. +Axiom carrier : forall { X : UU } ( A : hsubtypes X ), Type. +Definition hrel ( X : UU ) : Type := X -> X -> hProp. +Set Printing Universes. +Definition iseqclass { X : UU } ( R : hrel X ) ( A : hsubtypes X ) : Type. + intros; exact ( dirprod ( ishinh ( carrier A ) ) ( dirprod ( forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) + ( forall x1 x2 : X, A x1 -> A x2 -> R x1 x2 ) )) . +Defined. +Definition iseqclassconstr' { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 : ishinh ( carrier A ) ) + ( ax1 : forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( ax2 : forall x1 x2 : X, A x1 -> A x2 -> R x1 x2 ) : iseqclass R A. + intros. + apply dirprodpair. { exact ax0. } + apply dirprodpair. { exact ax1. } {exact ax2. } +Defined. +Definition iseqclassconstr { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 : ishinh ( carrier A ) ) + ( ax1 : forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( ax2 : forall x1 x2 : X, A x1 -> A x2 -> R x1 x2 ) : iseqclass R A. + pose @iseqclassconstr'. + intros. + exact (dirprodpair ax0 (dirprodpair ax1 ax2)). +Defined. +(* Toplevel input, characters 15-23: +Error: Illegal application: +The term "dirprodpair" of type + "forall (X Y : UU) (x : X), (fun _ : X => Y) x -> {_ : X & Y}" +cannot be applied to the terms + "forall x1 x2 : X, R x1 x2 -> A x1 -> A x2" + : "Type@{max(Set, Top.476, Top.479)}" + "forall x1 x2 : X, A x1 -> A x2 -> R x1 x2" + : "Type@{max(Set, Top.476, Top.479)}" + "ax1" : "forall x1 x2 : X, R x1 x2 -> A x1 -> A x2" + "ax2" : "forall x1 x2 : X, A x1 -> A x2 -> R x1 x2" +The 1st term has type "Type@{max(Set, Top.476, Top.479)}" +which should be coercible to "UU". + *) diff --git a/test-suite/bugs/opened/3372.v b/test-suite/bugs/opened/3372.v index 41ee400fd9..13ce75b84c 100644 --- a/test-suite/bugs/opened/3372.v +++ b/test-suite/bugs/opened/3372.v @@ -1,5 +1,5 @@ Set Universe Polymorphism. Definition hProp : Type := sigT (fun _ : Type => True). -Fail Goal hProp@{Set}. (* Toplevel input, characters 15-32: +Goal hProp@{Set}. (* Toplevel input, characters 15-32: Anomaly: Uncaught exception Invalid_argument("Array.iter2", _). Please report. *) diff --git a/test-suite/bugs/opened/3373.v b/test-suite/bugs/opened/3373.v deleted file mode 100644 index 8b3b515678..0000000000 --- a/test-suite/bugs/opened/3373.v +++ /dev/null @@ -1,15 +0,0 @@ -(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 332 lines to 21 lines *) -Set Universe Polymorphism. -Axiom admit : forall {T}, T. -Definition UU := Set. -Definition UU' := Type. -Definition hSet:= sigT (fun X : UU' => admit) . -Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type. -Coercion pr1hSet: hSet >-> Sortclass. -Axiom binop : UU -> Type. -Axiom setwithbinop : Type. -Definition pr1setwithbinop : setwithbinop -> hSet. -Fail exact ( @projT1 _ ( fun X : hSet@{i j} => binop X ) ). -(* Toplevel input, characters 15-69: -Anomaly: apply_coercion_args: mismatch between arguments and coercion. -Please report. *) diff --git a/test-suite/bugs/opened/3374.v b/test-suite/bugs/opened/3374.v deleted file mode 100644 index 8a62838f06..0000000000 --- a/test-suite/bugs/opened/3374.v +++ /dev/null @@ -1,50 +0,0 @@ -(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 331 lines to 59 lines *) - -Set Universe Polymorphism. -Axiom admit : forall {T}, T. -Notation paths := identity . -Definition UU := Set. -Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) . -Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) . -Definition hProp := sigT (fun X : Type => admit). -Definition hProptoType := @projT1 _ _ : hProp -> Type . -Coercion hProptoType: hProp >-> Sortclass. -Definition UU' := Type. -Definition hSet:= sigT (fun X : UU' => admit) . -Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type. -Coercion pr1hSet: hSet >-> Sortclass. -Axiom hsubtypes : UU -> Type. -Definition hrel ( X : UU ) := X -> X -> hProp. -Axiom hreldirprod : forall { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ), hrel ( dirprod X Y ) . -Axiom iseqclass : forall { X : UU } ( R : hrel X ) ( A : hsubtypes X ), Type. -Definition setquot { X : UU } ( R : hrel X ) : Type := sigT (fun A => iseqclass R A). -Axiom dirprodtosetquot : forall { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ), - setquot ( hreldirprod RX RY ). -Definition iscomprelfun2 { X Y : UU } ( R : hrel X ) ( f : X -> X -> Y ) - := forall x x' x0 x0' : X , R x x' -> R x0 x0' -> paths ( f x x0 ) ( f x' x0' ) . -Axiom setquotuniv : forall { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> Y ) ( c : setquot R ), Y . -Definition setquotuniv2 { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> X -> Y ) ( is : iscomprelfun2 R f ) ( c c0 : setquot R ) -: Y . -Proof. - intros . - set ( RR := hreldirprod R R ) . - apply (setquotuniv RR Y admit). - apply (dirprodtosetquot R R). - apply dirprodpair; [ exact c | exact c0 ]. - Undo. - Fail exact (dirprodpair c c0). - (* Toplevel input, characters 39-40: -Error: -In environment -X : UU -R : hrel X -Y : hSet -f : X -> X -> Y -is : iscomprelfun2 R f -c : setquot R -c0 : setquot R -RR := hreldirprod R R : hrel (dirprod X X) -The term "c" has type "setquot R" while it is expected to have type -"?42" (unable to find a well-typed instantiation for -"?42": cannot unify"Type" and "UU"). - *) diff --git a/test-suite/bugs/opened/3375.v b/test-suite/bugs/opened/3375.v deleted file mode 100644 index 9cb43413b3..0000000000 --- a/test-suite/bugs/opened/3375.v +++ /dev/null @@ -1,48 +0,0 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-impredicative-set") -*- *) -(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 330 lines to 45 lines *) - -Set Universe Polymorphism. -Axiom admit : forall {T}, T. -Definition UU := Set. -Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) . -Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) . -Definition hProp := sigT (fun X : Type => admit). -Axiom hProppair : forall ( X : UU ) ( is : admit ), hProp@{Set i}. -Definition hProptoType := @projT1 _ _ : hProp -> Type . -Coercion hProptoType: hProp >-> Sortclass. -Definition ishinh_UU ( X : UU ) : UU := forall P: Set, ( ( X -> P ) -> P ). -Definition ishinh ( X : UU ) : hProp := hProppair ( ishinh_UU X ) admit. -Definition hsubtypes ( X : UU ) : Type := X -> hProp. -Axiom carrier : forall { X : UU } ( A : hsubtypes X ), Type. -Definition hrel ( X : UU ) : Type := X -> X -> hProp. -Set Printing Universes. -Definition iseqclass { X : UU } ( R : hrel X ) ( A : hsubtypes X ) : Type. - intros; exact ( dirprod ( ishinh ( carrier A ) ) ( dirprod ( forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) - ( forall x1 x2 : X, A x1 -> A x2 -> R x1 x2 ) )) . -Defined. -Definition iseqclassconstr' { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 : ishinh ( carrier A ) ) - ( ax1 : forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( ax2 : forall x1 x2 : X, A x1 -> A x2 -> R x1 x2 ) : iseqclass R A. - intros. - apply dirprodpair. { exact ax0. } - apply dirprodpair. { exact ax1. } {exact ax2. } -Defined. -Definition iseqclassconstr { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 : ishinh ( carrier A ) ) - ( ax1 : forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( ax2 : forall x1 x2 : X, A x1 -> A x2 -> R x1 x2 ) : iseqclass R A. - pose @iseqclassconstr'. - intros. - exact (dirprodpair ax0 (dirprodpair ax1 ax2)). -Fail Defined. -(* Toplevel input, characters 15-23: -Error: Illegal application: -The term "dirprodpair" of type - "forall (X Y : UU) (x : X), (fun _ : X => Y) x -> {_ : X & Y}" -cannot be applied to the terms - "forall x1 x2 : X, R x1 x2 -> A x1 -> A x2" - : "Type@{max(Set, Top.476, Top.479)}" - "forall x1 x2 : X, A x1 -> A x2 -> R x1 x2" - : "Type@{max(Set, Top.476, Top.479)}" - "ax1" : "forall x1 x2 : X, R x1 x2 -> A x1 -> A x2" - "ax2" : "forall x1 x2 : X, A x1 -> A x2 -> R x1 x2" -The 1st term has type "Type@{max(Set, Top.476, Top.479)}" -which should be coercible to "UU". - *) -- cgit v1.2.3