Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_4627.v Sprache: Coq

Original von: Coq^©

Class sa (A:Type) := { }.

Record predicate A (sa:sa A) :=
  { pred_fun: A->Prop }.
Record ABC : Type :=
  { abc: Type }.
Record T :=
  { T_abc: ABC }.

(*
sa: forall _ : Type@{Top.179}, Prop
predicate: forall (A : Type@{Top.205}) (_ : sa A), Type@{max(Set+1, Top.205)}
T: Type@{Top.208+1}
ABC: Type@{Top.208+1}
abc: forall _ : ABC, Type@{Top.208}

Top.205 <= Top.179   predicate <= sa.A
Set < Top.208        Set < abc
Set < Top.205        Set < predicate
*)

Definition foo : predicate T (Build_sa T) :=
    {| pred_fun:= fun w => True |}.
(* *)
(* Top.208 < Top.205   <--- added by foo *)
(* *)

Check predicate nat (Build_sa nat).
(*

The issue is that the template polymorphic universe of [predicate], Top.205, does not get replaced with the universe of [nat] in the above line.
  -Jason Gross

8.5          -- predicate nat (Build_sa nat): Type@{max(Set+1, Top.205)}
8.5 EXPECTED -- predicate nat (Build_sa nat): Type@{Set+1}
8.4pl4       -- predicate nat {| |}: Type (* max(Set, (Set)+1) *)
*)

(* This works in 8.4pl4 and SHOULD work in 8.5 *)
Definition bar : ABC :=
  {| abc:= predicate nat (Build_sa nat) |}.
(*
The term "predicate nat (Build_sa nat)" has type
"Type@{max(Set+1, Top.205)}"
while it is expected to have type "Type@{Top.208}"
(universe inconsistency: Cannot enforce Top.205 <=
Top.208 because Top.208 < Top.205).
*)

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.