Stream: Coq devs & plugin devs

Topic: Unsoundness with module subtyping and Prop-squashing


view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 07:41):

Is this the first unsoundness bug of the year? https://github.com/coq/coq/issues/15838

view this post on Zulip Guillaume Melquiond (Mar 21 2022 at 07:44):

Does it go through coqchk?

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 07:45):

it doesn't seem so

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 07:46):

but you can probably write an example from within a module that will confuse coqchk

view this post on Zulip Guillaume Melquiond (Mar 21 2022 at 07:46):

Also, since when can we put inductive types inside module types? I though this was not supported.

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 07:46):

this has always been the case and is responsible for 90% of the module complexity

view this post on Zulip Paolo Giarrusso (Mar 21 2022 at 07:47):

Should this delay 8.15.1 which was planned for today? If not, you might need 8.15.2.

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 07:47):

not sure how to fix this in a nice way

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 07:48):

the best fix for the dev is to prohibit Prop ⊆ Type in module subtyping but it may be used out there

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 07:48):

so, that's not the best fix for the user

view this post on Zulip Paolo Giarrusso (Mar 21 2022 at 07:48):

That’d forbid Axiom foo : Type -> Definition foo : Prop., but you don’t need _that_…

view this post on Zulip Paolo Giarrusso (Mar 21 2022 at 07:50):

But if your module type has a concrete inductive, needing originality in the module seems… less fundamental?

view this post on Zulip Guillaume Melquiond (Mar 21 2022 at 07:51):

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.

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 07:51):

@Guillaume Melquiond what's forbidden is to implement a definition in an interface with an inductive

view this post on Zulip Paolo Giarrusso (Mar 21 2022 at 07:51):

_maybe_ declaring your inductive in Type and defining it in Set has potential use-cases, but even that might not be common?

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 07:51):

but you can implement a inductive with an inductive and you will get (now clearly unsound) subtyping

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 07:52):

@Paolo Giarrusso I think that I'll go for the simplest fix and assess the breakage

view this post on Zulip Paolo Giarrusso (Mar 21 2022 at 07:53):

my 2 cents: I’d have thought “disable all subtyping across _inductives_ in module types/modules” would be the simplest fix.

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 07:57):

you can probably still wreak havoc through encodings via definitions

view this post on Zulip Gaëtan Gilbert (Mar 21 2022 at 09:34):

Pierre-Marie Pédrot said:

not sure how to fix this in a nice way

just do https://github.com/coq/coq/pull/15839

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 09:40):

probably the simplest indeed (we discussed this with @Matthieu Sozeau)

view this post on Zulip Guillaume Melquiond (Mar 21 2022 at 09:46):

Do we need equality of sorts? Or could a variance be sufficient? (Just trying to reduce the potential amount of breakage.)

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 09:47):

Elimination of inductive types is contravariant so this must be at least so, so invariant is the best we can do


Last updated: Feb 02 2023 at 13:03 UTC