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 ?
@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
that particular issue is about template poly, but the same kind of problem may arise from arbitrary use of mono universes
it's a manifestation of "the global universe state is not modular"
(here despite the appearances, template polymorphism is helping precisely because it provides a poor-man universe polymorphism)
TLDR for others: Coq's template polymorphism can't really deal with
... but it can with
Monad (fun A => list A) (don't ask, don't tell)
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 ?
@Kenji Maillard correct
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.
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?
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