Stream: Coq devs & plugin devs

Topic: Universe incompatibility from MetaCoq and Iris


view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 11:41):

Pierre-Marie Pédrot said:

and in the long run, the Metacoq-vs-Iris catastrophe is in the tubes

@Pierre-Marie Pédrot you mean https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 and https://github.com/coq-community/coq-ext-lib/pull/123#discussion_r784960565 ?

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:45):

yep

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 11:47):

@Jason Gross showed how one might fight universe inference there, but if Notation "@ 'fmap' M becomes necessary I can't help thinking there must be a better way

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:48):

that particular issue is about template poly, but the same kind of problem may arise from arbitrary use of mono universes

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:48):

it's a manifestation of "the global universe state is not modular"

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:50):

(here despite the appearances, template polymorphism is helping precisely because it provides a poor-man universe polymorphism)

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 11:51):

TLDR for others: Coq's template polymorphism can't really deal with Monad list

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:53):

... but it can with Monad (fun A => list A) (don't ask, don't tell)

view this post on Zulip Kenji Maillard (Jan 24 2022 at 11:54):

Do I understand correctly that in these issues around universe levels for lists making the list inductive universe polymorphic would provide a theoretical solution ? In practice it may not be feasible because 1) it requires changing the stdlib and 2) it will probably break many developments (because of tactics incompatibilities, performance...). Am I overlooking other issues ?

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 11:55):

@Kenji Maillard correct

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 11:57):

the usual alternative is eta-expanding list, but here you'd have to eta-expand occurrences generated by both TC search and by Haskell-style programming. Jason's trick convinced me that you could get something done with enough effort, but it involves things like Notation "@ 'fmap' M := (@fmap (fun T => M T)). so it's not very ergonomic.

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 12:00):

and I'm not entirely sure why Coq can't automatically eta-expand partially-applied list, is it just that it's not transparent and would break clients anyway?

view this post on Zulip Gaëtan Gilbert (Jan 24 2022 at 12:09):

it could be implemented but the work needs to be done
and it has to be done in unclear how many places
note that it's not just eta-expand, it's eta-expand with fresh universes


Last updated: Feb 05 2023 at 23:30 UTC