The Coq mailing list

[Jesper Bengtson <jebe AT itu.dk>]

Dear Matthieu,

Thank you so much. The patch did not work for some reason, but I saw what it 
was trying to do, added the line to reduction.ml and now Coq has stopped 
complaining. I realise that I am on shaky ground but at least this will allow 
me to continue working for the time being.

Cheers, and thanks again.

/Jesper

On 24 Oct 2013, at 16:07, Matthieu Sozeau 
<mattam AT mattam.org>
 wrote:

> Le 24 oct. 2013 à 10:37, Jesper Bengtson 
> <jebe AT itu.dk>
>  a écrit :
> 
>> Dear Coq club,
> 
> Dear Jesper,
> 
>> In my current development of separation logic I rely heavily on type 
>> classes, in a very similar style to work by Spitters et al. I run into 
>> similar problems that they did that universe inconsistencies crop up quite 
>> regularly. I find these exceptionally difficult to debug. Coq will readily 
>> tell me which the offending types are, but to infer the circle (or find 
>> out which definitions use these types) the only way that I have found is 
>> to print the universes and manually check the levels and for large 
>> developments this doesn't really work.
> 
> Indeed, it's a hard issue. There has been improvements already in the trunk 
> version, which gives you the cycle in full if you allow printing of 
> universes (not in all cases, as [apply] unification hides universe 
> inconsistencies for example).
> 
>> I understand that a lot of work has recently gone into fixing this for the 
>> HoTT crowd, and I was wondering if any of this is making it into the 
>> standard Coq distribution.
> 
> It is planned to be merged with the trunk soon and will be part of the next 
> release.
> 
>> For the moment, I would be absolutely fine with an option to just disable 
>> the universe checking. To my mind this is analogous to an admit -- it's 
>> not something that should be in the end product, but it's perfectly fine 
>> to use for development purposes. There was a patch to this effect for Coq 
>> 8.3pl3. Is there something similar now?
> 
> Here is a patch for 8.4 if you need it, use at your own risk.
> -- Matthieu
> 
> Index: kernel/reduction.ml
> ===================================================================
> --- kernel/reduction.ml       (révision 16347)
> +++ kernel/reduction.ml       (copie de travail)
> @@ -196,6 +196,7 @@
>          | CUMUL -> enforce_geq u2 u1 cuniv)
>     | (_, _) -> raise NotConvertible
> 
> +let sort_cmp pb s0 s1 cuniv = cuniv
> 
> let conv_sort env s0 s1 = sort_cmp CONV s0 s1 empty_constraint
> 
> 
> 
>