Clean-up around substitution of globals #8971
Conversation
maximedenes
requested review from
herbelin,
mattam82,
ppedrot and
silene
as code owners
coqbot
added
the
needs: rebase
Kernel code should not silently drop universe instances.
maximedenes
force-pushed
the
clean-subst-global
branch
from
2efc553
to
4a49ec0
Compare
coqbot
removed
the
needs: rebase
Unfortunately, the most dangerous cases are when we don't inline, and |
|
In order to resolve cleanly the universe poly vs inlining tension, I experimented removing functor inlining, and improving support for aliases in tactics instead. I went pretty far, but I'd need an answer to #5301, to make hints not rely on inlining. |
| if c'==c then ref else ConstructRef c' | ||
|
|
||
| let subst_global subst ref = match ref with | ||
| | VarRef var -> ref, mkVar var | ||
| | ConstRef kn -> | ||
| let kn',t = subst_con_kn subst kn in | ||
| let kn',t = subst_con subst (Univ.in_punivs kn) in |
There was a problem hiding this comment.
This should have some XXX TODO universes comment.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
I talked too quickly. Reading the discussions, #8974 seems a very good direction.
| @@ -192,7 +192,7 @@ let subst_cl_typ subst ct = match ct with | |||
| let c' = subst_proj_repr subst c in | |||
| if c' == c then ct else CL_PROJ c' | |||
| | CL_CONST c -> | |||
| let c',t = subst_con_kn subst c in | |||
| let c',t = subst_con subst (Univ.in_punivs c) in | |||
There was a problem hiding this comment.
Should have a comment XXX TODO FIXME univs
| @@ -156,7 +156,7 @@ let cache_head o = | |||
|
|
|||
| let subst_head_approximation subst = function | |||
| | RigidHead (RigidParameter cst) as k -> | |||
| let cst,c = subst_con_kn subst cst in | |||
| let cst,c = subst_con subst (Univ.in_punivs cst) in | |||
I don't think there's a tension, we just need to update the code. |
There was a problem hiding this comment.
LGTM modulo the changes mentioned by @SkySkimmer. There is a call to subst_global in tacsubst.ml that can be removed as well, it triggers a warning that is not removable and not using the warning system, so it's better to just get rid of this check.
|
I think I prefer #8974 , but even better if we can really fix the problems. |
|
Closing in favor of #8974. |
We clean up the kernel API to not expose unsafe combinators (that silently insert dummy universe instances).
This is related to #8951 but does not solve it per se. It just makes the problem more visible on the user side (in that case,
library/heads.ml).