coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] universe inconsistency

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] universe inconsistency
Date: Wed, 25 Dec 2019 12:15:54 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=oXyIYZ0rDIPWZ/GAxF2CRggjcsKg+/cP7b0PfPjmcvw=; b=VeBPL4e/Bt+VIUD6LrzUj/Q6bBwUBlrNvUn7r1ilhJ7ZUnRXTG1rQejaXGWN4ZrTSFNqFdry7auH7mibubyz/oyU6hAYpCGb3UHvm3ZXkx7Y+sGHRWMqH4zUpNkp3epEGxuDO+DfSHr1bA/1BCbZAU0oJT5tTWfvHfy3TF4yrq9FCY/vrtObGfcxwauHtoYwlUAGvN497h5MMSqgtuNDxfKzo+6IcH3ImURBo9TuZp7iydPP/E+DD30ujd5GCfQttcH6lO3iYDrfElEePX6Xtg2NIyM1KjEa/PuplJy2d2IBGKKsC4YVAOJMnMbtyHuDxaStrVUl34ba74eVxmKD4g==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=XJQgP0UX+nSsGe31nsTuPMjxROz/8ee8rY9pdCQDWp1p4panMl7Au3WOw5Uq6HAD/v/pwx0d4SXWJOKWGo8yZM+CyIVLiLlbMthM3d3zAbSzzx/FZ/NV2cMVwneo/fGe/w0NOa4bwXPFo7T96MbZyWBKSwME6Zosuy68CK8EyYhXNsF64FJAauRln0c9JDVCfAkb9DG8qerqEuT+FxlIsWtYl+x0O87yP/Si9YPw0FlgRsCmSSrUEmexk9Ei7rZ208OKjNv6YBu/MUKYfSoltuy+eJanT1z+sM2WAAUdlu+i3lNjOXmrGD9M7XmDfUrkFM/oeGFNg50RdU3MhTaETA==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:970pZBHd+E9cPx/Oq1r/yZ1GYnF86YWxBRYc798ds5kLTJ7yp86wAkXT6L1XgUPTWs2DsrQY0rGQ6fq8Ejdfqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba58IRmsswndqMYbjYRsJ6sz1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrhK/qRJi347aboKbNPtica3SctwXXnZBUd1LWiBdHo+wc4kCAuwcNuhYtYn9oF4OoAO6CwayHuPg1DpIh3/r1qM0yesgHxrG3AsmH9kTt3naqMv6NL0MXuCwzKjE1zvNYOlY2Dfm74jIdAssruuKXbJta8be11QgFx7fglqKtIzoJjWY3fkDvWic6upvT+Ovi2g/pgxyozWj3Mcsio7Hh48T11vK9j15zZ46KNGkUkJ3fMKoHZlKuy2HOYZ7Q9kuTmV1tCoixbALvYS3cDUOxZkn3RLSafyKf5KK7x77WuaePzR1iG5gdb+6hhu/8kutx+z5W8S0zlpFtTFKn9zXuX8R0xHT5M2KSvVn8UqiwzmC0R3Y5PteLkAuj6XbLoYswr4umZoXtkTOBjP7l0vrgqOKa0ko4++m5ev6brn/oZ+TLJF7hhv5MqQzhsywGuM4MhUIX2eG4+i8zKfj/UrlQLpUkvI2jqjZsJfcJcgBoa65HhNV0oIk6xa4DDeqysgXnX4CLF5deRKHiZbmO03WLf33EfuzmUmgnCtpyvzcI7HsDJTAImLHnbv8Zbp97lRTyAs3zdBR/ZJUDbQBLer3VEDvrtzXEBo5Mgyuz+jpEtp82JgeWWWJAqKCKqzSt0KI6vgxLOaReY8ZoizyK+U96/70kXA5gUMdfbWu3ZYPdH+4Ge1mL1yFbnron9cOCnwHvhE+TezvkF2NSyRfZ3e0X6Im5zE0EpiqDYnZRtPlvLvUliy8B9hdYn1MIlGKC3bhMYueEb9YYyWLZ8RljzYsVL67SoZn2wv45yHgzL8yDOfO9ygJ/b7qy8Ny4aWHtxwo+DllSeiUzHqKSUl9mH5OSjMrmqli9x8ugmyf2LR11qQLXedY4OlEB19jaczsitdiAtW3YTrvO8+TQQ/8ENygHHc8Qs93ysJcOx8gSeXntQjK2m+RO5FQl7GPA8BroIvh5CCoYuNQkjPB3qRniEQ6SMxSM2HgnrR46wXYG4/OlQOeirqucqMfmiXK8TXalDvcjARjSAd1FJ79czUab0rSo87+4xqYHbaoFPIqPhYHwNPQc6Y=

Hi,

I've got the following error message

The term "rr" has type
"(rel (list W) -> rel (list W) -> Type@{Top.890}) -> Type@{Top.889}"
while it is expected to have type
"(rel (list W) -> rel (list W) -> Type@{k4.86}) -> Type@{Top.897}"
(universe inconsistency: Cannot enforce k4.86 <= Top.890 because Top.890
< Top.688 <= gstep.624 = k4.86).

How do I find out why Coq wants Top.890 < Top.688 and Top.688 <=
gstep.624 and gstep.624 = k4.86 ?

Is this the sort of error which is likely to be solved by putting
Set Universe Polymorphism? (When I tried this it led to errors
elsewhere so I didn't pursue this idea).

Thanks

Jeremy Dawson

[Coq-Club] universe inconsistency, Jeremy Dawson, 12/25/2019