Is this the first unsoundness bug of the year? https://github.com/coq/coq/issues/15838
Does it go through coqchk
?
it doesn't seem so
but you can probably write an example from within a module that will confuse coqchk
Also, since when can we put inductive types inside module types? I though this was not supported.
this has always been the case and is responsible for 90% of the module complexity
Should this delay 8.15.1 which was planned for today? If not, you might need 8.15.2.
not sure how to fix this in a nice way
the best fix for the dev is to prohibit Prop ⊆ Type in module subtyping but it may be used out there
so, that's not the best fix for the user
That’d forbid Axiom foo : Type
-> Definition foo : Prop.
, but you don’t need _that_…
But if your module type has a concrete inductive, needing originality in the module seems… less fundamental?
Pierre-Marie Pédrot said:
this has always been the case and is responsible for 90% of the module complexity
Interesting. Because in Interval, I have the following piece of code, and it was certainly to work around Coq's inability to handle inductive types in modules:
Inductive f_interval (A : Type) : Type := ...
Module FloatInterval (F : ...).
Definition type := f_interval F.type.
@Guillaume Melquiond what's forbidden is to implement a definition in an interface with an inductive
_maybe_ declaring your inductive in Type
and defining it in Set
has potential use-cases, but even that might not be common?
but you can implement a inductive with an inductive and you will get (now clearly unsound) subtyping
@Paolo Giarrusso I think that I'll go for the simplest fix and assess the breakage
my 2 cents: I’d have thought “disable all subtyping across _inductives_ in module types/modules” would be the simplest fix.
you can probably still wreak havoc through encodings via definitions
Pierre-Marie Pédrot said:
not sure how to fix this in a nice way
just do https://github.com/coq/coq/pull/15839
probably the simplest indeed (we discussed this with @Matthieu Sozeau)
Do we need equality of sorts? Or could a variance be sufficient? (Just trying to reduce the potential amount of breakage.)
Elimination of inductive types is contravariant so this must be at least so, so invariant is the best we can do
Last updated: Oct 13 2024 at 01:02 UTC