Since 8.10, AAC Tactics had a universe constraint issue when reasoning over lists with elements in Type
(and presumably other parameterized datatypes). Tactics like aac_reflexivity
succeeded but Qed
failed with universe mismatch error (described here).
By experimentation, I came up with a solution that makes the main test case with lists pass. However, it uses monomorphic universes nontrivially, and I don't know if there is a more general solution (if I use explicit universe polymorphism I get Anomaly "new_monomorphic_global raised an error ..."
).
Any chance some universe expert could review the PR? https://github.com/coq-community/aac-tactics/pull/112
At best this is a workaround, tactics should never generate ill-typed terms.
Most probably the OCaml code of AAC forgets some constraints
sure, the best fix would be at the OCaml level, but this code was originally written 10+ years ago and is likely not known very well by anyone anymore... I just try to solve the worst issues for users when I can.
so if we can agree on that the PR at least doesn't make anything worse or is fundamentally broken, I think it's reasonable to merge. Recall that AAC is in Coq's CI and the Platform, so everyone will have to live with it for a while.
one effect of the PR is that this can become Type
again...
Could it be the lift_reflexivity
which is missing a tclRETYPE
so that its inner universe constraints are propagated?
@Hugo Herbelin possibly. Fabian wrote about tclRETYPE
before (https://github.com/coq-community/aac-tactics/issues/36):
The ocaml-function Coq.retype (and Coq.tclRETYPE in #34 ) are used at various points. This has to do with the plugin building coq-terms without updating universe constrains (I guess?). This seems very fishy and like an ugly hack.
if you give an example how to add tclRETYPE
to lift_reflexivity
I can try that in a new PR
every time you build an application in OCaml you should check that the universe constraints are properly handled
it's a bit violent to type every thing at sight (I've been removing a lot of useless retyping last week for performance reasons, it doesn't scale at all)
I tried Hugo's advice and it seems to work: https://github.com/coq-community/aac-tactics/pull/113
Good that it works.
Pierre-Marie Pédrot said:
it's a bit violent to type every thing at sight (I've been removing a lot of useless retyping last week for performance reasons, it doesn't scale at all)
Yes, it is a lot of useless retyping, as what we only need here a priori is to ensure that the first argument in Type
infers a constraint. The advantage is that it is easy to do fix with the current AAC architecture. (Case by case, we could work on each different mkApp(Coq.get_efresh ..., carrier)
pattern and infer the constraint on the carrier, but that would require more time.)
In the case of AAC I don't think it's the major source of performance issues, so probably not very important in first approximation
am I reading it right that tclRETYPE
could potentially do wasteful work? Worth opening an issue in AAC to remember?
Yes, this function retypes the whole term. So if you call it recursively, expect some blowups on big terms
but last time I had a look, AAC was struggling orders of magnitudes worse with TC resolution
(anyone up to reimplementing AAC with CS?)
the better approach may be to reimplement AAC using Enrico's planned tabled TC resolution?
I think https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrAC.v solves an important part of what AAC does already using CS
that is, I think many applications don't require the full "modulo AC" so "with AC" suffices
In the same vein, there is applys_eq
from TLC, which, combined with ring
should give something similar. Would be good if someone can make a synthesis of these ideas.
Last updated: Oct 13 2024 at 01:02 UTC