Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix coq#11039: proof of False with template poly and nonlinear universes
Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes coq#10504.
- Loading branch information
1 parent
d7879b8
commit a5d124d
Showing
10 changed files
with
145 additions
and
19 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
Inductive any_list {A} := | ||
| nil : @any_list A | ||
| cons : forall X, A -> @any_list X -> @any_list A. | ||
|
||
Arguments nil {A}. | ||
Arguments cons {A X}. | ||
|
||
Notation "[]" := (@nil Type). | ||
Notation "hd :: tl" := (cons hd tl). | ||
|
||
Definition xs := true :: 2137 :: false :: 0 :: []. | ||
Fail Definition ys := xs :: xs. | ||
|
||
(* Goal ys = ys. produced an anomaly "Unable to handle arbitrary u+k <= v constraints" *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
(* this bug was a proof of False *) | ||
|
||
(* when we require template poly Coq recognizes that it's not allowed *) | ||
Fail #[universes(template)] | ||
Inductive foo@{i} (A:Type@{i}) : Type@{i+1} := bar (X:Type@{i}) : foo A. | ||
|
||
(* variants with letin *) | ||
Fail #[universes(template)] | ||
Inductive foo@{i} (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar (X:T) : foo A. | ||
|
||
Fail #[universes(template)] | ||
Record foo@{i} (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar { X:T }. | ||
|
||
|
||
(* no implicit template poly, no explicit universe annotations *) | ||
Inductive foo (A:Type) := bar X : foo X -> foo A | nonempty. | ||
Arguments nonempty {_}. | ||
|
||
Fail Check foo nat : Type@{foo.u0}. | ||
(* template poly didn't activate *) | ||
|
||
Definition U := Type. | ||
Definition A : U := foo nat. | ||
|
||
Fail Definition down : U -> A := fun u => bar nat u nonempty. | ||
(* this is the one where it's important that it fails *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters