From 779fd5d9a4982b19fd257b61f444ae8e6155dcbe Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 14 Mar 2016 19:50:29 +0100 Subject: Fix bug when a sort is ascribed to a Record Forcefully equating it to the inferred level is not always desirable or possible. --- test-suite/success/univers.v | 17 +++++++++++++++++ toplevel/record.ml | 13 +++++++------ 2 files changed, 24 insertions(+), 6 deletions(-) diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index e00701fb6..269359ae6 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -60,3 +60,20 @@ Qed. (* Submitted by Danko Ilik (bug report #1507); related to LetIn *) Record U : Type := { A:=Type; a:A }. + +(** Check assignement of sorts to inductives and records. *) + +Variable sh : list nat. + +Definition is_box_in_shape (b :nat * nat) := True. +Definition myType := Type. + +Module Ind. +Inductive box_in : myType := + myBox (coord : nat * nat) (_ : is_box_in_shape coord) : box_in. +End Ind. + +Module Rec. +Record box_in : myType := + BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }. +End Rec. \ No newline at end of file diff --git a/toplevel/record.ml b/toplevel/record.ml index 04da628c3..200d1a938 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -140,12 +140,13 @@ let typecheck_params_and_fields def id pl t ps nots fs = arity, evars else let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in - if Univ.is_small_univ univ then - (* We can assume that the level aritysort is not constrained - and clear it. *) - mkArity (ctx, Sorts.sort_of_univ univ), - Evd.set_eq_sort env_ar evars (Prop Pos) aritysort - else arity, evars + if Univ.is_small_univ univ && + Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars aritysort) then + (* We can assume that the level in aritysort is not constrained + and clear it, if it is flexible *) + mkArity (ctx, Sorts.sort_of_univ univ), + Evd.set_eq_sort env_ar evars (Prop Pos) aritysort + else arity, evars in let evars, nf = Evarutil.nf_evars_and_universes evars in let newps = map_rel_context nf newps in -- cgit v1.2.3