search

smtcoq / sniper

Other
33 stars 6 forks source link

Sniper is incompatible with QuickChick (universe inconsistency involving MetaCoq) #4

Open anton-trunov opened 3 years ago

anton-trunov commented 3 years ago

The following snippet

From QuickChick Require Import QuickChick.
From Sniper Require Import Sniper.

produces an error:

Error: Universe inconsistency. Cannot enforce Coq.Relations.Relation_Definitions.1
<= MetaCoq.Template.Induction.180 because MetaCoq.Template.Induction.180
<= MetaCoq.Template.Induction.173 <= MetaCoq.Template.utils.All_Forall.163
<= MetaCoq.Template.utils.All_Forall.232 <= MetaCoq.Template.utils.All_Forall.393
< Coq.Relations.Relation_Definitions.1.

This can be narrowed down further to

From QuickChick Require Import Sets.
From Sniper Require Import Sniper.

i.e. to this file in QuickChick: https://github.com/QuickChick/QuickChick/blob/master/src/Sets.v, but it's harder to try and pinpoint the issue because Sets.v uses Mathcomp and there there is a notation clash between Mathcomp's ssrnotations module (imported implicitly) and Sniper, I'll report this as a separate issue.

Tested with Coq 8.13.2, Sniper dev (commit d6a451a3), QuickChick dev (commit 80f4c88e).