From b8834d66013b38cef247507f312bb081de04da27 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 17 Jun 2014 11:18:10 +0200
Subject: Existing Class now works with universe polymorphism. Fixes HoTT bug
 #063

---
 pretyping/typeclasses.ml              |  7 ++++---
 test-suite/bugs/closed/HoTT_coq_063.v | 34 ++++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/HoTT_coq_063.v | 26 --------------------------
 3 files changed, 38 insertions(+), 29 deletions(-)
 create mode 100644 test-suite/bugs/closed/HoTT_coq_063.v
 delete mode 100644 test-suite/bugs/opened/HoTT_coq_063.v

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 8364387783..dd09d5b29a 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -403,9 +403,9 @@ let add_class cl =
 
 
 open Declarations
-(* FIXME: deal with universe instances *)
+
 let add_constant_class cst =
-  let ty = Typeops.type_of_constant_in (Global.env ()) (cst,Univ.Instance.empty) in
+  let ty = Universes.unsafe_type_of_global (ConstRef cst) in
   let ctx, arity = decompose_prod_assum ty in
   let tc = 
     { cl_impl = ConstRef cst;
@@ -420,9 +420,10 @@ let add_inductive_class ind =
   let mind, oneind = Global.lookup_inductive ind in
   let k =
     let ctx = oneind.mind_arity_ctxt in
+    let inst = Univ.UContext.instance mind.mind_universes in
     let ty = Inductive.type_of_inductive_knowing_parameters
       (push_rel_context ctx (Global.env ()))
-      ((mind,oneind),Univ.Instance.empty)
+      ((mind,oneind),inst)
       (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx))
     in
       { cl_impl = IndRef ind;
diff --git a/test-suite/bugs/closed/HoTT_coq_063.v b/test-suite/bugs/closed/HoTT_coq_063.v
new file mode 100644
index 0000000000..777f6483d5
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_063.v
@@ -0,0 +1,34 @@
+Set Universe Polymorphism.
+Module A.
+  Inductive paths A (x : A) : A -> Type := idpath : paths A x x.
+
+  Notation "x = y" := (paths _ x y).
+
+  Inductive IsTrunc : nat -> Type -> Type :=
+  | BuildContr : forall A (center : A) (contr : forall y, center = y), IsTrunc 0 A
+  | trunc_S : forall A n, (forall x y : A, IsTrunc n (x = y)) -> IsTrunc (S n) A.
+
+  Existing Class IsTrunc.
+
+
+  Instance is_trunc_unit : IsTrunc 0 unit.
+  Proof. apply BuildContr with (center:=tt). now intros []. Defined.
+
+  Check (_ : IsTrunc 0 unit).
+End A.
+
+Module B.
+  Fixpoint IsTrunc (n : nat) (A : Type) : Type :=
+    match n with
+      | O => True
+      | S _ => False
+    end.
+
+  Existing Class IsTrunc.
+
+  Instance is_trunc_unit : IsTrunc 0 unit.
+  Proof. exact I. Defined.
+
+  Check (_ : IsTrunc 0 unit).
+  Fail Definition foo := (_ : IsTrunc 1 unit).
+End B.
diff --git a/test-suite/bugs/opened/HoTT_coq_063.v b/test-suite/bugs/opened/HoTT_coq_063.v
deleted file mode 100644
index 8656fadaa9..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_063.v
+++ /dev/null
@@ -1,26 +0,0 @@
-Set Universe Polymorphism.
-Module A.
-  Inductive paths A (x : A) : A -> Type := idpath : paths A x x.
-
-  Notation "x = y" := (paths _ x y).
-
-  Inductive IsTrunc : nat -> Type -> Type :=
-  | BuildContr : forall A (center : A) (contr : forall y, center = y), IsTrunc 0 A
-  | trunc_S : forall A n, (forall x y : A, IsTrunc n (x = y)) -> IsTrunc (S n) A.
-
-  Fail Existing Class IsTrunc.
-  (* Anomaly: Mismatched instance and context when building universe substitution.
-Please report. *)
-End A.
-
-Module B.
-  Fixpoint IsTrunc (n : nat) (A : Type) : Type :=
-    match n with
-      | O => True
-      | S _ => False
-    end.
-
-  Fail Existing Class IsTrunc.
-  (* Anomaly: Mismatched instance and context when building universe substitution.
-Please report. *)
-End B.
-- 
cgit v1.2.3